awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
⊢ Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)} f) ↔
    Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ f (m * n + k)
have trans : Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)} f) ↔
  Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f)
Tactic: trans Summable ({n : ℕ | (n : ZMod m) = k ∧ k ≤ n}.indicator f)
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
trans :
  Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)} f) ↔
    Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f)
⊢ Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)} f) ↔
    Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ f (m * n + k)
have trans₁ : Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f) ↔
  Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ f (m * n + k)
Tactic: trans Summable ({n : ℕ | (n : ZMod m) = k ∧ k ≤ n}.indicator f)
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
⊢ Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)} f) ↔
    Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f)
have rw : Summable (β := (↑{i : ℕ | i < k}ᶜ : Type))
    (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)} f ∘
      Subtype.val (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {i : ℕ | i < k}ᶜ x)) ↔
  Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f)
Tactic: rw [← (finite_lt_nat k).summable_compl_iff (f := {n : ℕ | (n : ZMod m) = k}.indicator f)]
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (hypothesis)
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun (n : ℕ) ↦ m * n + k
⊢ Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f) ↔
    Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ f (m * n + k)
have hg : Function.Injective g
Tactic: have hg : Function.Injective g := fun m n hmn ↦ by simpa [g, hm.ne] using hmn
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun (n : ℕ) ↦ m * n + k
hg : Function.Injective g
n : ℕ
hn : n ∉ range g
⊢ indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f n = 0
have contrapose! : ∀ (hn : indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f n ≠ 0), n ∈ range g
Tactic: contrapose! hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (hypothesis)
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun (n : ℕ) ↦ m * n + k
hg : Function.Injective g
⊢ Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f) ↔
    Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ f (m * n + k)
have hg' : ∀ n ∉ range g, indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f n = 0
Tactic: have hg' : ∀ n ∉ range g, {n : ℕ | (n : ZMod m) = k ∧ k ≤ n}.indicator f n = 0 := by
      intro n hn
      contrapose! hn
      exact (Nat.range_mul_add m k).symm ▸ mem_of_indicator_ne_zero hn
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun (n : ℕ) ↦ m * n + k
hg : Function.Injective g
hg' : ∀ n ∉ range g, indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f n = 0
⊢ Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f) ↔
    Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ f (m * n + k)
have h : ∀ (x : ℕ), f (m * x + k) = (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f ∘ g) x
Tactic: convert! (Function.Injective.summable_iff hg hg').symm using 3
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (hypothesis)
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
⊢ False
have this : Filter.Tendsto f Filter.atTop (nhds 0)
Tactic: have := hs.tendsto_atTop_zero
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (hypothesis)
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : Filter.Tendsto f Filter.atTop (nhds 0)
⊢ False
have this₁ : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |f n| < ε
Tactic: simp only [Metric.tendsto_atTop, dist_zero_right, Real.norm_eq_abs] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |f n| < ε
⊢ False
have obtain : ∀ (N : ℕ) (hN : ∀ n_1 ≥ N, |f n_1| < |f n|), False
Tactic: obtain ⟨N, hN⟩ := this (|f n|) (abs_pos_of_neg hn)
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (hypothesis)
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |f n| < ε
N : ℕ
hN : ∀ n_1 ≥ N, |f n_1| < |f n|
⊢ False
have hN₁ : |f (max n N)| < |f n|
Tactic: specialize hN (max n N) (n.le_max_right N)
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |f n| < ε
N : ℕ
hN : |f (max n N)| < |f n|
⊢ False
have contrapose! : ∀ (hN : True), |f n| ≤ |f (max n N)|
Tactic: contrapose! hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (hypothesis)
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |f n| < ε
N : ℕ
⊢ |f n| ≤ |f (max n N)|
have H : f (max n N) ≤ f n
Tactic: have H : f (max n N) ≤ f n := hf (n.le_max_left N)
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |f n| < ε
N : ℕ
H : f (max n N) ≤ f n
⊢ |f n| ≤ |f (max n N)|
have rwa : -f n ≤ |f (max n N)|
Tactic: rwa [abs_of_neg hn, abs_of_neg (H.trans_lt hn), neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |f n| < ε
N : ℕ
H : f (max n N) ≤ f n
rwa : -f n ≤ |f (max n N)|
⊢ |f n| ≤ |f (max n N)|
have rwa₁ : -f n ≤ -f (max n N)
Tactic: rwa [abs_of_neg hn, abs_of_neg (H.trans_lt hn), neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
m : ℕ
hm : NeZero m
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
k : ZMod m
⊢ ¬Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
have rw : ¬Summable (α := ℝ) fun (n : ℕ) ↦ f (m * n + k.val)
Tactic: rw [← ZMod.natCast_zmod_val k, summable_indicator_mod_iff_summable]
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)
have pos : ∀ (hf₀ : ∀ (n : ℕ), 0 ≤ f n), Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)
Tactic: by_cases! hf₀ : ∀ n, 0 ≤ f n
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
pos : ∀ (hf₀ : ∀ (n : ℕ), 0 ≤ f n), Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)
have neg : ∀ (hf₀ : ∃ (n : ℕ), f n < 0), Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)
Tactic: by_cases! hf₀ : ∀ n, 0 ≤ f n
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (hypothesis)
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)
have hs₁ : Summable (α := ℝ) fun (n : ℕ) ↦ f (m * n + k.val)
Tactic: rw [← ZMod.natCast_zmod_val k, summable_indicator_mod_iff_summable] at hs
Cleared hypotheses: hs, hf₀
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (hypothesis)
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable (α := ℝ) fun (n : ℕ) ↦ f (m * n + k.val)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)
have hl : HAdd.hAdd (α := ZMod m) (↑l.val : ZMod m) (↑m : ZMod m) = l
Tactic: have hl : (l.val + m : ZMod m) = l := by
      simp only [ZMod.natCast_val, ZMod.cast_id', id_eq, CharP.cast_eq_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable (α := ℝ) fun (n : ℕ) ↦ f (m * n + k.val)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
hl : HAdd.hAdd (α := ZMod m) (↑l.val : ZMod m) (↑m : ZMod m) = l
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)
have pos : Summable (α := ℝ) fun (n : ℕ) ↦ f (m * n + (l.val + m))
Tactic: rw [← hl, ← Nat.cast_add, summable_indicator_mod_iff_summable]
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
hf₀ : ∃ (n : ℕ), f n < 0
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)
have neg : ∀ (n : ℕ) (hn : f n < 0), Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)
Tactic: obtain ⟨n, hn⟩ := hf₀
Cleared hypotheses: hf₀
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f) ↔ Summable f
have refine : ∀ (H : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)), Summable f
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ Summable.indicator H _⟩
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
H : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
⊢ Summable f
have rw : Summable (α := ℝ) (∑ a : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = a} f)
Tactic: rw [Finset.sum_indicator_mod m f]
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
H : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
⊢ Summable (α := ℝ) (∑ a : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = a} f)
have h : ∀ (x : ℕ),
  Eq (α := ℝ) ((∑ a : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = a} f) x)
    (∑ i : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = i} f x)
Tactic: convert!
    summable_sum (s := Finset.univ) fun a _ ↦
      summable_indicator_mod_iff_summable_indicator_mod hf a H
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
inst_3 : CompleteSpace R
inst_4 : T0Space R
f : ℕ → R
hf : Summable f
N : ℕ
inst_5 : NeZero N
⊢ Eq.{u_1 + 1} (α := R) (∑' (n : ℕ), f n) (∑ j : ZMod N, ∑' (m : ℕ), f (j.val + N * m))
have rw : Summable.{u_1, 0} (α := R) fun (c : ZMod N × ℕ) ↦ f ((N.residueClassesEquiv.symm : (a : ZMod N × ℕ) → ℕ) c)
Tactic: rw [← (residueClassesEquiv N).symm.tsum_eq f, Summable.tsum_prod, tsum_fintype,
    residueClassesEquiv, Equiv.coe_fn_symm_mk]
-- Lean 4 proof step from Mathlib.Analysis.VonNeumannAlgebra.Basic (goal)
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ S.commutant ↔ ∀ g ∈ S, g * z = z * g
have rw : z ∈ (↑S : Set (H →L[ℂ] H)).centralizer ↔ ∀ g ∈ S, g * z = z * g
Tactic: rw [← SetLike.mem_coe, coe_commutant]
-- Lean 4 proof step from Mathlib.Analysis.VonNeumannAlgebra.Basic (goal)
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
e : H →L[ℂ] H
h : IsIdempotentElem e
S : VonNeumannAlgebra H
| ∀ y ∈ S.commutant,
    (↑e : H →ₗ[ℂ] H).range ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H) ∧
      (↑e : H →ₗ[ℂ] H).ker ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H)
have simp : e ∈ S
Tactic: simp [← h.commute_iff, Commute.symm_iff (a := e), commute_iff_eq, ← mem_commutant_iff]
-- Lean 4 proof step from Mathlib.Analysis.VonNeumannAlgebra.Basic (goal)
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
e : H →L[ℂ] H
h : IsIdempotentElem e
S : VonNeumannAlgebra H
⊢ e ∈ S ↔
    ∀ y ∈ S.commutant,
      (↑e : H →ₗ[ℂ] H).range ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H) ∧
        (↑e : H →ₗ[ℂ] H).ker ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H)
have conv_rhs : e ∈ S ↔
  ∀ y ∈ S.commutant,
    (↑e : H →ₗ[ℂ] H).range ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H) ∧
      (↑e : H →ₗ[ℂ] H).ker ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H)
Tactic: conv_rhs => simp [← h.commute_iff, Commute.symm_iff (a := e), commute_iff_eq, ← mem_commutant_iff]
-- Lean 4 proof step from Mathlib.Analysis.VonNeumannAlgebra.Basic (goal)
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
e : H →L[ℂ] H
h : IsIdempotentElem e
S : VonNeumannAlgebra H
conv_rhs :
  e ∈ S ↔
    ∀ y ∈ S.commutant,
      (↑e : H →ₗ[ℂ] H).range ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H) ∧
        (↑e : H →ₗ[ℂ] H).ker ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H)
⊢ e ∈ S ↔
    ∀ y ∈ S.commutant,
      (↑e : H →ₗ[ℂ] H).range ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H) ∧
        (↑e : H →ₗ[ℂ] H).ker ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H)
have conv_rhs₁ : e ∈ S ↔ e ∈ S
Tactic: conv_rhs => simp [← h.commute_iff, Commute.symm_iff (a := e), commute_iff_eq, ← mem_commutant_iff]
-- Lean 4 proof step from Mathlib.Analysis.VonNeumannAlgebra.Basic (goal)
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
e : H →L[ℂ] H
he : IsStarProjection e
S : VonNeumannAlgebra H
⊢ e ∈ S ↔ ∀ y ∈ S.commutant, (↑e : H →ₗ[ℂ] H).range ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H)
have simp_rw : (∀ (x : H →L[ℂ] H) (x_1 : x ∈ S.commutant), e * (x * e) = x * e) →
  ∀ (x : H →L[ℂ] H) (x_1 : x ∈ S.commutant), e * (x * e) = e * x
Tactic: simp_rw [he.isIdempotentElem.mem_iff, he.isIdempotentElem.range_mem_invtSubmodule_iff,
    he.isIdempotentElem.ker_mem_invtSubmodule_iff, forall_and, and_iff_left_iff_imp, ← mul_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (imageMonoFactorisation f).e =
    CategoryStruct.comp (Y := cokernel (X := kernel f) (kernel.ι f)) (cokernel.π (kernel.ι f))
      (coimageImageComparison f)
have dsimp : Eq (α := X ⟶ Abelian.image f) (kernel.lift (cokernel.π f) f sorry : X ⟶ kernel (Y := cokernel f) (cokernel.π f))
  (CategoryStruct.comp (Y := cokernel (X := kernel f) (kernel.ι f)) (cokernel.π (kernel.ι f))
      (coimageImageComparison f) :
    X ⟶ Abelian.image f)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := X ⟶ Abelian.image f) (kernel.lift (cokernel.π f) f ⋯ : X ⟶ kernel (Y := cokernel f) (cokernel.π f))
    (CategoryStruct.comp (Y := cokernel (X := kernel f) (kernel.ι f)) (cokernel.π (kernel.ι f))
        (coimageImageComparison f) :
      X ⟶ Abelian.image f)
have h : CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
    (kernel.lift (cokernel.π f) f sorry : X ⟶ kernel (Y := cokernel f) (cokernel.π f))
    (equalizer.ι (cokernel.π f) 0 : equalizer (Y := cokernel f) (cokernel.π f) 0 ⟶ Y) =
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
    (CategoryStruct.comp (Y := cokernel (X := kernel f) (kernel.ι f)) (cokernel.π (kernel.ι f))
      (coimageImageComparison f))
    (equalizer.ι (cokernel.π f) 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
F : MonoFactorisation f
⊢ Eq (α := (imageMonoFactorisation f).I ⟶ Y)
    (CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f)) (cokernel.desc (kernel.ι f) F.e ⋯) ≫
      F.m)
    (kernel.ι (cokernel.π f))
have simp : Eq (α := (imageMonoFactorisation f).I ⟶ Y)
  (CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
    (cokernel.desc (kernel.ι f) F.e sorry ≫ F.m))
  (kernel.ι (cokernel.π f))
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
F : MonoFactorisation f
⊢ Eq (α := (imageMonoFactorisation f).I ⟶ Y)
    (CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
      (cokernel.desc (kernel.ι f) F.e ⋯ ≫ F.m))
    (kernel.ι (cokernel.π f))
have rw : Eq (α := Abelian.coimage f ⟶ Y) (cokernel.desc (kernel.ι f) F.e sorry ≫ F.m)
  (CategoryStruct.comp (Y := (imageMonoFactorisation f).I) (coimageImageComparison f) (kernel.ι (cokernel.π f)))
Tactic: rw [IsIso.inv_comp_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
F : MonoFactorisation f
⊢ Eq (α := Abelian.coimage f ⟶ Y) (cokernel.desc (kernel.ι f) F.e ⋯ ≫ F.m)
    (CategoryStruct.comp (Y := (imageMonoFactorisation f).I) (coimageImageComparison f) (kernel.ι (cokernel.π f)))
have h : CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
    (cokernel.desc (kernel.ι f) F.e sorry ≫ F.m) =
  CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
    (CategoryStruct.comp (Y := (imageMonoFactorisation f).I) (coimageImageComparison f) (kernel.ι (cokernel.π f)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
inst_5 : Mono f
inst_6 : IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
⊢ IsIso (imageMonoFactorisation f).e
have rw : IsIso (Y := (imageMonoFactorisation f).I)
  (CategoryStruct.comp (Y := cokernel (X := kernel f) (kernel.ι f)) (cokernel.π (kernel.ι f))
    (coimageImageComparison f))
Tactic: rw [imageMonoFactorisation_e']
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
inst_5 : Epi f
⊢ IsIso (imageMonoFactorisation f).m
have dsimp : IsIso (X := Abelian.image f) (kernel.ι (cokernel.π f))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
⊢ IsLimit (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
have this : HasImages.{v, u} C
Tactic: haveI : Limits.HasImages C := hasImages
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this : HasImages.{v, u} C
⊢ IsLimit (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
have this₁ : HasEqualizers.{v, u} C
Tactic: haveI : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this_1 : HasImages.{v, u} C
this : HasEqualizers.{v, u} C
⊢ IsLimit (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
have this₁ : HasZeroObject.{v, u} C
Tactic: haveI : HasZeroObject C := Limits.hasZeroObject_of_hasFiniteBiproducts _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
⊢ IsLimit (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
have refine_2 : (aux :
    ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f)),
      (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
          Fork.ι (KernelFork.ofι f sorry) =
        Fork.ι s) →
  IsLimit (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f sorry)
Tactic: have aux (s : KernelFork (cokernel.π f)) :
            (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
            Fork.ι (KernelFork.ofι _ (cokernel.condition f)) = Fork.ι s := ?_