mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
x✝² : x ∈ ↑(torsion R M)
a : ↥R⁰
hax : a • x = 0
x✝¹ : M
x✝ : ∃ a, a • x = x✝¹
b : R
hb : b • x = x✝¹
⊢ ↑a • x✝¹ = 0

Tactic:
rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero]

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: 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
i j : ℕ
⊢ I ^ i • F.N j ≤ F.N (i + j)

Tactic:
by
  induction i with
  | zero => simp
  | succ _ ih =>
    rw [pow_succ', mul_smul, add_assoc, add_comm 1, ← add_assoc]
    exact (smul_mono_right _ ih).trans (F.smul_le _)

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case mp
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c * b = x
⊢ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x

Tactic:
use c

Goal state after:
case h
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c * b = x
⊢ c • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
⊢ ∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n

Tactic:
obtain ⟨n₁, h₁⟩ := h.exists_forall_le (le_of_eq e)

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
n₁ : ℕ
h₁ : ∀ (n : ℕ), F.N (n + n₁) ≤ F'.N n
⊢ ∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : ↑B
algInst✝⁴ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝³ : Algebra ↑A' ↑B' := (Hom.hom f').toAlgebra
algInst✝² : Algebra ↑A ↑A' := (Hom.hom g).toAlgebra
algInst✝¹ : Algebra ↑B ↑B' := (Hom.hom g').toAlgebra
algInst✝ : Algebra ↑A ↑B' := ((Hom.hom f').comp (Hom.hom g)).toAlgebra
scalarTowerInst✝ : IsScalarTower ↑A ↑A' ↑B' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap ↑A ↑B'))
this : IsScalarTower ↑A ↑B ↑B'
⊢ (ConcreteCategory.hom (map fac)) (d b) = d ((ConcreteCategory.hom g') b)

Tactic:
exact _root_.KaehlerDifferential.map_D A A' B B' b

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr
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
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
⊢ (Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))).FG

Tactic:
simp_rw [Submodule.span_iUnion₂, ← Finset.mem_range_succ_iff, iSup_subtype']

Goal state after:
case mpr
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
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
⊢ (⨆ x, Submodule.span (↥(reesAlgebra I)) (single R ↑x '' ↑(F.N ↑x))).FG
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
k : K
c : (j : J) → q j = k → X.CofanMapObjFun p j
hc : (j : J) → (hj : q j = k) → IsColimit (c j hj)
c' : Cofan fun j ↦ (c ↑j ⋯).pt
hc' : IsColimit c'
i : I
hi : r i = k
⊢ q (p i) = k

Tactic:
hpqr,

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
k : K
c : (j : J) → q j = k → X.CofanMapObjFun p j
hc : (j : J) → (hj : q j = k) → IsColimit (c j hj)
c' : Cofan fun j ↦ (c ↑j ⋯).pt
hc' : IsColimit c'
i : I
hi : r i = k
⊢ r i = k
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 ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ { X := fun i ↦ if i = j then X✝ else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i = X✝

Tactic:
dsimp; rw [if_pos h]

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 ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ Y✝ = { X := fun i ↦ if i = j then Y✝ else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i

Tactic:
dsimp; rw [if_pos h]

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

Goal state before:
pp: case e'_1.e'_3
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i✝ : ι
h : ¬i✝ = j
⊢ (if i✝ = j then A else 0) = 0

Tactic:
simp [if_neg h]

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

Goal state before:
pp: case e'_1.e'_4
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i✝ : ι
h : ¬i✝ = j
⊢ (if i✝ = j then A else 0) = 0

Tactic:
simp [if_neg h]

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

Goal state before:
pp: case e'_2.e'_3.e'_2.e'_4
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i✝ : ι
h : ¬i✝ = j
e_1✝¹ : ((if i✝ = j then A else 0) ⟶ if i✝ = j then A else 0) = (0 ⟶ 0)
e_1✝ :
  ({ X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝ ⟶
      { X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝) =
    (0 ⟶ 0)
⊢ { X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝ = 0

Tactic:
simp [if_neg h]

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

Goal state before:
pp: case e'_2.e'_3.e'_2.e'_5
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i✝ : ι
h : ¬i✝ = j
e_1✝¹ : ((if i✝ = j then A else 0) ⟶ if i✝ = j then A else 0) = (0 ⟶ 0)
e_1✝ :
  ({ X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝ ⟶
      { X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝) =
    (0 ⟶ 0)
⊢ { X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝ = 0

Tactic:
simp [if_neg h]

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

Goal state before:
pp: case e'_3
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i✝ : ι
h : ¬i✝ = j
e_1✝ : ((if i✝ = j then A else 0) ⟶ if i✝ = j then A else 0) = (0 ⟶ 0)
⊢ (if i✝ = j then A else 0) = 0

Tactic:
simp [if_neg h]

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

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx✝ : x ∈ ideal R S
hx : x ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ ∀ x ∈ Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1,
    ∃ (hx : x ∈ ideal R S), (fromIdeal R S) ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
hx✝ : x✝ ∈ ideal R S
hx : x✝ ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
x : S
⊢ ∃ (hx : (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x ∈ ideal R S),
    (fromIdeal R S) ⟨(fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D 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
h : Function.Surjective ⇑(algebraMap R S)
⊢ Set.range ⇑(D R S) ⊆ ↑⊥

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
x : S
⊢ (D R S) x ∈ ↑⊥
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X✝ : α → V
d_X : (n : α) → X✝ (n + 1) ⟶ X✝ n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y✝ : α → V
d_Y : (n : α) → Y✝ (n + 1) ⟶ Y✝ n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
X Y : ChainComplex V α
f : (i : α) → X.X i ⟶ Y.X i
comm : ∀ (i : α), f (i + 1) ≫ Y.d (i + 1) i = X.d (i + 1) i ≫ f i
n m : α
⊢ (ComplexShape.down α).Rel n m → f n ≫ Y.d n m = X.d n m ≫ f m

Tactic:
by
    simp only [ComplexShape.down_Rel]
    rintro rfl
    simpa using comm m

Goal state after:
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 • ⊤)
⊢ ∀ r ∈ KaehlerDifferential.ideal R S,
    ∀ n ∈ ⊤, (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) (r • n) = 0

Tactic:
rintro x hx y -

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 : x ∈ KaehlerDifferential.ideal R S
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_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
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 ∈ Set.range ⇑(KaehlerDifferential.D R S), f x = f' x

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
case 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
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
⊢ f ((KaehlerDifferential.D R S) x) = f' ((KaehlerDifferential.D R S) x)
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
inst✝ : EssFiniteType R S
⊢ (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ⊆
    ↑(Ideal.span ↑(Finset.image (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S)))

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
case a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
x : S
⊢ (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x ∈
    ↑(Ideal.span ↑(Finset.image (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset 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
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)
⊢ Set.range ⇑(D R S) ⊆ ↑(Submodule.span S ↑s)

Tactic:
rintro _ ⟨x, rfl⟩

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
inst✝ : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun s ↦ (D R S) s) (EssFiniteType.finset R S)
x : S
⊢ (D R S) x ∈ ↑(Submodule.span S ↑s)
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
hk : k ≫ K.d i j = 0
⊢ K.liftCycles k j hj hk ≫ K.iCycles i = k

Tactic:
dsimp [liftCycles, iCycles]
  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)
⊢ Set.range ⇑(D S B) ⊆ ↑(map R S A B).range

Tactic:
rintro _ ⟨x, rfl⟩

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)
x : B
⊢ (D S B) x ∈ ↑(map R S A B).range
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case 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
⊢ (mapBaseChange R A B).range ≤ (map R A B B).ker

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
case 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
x : B ⊗[A] Ω[A⁄R]
⊢ (mapBaseChange R A B) x ∈ (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)
M : HomologicalComplex C c
α : M ⟶ K
β : M ⟶ L
i : ι
⊢ (biprod.lift α β).f i ≫ biprod.fst.f i = α.f i

Tactic:
rw [← comp_f, biprod.lift_fst]

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
⊢ ∀ a ∈ RingHom.ker (algebraMap A B),
    ⊤ ≤ Submodule.comap ((LinearMap.lsmul A ↥(RingHom.ker (algebraMap A B))) a) (kerToTensor R A B).ker

Tactic:
rintro x hx y -

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
x : A
hx : x ∈ RingHom.ker (algebraMap A B)
y : ↥(RingHom.ker (algebraMap A B))
⊢ y ∈ Submodule.comap ((LinearMap.lsmul A ↥(RingHom.ker (algebraMap A B))) x) (kerToTensor R A B).ker
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : A ⟶ X φ i
h : f ≫ sndX φ i = g ≫ sndX φ i
⊢ f = g

Tactic:
by
  rw [← cancel_mono (XIso φ i hi).hom]
  simpa only [sndX, dif_neg hi] using h

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

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

Tactic:
simp only [comp_v _ _ h p _ q rfl (by lia), neg_v, neg_comp]

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

Tactic:
by rw [hpq, sub_add_cancel]

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 : ℤ
r : R
a : Cochain F G n
⊢ δ n m (r • a) = (RingHom.id R) r • δ n m a

Tactic:
by_cases h : n + 1 = m
    · ext p q hpq
      dsimp
      simp only [δ_v n m h _ p q hpq _ _ rfl rfl, Cochain.smul_v, Linear.comp_smul,
        Linear.smul_comp, smul_add, smul_comm m.negOnePow r]
    · simp only [δ_shape _ _ h, smul_zero]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
h₁ : γ₁.comp (↑(fst φ)) hij = γ₂.comp (↑(fst φ)) hij
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
p q : ℤ
hpq : p + i = q
⊢ γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ ∧
    γ₁.v p q hpq ≫ (snd φ).v q q ⋯ = γ₂.v p q hpq ≫ (snd φ).v q q ⋯

Tactic:
replace h₁ := Cochain.congr_v h₁ p (q + 1) (by lia)

Goal state after:
case mpr
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
p q : ℤ
hpq : p + i = q
h₁ : (γ₁.comp (↑(fst φ)) hij).v p (q + 1) ⋯ = (γ₂.comp (↑(fst φ)) hij).v p (q + 1) ⋯
⊢ γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ ∧
    γ₁.v p q hpq ≫ (snd φ).v q q ⋯ = γ₂.v p q hpq ≫ (snd φ).v q q ⋯
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 : ℤ
x✝² x✝¹ : R
x✝ : Cocycle F G n
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
ext; dsimp; rw [smul_smul]

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

Goal state before:
pp: case h₂
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
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i j : ι
hij : c.Rel i j
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫ (mapHomologicalComplexObjXIso φ H i).inv ≫ H.map (d φ i j) =
    inrX ((H.mapHomologicalComplex c).map φ) i ≫
      d ((H.mapHomologicalComplex c).map φ) i j ≫ (mapHomologicalComplexObjXIso φ H j).inv

Tactic:
· simp [← Functor.map_comp]

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
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ (functor r).map f = (functor r).map f' ↔ r f f'

Tactic:
dsimp [functor]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ Quot.mk (HomRel.CompClosure r) f = Quot.mk (HomRel.CompClosure r) f' ↔ r f f'
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type ?u.8
inst✝ : Category.{v_2, ?u.8} D
F✝ : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F✝.map f₁ = F✝.map f₂
F G : Quotient r ⥤ D
τ : functor r ⋙ F ≅ functor r ⋙ G
⊢ natTransLift r τ.inv ≫ natTransLift r τ.hom = 𝟙 G

Tactic:
rw [comp_natTransLift, τ.inv_hom_id, natTransLift_id]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map f.inv ≫ (quotient V c).map f.hom = 𝟙 ((quotient V c).obj D)

Tactic:
rw [← (quotient V c).map_comp, ← (quotient V c).map_id]
    exact eq_of_homotopy _ _ f.homotopyInvHomId

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
⊢ ∀ (P Q R : Quotient r) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g

Tactic:
rintro _ _ _ ⟨_⟩ ⟨_⟩ ⟨_⟩

Goal state after:
case mk.mk.mk
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P✝ Q✝ R✝ : Quotient r
f✝ : P✝ ⟶ Q✝
a✝² : P✝.as ⟶ Q✝.as
f'✝ : P✝ ⟶ Q✝
a✝¹ : P✝.as ⟶ Q✝.as
g✝ : Q✝ ⟶ R✝
a✝ : Q✝.as ⟶ R✝.as
⊢ (Quot.mk (HomRel.CompClosure r) a✝² + Quot.mk (HomRel.CompClosure r) a✝¹) ≫ Quot.mk (HomRel.CompClosure r) a✝ =
    Quot.mk (HomRel.CompClosure r) a✝² ≫ Quot.mk (HomRel.CompClosure r) a✝ +
      Quot.mk (HomRel.CompClosure r) a✝¹ ≫ Quot.mk (HomRel.CompClosure r) a✝
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
⊢ ∀ (P Q R : Quotient r) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g'

Tactic:
rintro _ _ _ ⟨_⟩ ⟨_⟩ ⟨_⟩

Goal state after:
case mk.mk.mk
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P✝ Q✝ R✝ : Quotient r
f✝ : P✝ ⟶ Q✝
a✝² : P✝.as ⟶ Q✝.as
g✝ : Q✝ ⟶ R✝
a✝¹ : Q✝.as ⟶ R✝.as
g'✝ : Q✝ ⟶ R✝
a✝ : Q✝.as ⟶ R✝.as
⊢ Quot.mk (HomRel.CompClosure r) a✝² ≫ (Quot.mk (HomRel.CompClosure r) a✝¹ + Quot.mk (HomRel.CompClosure r) a✝) =
    Quot.mk (HomRel.CompClosure r) a✝² ≫ Quot.mk (HomRel.CompClosure r) a✝¹ +
      Quot.mk (HomRel.CompClosure r) a✝² ≫ Quot.mk (HomRel.CompClosure r) a✝