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_1 : 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
S : Subgroupoid.{u_1, u_3} D
c d : C
p : c ⟶ d
hp :
  Membership.mem (γ := Set (c ⟶ d))
    {f : c ⟶ d | Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map f)} p
⊢ Membership.mem (γ := Set (d ⟶ c))
    {f : d ⟶ c | Membership.mem (γ := Set (φ.obj d ⟶ φ.obj c)) (S.arrows (φ.obj d) (φ.obj c)) (φ.map f)}
    (Groupoid.inv p)
have rw : Membership.mem (γ := Set (φ.obj d ⟶ φ.obj c)) (S.arrows (φ.obj d) (φ.obj c)) (Groupoid.inv (φ.map p))
Tactic: rw [mem_setOf, inv_eq_inv, φ.map_inv, ← inv_eq_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : 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
S : Subgroupoid.{u_1, u_3} D
c d e : C
p : c ⟶ d
h :
  Membership.mem (γ := Set (c ⟶ d))
    {f : c ⟶ d | Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map f)} p
q : d ⟶ e
h_1 :
  Membership.mem (γ := Set (d ⟶ e))
    {f : d ⟶ e | Membership.mem (γ := Set (φ.obj d ⟶ φ.obj e)) (S.arrows (φ.obj d) (φ.obj e)) (φ.map f)} q
⊢ Membership.mem (γ := Set (c ⟶ e))
    {f : c ⟶ e | Membership.mem (γ := Set (φ.obj c ⟶ φ.obj e)) (S.arrows (φ.obj c) (φ.obj e)) (φ.map f)} (p ≫ q)
have simp : Membership.mem (γ := Set (φ.obj c ⟶ φ.obj e)) (S.arrows (φ.obj c) (φ.obj e)) (φ.map p ≫ φ.map q)
Tactic: simp only [mem_setOf, Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : 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
S : Subgroupoid.{u_1, u_3} D
c d e : C
p : c ⟶ d
h :
  Membership.mem (γ := Set (c ⟶ d))
    {f : c ⟶ d | Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map f)} p
q : d ⟶ e
h_1 :
  Membership.mem (γ := Set (d ⟶ e))
    {f : d ⟶ e | Membership.mem (γ := Set (φ.obj d ⟶ φ.obj e)) (S.arrows (φ.obj d) (φ.obj e)) (φ.map f)} q
⊢ Membership.mem (γ := Set (φ.obj c ⟶ φ.obj e)) (S.arrows (φ.obj c) (φ.obj e)) (φ.map p ≫ φ.map q)
have a : Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map p)
Tactic: apply S.mul
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : 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
S : Subgroupoid.{u_1, u_3} D
c d e : C
p : c ⟶ d
h :
  Membership.mem (γ := Set (c ⟶ d))
    {f : c ⟶ d | Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map f)} p
q : d ⟶ e
h_1 :
  Membership.mem (γ := Set (d ⟶ e))
    {f : d ⟶ e | Membership.mem (γ := Set (φ.obj d ⟶ φ.obj e)) (S.arrows (φ.obj d) (φ.obj e)) (φ.map f)} q
a : Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map p)
⊢ Membership.mem (γ := Set (φ.obj c ⟶ φ.obj e)) (S.arrows (φ.obj c) (φ.obj e)) (φ.map p ≫ φ.map q)
have a₁ : Membership.mem (γ := Set (φ.obj d ⟶ φ.obj e)) (S.arrows (φ.obj d) (φ.obj e)) (φ.map q)
Tactic: apply S.mul
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_3, u} C
D : Type u_1
inst_1 : Groupoid.{u_2, u_1} D
φ : Functor.{u_3, u_2, u, u_1} C D
S : Subgroupoid.{u_1, u_2} D
Sn : S.IsNormal
c : C
⊢ 𝟙 c ∈ (comap φ S).arrows c c
have rw : Membership.mem (γ := Set (φ.obj c ⟶ φ.obj c)) (S.arrows (φ.obj c) (φ.obj c)) (𝟙 (φ.obj c))
Tactic: rw [comap, mem_setOf, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_3, u} C
D : Type u_1
inst_1 : Groupoid.{u_2, u_1} D
φ : Functor.{u_3, u_2, u, u_1} C D
S : Subgroupoid.{u_1, u_2} D
Sn : S.IsNormal
c d : C
f : c ⟶ d
γ : c ⟶ c
hγ : γ ∈ (comap φ S).arrows c c
⊢ Groupoid.inv f ≫ γ ≫ f ∈ (comap φ S).arrows d d
have simp_rw : Membership.mem (γ := Set (φ.obj d ⟶ φ.obj d)) (S.arrows (φ.obj d) (φ.obj d))
  (Groupoid.inv (φ.map f) ≫ φ.map γ ≫ φ.map f)
Tactic: simp_rw [inv_eq_inv f, comap, mem_setOf, Functor.map_comp, Functor.map_inv, ← inv_eq_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} 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
S : Subgroupoid.{u, u_2} C
c d : D
f : c ⟶ d
⊢ Arrows φ hφ S c d f ↔
    ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
      f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb
have mp : Arrows φ hφ S c d f →
  ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
    f = eqToHom sorry ≫ φ.map g ≫ eqToHom hb
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} 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
S : Subgroupoid.{u, u_2} C
c d : D
f : c ⟶ d
mp :
  Arrows φ hφ S c d f →
    ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
      f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb
⊢ Arrows φ hφ S c d f ↔
    ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
      f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb
have mpr : (∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
    f = eqToHom sorry ≫ φ.map g ≫ eqToHom hb) →
  Arrows φ hφ S c d f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} 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
S : Subgroupoid.{u, u_2} C
a b : C
g : a ⟶ b
hg : g ∈ S.arrows a b
⊢ Arrows φ hφ S (φ.obj a) (φ.obj b) (eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯)
have mpr : Arrows φ hφ S (φ.obj a) (φ.obj b) (φ.map g)
Tactic: rw [← eq_conj_eqToHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : 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
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf : f ∈ S.arrows c_1 d_1
⊢ Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c_1))
    {x : φ.obj d_1 ⟶ φ.obj c_1 | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c_1) x} (Groupoid.inv (φ.map f))
have rw : Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c_1))
  {x : φ.obj d_1 ⟶ φ.obj c_1 | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c_1) x} (φ.map (Groupoid.inv f))
Tactic: rw [inv_eq_inv, ← Functor.map_inv, ← inv_eq_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : 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
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf : f ∈ S.arrows c_1 d_1
⊢ Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c_1))
    {x : φ.obj d_1 ⟶ φ.obj c_1 | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c_1) x} (φ.map (Groupoid.inv f))
have hf : Groupoid.inv f ∈ S.arrows d_1 c_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : 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
S : Subgroupoid.{u, u_2} C
e c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf : f ∈ S.arrows c_1 d_1
q : φ.obj d_1 ⟶ e
hq : Membership.mem (γ := Set (φ.obj d_1 ⟶ e)) {x : φ.obj d_1 ⟶ e | Map.Arrows φ hφ S (φ.obj d_1) e x} q
⊢ Membership.mem (γ := Set (φ.obj c_1 ⟶ e)) {x : φ.obj c_1 ⟶ e | Map.Arrows φ hφ S (φ.obj c_1) e x} (φ.map f ≫ q)
have obtain : ∀ (c₃ c₄ : C) (g : c₃ ⟶ c₄) (he : φ.obj c₃ = φ.obj d_1) {q : φ.obj d_1 ⟶ φ.obj c₄}
  (hq :
    Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c₄))
      {x : φ.obj d_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c₄) x} q)
  (hg : g ∈ S.arrows c₃ c₄) (gq : q = eqToHom sorry ≫ φ.map g ≫ eqToHom sorry),
  Membership.mem (γ := Set (φ.obj c_1 ⟶ φ.obj c₄))
    {x : φ.obj c_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj c_1) (φ.obj c₄) x} (φ.map f ≫ q)
Tactic: obtain ⟨c₃, c₄, g, he, rfl, hg, gq⟩ := (Map.arrows_iff φ hφ S q).mp hq
Cleared hypotheses: e, q, hq
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : 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
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf : f ∈ S.arrows c_1 d_1
c₃ c₄ : C
g : c₃ ⟶ c₄
he : φ.obj c₃ = φ.obj d_1
q : φ.obj d_1 ⟶ φ.obj c₄
hq :
  Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c₄))
    {x : φ.obj d_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c₄) x} q
hg : g ∈ S.arrows c₃ c₄
gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯
⊢ Membership.mem (γ := Set (φ.obj c_1 ⟶ φ.obj c₄))
    {x : φ.obj c_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj c_1) (φ.obj c₄) x} (φ.map f ≫ q)
have refl : ∀ (g : d_1 ⟶ c₄) (he : φ.obj d_1 = φ.obj d_1) (hg : g ∈ S.arrows d_1 c₄) (gq : q = eqToHom sorry ≫ φ.map g ≫ eqToHom sorry),
  Membership.mem (γ := Set (φ.obj c_1 ⟶ φ.obj c₄))
    {x : φ.obj c_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj c_1) (φ.obj c₄) x} (φ.map f ≫ q)
Tactic: cases hφ he
Cleared hypotheses: c₃, g, he, hg, gq
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : 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
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf : f ∈ S.arrows c_1 d_1
c₄ : C
q : φ.obj d_1 ⟶ φ.obj c₄
hq :
  Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c₄))
    {x : φ.obj d_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c₄) x} q
g : d_1 ⟶ c₄
he : φ.obj d_1 = φ.obj d_1
hg : g ∈ S.arrows d_1 c₄
gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯
⊢ Membership.mem (γ := Set (φ.obj c_1 ⟶ φ.obj c₄))
    {x : φ.obj c_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj c_1) (φ.obj c₄) x} (φ.map f ≫ q)
have refl : Membership.mem (γ := Set (φ.obj c_1 ⟶ φ.obj c₄)) {x : φ.obj c_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj c_1) (φ.obj c₄) x}
  (φ.map (f ≫ g))
Tactic: rw [gq, ← eq_conj_eqToHom, ← φ.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : 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
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf : f ∈ S.arrows c_1 d_1
c₄ : C
q : φ.obj d_1 ⟶ φ.obj c₄
hq :
  Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c₄))
    {x : φ.obj d_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c₄) x} q
g : d_1 ⟶ c₄
he : φ.obj d_1 = φ.obj d_1
hg : g ∈ S.arrows d_1 c₄
gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯
⊢ Membership.mem (γ := Set (φ.obj c_1 ⟶ φ.obj c₄))
    {x : φ.obj c_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj c_1) (φ.obj c₄) x} (φ.map (f ≫ g))
have refl : f ≫ g ∈ S.arrows c_1 c₄
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} 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
S : Subgroupoid.{u, u_2} C
T : Subgroupoid.{u_1, u_3} D
⊢ map φ hφ S ≤ T ↔ S ≤ comap φ T
have simp_rw : (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) ↔ ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d
Tactic: simp_rw [le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} 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
S : Subgroupoid.{u, u_2} C
T : Subgroupoid.{u_1, u_3} D
⊢ (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) ↔ ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d
have mp : (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) → ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} 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
S : Subgroupoid.{u, u_2} C
T : Subgroupoid.{u_1, u_3} D
mp : (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) → ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d
⊢ (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) ↔ ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d
have mpr : (∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d) → ∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d
Tactic: constructor
-- 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
d : D
⊢ Set.Nonempty.{u_3} (α := d ⟶ d) {x : d ⟶ d | Map.Arrows φ hφ S d d x} ↔
    ∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d
have mp : Set.Nonempty.{u_3} (α := d ⟶ d) {x : d ⟶ d | Map.Arrows φ hφ S d d x} → ∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d
Tactic: constructor
-- 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
d : D
mp :
  Set.Nonempty.{u_3} (α := d ⟶ d) {x : d ⟶ d | Map.Arrows φ hφ S d d x} →
    ∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d
⊢ Set.Nonempty.{u_3} (α := d ⟶ d) {x : d ⟶ d | Map.Arrows φ hφ S d d x} ↔
    ∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d
have mpr : (∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d) →
  Set.Nonempty.{u_3} (α := d ⟶ d) {x : d ⟶ d | Map.Arrows φ hφ S d d x}
Tactic: constructor
-- 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
d : D
f : d ⟶ d
hf : Membership.mem (γ := Set (d ⟶ d)) {x : d ⟶ d | Map.Arrows φ hφ S d d x} f
⊢ ∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d
have hf₁ : Map.Arrows φ hφ S d d f
Tactic: change Map.Arrows φ hφ S d d f at hf
Cleared hypotheses: hf
-- 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
d : D
f : d ⟶ d
hf : Map.Arrows φ hφ S d d f
⊢ ∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d
have hf₁ : ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = d) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
  f = eqToHom sorry ≫ φ.map g ≫ eqToHom hb
Tactic: rw [Map.arrows_iff] at hf
Cleared hypotheses: hf
-- 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
d : D
f : d ⟶ d
hf :
  ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = d) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
    f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb
⊢ ∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d
have mp : ∀ (c d_1 : C) (g : c ⟶ d_1) (ec : φ.obj c = d) (ed : φ.obj d_1 = d) (eg : g ∈ S.arrows c d_1),
  ∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d
Tactic: obtain ⟨c, d, g, ec, ed, eg, gS, eg⟩ := hf
Cleared hypotheses: f, hf
-- 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
⊢ (map φ hφ S).objs = φ.obj '' S.objs
have h : ∀ (x : D), x ∈ (map φ hφ S).objs ↔ x ∈ φ.obj '' S.objs
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} 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
c d : D
f : c ⟶ d
⊢ f ∈ (im φ hφ).arrows c d ↔
    ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb
have h : ∀ (x x_1 : C) (x_2 : x ⟶ x_1) (x_3 : φ.obj x = c) (x_4 : φ.obj x_1 = d),
  f = eqToHom sorry ≫ φ.map x_2 ≫ eqToHom x_4 ↔
    ∃ (_ : Membership.mem (γ := Set (x ⟶ x_1)) (arrows ⊤ x x_1) x_2), f = eqToHom sorry ≫ φ.map x_2 ≫ eqToHom x_4
Tactic: convert! Map.arrows_iff φ hφ ⊤ f
-- Lean 4 proof step from Mathlib.CategoryTheory.Groupoid.Subgroupoid (goal)
Goal:
C : Type u
inst : Groupoid.{u_2, u} 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φ = ⊤
d : D
⊢ ∃ (a : C), φ.obj a = d
have rw : Membership.mem (γ := Set D) (objs.{u_1, u_3} ⊤) d
Tactic: rw [← mem_im_objs_iff _ hφ, hφ']
-- 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
d : D
⊢ 𝟙 d ∈ (map φ hφ S).arrows d d
have obtain : ∀ (c : C), Membership.mem (γ := Set (φ.obj c ⟶ φ.obj c)) ((map φ hφ S).arrows (φ.obj c) (φ.obj c)) (𝟙 (φ.obj c))
Tactic: obtain ⟨c, rfl⟩ := obj_surjective_of_im_eq_top φ hφ hφ' d
Cleared hypotheses: d
-- 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
⊢ Map.Arrows φ hφ S (φ.obj c) (φ.obj c) (𝟙 (φ.obj c))
have rw : Map.Arrows φ hφ S (φ.obj c) (φ.obj c) (φ.map (𝟙 c))
Tactic: rw [← Functor.map_id]
-- 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
⊢ Map.Arrows φ hφ S (φ.obj c) (φ.obj c) (φ.map (𝟙 c))
have hf : 𝟙 c ∈ S.arrows c c
Tactic: constructor
-- 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
d d' : D
g : d ⟶ d'
δ : d ⟶ d
hδ : δ ∈ (map φ hφ S).arrows d d
⊢ Groupoid.inv g ≫ δ ≫ g ∈ (map φ hφ S).arrows d' d'
have hδ₁ : ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = d) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
  δ = eqToHom sorry ≫ φ.map g ≫ eqToHom hb
Tactic: rw [mem_map_iff] at hδ
Cleared hypotheses: hδ
-- 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
d d' : D
g : d ⟶ d'
δ : d ⟶ d
hδ :
  ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = d) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
    δ = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb
⊢ Groupoid.inv g ≫ δ ≫ g ∈ (map φ hφ S).arrows d' d'
have obtain : ∀ (c c' : C) (γ : c ⟶ c') (cd : φ.obj c = d) (cd' : φ.obj c' = d) (γS : γ ∈ S.arrows c c')
  (hγ : δ = eqToHom sorry ≫ φ.map γ ≫ eqToHom cd'), Groupoid.inv g ≫ δ ≫ g ∈ (map φ hφ S).arrows d' d'
Tactic: obtain ⟨c, c', γ, cd, cd', γS, hγ⟩ := hδ
Cleared hypotheses: hδ
-- 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
d d' : D
g : d ⟶ d'
δ : d ⟶ d
c c' : C
γ : c ⟶ c'
cd : φ.obj c = d
cd' : φ.obj c' = d
γS : γ ∈ S.arrows c c'
hγ : δ = eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd'
⊢ Groupoid.inv g ≫ δ ≫ g ∈ (map φ hφ S).arrows d' d'
have subst_vars : ∀ (g : φ.obj c ⟶ d') (cd' : φ.obj c' = φ.obj c),
  Groupoid.inv g ≫ (eqToHom sorry ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'
Tactic: subst_vars
Cleared hypotheses: d, g, δ, cd, cd', hγ
-- 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
d' : D
c c' : C
γ : c ⟶ c'
γS : γ ∈ S.arrows c c'
g : φ.obj c ⟶ d'
cd' : φ.obj c' = φ.obj c
⊢ Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'
have refl : ∀ (γ : c ⟶ c) (γS : γ ∈ S.arrows c c) (cd' : φ.obj c = φ.obj c),
  Groupoid.inv g ≫ (eqToHom sorry ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'
Tactic: cases hφ cd'
Cleared hypotheses: c', γ, γS, cd'
-- 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
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
⊢ d' ∈ (im φ hφ).objs
have rw : Membership.mem (γ := Set D) (objs.{u_1, u_3} ⊤) d'
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
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
⊢ Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'
have this : d' ∈ (im φ hφ).objs
Tactic: have : d' ∈ (im φ hφ).objs := by rw [hφ']; apply mem_top_objs
-- 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
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
this : d' ∈ (im φ hφ).objs
⊢ Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'
have this₁ : ∃ (c : C), φ.obj c = d'
Tactic: rw [mem_im_objs_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
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
this : ∃ (c : C), φ.obj c = d'
⊢ Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'
have refl : ∀ (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 sorry ≫ φ.map γ ≫ eqToHom cd') ≫ g)
Tactic: obtain ⟨c', rfl⟩ := this
Cleared hypotheses: d', g, this