awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst_2 : Mono i
pos : ∀ (h : Δ' = Δ), eqToHom ⋯ ≫ f.f Δ.len = f.f Δ'.len ≫ eqToHom ⋯
pos₁ :
  ∀ (h : ¬Δ' = Δ),
    Isδ₀ i → Eq (α := K.X Δ'.len ⟶ K'.X Δ.len) (K.d Δ'.len Δ.len ≫ f.f Δ.len) (f.f Δ'.len ≫ K'.d Δ'.len Δ.len)
⊢ Eq (α := K.X Δ'.len ⟶ K'.X Δ.len)
    ((if h : Δ' = Δ then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ'.len Δ.len else 0) ≫ f.f Δ.len)
    (f.f Δ'.len ≫ if h : Δ' = Δ then eqToHom ⋯ else if h : Isδ₀ i then K'.d Δ'.len Δ.len else 0)
have neg : ∀ (h : ¬Δ' = Δ), ¬Isδ₀ i → Eq (α := K.X Δ'.len ⟶ K'.X Δ.len) (0 ≫ f.f Δ.len) (f.f Δ'.len ≫ 0)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst_2 : Mono i
h : Δ' = Δ
⊢ eqToHom ⋯ ≫ f.f Δ.len = f.f Δ'.len ≫ eqToHom ⋯
have pos : ∀ (i : Δ' ⟶ Δ') [Mono i], eqToHom sorry ≫ f.f Δ'.len = f.f Δ'.len ≫ eqToHom sorry
Tactic: subst h
Cleared hypotheses: Δ, i, inst_2, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst_2 : Mono i
h : ¬Δ' = Δ
h_1 : Isδ₀ i
⊢ Eq (α := K.X Δ'.len ⟶ K'.X Δ.len) (K.d Δ'.len Δ.len ≫ f.f Δ.len) (f.f Δ'.len ≫ K'.d Δ'.len Δ.len)
have pos : Eq (α := K.X Δ'.len ⟶ K'.X Δ.len) (K.d Δ'.len Δ.len ≫ f.f Δ.len) (K.d Δ'.len Δ.len ≫ f.f Δ.len)
Tactic: rw [HomologicalComplex.Hom.comm]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst_2 : Mono i
h : ¬Δ' = Δ
h_1 : ¬Isδ₀ i
⊢ Eq (α := K.X Δ'.len ⟶ K'.X Δ.len) (0 ≫ f.f Δ.len) (f.f Δ'.len ≫ 0)
have neg : Eq (α := K.X Δ'.len ⟶ K'.X Δ.len) 0 (f.f Δ'.len ≫ 0)
Tactic: rw [zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst_2 : Mono i
h : ¬Δ' = Δ
h_1 : ¬Isδ₀ i
neg : Eq (α := K.X Δ'.len ⟶ K'.X Δ.len) 0 (f.f Δ'.len ≫ 0)
⊢ Eq (α := K.X Δ'.len ⟶ K'.X Δ.len) (0 ≫ f.f Δ.len) (f.f Δ'.len ≫ 0)
have neg₁ : Eq.{v_1 + 1} (α := K.X Δ'.len ⟶ K'.X Δ.len) 0 0
Tactic: rw [zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
have pos : ∀ (h₁ : Δ = Δ'), mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
Tactic: by_cases h₁ : Δ = Δ'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
pos : ∀ (h₁ : Δ = Δ'), mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
have neg : ∀ (h₁ : ¬Δ = Δ'), mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
Tactic: by_cases h₁ : Δ = Δ'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : Δ = Δ'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
have pos : ∀ (i' : Δ'' ⟶ Δ) (i : Δ ⟶ Δ) [inst_4 : Mono i'] [inst_5 : Mono i], mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
Tactic: subst h₁
Cleared hypotheses: Δ', i', i, inst_2, inst_3, h₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
have pos : ∀ (h₂ : Δ' = Δ''), mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
Tactic: by_cases h₂ : Δ' = Δ''
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
pos : ∀ (h₂ : Δ' = Δ''), mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
have neg : ∀ (h₂ : ¬Δ' = Δ''), mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
Tactic: by_cases h₂ : Δ' = Δ''
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : Δ' = Δ''
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
have pos : ∀ (i' : Δ' ⟶ Δ') [inst_4 : Mono i'], mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
Tactic: subst h₂
Cleared hypotheses: Δ'', i', inst_2, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
have neg : ∀ (k : ℕ) (hk : Δ.len = Δ'.len + k + 1), mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
Tactic: obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i h₁)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
have neg : ∀ (k' : ℕ) (hk' : Δ'.len = Δ''.len + k' + 1), mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
Tactic: obtain ⟨k', hk'⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i' h₂)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
have eq : Δ.len = Δ''.len + (k + k' + 2)
Tactic: have eq : Δ.len = Δ''.len + (k + k' + 2) := by lia
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
have neg : mapMono K i ≫ mapMono K i' = 0
Tactic: rw [mapMono_eq_zero K (i' ≫ i) _ _]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
neg : mapMono K i ≫ mapMono K i' = 0
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
have rw : Δ ≠ Δ''
Tactic: rw [mapMono_eq_zero K (i' ≫ i) _ _]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
neg : mapMono K i ≫ mapMono K i' = 0
rw : Δ ≠ Δ''
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
have rw₁ : ¬Isδ₀ (i' ≫ i)
Tactic: rw [mapMono_eq_zero K (i' ≫ i) _ _]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h : Isδ₀ (i' ≫ i)
⊢ False
have eq₁ : 1 = k + k' + 2
Tactic: simp only [h.1, add_right_inj] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = 0
have pos : ∀ (h₃ : Isδ₀ i), mapMono K i ≫ mapMono K i' = 0
Tactic: by_cases h₃ : Isδ₀ i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
pos : ∀ (h₃ : Isδ₀ i), mapMono K i ≫ mapMono K i' = 0
⊢ mapMono K i ≫ mapMono K i' = 0
have neg : ∀ (h₃ : ¬Isδ₀ i), mapMono K i ≫ mapMono K i' = 0
Tactic: by_cases h₃ : Isδ₀ i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
⊢ mapMono K i ≫ mapMono K i' = 0
have pos : ∀ (h₄ : Isδ₀ i'), mapMono K i ≫ mapMono K i' = 0
Tactic: by_cases h₄ : Isδ₀ i'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
pos : ∀ (h₄ : Isδ₀ i'), mapMono K i ≫ mapMono K i' = 0
⊢ mapMono K i ≫ mapMono K i' = 0
have neg : ∀ (h₄ : ¬Isδ₀ i'), mapMono K i ≫ mapMono K i' = 0
Tactic: by_cases h₄ : Isδ₀ i'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : Isδ₀ i'
⊢ mapMono K i ≫ mapMono K i' = 0
have pos : Eq (α := K.X Δ.len ⟶ K.X Δ''.len) (K.d Δ.len Δ'.len ≫ mapMono K i') 0
Tactic: rw [mapMono_δ₀' K i h₃, mapMono_δ₀' K i' h₄, HomologicalComplex.d_comp_d]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : Isδ₀ i'
pos : Eq (α := K.X Δ.len ⟶ K.X Δ''.len) (K.d Δ.len Δ'.len ≫ mapMono K i') 0
⊢ mapMono K i ≫ mapMono K i' = 0
have pos₁ : Eq (α := K.X Δ.len ⟶ K.X Δ''.len) (CategoryStruct.comp (Y := K.X Δ'.len) (K.d Δ.len Δ'.len) (K.d Δ'.len Δ''.len)) 0
Tactic: rw [mapMono_δ₀' K i h₃, mapMono_δ₀' K i' h₄, HomologicalComplex.d_comp_d]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : Isδ₀ i'
pos : Eq (α := K.X Δ.len ⟶ K.X Δ''.len) (K.d Δ.len Δ'.len ≫ mapMono K i') 0
pos₁ :
  Eq (α := K.X Δ.len ⟶ K.X Δ''.len) (CategoryStruct.comp (Y := K.X Δ'.len) (K.d Δ.len Δ'.len) (K.d Δ'.len Δ''.len)) 0
⊢ mapMono K i ≫ mapMono K i' = 0
have pos₂ : Eq.{v_1 + 1} (α := K.X Δ.len ⟶ K.X Δ''.len) 0 0
Tactic: rw [mapMono_δ₀' K i h₃, mapMono_δ₀' K i' h₄, HomologicalComplex.d_comp_d]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Eq (α := summand K Δ A ⟶ obj₂ K Δ') (Sigma.ι (summand K Δ) A ≫ map K θ)
    (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
have simp : Eq (α := summand K Δ A ⟶ obj₂ K Δ')
  (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
    (Sigma.ι (summand K Δ') (A.pull θ)))
  (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
Tactic: simp only [map, colimit.ι_desc, Cofan.mk_ι_app]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Eq (α := summand K Δ A ⟶ obj₂ K Δ')
    (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
      (Sigma.ι (summand K Δ') (A.pull θ)))
    (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
have obtain : ∀ {e : unop Δ' ⟶ image (θ.unop ≫ A.e)}
  {i : image (θ.unop ≫ A.e) ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))}
  [inst_5 : Epi e] [inst_6 : Mono i] (fac : e ≫ i = θ.unop ≫ A.e),
  Eq (α := summand K Δ A ⟶ obj₂ K Δ')
    (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
      (Sigma.ι (summand K Δ') (A.pull θ)))
    (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
Tactic: obtain rfl := SimplexCategory.image_eq fac
Cleared hypotheses: Δ'', e, i, inst_3, inst_4, fac
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Eq (α := summand K Δ A ⟶ obj₂ K Δ')
    (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
      (Sigma.ι (summand K Δ') (A.pull θ)))
    (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
have e_a : image.ι (θ.unop ≫ A.e) = i
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
e_a : image.ι (θ.unop ≫ A.e) = i
⊢ Eq (α := summand K Δ A ⟶ obj₂ K Δ')
    (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
      (Sigma.ι (summand K Δ') (A.pull θ)))
    (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
have e_a₁ : A.pull θ = Splitting.IndexSet.mk e
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Splitting.IndexSet.mk (Δ' := image (θ.unop ≫ A.e)) (factorThruImage (θ.unop ≫ A.e)) = Splitting.IndexSet.mk e
have e_a : factorThruImage (θ.unop ≫ A.e) = e
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategoryᵒᵖ
x : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) =
    Quiver.Hom.unop (𝟙 Δ) ≫ A.e
have rw : A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) = 𝟙 (unop Δ) ≫ A.e
Tactic: rw [unop_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategoryᵒᵖ
x : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
rw : A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) = 𝟙 (unop Δ) ≫ A.e
⊢ A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) =
    Quiver.Hom.unop (𝟙 Δ) ≫ A.e
have rw₁ : A.e = 𝟙 (unop Δ) ≫ A.e
Tactic: rw [unop_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategoryᵒᵖ
x : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
rw : A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) = 𝟙 (unop Δ) ≫ A.e
rw₁ : A.e = 𝟙 (unop Δ) ≫ A.e
⊢ A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) =
    Quiver.Hom.unop (𝟙 Δ) ≫ A.e
have rw₂ : A.e = A.e
Tactic: rw [unop_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategoryᵒᵖ
x : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A) { as := A } ≫ Obj.map K (𝟙 Δ) =
    colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
        { as := A : Discrete (Splitting.IndexSet Δ) } ≫
      𝟙 (Obj.obj₂ K Δ)
have fac : A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) =
  Quiver.Hom.unop (𝟙 Δ) ≫ A.e
Tactic: have fac : A.e ≫ 𝟙 A.1.unop = (𝟙 Δ).unop ≫ A.e := by rw [unop_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategoryᵒᵖ
x : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac :
  A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) =
    Quiver.Hom.unop (𝟙 Δ) ≫ A.e
⊢ colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A) { as := A } ≫ Obj.map K (𝟙 Δ) =
    colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
        { as := A : Discrete (Splitting.IndexSet Δ) } ≫
      𝟙 (Obj.obj₂ K Δ)
have rw : Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e) =
  colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
      { as := A : Discrete (Splitting.IndexSet Δ) } ≫
    𝟙 (Obj.obj₂ K Δ)
Tactic: rw [Obj.map_on_summand₀ K A fac, Obj.Termwise.mapMono_id, id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategoryᵒᵖ
x : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac :
  A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) =
    Quiver.Hom.unop (𝟙 Δ) ≫ A.e
⊢ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e) =
    colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
        { as := A : Discrete (Splitting.IndexSet Δ) } ≫
      𝟙 (Obj.obj₂ K Δ)
have dsimp : Eq.{v_1 + 1} (α := Obj.summand K Δ A ⟶ sigmaObj.{0, v_1, u_1} fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
  (Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))
  (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A) { as := A } ≫
    𝟙 (sigmaObj.{0, v_1, u_1} fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A))
Tactic: dsimp only [Obj.obj₂]