mathlib-initiative/mathlib-tactics huggingface dataset:
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 : R
y : S
⊢ y • single ((algebraMap R S) x) 1 ∈ kerTotal R S

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
y : S
⊢ y • single ((algebraMap R S) x) 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 : S
⊢ 0 = 0

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
r : R
x y : S
this : SMulZeroClass R S := inferInstance
⊢ (((algebraMap R S) r * y)𝖣x) = ((algebraMap R S) r * y)𝖣x

Tactic:
]

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

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (linearCombination S ⇑(D R S)).ker ≤
    ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)).ker

Tactic:
]

Goal state after:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (linearCombination S ⇑(D R S)).ker ≤
    ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)).ker
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (((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 R S) x) 1) ⊆
    ↑(linearCombination S ⇑(D R S)).ker

Tactic:
]

Goal state after:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (((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 R S) x) 1) ⊆
    ↑(linearCombination S ⇑(D R S)).ker
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
⊢ ⊤ = ⊤

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
x : S →₀ S
this : (derivationQuotKerTotal R S).liftKaehlerDifferential ((linearCombination S ⇑(D R S)) x) = (kerTotal R S).mkQ x
⊢ ((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun
      ((derivationQuotKerTotal R S).liftKaehlerDifferential ((linearCombination S ⇑(D R S)) x)) =
    (linearCombination S ⇑(D R S)) x

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
x : S →₀ S
this : (derivationQuotKerTotal R S).liftKaehlerDifferential ((linearCombination S ⇑(D R S)) x) = (kerTotal R S).mkQ x
⊢ ((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun
      ((derivationQuotKerTotal R S).liftKaehlerDifferential ((linearCombination S ⇑(D R S)) x)) =
    (linearCombination S ⇑(D R S)) 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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x : S →₀ S
this : (derivationQuotKerTotal R S).liftKaehlerDifferential ((linearCombination S ⇑(D R S)) x) = (kerTotal R S).mkQ x
⊢ ((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun ((kerTotal R S).mkQ x) =
    (linearCombination S ⇑(D R S)) x

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
x : S →₀ S
this : (derivationQuotKerTotal R S).liftKaehlerDifferential ((linearCombination S ⇑(D R S)) x) = (kerTotal R S).mkQ x
⊢ ((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun ((kerTotal R S).mkQ x) =
    (linearCombination S ⇑(D R S)) x
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology i
hij : ¬c.Rel i j
⊢ 0 = 0

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
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
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A
        (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap 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 R A) x) 1)) ⊔
      Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1) =
    Submodule.span A
      (((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 S B) x) 1)

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
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A
        (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap 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 R A) x) 1)) ⊔
      Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1) =
    Submodule.span A
      (((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 S B) x) 1)
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology j
hij : ¬c.Rel i j
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A' A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
α : A' ⟶ A
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
⊢ k ≫ K.d i j = 0

Tactic:
by rw [hx, assoc, K.d_comp_d, comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
⊢ k ≫ K.d i j = 0

Tactic:
by rw [hx, assoc, K.d_comp_d, comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx✝ : k = x ≫ K.d i' i
hx : k = 0
h : ¬c.Rel i' i
⊢ K.liftCycles k j hj ⋯ = 0

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx✝ : k = x ≫ K.d i' i
hx : k = 0
h : ¬c.Rel i' i
⊢ K.liftCycles k j hj ⋯ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx✝ : k = x ≫ K.d i' i
hx : k = 0
h : ¬c.Rel i' i
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
this : K.liftCycles k j hj ⋯ = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology j
hij : ¬c.Rel i j
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology i
hij : ¬c.Rel i j
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A A' : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
hk : K.d j i ≫ k = 0
α : A ⟶ A'
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx✝ : k = K.d i i' ≫ x
hx : k = 0
h : ¬c.Rel i i'
⊢ K.descOpcycles k j hj ⋯ = 0

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx✝ : k = K.d i i' ≫ x
hx : k = 0
h : ¬c.Rel i i'
⊢ K.descOpcycles k j hj ⋯ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx✝ : k = K.d i i' ≫ x
hx : k = 0
h : ¬c.Rel i i'
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
this : K.descOpcycles k j hj ⋯ = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.homologyMap ((shortComplexFunctor C c i).map ψ) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.homologyMap ((shortComplexFunctor C c i).map ψ)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ ShortComplex.cyclesMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.cyclesMap ((shortComplexFunctor C c i).map ψ) =
    ShortComplex.cyclesMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.cyclesMap ((shortComplexFunctor C c i).map ψ)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map ψ) =
    ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map ψ)

Tactic:
]

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

Goal state before:
pp: case e'_4.e'_4
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
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A (Set.range fun x ↦ single ((algebraMap A B) ((algebraMap R A) x)) 1) ≤
    Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1)

Tactic:
]

Goal state after:
case e'_4.e'_4
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
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A (Set.range fun x ↦ single ((algebraMap A B) ((algebraMap R A) x)) 1) ≤
    Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1)
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ✝ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
A : C
k : L.X i ⟶ A
j : ι
hj : c.prev i = j
hk : L.d j i ≫ k = 0
φ : K ⟶ L
⊢ 0 = 0

Tactic:
]

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)
⊢ Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (kerTotal R A) ⊔
      Submodule.span A
        (Set.range
          (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ∘ fun x ↦
            single ((algebraMap R A) x) 1)) =
    Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (kerTotal R A) ⊔
      Submodule.span A (Set.range fun x ↦ single ((algebraMap R B) x) 1)

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.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (kerTotal R A) ⊔
      Submodule.span A
        (Set.range
          (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ∘ fun x ↦
            single ((algebraMap R A) x) 1)) =
    Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (kerTotal R A) ⊔
      Submodule.span A (Set.range fun x ↦ single ((algebraMap R B) x) 1)
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:
]

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
⊢ 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)))
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ✝ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
φ : K ⟶ L
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
hK : (K.sc i).Exact
L : HomologicalComplex C c
e : K ≅ L
⊢ (L.sc i).Exact

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
hK : (K.sc i).Exact
L : HomologicalComplex C c
e : K ≅ L
⊢ (L.sc i).Exact
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
⊢ IsZero (K.sc i).homology ↔ IsZero (K.sc i).homology

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
h : K.ExactAt i
⊢ K.ExactAt i

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
h : K.ExactAt i
⊢ K.ExactAt i
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
hK : IsZero K
⊢ ∀ (i : ι), K.ExactAt i

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
hK : IsZero K
⊢ ∀ (i : ι), K.ExactAt i
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 φ)

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 φ)