mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Kaehler.Basic

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

Tactic:
map_add,

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

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

Tactic:
map_add,

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

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

Tactic:
map_add,

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ eqToHom ⋯

Tactic:
eqToHom_trans,

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ 𝟙 ((h.F (n + 0)).obj X) = eqToHom ⋯ ≫ eqToHom ⋯

Tactic:
eqToHom_trans,

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ 𝟙 ((h.F (n + 0)).obj X) = eqToHom ⋯
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 y : S ⊗[R] S
hx : x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
hy : 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:
map_add,

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
hx : x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
hy : 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 + (TensorProduct.lmul' R) y) ⊗ₜ[R] 1 ∈
    Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
j : α
⊢ (if j + 1 = j + 1 then 𝟙 (X (j + 1)) ≫ d j else 0) = d j

Tactic:
if_pos rfl,

Goal state after:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
j : α
⊢ 𝟙 (X (j + 1)) ≫ d j = d j
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ (if 1 = 0 + 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀

Tactic:
if_pos rfl,

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ 𝟙 X₁ ≫ d₀ = d₀
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ (if 2 = 1 + 1 then 𝟙 X₂ ≫ d₁ else 0) = d₁

Tactic:
if_pos rfl,

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ 𝟙 X₂ ≫ d₁ = d₁
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_2.refine_1
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 : S ⊗[R] S
hx : x ∈ KaehlerDifferential.ideal R S
y : ↥(KaehlerDifferential.ideal R S)
⊢ (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) (x • y) = 0

Tactic:
RingHom.mem_ker

Goal state after:
case refine_2.refine_1
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 : S ⊗[R] S
hx : (TensorProduct.lmul' R) x = 0
y : ↥(KaehlerDifferential.ideal R S)
⊢ (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) (x • y) = 0
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 y : ↥(KaehlerDifferential.ideal R S)
ex : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) x = 0
ey : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) y = 0
⊢ (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) (x + y) = 0

Tactic:
map_add,

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)
ex : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) x = 0
ey : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) y = 0
⊢ (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) x +
      (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) y =
    0
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ (if 1 = 0 + 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀

Tactic:
if_pos rfl,

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ 𝟙 X₁ ≫ d₀ = d₀
Module: Mathlib.RingTheory.Kaehler.Basic

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

Tactic:
map_add,

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]
hx✝ : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
hy✝ : y ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
hx : f x = f' x
hy : f y = f' y
⊢ f x + f y = f' (x + y)
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
j : α
⊢ (if j + 1 = j + 1 then d j ≫ 𝟙 (X (j + 1)) else 0) = d j

Tactic:
if_pos rfl,

Goal state after:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
j : α
⊢ d j ≫ 𝟙 (X (j + 1)) = d j
Module: Mathlib.RingTheory.Kaehler.Basic

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

Tactic:
map_add,

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]
hx✝ : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
hy✝ : y ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
hx : f x = f' x
hy : f y = f' y
⊢ f x + f y = f' x + f' y
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (if 1 = 0 + 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀

Tactic:
if_pos rfl,

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ d₀ ≫ 𝟙 X₁ = d₀
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (if 2 = 1 + 1 then d₁ ≫ 𝟙 X₂ else 0) = d₁

Tactic:
if_pos rfl,

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ d₁ ≫ 𝟙 X₂ = d₁
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₀ ⟶ X₁
succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0
⊢ (if 1 = 0 + 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀

Tactic:
if_pos rfl,

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₀ ⟶ X₁
succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0
⊢ d₀ ≫ 𝟙 X₁ = d₀
Module: Mathlib.CategoryTheory.Shift.Basic

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

Tactic:
by
        have := dcongr_arg (fun a => (i a).hom.app X) (zero_add n)
        rw [← cancel_mono ((i n).hom.app ((s 0).obj X))]
        simp only [comp_obj, map_add_hom_app, this, shiftFunctorAdd_zero_add_hom_app, id_obj,
          Category.assoc, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp, Iso.inv_hom_id_app,
          Category.comp_id, map_comp, eqToHom_map]
        congr 1
        erw [(i n).hom.naturality]
        simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.restrictScalars A (Submodule.span B (Set.range ⇑(D S B))) ≤ (map R S A B).range

Tactic:
Submodule.restrictScalars_span _ _ h,

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)
⊢ Submodule.span A (Set.range ⇑(D S B)) ≤ (map R S 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
⊢ (prevD i) f = 0

Tactic:
dsimp [prevD]

Goal state after:
ι : 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
⊢ f i (c.prev i) ≫ D.d (c.prev i) i = 0
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : (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:
dsimp [prevD]

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 : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
j : ι
⊢ (f j (c.prev j) ≫ g.f (c.prev j)) ≫ E.d (c.prev j) j = (f j (c.prev j) ≫ D.d (c.prev j) j) ≫ g.f j
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:
dsimp [prevD]

Goal state after:
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
⊢ f i ((ComplexShape.up ℕ).prev i) ≫ D.d ((ComplexShape.up ℕ).prev i) i = f i (i - 1) ≫ D.d (i - 1) i
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
j : ι
hij : c.Rel j (c.next j)
this : HasBinaryBiproduct (F.X (c.next j)) (G.X j)
⊢ inrX φ j ≫ (XIsoBiprod φ j (c.next j) hij).hom = biprod.inr

Tactic:
simp [inrX, XIsoBiprod, dif_pos hij]

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

Tactic:
rw [nullHomotopicMap', comp_nullHomotopicMap]
  congr
  ext i j
  split_ifs
  · rfl
  · rw [comp_zero]

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

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

Tactic:
dsimp [prevD]

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ f j ((ComplexShape.down ℕ).prev j) ≫ Q.d ((ComplexShape.down ℕ).prev j) j = f j (j + 1) ≫ Q.d (j + 1) j
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
hc : ∀ (j : ι), ∃ i, c.Rel i j
i j : ι
hij : ¬c.Rel j i
⊢ (inrCompHomotopy φ hc).hom i j ≫ (desc φ α hα).f j = hα.hom i j

Tactic:
simp only [Homotopy.zero _ _ _ hij, zero_comp]

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

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

Tactic:
dsimp [prevD]

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
⊢ f (i + 1) ((ComplexShape.up ℕ).prev (i + 1)) ≫ Q.d ((ComplexShape.up ℕ).prev (i + 1)) (i + 1) =
    f (i + 1) i ≫ Q.d i (i + 1)
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ (prevD 0) f = 0

Tactic:
dsimp [prevD]

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ f 0 ((ComplexShape.up ℕ).prev 0) ≫ Q.d ((ComplexShape.up ℕ).prev 0) 0 = 0
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 : ℤ
z₁ : Cocycle F G 0
z₂ : Cochain G K n
m : ℤ
⊢ δ n m ((↑z₁).comp z₂ ⋯) = (↑z₁).comp (δ n m z₂) ⋯

Tactic:
by_cases hnm : n + 1 = m
  · simp [δ_zero_cochain_comp _ _ _ hnm]
  · simp [δ_shape _ _ hnm]

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
r : HomRel C
inst✝¹ : IsStableUnderPrecomp r
inst✝ : IsStableUnderPostcomp r
X Y : C
f g : X ⟶ Y
⊢ CompClosure r f g → r f g

Tactic:
rintro ⟨_, _, _, _, _, _, h⟩

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
r : HomRel C
inst✝¹ : IsStableUnderPrecomp r
inst✝ : IsStableUnderPostcomp r
X✝ Y✝ X Y a✝ b✝ : C
m₁✝ m₂✝ : a✝ ⟶ b✝
h : r m₁✝ m₂✝
f✝ : X✝ ⟶ a✝
g✝ : b✝ ⟶ Y✝
⊢ r (f✝ ≫ m₁✝ ≫ g✝) (f✝ ≫ m₂✝ ≫ g✝)