ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>SubtractionMonoid G<VAR>a b c d : G<VAR>hbc : AddCommute b c<VAR>hbd : AddCommute (-b) d<VAR>hcd : AddCommute (-c) d<GOAL>a - b - (c - d) = a - c - (b - d)
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<GOAL>Commute a⁻¹ b ↔ Commute a b
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<GOAL>AddCommute (-a) b ↔ AddCommute a b
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<GOAL>AddCommute a (-b) ↔ AddCommute a b
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<GOAL>Commute a b⁻¹ ↔ Commute a b
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<VAR>h : Commute a b<GOAL>a⁻¹ * b * a = b
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<VAR>h : AddCommute a b<GOAL>-a + b + a = b
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<VAR>h : AddCommute a b<GOAL>-a + (b + a) = b
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<VAR>h : Commute a b<GOAL>a⁻¹ * (b * a) = b
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<VAR>h : G<GOAL>Commute (h * a * h⁻¹) (h * b * h⁻¹) ↔ Commute a b
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<VAR>h : G<GOAL>AddCommute (h + a + -h) (h + b + -h) ↔ AddCommute a b
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<VAR>comm : Commute a b<VAR>h : G<GOAL>Commute (h * a * h⁻¹) (h * b * h⁻¹)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<VAR>comm : AddCommute a b<VAR>h : G<GOAL>AddCommute (h + a + -h) (h + b + -h)
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<VAR>h : Commute a b<VAR>m : ℤ<GOAL>Commute a (b ^ m)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<VAR>h : AddCommute a b<VAR>m : ℤ<GOAL>AddCommute a (m • b)
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<VAR>h : Commute a b<VAR>m : ℤ<GOAL>Commute (a ^ m) b
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<VAR>h : AddCommute a b<VAR>m : ℤ<GOAL>AddCommute (m • a) b
<VAR>G : Type u_1<VAR>Group G<VAR>a b : G<VAR>h : Commute a b<VAR>m n : ℤ<GOAL>Commute (a ^ m) (b ^ n)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a b : G<VAR>h : AddCommute a b<VAR>m n : ℤ<GOAL>AddCommute (m • a) (n • b)
<VAR>G : Type u_1<VAR>Group G<VAR>a : G<VAR>n : ℤ<GOAL>Commute a (a ^ n)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a : G<VAR>n : ℤ<GOAL>AddCommute a (n • a)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a : G<VAR>n : ℤ<GOAL>AddCommute (n • a) a
<VAR>G : Type u_1<VAR>Group G<VAR>a : G<VAR>n : ℤ<GOAL>Commute (a ^ n) a
<VAR>G : Type u_1<VAR>Group G<VAR>a : G<VAR>m n : ℤ<GOAL>Commute (a ^ m) (a ^ n)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a : G<VAR>m n : ℤ<GOAL>AddCommute (m • a) (n • a)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a : G<VAR>m n : ℕ<GOAL>m • -a + n • a = n • a + m • -a
<VAR>G : Type u_1<VAR>Group G<VAR>a : G<VAR>m n : ℕ<GOAL>a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>a : K<VAR>b c : K<VAR>fract_a_ne_zero : Int.fract a ≠ 0<GOAL>(↑⌊a⌋ * b + c) / Int.fract a + b = (b * a + c) / Int.fract a
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>v : K<VAR>n : ℕ<VAR>FloorRing K<VAR>ifp_n : GenContFract.IntFractPair K<GOAL>GenContFract.IntFractPair.stream v n = some ifp_n → v = GenContFract.compExactValue ((GenContFract.of v).contsAux n) ((GenContFract.of v).contsAux (n + 1)) ifp_n.fr
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>v : K<VAR>n : ℕ<VAR>FloorRing K<VAR>nth_stream_eq_none : GenContFract.IntFractPair.stream v n = none<GOAL>v = (GenContFract.of v).convs (n - 1)
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>v : K<VAR>n : ℕ<VAR>FloorRing K<VAR>terminatedAt_n : (GenContFract.of v).TerminatedAt n<GOAL>v = (GenContFract.of v).convs n
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>v : K<VAR>FloorRing K<VAR>terminates : (GenContFract.of v).Terminates<GOAL>∃ n, v = (GenContFract.of v).convs n
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>v : K<VAR>FloorRing K<VAR>terminates : (GenContFract.of v).Terminates<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, v = (GenContFract.of v).convs n
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : (i j : ι) → C.X i ⟶ D.X j<VAR>i : ι<GOAL>(dNext i) f = C.dFrom i ≫ (fromNext i) f
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : (i j : ι) → C.X i ⟶ D.X j<VAR>i i' : ι<VAR>w : c.Rel i i'<GOAL>(dNext i) f = C.d i i' ≫ f i' i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : (i j : ι) → C.X i ⟶ D.X j<VAR>i : ι<VAR>hi : ¬c.Rel i (c.next i)<GOAL>(dNext i) f = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f : C ⟶ D<VAR>g : (i j : ι) → D.X i ⟶ E.X j<VAR>i : ι<GOAL>((dNext i) fun i j => f.f i ≫ g i j) = f.f i ≫ (dNext i) g
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f : (i j : ι) → C.X i ⟶ D.X j<VAR>g : D ⟶ E<VAR>i : ι<GOAL>((dNext i) fun i j => f i j ≫ g.f j) = (dNext i) f ≫ g.f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : (i j : ι) → C.X i ⟶ D.X j<VAR>i : ι<VAR>hi : ¬c.Rel (c.prev i) i<GOAL>(prevD i) f = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : (i j : ι) → C.X i ⟶ D.X j<VAR>j : ι<GOAL>(prevD j) f = (toPrev j) f ≫ D.dTo j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : (i j : ι) → C.X i ⟶ D.X j<VAR>j j' : ι<VAR>w : c.Rel j' j<GOAL>(prevD j) f = f j j' ≫ D.d j' j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f : C ⟶ D<VAR>g : (i j : ι) → D.X i ⟶ E.X j<VAR>j : ι<GOAL>((prevD j) fun i j => f.f i ≫ g i j) = f.f j ≫ (prevD j) g
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f : (i j : ι) → C.X i ⟶ D.X j<VAR>g : D ⟶ E<VAR>j : ι<GOAL>((prevD j) fun i j => f i j ≫ g.f j) = (prevD j) f ≫ g.f j
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>C D : ChainComplex V ℕ<VAR>i : ℕ<VAR>f : (i j : ℕ) → C.X i ⟶ D.X j<GOAL>(dNext i) f = C.d i (i - 1) ≫ f (i - 1) i
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>C D : CochainComplex V ℕ<VAR>i : ℕ<VAR>f : (i j : ℕ) → C.X i ⟶ D.X j<GOAL>(prevD i) f = f i (i - 1) ≫ D.d (i - 1) i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>self : Homotopy f g<VAR>i j : ι<GOAL>¬c.Rel j i → self.hom i j = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>self : Homotopy f g<VAR>i : ι<GOAL>f.f i = (dNext i) self.hom + (prevD i) self.hom + g.f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h : f = g<VAR>i j : ι<GOAL>(Homotopy.ofEq h).hom i j = 0 i j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : C ⟶ D<VAR>i j : ι<GOAL>(Homotopy.refl f).hom i j = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h : Homotopy f g<VAR>i j : ι<GOAL>h.symm.hom i j = -h.hom i j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>e f g : C ⟶ D<VAR>h : Homotopy e f<VAR>k : Homotopy f g<VAR>i j : ι<GOAL>(h.trans k).hom i j = h.hom i j + k.hom i j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f₁ g₁ f₂ g₂ : C ⟶ D<VAR>h₁ : Homotopy f₁ g₁<VAR>h₂ : Homotopy f₂ g₂<VAR>i j : ι<GOAL>(h₁.add h₂).hom i j = h₁.hom i j + h₂.hom i j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>R : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Linear R V<VAR>h : Homotopy f g<VAR>a : R<VAR>i j : ι<GOAL>(h.smul a).hom i j = a • h.hom i j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>e f : C ⟶ D<VAR>h : Homotopy e f<VAR>g : D ⟶ E<VAR>i j : ι<GOAL>(h.compRight g).hom i j = h.hom i j ≫ g.f j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : D ⟶ E<VAR>h : Homotopy f g<VAR>e : C ⟶ D<VAR>i j : ι<GOAL>(h.compLeft e).hom i j = e.f i ≫ h.hom i j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C₁ C₂ C₃ : HomologicalComplex V c<VAR>f₁ g₁ : C₁ ⟶ C₂<VAR>f₂ g₂ : C₂ ⟶ C₃<VAR>h₁ : Homotopy f₁ g₁<VAR>h₂ : Homotopy f₂ g₂<VAR>i j : ι<GOAL>(h₁.comp h₂).hom i j = h₁.hom i j ≫ f₂.f j + g₁.f i ≫ h₂.hom i j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : C ⟶ C<VAR>h : Homotopy f (𝟙 C)<VAR>g : C ⟶ D<VAR>i j : ι<GOAL>(h.compRightId g).hom i j = h.hom i j ≫ g.f j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f : D ⟶ D<VAR>h : Homotopy f (𝟙 D)<VAR>g : C ⟶ D<VAR>i j : ι<GOAL>(h.compLeftId g).hom i j = g.f i ≫ h.hom i j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<VAR>g : D ⟶ E<GOAL>Homotopy.nullHomotopicMap hom ≫ g = Homotopy.nullHomotopicMap fun i j => hom i j ≫ g.f j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<VAR>g : D ⟶ E<GOAL>Homotopy.nullHomotopicMap' hom ≫ g = Homotopy.nullHomotopicMap' fun i j hij => hom i j hij ≫ g.f j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f : C ⟶ D<VAR>hom : (i j : ι) → D.X i ⟶ E.X j<GOAL>f ≫ Homotopy.nullHomotopicMap hom = Homotopy.nullHomotopicMap fun i j => f.f i ≫ hom i j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f : C ⟶ D<VAR>hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)<GOAL>f ≫ Homotopy.nullHomotopicMap' hom = Homotopy.nullHomotopicMap' fun i j hij => f.f i ≫ hom i j hij
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>W : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} W<VAR>CategoryTheory.Preadditive W<VAR>G : V ⥤ W<VAR>G.Additive<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<GOAL>(G.mapHomologicalComplex c).map (Homotopy.nullHomotopicMap hom) = Homotopy.nullHomotopicMap fun i j => G.map (hom i j)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>W : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} W<VAR>CategoryTheory.Preadditive W<VAR>G : V ⥤ W<VAR>G.Additive<VAR>hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<GOAL>(G.mapHomologicalComplex c).map (Homotopy.nullHomotopicMap' hom) = Homotopy.nullHomotopicMap' fun i j hij => G.map (hom i j hij)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<VAR>zero : ∀ (i j : ι), ¬c.Rel j i → hom i j = 0<VAR>i j : ι<GOAL>(Homotopy.nullHomotopy hom zero).hom i j = hom i j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<VAR>i j : ι<GOAL>(Homotopy.nullHomotopy' h).hom i j = dite (c.Rel j i) (h i j) fun x => 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>k₂ k₁ k₀ : ι<VAR>r₂₁ : c.Rel k₂ k₁<VAR>r₁₀ : c.Rel k₁ k₀<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<GOAL>(Homotopy.nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>k₂ k₁ k₀ : ι<VAR>r₂₁ : c.Rel k₂ k₁<VAR>r₁₀ : c.Rel k₁ k₀<VAR>h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<GOAL>(Homotopy.nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>k₁ k₀ : ι<VAR>r₁₀ : c.Rel k₁ k₀<VAR>hk₀ : ∀ (l : ι), ¬c.Rel k₀ l<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<GOAL>(Homotopy.nullHomotopicMap hom).f k₀ = hom k₀ k₁ ≫ D.d k₁ k₀
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>k₁ k₀ : ι<VAR>r₁₀ : c.Rel k₁ k₀<VAR>hk₀ : ∀ (l : ι), ¬c.Rel k₀ l<VAR>h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<GOAL>(Homotopy.nullHomotopicMap' h).f k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>k₁ k₀ : ι<VAR>r₁₀ : c.Rel k₁ k₀<VAR>hk₁ : ∀ (l : ι), ¬c.Rel l k₁<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<GOAL>(Homotopy.nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>k₁ k₀ : ι<VAR>r₁₀ : c.Rel k₁ k₀<VAR>hk₁ : ∀ (l : ι), ¬c.Rel l k₁<VAR>h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<GOAL>(Homotopy.nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>k₀ : ι<VAR>hk₀ : ∀ (l : ι), ¬c.Rel k₀ l<VAR>hk₀' : ∀ (l : ι), ¬c.Rel l k₀<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<GOAL>(Homotopy.nullHomotopicMap hom).f k₀ = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>k₀ : ι<VAR>hk₀ : ∀ (l : ι), ¬c.Rel k₀ l<VAR>hk₀' : ∀ (l : ι), ¬c.Rel l k₀<VAR>h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<GOAL>(Homotopy.nullHomotopicMap' h).f k₀ = 0
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>P Q : ChainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<VAR>j : ℕ<GOAL>(prevD j) f = f j (j + 1) ≫ Q.d (j + 1) j
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>P Q : ChainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<VAR>i : ℕ<GOAL>(dNext (i + 1)) f = P.d (i + 1) i ≫ f i (i + 1)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>P Q : ChainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<GOAL>(dNext 0) f = 0
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>P Q : ChainComplex V ℕ<VAR>e : P ⟶ Q<VAR>zero : P.X 0 ⟶ Q.X 1<VAR>comm_zero : e.f 0 = zero ≫ Q.d 1 0<VAR>one : P.X 1 ⟶ Q.X 2<VAR>comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1<VAR>succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X (n + 1)) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) → (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)<GOAL>Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ 0 = ⟨0, ⟨zero ≫ (HomologicalComplex.xPrevIso Q ⋯).inv, ⋯⟩⟩
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>P Q : ChainComplex V ℕ<VAR>e : P ⟶ Q<VAR>zero : P.X 0 ⟶ Q.X 1<VAR>comm_zero : e.f 0 = zero ≫ Q.d 1 0<VAR>one : P.X 1 ⟶ Q.X 2<VAR>comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1<VAR>succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X (n + 1)) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) → (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)<VAR>n : ℕ<GOAL>Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ (n + 1) = let I := Homotopy.mkInductiveAux₁ e zero one comm_one succ n; ⟨(HomologicalComplex.xNextIso P ⋯).hom ≫ I.fst, ⟨I.snd.fst ≫ (HomologicalComplex.xPrevIso Q ⋯).inv, ⋯⟩⟩
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>P Q : ChainComplex V ℕ<VAR>e : P ⟶ Q<VAR>zero : P.X 0 ⟶ Q.X 1<VAR>comm_zero : e.f 0 = zero ≫ Q.d 1 0<VAR>one : P.X 1 ⟶ Q.X 2<VAR>comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1<VAR>succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X (n + 1)) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) → (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)<VAR>i j : ℕ<VAR>h : i + 1 = j<GOAL>(Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (HomologicalComplex.xPrevIso Q h).hom = (HomologicalComplex.xNextIso P h).inv ≫ (Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ j).fst
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>P Q : CochainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<VAR>j : ℕ<GOAL>(dNext j) f = P.d j (j + 1) ≫ f (j + 1) j
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>P Q : CochainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<VAR>i : ℕ<GOAL>(prevD (i + 1)) f = f (i + 1) i ≫ Q.d i (i + 1)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>P Q : CochainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<GOAL>(prevD 0) f = 0
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>P Q : CochainComplex V ℕ<VAR>e : P ⟶ Q<VAR>zero : P.X 1 ⟶ Q.X 0<VAR>comm_zero : e.f 0 = P.d 0 1 ≫ zero<VAR>one : P.X 2 ⟶ Q.X 1<VAR>comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one<VAR>succ : (n : ℕ) → (p : (f : P.X (n + 1) ⟶ Q.X n) ×' (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') → (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''<GOAL>Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ 0 = ⟨0, ⟨(HomologicalComplex.xNextIso P ⋯).hom ≫ zero, ⋯⟩⟩
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>P Q : CochainComplex V ℕ<VAR>e : P ⟶ Q<VAR>zero : P.X 1 ⟶ Q.X 0<VAR>comm_zero : e.f 0 = P.d 0 1 ≫ zero<VAR>one : P.X 2 ⟶ Q.X 1<VAR>comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one<VAR>succ : (n : ℕ) → (p : (f : P.X (n + 1) ⟶ Q.X n) ×' (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') → (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''<VAR>n : ℕ<GOAL>Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ (n + 1) = let I := Homotopy.mkCoinductiveAux₁ e zero one comm_one succ n; ⟨I.fst ≫ (HomologicalComplex.xPrevIso Q ⋯).inv, ⟨(HomologicalComplex.xNextIso P ⋯).hom ≫ I.snd.fst, ⋯⟩⟩
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>P Q : CochainComplex V ℕ<VAR>e : P ⟶ Q<VAR>zero : P.X 1 ⟶ Q.X 0<VAR>comm_zero : e.f 0 = P.d 0 1 ≫ zero<VAR>one : P.X 2 ⟶ Q.X 1<VAR>comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one<VAR>succ : (n : ℕ) → (p : (f : P.X (n + 1) ⟶ Q.X n) ×' (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') → (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''<VAR>i j : ℕ<VAR>h : i + 1 = j<GOAL>(HomologicalComplex.xNextIso P h).inv ≫ (Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst = (Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst ≫ (HomologicalComplex.xPrevIso Q h).hom
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>W : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} W<VAR>CategoryTheory.Preadditive W<VAR>F : V ⥤ W<VAR>F.Additive<VAR>f g : C ⟶ D<VAR>h : Homotopy f g<VAR>i j : ι<GOAL>(F.mapHomotopy h).hom i j = F.map (h.hom i j)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>W : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} W<VAR>CategoryTheory.Preadditive W<VAR>F : V ⥤ W<VAR>F.Additive<VAR>h : HomotopyEquiv C D<GOAL>(F.mapHomotopyEquiv h).inv = (F.mapHomologicalComplex c).map h.inv
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>W : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} W<VAR>CategoryTheory.Preadditive W<VAR>F : V ⥤ W<VAR>F.Additive<VAR>h : HomotopyEquiv C D<GOAL>(F.mapHomotopyEquiv h).homotopyInvHomId = ⋯.mpr (⋯.mpr (F.mapHomotopy h.homotopyInvHomId))
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>W : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} W<VAR>CategoryTheory.Preadditive W<VAR>F : V ⥤ W<VAR>F.Additive<VAR>h : HomotopyEquiv C D<GOAL>(F.mapHomotopyEquiv h).hom = (F.mapHomologicalComplex c).map h.hom
<VAR>ι : Type u_1<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Preadditive V<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>W : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} W<VAR>CategoryTheory.Preadditive W<VAR>F : V ⥤ W<VAR>F.Additive<VAR>h : HomotopyEquiv C D<GOAL>(F.mapHomotopyEquiv h).homotopyHomInvId = ⋯.mpr (⋯.mpr (F.mapHomotopy h.homotopyHomInvId))
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_4<VAR>c : ComplexShape ι<VAR>DecidableRel c.Rel<VAR>K L : HomologicalComplex C c<VAR>f g : K ⟶ L<VAR>ho : Homotopy f g<VAR>i : ι<VAR>K.HasHomology i<VAR>L.HasHomology i<GOAL>HomologicalComplex.homologyMap f i = HomologicalComplex.homologyMap g i
<VAR>S : Type u_3<VAR>Mul S<VAR>a b : S<GOAL>Commute a b ↔ a * b = b * a
<VAR>S : Type u_3<VAR>Add S<VAR>a b : S<GOAL>AddCommute a b ↔ a + b = b + a
<VAR>S : Type u_3<VAR>Mul S<VAR>a b : S<VAR>h : Commute a b<GOAL>a * b = b * a
<VAR>S : Type u_3<VAR>Add S<VAR>a b : S<VAR>h : AddCommute a b<GOAL>a + b = b + a
<VAR>S : Type u_3<VAR>Add S<VAR>a : S<GOAL>AddCommute a a
<VAR>S : Type u_3<VAR>Mul S<VAR>a : S<GOAL>Commute a a
<VAR>S : Type u_3<VAR>Mul S<VAR>a b : S<VAR>h : Commute a b<GOAL>Commute b a
<VAR>S : Type u_3<VAR>Add S<VAR>a b : S<VAR>h : AddCommute a b<GOAL>AddCommute b a
<VAR>S : Type u_3<VAR>Mul S<VAR>a b : S<VAR>h : Commute a b<GOAL>SemiconjBy a b b