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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f : R⟦σ →₀ ℕ⟧
⊢ (fun f ↦ { coeff := f, isPWO_support' := ⋯ }) ((fun f ↦ f.coeff) f) = f

Tactic:
ext

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f : R⟦σ →₀ ℕ⟧
x✝ : σ →₀ ℕ
⊢ ((fun f ↦ { coeff := f, isPWO_support' := ⋯ }) ((fun f ↦ f.coeff) f)).coeff x✝ = f.coeff x✝
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f : MvPowerSeries σ R
⊢ (fun f ↦ f.coeff) ((fun f ↦ { coeff := f, isPWO_support' := ⋯ }) f) = f

Tactic:
ext

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f : MvPowerSeries σ R
n✝ : σ →₀ ℕ
⊢ (MvPowerSeries.coeff n✝) ((fun f ↦ f.coeff) ((fun f ↦ { coeff := f, isPWO_support' := ⋯ }) f)) =
    (MvPowerSeries.coeff n✝) f
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f g : R⟦σ →₀ ℕ⟧
⊢ (f + g).coeff = f.coeff + g.coeff

Tactic:
ext

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f g : R⟦σ →₀ ℕ⟧
n✝ : σ →₀ ℕ
⊢ (MvPowerSeries.coeff n✝) (f + g).coeff = (MvPowerSeries.coeff n✝) (f.coeff + g.coeff)
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
⊢ IsLocalHom (Ideal.Quotient.mk I)

Tactic:
constructor

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≤ ⊥.jacobson
⊢ ∀ (a : R), IsUnit ((Ideal.Quotient.mk I) a) → IsUnit a
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
x✝ :
  ∀ (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
H : ∀ (f : R[X]),
  f.Monic →
    ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀ :=
  x✝
⊢ HenselianLocalRing R

Tactic:
constructor

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
x✝ :
  ∀ (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
H : ∀ (f : R[X]),
  f.Monic →
    ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀ :=
  x✝
⊢ ∀ (f : R[X]),
    f.Monic →
      ∀ (a₀ : R),
        Polynomial.eval a₀ f ∈ maximalIdeal R →
          IsUnit (Polynomial.eval a₀ (derivative f)) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal R
Module: Mathlib.RingTheory.HopfAlgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ { val := ↑1, inv := (antipode R) ↑1, val_inv := ⋯, inv_val := ⋯ } = 1

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ ↑{ val := ↑1, inv := (antipode R) ↑1, val_inv := ⋯, inv_val := ⋯ } = ↑1
Module: Mathlib.RingTheory.HopfAlgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a✝ b✝ : A
a b : GroupLike R A
⊢ { val := ↑(a * b), inv := (antipode R) ↑(a * b), val_inv := ⋯, inv_val := ⋯ } =
    { val := ↑a, inv := (antipode R) ↑a, val_inv := ⋯, inv_val := ⋯ } *
      { val := ↑b, inv := (antipode R) ↑b, val_inv := ⋯, inv_val := ⋯ }

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a✝ b✝ : A
a b : GroupLike R A
⊢ ↑{ val := ↑(a * b), inv := (antipode R) ↑(a * b), val_inv := ⋯, inv_val := ⋯ } =
    ↑({ val := ↑a, inv := (antipode R) ↑a, val_inv := ⋯, inv_val := ⋯ } *
        { val := ↑b, inv := (antipode R) ↑b, val_inv := ⋯, inv_val := ⋯ })
Module: Mathlib.RingTheory.HopfAlgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a✝ b : A
a : GroupLike R A
⊢ a⁻¹ * a = 1

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a✝ b : A
a : GroupLike R A
⊢ ↑(a⁻¹ * a) = ↑1
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
n : ℕ
⊢ c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ

Tactic:
simp only [c]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R⟦Γ⟧
⊢ IsUnit x ↔ IsUnit x.leadingCoeff

Tactic:
constructor

Goal state after:
case mp
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R⟦Γ⟧
⊢ IsUnit x → IsUnit x.leadingCoeff

case mpr
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R⟦Γ⟧
⊢ IsUnit x.leadingCoeff → IsUnit x
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
q : ℚ≥0
x : R⟦Γ⟧
⊢ q • x = ↑q * x

Tactic:
ext

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
q : ℚ≥0
x : R⟦Γ⟧
x✝ : Γ
⊢ (q • x).coeff x✝ = (↑q * x).coeff x✝
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
q : ℚ
x : R⟦Γ⟧
⊢ q • x = ↑q * x

Tactic:
ext

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
q : ℚ
x : R⟦Γ⟧
x✝ : Γ
⊢ (q • x).coeff x✝ = (↑q * x).coeff x✝
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : HopfAlgebraStruct R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Ideal.IsHopfIdeal R I
⊢ antipode R ∘ₗ (mkₐ R I).toLinearMap = (mkₐ R I).toLinearMap ∘ₗ antipode R

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : HopfAlgebraStruct R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Ideal.IsHopfIdeal R I
x✝ : A
⊢ (antipode R ∘ₗ (mkₐ R I).toLinearMap) x✝ = ((mkₐ R I).toLinearMap ∘ₗ antipode R) x✝
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
⊢ F.IsTorsionQuot (L ⊓ K) K ↔ F.IsTorsionQuot L K

Tactic:
constructor

Goal state after:
case mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
⊢ F.IsTorsionQuot (L ⊓ K) K → F.IsTorsionQuot L K

case mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
⊢ F.IsTorsionQuot L K → F.IsTorsionQuot (L ⊓ K) K
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
⊢ F.IsGabriel ↔ F.IsUniform ∧ F • F = F

Tactic:
constructor

Goal state after:
case mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
⊢ F.IsGabriel → F.IsUniform ∧ F • F = F

case mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
⊢ F.IsUniform ∧ F • F = F → F.IsGabriel
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
hF : F.IsGabriel
I : Ideal A
⊢ I ∈ ↑(F • F) ↔ I ∈ ↑F

Tactic:
constructor

Goal state after:
case mp.mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
hF : F.IsGabriel
I : Ideal A
⊢ I ∈ ↑(F • F) → I ∈ ↑F

case mp.mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
hF : F.IsGabriel
I : Ideal A
⊢ I ∈ ↑F → I ∈ ↑(F • F)
Module: Mathlib.RingTheory.IdealFilter.Topology

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
⊢ s ∈ 𝓝 a ↔ ∃ I ∈ F, a +ᵥ idealSet I ⊆ s

Tactic:
constructor

Goal state after:
case mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
⊢ s ∈ 𝓝 a → ∃ I ∈ F, a +ᵥ idealSet I ⊆ s

case mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
a : WithIdealFilter F
s : Set (WithIdealFilter F)
⊢ (∃ I ∈ F, a +ᵥ idealSet I ⊆ s) → s ∈ 𝓝 a
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
⊢ F.IsGabriel ↔ F.IsUniform ∧ F • F = F

Tactic:
constructor
  · intro hF
    refine ⟨hF.toIsUniform, ?_⟩
    ext I
    constructor <;> intro hI
    · rcases hI with ⟨J, hJ, htors⟩
      refine hF.gabriel_closed I ⟨J, hJ, fun x hx ↦ ?_⟩
      rcases htors x hx with ⟨K, hK, hincl⟩
      exact Order.PFilter.mem_of_le hincl hK
    · exact ⟨I, hI, isTorsionQuot_self F I⟩
  · rintro ⟨h₁, h₂⟩
    refine { toIsUniform := h₁, gabriel_closed := ?_ }
    rintro I ⟨J, hJ, hcolon⟩
    exact h₂.le ⟨J, hJ, fun x hx ↦ ⟨I.colon {x}, hcolon x hx, by simp⟩⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
f : ↥J ⧸ I • ⊤ →ₗ[R] R ⧸ I := (I • ⊤).mapQ I (Submodule.subtype J) ⋯
⊢ LinearMap.lTensor (R ⧸ I) (Submodule.subtype J) =
    ↑(TensorProduct.rid R (R ⧸ I)).symm ∘ₗ f ∘ₗ ↑(quotTensorEquivQuotSMul (↥J) I)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
f : ↥J ⧸ I • ⊤ →ₗ[R] R ⧸ I := (I • ⊤).mapQ I (Submodule.subtype J) ⋯
x✝ : ↥J
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) ∘ₗ Submodule.mkQ I) 1) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.rid R (R ⧸ I)).symm ∘ₗ f ∘ₗ ↑(quotTensorEquivQuotSMul (↥J) I)) ∘ₗ
          Submodule.mkQ I)
        1)
      x✝
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
hx' : ¬IsUnit x
⊢ (span {x}).height ≤ 1

Tactic:
by
  obtain ⟨p, hp⟩ := (span {x}).nonempty_minimalPrimes (by simpa)
  refine le_trans (height_mono hp.1.2) ?_
  exact Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes (span {x}) _ hp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
w✝ : IsLocalRing R
this✝ : (maximalIdeal R).IsPrime
q : Ideal R
hq✝ : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : maximalIdeal R ∈ (span ↑(insert x s')).minimalPrimes
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : ↑s' ⊆ ↑(q ⊔ span {x}).radical
t✝ : ↑↑s' → R
ht : Set.range t✝ ⊆ ↑q
hspan : ↑s' ⊆ ↑(span (Set.range t✝) ⊔ span {x}).radical
t : Finset R := Finset.image t✝ Finset.univ
hq : q ∈ (span ↑t).minimalPrimes
tcard : t.card ≤ n
⊢ ↑t.card ≤ ↑n

Tactic:
by norm_cast

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ ↑(IsLocalRing.maximalIdeal R).height ≠ ⊥ ∧ ↑(IsLocalRing.maximalIdeal R).height ≠ ⊤

Tactic:
constructor

Goal state after:
case left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ ↑(IsLocalRing.maximalIdeal R).height ≠ ⊥

case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ ↑(IsLocalRing.maximalIdeal R).height ≠ ⊤
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ∞
⊢ p.height ≤ n ↔ ∃ I, p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ ↑n

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ∞
⊢ p.height ≤ n → ∃ I, p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ ↑n

case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ∞
⊢ (∃ I, p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ ↑n) → p.height ≤ n
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
⊢ P.height = p.height + 1

Tactic:
by
  have : p.IsPrime := by rw [P.over_def p]; infer_instance
  let Rₚ := Localization.AtPrime p
  set p' : Ideal Rₚ := p.map (algebraMap R Rₚ) with p'_def
  have : p'.IsMaximal := by
    rw [p'_def, Localization.AtPrime.map_eq_maximalIdeal]
    exact IsLocalRing.maximalIdeal.isMaximal Rₚ
  let P' : Ideal Rₚ[X] := P.map (algebraMap R[X] Rₚ[X])
  have disj : Disjoint (p.primeCompl.map C : Set R[X]) P := by
    refine Set.disjoint_left.mpr fun a ⟨b, hb⟩ ha ↦ hb.1 ?_
    rwa [SetLike.mem_coe, LiesOver.over (P := P) (p := p), mem_comap, algebraMap_eq, hb.2]
  have eq := under_map_of_isPrime_disjoint _ Rₚ[X] ‹P.IsMaximal›.isPrime disj
  have : (P'.under R[X]).IsMaximal := eq.symm ▸ ‹P.IsMaximal›
  have : P'.IsMaximal := .of_isLocalization_of_disjoint (p.primeCompl.map C)
  have : P'.LiesOver p' := liesOver_of_isPrime_of_disjoint p.primeCompl _ _ disj
  have eq1 : p.height = p'.height := by
    rw [height_map_of_disjoint p.primeCompl]
    exact Disjoint.symm <| Set.disjoint_left.mpr fun _ a b ↦ b a
  have eq2 : P.height = P'.height := by
    rw [height_map_of_disjoint (Submonoid.map C <| p.primeCompl) _ disj]
  rw [eq1, eq2]
  apply height_eq_height_add_one_of_isMaximal p' P'

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
⊢ (Finset.image (fun t ↦ t.inf id)
          (Finset.image (fun J ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s)).inf
      id =
    N

Tactic:
ext

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
x✝ : M
⊢ x✝ ∈
      (Finset.image (fun t ↦ t.inf id)
            (Finset.image (fun J ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s)).inf
        id ↔
    x✝ ∈ N
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
J : Submodule R M
hJ : J ∈ s
⊢ ∀ ⦃y : Submodule R M⦄, y ∈ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical} → (id y).IsPrimary

Tactic:
simp only [Finset.mem_filter, id_eq, and_imp]
      intro y hy
      simp [hs' hy]

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
p : Ideal R
⊢ p ∈ (fun J ↦ (J.colon Set.univ).radical) '' ↑t ↔ p ∈ N.associatedPrimes

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
p : Ideal R
⊢ p ∈ (fun J ↦ (J.colon Set.univ).radical) '' ↑t → p ∈ N.associatedPrimes

case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
p : Ideal R
⊢ p ∈ N.associatedPrimes → p ∈ (fun J ↦ (J.colon Set.univ).radical) '' ↑t
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case neg
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
hy2 : y ∈ S
x : M
⊢ (mkLinearMap S M) x ∈ localized₀ S (mkLinearMap S M) q

Tactic:
simp_rw [mem_localized₀, IsLocalizedModule.mk'_eq_iff, ← LinearMap.map_smul_of_tower]

Goal state after:
case neg
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
hy2 : y ∈ S
x : M
⊢ ∃ m ∈ q, ∃ s, (mkLinearMap S M) m = (mkLinearMap S M) (s • x)
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u
inst✝¹⁰ : Group G
inst✝⁹ : MulSemiringAction G B
inst✝⁸ : SMulCommClass G A B
inst✝⁷ : TopologicalSpace G
inst✝⁶ : CompactSpace G
inst✝⁵ : TotallyDisconnectedSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : TopologicalSpace B
inst✝² : DiscreteTopology B
inst✝¹ : ContinuousSMul G B
inst✝ : IsInvariant A B G
⊢ Algebra.IsIntegral A B

Tactic:
constructor

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u
inst✝¹⁰ : Group G
inst✝⁹ : MulSemiringAction G B
inst✝⁸ : SMulCommClass G A B
inst✝⁷ : TopologicalSpace G
inst✝⁶ : CompactSpace G
inst✝⁵ : TotallyDisconnectedSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : TopologicalSpace B
inst✝² : DiscreteTopology B
inst✝¹ : ContinuousSMul G B
inst✝ : IsInvariant A B G
⊢ ∀ (x : B), IsIntegral A x
Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
a : ↥S
g' : R →ₗ[R] M
e :
  ↑a • g =
    (mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
      ((LinearMap.lcomp R M I.subtype) g', a).1
⊢ ↑R
        ((algebraMap R Rₛ) 1 •
          (LinearMap.lcomp Rₛ Mₛ (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I).subtype)
            ((mapExtendScalars S (Algebra.linearMap R Rₛ) f Rₛ) g')) ∘ₗ
      Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I =
    ↑R
        ((mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
          ((LinearMap.lcomp R M I.subtype) g')) ∘ₗ
      Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I

Tactic:
ext

Goal state after:
R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
a : ↥S
g' : R →ₗ[R] M
e :
  ↑a • g =
    (mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
      ((LinearMap.lcomp R M I.subtype) g', a).1
x✝ : ↥I
⊢ (↑R
          ((algebraMap R Rₛ) 1 •
            (LinearMap.lcomp Rₛ Mₛ (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I).subtype)
              ((mapExtendScalars S (Algebra.linearMap R Rₛ) f Rₛ) g')) ∘ₗ
        Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I)
      x✝ =
    (↑R
          ((mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
            ((LinearMap.lcomp R M I.subtype) g')) ∘ₗ
        Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I)
      x✝