mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

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
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ + ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ + (shortComplexFunctor C c i).map ψ)

Tactic:
]

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
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ + ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ + (shortComplexFunctor C c i).map ψ)
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)
⊢ Submodule.span A (Set.range (⇑(linearCombination A ⇑(D R A)) ∘ fun x ↦ single ((algebraMap R A) x) 1)) ⊔
      Submodule.map (linearCombination A ⇑(D R A))
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker =
    Submodule.map (linearCombination A ⇑(D R A))
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker

Tactic:
]

Goal state after:
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)) ⊔
      Submodule.map (linearCombination A ⇑(D R A))
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker =
    Submodule.map (linearCombination A ⇑(D R A))
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
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)
⊢ ∀ x ∈ Set.range (⇑(linearCombination A ⇑(D R A)) ∘ fun x ↦ single ((algebraMap R A) x) 1), x = 0

Tactic:
]

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.Algebra.Homology.ShortComplex.HomologicalComplex

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
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ - ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ - (shortComplexFunctor C c i).map ψ)

Tactic:
]

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
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ - ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ - (shortComplexFunctor C c i).map ψ)
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
h : Function.Surjective ⇑(algebraMap A B)
⊢ Set.range ⇑(D S B) ⊆ ↑(map R S A B).range

Tactic:
]

Goal state after:
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
h : Function.Surjective ⇑(algebraMap A B)
⊢ Set.range ⇑(D S B) ⊆ ↑(map R S A B).range
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
h : Function.Surjective ⇑(algebraMap A B)
y : A
⊢ (map R S A B) ((D R A) y) ∈ ↑(map R S A B).range

Tactic:
]

Goal state after:
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
h : Function.Surjective ⇑(algebraMap A B)
y : A
⊢ (map R S A B) ((D R A) y) ∈ ↑(map R S A B).range
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)
i : ι
⊢ 𝟙 (K.X i) = 𝟙 (K.X i)

Tactic:
]

Goal state after:
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)
i : ι
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case a.add
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✝ y✝ : B ⊗[A] Ω[A⁄R]
a✝¹ : (mapBaseChange R A B) x✝ ∈ (map R A B B).ker
a✝ : (mapBaseChange R A B) y✝ ∈ (map R A B B).ker
⊢ (mapBaseChange R A B) x✝ + (mapBaseChange R A B) y✝ ∈ (map R A B B).ker

Tactic:
]

Goal state after:
case a.add
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✝ y✝ : B ⊗[A] Ω[A⁄R]
a✝¹ : (mapBaseChange R A B) x✝ ∈ (map R A B B).ker
a✝ : (mapBaseChange R A B) y✝ ∈ (map R A B B).ker
⊢ (mapBaseChange R A B) x✝ + (mapBaseChange R A B) y✝ ∈ (map R A B B).ker
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)
i : ι
⊢ 𝟙 (L.X i) = 𝟙 (L.X i)

Tactic:
]

Goal state after:
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
⊢ 𝟙 ((K ⊞ L).X i) ≫ f = 𝟙 ((K ⊞ L).X i) ≫ g

Tactic:
]

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:
]

Goal state after:
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)
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 : A ⟶ (K ⊞ L).X i
x✝ : f ≫ biprod.fst.f i = g ≫ biprod.fst.f i ∧ f ≫ biprod.snd.f i = g ≫ biprod.snd.f i
h₁ : f ≫ biprod.fst.f i = g ≫ biprod.fst.f i
h₂ : f ≫ biprod.snd.f i = g ≫ biprod.snd.f i
⊢ f ≫ 𝟙 ((K ⊞ L).X i) = g ≫ 𝟙 ((K ⊞ L).X i)

Tactic:
]

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 : A ⟶ (K ⊞ L).X i
x✝ : f ≫ biprod.fst.f i = g ≫ biprod.fst.f i ∧ f ≫ biprod.snd.f i = g ≫ biprod.snd.f i
h₁ : f ≫ biprod.fst.f i = g ≫ biprod.fst.f i
h₂ : f ≫ biprod.snd.f i = g ≫ biprod.snd.f i
⊢ f ≫ 𝟙 ((K ⊞ L).X i) = g ≫ 𝟙 ((K ⊞ L).X i)
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)
M : HomologicalComplex C c
α : K ⟶ M
β : L ⟶ M
i : ι
⊢ α.f i = α.f i

Tactic:
]

Goal state after:
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)
M : HomologicalComplex C c
α : K ⟶ M
β : L ⟶ M
i : ι
⊢ β.f i = β.f i

Tactic:
]

Goal state after:
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)
M : HomologicalComplex C c
α : M ⟶ K
β : M ⟶ L
i : ι
⊢ α.f i = α.f i

Tactic:
]

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

Goal state before:
pp: case a.convert_2
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
⊢ (((Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
        Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
      Set.range fun x ↦ single ((algebraMap A B) x) 1) ⊆
    ↑(Submodule.comap (linearCombination B ⇑(D R B)) (mapBaseChange R A B).range)

Tactic:
]

Goal state after:
case a.convert_2
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
⊢ (((Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
        Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
      Set.range fun x ↦ single ((algebraMap A B) x) 1) ⊆
    ↑(Submodule.comap (linearCombination B ⇑(D R B)) (mapBaseChange R A B).range)
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)
M : HomologicalComplex C c
α : M ⟶ K
β : M ⟶ L
i : ι
⊢ β.f i = β.f i

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E₁ : Type u_3
E₂ : Type u_4
inst✝¹ : Category.{v_3, u_3} E₁
inst✝ : Category.{v_4, u_4} E₂
F₁ : C₁ ⥤ E₁
F₂ : C₂ ⥤ E₂
h₁ : W₁.IsInvertedBy F₁
h₂ : W₂.IsInvertedBy F₂
x✝¹ x✝ : C₁ × C₂
f : x✝¹ ⟶ x✝
hf : W₁.prod W₂ f
⊢ IsIso ((F₁.prod F₂).map f).1 ∧ IsIso ((F₁.prod F₂).map f).2

Tactic:
]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E₁ : Type u_3
E₂ : Type u_4
inst✝¹ : Category.{v_3, u_3} E₁
inst✝ : Category.{v_4, u_4} E₂
F₁ : C₁ ⥤ E₁
F₂ : C₂ ⥤ E₂
h₁ : W₁.IsInvertedBy F₁
h₂ : W₂.IsInvertedBy F₂
x✝¹ x✝ : C₁ × C₂
f : x✝¹ ⟶ x✝
hf : W₁.prod W₂ f
⊢ IsIso ((F₁.prod F₂).map f).1 ∧ IsIso ((F₁.prod F₂).map f).2
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ Y✝ : (j : J) → C j
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi W f
⊢ ∀ (i : J), IsIso ((Functor.pi F).map f i)

Tactic:
]

Goal state after:
J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ Y✝ : (j : J) → C j
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi W f
⊢ ∀ (i : J), IsIso ((Functor.pi F).map f i)
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.isoClosure.IsInvertedBy F → W.IsInvertedBy F

Tactic:
intro h X Y f hf
    exact h _ (W.le_isoClosure _ hf)

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W ≤ (isomorphisms D).inverseImage F ↔ W ≤ (isomorphisms D).inverseImage F

Tactic:
]

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
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
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
⊢ Submodule.map₂ (LinearMap.lsmul A ↥(RingHom.ker (algebraMap A B))) (RingHom.ker (algebraMap A B)) ⊤ ≤
    (kerToTensor R A B).ker

Tactic:
]

Goal state after:
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
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
⊢ Submodule.map₂ (LinearMap.lsmul A ↥(RingHom.ker (algebraMap A B))) (RingHom.ker (algebraMap A B)) ⊤ ≤
    (kerToTensor R A B).ker
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 ∈
    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

Tactic:
]

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 : ι
hi : ¬c.Rel i (c.next i)
⊢ 0 = 0

Tactic:
]

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

Tactic:
]

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.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
⊢ 0 = 0

Tactic:
]

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 p

Tactic:
]

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
hpq : p = q
⊢ (ofHoms ψ).v p q hpq✝ ≫ G.d q q' = ψ p ≫ G.d p q'

Tactic:
]

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.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
⊢ 0 = 0

Tactic:
]

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' : ℤ
hpq : p + 0 = p
⊢ ψ p ≫ G.d p q' = ψ p ≫ G.d p q'

Tactic:
]

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
hpq : p = q
⊢ F.d p' p ≫ (ofHoms ψ).v p q hpq✝ = F.d p' q ≫ ψ q

Tactic:
]

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 : C ⟶ D
h : Homotopy f g
i : ι
⊢ g.f i = g.f i

Tactic:
]

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 : ℤ
hpq : p + 0 = p
⊢ F.d p' p ≫ ψ p = F.d p' p ≫ ψ p

Tactic:
]

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
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case h
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
⊢ 0 = 0

Tactic:
]

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
⊢ 0 = 0

Tactic:
]

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'
⊢ q = q

Tactic:
]

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
⊢ 0 = 0

Tactic:
]

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
⊢ q = q

Tactic:
]

Goal state after: