awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P.Hom Q
rw : P.p ≫ P.p ≫ f.f ≫ Q.p = P.p ≫ f.f ≫ Q.p
rw₁ : (P.p ≫ P.p) ≫ f.f ≫ Q.p = P.p ≫ f.f ≫ Q.p
⊢ P.p ≫ f.f = f.f
have rw₂ : P.p ≫ f.f ≫ Q.p = P.p ≫ f.f ≫ Q.p
Tactic: rw [← f.comm, ← assoc, P.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P.Hom Q
⊢ f.f ≫ Q.p = f.f
have rw : (P.p ≫ f.f ≫ Q.p) ≫ Q.p = P.p ≫ f.f ≫ Q.p
Tactic: rw [← f.comm, assoc, assoc, Q.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P.Hom Q
rw : (P.p ≫ f.f ≫ Q.p) ≫ Q.p = P.p ≫ f.f ≫ Q.p
⊢ f.f ≫ Q.p = f.f
have rw₁ : P.p ≫ (f.f ≫ Q.p) ≫ Q.p = P.p ≫ f.f ≫ Q.p
Tactic: rw [← f.comm, assoc, assoc, Q.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P.Hom Q
rw : (P.p ≫ f.f ≫ Q.p) ≫ Q.p = P.p ≫ f.f ≫ Q.p
rw₁ : P.p ≫ (f.f ≫ Q.p) ≫ Q.p = P.p ≫ f.f ≫ Q.p
⊢ f.f ≫ Q.p = f.f
have rw₂ : P.p ≫ f.f ≫ Q.p ≫ Q.p = P.p ≫ f.f ≫ Q.p
Tactic: rw [← f.comm, assoc, assoc, Q.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P.Hom Q
rw : (P.p ≫ f.f ≫ Q.p) ≫ Q.p = P.p ≫ f.f ≫ Q.p
rw₁ : P.p ≫ (f.f ≫ Q.p) ≫ Q.p = P.p ≫ f.f ≫ Q.p
rw₂ : P.p ≫ f.f ≫ Q.p ≫ Q.p = P.p ≫ f.f ≫ Q.p
⊢ f.f ≫ Q.p = f.f
have rw₃ : P.p ≫ f.f ≫ Q.p = P.p ≫ f.f ≫ Q.p
Tactic: rw [← f.comm, assoc, assoc, Q.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P.Hom Q
⊢ P.p ≫ f.f = f.f ≫ Q.p
have rw : f.f = f.f ≫ Q.p
Tactic: rw [p_comp, comp_p]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P.Hom Q
rw : f.f = f.f ≫ Q.p
⊢ P.p ≫ f.f = f.f ≫ Q.p
have rw₁ : f.f = f.f
Tactic: rw [p_comp, comp_p]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
⊢ P.p ≫ P.p ≫ P.p = P.p
have rw : P.p ≫ P.p = P.p
Tactic: rw [P.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
⊢ P.p ≫ P.p = P.p
have rw : P.p = P.p
Tactic: rw [P.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
⊢ P.p ≫ P.p ≫ P.p = P.p
have repeat' : P.p ≫ P.p = P.p
Tactic: repeat' rw [P.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
⊢ f = g ↔ f.f = g.f
have mp : f = g → f.f = g.f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
mp : f = g → f.f = g.f
⊢ f = g ↔ f.f = g.f
have mpr : f.f = g.f → f = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
h : f = g
⊢ f.f = g.f
have mp : g.f = g.f
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := X ⟶ X) (𝟙 X ≫ 𝟙 X) (𝟙 X)
have rw : Eq.{v_1 + 1} (α := X ⟶ X) (𝟙 X) (𝟙 X)
Tactic: rw [comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
h : P = Q
⊢ Hom.f (eqToHom h) = P.p ≫ eqToHom ⋯
have subst : Hom.f (eqToHom sorry) = P.p ≫ eqToHom sorry
Tactic: subst h
Cleared hypotheses: Q, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
⊢ P.p ≫ (f.f + g.f) ≫ Q.p = f.f + g.f
have rw : P.p ≫ (f.f ≫ Q.p + g.f ≫ Q.p) = f.f + g.f
Tactic: rw [add_comp, comp_add, f.comm, g.comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
rw : P.p ≫ (f.f ≫ Q.p + g.f ≫ Q.p) = f.f + g.f
⊢ P.p ≫ (f.f + g.f) ≫ Q.p = f.f + g.f
have rw₁ : P.p ≫ f.f ≫ Q.p + P.p ≫ g.f ≫ Q.p = f.f + g.f
Tactic: rw [add_comp, comp_add, f.comm, g.comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
rw : P.p ≫ (f.f ≫ Q.p + g.f ≫ Q.p) = f.f + g.f
rw₁ : P.p ≫ f.f ≫ Q.p + P.p ≫ g.f ≫ Q.p = f.f + g.f
⊢ P.p ≫ (f.f + g.f) ≫ Q.p = f.f + g.f
have rw₂ : f.f + P.p ≫ g.f ≫ Q.p = f.f + g.f
Tactic: rw [add_comp, comp_add, f.comm, g.comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
rw : P.p ≫ (f.f ≫ Q.p + g.f ≫ Q.p) = f.f + g.f
rw₁ : P.p ≫ f.f ≫ Q.p + P.p ≫ g.f ≫ Q.p = f.f + g.f
rw₂ : f.f + P.p ≫ g.f ≫ Q.p = f.f + g.f
⊢ P.p ≫ (f.f + g.f) ≫ Q.p = f.f + g.f
have rw₃ : f.f + g.f = f.f + g.f
Tactic: rw [add_comp, comp_add, f.comm, g.comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g h' : P ⟶ Q
⊢ f + g + h' = f + (g + h')
have h : (f + g + h').f = (f + (g + h')).f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
⊢ 0 + f = f
have h : (0 + f).f = f.f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
⊢ f + 0 = f
have h : (f + 0).f = f.f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
⊢ -f + f = 0
have h : (-f + f).f = Karoubi.Hom.f 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
⊢ f + g = g + f
have h : (f + g).f = (g + f).f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ IsIdempotentComplete (Karoubi.{v_1, u_1} C)
have refine : ∀ (X : Karoubi.{v_1, u_1} C) (p : X ⟶ X),
  p ≫ p = p → ∃ (Y : Karoubi.{v_1, u_1} C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
Tactic: refine ⟨?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p ≫ p = p
⊢ ∃ (Y : Karoubi.{v_1, u_1} C) (i : Y ⟶ P) (e : P ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
have hp₁ : p.f ≫ p.f = p.f
Tactic: simp only [hom_ext_iff, comp_f] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ ∃ (Y : Karoubi.{v_1, u_1} C) (i : Y ⟶ P) (e : P ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
have h : ∃ (i : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C } ⟶ P) (e : P ⟶ { X := P.X, p := p.f, idem := hp }),
  i ≫ e = 𝟙 { X := P.X, p := p.f, idem := hp } ∧ e ≫ i = p
Tactic: use ⟨P.X, p.f, hp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.p ≫ p.f ≫ P.p = p.f
have rw : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.p ≫ p.f = p.f
Tactic: rw [comp_p p, hp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
rw : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.p ≫ p.f = p.f
⊢ { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.p ≫ p.f ≫ P.p = p.f
have rw₁ : p.f = p.f
Tactic: rw [comp_p p, hp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ ∃ (i : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C } ⟶ P) (e : P ⟶ { X := P.X, p := p.f, idem := hp }),
    i ≫ e = 𝟙 { X := P.X, p := p.f, idem := hp } ∧ e ≫ i = p
have h : ∃ (e : P ⟶ { X := P.X, p := p.f, idem := hp }),
  { f := p.f, comm := sorry : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.Hom P } ≫ e =
      𝟙 { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C } ∧
    e ≫ { f := p.f, comm := sorry : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.Hom P } = p
Tactic: use ⟨p.f, by rw [comp_p p, hp]⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ P.p ≫ p.f ≫ { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.p = p.f
have rw : P.p ≫ p.f = p.f
Tactic: rw [hp, p_comp p]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
rw : P.p ≫ p.f = p.f
⊢ P.p ≫ p.f ≫ { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.p = p.f
have rw₁ : p.f = p.f
Tactic: rw [hp, p_comp p]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ ∃ (e : P ⟶ { X := P.X, p := p.f, idem := hp }),
    { f := p.f, comm := ⋯ : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.Hom P } ≫ e =
        𝟙 { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C } ∧
      e ≫ { f := p.f, comm := ⋯ : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.Hom P } = p
have h : { f := p.f, comm := sorry : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.Hom P } ≫ { f := p.f, comm := sorry } =
    𝟙 { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C } ∧
  { f := p.f, comm := sorry : P.Hom { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C } } ≫ { f := p.f, comm := sorry } =
    p
Tactic: use ⟨p.f, by rw [hp, p_comp p]⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : IsIdempotentComplete.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
⊢ Functor.essImage (toKaroubi C) P
have rcases : ∀ (Y : C) (i : Y ⟶ P.X) (e : P.X ⟶ Y) (h₁ : i ≫ e = 𝟙 Y) (h₂ : e ≫ i = P.p), Functor.essImage (toKaroubi C) P
Tactic: rcases IsIdempotentComplete.idempotents_split P.X P.p P.idem with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : IsIdempotentComplete.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ Functor.essImage (toKaroubi C) P
have h : Nonempty.{v_1 + 1} (Functor.obj (toKaroubi C) Y ≅ P)
Tactic: use Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
⊢ P.p ≫ P.p ≫ p { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } = P.p
have rw : P.p ≫ P.p ≫ 𝟙 P.X = P.p
Tactic: rw [coe_p, comp_id, P.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
rw : P.p ≫ P.p ≫ 𝟙 P.X = P.p
⊢ P.p ≫ P.p ≫ p { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } = P.p
have rw₁ : P.p ≫ P.p = P.p
Tactic: rw [coe_p, comp_id, P.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
rw : P.p ≫ P.p ≫ 𝟙 P.X = P.p
rw₁ : P.p ≫ P.p = P.p
⊢ P.p ≫ P.p ≫ p { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } = P.p
have rw₂ : P.p = P.p
Tactic: rw [coe_p, comp_id, P.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
⊢ p { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } ≫ P.p ≫ P.p = P.p
have rw : 𝟙 P.X ≫ P.p ≫ P.p = P.p
Tactic: rw [coe_p, id_comp, P.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
rw : 𝟙 P.X ≫ P.p ≫ P.p = P.p
⊢ p { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } ≫ P.p ≫ P.p = P.p
have rw₁ : P.p ≫ P.p = P.p
Tactic: rw [coe_p, id_comp, P.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
rw : 𝟙 P.X ≫ P.p ≫ P.p = P.p
rw₁ : P.p ≫ P.p = P.p
⊢ p { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } ≫ P.p ≫ P.p = P.p
have rw₂ : P.p = P.p
Tactic: rw [coe_p, id_comp, P.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
⊢ 𝟙 P = P.decompId_i ≫ P.decompId_p
have h : Hom.f (𝟙 P) = (P.decompId_i ≫ P.decompId_p).f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
⊢ Functor.map (toKaroubi C) P.p = P.decompId_p ≫ P.decompId_i
have h : Hom.f (Functor.map (toKaroubi C) P.p) = (P.decompId_p ≫ P.decompId_i).f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : Epi f
Z : Karoubi.{v_1, u_1} C
g h : Functor.obj (toKaroubi C) Y ⟶ Z
eq : Functor.map (toKaroubi C) f ≫ g = Functor.map (toKaroubi C) f ≫ h
⊢ g = h
have h₁ : g.f = h.f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : Epi f
Z : Karoubi.{v_1, u_1} C
g h : Functor.obj (toKaroubi C) Y ⟶ Z
eq : Functor.map (toKaroubi C) f ≫ g = Functor.map (toKaroubi C) f ≫ h
⊢ g.f = h.f
have h₁ : f ≫ g.f = f ≫ h.f
Tactic: rw [← cancel_epi f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : Mono f
Z : Karoubi.{v_1, u_1} C
g h : Z ⟶ Functor.obj (toKaroubi C) X
eq : g ≫ Functor.map (toKaroubi C) f = h ≫ Functor.map (toKaroubi C) f
⊢ g = h
have h₁ : g.f = h.f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h_1 : Mono f
Z : Karoubi.{v_1, u_1} C
g h : Z ⟶ Functor.obj (toKaroubi C) X
eq : g ≫ Functor.map (toKaroubi C) f = h ≫ Functor.map (toKaroubi C) f
⊢ g.f = h.f
have h₁ : g.f ≫ f = h.f ≫ f
Tactic: rw [← cancel_mono f]
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
α : Type u₂
F : Functor.{v₁, u₂, u₁, u₂} J (Discrete α)
j j' : J
⊢ F.obj j = F.obj j'
have as : (F.obj j).as = (F.obj j').as
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
inst_2 : IsPreconnected.{v₁, u₁} J
inst_3 : IsPreconnected.{v₂, u₂} K
⊢ IsPreconnected (J × K)
have refine : ∀ {a : Type (max u₁ u₂)} (F : J × K ⥤ Discrete a) (x x : J × K) (j : J) (k : K) (j' : J) (k' : K),
  F.obj (j, k) = F.obj (j', k')
Tactic: refine .of_any_functor_const_on_obj (fun {a} F ⟨j, k⟩ ⟨j', k'⟩ => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' X Y : J
f : X ⟶ Y
⊢ (Discrete.mk ∘ F) X = (Discrete.mk ∘ F) Y
have as : ((Discrete.mk ∘ F) X).as = ((Discrete.mk ∘ F) Y).as
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
α : Type u₁
F : Functor.{v₁, u₁, u₁, u₁} J (Discrete α)
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ F.obj j₁ = F.obj j₂
have as : (F.obj j₁).as = (F.obj j₂).as
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
aux : ∀ (j₁ j₂ : J) (f : j₁ ⟶ j₂), { down := j₁ ∈ p : ULift.{u₁, 0} Prop } = { down := j₂ ∈ p } := ⋯
⊢ j ∈ p
have i : (j ∈ p) = (j₀ ∈ p)
Tactic: injection constant_of_preserves_morphisms (fun k => ULift.up.{u₁} (k ∈ p)) aux j j₀ with i
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (j j' : J), F j = F j'
have w : ∀ (j : J), Membership.mem (γ := Set J) {j : J | F j = F j₀} j
Tactic: have w := h { j | F j = F j₀ } rfl (fun {j₁} {j₂} f => by
      change F j₁ = F j₀ ↔ F j₂ = F j₀
      simp [a f])
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
w : ∀ (j : J), Membership.mem (γ := Set J) {j : J | F j = F j₀} j
j j' : J
⊢ F j = F j'
have rw : F j₀ = F j'
Tactic: rw [w j, w j']
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
w : ∀ (j : J), Membership.mem (γ := Set J) {j : J | F j = F j₀} j
j j' : J
rw : F j₀ = F j'
⊢ F j = F j'
have rw₁ : F j₀ = F j₀
Tactic: rw [w j, w j']
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
hc : IsConnected.{v₁, u₁} J
⊢ IsConnected (ULiftHom (ULift.{u₂, u₁} J))
have h : ∀ (p : Set (ULiftHom (ULift.{u₂, u₁} J))),
  { down := Classical.choice sorry } ∈ p →
    (∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) →
      ∀ (j : ULiftHom (ULift.{u₂, u₁} J)), j ∈ p
Tactic: apply IsConnected.of_induct
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
hc : IsConnected.{v₁, u₁} J
h :
  ∀ (p : Set (ULiftHom (ULift.{u₂, u₁} J))),
    { down := Classical.choice ⋯ } ∈ p →
      (∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) →
        ∀ (j : ULiftHom (ULift.{u₂, u₁} J)), j ∈ p
⊢ IsConnected (ULiftHom (ULift.{u₂, u₁} J))
have j₀ : ULiftHom (ULift.{u₂, u₁} J)
Tactic: apply IsConnected.of_induct
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
hc : IsConnected.{v₁, u₁} J
p : Set (ULiftHom (ULift.{u₂, u₁} J))
hj₀ : { down := Classical.choice ⋯ } ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
p' : Set J := {j : J | { down := j : ULift.{u₂, u₁} J } ∈ p}
⊢ { down := j : ULift.{u₂, u₁} J } ∈ p
have hj₀' : Classical.choice sorry ∈ p'
Tactic: have hj₀' : Classical.choice hc.is_nonempty ∈ p' := by
      simp only [p']
      exact hj₀
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
X : Type u_1
a b : Discrete X
h : Zigzag a b
⊢ a.as = b.as
have refl : a.as = a.as
Tactic: induction h with
  | refl => rfl
  | tail _ h eq => exact eq.trans (eq_of_zag _ h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
X : Type u_1
a b : Discrete X
h : Zigzag a b
refl : a.as = a.as
⊢ a.as = b.as
have tail : ∀ {b c : Discrete X}, Relation.ReflTransGen Zag a b → ∀ (h : Zag b c) (eq : a.as = b.as), a.as = c.as
Tactic: induction h with
  | refl => rfl
  | tail _ h eq => exact eq.trans (eq_of_zag _ h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
inst_1 : IsPreconnected.{v₁, u₁} J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), r j₁ j₂
j₁ j₂ : J
⊢ r j₁ j₂
have have : ∀ (z : ∀ (j : J), r j₁ j), r j₁ j₂
Tactic: have z : ∀ j : J, r j₁ j :=
    induct_on_objects {k | r j₁ k} (hr.1 j₁)
      fun f => ⟨fun t => hr.3 t (h f), fun t => hr.3 t (hr.2 (h f))⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag.{v₁, u₁} j₁ j₂
⊢ IsPreconnected.{v₁, u₁} J
have h₁ : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
Tactic: apply IsPreconnected.of_constant_of_preserves_morphisms
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag.{v₁, u₁} j₁ j₂
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' : J
⊢ F j = F j'
have h₁ : Zigzag.{v₁, u₁} j j'
Tactic: specialize h j j'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' b c : J
h : Relation.ReflTransGen Zag.{v₁, u₁} j b
hj : Zag.{v₁, u₁} b c
ih : F j = F b
⊢ F j = F c
have h : F b = F c
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' b c : J
h : Relation.ReflTransGen Zag.{v₁, u₁} j b
hj : Zag.{v₁, u₁} b c
ih : F j = F b
⊢ F b = F c
have h : ∀ (hj : b ⟶ c), F b = F c
Tactic: rcases hj with (⟨⟨hj⟩⟩ | ⟨⟨hj⟩⟩)
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' b c : J
h_1 : Relation.ReflTransGen Zag.{v₁, u₁} j b
hj : Zag.{v₁, u₁} b c
ih : F j = F b
h : ∀ (hj : b ⟶ c), F b = F c
⊢ F b = F c
have h₁ : ∀ (hj : c ⟶ b), F b = F c
Tactic: rcases hj with (⟨⟨hj⟩⟩ | ⟨⟨hj⟩⟩)
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.CategoryTheory.IsConnected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' : J
h : Zigzag.{v₁, u₁} j j'
⊢ F j = F j'
have h₁ : F j = F j
Tactic: induction h with
  | refl => rfl
  | tail _ hj ih =>
    rw [ih]
    rcases hj with (⟨⟨hj⟩⟩ | ⟨⟨hj⟩⟩)
    exacts [hF hj, (hF hj).symm]
Cleared hypotheses: h