mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn : N.FG
hin : N ≤ I • N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0

Tactic:
fg_def

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn : ∃ S, S.Finite ∧ span R S = N
hin : N ≤ I • N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
n : M
hn : n ∈ N
⊢ ((LinearMap.lsmul R M) 1) n ∈ I • N

Tactic:
change (1 : R) • n ∈ I • N

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
n : M
hn : n ∈ N
⊢ 1 • n ∈ I • N
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
i : ℕ
⊢ ∀ c ∈ Finset.antidiagonal i, a✝.coeff c.1 * b✝.coeff c.2 ∈ I ^ i

Tactic:
rintro ⟨j, k⟩ e

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
i j k : ℕ
e : (j, k) ∈ Finset.antidiagonal i
⊢ a✝.coeff (j, k).1 * b✝.coeff (j, k).2 ∈ I ^ i
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case succ.refine_2
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
x y : R
hx : (monomial (n + 1)) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
hy : (monomial (n + 1)) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
⊢ (monomial (n + 1)) (x + y) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
map_add

Goal state after:
case succ.refine_2
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
x y : R
hx : (monomial (n + 1)) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
hy : (monomial (n + 1)) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
⊢ (monomial (n + 1)) x + (monomial (n + 1)) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case a
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ reesAlgebra I ≤ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
intro p

Goal state after:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
p : R[X]
⊢ p ∈ reesAlgebra I → p ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : Infinite R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
h : y ≠ 0
r s : R
hrs : r • y = s • y
⊢ r = s

Tactic:
exact smul_left_injective _ h hrs

Goal state after:
Module: Mathlib.RingTheory.Nakayama

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
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
⊢ ∃ r, r - 1 ∈ I ∧ r • P ≤ N

Tactic:
have hNN'' : P ≤ N ⊔ N' := le_trans hNN' (by simpa using le_trans smul_le_right le_sup_right)
  have h1 : P.map N.mkQ = N'.map N.mkQ := by
    refine le_antisymm ?_ (map_mono hN'le)
    simpa using map_mono (f := N.mkQ) hNN''
  have h2 : P.map N.mkQ = (I • N').map N.mkQ := by
    apply le_antisymm
    · simpa using map_mono (f := N.mkQ) hNN'
    · rw [h1]
      simp [smul_le_right]
  have hle : (P.map N.mkQ) ≤ I • P.map N.mkQ := by
    conv_lhs => rw [h2]
    simp [← h1]
  obtain ⟨r, hmem, hr⟩ := exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I _
    (h1 ▸ hN'.map _) hle
  refine ⟨r, hmem, fun x hx ↦ ?_⟩
  induction hx using Submodule.smul_inductionOn_pointwise with
  | smul₀ p hp =>
    rw [← Submodule.Quotient.mk_eq_zero, Quotient.mk_smul]
    exact hr _ ⟨p, hp, rfl⟩
  | smul₁ _ _ _ h => exact N.smul_mem _ h
  | add _ _ _ _ hx hy => exact N.add_mem hx hy
  | zero => exact N.zero_mem

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 F' : I.Filtration M
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf : f ∈ {f | ∀ (i : ℕ), f.coeff i ∈ F.N i}
i : ℕ
⊢ ∀ c ∈ Finset.antidiagonal i, (↑r).coeff c.1 • f.coeff c.2 ∈ F.N i

Tactic:
rintro ⟨j, k⟩ 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
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf : f ∈ {f | ∀ (i : ℕ), f.coeff i ∈ F.N i}
i j k : ℕ
e : (j, k) ∈ Finset.antidiagonal i
⊢ (↑r).coeff (j, k).1 • f.coeff (j, k).2 ∈ F.N i
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
this : (ModuleCat.Hom.hom (α - β)).ker = ⊤
⊢ α - β = 0

Tactic:
LinearMap.ker_eq_top

Goal state after:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
this : ModuleCat.Hom.hom (α - β) = 0
⊢ α - β = 0
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
this : ModuleCat.Hom.hom (α - β) = 0
⊢ ModuleCat.Hom.hom (α - β) = ModuleCat.Hom.hom 0

Tactic:
exact this

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

Goal state before:
pp: R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
⊢ I₁.Cotangent →ₗ[R] I₂.Cotangent

Tactic:
refine Submodule.mapQ ((I₁ • ⊤ : Submodule A I₁).restrictScalars R)
    ((I₂ • ⊤ : Submodule B I₂).restrictScalars R) ?_ ?_

Goal state after:
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
⊢ ↥I₁ →ₗ[R] ↥I₂

case refine_2
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
⊢ Submodule.restrictScalars R (I₁ • ⊤) ≤ Submodule.comap ?refine_1 (Submodule.restrictScalars R (I₂ • ⊤))
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
I : Ideal S
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ↥I →ₗ[R] M
hf : ∀ (x y : ↥I), f (x * y) = 0
⊢ Function.Surjective ⇑(lift f hf) ↔ Function.Surjective ⇑f

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
R : Type u
inst✝⁴ : CommRing R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
I : Ideal S
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ↥I →ₗ[R] M
hf : ∀ (x y : ↥I), f (x * y) = 0
h : Function.Surjective ⇑(lift f hf)
⊢ Function.Surjective ⇑f

case refine_2
R : Type u
inst✝⁴ : CommRing R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
I : Ideal S
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ↥I →ₗ[R] M
hf : ∀ (x y : ↥I), f (x * y) = 0
h : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(lift f hf)
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⨅ i, I ^ i • ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
⊢ N ≤ I • N

Tactic:
obtain ⟨k, hk⟩ := (I.stableFiltration_stable ⊤).inter_right (I.trivialFiltration N)
        have := hk k (le_refl _)
        rw [hN, hN] at this
        exact le_of_eq this.symm

Goal state after:
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
⊢ ∀ (a : M₁ ⟶ M₂), -a + a = 0

Tactic:
intros; ext1; simp only [add_app, neg_app, neg_add_cancel, zero_app]

Goal state after:
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 : HomologicalComplex V c
inst✝ : HasKernels V
i j j' : ι
r : c.Rel i j
r' : c.Rel i j'
⊢ kernelSubobject (C.d i j) = kernelSubobject (C.d i j')

Tactic:
rw [← d_comp_eqToHom C r r']

Goal state after:
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j j' : ι
r : c.Rel i j
r' : c.Rel i j'
⊢ kernelSubobject (C.d i j' ≫ eqToHom ⋯) = kernelSubobject (C.d i j')
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 : ι), IsZero (S.map (eval C c i)).homology
⊢ IsZero S.homology

Tactic:
IsZero.iff_id_eq_zero

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
⊢ 𝟙 S.homology = 0
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case h.a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) '' ↑(EssFiniteType.finset R S) ⊆ ↑(ideal R S)

Tactic:
rintro _ ⟨x, _, rfl⟩

Goal state after:
case h.a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
x : S
left✝ : x ∈ ↑(EssFiniteType.finset R S)
⊢ (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x ∈ ↑(ideal R 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 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'
⊢ K.d j i ≫ k ≫ α = 0

Tactic:
reassoc_of% hk,

Goal state after:
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
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
⊢ k ≫ K.d i j ≫ φ.f j = 0

Tactic:
reassoc_of% hk,

Goal state after:
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 ≫ φ.f j = 0
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a.add
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x✝ y✝ : B ⊗[A] Ω[A⁄R]
a✝¹ : (mapBaseChange R A B) x✝ ∈ (map R A B B).ker
a✝ : (mapBaseChange R A B) y✝ ∈ (map R A B B).ker
⊢ (mapBaseChange R A B) (x✝ + y✝) ∈ (map R A B B).ker

Tactic:
map_add

Goal state after:
case a.add
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x✝ y✝ : B ⊗[A] Ω[A⁄R]
a✝¹ : (mapBaseChange R A B) x✝ ∈ (map R A B B).ker
a✝ : (mapBaseChange R A B) y✝ ∈ (map R A B B).ker
⊢ (mapBaseChange R A B) x✝ + (mapBaseChange R A B) y✝ ∈ (map R A B B).ker
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a.convert_2
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
⊢ (((Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
        Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
      Set.range fun x ↦ single ((algebraMap A B) x) 1) ⊆
    ↑(Submodule.comap (linearCombination B ⇑(D R B)) (mapBaseChange R A B).range)

Tactic:
rintro f ((⟨⟨x, y⟩, rfl⟩ | ⟨⟨x, y⟩, rfl⟩) | ⟨x, rfl⟩)

Goal state after:
case a.convert_2.inl.inl
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x y : B
⊢ (fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) (x, y) ∈
    ↑(Submodule.comap (linearCombination B ⇑(D R B)) (mapBaseChange R A B).range)

case a.convert_2.inl.inr
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x y : B
⊢ (fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) (x, y) ∈
    ↑(Submodule.comap (linearCombination B ⇑(D R B)) (mapBaseChange R A B).range)

case a.convert_2.inr
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 : A
⊢ (fun x ↦ single ((algebraMap A B) x) 1) x ∈
    ↑(Submodule.comap (linearCombination B ⇑(D R B)) (mapBaseChange R A B).range)
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
⊢ W.IsInvertedBy (F ⋙ G) → W.IsInvertedBy F

pp: case mpr
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
⊢ W.IsInvertedBy F → W.IsInvertedBy (F ⋙ G)

Tactic:
· intro h X Y f hf
    have : IsIso (G.map (F.map f)) := h _ hf
    exact isIso_of_reflects_iso (F.map f) G

Goal state after:
case mpr
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
⊢ W.IsInvertedBy F → W.IsInvertedBy (F ⋙ G)
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 : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
⊢ ofHom φ₁ = δ (-1) 0 (ofHomotopy ho) + ofHom φ₂

Tactic:
simp only [δ_ofHomotopy, sub_add_cancel]

Goal state after:
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 K : HomologicalComplex C c
φ : F ⟶ G
inst✝³ : HasHomotopyCofiber φ
inst✝² : DecidableRel c.Rel
F' F'' G' G'' : HomologicalComplex C c
φ' : F' ⟶ G'
φ'' : F'' ⟶ G''
inst✝¹ : HasHomotopyCofiber φ'
inst✝ : HasHomotopyCofiber φ''
H : ∀ (j : ι), ∃ i, c.Rel i j
α : Arrow.mk φ ≅ Arrow.mk φ'
⊢ mapArrowHom φ' φ' H (α.inv ≫ α.hom) = 𝟙 (homotopyCofiber φ')

Tactic:
Iso.inv_hom_id,

Goal state after:
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
F' F'' G' G'' : HomologicalComplex C c
φ' : F' ⟶ G'
φ'' : F'' ⟶ G''
inst✝¹ : HasHomotopyCofiber φ'
inst✝ : HasHomotopyCofiber φ''
H : ∀ (j : ι), ∃ i, c.Rel i j
α : Arrow.mk φ ≅ Arrow.mk φ'
⊢ mapArrowHom φ' φ' H (𝟙 (Arrow.mk φ')) = 𝟙 (homotopyCofiber φ')
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
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 : ι
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫
      (mapHomologicalComplexObjXIso φ H i).inv ≫ (mapHomologicalComplexObjXIso φ H i).hom =
    inrX ((H.mapHomologicalComplex c).map φ) i

Tactic:
Iso.inv_hom_id,

Goal state after:
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
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 : ι
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫ 𝟙 (X ((H.mapHomologicalComplex c).map φ) i) =
    inrX ((H.mapHomologicalComplex c).map φ) 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✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ i + 1 = (ComplexShape.up ℕ).next i

Tactic:
simp only [CochainComplex.next]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ H.map ((inr φ).f n) ≫ (mapHomologicalComplexXIso φ H n).hom =
    (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n

Tactic:
simp only [mapHomologicalComplexXIso_eq φ H n (n + 1) rfl, mappingCone.ext_to_iff _ _ _ rfl,
    Functor.mapHomologicalComplex_obj_X, mapHomologicalComplexXIso'_hom, comp_add,
    add_comp, assoc, inl_v_fst_v, comp_id, inr_f_fst_v, comp_zero, add_zero, inl_v_snd_v,
    inr_f_snd_v, zero_add, ← H.map_comp, H.map_zero, H.map_id, and_self]

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

Goal state before:
pp: ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
⊢ IsZero ((quotient V c).obj C) ↔ Nonempty (Homotopy (𝟙 C) 0)

Tactic:
IsZero.iff_id_eq_zero

Goal state after:
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
⊢ 𝟙 ((quotient V c).obj C) = 0 ↔ Nonempty (Homotopy (𝟙 C) 0)
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
h : Homotopy φ₀ φ₁
hc : ∀ (j : ι), ∃ i, c.Rel i j
inst✝² : ∀ (i : ι), HasBinaryBiproduct (F.X i) (F.X i)
inst✝¹ : HasHomotopyCofiber (biprod.lift (𝟙 F) (-𝟙 F))
D : Type u_3
inst✝ : Category.{v_2, u_3} D
H : HomologicalComplex C c ⥤ D
hH : (homotopyEquivalences C c).IsInvertedBy H
⊢ H.map φ₀ = H.map φ₁

Tactic:
simp only [← cylinder.ι₀_desc _ _ h, ← cylinder.ι₁_desc _ _ h, H.map_comp,
    cylinder.map_ι₀_eq_map_ι₁ _ hc _ hH]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
subst h
  rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_hom_app_f]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a p q : ℤ
hpq : p + n = q
⊢ (γ.shift a).v p q hpq = γ.v (p + a) (q + a) ⋯

Tactic:
by
  simp only [shift_v γ a p q hpq _ _ rfl rfl, shiftFunctor_obj_X, shiftFunctorObjXIso,
    HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
this : HasShift D A := HasShift.induced F A s i
⊢ F.CommShift A

Tactic:
exact
    { commShiftIso := fun a => (i a).symm
      commShiftIso_zero := by
        ext X
        dsimp
        simp only [isoZero_hom_app, shiftFunctorZero_inv_app_obj_of_induced,
          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp]
      commShiftIso_add := fun a b => by
        ext X
        dsimp
        simp only [isoAdd_hom_app, Iso.symm_hom, shiftFunctorAdd_inv_app_obj_of_induced,
          shiftFunctor_of_induced]
        rw [← Functor.map_comp_assoc, Iso.inv_hom_id_app]
        dsimp
        rw [Functor.map_id, Category.id_comp, Iso.inv_hom_id_app_assoc,
          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp] }

Goal state after: