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

Goal state before:
pp: case neg.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
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, single R i '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : single R j '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • F.N j)
x y : M
hx : single R (j + 1) x ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
hy : single R (j + 1) y ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
⊢ single R (j + 1) (x + y) ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))

Tactic:
rw [PolynomialModule.single_add]

Goal state after:
case neg.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
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, single R i '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : single R j '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • F.N j)
x y : M
hx : single R (j + 1) x ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
hy : single R (j + 1) y ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
⊢ single R (j + 1) x + single R (j + 1) y ∈
    ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: 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
f : A →ₐ[R] B
a : A
ha : a ∈ RingHom.ker f.toRingHom ^ 2
⊢ f.toRingHom a = 0

Tactic:
exact Ideal.pow_le_self two_ne_zero ha

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Projective

Goal state before:
pp: R : Type u
inst✝² : Ring R
P : ModuleCat R
inst✝¹ : Small.{v, u} R
inst✝ : CategoryTheory.Projective P
M✝ : Type v
⊢ ∀ {N : Type v} [inst : AddCommGroup M✝] [inst_1 : AddCommGroup N] [inst_2 : Module R M✝] [inst_3 : Module R N]
    (f : M✝ →ₗ[R] N) (g : ↑P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g

Tactic:
_

Goal state after:
R : Type u
inst✝² : Ring R
P : ModuleCat R
inst✝¹ : Small.{v, u} R
inst✝ : CategoryTheory.Projective P
M✝ N✝ : Type v
⊢ ∀ [inst : AddCommGroup M✝] [inst_1 : AddCommGroup N✝] [inst_2 : Module R M✝] [inst_3 : Module R N✝] (f : M✝ →ₗ[R] N✝)
    (g : ↑P →ₗ[R] N✝), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
Module: Mathlib.Algebra.Category.ModuleCat.Projective

Goal state before:
pp: R : Type u
inst✝² : Ring R
P : ModuleCat R
inst✝¹ : Small.{v, u} R
inst✝ : CategoryTheory.Projective P
M✝ N✝ : Type v
⊢ ∀ [inst : AddCommGroup M✝] [inst_1 : AddCommGroup N✝] [inst_2 : Module R M✝] [inst_3 : Module R N✝] (f : M✝ →ₗ[R] N✝)
    (g : ↑P →ₗ[R] N✝), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g

Tactic:
_

Goal state after:
R : Type u
inst✝³ : Ring R
P : ModuleCat R
inst✝² : Small.{v, u} R
inst✝¹ : CategoryTheory.Projective P
M✝ N✝ : Type v
inst✝ : AddCommGroup M✝
⊢ ∀ [inst : AddCommGroup N✝] [inst_1 : Module R M✝] [inst_2 : Module R N✝] (f : M✝ →ₗ[R] N✝) (g : ↑P →ₗ[R] N✝),
    Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
Module: Mathlib.Algebra.Category.ModuleCat.Projective

Goal state before:
pp: R : Type u
inst✝³ : Ring R
P : ModuleCat R
inst✝² : Small.{v, u} R
inst✝¹ : CategoryTheory.Projective P
M✝ N✝ : Type v
inst✝ : AddCommGroup M✝
⊢ ∀ [inst : AddCommGroup N✝] [inst_1 : Module R M✝] [inst_2 : Module R N✝] (f : M✝ →ₗ[R] N✝) (g : ↑P →ₗ[R] N✝),
    Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g

Tactic:
_

Goal state after:
R : Type u
inst✝⁴ : Ring R
P : ModuleCat R
inst✝³ : Small.{v, u} R
inst✝² : CategoryTheory.Projective P
M✝ N✝ : Type v
inst✝¹ : AddCommGroup M✝
inst✝ : AddCommGroup N✝
⊢ ∀ [inst : Module R M✝] [inst_1 : Module R N✝] (f : M✝ →ₗ[R] N✝) (g : ↑P →ₗ[R] N✝),
    Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
Module: Mathlib.Algebra.Category.ModuleCat.Projective

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
P : ModuleCat R
inst✝³ : Small.{v, u} R
inst✝² : CategoryTheory.Projective P
M✝ N✝ : Type v
inst✝¹ : AddCommGroup M✝
inst✝ : AddCommGroup N✝
⊢ ∀ [inst : Module R M✝] [inst_1 : Module R N✝] (f : M✝ →ₗ[R] N✝) (g : ↑P →ₗ[R] N✝),
    Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g

Tactic:
_

Goal state after:
R : Type u
inst✝⁵ : Ring R
P : ModuleCat R
inst✝⁴ : Small.{v, u} R
inst✝³ : CategoryTheory.Projective P
M✝ N✝ : Type v
inst✝² : AddCommGroup M✝
inst✝¹ : AddCommGroup N✝
inst✝ : Module R M✝
⊢ ∀ [inst : Module R N✝] (f : M✝ →ₗ[R] N✝) (g : ↑P →ₗ[R] N✝), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
Module: Mathlib.Algebra.Category.ModuleCat.Projective

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
P : ModuleCat R
inst✝⁴ : Small.{v, u} R
inst✝³ : CategoryTheory.Projective P
M✝ N✝ : Type v
inst✝² : AddCommGroup M✝
inst✝¹ : AddCommGroup N✝
inst✝ : Module R M✝
⊢ ∀ [inst : Module R N✝] (f : M✝ →ₗ[R] N✝) (g : ↑P →ₗ[R] N✝), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g

Tactic:
_

Goal state after:
R : Type u
inst✝⁶ : Ring R
P : ModuleCat R
inst✝⁵ : Small.{v, u} R
inst✝⁴ : CategoryTheory.Projective P
M✝ N✝ : Type v
inst✝³ : AddCommGroup M✝
inst✝² : AddCommGroup N✝
inst✝¹ : Module R M✝
inst✝ : Module R N✝
⊢ ∀ (f : M✝ →ₗ[R] N✝) (g : ↑P →ₗ[R] N✝), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
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]
⊢ 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:
_

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))
⊢ 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.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))
⊢ 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:
_

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))
⊢ f x = f' x → f y = f' y → f (x + y) = f' (x + y)
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
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))
a : S
x : Ω[S⁄R]
⊢ x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) → f x = f' x → f (a • x) = f' (a • x)

Tactic:
_

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
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))
a : S
x : Ω[S⁄R]
hx✝ : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ f x = f' x → f (a • x) = f' (a • x)
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 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:
_

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
hx✝ : 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: 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
hx✝ : 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:
_

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
hx✝ : x ∈ adjoin R ↑(EssFiniteType.finset R S)
hy✝ : 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.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ : (j : J) → C j
⊢ ∀ ⦃Y : (j : J) → C j⦄ (f : X✝ ⟶ Y), MorphismProperty.pi W f → IsIso ((Functor.pi F).map f)

Tactic:
_

Goal state after:
J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ Y✝ : (j : J) → C j
⊢ ∀ (f : X✝ ⟶ Y✝), MorphismProperty.pi W f → IsIso ((Functor.pi F).map f)
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.isoClosure.IsInvertedBy F
⊢ W.IsInvertedBy F

Tactic:
X

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.isoClosure.IsInvertedBy F
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), W f → IsIso (F.map f)
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.IsInvertedBy F
⊢ W.isoClosure.IsInvertedBy F

Tactic:
X

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
h : W.IsInvertedBy F
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), W.isoClosure f → IsIso (F.map f)
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
h : W.IsInvertedBy (F ⋙ G)
⊢ W.IsInvertedBy F

Tactic:
X

Goal state after:
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
h : W.IsInvertedBy (F ⋙ G)
X : C₁
⊢ ∀ ⦃Y : C₁⦄ (f : X ⟶ Y), W f → IsIso (F.map f)
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), isomorphisms C f → IsIso (F.map f)

Tactic:
_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), isomorphisms C f → IsIso (F.map f)
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), isomorphisms C f → IsIso (F.map f)

Tactic:
_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ isomorphisms C f✝ → IsIso (F.map f✝)
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 : ι
⊢ (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

Tactic:
simp only [assoc, g.comm]

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

Goal state before:
pp: case mpr
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 : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
c : B
⊢ c ∈ Finset.image (⇑(algebraMap A B)) x.support →
    1 ⊗ₜ[A] (linearCombination A ⇑(D R A)) (∑ i ∈ x.support with (algebraMap A B) i = c, single i (x i)) ∈
      (kerCotangentToTensor R A B).range

Tactic:
_

Goal state after:
case mpr
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 : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
⊢ 1 ⊗ₜ[A] (linearCombination A ⇑(D R A)) (∑ i ∈ x.support with (algebraMap A B) i = c, single i (x i)) ∈
    (kerCotangentToTensor R A B).range
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

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

Tactic:
comp_v z₁ (z₂.comp z₃ rfl) (add_assoc n₁ n₂ n₃).symm p (p + n₁) q (by lia) (by lia),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K L : CochainComplex C ℤ
n₁ n₂ n₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
p q : ℤ
hpq : p + (n₁ + n₂ + n₃) = q
⊢ (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ z₃.v (p + n₁ + n₂) q ⋯ =
    z₁.v p (p + n₁) ⋯ ≫ (z₂.comp z₃ ⋯).v (p + n₁) q ⋯
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₁ z₁' : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ ((z₁ + z₁').comp z₂ h).v p q hpq = (z₁.comp z₂ h + z₁'.comp z₂ h).v p q hpq

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

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain G K d
he : 0 + d = e
⊢ (Cochain.ofHom (inr φ)).comp ((snd φ).comp γ he) ⋯ = γ

Tactic:
obtain rfl : d = e := by lia

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d : ℤ
γ : Cochain G K d
he : 0 + d = d
⊢ (Cochain.ofHom (inr φ)).comp ((snd φ).comp γ he) ⋯ = γ
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

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

Tactic:
simp only [δ_v n₁ n₂ h₁₂ _ p q hpq _ _ rfl rfl,
    δ_v n₀ n₁ h₀₁ z p (q - 1) (by lia) (q - 2) _ (by lia) rfl,
    δ_v n₀ n₁ h₀₁ z (p + 1) q (by lia) _ (p + 2) rfl (by lia),
    ← h₁₂, Int.negOnePow_succ, add_comp, assoc,
    HomologicalComplex.d_comp_d, comp_zero, zero_add, comp_add,
    HomologicalComplex.d_comp_d_assoc, zero_comp, smul_zero,
    add_zero, add_neg_cancel, Units.neg_smul,
    Linear.units_smul_comp, Linear.comp_units_smul]

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
K : HomologicalComplex C c
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
y₂ : Homotopy (φ ≫ ⟨x₁, x₂⟩.fst) 0
h : ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = ⟨⟨x₁, x₂⟩.fst, y₂⟩.snd.hom i j
i j : ι
hij : ¬c.Rel j i
⊢ x₂.hom i j = y₂.hom i j

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

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 i : ℤ
z : Cochain F G 0
hz : δ 0 1 z = 0
⊢ z.v i i ⋯ ≫ G.d i (i + 1) = F.d i (i + 1) ≫ z.v (i + 1) (i + 1) ⋯

Tactic:
simpa only [δ_zero_cochain_v, Cochain.zero_v, sub_eq_zero]
      using Cochain.congr_v hz i (i + 1) rfl

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 : Cocycle F G 0
⊢ ∀ (i j : ℤ), (ComplexShape.up ℤ).Rel i j → (↑z).v i i ⋯ ≫ G.d i j = F.d i j ≫ (↑z).v j j ⋯

Tactic:
rintro i j rfl
    rcases z with ⟨z, hz⟩
    dsimp
    rw [mem_iff 0 1 (zero_add 1)] at hz
    simpa only [δ_zero_cochain_v, Cochain.zero_v, sub_eq_zero]
      using Cochain.congr_v hz i (i + 1) rfl

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
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
⊢ (mapHomologicalComplexObjXIso φ H i).inv ≫ H.map (d φ i j) =
    d ((H.mapHomologicalComplex c).map φ) i j ≫ (mapHomologicalComplexObjXIso φ H j).inv

Tactic:
apply ext_from_X _ _ _ hij

Goal state after:
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
⊢ inlX ((H.mapHomologicalComplex c).map φ) j i hij ≫ (mapHomologicalComplexObjXIso φ H i).inv ≫ H.map (d φ i j) =
    inlX ((H.mapHomologicalComplex c).map φ) j i hij ≫
      d ((H.mapHomologicalComplex c).map φ) i j ≫ (mapHomologicalComplexObjXIso φ H j).inv

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