mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C (a + 0)).obj X = (shiftFunctor C a).obj X

Tactic:
add_zero

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C a).obj X = (shiftFunctor C a).obj X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C a).obj X = (shiftFunctor C (a + 0)).obj X

Tactic:
add_zero

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C a).obj X = (shiftFunctor C a).obj X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
⊢ j + 0 = j

Tactic:
add_zero

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
⊢ j = j
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
X : C
⊢ j + 0 = j

Tactic:
add_zero

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
X : C
⊢ j = j
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3) =
    (succ
        { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
          X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1),
          g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).fst

Tactic:
rw [← mk_congr_succ_X₃ succ
      (mkAux_eq_shortComplex_mk_d_comp_d X₀ X₁ X₂ d₀ d₁ s succ n)]

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3) = (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).fst
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ (shiftFunctorZero C A).inv.app X ≫ (shiftFunctorAdd' C p' p 0 hp).hom.app X =
    (shiftFunctorZero C A).inv.app X ≫
      (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
        (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
              (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)

Tactic:
congr 1

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ (shiftFunctorAdd' C p' p 0 hp).hom.app X =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' + 0 = n'

Tactic:
add_zero

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' = n'
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ ∀ (x y : Ω[S⁄R]),
    x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) →
      y ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) → f x = f' x → f y = f' y → f (x + y) = f' (x + y)

Tactic:
intro x y _ _ hx hy; rw [map_add, map_add, hx, hy]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
⊢ (TensorProduct.lmul' R).kerSquareLift (f x) =
    (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) (f x))

Tactic:
generalize f x = y

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
y : S ⊗[R] S ⧸ ideal R S ^ 2
⊢ (TensorProduct.lmul' R).kerSquareLift y =
    (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) y)
Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
i j : ι
I : C
inst✝ : Injective I
hij : ¬j = i
⊢ Injective (((single C c i).obj I).X j)

Tactic:
exact (isZero_single_obj_X _ _ _ _ hij).injective

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this : (i (0 + n)).hom.app X = eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯
⊢ eqToHom ⋯ ≫
      (i n).hom.app X ≫
        (shiftFunctor D n).map ((shiftFunctorZero D A).inv.app (F.obj X)) ≫ (shiftFunctor D n).map ((i 0).inv.app X) =
    eqToHom ⋯ ≫ F.map ((s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X)

Tactic:
congr 1

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this : (i (0 + n)).hom.app X = eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯
⊢ (i n).hom.app X ≫
      (shiftFunctor D n).map ((shiftFunctorZero D A).inv.app (F.obj X)) ≫ (shiftFunctor D n).map ((i 0).inv.app X) =
    F.map ((s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ single x z + single y z - single (x + y) z ∈ kerTotal R S

Tactic:
simp_rw [← Finsupp.smul_single_one _ z, ← smul_add, ← smul_sub]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ z • (single x 1 + single y 1 - single (x + y) 1) ∈ kerTotal R S
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ z • (single y x + single x y - single (x * y) 1) ∈ kerTotal R S

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span (Or.inl <| Or.inr <| ⟨⟨_, _⟩, rfl⟩))

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
⊢ Submodule.map (linearCombination A ⇑(D R A)) (Submodule.comap (linearCombination A ⇑(D R A)) (map R S A B).ker) =
    Submodule.map (linearCombination A ⇑(D R A))
      (Submodule.comap (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
        (Submodule.restrictScalars A (kerTotal S B)))

Tactic:
congr 1

Goal state after:
case e_p
R : Type u
S : Type v
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
⊢ Submodule.comap (linearCombination A ⇑(D R A)) (map R S A B).ker =
    Submodule.comap (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
      (Submodule.restrictScalars A (kerTotal S B))
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case e'_2.e'_3
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A (Set.range (⇑(linearCombination A ⇑(D R A)) ∘ fun x ↦ single ((algebraMap R A) x) 1)) = ⊥

pp: case convert_3
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ OrderBot (Submodule A Ω[A⁄R])

Tactic:
Submodule.span_eq_bot

Goal state after:
case e'_2.e'_3
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ ∀ x ∈ Set.range (⇑(linearCombination A ⇑(D R A)) ∘ fun x ↦ single ((algebraMap R A) x) 1), x = 0
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
y : Ω[A⁄R]
⊢ x • (mapBaseChange R A B) (1 ⊗ₜ[A] y) = x • (map R R A B) y

Tactic:
congr 1

Goal state after:
case e_a
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
y : Ω[A⁄R]
⊢ (mapBaseChange R A B) (1 ⊗ₜ[A] y) = (map R R A B) y
Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
A : C
i : ι
f g : (K ⊞ L).X i ⟶ A
x✝ : biprod.inl.f i ≫ f = biprod.inl.f i ≫ g ∧ biprod.inr.f i ≫ f = biprod.inr.f i ≫ g
h₁ : biprod.inl.f i ≫ f = biprod.inl.f i ≫ g
h₂ : biprod.inr.f i ≫ f = biprod.inr.f i ≫ g
⊢ f = g

Tactic:
rw [← cancel_epi (𝟙 _)]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
A : C
i : ι
f g : (K ⊞ L).X i ⟶ A
x✝ : biprod.inl.f i ≫ f = biprod.inl.f i ≫ g ∧ biprod.inr.f i ≫ f = biprod.inr.f i ≫ g
h₁ : biprod.inl.f i ≫ f = biprod.inl.f i ≫ g
h₂ : biprod.inr.f i ≫ f = biprod.inr.f i ≫ g
⊢ 𝟙 ((K ⊞ L).X i) ≫ f = 𝟙 ((K ⊞ L).X i) ≫ g
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case e'_3
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
⊢ Submodule.map (linearCombination B ⇑(D R B))
      (Submodule.comap (mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B ⇑(algebraMap B B))
        (Submodule.restrictScalars B (kerTotal A B))) =
    Submodule.map (linearCombination B ⇑(D R B)) (kerTotal A B)

Tactic:
congr 1

Goal state after:
case e'_3.e_p
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
⊢ Submodule.comap (mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B ⇑(algebraMap B B))
      (Submodule.restrictScalars B (kerTotal A B)) =
    kerTotal A B
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
⊢ 1 ⊗ₜ[A] (linearCombination A ⇑(D R A)) x ∈ (kerCotangentToTensor R A B).range

Tactic:
← Finsupp.sum_single x,

Goal state after:
case mpr
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
⊢ 1 ⊗ₜ[A] (linearCombination A ⇑(D R A)) (x.sum single) ∈ (kerCotangentToTensor R A B).range
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
⊢ 1 ⊗ₜ[A] (linearCombination A ⇑(D R A)) (∑ a ∈ x.support, single a (x a)) ∈ (kerCotangentToTensor R A B).range

Tactic:
← Finset.sum_fiberwise_of_maps_to
      (fun _ ↦ Finset.mem_image_of_mem (algebraMap A B))

Goal state after:
case mpr
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
⊢ 1 ⊗ₜ[A]
      (linearCombination A ⇑(D R A))
        (∑ j ∈ Finset.image (⇑(algebraMap A B)) x.support,
          ∑ i ∈ x.support with (algebraMap A B) i = j, single i (x i)) ∈
    (kerCotangentToTensor R A B).range
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q : ℤ
hpq : p + 0 = q
⊢ G.X p = G.X (p + 0)

Tactic:
add_zero

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q : ℤ
hpq : p + 0 = q
⊢ G.X p = G.X p
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q q' : ℤ
hpq : p + 0 = q
⊢ (ofHoms ψ).v p q hpq ≫ G.d q q' = ψ p ≫ G.d p q'

Tactic:
add_zero

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q q' : ℤ
hpq✝ : p + 0 = q
hpq : p = q
⊢ (ofHoms ψ).v p q hpq✝ ≫ G.d q q' = ψ p ≫ G.d p q'
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p q : ℤ
hpq : p + 0 = q
⊢ F.d p' p ≫ (ofHoms ψ).v p q hpq = F.d p' q ≫ ψ q

Tactic:
add_zero

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p' p q : ℤ
hpq✝ : p + 0 = q
hpq : p = q
⊢ F.d p' p ≫ (ofHoms ψ).v p q hpq✝ = F.d p' q ≫ ψ q
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f₁ g₁ f₂ g₂ : C ⟶ D
h₁ : Homotopy f₁ g₁
h₂ : Homotopy f₂ g₂
i j : ι
hij : ¬c.Rel j i
⊢ 0 + 0 = 0

Tactic:
add_zero

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f₁ g₁ f₂ g₂ : C ⟶ D
h₁ : Homotopy f₁ g₁
h₂ : Homotopy f₂ g₂
i j : ι
hij : ¬c.Rel j i
⊢ 0 = 0
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f₁ g₁ f₂ g₂ : C ⟶ D
h₁ : Homotopy f₁ g₁
h₂ : Homotopy f₂ g₂
i j : ι
hij : ¬c.Rel j i
⊢ (h₁.hom + h₂.hom) i j = 0

Tactic:
by rw [Pi.add_apply, Pi.add_apply, h₁.zero i j hij, h₂.zero i j hij, add_zero]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
this : Subsingleton Ω[B⁄A]
⊢ ⊤ ≤ (map R A B B).ker

Tactic:
exact fun x _ ↦ Subsingleton.elim _ _

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K (-n₂)
z₃ : Cochain K L n₂
h₁₂ : n₁ + -n₂ = n₁₂
⊢ n₁ + 0 = n₁

Tactic:
add_zero

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K (-n₂)
z₃ : Cochain K L n₂
h₁₂ : n₁ + -n₂ = n₁₂
⊢ n₁ = n₁
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → C.X i ⟶ D.X j
zero : ∀ (i j : ι), ¬c.Rel j i → hom i j = 0
i : ι
⊢ (nullHomotopicMap hom).f i = (dNext i) hom + (prevD i) hom + 0

Tactic:
add_zero

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → C.X i ⟶ D.X j
zero : ∀ (i j : ι), ¬c.Rel j i → hom i j = 0
i : ι
⊢ (nullHomotopicMap hom).f i = (dNext i) hom + (prevD i) hom
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ C.d k₁ k₀ ≫ hom k₀ k₁ + 0 = C.d k₁ k₀ ≫ hom k₀ k₁

pp: case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel (c.prev k₁) k₁

Tactic:
add_zero

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ C.d k₁ k₀ ≫ hom k₀ k₁ = C.d k₁ k₀ ≫ hom k₀ k₁

case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel (c.prev k₁) k₁
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ 0 + 0 = 0

pp: case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel (c.prev k₀) k₀

pp: case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel k₀ (c.next k₀)

Tactic:
add_zero

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ 0 = 0

case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel (c.prev k₀) k₀

case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel k₀ (c.next k₀)
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
⊢ hα.hom (c.next j) j + 0 = hα.hom (c.next j) j

Tactic:
add_zero

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
⊢ hα.hom (c.next j) j = hα.hom (c.next j) j
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case pos.refine_1
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
H : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : c.Rel i (c.next i)
⊢ (mapArrowHom φ φ H (𝟙 (Arrow.mk φ))).f i ≫ fstX φ i (c.next i) hi = 𝟙 (X φ i) ≫ fstX φ i (c.next i) hi

Tactic:
simp [mapArrowHom, desc_f _ _ _ _ _ hi, inrCompHomotopy_hom _ _ _ _ hi]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case pos.refine_2
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
H : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : c.Rel i (c.next i)
⊢ (mapArrowHom φ φ H (𝟙 (Arrow.mk φ))).f i ≫ sndX φ i = 𝟙 (X φ i) ≫ sndX φ i

Tactic:
simp [mapArrowHom, desc_f _ _ _ _ _ hi, inrCompHomotopy_hom _ _ _ _ hi]

Goal state after: