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

Goal state before:
pp: case refine_1
R₀ : Type u_1
R : Type u_2
M✝ : Type u
inst✝⁹ : Ring R₀
inst✝⁸ : Ring R
inst✝⁷ : Module R₀ R
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R₀ M✝
inst✝⁴ : Module R M✝
inst✝³ : IsScalarTower R₀ R M✝
inst✝² : IsSemiprimaryRing R
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝⁵ : AddCommGroup M
x✝⁴ : Module R₀ M
x✝³ : Module R M
x✝² : IsScalarTower R₀ R M
x✝¹ : IsSemisimpleModule R M
hJ : Module.IsTorsionBySet R M ↑(Ring.jacobson R)
x✝ : Module (R ⧸ Ring.jacobson R) M := hJ.module
this :
  [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE
h : Module.Finite R M ∨ IsArtinian R M
⊢ Module.Finite R₀ M

Tactic:
this.out 2 0,

Goal state after:
case refine_1
R₀ : Type u_1
R : Type u_2
M✝ : Type u
inst✝⁹ : Ring R₀
inst✝⁸ : Ring R
inst✝⁷ : Module R₀ R
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R₀ M✝
inst✝⁴ : Module R M✝
inst✝³ : IsScalarTower R₀ R M✝
inst✝² : IsSemiprimaryRing R
inst✝¹ : IsScalarTower R₀ R R
inst✝ : Module.Finite R₀ (R ⧸ Ring.jacobson R)
M : Type u
x✝⁵ : AddCommGroup M
x✝⁴ : Module R₀ M
x✝³ : Module R M
x✝² : IsScalarTower R₀ R M
x✝¹ : IsSemisimpleModule R M
hJ : Module.IsTorsionBySet R M ↑(Ring.jacobson R)
x✝ : Module (R ⧸ Ring.jacobson R) M := hJ.module
this :
  [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE
h : Module.Finite R M ∨ Module.Finite R M
⊢ Module.Finite R₀ M
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
hq : q.IsPrime
inst✝¹ : Algebra (Localization.AtPrime (under R q)) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (under R q) q
⊢ q.inertiaDeg R = Module.finrank (under R q).ResidueField q.ResidueField

Tactic:
convert! dif_pos hq

Goal state after:
case e'_3
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
hq : q.IsPrime
inst✝¹ : Algebra (Localization.AtPrime (under R q)) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (under R q) q
⊢ inst✝¹ = Localization.AtPrime.algebraOfLiesOver (under R q) q
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
⊢ (g • q).inertiaDeg R = q.inertiaDeg R

Tactic:
let p := q.under R

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
p : Ideal R := under R q
⊢ (g • q).inertiaDeg R = q.inertiaDeg R
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
h : IsFiniteLength A M
⊢ length B (B ⊗[A] M) = length A M * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
obtain ⟨s, hs_bot, hs_top⟩ := isFiniteLength_iff_exists_compositionSeries.mp h
    rw [← length_compositionSeries s hs_bot hs_top]
    suffices ∀ k, length B ((s k).baseChange B) =
        k * length B (B ⧸ (maximalIdeal A).map (algebraMap A B)) by
      rw [← Fin.val_last s.length, ← this, ← RelSeries.last, hs_top, baseChange_top, length_top]
    intro k
    induction k using Fin.induction with
    | zero => rw [← RelSeries.head, hs_bot, baseChange_bot]; simp
    | succ i hi => simpa [hi, add_one_mul] using (s.step i).length_baseChange B

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
A : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
B : Type u_3
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ (Ideal.Quotient.mkₐ R I).comp (f₁.comp (IsScalarTower.toAlgHom R A B)) =
    (Ideal.Quotient.mkₐ R I).comp (f₂.comp (IsScalarTower.toAlgHom R A B))

Tactic:
by rw [← AlgHom.comp_assoc, e, AlgHom.comp_assoc]

Goal state after:
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
s : S
⊢ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 ∈ Ideal.span {e}

Tactic:
← he₂

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
s : S
⊢ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
inst✝ : QuasiFiniteAt R Q
⊢ ∀ (y : ↥Q.primeCompl), IsUnit ((IsScalarTower.toAlgHom R S (Localization.AtPrime P)) ↑y)

Tactic:
simp only [IsScalarTower.coe_toAlgHom', Subtype.forall, Ideal.mem_primeCompl_iff]
      exact fun a ha ↦ IsLocalization.map_units (M := P.primeCompl) _ ⟨a, fun h ↦ ha (h₁ h)⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : IsArtinianRing R
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R p
⊢ ∀ {x₁ x₂ : Localization.AtPrime p}, LinearMap.id x₁ = LinearMap.id x₂ → ∃ c, c • x₁ = c • x₂

Tactic:
by simpa using ⟨1, p.primeCompl.one_mem⟩

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_1
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u_4
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker g)
x : A
⊢ g ((liftOfSurjective f g hg hg') x) = f x

Tactic:
apply (Ideal.quotientKerAlgEquivOfSurjective hg).symm.injective

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_1
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u_4
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker g)
x : A
⊢ (Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x)) =
    (Ideal.quotientKerAlgEquivOfSurjective hg).symm (f x)
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
a b : S
this : ∀ (x y : S ⊗[P] Ω[P⁄R]), ↑(l x) * ↑(l y) = 0
⊢ σ (a * b) - ↑(l (1 ⊗ₜ[P] (D R P) (σ (a * b)))) =
    (σ a - ↑(l (1 ⊗ₜ[P] (D R P) (σ a)))) * (σ b - ↑(l (1 ⊗ₜ[P] (D R P) (σ b))))

Tactic:
simp only [sectionOfRetractionKerToTensorAux_prop l hl (σ (a * b)) (σ a * σ b) (by simp [hσ]),
      Derivation.leibniz, tmul_add, tmul_smul, map_add, map_smul, Submodule.coe_add,
      SetLike.val_smul, smul_eq_mul, mul_sub, sub_mul, this, sub_zero]

Goal state after:
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
a b : S
this : ∀ (x y : S ⊗[P] Ω[P⁄R]), ↑(l x) * ↑(l y) = 0
⊢ σ a * σ b - (σ a * ↑(l (1 ⊗ₜ[P] (D R P) (σ b))) + σ b * ↑(l (1 ⊗ₜ[P] (D R P) (σ a)))) =
    σ a * σ b - ↑(l (1 ⊗ₜ[P] (D R P) (σ a))) * σ b - σ a * ↑(l (1 ⊗ₜ[P] (D R P) (σ b)))
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case refine_4
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
P' : Type u_2 := P ⧸ RingHom.ker (algebraMap P S) ^ 2
h₁ : Surjective ⇑(algebraMap P' S)
h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥
e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] ↥(RingHom.ker (algebraMap P' S)) :=
  (RingHom.ker (algebraMap P S)).cotangentEquivIdeal ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq (RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom).cotangentIdeal
        (RingHom.ker (IsScalarTower.toAlgHom R P S).kerSquareLift.toRingHom) ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H : kerCotangentToTensor R P S = ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁
⊢ Function.LeftInverse
    (fun x ↦
      match x with
      | ⟨l, hl⟩ => ⟨↑e₁.symm ∘ₗ ↑P l ∘ₗ ↑e₂.symm, ⋯⟩)
    fun x ↦
    match x with
    | ⟨l, hl⟩ => ⟨{ toAddHom := ↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂), map_smul' := ⋯ }, ⋯⟩

Tactic:
intro f
    ext x
    simp only [AlgebraTensorModule.curry_apply, Derivation.coe_comp, LinearMap.coe_comp,
      LinearMap.coe_restrictScalars, Derivation.coeFn_coe, Function.comp_apply, curry_apply,
      LinearEquiv.coe_coe, LinearMap.coe_mk, AddHom.coe_coe,
      LinearEquiv.apply_symm_apply, LinearEquiv.symm_apply_apply]

Goal state after:
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
⊢ 0 < q.ramificationIdx R

Tactic:
let p := q.under R

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
⊢ 0 < q.ramificationIdx R
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: S : Type u_1
inst✝⁵ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R S
inst✝² : q.IsPrime
inst✝¹ : Algebra.EssFiniteType R S
inst✝ : Algebra.IsUnramifiedAt R q
⊢ q.ramificationIdx R = 1

Tactic:
let p := q.under R

Goal state after:
S : Type u_1
inst✝⁵ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R S
inst✝² : q.IsPrime
inst✝¹ : Algebra.EssFiniteType R S
inst✝ : Algebra.IsUnramifiedAt R q
p : Ideal R := under R q
⊢ q.ramificationIdx R = 1
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: S : Type u_1
inst✝⁶ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
inst✝³ : q.IsPrime
inst✝² : Algebra.EssFiniteType R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : PerfectField (under R q).ResidueField
h : map (algebraMap R (Localization.AtPrime q)) (under R q) = IsLocalRing.maximalIdeal (Localization.AtPrime q)
⊢ Algebra.IsUnramifiedAt R q

Tactic:
let p := q.under R

Goal state after:
S : Type u_1
inst✝⁶ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
inst✝³ : q.IsPrime
inst✝² : Algebra.EssFiniteType R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : PerfectField (under R q).ResidueField
h : map (algebraMap R (Localization.AtPrime q)) (under R q) = IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal R := under R q
⊢ Algebra.IsUnramifiedAt R q
Module: Mathlib.RingTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsPrime
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this✝ : Fintype (PrimeSpectrum (p.Fiber S)) := Fintype.ofFinite (PrimeSpectrum (p.Fiber S))
q : PrimeSpectrum (p.Fiber S)
a✝ : q ∈ Finset.univ
r : Ideal S := comap Algebra.TensorProduct.includeRight q.asIdeal
this : Algebra (Localization.AtPrime p) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver p r
Rp : Type u_1 := Localization.AtPrime p
Sq : Type (max u_1 u_2) := Localization.AtPrime q.asIdeal
Sr : Type u_2 := Localization.AtPrime r
κp : Type u_1 := p.ResidueField
κr : Type u_2 := r.ResidueField
A : Type u_2 := Sr ⧸ map (algebraMap R Sr) p
⊢ length Sr A * ↑(finrank κp κr) = length Sr A * length κp κr

Tactic:
by rw [length_eq_finrank]

Goal state after:
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

Tactic:
let p := q.under R

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
p : Ideal R := under R q
⊢ (g • q).ramificationIdx R = q.ramificationIdx R
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁴ : CommRing A
I : Ideal A
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
φ : M₁ →ₗ[A] M₂
c : M₁
n : ℕ
hn : ∀ a ∈ I ^ n, a • c = 0
⊢ ∃ n, ∀ a ∈ I ^ n, φ (a • c) = 0

Tactic:
use n

Goal state after:
case h
A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁴ : CommRing A
I : Ideal A
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
φ : M₁ →ₗ[A] M₂
c : M₁
n : ℕ
hn : ∀ a ∈ I ^ n, a • c = 0
⊢ ∀ a ∈ I ^ n, φ (a • c) = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
J : Ideal A
hD : IsCoprime I J
this : ∀ (n : ℕ), Disjoint (torsionBySet A M ↑(I ^ n)) (torsionBySet A M ↑J)
⊢ primaryComponent (↥(torsionBySet A M ↑J)) I = ⊥

Tactic:
apply Submodule.map_injective_of_injective (Submodule.subtype_injective (torsionBySet A M ↑J))

Goal state after:
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
J : Ideal A
hD : IsCoprime I J
this : ∀ (n : ℕ), Disjoint (torsionBySet A M ↑(I ^ n)) (torsionBySet A M ↑J)
⊢ Submodule.map (torsionBySet A M ↑J).subtype (primaryComponent (↥(torsionBySet A M ↑J)) I) =
    Submodule.map (torsionBySet A M ↑J).subtype ⊥
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
⊢ sSup s⁻¹ = (sInf s)⁻¹

Tactic:
rw [← image_inv_eq_inv, sSup_image]
  exact ((OrderIso.inv M).map_sInf _).symm

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: s : Set ℝ≥0
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
rcases Set.eq_empty_or_nonempty s with rfl | hs
  · simp
  by_cases H : BddAbove s
  · have A : sSup (Subtype.val '' s) ∈ Set.Ici 0 := by
      apply Real.sSup_nonneg
      rintro - ⟨y, -, rfl⟩
      exact y.2
    exact (@subset_sSup_of_within ℝ (Set.Ici (0 : ℝ)) _ _ (_) s hs H A).symm
  · simp only [csSup_of_not_bddAbove H, csSup_empty, bot_eq_zero', NNReal.coe_zero]
    apply (Real.sSup_of_not_bddAbove ?_).symm
    contrapose H
    exact bddAbove_coe.1 H

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: a b : ℝ≥0
ha : 0 < a
hb : b < 1
⊢ ∃ n, b ^ n < a

Tactic:
by
  simpa only [← coe_pow, NNReal.coe_lt_coe] using
    exists_pow_lt_of_lt_one (NNReal.coe_pos.2 ha) (NNReal.coe_lt_coe.2 hb)

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_1
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ ↑(const abs (sSup s) - f) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ ↑(const abs (sSup s - ε / 2) - f) j

Tactic:
rw [sub_apply, const_apply, sub_right_comm, le_sub_iff_add_le, add_halves]

Goal state after:
case refine_1
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ ↑(const abs (sSup s) - f) j
j : ℕ
ij : j ≥ i
⊢ ε ≤ sSup s - ↑f j
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: b : ℝ
hb : 0 < b
⊢ ∃ n, 0 < n ∧ (↑n)⁻¹ < b

Tactic:
by
  refine (exists_nat_gt b⁻¹).imp fun k hk ↦ ?_
  have := (inv_pos_of_pos hb).trans hk
  refine ⟨Nat.cast_pos.mp this, ?_⟩
  rwa [inv_lt_comm₀ this hb]

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: x y : ℝ≥0
⊢ ofNNReal '' uIoo x y = uIoo ↑x ↑y

Tactic:
by simp [uIoo]

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
i : ι
⊢ a + f i ≤ a + ⨆ i, f i

Tactic:
grw [← le_iSup]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ x * 1 = x

Tactic:
EReal.mul_comm,

Goal state after:
x : EReal
⊢ 1 * x = x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ x * 0 = 0

Tactic:
EReal.mul_comm,

Goal state after:
x : EReal
⊢ 0 * x = 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ≥0
⊢ ⊤ * ↑↑x = ↑↑x * ↑∞

Tactic:
EReal.mul_comm,

Goal state after:
x : ℝ≥0
⊢ ↑↑x * ⊤ = ↑↑x * ↑∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ a * c / (b * c) = a / b

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ENNReal.mul_inv (Or.inr hc') (Or.inr hc), mul_mul_mul_comm,
    ENNReal.mul_inv_cancel hc hc', mul_one]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ a < b⁻¹ ↔ b < a⁻¹

Tactic:
by
  simpa only [inv_inv] using @ENNReal.inv_lt_inv a⁻¹ b

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ 0
hb : b ≠ ∞
n : ℕ
hn : b / a < ↑n
⊢ b < ↑n * a

Tactic:
rwa [← ENNReal.div_lt_iff (Or.inl ha) (Or.inr hb)]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
⊢ Int.negSucc b < Int.ofNat a

Tactic:
exact lt_of_lt_of_le (Int.negSucc_lt_zero _) (Int.natCast_nonneg _)

Goal state after:
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: α : Type u_3
m : MetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
⊢ m.replaceBornology H = m

Tactic:
by
  ext
  rfl

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : dist x y ≤ ε₂ - ε₁
z : α
zx : z ∈ ball x ε₁
⊢ z ∈ ball y ε₂

Tactic:
← add_sub_cancel ε₁ ε₂

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : dist x y ≤ ε₂ - ε₁
z : α
zx : z ∈ ball x ε₁
⊢ z ∈ ball y (ε₁ + (ε₂ - ε₁))
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u_3
U : UniformSpace α
m : PseudoMetricSpace α
H : 𝓤 α = 𝓤 α
⊢ m.replaceUniformity H = m

Tactic:
by
  ext
  rfl

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: γ : Type u_3
U : TopologicalSpace γ
m : PseudoMetricSpace γ
H : U = toUniformSpace.toTopologicalSpace
⊢ m.replaceTopology H = m

Tactic:
by
  ext
  rfl

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u_3
m : PseudoMetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
⊢ m.replaceBornology H = m

Tactic:
by
  ext
  rfl

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
⊢ a p' ∈ J * ∏ q ∈ s, q.asIdeal

Tactic:
have inst : Nonempty {x // x ∈ s} := ⟨_, hp's⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
⊢ a p' ∈ J * ∏ q ∈ s, q.asIdeal
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : ¬BddAbove (range fun x ↦ f ↑x)
this : ¬BddAbove (range f)
⊢ ⨆ s, f ↑s = ⨆ i, f i

Tactic:
by simp [ciSup_of_not_bddAbove, this, h]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ (𝓝 1).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {y | ‖y‖ < ε}

Tactic:
convert! NormedGroup.nhds_basis_norm_lt (1 : E) using 1

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ (fun ε ↦ {y | ‖y‖ < ε}) = fun ε ↦ {y | ‖y⁻¹ * 1‖ < ε}