gaxiiiiiiiiiiii

import Mathlib.tactic
import Mathlib.CategoryTheory.Limits.HasLimits

open CategoryTheory
open Limits


structure Elm [Category.{u, v} 𝓐] (X : 𝓐ᵒᵖ ⥤ Type w) where
  obj : 𝓐
  elm : X.obj (Opposite.op obj)

gaxiiiiiiiiiiii

import Mathlib.tactic
open CategoryTheory

-- F.Full := Function.Surjective F.map
-- F.Faithful := Function.Injective F.map
-- F.FullyFaithful := Function.Bijective F.map


structure equiv (𝓐 𝓑 : Type) [Category 𝓐] [Category 𝓑] where
  func : 𝓐 ⥤ 𝓑

gaxiiiiiiiiiiii

import Mathlib.tactic

abbrev Var := Nat

structure Lang where
  Const : Type
  Func : Nat → Type
  Rel : Nat → Type

/------

gaxiiiiiiiiiiii

import Mathlib
open scoped Pointwise
open Polynomial

#check Finset.sup_le
example [inst : SemilatticeSup α] [inst_1 : OrderBot α] [DecidableEq β] {s : Finset β} {f : β → α} {a : α} :
  (∀ b ∈ s, f b ≤ a) → s.sup f ≤ a
:= by
  induction s using Finset.induction_on with
  | empty => simp

gaxiiiiiiiiiiii

論理式

ϕ, ψ := A | ⊥ | R₁ t | R₂ (t₁, t₂) | ¬ϕ | ϕ ∧ ψ | ϕ ∨ ψ | ϕ → ψ | ∀x.ϕ | ∃x.ϕ

A は命題記号
x は変数記号
t,t₁,t₂ は項
R₁は1変数述語記号
R₂は2変数述語記号

gaxiiiiiiiiiiii

import Mathlib

lemma Subgroup.IsCyclic [Group G] [HG : IsCyclic G] (H : Subgroup G)  :
  IsCyclic H
:= by
  haveI := Classical.propDecidable
  obtain ⟨g, Hg : ∀ h, ∃ k, g ^ k = h⟩ := HG
  cases' subsingleton_or_nontrivial H with H0 H0
  · rcases H0 with ⟨H0⟩
    constructor; use 1; intro h; simp

gaxiiiiiiiiiiii

import Mathlib.tactic

example [Group G] [Fintype G] (g : G) :
  Fintype.card (Subgroup.zpowers g) = orderOf g
:= by
   have : orderOf g = Fintype.card (Fin (orderOf g)) := by simp
   rw [this]
   apply Fintype.card_congr
   refine {
    toFun := λ ⟨x, Hx⟩ => by

gaxiiiiiiiiiiii

import Mathlib.tactic
import Mathlib.GroupTheory.Complement

open Classical
open scoped Pointwise

lemma Subgroup.card_not_eq [Group G] [Fintype G] (H : Subgroup G) :
  Fintype.card ↑H ≠ 0
:= by
  intro F

gaxiiiiiiiiiiii

From mathcomp Require Import ssreflect.
Require Import Nat.

Definition name := nat.

Inductive proc :=
  | Nil
  | Tau (P : proc)
  | Para (P Q : proc)
  | Sum (P Q : proc)

gaxiiiiiiiiiiii

From mathcomp Require Import ssreflect.
From Autosubst Require Import Autosubst.
Require Import Nat.

Inductive proc_ :=
  | Var (x : var)
  | Nil
  | Para (P Q : proc_)
  | Repl (P : proc_)
  | Send (M : proc_) (N : proc_) (P : proc_)