mathlib-initiative/mathlib-tactics huggingface dataset:
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⁄R]
hx : x ∈ (map R R A B).ker
⊢ (LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B)) ((TensorProduct.lid A Ω[A⁄R]).symm x) ∈
    (kerCotangentToTensor R A B).range

Tactic:
rw [KaehlerDifferential.ker_map_of_surjective R A B h] at hx

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⁄R]
hx :
  x ∈
    Submodule.map (linearCombination A ⇑(D R A))
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
⊢ (LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B)) ((TensorProduct.lid A Ω[A⁄R]).symm x) ∈
    (kerCotangentToTensor R A B).range
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
f : (i j : ι) → C.X i ⟶ D.X j
i i' : ι
w : c.Rel i i'
⊢ (dNext i) f = C.d i i' ≫ f i' i

Tactic:
by

Goal state after:
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
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (dNext i) f = 0

Tactic:
by

Goal state after:
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
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel (c.prev i) i
⊢ (prevD i) f = 0

Tactic:
by

Goal state after:
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
f : (i j : ι) → C.X i ⟶ D.X j
j j' : ι
w : c.Rel j' j
⊢ (prevD j) f = f j j' ≫ D.d j' j

Tactic:
by

Goal state after:
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 : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
j : ι
⊢ ((prevD j) fun i j ↦ f i j ≫ g.f j) = (prevD j) f ≫ g.f j

Tactic:
by

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)
x : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
⊢ ∑ i ∈ x.support with (algebraMap A B) i = c, x i ∈ RingHom.ker (algebraMap A B)

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ (dNext i) f = C.d i (i - 1) ≫ f (i - 1) i

Tactic:
by

Goal state after:
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 ℤ
n : ℤ
z₁ z₂ : Cochain F G n
h : z₁ = z₂
p q : ℤ
hpq : p + n = q
⊢ z₁.v p q hpq = z₂.v p q hpq

Tactic:
by

Goal state after:
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 ℤ
n : ℤ
z₁ z₂ : Cochain F G n
h : ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq
⊢ z₁ = z₂

Tactic:
by

Goal state after:
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 ℤ
z₁ z₂ : Cochain F G 0
h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯
⊢ z₁ = z₂

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ (prevD i) f = f i (i - 1) ≫ D.d (i - 1) i

Tactic:
by

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 : ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p q : ℤ
hpq : p + 0 = q
⊢ G.X p = G.X q

Tactic:
by

Goal state after:
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 : ℤ
⊢ (ofHoms ψ).v p p ⋯ = ψ p

Tactic:
by

Goal state after:
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✝ : ι
h : Homotopy f g
i : ι
⊢ (f - g).f i = (((dNext i) fun i j ↦ h.hom i j) + (prevD i) fun i j ↦ h.hom i j) + Hom.f 0 i

Tactic:
by

Goal state after:
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 ℤ
⊢ (ofHoms fun p ↦ 0) = 0

Tactic:
by

Goal state after:
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✝ : ι
h : Homotopy (f - g) 0
i : ι
⊢ f.f i = (((dNext i) fun i j ↦ h.hom i j) + (prevD i) fun i j ↦ h.hom i j) + g.f i

Tactic:
by

Goal state after:
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 : ι
⊢ Function.LeftInverse (fun h ↦ { hom := fun i j ↦ h.hom i j, zero := ⋯, comm := ⋯ }) fun h ↦
    { hom := fun i j ↦ h.hom i j, zero := ⋯, comm := ⋯ }

Tactic:
by

Goal state after:
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 : ι
⊢ Function.RightInverse (fun h ↦ { hom := fun i j ↦ h.hom i j, zero := ⋯, comm := ⋯ }) fun h ↦
    { hom := fun i j ↦ h.hom i j, zero := ⋯, comm := ⋯ }

Tactic:
by

Goal state after:
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 : C ⟶ D
h : Homotopy f g
i j : ι
w : ¬c.Rel j i
⊢ (-h.hom) i j = 0

Tactic:
by

Goal state after:
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:
by

Goal state after:
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 : C ⟶ D
h : Homotopy f g
i : ι
⊢ g.f i = (dNext i) (-h.hom) + (prevD i) (-h.hom) + f.f i

Tactic:
by

Goal state after:
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:
by

Goal state after:
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 ℤ
⊢ ofHom 0 = 0

Tactic:
by

Goal state after:
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
i j : ι
hij : c.Rel i j
inst✝ : HasBinaryBiproduct (F.X j) (G.X i)
⊢ X φ i = (F.X j ⊞ G.X i)

Tactic:
by

Goal state after:
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 ℤ
φ : F ⟶ G
p : ℤ
⊢ (ofHom φ).v p p ⋯ = φ.f p

Tactic:
by

Goal state after:
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✝ : ι
e f g : C ⟶ D
h : Homotopy e f
k : Homotopy f g
i j : ι
w : ¬c.Rel j i
⊢ (h.hom + k.hom) i j = 0

Tactic:
by

Goal state after:
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 ℤ
φ : F ⟶ G
p q q' : ℤ
hpq : p + 0 = q
⊢ (ofHom φ).v p q hpq ≫ G.d q q' = φ.f p ≫ G.d p q'

Tactic:
by

Goal state after:
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✝ : ι
e f g : C ⟶ D
h : Homotopy e f
k : Homotopy f g
i : ι
⊢ e.f i = (dNext i) (h.hom + k.hom) + (prevD i) (h.hom + k.hom) + g.f i

Tactic:
by

Goal state after:
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 ℤ
φ : F ⟶ G
p' p q : ℤ
hpq : p + 0 = q
⊢ F.d p' p ≫ (ofHom φ).v p q hpq = F.d p' q ≫ φ.f q

Tactic:
by

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hG : IsZero (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero (F.X j)
⊢ IsZero (X φ i)

Tactic:
by

Goal state after:
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 ℤ
φ₁ φ₂ : F ⟶ G
⊢ ofHom (φ₁ + φ₂) = ofHom φ₁ + ofHom φ₂

Tactic:
by

Goal state after:
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 ℤ
φ₁ φ₂ : F ⟶ G
⊢ ofHom (φ₁ - φ₂) = ofHom φ₁ - ofHom φ₂

Tactic:
by

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)
x : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
this : ∑ i ∈ x.support with (algebraMap A B) i = c, x i ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
i : ↥({i ∈ x.support | (algebraMap A B) i = c})
⊢ x ↑i ≠ 0 ∧ (algebraMap A B) ↑i = c

Tactic:
by

Goal state after:
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 ℤ
φ : F ⟶ G
⊢ ofHom (-φ) = -ofHom φ

Tactic:
by

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
⊢ inrX φ i ≫ sndX φ i = 𝟙 (G.X i)

Tactic:
by

Goal state after:
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

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
⊢ sndX φ i ≫ inrX φ i = 𝟙 (X φ i)

Tactic:
by

Goal state after:
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 : ι
⊢ (f₁ + f₂).f i = (dNext i) (h₁.hom + h₂.hom) + (prevD i) (h₁.hom + h₂.hom) + (g₁ + g₂).f i

Tactic:
by

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 : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q = q'
⊢ p + n = q'

Tactic:
by

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
⊢ inlX φ i j hij ≫ fstX φ j i hij = 𝟙 (F.X i)

Tactic:
by

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
⊢ inlX φ i j hij ≫ sndX φ j = 0

Tactic:
by

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
⊢ inrX φ i ≫ fstX φ i j hij = 0

Tactic:
by

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
⊢ inlX φ i j hij ≫ (XIsoBiprod φ j i hij).hom = biprod.inl

Tactic:
by

Goal state after:
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 ℤ
n : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q = q'
⊢ γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G hq').hom = γ.v p q' ⋯

Tactic:
by

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
⊢ biprod.inl ≫ (XIsoBiprod φ j i hij).inv = inlX φ i j hij

Tactic:
by

Goal state after:
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✝ : ι
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Linear R V
h : Homotopy f g
a : R
i j : ι
hij : ¬c.Rel j i
⊢ a • h.hom i j = 0

Tactic:
by

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
⊢ inrX φ j ≫ (XIsoBiprod φ j i hij).hom = biprod.inr

Tactic:
by

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 : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q' = q
⊢ p + n = q'

Tactic:
by

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
⊢ biprod.inr ≫ (XIsoBiprod φ j i hij).inv = inrX φ j

Tactic:
by

Goal state after:
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 ℤ
n : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q' = q
⊢ γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G hq').inv = γ.v p q' ⋯

Tactic:
by

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₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ p + n₁ + n₂ = q

Tactic:
by

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)
⊢ (kerCotangentToTensor R A B).range = Submodule.restrictScalars A (mapBaseChange R A B).ker

Tactic:
by

Goal state after:
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✝ : ι
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Linear R V
h : Homotopy f g
a : R
i : ι
⊢ (a • f).f i = (((dNext i) fun i j ↦ a • h.hom i j) + (prevD i) fun i j ↦ a • h.hom i j) + (a • g).f i

Tactic:
by

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₂
h : n₁ + n₂ = n₁₂
p₁ p₂ p₃ : ℤ
h₁ : p₁ + n₁ = p₂
h₂ : p₂ + n₂ = p₃
⊢ p₁ + n₁₂ = p₃

Tactic:
by

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
⊢ f = g

Tactic:
by

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : A ⟶ X φ i
h : f ≫ sndX φ i = g ≫ sndX φ i
⊢ f = g

Tactic:
by

Goal state after:
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✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i j : ι
w : ¬c.Rel j i
⊢ h.hom i j ≫ g.f j = 0

Tactic:
by

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)
⊢ Function.Surjective ⇑(mapBaseChange R A B)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p₁ p₂ p₃ : ℤ
h₁ : p₁ + n₁ = p₂
h₂ : p₂ + n₂ = p₃
⊢ (z₁.comp z₂ h).v p₁ p₃ ⋯ = z₁.v p₁ p₂ h₁ ≫ z₂.v p₂ p₃ h₂

Tactic:
by

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₃ n₁₂ n₂₃ n₁₂₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
h₁₂ : n₁ + n₂ = n₁₂
h₂₃ : n₂ + n₃ = n₂₃
h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃
⊢ n₁ + n₂₃ = n₁₂₃

Tactic:
by

Goal state after:
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✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i : ι
⊢ (e ≫ g).f i = (((dNext i) fun i j ↦ h.hom i j ≫ g.f j) + (prevD i) fun i j ↦ h.hom i j ≫ g.f j) + (f ≫ g).f i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K L : CochainComplex C ℤ
n₁ n₂ n₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
p q : ℤ
hpq : p + (n₁ + n₂ + n₃) = q
⊢ p + n₁ + n₂ + n₃ = q

Tactic:
by

Goal state after:
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 : D ⟶ E
h : Homotopy f g
e : C ⟶ D
i j : ι
w : ¬c.Rel j i
⊢ e.f i ≫ h.hom i j = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K L : CochainComplex C ℤ
n₁ n₂ n₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
p q : ℤ
hpq : p + (n₁ + n₂ + n₃) = q
⊢ p + n₁ = p + n₁

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K L : CochainComplex C ℤ
n₁ n₂ n₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
p q : ℤ
hpq : p + (n₁ + n₂ + n₃) = q
⊢ p + n₁ + n₂ = p + n₁ + n₂

Tactic:
by

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
⊢ f = g

Tactic:
by

Goal state after: