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

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h✝ : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ PrimeSpectrum.comap (algebraMap R S) Q
P : Ideal S
hle : P ≤ Q.asIdeal
hP : P.IsPrime
h : P.LiesOver p.asIdeal
⊢ ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' Q ∧ PrimeSpectrum.comap (algebraMap R S) a' = p

Tactic:
refine ⟨⟨P, hP⟩, (PrimeSpectrum.le_iff_specializes _ Q).mp hle, ?_⟩

Goal state after:
case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h✝ : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ PrimeSpectrum.comap (algebraMap R S) Q
P : Ideal S
hle : P ≤ Q.asIdeal
hP : P.IsPrime
h : P.LiesOver p.asIdeal
⊢ PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := hP } = p
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this✝ : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
this : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
hl : Ideal.under (Localization.AtPrime (Ideal.under R Q)) Pl = pl
⊢ p = Ideal.under R (Ideal.under S Pl)

Tactic:
Ideal.under_under,

Goal state after:
case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this✝ : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
this : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
hl : Ideal.under (Localization.AtPrime (Ideal.under R Q)) Pl = pl
⊢ p = Ideal.under R Pl
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x y : M
this : f (d (f_inv (x * y) - f_inv x * f_inv y)) = 0
⊢ { toFun := fun x ↦ f (d (f_inv x)), map_add' := ⋯, map_smul' := ⋯ } (x * y) =
    x • { toFun := fun x ↦ f (d (f_inv x)), map_add' := ⋯, map_smul' := ⋯ } y +
      y • { toFun := fun x ↦ f (d (f_inv x)), map_add' := ⋯, map_smul' := ⋯ } x

Tactic:
by simpa [sub_eq_zero, hf _]

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

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-(a ^ ↑(n.natAbs * 2))⁻¹ * ↑n.natAbs * a ^ ↑(n.natAbs - 1)) • D a = (↑(-↑n.natAbs) * a ^ (-↑n.natAbs - 1)) • D a

Tactic:
trans (-n.natAbs * (a ^ ((n.natAbs - 1 : ℕ) : ℤ) / (a ^ ((n.natAbs * 2 : ℕ) : ℤ)))) • D a

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-(a ^ ↑(n.natAbs * 2))⁻¹ * ↑n.natAbs * a ^ ↑(n.natAbs - 1)) • D a =
    (-↑n.natAbs * (a ^ ↑(n.natAbs - 1) / a ^ ↑(n.natAbs * 2))) • D a

R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ (-↑n.natAbs * (a ^ ↑(n.natAbs - 1) / a ^ ↑(n.natAbs * 2))) • D a = (↑(-↑n.natAbs) * a ^ (-↑n.natAbs - 1)) • D a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
a : ↑(Set.range f)
⊢ IsLocalization.Away (f (e.symm a)) (Localization.Away ↑a)

Tactic:
simp_rw [e, Equiv.apply_ofInjective_symm]

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
a : ↑(Set.range f)
⊢ IsLocalization.Away (↑a) (Localization.Away ↑a)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
g : G
hg : orderOf g = Nat.card G
⊢ ↑⋯.choose = 1

Tactic:
← Int.cast_one,

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
g : G
hg : orderOf g = Nat.card G
⊢ ↑⋯.choose = ↑1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
⊢ s = ↑(basicOpen x)

Tactic:
refine subset_antisymm ?_ ?_

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
⊢ s ⊆ ↑(basicOpen x)

case refine_2
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ J ^ n
add : x + y = 1
mul : x * y = 0
⊢ ↑(basicOpen x) ⊆ s
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Function.Bijective fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }

Tactic:
refine ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ eq ↦ mul_eq_zero_add_eq_one_ext_left ?_, fun s ↦ ?_⟩
      · exact basicOpen_injOn_isIdempotentElem (IsIdempotentElem.of_mul_add hx.1 hx.2).1
          (IsIdempotentElem.of_mul_add hy.1 hy.2).1 <| SetLike.ext' (congr_arg (·.1) eq)
      · have ⟨e, f, mul, add, eq⟩ := isClopen_iff_mul_add.mp s.2
        exact ⟨⟨(e, f), mul, add⟩, SetLike.ext' eq.symm⟩

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this✝ : Finite G
hcG : IsPGroup p ↥(center G)
x✝ : ∃ n, Nat.card ↥(center G) = p ^ n
this : Nontrivial G
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k

Tactic:
exact (nontrivial_iff_card hcG).mp (center_nontrivial (of_card hGpn))

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 ↦ x * x_1) n 1
⊢ ↑(⟨x, ⋯⟩ ^ n) = 1

Tactic:
SubmonoidClass.coe_pow,

Goal state after:
G : Type u_1
inst✝ : CommMonoid G
x✝ : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun x_1 ↦ x * x_1) n 1
⊢ ↑⟨x, ⋯⟩ ^ n = 1
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
hf : Function.Injective ⇑f
⊢ Subgroup.comap f (torsion H) = torsion G

Tactic:
ext x
  exact hf.isOfFinOrder_iff

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

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Ring S
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
⊢ ∃ a, ⊥ = R ∙ a

pp: case inr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Ring S
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
⊢ ∃ a, ⊤ = R ∙ a

Tactic:
· exact ⟨0, Submodule.span_zero.symm⟩

Goal state after:
case inr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Ring S
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
⊢ ∃ a, ⊤ = R ∙ a
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
⊢ Iso (x₁, y₁) (s.toFun (Fin.last s.length), x₂)

Tactic:
exact hr₂

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

Goal state before:
pp: case mem
R : Type u_2
inst✝⁴ : Ring R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite (End R M) M
s : Finset M
hs : span (End R M) ↑s = ⊤
f : End (End R M) M
r : R
hr : ∀ m ∈ s, f m = r • m
m✝ m : M
hm : m ∈ ↑s
⊢ ((toModuleEnd (End R M) M) r) m = f m

Tactic:
exact (hr m hm).symm

Goal state after:
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
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
this : Ideal.span s ≤ Ideal.torsionOf R M x
a : R
ha : a ∈ ↑(Ideal.span s)
⊢ ↑⟨a, ha⟩ • x = 0

Tactic:
exact this ha

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

Goal state before:
pp: case zero
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
⊢ (map R' f) (p • 0) = Polynomial.map (algebraMap R R') p • (map R' f) 0

Tactic:
rw [smul_zero, map_zero, smul_zero]

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

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_5
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m✝ m' m₁ m₂ m₁' m₂' : M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ (((coeffEquiv R).toFun m).sum fun i c ↦ r ^ i • s • c) = (RingHom.id R) s • m.coeff.sum fun i m ↦ r ^ i • m

Tactic:
simp_rw [RingHom.id_apply, Finsupp.smul_sum]
      congr
      ext i c
      rw [smul_comm]

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

Goal state before:
pp: case zero
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
⊢ (eval r) (p • 0) = Polynomial.eval r p • (eval r) 0

Tactic:
rw [smul_zero, map_zero, smul_zero]

Goal state after:
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case h.refine_2.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hsspan : span R s = map (I • N).mkQ N
⊢ span R (Quotient.out '' s) = N

Tactic:
· symm; apply eq_of_map_mkQ_eq_map_mkQ_of_le_jacobson_bot hN hIjac
    simp [← hsspan, map_span, Set.image_image]

Goal state after:
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)
y : ↑B
⊢ (ModuleCat.Hom.hom α - ModuleCat.Hom.hom β) ((_root_.KaehlerDifferential.D ↑A ↑B) y) = 0

Tactic:
LinearMap.sub_apply,

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)
y : ↑B
⊢ (ModuleCat.Hom.hom α) ((_root_.KaehlerDifferential.D ↑A ↑B) y) -
      (ModuleCat.Hom.hom β) ((_root_.KaehlerDifferential.D ↑A ↑B) y) =
    0
Module: Mathlib.RingTheory.Ideal.Cotangent

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

Tactic:
rw [to_quotient_square_comp_toCotangent, LinearMap.range_comp, I.range_subtype]; ext; rfl

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ F'.submodule.FG

pp: case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ ∀ (i : ℕ), (F'.N i).FG

pp: case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
⊢ ∀ (i : ℕ), (F.N i).FG

Tactic:
any_goals intro i; exact IsNoetherian.noetherian _

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 : I.Filtration M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ F'.submodule.FG
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
d : M.Derivation φ
h₁ h₂ : d.Universal
this : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), h₁.desc d' = h₂.desc d'
⊢ h₁ = h₂

Tactic:
cases h₁
        cases h₂
        simp only [Universal.mk.injEq]
        ext : 2
        apply this

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 b : M₁ ⟶ M₂), a - b = a + -b

Tactic:
intros; ext1; simp only [add_app, sub_app, neg_app, sub_eq_add_neg]

Goal state after:
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
m₁ m₂ m₃ : A
X : C
⊢ (h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫ (h.add (m₁ + m₂) m₃).inv.app X =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫ (h.add m₁ (m₂ + m₃)).inv.app X ≫ eqToHom ⋯

Tactic:
rw [← cancel_mono ((h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)),
    Category.assoc, Category.assoc, Category.assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp,
    Iso.inv_hom_id_app, Functor.map_id, h.assoc_hom_app, eqToHom_trans_assoc, eqToHom_refl,
    Category.id_comp, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ 𝟙 ((h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X)) = 𝟙 ((h.F m₂ ⋙ h.F m₃).obj ((h.F m₁).obj X))
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
x✝ : S ⊗[R] S
x y : S
⊢ x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)

Tactic:
smul_sub,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
⊢ x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • 1 ⊗ₜ[R] y - x • y ⊗ₜ[R] 1
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ eqToHom ⋯ ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ }
              (MonoidalCategoryStruct.tensorObj { as := a₂ } { as := a₃ })).app
          X ≫
        (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
          (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X) =
    (eqToHom ⋯ ≫ (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }).app X) ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
        (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X)

Tactic:
Category.assoc

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ eqToHom ⋯ ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ }
              (MonoidalCategoryStruct.tensorObj { as := a₂ } { as := a₃ })).app
          X ≫
        (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
          (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X) =
    eqToHom ⋯ ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }).app X ≫
        (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
          (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X)
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
x y z : S
⊢ (z𝖣x + y) = (z𝖣x) + z𝖣y

Tactic:
rw [← map_add, eq_comm, ← sub_eq_zero, ← map_sub (Submodule.mkQ (kerTotal R S)),
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]
  simp_rw [← Finsupp.smul_single_one _ z, ← smul_add, ← smul_sub]
  exact Submodule.smul_mem _ _ (Submodule.subset_span (Or.inl <| Or.inl <| ⟨⟨_, _⟩, rfl⟩))

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
⊢ RingHom.ker (algebraMap A B) • ⊤ ≤ (kerToTensor R A B).ker

Tactic:
rw [Submodule.smul_eq_map₂]
    apply iSup_le_iff.mpr
    simp only [Submodule.map_le_iff_le_comap, Subtype.forall]
    rintro x hx y -
    simp only [Submodule.mem_comap, LinearMap.lsmul_apply, LinearMap.mem_ker, map_smul,
      kerToTensor_apply, TensorProduct.smul_tmul', ← algebraMap_eq_smul_one,
      RingHom.mem_ker.mp hx, TensorProduct.zero_tmul]

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

Goal state before:
pp: case w
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
this : ∑ i ∈ x.support with (algebraMap A B) i = c, x i ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
i : ↥({i ∈ x.support | (algebraMap A B) i = c})
⊢ ↑i - a ∈ RingHom.ker (algebraMap A B)

Tactic:
have : x i ≠ 0 ∧ algebraMap A B i = c := by
        convert! i.prop
        simp_rw [Finset.mem_filter, Finsupp.mem_support_iff]
      simp [RingHom.mem_ker, ha, this.2]

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 ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
⊢ (inl φ).v p₁ p₂ h₁₂ ≫ (descCochain φ α β h).v p₂ p₃ h₂₃ = α.v p₁ p₃ ⋯

Tactic:
simpa only [Cochain.comp_v _ _ (show -1 + n = m by lia) p₁ p₂ p₃
    (by lia) (by lia)] using
      Cochain.congr_v (inl_descCochain φ α β h) p₁ p₃ (by lia)

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 : ℤ
φ₁ φ₂ : F ⟶ G
z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq : φ₁.f p = F.d p (p + 1) ≫ (↑z).v (p + 1) p ⋯ + (↑z).v p (p - 1) ⋯ ≫ G.d (p - 1) p + φ₂.f p
⊢ φ₁.f p =
    ((F.d p (p + 1) ≫ if hij : p + 1 + -1 = p then (↑z).v (p + 1) p hij else 0) +
        (prevD p) fun i j ↦ if hij : i + -1 = j then (↑z).v i j hij else 0) +
      φ₂.f p

Tactic:
prevD_eq _ h₁,

Goal state after:
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
z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq : φ₁.f p = F.d p (p + 1) ≫ (↑z).v (p + 1) p ⋯ + (↑z).v p (p - 1) ⋯ ≫ G.d (p - 1) p + φ₂.f p
⊢ φ₁.f p =
    (F.d p (p + 1) ≫ if hij : p + 1 + -1 = p then (↑z).v (p + 1) p hij else 0) +
        (if hij : p + -1 = p - 1 then (↑z).v p (p - 1) hij else 0) ≫ G.d (p - 1) p +
      φ₂.f p
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
f₁ f₂ : F ⟶ G
h : ofHom f₁ = ofHom f₂
⊢ (Cocycle.equivHom F G) f₁ = (Cocycle.equivHom F G) f₂

Tactic:
by ext1; exact h

Goal state after: