awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) (𝟙 X - p)
⊢ p = 𝟙 X - (𝟙 X - p)
have h₁ : p = p
Tactic: rw [sub_sub_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasEqualizer (𝟙 X) p
have this : HasKernel (𝟙 X - p)
Tactic: haveI : HasKernel (𝟙 _ - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_2, u_2} D
⊢ IsIdempotentComplete.{v_2, u_2} D
have rw : ∀ (X : D) (p : X ⟶ X), p ≫ p = p → HasKernel p
Tactic: rw [isIdempotentComplete_iff_idempotents_have_kernels]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
h : ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
⊢ ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
have rcases : ∀ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y) (h₁ : i ≫ e = 𝟙 Y) (h₂ : e ≫ i = p),
  ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
Tactic: rcases h with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
have h : (i ≫ φ.hom) ≫ φ.inv ≫ e = 𝟙 Y ∧ (φ.inv ≫ e) ≫ i ≫ φ.hom = p'
Tactic: use Y, i ≫ φ.hom, φ.inv ≫ e
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p) ↔
    ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
have mp : (∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p) →
  ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
mp :
  (∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p) →
    ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
⊢ (∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p) ↔
    ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
have mpr : (∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') →
  ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') →
    ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
have mpr : p' ≫ φ.symm.hom = φ.symm.hom ≫ p
Tactic: apply split_imp_of_iso φ.symm p' p
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p
have mpr : p' ≫ φ.symm.hom = φ.symm.hom ≫ p ≫ φ.hom ≫ φ.inv
Tactic: rw [← comp_id p, ← φ.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
| p ≫ φ.hom
have a : φ.hom ≫ p'
Tactic: rw [hpp']
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p ≫ φ.hom ≫ φ.inv
have mpr : p' ≫ φ.symm.hom = φ.symm.hom ≫ (φ.hom ≫ p') ≫ φ.inv
Tactic: slice_rhs 2 3 => rw [hpp']
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_2, u_2} D
have refine : ∀ (X : D) (p : X ⟶ X), p ≫ p = p → ∃ (Y : D) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
Tactic: refine ⟨?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom ≫ φ.inv
have a : 𝟙 X'
Tactic: rw [φ.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ p ≫ φ.hom = φ.hom ≫ φ.inv ≫ p ≫ φ.hom
have slice_rhs : p ≫ φ.hom = (𝟙 X' ≫ p) ≫ φ.hom
Tactic: slice_rhs 1 2 => rw [φ.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ p ≫ φ.hom = (𝟙 X' ≫ p) ≫ φ.hom
have rw : p ≫ φ.hom = p ≫ φ.hom
Tactic: rw [id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ∃ (Y : D) (i : Y ⟶ X') (e : X' ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
have rw : ∃ (Y' : D) (i' : Y' ⟶ (ε.inverse ⋙ ε.functor).obj X') (e' : (ε.inverse ⋙ ε.functor).obj X' ⟶ Y'),
  i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
Tactic: rw [split_iff_of_iso φ p (φ.inv ≫ p ≫ φ.hom)
      (by
        slice_rhs 1 2 => rw [φ.hom_inv_id]
        rw [id_comp])]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ε.inverse.map p ≫ ε.inverse.map p = ε.inverse.map p
have rw : ε.inverse.map (p ≫ p) = ε.inverse.map p
Tactic: rw [← ε.inverse.map_comp, hp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
rw : ε.inverse.map (p ≫ p) = ε.inverse.map p
⊢ ε.inverse.map p ≫ ε.inverse.map p = ε.inverse.map p
have rw₁ : ε.inverse.map p = ε.inverse.map p
Tactic: rw [← ε.inverse.map_comp, hp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ∃ (Y' : D) (i' : Y' ⟶ (ε.inverse ⋙ ε.functor).obj X') (e' : (ε.inverse ⋙ ε.functor).obj X' ⟶ Y'),
    i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
have rcases : ∀ (Y : C) (i : Y ⟶ ε.inverse.obj X') (e : ε.inverse.obj X' ⟶ Y) (h₁ : i ≫ e = 𝟙 Y) (h₂ : e ≫ i = ε.inverse.map p),
  ∃ (Y' : D) (i' : Y' ⟶ (ε.inverse ⋙ ε.functor).obj X') (e' : (ε.inverse ⋙ ε.functor).obj X' ⟶ Y'),
    i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
Tactic: rcases IsIdempotentComplete.idempotents_split (ε.inverse.obj X') (ε.inverse.map p)
      (by rw [← ε.inverse.map_comp, hp]) with
    ⟨Y, i, e, ⟨h₁, h₂⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ∃ (Y' : D) (i' : Y' ⟶ (ε.inverse ⋙ ε.functor).obj X') (e' : (ε.inverse ⋙ ε.functor).obj X' ⟶ Y'),
    i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
have h₃ : ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y) ∧ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
Tactic: use ε.functor.obj Y, ε.functor.map i, ε.functor.map e
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y) ∧ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
have h₃ : ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
h₃ : ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y) ∧ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
have h₄ : ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)
have h₃ : ε.functor.map (i ≫ e) = 𝟙 (ε.functor.obj Y)
Tactic: rw [← ε.functor.map_comp, h₁, ε.functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
h₃ : ε.functor.map (i ≫ e) = 𝟙 (ε.functor.obj Y)
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)
have h₄ : ε.functor.map (𝟙 Y) = 𝟙 (ε.functor.obj Y)
Tactic: rw [← ε.functor.map_comp, h₁, ε.functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
h₃ : ε.functor.map (i ≫ e) = 𝟙 (ε.functor.obj Y)
h₄ : ε.functor.map (𝟙 Y) = 𝟙 (ε.functor.obj Y)
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)
have h₅ : Eq.{v_2 + 1} (α := ε.functor.obj Y ⟶ ε.functor.obj Y) (𝟙 (ε.functor.obj Y)) (𝟙 (ε.functor.obj Y))
Tactic: rw [← ε.functor.map_comp, h₁, ε.functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
have h₃ : ε.counit.app X' ≫ p ≫ ε.counitInv.app X' = φ.inv ≫ p ≫ φ.hom
Tactic: simp only [← ε.functor.map_comp, h₂, Equivalence.fun_inv_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
⊢ IsIdempotentComplete.{v_1, u_1} C ↔ IsIdempotentComplete.{v_2, u_2} D
have mp : IsIdempotentComplete.{v_1, u_1} C → IsIdempotentComplete.{v_2, u_2} D
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
mp : IsIdempotentComplete.{v_1, u_1} C → IsIdempotentComplete.{v_2, u_2} D
⊢ IsIdempotentComplete.{v_1, u_1} C ↔ IsIdempotentComplete.{v_2, u_2} D
have mpr : IsIdempotentComplete.{v_2, u_2} D → IsIdempotentComplete.{v_1, u_1} C
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
⊢ IsIdempotentComplete.{v_1, u_1} C
have refine : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
Tactic: refine ⟨?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ p.op ≫ p.op = p.op
have rw : (p ≫ p).op = p.op
Tactic: rw [← op_comp, hp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
rw : (p ≫ p).op = p.op
⊢ p.op ≫ p.op = p.op
have rw₁ : p.op = p.op
Tactic: rw [← op_comp, hp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
have rcases : ∀ (Y : Cᵒᵖ) (i : Y ⟶ op X) (e : op X ⟶ Y) (h₁ : i ≫ e = 𝟙 Y) (h₂ : e ≫ i = p.op),
  ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
Tactic: rcases IsIdempotentComplete.idempotents_split (op X) p.op (by rw [← op_comp, hp]) with
    ⟨Y, i, e, ⟨h₁, h₂⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
have h₃ : e.unop ≫ i.unop = 𝟙 (unop Y) ∧ i.unop ≫ e.unop = p
Tactic: use Y.unop, e.unop, i.unop
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 (unop Y) ∧ i.unop ≫ e.unop = p
have h₃ : e.unop ≫ i.unop = 𝟙 (unop Y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
h₃ : e.unop ≫ i.unop = 𝟙 (unop Y)
⊢ e.unop ≫ i.unop = 𝟙 (unop Y) ∧ i.unop ≫ e.unop = p
have h₄ : i.unop ≫ e.unop = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 (unop Y)
have h₃ : Eq.{v_1 + 1} (α := unop Y ⟶ unop Y) (Quiver.Hom.unop (𝟙 Y)) (𝟙 (unop Y))
Tactic: simp only [← unop_comp, h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ i.unop ≫ e.unop = p
have h₃ : p.op.unop = p
Tactic: simp only [← unop_comp, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_1, u_1} Cᵒᵖ ↔ IsIdempotentComplete.{v_1, u_1} C
have mp : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ → IsIdempotentComplete.{v_1, u_1} C
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
mp : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ → IsIdempotentComplete.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_1, u_1} Cᵒᵖ ↔ IsIdempotentComplete.{v_1, u_1} C
have mpr : IsIdempotentComplete.{v_1, u_1} C → IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
have mpr : IsIdempotentComplete.{v_1, u_1} Cᵒᵖᵒᵖ
Tactic: apply isIdempotentComplete_of_isIdempotentComplete_opposite
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Biproducts (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasFiniteBiproducts.{v, u_1} C
J : Type
inst_3 : Finite J
F : J → Karoubi.{v, u_1} C
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
      (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X))
    (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X) (biproduct.map fun (j : J) ↦ (F j).p)
      (biproduct.map fun (j : J) ↦ (F j).p))
    (biproduct.map fun (j : J) ↦ (F j).p)
have w : ∀ (j j_1 : J),
  Eq.{v + 1} (α := (F j_1).X ⟶ (F j).X)
    (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
        (biproduct.ι.{0, v, u_1} (C := C) (fun (j : J) ↦ (F j).X) j_1)
        (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
          (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X) (biproduct.map fun (j : J) ↦ (F j).p)
            (biproduct.map fun (j : J) ↦ (F j).p))
          (biproduct.π (fun (j : J) ↦ (F j).X) j)) :
      (F j_1).X ⟶ (F j).X)
    (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
        (biproduct.ι.{0, v, u_1} (C := C) (fun (j : J) ↦ (F j).X) j_1)
        (CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X) (biproduct.map fun (j : J) ↦ (F j).p)
          (biproduct.π (fun (j : J) ↦ (F j).X) j)) :
      (F j_1).X ⟶ (F j).X)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Biproducts (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasFiniteBiproducts.{v, u_1} C
n : ℕ
F : Fin n → Karoubi.{v, u_1} C
⊢ HasBiproduct F
have apply : Eq.{v + 1} (α := Bicone.pt (Biproducts.bicone F) ⟶ Bicone.pt (Biproducts.bicone F))
  (∑ j : Fin n, Bicone.π (Biproducts.bicone F) j ≫ Bicone.ι (Biproducts.bicone F) j)
  (𝟙 (Bicone.pt (Biproducts.bicone F)))
Tactic: apply hasBiproduct_of_total (Biproducts.bicone F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Biproducts (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p =
    𝟙 (P ⊞ P.complement)
have h₀ : CategoryStruct.comp (Y := P ⊞ P.complement) biprod.inl
    (biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p) =
  biprod.inl ≫ 𝟙 (P ⊞ P.complement)
Tactic: apply biprod.hom_ext'
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Biproducts (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
h₀ :
  CategoryStruct.comp (Y := P ⊞ P.complement) biprod.inl
      (biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p) =
    biprod.inl ≫ 𝟙 (P ⊞ P.complement)
⊢ biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p =
    𝟙 (P ⊞ P.complement)
have h₁ : CategoryStruct.comp (Y := P ⊞ P.complement) biprod.inr
    (biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p) =
  biprod.inr ≫ 𝟙 (P ⊞ P.complement)
Tactic: apply biprod.hom_ext'
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Biproducts (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ CategoryStruct.comp (Y := P ⊞ P.complement) biprod.inl
      (biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p) =
    biprod.inl ≫ 𝟙 (P ⊞ P.complement)
have h₀ : Eq (α := P ⟶ P ⊞ P.complement) ((P.decompId_i ≫ P.complement.decompId_p) ≫ biprod.inr) 0
Tactic: rw [biprod.inl_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc,
        add_eq_left, ← assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Biproducts (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ Eq (α := P ⟶ P ⊞ P.complement) ((P.decompId_i ≫ P.complement.decompId_p) ≫ biprod.inr) 0
have h₀ : P.decompId_i ≫ P.complement.decompId_p = 0
Tactic: refine (?_ =≫ _).trans zero_comp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Biproducts (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ P.decompId_i ≫ P.complement.decompId_p = 0
have h₀ : (P.decompId_i ≫ P.complement.decompId_p).f = Hom.f 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Biproducts (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ CategoryStruct.comp (Y := P ⊞ P.complement) biprod.inr
      (biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p) =
    biprod.inr ≫ 𝟙 (P ⊞ P.complement)
have h₁ : Eq (α := P.complement ⟶ P ⊞ P.complement) ((P.complement.decompId_i ≫ P.decompId_p) ≫ biprod.inl) 0
Tactic: rw [biprod.inr_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc,
        add_eq_right, ← assoc]