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

Goal state before:
pp: case zero
Γ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (PowerSeries.coeff 0) (toPowerSeries.toFun ((algebraMap R A⟦ℕ⟧) r)) =
    (PowerSeries.coeff 0) ((algebraMap R (PowerSeries A)) r)

pp: case succ
Γ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
n✝ : ℕ
⊢ (PowerSeries.coeff (n✝ + 1)) (toPowerSeries.toFun ((algebraMap R A⟦ℕ⟧) r)) =
    (PowerSeries.coeff (n✝ + 1)) ((algebraMap R (PowerSeries A)) r)

Tactic:
<;>

Goal state after:
case zero
Γ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (PowerSeries.coeff 0) (toPowerSeries.toFun ((algebraMap R A⟦ℕ⟧) r)) =
    (PowerSeries.coeff 0) ((algebraMap R (PowerSeries A)) r)

case succ
Γ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
n✝ : ℕ
⊢ (PowerSeries.coeff (n✝ + 1)) (toPowerSeries.toFun ((algebraMap R A⟦ℕ⟧) r)) =
    (PowerSeries.coeff (n✝ + 1)) ((algebraMap R (PowerSeries A)) r)
Module: Mathlib.RingTheory.HahnSeries.Cardinal

Goal state before:
pp: case neg.zero
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h✝ : ¬0 < x.orderTop
⊢ (0 ^ 0).cardSupp ≤ x.cardSupp ^ 0

pp: case neg.succ
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h✝ : ¬0 < x.orderTop
n✝ : ℕ
⊢ (0 ^ (n✝ + 1)).cardSupp ≤ x.cardSupp ^ (n✝ + 1)

Tactic:
<;>

Goal state after:
case neg.zero
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h✝ : ¬0 < x.orderTop
⊢ (0 ^ 0).cardSupp ≤ x.cardSupp ^ 0

case neg.succ
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h✝ : ¬0 < x.orderTop
n✝ : ℕ
⊢ (0 ^ (n✝ + 1)).cardSupp ≤ x.cardSupp ^ (n✝ + 1)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : ¬0 < x.orderTop
x✝ : Γ
⊢ ((powers x) 0).coeff x✝ = ((single 0 1) 0).coeff x✝

pp: case inr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : ¬0 < x.orderTop
a : ℕ
x✝ : Γ
ha : a ≠ 0
⊢ ((powers x) a).coeff x✝ = ((single 0 1) a).coeff x✝

Tactic:
<;>

Goal state after:
case inl
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : ¬0 < x.orderTop
x✝ : Γ
⊢ ((powers x) 0).coeff x✝ = ((single 0 1) 0).coeff x✝

case inr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : ¬0 < x.orderTop
a : ℕ
x✝ : Γ
ha : a ≠ 0
⊢ ((powers x) a).coeff x✝ = ((single 0 1) a).coeff x✝
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : ¬0 < x.orderTop
a : ℕ
x✝ : Γ
⊢ ((powers x) a).coeff x✝ = ((single 0 1) a).coeff x✝

Tactic:
obtain rfl | ha := eq_or_ne a 0 <;> simp [powers, *]

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

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x✝ : Γ
⊢ (0 ^ 0).coeff x✝ = ((single 0 1) 0).coeff x✝

pp: case inr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
n : ℕ
x✝ : Γ
ha : n ≠ 0
⊢ (0 ^ n).coeff x✝ = ((single 0 1) n).coeff x✝

Tactic:
<;>

Goal state after:
case inl
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x✝ : Γ
⊢ (0 ^ 0).coeff x✝ = ((single 0 1) 0).coeff x✝

case inr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
n : ℕ
x✝ : Γ
ha : n ≠ 0
⊢ (0 ^ n).coeff x✝ = ((single 0 1) n).coeff x✝
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
h : u = x.leadingCoeff
h' : (1 - (1 - (single ↑(-hxo.addUnit)) i * x)) * (SummableFamily.powers (1 - (single ↑(-hxo.addUnit)) i * x)).hsum = 1
⊢ IsUnit x

Tactic:
rw [sub_sub_cancel] at h'

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
h : u = x.leadingCoeff
h' : (single ↑(-hxo.addUnit)) i * x * (SummableFamily.powers (1 - (single ↑(-hxo.addUnit)) i * x)).hsum = 1
⊢ IsUnit x
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv (antipode R) * toConv LinearMap.id).ofConv = ofConv 1

pp: case refine_2
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv LinearMap.id * toConv (antipode R)).ofConv = ofConv 1

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv (antipode R) * toConv LinearMap.id).ofConv = ofConv 1

case refine_2
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv LinearMap.id * toConv (antipode R)).ofConv = ofConv 1
Module: Mathlib.RingTheory.Ideal.HasGoingUp

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 : HasGoingUp R S
P : PrimeSpectrum S
q : PrimeSpectrum R
hq : PrimeSpectrum.comap (algebraMap R S) P ⤳ q
⊢ ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' P ∧ PrimeSpectrum.comap (algebraMap R S) a' = q

Tactic:
rw [← PrimeSpectrum.le_iff_specializes] at hq

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 : HasGoingUp R S
P : PrimeSpectrum S
q : PrimeSpectrum R
hq : PrimeSpectrum.comap (algebraMap R S) P ≤ q
⊢ ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' P ∧ PrimeSpectrum.comap (algebraMap R S) a' = q
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] := ⋯
c : ℕ → R := ⋯
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ : i < ((taylor (c n)) f).natDegree + 2
⊢ n + 2 ≤ 2 * (n + 1)

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] := ⋯
c : ℕ → R := ⋯
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ : i < ((taylor (c n)) f).natDegree + 2
⊢ 2 * (n + 1) ≤ i * (n + 1)

Tactic:
<;>

Goal state after:
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] := ⋯
c : ℕ → R := ⋯
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ : i < ((taylor (c n)) f).natDegree + 2
⊢ n + 2 ≤ 2 * (n + 1)

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] := ⋯
c : ℕ → R := ⋯
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ : i < ((taylor (c n)) f).natDegree + 2
⊢ 2 * (n + 1) ≤ i * (n + 1)
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: 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

pp: 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

Tactic:
<;>

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: 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

Tactic:
intro h k hk

Goal state after:
case mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot (L ⊓ K) K
k : A
hk : k ∈ K
⊢ ∃ I ∈ F, I ≤ Submodule.colon L {k}
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: 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

Tactic:
intro h k hk

Goal state after:
case mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot L K
k : A
hk : k ∈ K
⊢ ∃ I ∈ F, I ≤ Submodule.colon (L ⊓ K) {k}
Module: Mathlib.RingTheory.IdealFilter.Basic

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

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

Tactic:
<;>

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.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : n = 0
⊢ 1 = ⟨n + 1, ⋯⟩

Tactic:
h0,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : n = 0
⊢ 1 = ⟨0 + 1, ⋯⟩
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: 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
x : M
hp : (N.colon {x}).radical.IsPrime
⊢ (N.colon {x}).radical ∈ (fun J ↦ (J.colon Set.univ).radical) '' ↑t

Tactic:
rw [h] at hp ⊢

Goal state after:
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
x : M
hp : ({x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical).IsPrime
⊢ ({x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical) ∈ (fun J ↦ (J.colon Set.univ).radical) '' ↑t
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:
by
  constructor
  intro x
  obtain ⟨N, hN⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
    (stabilizer_isOpen G x) (one_mem _)
  have := (Algebra.IsInvariant.isIntegral A (FixedPoints.subalgebra A B N.1.1) (G ⧸ N.1.1)).1
    ⟨x, fun g ↦ hN g.2⟩
  exact this.map (FixedPoints.subalgebra A B N.1.1).val

Goal state after:
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
⊢ IsLocalIso R T

Tactic:
let s : Set S := {g : S | IsStandardOpenImmersion R (Localization.Away g)}
  let T' (g : S) := Localization.Away (algebraMap S T g)
  let (g : S) : Algebra (Localization.Away g) (T' g) := localizationAlgebra (.powers g) T
  let T'' (g : S) (x : T) := Localization.Away (algebraMap _ (T' g) x)
  let t (g : S) : Set T := {x : T | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
  let ι : Type _ := Σ i : s, t i.1
  have (i : ι) : IsStandardOpenImmersion (Localization.Away i.1.1) (T'' i.1 i.2) := i.2.2
  suffices h : Ideal.span (Set.range fun i : ι ↦ algebraMap S T i.1 * i.2) = ⊤ by
    have (i : ι) : IsStandardOpenImmersion R (T'' i.1 i.2) :=
      have : IsScalarTower R (Localization.Away i.1.1) (T' i.1.1) :=
        IsScalarTower.to₁₃₄ _ S _ _
      have : IsStandardOpenImmersion (Localization.Away i.1.1) (T'' i.1.1 i.2.1) := i.2.2
      have : IsStandardOpenImmersion R (Localization.Away i.1.1) := i.1.2
      .trans _ (Localization.Away i.1.1) _
    exact .of_span_range_eq_top _ h fun i : ι ↦ T'' i.1 i.2
  have h1 := congr(Ideal.map (algebraMap S T) $(span_isStandardOpenImmersion_eq_top R S))
  rw [Ideal.map_top, Ideal.map_span] at h1
  nth_rw 1 [_root_.eq_top_iff, ← Ideal.top_mul ⊤, ← h1, ← span_isStandardOpenImmersion_eq_top S T,
    Ideal.span_mul_span, Ideal.span_le, Set.mul_subset_iff]
  simp only [Set.mem_image, Set.mem_ofPred_eq, SetLike.mem_coe, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂]
  intro g hg x hx
  refine Ideal.subset_span ⟨⟨⟨g, hg⟩, ⟨x, ?_⟩⟩, rfl⟩
  simp only [Set.mem_ofPred_eq, t]
  let : Algebra (Localization.Away x) (T'' g x) :=
    localizationAlgebra (.powers x) (T' g)
  have : IsScalarTower S (Localization.Away x) (T'' g x) :=
    IsScalarTower.to₁₃₄ _ T _ _
  have : IsLocalization (algebraMapSubmonoid (Localization.Away x) (.powers g)) (T'' g x) := by
    have : algebraMapSubmonoid (Localization.Away x) (.powers g) =
      algebraMapSubmonoid (Localization.Away x) (.powers (algebraMap S T g)) := by
        simp [IsScalarTower.algebraMap_apply S T (Localization.Away x)]
    rw [this]
    exact .commutes _ (T' g) _ (.powers x) (.powers (algebraMap S T g))
  have : IsPushout S (Localization.Away x) (Localization.Away g) (T'' g x) :=
    Algebra.isPushout_of_isLocalization (.powers g) _ _ _
  exact .of_isPushout S (Localization.Away x) _ _

Goal state after:
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: case isTrue
ι : Type u_1
inst✝² : Nontrivial ι
R : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit fun i ↦ if i = i₁ then 0 else 1
hb : ¬IsUnit fun i ↦ if i = i₁ then 1 else 0
x✝ : ι
h✝ : x✝ = i₁
⊢ 0 + 1 = 1

pp: case isFalse
ι : Type u_1
inst✝² : Nontrivial ι
R : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit fun i ↦ if i = i₁ then 0 else 1
hb : ¬IsUnit fun i ↦ if i = i₁ then 1 else 0
x✝ : ι
h✝ : ¬x✝ = i₁
⊢ 1 + 0 = 1

Tactic:
<;>

Goal state after:
case isTrue
ι : Type u_1
inst✝² : Nontrivial ι
R : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit fun i ↦ if i = i₁ then 0 else 1
hb : ¬IsUnit fun i ↦ if i = i₁ then 1 else 0
x✝ : ι
h✝ : x✝ = i₁
⊢ 0 + 1 = 1

case isFalse
ι : Type u_1
inst✝² : Nontrivial ι
R : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit fun i ↦ if i = i₁ then 0 else 1
hb : ¬IsUnit fun i ↦ if i = i₁ then 1 else 0
x✝ : ι
h✝ : ¬x✝ = i₁
⊢ 1 + 0 = 1
Module: Mathlib.RingTheory.LocalRing.Subring

Goal state before:
pp: case refine_1
R : Type u_2
S : Type u_1
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : IsLocalRing S
f : R →+* S
hf : Function.Injective ⇑f
h : ∀ a ∈ R⁰, IsUnit a
this : Nontrivial R
a b : R
hab : a + b = 1
⊢ IsUnit (f a) → IsUnit a

pp: case refine_2
R : Type u_2
S : Type u_1
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : IsLocalRing S
f : R →+* S
hf : Function.Injective ⇑f
h : ∀ a ∈ R⁰, IsUnit a
this : Nontrivial R
a b : R
hab : a + b = 1
⊢ IsUnit (f b) → IsUnit b

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_2
S : Type u_1
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : IsLocalRing S
f : R →+* S
hf : Function.Injective ⇑f
h : ∀ a ∈ R⁰, IsUnit a
this : Nontrivial R
a b : R
hab : a + b = 1
⊢ IsUnit (f a) → IsUnit a

case refine_2
R : Type u_2
S : Type u_1
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : IsLocalRing S
f : R →+* S
hf : Function.Injective ⇑f
h : ∀ a ∈ R⁰, IsUnit a
this : Nontrivial R
a b : R
hab : a + b = 1
⊢ IsUnit (f b) → IsUnit b
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := max ℓ D
⊢ ∀ i < D, (⋂ n, ⋂ (_ : n < ℓ), φ n) ∩ ⋂ n, ⋂ (_ : ℓ ≤ n ∧ n ≤ N), φ n ⊆ φ i

Tactic:
intro i hi x hx

Goal state after:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := max ℓ D
i : ℤ
hi : i < D
x : K⸨X⸩
hx : x ∈ (⋂ n, ⋂ (_ : n < ℓ), φ n) ∩ ⋂ n, ⋂ (_ : ℓ ≤ n ∧ n ≤ N), φ n
⊢ x ∈ φ i
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
r : R
t s : Fin n →₀ ℕ
⊢ esymmAlgHomMonomial σ (t + s) r = esymmAlgHomMonomial σ t r * esymmAlgHomMonomial σ s 1

Tactic:
by
  simp_rw [esymmAlgHomMonomial, esymmAlgHom_apply, ← map_mul, monomial_mul, mul_one]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ

pp: case neg
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ

Tactic:
· set η : ℤᵐ⁰ˣ := Units.mk0 (exp f.order) coe_ne_zero
      with hη
    obtain ⟨P, hP⟩ := exists_Polynomial_intValuation_lt F (η * γ)
    use RatFunc.X ^ f.order * (P : K⟮X⟯)
    have F_mul := f.ofPowerSeries_powerSeriesPart
    obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (le_of_lt ord_nonpos)
    rw [← hF, hs, neg_neg, ← ofPowerSeries_X_pow s, ← inv_mul_eq_iff_eq_mul₀] at F_mul
    · have : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1 := by exact algebraMap.coe_one
      rw [hs, ← F_mul, PowerSeries.coe_pow, PowerSeries.coe_X, map_mul, zpow_neg,
        zpow_natCast, inv_eq_one_div (RatFunc.X ^ s), map_div₀, map_pow,
        RatFunc.coe_X]
      simp only [map_one]
      rw [← inv_eq_one_div, ← mul_sub, map_mul, map_inv₀,
        ← PowerSeries.coe_X, valuation_X_pow, ← hs, ← RatFunc.coe_coe, ← PowerSeries.coe_sub,
        ← coe_algebraMap, adicValued_apply, valuation_of_algebraMap,
        ← Units.val_mk0 (a := exp f.order) exp_ne_zero, ← hη]
      apply inv_mul_lt_of_lt_mul₀
      rwa [← Units.val_mul]
    · simp

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ