awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Groupoid.{v₂, u₂} E
F : Functor.{v, v₁, u, u₁} C D
G : Functor.{v₁, v₂, u₁, u₂} D E
hΦ : (of C ⋙ map F) ⋙ lift G = F ⋙ G
hΦ₁ : (F ⋙ of D) ⋙ lift G = F ⋙ G
⊢ of C ⋙ map F ⋙ lift G = F ⋙ G
have hΦ₂ : F ⋙ of D ⋙ lift G = F ⋙ G
Tactic: rw [← Functor.assoc, of_comp_map, Functor.assoc, lift_spec G]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Groupoid.{v₂, u₂} E
F : Functor.{v, v₁, u, u₁} C D
G : Functor.{v₁, v₂, u₁, u₂} D E
hΦ : (of C ⋙ map F) ⋙ lift G = F ⋙ G
hΦ₁ : (F ⋙ of D) ⋙ lift G = F ⋙ G
hΦ₂ : F ⋙ of D ⋙ lift G = F ⋙ G
⊢ of C ⋙ map F ⋙ lift G = F ⋙ G
have hΦ₃ : F ⋙ G = F ⋙ G
Tactic: rw [← Functor.assoc, of_comp_map, Functor.assoc, lift_spec G]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Grpd.Basic (goal)
Goal:
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
w : ∀ (j : J), m ≫ (piLimitFan F).proj j = s.proj j
⊢ m =
    (fun (s : Limits.Fan F) ↦
        (Functor.pi' (C := fun (j : J) ↦ (↑(F j) : Type u)) fun (j : J) ↦ s.proj j :
          (↑s.pt : Type u) ⥤ ((i : J) → (↑(F i) : Type u))))
      s
have h : ∀ (i : J),
  m ⋙ Pi.eval (fun (i : J) ↦ (↑(F i) : Type u)) i =
    Functor.comp (D := (i : J) → (↑(F i) : Type u))
      ((fun (s : Limits.Fan F) ↦
          (Functor.pi' (C := fun (j : J) ↦ (↑(F j) : Type u)) fun (j : J) ↦ s.proj j :
            (↑s.pt : Type u) ⥤ ((i : J) → (↑(F i) : Type u))))
        s)
      (Pi.eval (fun (i : J) ↦ (↑(F i) : Type u)) i)
Tactic: apply Functor.pi_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Grpd.Basic (hypothesis)
Goal:
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
w : ∀ (j : J), m ≫ (piLimitFan F).proj j = s.proj j
j : J
⊢ m ⋙ Pi.eval (fun (i : J) ↦ (↑(F i) : Type u)) j =
    Functor.comp (D := (i : J) → (↑(F i) : Type u))
      ((fun (s : Limits.Fan F) ↦
          (Functor.pi' (C := fun (j : J) ↦ (↑(F j) : Type u)) fun (j : J) ↦ s.proj j :
            (↑s.pt : Type u) ⥤ ((i : J) → (↑(F i) : Type u))))
        s)
      (Pi.eval (fun (i : J) ↦ (↑(F i) : Type u)) j)
have w₁ : m ≫ (piLimitFan F).proj j = s.proj j
Tactic: specialize w j
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Grpd.Basic (goal)
Goal:
J : Type u
f : J → Grpd
j : J
⊢ (piIsoPi J f).hom ≫ Limits.Pi.π f j = Pi.eval (fun (i : J) ↦ (↑(f i) : Type u)) j
have simp : (piLimitFan f).π.app { as := j } = Pi.eval (fun (i : J) ↦ (↑(f i) : Type u)) j
Tactic: simp [piIsoPi]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d : C
f : c ⟶ d
⊢ Groupoid.inv f ∈ S.arrows d c ↔ f ∈ S.arrows c d
have mp : Groupoid.inv f ∈ S.arrows d c → f ∈ S.arrows c d
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d : C
f : c ⟶ d
mp : Groupoid.inv f ∈ S.arrows d c → f ∈ S.arrows c d
⊢ Groupoid.inv f ∈ S.arrows d c ↔ f ∈ S.arrows c d
have mpr : f ∈ S.arrows c d → Groupoid.inv f ∈ S.arrows d c
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ f ≫ g ∈ S.arrows c e ↔ g ∈ S.arrows d e
have mp : f ≫ g ∈ S.arrows c e → g ∈ S.arrows d e
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
mp : f ≫ g ∈ S.arrows c e → g ∈ S.arrows d e
⊢ f ≫ g ∈ S.arrows c e ↔ g ∈ S.arrows d e
have mpr : g ∈ S.arrows d e → f ≫ g ∈ S.arrows c e
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
h : f ≫ g ∈ S.arrows c e
⊢ g ∈ S.arrows d e
have mp : Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e
Tactic: suffices Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e by
      simpa only [inv_eq_inv, IsIso.inv_hom_id_assoc] using this
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ≫ g ∈ S.arrows c e ↔ f ∈ S.arrows c d
have mp : f ≫ g ∈ S.arrows c e → f ∈ S.arrows c d
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
mp : f ≫ g ∈ S.arrows c e → f ∈ S.arrows c d
⊢ f ≫ g ∈ S.arrows c e ↔ f ∈ S.arrows c d
have mpr : f ∈ S.arrows c d → f ≫ g ∈ S.arrows c e
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
⊢ f ∈ S.arrows c d
have mp : (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d
Tactic: suffices (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d by
      simpa only [inv_eq_inv, IsIso.hom_inv_id, Category.comp_id, Category.assoc] using this
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c : C
γ : c ⟶ c
hγ : γ ∈ S.arrows c c
⊢ 𝟙 c ∈ S.arrows c c
have h : 𝟙 c = γ ≫ Groupoid.inv γ
Tactic: convert! S.mul hγ (S.inv hγ)
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
hcd :
  S.hom.obj (Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) =
    S.hom.obj (Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd)
⊢ Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc = Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd
have simp : c = d
Tactic: simp only [Subtype.mk_eq_mk]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S_1 x x_1 : Subgroupoid.{u, u_1} C
S : (c d : C) → Set (c ⟶ d)
inv : ∀ {c d : C} {p : c ⟶ d}, p ∈ S c d → Groupoid.inv p ∈ S d c
mul : ∀ {c d e : C} {p : c ⟶ d}, p ∈ S c d → ∀ {q : d ⟶ e}, q ∈ S d e → p ≫ q ∈ S c e
T : (c d : C) → Set (c ⟶ d)
inv_1 : ∀ {c d : C} {p : c ⟶ d}, p ∈ T c d → Groupoid.inv p ∈ T d c
mul_1 : ∀ {c d e : C} {p : c ⟶ d}, p ∈ T c d → ∀ {q : d ⟶ e}, q ∈ T d e → p ≫ q ∈ T c e
h :
  (↑{ arrows := S, inv := @inv, mul := @mul : Subgroupoid.{u, u_1} C } : Set ((c : C) × (d : C) × (c ⟶ d))) =
    (↑{ arrows := T, inv := @inv_1, mul := @mul_1 } : Set ((c : C) × (d : C) × (c ⟶ d)))
⊢ { arrows := S, inv := @inv, mul := @mul : Subgroupoid.{u, u_1} C } = { arrows := T, inv := @inv_1, mul := @mul_1 }
have arrows : ∀ (c d : C) (f : c ⟶ d),
  f ∈ { arrows := S, inv := @inv, mul := @mul : Subgroupoid.{u, u_1} C }.arrows c d ↔
    f ∈ { arrows := T, inv := @inv_1, mul := @mul_1 : Subgroupoid.{u, u_1} C }.arrows c d
Tactic: ext c d f
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S T : Subgroupoid.{u, u_1} C
⊢ S ≤ T ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d
have rw : (∀ (a : C) (b : (d : C) × (a ⟶ d)),
    Sigma.mk (β := fun (a : C) ↦ (d : C) × (a ⟶ d)) a b ∈ S → Sigma.mk (β := fun (a : C) ↦ (d : C) × (a ⟶ d)) a b ∈ T) ↔
  ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d
Tactic: rw [SetLike.le_def, Sigma.forall]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
s : Set (Subgroupoid.{u, u_1} C)
c d : C
p : c ⟶ d
hp : Membership.mem (γ := Set (c ⟶ d)) (⋂ S ∈ s, S.arrows c d) p
⊢ Membership.mem (γ := Set (d ⟶ c)) (⋂ S ∈ s, S.arrows d c) (Groupoid.inv p)
have rw : ∀ (hp : ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), p ∈ i.arrows c d) (i : Subgroupoid.{u, u_1} C) (j : i ∈ s),
  Groupoid.inv p ∈ i.arrows d c
Tactic: rw [mem_iInter₂] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
s : Set (Subgroupoid.{u, u_1} C)
c d e : C
p : c ⟶ d
hp : Membership.mem (γ := Set (c ⟶ d)) (⋂ S ∈ s, S.arrows c d) p
x : d ⟶ e
hq : Membership.mem (γ := Set (d ⟶ e)) (⋂ S ∈ s, S.arrows d e) x
⊢ Membership.mem (γ := Set (c ⟶ e)) (⋂ S ∈ s, S.arrows c e) (p ≫ x)
have rw : ∀ (hp : ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), p ∈ i.arrows c d) (x : d ⟶ e)
  (hq : ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), x ∈ i.arrows d e) (i : Subgroupoid.{u, u_1} C) (j : i ∈ s),
  p ≫ x ∈ i.arrows c e
Tactic: rw [mem_iInter₂] at hp hq ⊢
Cleared hypotheses: hp, x, hq
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
⊢ ∀ (s : Set (Subgroupoid.{u, u_1} C)), IsGLB s (sInf s)
have refine_1 : ∀ (s : Set (Subgroupoid.{u, u_1} C)) (S : Subgroupoid.{u, u_1} C) (Ss : S ∈ s), ∀ F ∈ sInf s, F ∈ S
Tactic: refine fun s => ⟨fun S Ss F => ?_, fun T Tl F fT => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
refine_1 : ∀ (s : Set (Subgroupoid.{u, u_1} C)) (S : Subgroupoid.{u, u_1} C) (Ss : S ∈ s), ∀ F ∈ sInf s, F ∈ S
⊢ ∀ (s : Set (Subgroupoid.{u, u_1} C)), IsGLB s (sInf s)
have refine_2 : ∀ (s : Set (Subgroupoid.{u, u_1} C)) (T : Subgroupoid.{u, u_1} C) (Tl : T ∈ lowerBounds s)
  (F : (c : C) × (d : C) × (c ⟶ d)) (fT : F ∈ T), F ∈ sInf s
Tactic: refine fun s => ⟨fun S Ss F => ?_, fun T Tl F fT => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S_1 : Subgroupoid.{u, u_1} C
s : Set (Subgroupoid.{u, u_1} C)
S : Subgroupoid.{u, u_1} C
Ss : S ∈ s
F : (c : C) × (d : C) × (c ⟶ d)
⊢ F ∈ sInf s → F ∈ S
have refine_1 : (∀ S ∈ s, F ∈ S) → F ∈ S
Tactic: simp only [mem_sInf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
s : Set (Subgroupoid.{u, u_1} C)
T : Subgroupoid.{u, u_1} C
Tl : T ∈ lowerBounds s
F : (c : C) × (d : C) × (c ⟶ d)
fT : F ∈ T
⊢ F ∈ sInf s
have refine_2 : ∀ S ∈ s, F ∈ S
Tactic: simp only [mem_sInf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S T : Subgroupoid.{u, u_1} C
h : S ≤ T
s t : (↑S.objs : Type u)
x x_1 : s ⟶ t
f : (↑s : C) ⟶ (↑t : C)
hf : Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) f
g : (↑s : C) ⟶ (↑t : C)
hg : Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) g
⊢ Eq.{u_1 + 1} (α := (inclusion h).obj s ⟶ (inclusion h).obj t)
      ((fun (f : s ⟶ t) ↦ (inclusion h).map f)
        (Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
          Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) f hf))
      ((fun (f : s ⟶ t) ↦ (inclusion h).map f)
        (Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
          Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) g hg)) →
    Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) f hf =
      Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) g hg
have dsimp : Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
      Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (T.arrows (↑s : C) (↑t : C)) x) f sorry =
    Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
      Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (T.arrows (↑s : C) (↑t : C)) x) g sorry →
  Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
      Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) f hf =
    Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
      Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) g hg
Tactic: dsimp only [inclusion]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S T : Subgroupoid.{u, u_1} C
h : S ≤ T
s t : (↑S.objs : Type u)
x x_1 : s ⟶ t
f : (↑s : C) ⟶ (↑t : C)
hf : Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) f
g : (↑s : C) ⟶ (↑t : C)
hg : Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) g
⊢ Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (T.arrows (↑s : C) (↑t : C)) x) f ⋯ =
      Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (T.arrows (↑s : C) (↑t : C)) x) g ⋯ →
    Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) f hf =
      Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) g hg
have rw : f = g → f = g
Tactic: rw [Subtype.mk_eq_mk, Subtype.mk_eq_mk]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d : C
⊢ Membership.mem (γ := Set (c ⟶ c)) {p : c ⟶ c | Discrete.Arrows c c p} (Groupoid.inv (𝟙 c))
have simp : Membership.mem (γ := Set (c ⟶ c)) {p : c ⟶ c | Discrete.Arrows c c p} (𝟙 c)
Tactic: simp only [inv_eq_inv, IsIso.inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d_1 d : C
⊢ Membership.mem (γ := Set (c ⟶ c)) {p : c ⟶ c | Discrete.Arrows c c p} (𝟙 c ≫ 𝟙 c)
have rw : Membership.mem (γ := Set (c ⟶ c)) {p : c ⟶ c | Discrete.Arrows c c p} (𝟙 c)
Tactic: rw [Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
⊢ S.IsWide ↔ S.objs = univ
have mp : S.IsWide → S.objs = univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
mp : S.IsWide → S.objs = univ
⊢ S.IsWide ↔ S.objs = univ
have mpr : S.objs = univ → S.IsWide
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.IsWide
⊢ S.objs = univ
have mp : ∀ (x : C), x ∈ S.objs ↔ Membership.mem (γ := Set C) univ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.IsWide
x : C
⊢ x ∈ S.objs ↔ Membership.mem (γ := Set C) univ x
have mp : x ∈ S.objs → Membership.mem (γ := Set C) univ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.IsWide
x : C
mp : x ∈ S.objs → Membership.mem (γ := Set C) univ x
⊢ x ∈ S.objs ↔ Membership.mem (γ := Set C) univ x
have mp₁ : Membership.mem (γ := Set C) univ x → x ∈ S.objs
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.IsWide
x : C
⊢ Membership.mem (γ := Set C) univ x → x ∈ S.objs
have mp : x ∈ S.objs
Tactic: simp only [mem_univ, imp_true_iff, forall_true_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.objs = univ
⊢ S.IsWide
have mpr : ∀ (c : C), 𝟙 c ∈ S.arrows c c
Tactic: refine ⟨fun c => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.objs = univ
c : C
⊢ 𝟙 c ∈ S.arrows c c
have mpr : ∀ (γ : c ⟶ c) (γS : γ ∈ S.arrows c c), 𝟙 c ∈ S.arrows c c
Tactic: obtain ⟨γ, γS⟩ := (le_of_eq h.symm : ⊤ ⊆ S.objs) (Set.mem_univ c)
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sw : S.IsWide
c d : C
h : c = d
⊢ eqToHom h ∈ S.arrows c d
have refl : eqToHom sorry ∈ S.arrows c c
Tactic: cases h
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sw : S.IsWide
c : C
⊢ eqToHom ⋯ ∈ S.arrows c c
have refl : 𝟙 c ∈ S.arrows c c
Tactic: simp only [eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
c d : C
p : d ⟶ c
γ : c ⟶ c
hs : γ ∈ S.arrows c c
⊢ p ≫ γ ≫ Groupoid.inv p ∈ S.arrows d d
have h : p = Groupoid.inv (Groupoid.inv p)
Tactic: convert! Sn.conj (Groupoid.inv p) hs
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
c d : C
p : c ⟶ d
⊢ BijOn (fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) (S.arrows c c) (S.arrows d d)
have refine_1 : ∀ γ₁ ∈ S.arrows c c,
  ∀ γ₂ ∈ S.arrows c c,
    ∀
      (h :
        Eq.{u_1 + 1} (α := d ⟶ d) ((fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) γ₁)
          ((fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) γ₂)),
      γ₁ = γ₂
Tactic: refine ⟨fun γ γS => Sn.conj p γS, fun γ₁ _ γ₂ _ h => ?_, fun δ δS =>
    ⟨p ≫ δ ≫ Groupoid.inv p, Sn.conj' p δS, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
c d : C
p : c ⟶ d
refine_1 :
  ∀ γ₁ ∈ S.arrows c c,
    ∀ γ₂ ∈ S.arrows c c,
      ∀
        (h :
          Eq.{u_1 + 1} (α := d ⟶ d) ((fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) γ₁)
            ((fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) γ₂)),
        γ₁ = γ₂
⊢ BijOn (fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) (S.arrows c c) (S.arrows d d)
have refine_2 : ∀ (δ : d ⟶ d) (δS : δ ∈ S.arrows d d), (fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) (p ≫ δ ≫ Groupoid.inv p) = δ
Tactic: refine ⟨fun γ γS => Sn.conj p γS, fun γ₁ _ γ₂ _ h => ?_, fun δ δS =>
    ⟨p ≫ δ ≫ Groupoid.inv p, Sn.conj' p δS, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
s : Set (Subgroupoid.{u, u_1} C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ (c : C), 𝟙 c ∈ (sInf s).arrows c c
have simp_rw : ∀ (c : C) (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), 𝟙 c ∈ i.arrows c c
Tactic: simp_rw [sInf, mem_iInter₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
s : Set (Subgroupoid.{u, u_1} C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c}, γ ∈ (sInf s).arrows c c → Groupoid.inv p ≫ γ ≫ p ∈ (sInf s).arrows d d
have simp_rw : ∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c},
  (∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), γ ∈ i.arrows c c) →
    ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), Groupoid.inv p ≫ γ ≫ p ∈ i.arrows d d
Tactic: simp_rw [sInf, mem_iInter₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
γ : c ⟶ c
hγ : Membership.mem (γ := Set (c ⟶ c)) (arrows discrete c c) γ
⊢ Membership.mem (γ := Set (d ⟶ d)) (arrows discrete d d) (Groupoid.inv f ≫ γ ≫ f)
have id : Membership.mem (γ := Set (d ⟶ d)) (arrows discrete d d) (Groupoid.inv f ≫ 𝟙 c ≫ f)
Tactic: cases hγ
Cleared hypotheses: γ, hγ
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
⊢ Membership.mem (γ := Set (d ⟶ d)) (arrows discrete d d) (Groupoid.inv f ≫ 𝟙 c ≫ f)
have id : Membership.mem (γ := Set (d ⟶ d)) (arrows discrete d d) (𝟙 d)
Tactic: simp only [inv_eq_inv, Category.id_comp, IsIso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
c : C
cS : c ∈ S.objs
x : c ⟶ c
hx : x ∈ S.vertexSubgroup cS
y : c ⟶ c
⊢ y * x * y⁻¹ ∈ S.vertexSubgroup cS
have rw : y * (x * y⁻¹) ∈ S.vertexSubgroup cS
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
c d : C
⊢ X c d ⊆
    ⋂ (S : Subgroupoid.{u, u_1} C),
      ⋂ (_ :
        Membership.mem (γ := Set (Subgroupoid.{u, u_1} C))
          {S : Subgroupoid.{u, u_1} C | ∀ (c d : C), X c d ⊆ S.arrows c d} S),
        S.arrows c d
have simp : ∀ (i : Subgroupoid.{u, u_1} C)
  (j :
    Membership.mem (γ := Set (Subgroupoid.{u, u_1} C)) {S : Subgroupoid.{u, u_1} C | ∀ (c d : C), X c d ⊆ S.arrows c d}
      i),
  X c d ⊆ i.arrows c d
Tactic: simp only [subset_iInter₂_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
⊢ generated X ≤ generatedNormal X
have h : Subset (α := Set (Subgroupoid.{u, u_1} C))
  {S : Subgroupoid.{u, u_1} C | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ S.IsNormal}
  {S : Subgroupoid.{u, u_1} C | ∀ (c d : C), X c d ⊆ S.arrows c d}
Tactic: apply @sInf_le_sInf (Subgroupoid C) _
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
⊢ generatedNormal X ≤ S ↔ ∀ (c d : C), X c d ⊆ S.arrows c d
have mp : generatedNormal X ≤ S → ∀ (c d : C), X c d ⊆ S.arrows c d
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
mp : generatedNormal X ≤ S → ∀ (c d : C), X c d ⊆ S.arrows c d
⊢ generatedNormal X ≤ S ↔ ∀ (c d : C), X c d ⊆ S.arrows c d
have mpr : (∀ (c d : C), X c d ⊆ S.arrows c d) → generatedNormal X ≤ S
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (hypothesis)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
h : generatedNormal X ≤ S
c d : C
⊢ X c d ⊆ S.arrows c d
have h' : generated X ≤ generatedNormal X
Tactic: have h' := generated_le_generatedNormal X
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
h : generatedNormal X ≤ S
c d : C
h' : generated X ≤ generatedNormal X
⊢ X c d ⊆ S.arrows c d
have mp : ∀ (h : ∀ {c d : C}, (generatedNormal X).arrows c d ⊆ S.arrows c d) (c d : C)
  (h' : ∀ {c d : C}, (generated X).arrows c d ⊆ (generatedNormal X).arrows c d), X c d ⊆ S.arrows c d
Tactic: rw [le_iff] at h h'
Cleared hypotheses: h, c, d, h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
h : ∀ (c d : C), X c d ⊆ S.arrows c d
⊢ generatedNormal X ≤ S
have mpr : Membership.mem (γ := Set (Subgroupoid.{u, u_1} C))
  {S : Subgroupoid.{u, u_1} C | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ S.IsNormal} S
Tactic: apply @sInf_le (Subgroupoid C) _