mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x : R ⧸ I ^ 2
⊢ ∀ (y : R ⧸ I ^ 2), x ∈ ⊥ → y ∈ ⊥ → x + y ∈ ⊥

Tactic:
y

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x y : R ⧸ I ^ 2
⊢ x ∈ ⊥ → y ∈ ⊥ → x + y ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.cotangentToQuotientSquare.range = (I.cotangentToQuotientSquare ∘ₗ I.toCotangent).range

Tactic:
rw [LinearMap.range_comp, I.toCotangent_range, Submodule.map_top]

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
⊢ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ i_1, ⋃ (_ : i_1 ≤ i), single R i_1 '' ↑(F.N i_1)) = F.submodule

Tactic:
← submodule_span_single

Goal state after:
case mp.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
⊢ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ i_1, ⋃ (_ : i_1 ≤ i), single R i_1 '' ↑(F.N i_1)) =
    Submodule.span (↥(reesAlgebra I)) (⋃ i, single R i '' ↑(F.N i))
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case a
R : Type u
inst✝⁴ : CommRing R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ (RingHom.ker f.toRingHom).cotangentIdeal ≤ RingHom.ker f.kerSquareLift.toRingHom

Tactic:
· rintro _ ⟨x, hx, rfl⟩; exact hx

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
x' : ↥I
y' : A
mem : y' ∈ J
hy' : (algebraMap A B) y' = ↑x'
⊢ ∃ a, (J.mapCotangent I (Algebra.ofId A B) ⋯) a = I.toCotangent x'

Tactic:
use J.toCotangent ⟨y', mem⟩

Goal state after:
case h
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
x' : ↥I
y' : A
mem : y' ∈ J
hy' : (algebraMap A B) y' = ↑x'
⊢ (J.mapCotangent I (Algebra.ofId A B) ⋯) (J.toCotangent ⟨y', mem⟩) = I.toCotangent x'
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
i j : ι
rij : c.Rel i j
k : ι
rik : c.Rel i k
⊢ ⟨j, rij⟩ = ⟨k, rik⟩

Tactic:
congr

Goal state after:
ι : Type u_1
c : ComplexShape ι
i j : ι
rij : c.Rel i j
k : ι
rik : c.Rel i k
⊢ j = k
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
X : Cᵒᵖ
hX : Limits.IsInitial X
M : PresheafOfModules R
Y Z : Cᵒᵖ
f : Y ⟶ Z
r : ↑(R.obj X)
x : ↑(forgetToPresheafModuleCatObjObj X hX M Y)
⊢ (ConcreteCategory.hom (R.map (hX.to Y ≫ f))) r • (ConcreteCategory.hom (M.map f)) x =
    (RingCat.Hom.hom (R.map (hX.to Z))) r • (ConcreteCategory.hom (M.map f)) x

Tactic:
congr

Goal state after:
case e_a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
X : Cᵒᵖ
hX : Limits.IsInitial X
M : PresheafOfModules R
Y Z : Cᵒᵖ
f : Y ⟶ Z
r : ↑(R.obj X)
x : ↑(forgetToPresheafModuleCatObjObj X hX M Y)
⊢ hX.to Y ≫ f = hX.to Z
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst✝² : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
i : I
c : (j : J) → q j = q (p i) → X.CofanMapObjFun p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan fun j ↦ (c ↑j ⋯).pt
hc' : IsColimit c'
s : Cofan (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : ↑(r ⁻¹' {q (p i)})), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
⊢ Cofan.inj (c (p i) ⋯) ⟨i, ⋯⟩ ≫ c'.inj ⟨p i, ⋯⟩ ≫ m =
    Cofan.inj (c (p i) ⋯) ⟨i, ⋯⟩ ≫
      c'.inj ⟨p i, ⋯⟩ ≫ Cofan.IsColimit.desc hc' fun x ↦ Cofan.IsColimit.desc (hc ↑x ⋯) fun x_1 ↦ s.inj ⟨↑x_1, ⋯⟩

Tactic:
Cofan.IsColimit.fac,

Goal state after:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst✝² : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
i : I
c : (j : J) → q j = q (p i) → X.CofanMapObjFun p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan fun j ↦ (c ↑j ⋯).pt
hc' : IsColimit c'
s : Cofan (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : ↑(r ⁻¹' {q (p i)})), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
⊢ Cofan.inj (c (p i) ⋯) ⟨i, ⋯⟩ ≫ c'.inj ⟨p i, ⋯⟩ ≫ m =
    Cofan.inj (c (p i) ⋯) ⟨i, ⋯⟩ ≫ Cofan.IsColimit.desc (hc ↑⟨p i, ⋯⟩ ⋯) fun x ↦ s.inj ⟨↑x, ⋯⟩
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst✝² : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
i : I
c : (j : J) → q j = q (p i) → X.CofanMapObjFun p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan fun j ↦ (c ↑j ⋯).pt
hc' : IsColimit c'
s : Cofan (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : ↑(r ⁻¹' {q (p i)})), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
⊢ Cofan.inj (c (p i) ⋯) ⟨i, ⋯⟩ ≫ c'.inj ⟨p i, ⋯⟩ ≫ m =
    Cofan.inj (c (p i) ⋯) ⟨i, ⋯⟩ ≫ Cofan.IsColimit.desc (hc ↑⟨p i, ⋯⟩ ⋯) fun x ↦ s.inj ⟨↑x, ⋯⟩

Tactic:
Cofan.IsColimit.fac,

Goal state after:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst✝² : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
i : I
c : (j : J) → q j = q (p i) → X.CofanMapObjFun p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan fun j ↦ (c ↑j ⋯).pt
hc' : IsColimit c'
s : Cofan (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : ↑(r ⁻¹' {q (p i)})), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
⊢ Cofan.inj (c (p i) ⋯) ⟨i, ⋯⟩ ≫ c'.inj ⟨p i, ⋯⟩ ≫ m = s.inj ⟨↑⟨i, ⋯⟩, ⋯⟩
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_2.refine_2
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
D : Derivation R S M
x✝ y : S ⊗[R] S
x₁ x₂ x : S
⊢ ∀ (y : S),
    D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x ⊗ₜ[R] y) =
      (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x ⊗ₜ[R] y) +
        (TensorProduct.lmul' R) (x ⊗ₜ[R] y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

Tactic:
y

Goal state after:
case refine_2.refine_2
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
D : Derivation R S M
x✝ y✝ : S ⊗[R] S
x₁ x₂ x y : S
⊢ D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x ⊗ₜ[R] y) =
    (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x ⊗ₜ[R] y) +
      (TensorProduct.lmul' R) (x ⊗ₜ[R] y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
i : ι
h : ¬i = j
⊢ f.f i = g.f i

Tactic:
· apply (isZero_single_obj_X c j A i h).eq_of_tgt

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

Goal state before:
pp: case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x : S
⊢ ∀ (y : S),
    x ⊗ₜ[R] y - (TensorProduct.lmul' R) (x ⊗ₜ[R] y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
y

Goal state after:
case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
⊢ x ⊗ₜ[R] y - (TensorProduct.lmul' R) (x ⊗ₜ[R] y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
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
i j : A
⊢ shiftFunctorAdd' C i j (i + j) ⋯ = shiftFunctorAdd C i j

Tactic:
by
  ext1
  apply Category.id_comp

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

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
i k : ι
hik : c.Rel i k
⊢ (if hi : i = j then (singleObjXIsoOfEq c j A i hi).hom ≫ φ ≫ (K.XIsoOfEq hi).inv else 0) ≫ K.d i k = 0

Tactic:
split_ifs with hi

Goal state after:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
i k : ι
hik : c.Rel i k
hi : i = j
⊢ ((singleObjXIsoOfEq c j A i hi).hom ≫ φ ≫ (K.XIsoOfEq hi).inv) ≫ K.d i k = 0

case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
i k : ι
hik : c.Rel i k
hi : ¬i = j
⊢ 0 ≫ K.d i k = 0
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a.refine_3
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ x : S ⊗[R] S
⊢ ∀ (y : S ⊗[R] S),
    x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
      y - (TensorProduct.lmul' R) y ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
        x + y - (TensorProduct.lmul' R) (x + y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
y

Goal state after:
case a.refine_3
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ x y : S ⊗[R] S
⊢ x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
    y - (TensorProduct.lmul' R) y ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
      x + y - (TensorProduct.lmul' R) (x + y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
⊢ Submodule.Quotient.mk ⟨1 ⊗ₜ[R] 1 - 1 ⊗ₜ[R] 1, ⋯⟩ = 0

Tactic:
congr

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
⊢ 1 ⊗ₜ[R] 1 - 1 ⊗ₜ[R] 1 = 0
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : IsIso f
j : ι
⊢ (inv f).f j = inv (f.f j)

Tactic:
apply IsIso.eq_inv_of_inv_hom_id

Goal state after:
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : IsIso f
j : ι
⊢ (inv f).f j ≫ f.f j = 𝟙 (C₂.X j)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_2.refine_2
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
D : Derivation R S M
x✝ : ↥(KaehlerDifferential.ideal R S)
hx : x✝ ∈ Submodule.restrictScalars S (KaehlerDifferential.ideal R S • ⊤)
x : ↥(KaehlerDifferential.ideal R S)
⊢ ∀ (y : ↥(KaehlerDifferential.ideal R S)),
    (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) x = 0 →
      (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) y = 0 →
        (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) (x + y) = 0

Tactic:
y

Goal state after:
case refine_2.refine_2
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
D : Derivation R S M
x✝ : ↥(KaehlerDifferential.ideal R S)
hx : x✝ ∈ Submodule.restrictScalars S (KaehlerDifferential.ideal R S • ⊤)
x y : ↥(KaehlerDifferential.ideal R S)
⊢ (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) x = 0 →
    (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) y = 0 →
      (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) (x + y) = 0
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 : Ω[S⁄R]
⊢ ∀ (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:
y

Goal state after:
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)
Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian

Goal state before:
pp: C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : ∀ (i : ι), (S.map (eval C c i)).Exact
⊢ S.Exact

Tactic:
simp only [ShortComplex.exact_iff_isZero_homology] at hS ⊢

Goal state after:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : ∀ (i : ι), IsZero (S.map (eval C c i)).homology
⊢ IsZero S.homology
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_4
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
inst✝ : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun s ↦ (D R S) s) (EssFiniteType.finset R S)
x✝¹ x✝ : S
hx : x✝ ∈ adjoin R ↑(EssFiniteType.finset R S)
x : S
⊢ ∀ (y : S),
    x ∈ adjoin R ↑(EssFiniteType.finset R S) →
      y ∈ adjoin R ↑(EssFiniteType.finset R S) →
        (D R S) x ∈ Submodule.span S ↑s → (D R S) y ∈ Submodule.span S ↑s → (D R S) (x * y) ∈ Submodule.span S ↑s

Tactic:
y

Goal state after:
case refine_4
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
inst✝ : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun s ↦ (D R S) s) (EssFiniteType.finset R S)
x✝¹ x✝ : S
hx : x✝ ∈ adjoin R ↑(EssFiniteType.finset R S)
x y : S
⊢ x ∈ adjoin R ↑(EssFiniteType.finset R S) →
    y ∈ adjoin R ↑(EssFiniteType.finset R S) →
      (D R S) x ∈ Submodule.span S ↑s → (D R S) y ∈ Submodule.span S ↑s → (D R S) (x * y) ∈ Submodule.span S ↑s
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:
congr

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
h : Function.Surjective ⇑(algebraMap A B)
⊢ (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ∘ fun x ↦
      single ((algebraMap R A) x) 1) =
    fun x ↦ single ((algebraMap R B) x) 1
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case mp
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 : (RingHom.ker (algebraMap A B)).Cotangent
⊢ (kerCotangentToTensor R A B) x ∈ Submodule.restrictScalars A (mapBaseChange R A B).ker

Tactic:
obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x

Goal state after:
case mp
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 : ↥(RingHom.ker (algebraMap A B))
⊢ (kerCotangentToTensor R A B) ((RingHom.ker (algebraMap A B)).toCotangent x) ∈
    Submodule.restrictScalars A (mapBaseChange R A B).ker
Module: Mathlib.Algebra.Homology.Homotopy

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

Tactic:
congr

Goal state after:
case succ.e_4.e_a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.down ℕ).next (n✝ + 1) = n✝ + 1 - 1

case succ.e_6.e_8
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.down ℕ).next (n✝ + 1) = n✝ + 1 - 1

case succ.e_7.e_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.down ℕ).next (n✝ + 1) = n✝ + 1 - 1
Module: Mathlib.Algebra.Homology.Homotopy

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

Tactic:
congr

Goal state after:
case succ.e_4.e_a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.up ℕ).prev (n✝ + 1) = n✝ + 1 - 1

case succ.e_6.e_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.up ℕ).prev (n✝ + 1) = n✝ + 1 - 1

case succ.e_7.e_7
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.up ℕ).prev (n✝ + 1) = n✝ + 1 - 1
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 : ι
⊢ ((if hi : c.Rel i (c.next i) then biprod.inr ≫ (XIsoBiprod φ i (c.next i) hi).inv else (XIso φ i hi).inv) ≫
      if hi : c.Rel i (c.next i) then (XIsoBiprod φ i (c.next i) hi).hom ≫ biprod.snd else (XIso φ i hi).hom) =
    𝟙 (G.X i)

Tactic:
split_ifs with hi

Goal state after:
case pos
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)
⊢ (biprod.inr ≫ (XIsoBiprod φ i (c.next i) hi).inv) ≫ (XIsoBiprod φ i (c.next i) hi).hom ≫ biprod.snd = 𝟙 (G.X i)

case neg
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)
⊢ (XIso φ i hi).inv ≫ (XIso φ i hi).hom = 𝟙 (G.X i)
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 : ι
⊢ e.f i ≫ ((dNext i) h.hom + (prevD i) h.hom + g.f i) =
    (((dNext i) fun i j ↦ e.f i ≫ h.hom i j) + (prevD i) fun i j ↦ e.f i ≫ h.hom i j) + (e ≫ g).f i

Tactic:
dNext_comp_left,

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 : D ⟶ E
h : Homotopy f g
e : C ⟶ D
i : ι
⊢ e.f i ≫ ((dNext i) h.hom + (prevD i) h.hom + g.f i) =
    (e.f i ≫ (dNext i) h.hom + (prevD i) fun i j ↦ e.f i ≫ h.hom i j) + (e ≫ g).f i
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
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
⊢ (nullHomotopicMap fun i j ↦ (dite (c.Rel j i) (hom i j) fun x ↦ 0) ≫ g.f j) =
    nullHomotopicMap' fun i j hij ↦ hom i j hij ≫ g.f j

Tactic:
congr

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
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
⊢ (fun i j ↦ (dite (c.Rel j i) (hom i j) fun x ↦ 0) ≫ g.f j) = fun i j ↦
    dite (c.Rel j i) ((fun i j hij ↦ hom i j hij ≫ g.f j) i j) fun x ↦ 0