awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
⊢ Membership.mem (γ := Set (φ.obj c ⟶ φ.obj c')) ((im φ hφ).arrows (φ.obj c) (φ.obj c')) g
have rw : Membership.mem (γ := Set (φ.obj c ⟶ φ.obj c')) (arrows ⊤ (φ.obj c) (φ.obj c')) g
Tactic: rw [hφ']
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (hypothesis)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
⊢ Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
    (Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g)
have this : Membership.mem (γ := Set (φ.obj c ⟶ φ.obj c')) ((im φ hφ).arrows (φ.obj c) (φ.obj c')) g
Tactic: have : g ∈ (im φ hφ).arrows (φ.obj c) (φ.obj c') := by rw [hφ']; trivial
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (hypothesis)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
this : Membership.mem (γ := Set (φ.obj c ⟶ φ.obj c')) ((im φ hφ).arrows (φ.obj c) (φ.obj c')) g
⊢ Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
    (Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g)
have this₁ : ∃ (a : C) (b : C) (g_1 : a ⟶ b) (ha : φ.obj a = φ.obj c) (hb : φ.obj b = φ.obj c'),
  g = eqToHom sorry ≫ φ.map g_1 ≫ eqToHom hb
Tactic: rw [mem_im_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
this :
  ∃ (a : C) (b : C) (g_1 : a ⟶ b) (ha : φ.obj a = φ.obj c) (hb : φ.obj b = φ.obj c'),
    g = eqToHom ⋯ ≫ φ.map g_1 ≫ eqToHom hb
⊢ Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
    (Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g)
have refl : ∀ (b b' : C) (f : b ⟶ b') (hb : φ.obj b = φ.obj c) (hb' : φ.obj b' = φ.obj c'),
  Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
    (Groupoid.inv (eqToHom sorry ≫ φ.map f ≫ eqToHom hb') ≫
      (eqToHom sorry ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom sorry ≫ φ.map f ≫ eqToHom hb')
Tactic: obtain ⟨b, b', f, hb, hb', _, hf⟩ := this
Cleared hypotheses: g, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' b b' : C
f : b ⟶ b'
hb : φ.obj b = φ.obj c
hb' : φ.obj b' = φ.obj c'
⊢ Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
    (Groupoid.inv (eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb') ≫
      (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb')
have refl : ∀ (f : c ⟶ b') (hb : φ.obj c = φ.obj c),
  Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
    (Groupoid.inv (eqToHom sorry ≫ φ.map f ≫ eqToHom hb') ≫
      (eqToHom sorry ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom sorry ≫ φ.map f ≫ eqToHom hb')
Tactic: cases hφ hb
Cleared hypotheses: b, f, hb
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' b' : C
hb' : φ.obj b' = φ.obj c'
f : c ⟶ b'
hb : φ.obj c = φ.obj c
⊢ Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
    (Groupoid.inv (eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb') ≫
      (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb')
have refl : ∀ (hb' : φ.obj c' = φ.obj c') (f : c ⟶ c'),
  Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
    (Groupoid.inv (eqToHom sorry ≫ φ.map f ≫ eqToHom hb') ≫
      (eqToHom sorry ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom sorry ≫ φ.map f ≫ eqToHom hb')
Tactic: cases hφ hb'
Cleared hypotheses: b', hb', f
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c')
    (Groupoid.inv (eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb') ≫
      (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb')
have refl : Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)
Tactic: simp only [eqToHom_refl, Category.comp_id, Category.id_comp, inv_eq_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)
have refl : Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map (Groupoid.inv f ≫ γ ≫ f))
Tactic: suffices Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map <| Groupoid.inv f ≫ γ ≫ f) by
        simp only [inv_eq_inv, Functor.map_comp, Functor.map_inv] at this; exact this
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map (Groupoid.inv f ≫ γ ≫ f))
have refl : Groupoid.inv f ≫ γ ≫ f ∈ S.arrows c' 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
⊢ S.IsTotallyDisconnected ↔ ∀ (c d : C), (S.arrows c d).Nonempty → c = d
have mp : S.IsTotallyDisconnected → ∀ (c d : C), (S.arrows c d).Nonempty → 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
mp : S.IsTotallyDisconnected → ∀ (c d : C), (S.arrows c d).Nonempty → c = d
⊢ S.IsTotallyDisconnected ↔ ∀ (c d : C), (S.arrows c d).Nonempty → c = d
have mpr : (∀ (c d : C), (S.arrows c d).Nonempty → c = d) → S.IsTotallyDisconnected
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 : ∀ (c d : C), (S.arrows c d).Nonempty → c = d
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
f : (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶ (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)
fS :
  Membership.mem (γ :=
    Set
      ((↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶
        (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)))
    (S.arrows (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C)
      (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C))
    f
⊢ Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc = Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd
have mpr : 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 : Subgroupoid.{u, u_1} C
⊢ S.disconnect ≤ S
have rw : ∀ {c d : C}, S.disconnect.arrows c d ⊆ S.arrows c d
Tactic: rw [le_iff]
-- 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.disconnect.IsTotallyDisconnected
have rw : ∀ (c d : C), (S.disconnect.arrows c d).Nonempty → c = d
Tactic: rw [isTotallyDisconnected_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
D : Set C
c : C
⊢ c ∈ objs.{u, u_1} (full D) ↔ c ∈ D
have rw : c ∈ D ↔ c ∈ D
Tactic: rw [full_objs]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
⊢ Eq (α := Subgroupoid.{u, u_1} C) (full ∅) ⊥
have arrows : ∀ (x x_1 : C) (x_2 : x ⟶ x_1),
  Membership.mem (γ := Set (x ⟶ x_1)) (arrows (full ∅) x x_1) x_2 ↔
    Membership.mem (γ := Set (x ⟶ x_1)) (arrows ⊥ x x_1) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
⊢ Eq (α := Subgroupoid.{u, u_1} C) (full univ) ⊤
have arrows : ∀ (x x_1 : C) (x_2 : x ⟶ x_1),
  Membership.mem (γ := Set (x ⟶ x_1)) (arrows (full univ) x x_1) x_2 ↔
    Membership.mem (γ := Set (x ⟶ x_1)) (arrows ⊤ x x_1) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
D E : Set C
h : D ≤ E
⊢ LE.le (α := Subgroupoid.{u, u_1} C) (full D) (full E)
have rw : ∀ {c d : C}, Subset.{u_1} (α := Set (c ⟶ d)) (arrows (full D) c d) (arrows (full E) c d)
Tactic: rw [le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.VertexGroup (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
γ : c ⟶ c
simp_rw simp_rw₁ : f ≫ (inv f ≫ γ ≫ f) ≫ inv f = γ
⊢ (fun (δ : d ⟶ d) ↦ f ≫ δ ≫ inv f) ((fun (γ : c ⟶ c) ↦ inv f ≫ γ ≫ f) γ) = γ
have simp_rw₂ : f ≫ inv f ≫ γ ≫ f ≫ inv f = γ
Tactic: simp_rw [Category.assoc, comp_inv, Category.comp_id, ← Category.assoc, comp_inv,
      Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.VertexGroup (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
γ : c ⟶ c
simp_rw simp_rw₁ : f ≫ (inv f ≫ γ ≫ f) ≫ inv f = γ
simp_rw₂ : f ≫ inv f ≫ γ ≫ f ≫ inv f = γ
⊢ (fun (δ : d ⟶ d) ↦ f ≫ δ ≫ inv f) ((fun (γ : c ⟶ c) ↦ inv f ≫ γ ≫ f) γ) = γ
have simp_rw₃ : f ≫ inv f ≫ γ ≫ 𝟙 c = γ
Tactic: simp_rw [Category.assoc, comp_inv, Category.comp_id, ← Category.assoc, comp_inv,
      Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.VertexGroup (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
γ : c ⟶ c
simp_rw simp_rw₁ : f ≫ (inv f ≫ γ ≫ f) ≫ inv f = γ
simp_rw₂ : f ≫ inv f ≫ γ ≫ f ≫ inv f = γ
simp_rw₃ : f ≫ inv f ≫ γ ≫ 𝟙 c = γ
⊢ (fun (δ : d ⟶ d) ↦ f ≫ δ ≫ inv f) ((fun (γ : c ⟶ c) ↦ inv f ≫ γ ≫ f) γ) = γ
have simp_rw₄ : f ≫ inv f ≫ γ = γ
Tactic: simp_rw [Category.assoc, comp_inv, Category.comp_id, ← Category.assoc, comp_inv,
      Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.VertexGroup (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
γ : c ⟶ c
simp_rw simp_rw₁ : f ≫ (inv f ≫ γ ≫ f) ≫ inv f = γ
simp_rw₂ : f ≫ inv f ≫ γ ≫ f ≫ inv f = γ
simp_rw₃ : f ≫ inv f ≫ γ ≫ 𝟙 c = γ
simp_rw₄ : f ≫ inv f ≫ γ = γ
⊢ (fun (δ : d ⟶ d) ↦ f ≫ δ ≫ inv f) ((fun (γ : c ⟶ c) ↦ inv f ≫ γ ≫ f) γ) = γ
have simp_rw₅ : (f ≫ inv f) ≫ γ = γ
Tactic: simp_rw [Category.assoc, comp_inv, Category.comp_id, ← Category.assoc, comp_inv,
      Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.VertexGroup (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
γ : c ⟶ c
simp_rw simp_rw₁ : f ≫ (inv f ≫ γ ≫ f) ≫ inv f = γ
simp_rw₂ : f ≫ inv f ≫ γ ≫ f ≫ inv f = γ
simp_rw₃ : f ≫ inv f ≫ γ ≫ 𝟙 c = γ
simp_rw₄ : f ≫ inv f ≫ γ = γ
simp_rw₅ : (f ≫ inv f) ≫ γ = γ
⊢ (fun (δ : d ⟶ d) ↦ f ≫ δ ≫ inv f) ((fun (γ : c ⟶ c) ↦ inv f ≫ γ ≫ f) γ) = γ
have simp_rw₆ : 𝟙 c ≫ γ = γ
Tactic: simp_rw [Category.assoc, comp_inv, Category.comp_id, ← Category.assoc, comp_inv,
      Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.VertexGroup (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
δ : d ⟶ d
simp_rw simp_rw₁ : inv f ≫ (f ≫ δ ≫ inv f) ≫ f = δ
⊢ (fun (γ : c ⟶ c) ↦ inv f ≫ γ ≫ f) ((fun (δ : d ⟶ d) ↦ f ≫ δ ≫ inv f) δ) = δ
have simp_rw₂ : inv f ≫ f ≫ δ ≫ inv f ≫ f = δ
Tactic: simp_rw [Category.assoc, inv_comp, ← Category.assoc, inv_comp, Category.id_comp,
      Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.VertexGroup (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
δ : d ⟶ d
simp_rw simp_rw₁ : inv f ≫ (f ≫ δ ≫ inv f) ≫ f = δ
simp_rw₂ : inv f ≫ f ≫ δ ≫ inv f ≫ f = δ
⊢ (fun (γ : c ⟶ c) ↦ inv f ≫ γ ≫ f) ((fun (δ : d ⟶ d) ↦ f ≫ δ ≫ inv f) δ) = δ
have simp_rw₃ : inv f ≫ f ≫ δ ≫ 𝟙 d = δ
Tactic: simp_rw [Category.assoc, inv_comp, ← Category.assoc, inv_comp, Category.id_comp,
      Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.VertexGroup (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
δ : d ⟶ d
simp_rw simp_rw₁ : inv f ≫ (f ≫ δ ≫ inv f) ≫ f = δ
simp_rw₂ : inv f ≫ f ≫ δ ≫ inv f ≫ f = δ
simp_rw₃ : inv f ≫ f ≫ δ ≫ 𝟙 d = δ
⊢ (fun (γ : c ⟶ c) ↦ inv f ≫ γ ≫ f) ((fun (δ : d ⟶ d) ↦ f ≫ δ ≫ inv f) δ) = δ
have simp_rw₄ : ((inv f ≫ f) ≫ δ) ≫ 𝟙 d = δ
Tactic: simp_rw [Category.assoc, inv_comp, ← Category.assoc, inv_comp, Category.id_comp,
      Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.VertexGroup (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
δ : d ⟶ d
simp_rw simp_rw₁ : inv f ≫ (f ≫ δ ≫ inv f) ≫ f = δ
simp_rw₂ : inv f ≫ f ≫ δ ≫ inv f ≫ f = δ
simp_rw₃ : inv f ≫ f ≫ δ ≫ 𝟙 d = δ
simp_rw₄ : ((inv f ≫ f) ≫ δ) ≫ 𝟙 d = δ
⊢ (fun (γ : c ⟶ c) ↦ inv f ≫ γ ≫ f) ((fun (δ : d ⟶ d) ↦ f ≫ δ ≫ inv f) δ) = δ
have simp_rw₅ : (𝟙 d ≫ δ) ≫ 𝟙 d = δ
Tactic: simp_rw [Category.assoc, inv_comp, ← Category.assoc, inv_comp, Category.id_comp,
      Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.VertexGroup (goal)
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
δ : d ⟶ d
simp_rw simp_rw₁ : inv f ≫ (f ≫ δ ≫ inv f) ≫ f = δ
simp_rw₂ : inv f ≫ f ≫ δ ≫ inv f ≫ f = δ
simp_rw₃ : inv f ≫ f ≫ δ ≫ 𝟙 d = δ
simp_rw₄ : ((inv f ≫ f) ≫ δ) ≫ 𝟙 d = δ
simp_rw₅ : (𝟙 d ≫ δ) ≫ 𝟙 d = δ
⊢ (fun (γ : c ⟶ c) ↦ inv f ≫ γ ≫ f) ((fun (δ : d ⟶ d) ↦ f ≫ δ ≫ inv f) δ) = δ
have simp_rw₆ : δ ≫ 𝟙 d = δ
Tactic: simp_rw [Category.assoc, inv_comp, ← Category.assoc, inv_comp, Category.id_comp,
      Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid (goal)
Goal:
C : Type u
inst : Groupoid.{v, u} C
X Y a b : C
f : a ⟶ b
⊢ Quiver.reverse (Quiver.reverse f) = f
have dsimp : Groupoid.inv (Groupoid.inv f) = f
Tactic: dsimp [Quiver.reverse]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid (goal)
Goal:
C : Type u_1
𝒞 : Category.{u_2, u_1} C
D : Type u
inst : Groupoid.{v, u} D
F : Functor.{u_2, v, u_1, u} C D
h : F.FullyFaithful
X Y : C
f : X ⟶ Y
⊢ h.preimage (inv (F.map f)) ≫ f = 𝟙 Y
have apply : F.map (h.preimage (inv (F.map f)) ≫ f) = F.map (𝟙 Y)
Tactic: apply h.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid (goal)
Goal:
C : Type u_1
𝒞 : Category.{u_2, u_1} C
D : Type u
inst : Groupoid.{v, u} D
F : Functor.{u_2, v, u_1, u} C D
h : F.FullyFaithful
X Y : C
f : X ⟶ Y
⊢ f ≫ h.preimage (inv (F.map f)) = 𝟙 X
have apply : F.map (f ≫ h.preimage (inv (F.map f))) = F.map (𝟙 X)
Tactic: apply h.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid (goal)
Goal:
I : Type u
J : I → Type u₂
inst : (i : I) → Groupoid.{v, u₂} (J i)
X Y : (i : I) → J i
f : X ⟶ Y
⊢ (fun (i : I) ↦ Groupoid.inv (f i)) ≫ f = 𝟙 Y
have h : ∀ (i : I), Eq.{v + 1} (((fun (i : I) ↦ Groupoid.inv (f i)) ≫ f) i) (𝟙 Y i)
Tactic: funext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid (goal)
Goal:
I : Type u
J : I → Type u₂
inst : (i : I) → Groupoid.{v, u₂} (J i)
X Y : (i : I) → J i
f : X ⟶ Y
⊢ (f ≫ fun (i : I) ↦ Groupoid.inv (f i)) = 𝟙 X
have h : ∀ (i : I), Eq.{v + 1} ((f ≫ fun (i : I) ↦ Groupoid.inv (f i)) i) (𝟙 X i)
Tactic: funext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ IsGroupoid.{v_1, u_1} C ↔ Eq (α := MorphismProperty.{v_1, u_1} C) (isomorphisms C) ⊤
have mp : IsGroupoid.{v_1, u_1} C → Eq (α := MorphismProperty.{v_1, u_1} C) (isomorphisms C) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
mp : IsGroupoid.{v_1, u_1} C → Eq (α := MorphismProperty.{v_1, u_1} C) (isomorphisms C) ⊤
⊢ IsGroupoid.{v_1, u_1} C ↔ Eq (α := MorphismProperty.{v_1, u_1} C) (isomorphisms C) ⊤
have mpr : Eq (α := MorphismProperty.{v_1, u_1} C) (isomorphisms C) ⊤ → IsGroupoid.{v_1, u_1} C
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ IsGroupoid.{v_1, u_1} C → Eq (α := MorphismProperty.{v_1, u_1} C) (isomorphisms C) ⊤
have mp : IsGroupoid.{v_1, u_1} C → LE.le (α := MorphismProperty.{v_1, u_1} C) ⊤ (isomorphisms C)
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsGroupoid.{v_1, u_1} C
⊢ LE.le (α := MorphismProperty.{v_1, u_1} C) ⊤ (isomorphisms C)
have mp : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), ⊤ f → isomorphisms C f
Tactic: _
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f : w.StructuredArrowRightwards g
⊢ ∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm : R.map a ≫ w.app X₁ ≫ B.map b = g), f = mk w g X₁ a b comm
have obtain : ∀ (g_1 : CostructuredArrow L X₃) (φ : CostructuredArrow.mk g ⟶ (w.costructuredArrowRightwards X₃).obj g_1),
  ∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm : R.map a ≫ w.app X₁ ≫ B.map b = g),
    StructuredArrow.mk φ = mk w g X₁ a b comm
Tactic: obtain ⟨g, φ, rfl⟩ := StructuredArrow.mk_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g_1 : R.obj X₂ ⟶ B.obj X₃
g : CostructuredArrow L X₃
φ : CostructuredArrow.mk g_1 ⟶ (w.costructuredArrowRightwards X₃).obj g
⊢ ∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm : R.map a ≫ w.app X₁ ≫ B.map b = g_1),
    StructuredArrow.mk φ = mk w g_1 X₁ a b comm
have obtain : ∀ (X₁ : C₁) (b : L.obj X₁ ⟶ X₃)
  (φ : CostructuredArrow.mk g_1 ⟶ (w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)),
  ∃ (X₁_1 : C₁) (a : X₂ ⟶ T.obj X₁_1) (b_1 : L.obj X₁_1 ⟶ X₃) (comm : R.map a ≫ w.app X₁_1 ≫ B.map b_1 = g_1),
    StructuredArrow.mk φ = mk w g_1 X₁_1 a b_1 comm
Tactic: obtain ⟨X₁, b, rfl⟩ := g.mk_surjective
Cleared hypotheses: g, φ
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
X₁ : C₁
b : L.obj X₁ ⟶ X₃
φ : CostructuredArrow.mk g ⟶ (w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)
⊢ ∃ (X₁_1 : C₁) (a : X₂ ⟶ T.obj X₁_1) (b_1 : L.obj X₁_1 ⟶ X₃) (comm : R.map a ≫ w.app X₁_1 ≫ B.map b_1 = g),
    StructuredArrow.mk φ = mk w g X₁_1 a b_1 comm
have obtain : ∀ (a : (CostructuredArrow.mk g).left ⟶ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).left)
  (ha : R.map a ≫ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk b)).hom = (CostructuredArrow.mk g).hom),
  ∃ (X₁_1 : C₁) (a_1 : X₂ ⟶ T.obj X₁_1) (b_1 : L.obj X₁_1 ⟶ X₃) (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b_1 = g),
    StructuredArrow.mk (CostructuredArrow.homMk a ha) = mk w g X₁_1 a_1 b_1 comm
Tactic: obtain ⟨a, ha, rfl⟩ := CostructuredArrow.homMk_surjective φ
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f : w.CostructuredArrowDownwards g
⊢ ∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm : R.map a ≫ w.app X₁ ≫ B.map b = g), f = mk w g X₁ a b comm
have obtain : ∀ (g_1 : StructuredArrow X₂ T) (φ : (w.structuredArrowDownwards X₂).obj g_1 ⟶ StructuredArrow.mk g),
  ∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm : R.map a ≫ w.app X₁ ≫ B.map b = g),
    CostructuredArrow.mk φ = mk w g X₁ a b comm
Tactic: obtain ⟨g, φ, rfl⟩ := CostructuredArrow.mk_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.GuitartExact.Basic (goal)
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g_1 : R.obj X₂ ⟶ B.obj X₃
g : StructuredArrow X₂ T
φ : (w.structuredArrowDownwards X₂).obj g ⟶ StructuredArrow.mk g_1
⊢ ∃ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁) (b : L.obj X₁ ⟶ X₃) (comm : R.map a ≫ w.app X₁ ≫ B.map b = g_1),
    CostructuredArrow.mk φ = mk w g_1 X₁ a b comm
have obtain : ∀ (X₁ : C₁) (a : X₂ ⟶ T.obj X₁)
  (φ : (w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a) ⟶ StructuredArrow.mk g_1),
  ∃ (X₁_1 : C₁) (a_1 : X₂ ⟶ T.obj X₁_1) (b : L.obj X₁_1 ⟶ X₃) (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b = g_1),
    CostructuredArrow.mk φ = mk w g_1 X₁_1 a_1 b comm
Tactic: obtain ⟨X₁, a, rfl⟩ := g.mk_surjective
Cleared hypotheses: g, φ