awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
X Y_1 : GradedObject J C
e : X ≅ Y_1
F : C ⥤ Functor.{v_2, v_3, u_2, u_3} D E
j : J
Y : D
⊢ (F.map (e.inv j)).app Y ≫ (F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
have rw : (F.map (e.inv j) ≫ F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
Tactic: rw [← NatTrans.comp_app, ← F.map_comp, inv_hom_id_eval,
    Functor.map_id, NatTrans.id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
X Y_1 : GradedObject J C
e : X ≅ Y_1
F : C ⥤ Functor.{v_2, v_3, u_2, u_3} D E
j : J
Y : D
rw : (F.map (e.inv j) ≫ F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
⊢ (F.map (e.inv j)).app Y ≫ (F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
have rw₁ : (F.map (e.inv j ≫ e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
Tactic: rw [← NatTrans.comp_app, ← F.map_comp, inv_hom_id_eval,
    Functor.map_id, NatTrans.id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
X Y_1 : GradedObject J C
e : X ≅ Y_1
F : C ⥤ Functor.{v_2, v_3, u_2, u_3} D E
j : J
Y : D
rw : (F.map (e.inv j) ≫ F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
rw₁ : (F.map (e.inv j ≫ e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
⊢ (F.map (e.inv j)).app Y ≫ (F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
have rw₂ : (F.map (𝟙 (Y_1 j))).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
Tactic: rw [← NatTrans.comp_app, ← F.map_comp, inv_hom_id_eval,
    Functor.map_id, NatTrans.id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
X Y_1 : GradedObject J C
e : X ≅ Y_1
F : C ⥤ Functor.{v_2, v_3, u_2, u_3} D E
j : J
Y : D
rw : (F.map (e.inv j) ≫ F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
rw₁ : (F.map (e.inv j ≫ e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
rw₂ : (F.map (𝟙 (Y_1 j))).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
⊢ (F.map (e.inv j)).app Y ≫ (F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
have rw₃ : NatTrans.app (𝟙 (F.obj (Y_1 j))) Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
Tactic: rw [← NatTrans.comp_app, ← F.map_comp, inv_hom_id_eval,
    Functor.map_id, NatTrans.id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
X Y_1 : GradedObject J C
e : X ≅ Y_1
F : C ⥤ Functor.{v_2, v_3, u_2, u_3} D E
j : J
Y : D
rw : (F.map (e.inv j) ≫ F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
rw₁ : (F.map (e.inv j ≫ e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
rw₂ : (F.map (𝟙 (Y_1 j))).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
rw₃ : NatTrans.app (𝟙 (F.obj (Y_1 j))) Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
⊢ (F.map (e.inv j)).app Y ≫ (F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
have rw₄ : Eq.{v_3 + 1} (α := (F.obj (Y_1 j)).obj Y ⟶ (F.obj (Y_1 j)).obj Y) (𝟙 ((F.obj (Y_1 j)).obj Y))
  (𝟙 ((F.obj (Y_1 j)).obj Y))
Tactic: rw [← NatTrans.comp_app, ← F.map_comp, inv_hom_id_eval,
    Functor.map_id, NatTrans.id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : Type u_1
x x' : GradedObject I C
h : x = x'
i : I
⊢ Eq.{v + 1} (α := x i ⟶ x' i) (eqToHom h i : x i ⟶ x' i) (eqToHom ⋯ : x i ⟶ x' i)
have subst : Eq.{v + 1} (α := x i ⟶ x i) (eqToHom sorry i : x i ⟶ x i) (eqToHom sorry : x i ⟶ x i)
Tactic: subst h
Cleared hypotheses: x', h
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ Functor.obj (comap C f) X b = Functor.obj (comap C g) X b
have dsimp : X (f b) = X (g b)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ Functor.obj (comap C g) X b = Functor.obj (comap C f) X b
have dsimp : X (g b) = X (f b)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
β : Type w
X Y : β → C
h : X = Y
b : β
⊢ X b = Y b
have rw : Y b = Y b
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
β : Type w
X Y : β → C
h : X = Y
b : β
⊢ Eq.{v + 1} (α := X b ⟶ Y b) (eqToHom h b : X b ⟶ Y b) (eqToHom ⋯ : X b ⟶ Y b)
have subst : Eq.{v + 1} (α := X b ⟶ X b) (eqToHom sorry b : X b ⟶ X b) (eqToHom sorry : X b ⟶ X b)
Tactic: subst h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
β γ : Type w
e : β ≃ γ
⊢ Eq (α := β → β) (fun (i : β) ↦ i) (Function.comp (β := γ) (⇑e.symm : (a : γ) → β) (⇑e : (a : β) → γ))
have h : ∀ (x : β), x = Function.comp (β := γ) (⇑e.symm : (a : γ) → β) (⇑e : (a : β) → γ) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
β γ : Type w
e : β ≃ γ
⊢ Eq (α := γ → γ) (Function.comp (β := β) (⇑e : (a : β) → γ) (⇑e.symm : (a : γ) → β)) fun (i : γ) ↦ i
have h : ∀ (x : γ), Function.comp (β := β) (⇑e : (a : β) → γ) (⇑e.symm : (a : γ) → β) x = x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
inst_1 : AddCommGroup β
s : β
m n : ℤ
⊢ Eq.{u_1 + 1} (α := β → β) (fun (b : β) ↦ b + (m + n) • s) ((fun (b : β) ↦ b + m • s) ∘ fun (b : β) ↦ b + n • s)
have h : ∀ (x : β), x + (m + n) • s = ((fun (b : β) ↦ b + m • s) ∘ fun (b : β) ↦ b + n • s) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
inst_1 : AddCommGroup β
s : β
m n : ℤ
x : β
⊢ x + (m + n) • s = ((fun (b : β) ↦ b + m • s) ∘ fun (b : β) ↦ b + n • s) x
have h : x + (m + n) • s = x + n • s + m • s
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
inst_1 : AddCommGroup β
s : β
m n : ℤ
x : β
⊢ x + (m + n) • s = x + n • s + m • s
have h : x + (n + m) • s = x + n • s + m • s
Tactic: rw [add_comm m n, add_zsmul, add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
inst_1 : AddCommGroup β
s : β
m n : ℤ
x : β
h : x + (n + m) • s = x + n • s + m • s
⊢ x + (m + n) • s = x + n • s + m • s
have h₁ : x + (n • s + m • s) = x + n • s + m • s
Tactic: rw [add_comm m n, add_zsmul, add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
inst_1 : AddCommGroup β
s : β
m n : ℤ
x : β
h : x + (n + m) • s = x + n • s + m • s
h₁ : x + (n • s + m • s) = x + n • s + m • s
⊢ x + (m + n) • s = x + n • s + m • s
have h₂ : x + (n • s + m • s) = x + (n • s + m • s)
Tactic: rw [add_comm m n, add_zsmul, add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
β : Type w
⊢ HasZeroObject (GradedObject β C)
have refine_1 : ∀ (X : GradedObject β C) (f : (fun (x : β) ↦ 0) ⟶ X), f = default
Tactic: refine ⟨⟨fun _ => 0, fun X => ⟨⟨⟨fun b => 0⟩, fun f => ?_⟩⟩, fun X =>
    ⟨⟨⟨fun b => 0⟩, fun f => ?_⟩⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
β : Type w
refine_1 : ∀ (X : GradedObject β C) (f : (fun (x : β) ↦ 0) ⟶ X), f = default
⊢ HasZeroObject (GradedObject β C)
have refine_2 : ∀ (X : GradedObject β C) (f : X ⟶ fun (x : β) ↦ 0), f = default
Tactic: refine ⟨⟨fun _ => 0, fun X => ⟨⟨⟨fun b => 0⟩, fun f => ?_⟩⟩, fun X =>
    ⟨⟨⟨fun b => 0⟩, fun f => ?_⟩⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
β : Type
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{0, v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : GradedObject β C
f g : X ⟶ Y
w :
  Eq (α := Functor.obj.{v, v, u, u} (total β C) X ⟶ Functor.obj.{v, v, u, u} (total β C) Y) (Functor.map (total β C) f)
    (Functor.map (total β C) g)
⊢ f = g
have h : ∀ (i : β), f i = g i
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (hypothesis)
Goal:
β : Type
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{0, v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : GradedObject β C
f g : X ⟶ Y
w :
  Eq (α := Functor.obj.{v, v, u, u} (total β C) X ⟶ Functor.obj.{v, v, u, u} (total β C) Y) (Functor.map (total β C) f)
    (Functor.map (total β C) g)
i : β
⊢ f i = g i
have w₁ : Eq.{v + 1} (α := X i ⟶ Functor.obj.{v, v, u, u} (total β C) Y)
  (CategoryStruct.comp (Y := sigmaObj.{0, v, u} fun (i : β) ↦ X i) (Sigma.ι (fun (i : β) ↦ X i) i)
    (Functor.map (total β C) f))
  (CategoryStruct.comp (Y := sigmaObj.{0, v, u} fun (i : β) ↦ X i) (Sigma.ι (fun (i : β) ↦ X i) i)
    (Functor.map (total β C) g))
Tactic: replace w := Sigma.ι (fun i : β => X i) i ≫= w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (hypothesis)
Goal:
β : Type
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{0, v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w :
  Eq.{v + 1} (α := X i ⟶ Functor.obj.{v, v, u, u} (total β C) Y)
    (CategoryStruct.comp (Y := sigmaObj.{0, v, u} fun (i : β) ↦ X i) (Sigma.ι (fun (i : β) ↦ X i) i)
      (Functor.map (total β C) f))
    (CategoryStruct.comp (Y := sigmaObj.{0, v, u} fun (i : β) ↦ X i) (Sigma.ι (fun (i : β) ↦ X i) i)
      (Functor.map (total β C) g))
⊢ f i = g i
have w₁ : Eq.{v + 1} (α := X i ⟶ Functor.obj.{v, v, u, u} (total β C) Y)
  (NatTrans.app (Discrete.natTrans fun (X : Discrete β) ↦ (fun (i : β) ↦ f i) X.as) { as := i } ≫
      colimit.ι (Discrete.functor fun (i : β) ↦ Y i) { as := i : Discrete β } :
    Quiver.Hom.{v, u} (V := C) (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : β) ↦ X i) { as := i : Discrete β })
      (colimit.{0, 0, v, u} (J := Discrete β) (Discrete.functor fun (i : β) ↦ Y i)))
  (NatTrans.app (Discrete.natTrans fun (X : Discrete β) ↦ (fun (i : β) ↦ g i) X.as) { as := i } ≫
    colimit.ι (Discrete.functor fun (i : β) ↦ Y i) { as := i : Discrete β })
Tactic: erw [colimit.ι_map, colimit.ι_map] at w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (hypothesis)
Goal:
β : Type
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{0, v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w :
  Eq.{v + 1} (α := X i ⟶ Functor.obj.{v, v, u, u} (total β C) Y)
    (NatTrans.app (Discrete.natTrans fun (X : Discrete β) ↦ (fun (i : β) ↦ f i) X.as) { as := i } ≫
        colimit.ι (Discrete.functor fun (i : β) ↦ Y i) { as := i : Discrete β } :
      Quiver.Hom.{v, u} (V := C)
        (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : β) ↦ X i) { as := i : Discrete β })
        (colimit.{0, 0, v, u} (J := Discrete β) (Discrete.functor fun (i : β) ↦ Y i)))
    (NatTrans.app (Discrete.natTrans fun (X : Discrete β) ↦ (fun (i : β) ↦ g i) X.as) { as := i } ≫
      colimit.ι (Discrete.functor fun (i : β) ↦ Y i) { as := i : Discrete β })
⊢ f i = g i
have w₁ : Eq.{v + 1} (α := X i ⟶ colimit.{0, 0, v, u} (Discrete.functor Y)) (f i ≫ colimit.ι (Discrete.functor Y) { as := i })
  (g i ≫ colimit.ι (Discrete.functor Y) { as := i })
Tactic: replace w : f i ≫ colimit.ι (Discrete.functor Y) ⟨i⟩ =
      g i ≫ colimit.ι (Discrete.functor Y) ⟨i⟩ := by simpa
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X Y : GradedObject I C
e : X ≅ Y
p : I → J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
j : J
⊢ HasCoproduct.{u_1, v_1, u_4} (Y.mapObjFun p j)
have have : ∀
  (α :
    Iso (C := Functor.{u_1, v_1, u_1, u_4} (Discrete (↑(p ⁻¹' {j}) : Type u_1)) C) (Discrete.functor (X.mapObjFun p j))
      (Discrete.functor (Y.mapObjFun p j))),
  HasCoproduct.{u_1, v_1, u_4} (Y.mapObjFun p j)
Tactic: have α : Discrete.functor (X.mapObjFun p j) ≅ Discrete.functor (Y.mapObjFun p j) :=
    Discrete.natIso (fun ⟨i, _⟩ => (GradedObject.eval i).mapIso e)
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X Y : GradedObject I C
p : I → J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
φ₁ φ₂ : X ⟶ Y
h : φ₁ = φ₂
⊢ Eq (α := mapObj.{u_1, u_2, v_1, u_4} X p ⟶ mapObj.{u_1, u_2, v_1, u_4} Y p) (mapMap φ₁ p) (mapMap φ₂ p)
have subst : Eq (α := mapObj.{u_1, u_2, v_1, u_4} X p ⟶ mapObj.{u_1, u_2, v_1, u_4} Y p) (mapMap φ₁ p) (mapMap φ₁ p)
Tactic: subst h
Cleared hypotheses: φ₂, h
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
k : K
c : (j : J) → q j = k → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = k) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {k}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
i : I
hi rw : r i = k
⊢ q (p i) = k
have rw₁ : k = k
Tactic: rw [hpqr, hi]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
k : K
c : (j : J) → q j = k → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = k) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {k}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
i : I
hi : r i = k
⊢ p i ∈ q ⁻¹' {k}
have rw : Membership.mem (γ := Set K) {k} (q (p i))
Tactic: rw [Set.mem_preimage, Set.mem_singleton_iff, hpqr, hi]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
k : K
c : (j : J) → q j = k → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = k) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {k}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
i : I
hi : r i = k
rw : Membership.mem (γ := Set K) {k} (q (p i))
⊢ p i ∈ q ⁻¹' {k}
have rw₁ : q (p i) = k
Tactic: rw [Set.mem_preimage, Set.mem_singleton_iff, hpqr, hi]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
k : K
c : (j : J) → q j = k → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = k) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {k}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
i : I
hi : r i = k
rw : Membership.mem (γ := Set K) {k} (q (p i))
rw₁ : q (p i) = k
rw₂ : r i = k
⊢ p i ∈ q ⁻¹' {k}
have rw₃ : k = k
Tactic: rw [Set.mem_preimage, Set.mem_singleton_iff, hpqr, hi]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
k : K
c : (j : J) → q j = k → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = k) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {k}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
s : Cofan.{u_1, v_1, u_4} (X.mapObjFun r k)
m : (X.cofanMapObjComp p q r hpqr k c c').pt ⟶ s.pt
hm : ∀ (j : (↑(r ⁻¹' {k}) : Type u_1)), Cofan.inj (X.cofanMapObjComp p q r hpqr k c c') j ≫ m = s.inj j
⊢ m =
    (fun (s : Cofan.{u_1, v_1, u_4} (X.mapObjFun r k)) ↦
        (Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {k}) : Type u_2)) ↦
            match (motive := (x : (↑(q ⁻¹' {k}) : Type u_2)) → (c (↑x : J) ⋯).pt ⟶ s.pt) x with
            | ⟨j, hj⟩ =>
              Cofan.IsColimit.desc (hc j hj) fun (x : (↑(p ⁻¹' {j}) : Type u_1)) ↦
                match (motive := (x : (↑(p ⁻¹' {j}) : Type u_1)) → X.mapObjFun p j x ⟶ s.pt) x with
                | ⟨i, hi⟩ => s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {k}) i ⋯) :
          c'.pt ⟶ s.pt))
      s
have h : ∀ (i : (↑(q ⁻¹' {k}) : Type u_2)),
  c'.inj i ≫ m =
    c'.inj i ≫
      (fun (s : Cofan.{u_1, v_1, u_4} (X.mapObjFun r k)) ↦
          (Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {k}) : Type u_2)) ↦
              match (motive := (x : (↑(q ⁻¹' {k}) : Type u_2)) → (c (↑x : J) sorry).pt ⟶ s.pt) x with
              | ⟨j, hj⟩ =>
                Cofan.IsColimit.desc (hc j hj) fun (x : (↑(p ⁻¹' {j}) : Type u_1)) ↦
                  match (motive := (x : (↑(p ⁻¹' {j}) : Type u_1)) → X.mapObjFun p j x ⟶ s.pt) x with
                  | ⟨i, hi⟩ => s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {k}) i sorry) :
            c'.pt ⟶ s.pt))
        s
Tactic: apply Cofan.IsColimit.hom_ext hc'
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j_1 : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
j : J
c : (j_2 : J) → q j_2 = q j → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j_2
hc : (j_2 : J) → (hj : q j_2 = q j) → IsColimit (c j_2 hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j_2 : (↑(q ⁻¹' {q j}) : Type u_2)) ↦ (c (↑j_2 : J) ⋯).pt
hc' : IsColimit c'
s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q j}) : Type u_1)) (X.mapObjFun r (q j))
m : (X.cofanMapObjComp p q r hpqr (q j) c c').pt ⟶ s.pt
hm : ∀ (j_2 : (↑(r ⁻¹' {q j}) : Type u_1)), Cofan.inj (X.cofanMapObjComp p q r hpqr (q j) c c') j_2 ≫ m = s.inj j_2
⊢ Eq (α :=
    Cocone.pt.{u_1, v_1, u_1, u_4} (J :=
        Discrete (↑(p ⁻¹' {(↑(Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q j}) j ⋯) : J)}) : Type u_1))
        (c (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q j}) j ⋯) : J) ⋯) ⟶
      s.pt)
    (c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q j}) j ⋯) ≫ m)
    (c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q j}) j ⋯) ≫
      (fun (s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q j}) : Type u_1)) (X.mapObjFun r (q j))) ↦
          (Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {q j}) : Type u_2)) ↦
              match (motive := (x : (↑(q ⁻¹' {q j}) : Type u_2)) → (c (↑x : J) ⋯).pt ⟶ s.pt) x with
              | ⟨j_2, hj⟩ =>
                Cofan.IsColimit.desc (hc j_2 hj) fun (x : (↑(p ⁻¹' {j_2}) : Type u_1)) ↦
                  match (motive := (x : (↑(p ⁻¹' {j_2}) : Type u_1)) → X.mapObjFun p j_2 x ⟶ s.pt) x with
                  | ⟨i, hi⟩ => s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {q j}) i ⋯) :
            c'.pt ⟶ s.pt))
        s)
have h : ∀ (i : (↑(p ⁻¹' {j}) : Type u_1)),
  Eq (α := X.mapObjFun p j i ⟶ s.pt)
    (Cofan.inj (c j sorry) i ≫ c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q j}) j sorry) ≫ m)
    (Cofan.inj (c j sorry) i ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q j}) j sorry) ≫
        (fun (s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q j}) : Type u_1)) (X.mapObjFun r (q j))) ↦
            (Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {q j}) : Type u_2)) ↦
                match (motive := (x : (↑(q ⁻¹' {q j}) : Type u_2)) → (c (↑x : J) sorry).pt ⟶ s.pt) x with
                | ⟨j_2, hj⟩ =>
                  Cofan.IsColimit.desc (hc j_2 hj) fun (x : (↑(p ⁻¹' {j_2}) : Type u_1)) ↦
                    match (motive := (x : (↑(p ⁻¹' {j_2}) : Type u_1)) → X.mapObjFun p j_2 x ⟶ s.pt) x with
                    | ⟨i, hi⟩ => s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {q j}) i sorry) :
              c'.pt ⟶ s.pt))
          s)
Tactic: apply Cofan.IsColimit.hom_ext (hc j rfl)
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
i : I
c : (j : J) → q j = q (p i) → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {q (p i)}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q (p i)}) : Type u_1)) (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : (↑(r ⁻¹' {q (p i)}) : Type u_1)), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
⊢ Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶ s.pt)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫ m)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫
        (fun (s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q (p i)}) : Type u_1)) (X.mapObjFun r (q (p i)))) ↦
            (Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {q (p i)}) : Type u_2)) ↦
                match (motive := (x : (↑(q ⁻¹' {q (p i)}) : Type u_2)) → (c (↑x : J) ⋯).pt ⟶ s.pt) x with
                | ⟨j, hj⟩ =>
                  Cofan.IsColimit.desc (hc j hj) fun (x : (↑(p ⁻¹' {j}) : Type u_1)) ↦
                    match (motive := (x : (↑(p ⁻¹' {j}) : Type u_1)) → X.mapObjFun p j x ⟶ s.pt) x with
                    | ⟨i_1, hi⟩ => s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {q (p i)}) i_1 ⋯) :
              c'.pt ⟶ s.pt))
          s)
have h : Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i sorry) ⟶ s.pt)
  (Cofan.inj (c (p i) sorry) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i sorry) ≫
    c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) sorry) ≫ m)
  (Cofan.inj (c (p i) sorry) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i sorry) ≫
    c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) sorry) ≫
      Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {q (p i)}) : Type u_2)) ↦
        Cofan.IsColimit.desc (hc (↑x : J) sorry) fun (x_1 : (↑(p ⁻¹' {(↑x : J)}) : Type u_1)) ↦
          s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {q (p i)}) (↑x_1 : I) sorry))
Tactic: dsimp