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 g : R⟦σ →₀ ℕ⟧
⊢ (f + g).coeff = f.coeff + g.coeff

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K[X]
x✝¹ : f.Monic
a₀ : K
h₁ : Polynomial.eval a₀ f ∈ maximalIdeal K
x✝ : IsUnit (Polynomial.eval a₀ (derivative f))
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal K

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 : A
ha : IsGroupLikeElem R a
⊢ (antipode R) a * a = 1

Tactic:
by

Goal state after:
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 : A
ha : IsGroupLikeElem R a
⊢ a * (antipode R) a = 1

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero S
x : R⟦Γ⟧
y : S⟦Γ⟧
h : x.support = y.support
⊢ x.cardSupp = y.cardSupp

Tactic:
by

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
⊢ cardSupp 0 = 0

Tactic:
by

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ ((single a) r).cardSupp = 1

Tactic:
by

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x : R⟦Γ⟧
a : Γ
r : R
⊢ ((single a) r * x).cardSupp ≤ x.cardSupp

Tactic:
by

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x : R⟦Γ⟧
a : Γ
r : R
⊢ (x * (single a) r).cardSupp ≤ x.cardSupp

Tactic:
by

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
⊢ (x ^ n).cardSupp ≤ x.cardSupp ^ n

Tactic:
by

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
⊢ (SummableFamily.powers x).hsum.cardSupp ≤ max ℵ₀ x.cardSupp

Tactic:
by

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommGroup Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
x : R⟦Γ⟧
⊢ x⁻¹.cardSupp ≤ max ℵ₀ x.cardSupp

Tactic:
by

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
S : Type u_3
α : Type u_4
κ : Cardinal.{u_1}
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
hκ : Fact (ℵ₀ ≤ κ)
⊢ 0 ∈ {x | x.cardSupp < κ}

Tactic:
by

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

Goal state before:
pp: case pos.refine_2
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite
⊢ {a | ((fun n ↦ x ^ n) a).coeff y ≠ 0} ⊆
    (Nat.succ '' ⋃ i ∈ ↑(antidiagonal ⋯ hpwo y), {a | ((fun n ↦ x ^ n) a).coeff i.2 ≠ 0}) ∪ {0}

Tactic:
rintro (_ | n) hn
    · exact Set.mem_union_right _ (Set.mem_singleton 0)
    · obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset hn
      refine Set.mem_union_left _ ⟨n, Set.mem_iUnion.2 ⟨⟨j, i⟩, Set.mem_iUnion.2 ⟨?_, hi⟩⟩, rfl⟩
      simp only [mem_coe, mem_antidiagonal, mem_support, ne_eq, Set.mem_iUnion]
      exact ⟨hj, ⟨n, hi⟩, add_comm j i⟩

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
S : Type u_3
α : Type u_4
κ : Cardinal.{u_1}
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
hκ : Fact (ℵ₀ ≤ κ)
⊢ ∀ {x : R⟦Γ⟧}, x ∈ (cardSuppLTAddSubmonoid Γ R κ).carrier → -x ∈ (cardSuppLTAddSubmonoid Γ R κ).carrier

Tactic:
by

Goal state after:
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
g : Γ
⊢ {a | ((fun n ↦ x ^ n) a).coeff g ≠ 0}.Finite

Tactic:
by

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
S : Type u_3
α : Type u_4
κ : Cardinal.{u_1}
inst✝³ : LinearOrder Γ
inst✝² : AddCommGroup Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
hκ : Fact (ℵ₀ < κ)
x✝¹ : R⟦Γ⟧
x✝ :
  x✝¹ ∈
    (have this := ⋯;
      cardSuppLTSubring Γ R κ).carrier
⊢ max ℵ₀ x✝¹.cardSupp < κ

Tactic:
by

Goal state after:
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✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
⊢ (⋃ a, ((if 0 < x.orderTop then x else 0) ^ a).support).IsPWO

Tactic:
by

Goal state after:
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✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
g : Γ
⊢ {a | ((if 0 < x.orderTop then x else 0) ^ a).coeff g ≠ 0}.Finite

Tactic:
by

Goal state after:
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
n : ℕ
⊢ (powers x) n = x ^ n

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ powers x = single 0 1

Tactic:
by

Goal state after:
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
n : ℕ
x✝ : Γ
⊢ 0 < orderTop 0

Tactic:
by

Goal state after:
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
⊢ powers 0 = single 0 1

Tactic:
by

Goal state after:
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
⊢ ⇑(powers x) = HPow.hPow x

Tactic:
by

Goal state after:
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
⊢ (x • powers x).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } = powers x - ofFinsupp (Finsupp.single 0 1)

Tactic:
by

Goal state after:
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
⊢ (1 - x) * (powers x).hsum = 1

Tactic:
by

Goal state after:
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₀
tfae_2_to_1 :
  (∀ (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₀) →
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective ⇑φ
f : R[X]
hf : f.Monic
a₀ : R
H : φ (Polynomial.eval a₀ f) = 0 → IsUnit (Polynomial.eval a₀ (derivative f)) → ∃ a, f.IsRoot a ∧ φ (a - a₀) = 0
h₁ : φ (Polynomial.eval a₀ f) = 0
h₂ : φ (Polynomial.eval a₀ (derivative f)) ≠ 0
⊢ IsUnit (Polynomial.eval a₀ (derivative f))

Tactic:
by

Goal state after:
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 y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = y + (single x.order) x.leadingCoeff
oinv : Γ
hxo : oinv + x.order = 0
⊢ 1 - (single oinv) r * x = -((single oinv) r * y)

Tactic:
by

Goal state after:
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⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := x - (single x.order) x.leadingCoeff
hy : y = 0
⊢ (single oinv) r * x = 1

Tactic:
by

Goal state after:
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₀
tfae_2_to_1 :
  (∀ (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₀) →
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective ⇑φ
f : R[X]
hf : f.Monic
a₀ : K
h₁ : eval₂ φ a₀ f = 0
h₂ : eval₂ φ a₀ (derivative f) ≠ 0
⊢ ∃ a, f.IsRoot a ∧ φ a = a₀

Tactic:
by

Goal state after:
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⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
⊢ 0 < ((single oinv) r * y).order

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
⊢ [HenselianLocalRing R,
      ∀ (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₀,
      ∀ {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₀].TFAE

Tactic:
by

Goal state after:
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⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
⊢ 0 < (1 - (single oinv) r * x).orderTop

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
⊢ maximalIdeal R ≤ ⊥.jacobson

Tactic:
by

Goal state after:
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
⊢ IsUnit x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : HenselianLocalRing R
⊢ ∀ (f : R[X]),
    f.Monic →
      ∀ (a₀ : R),
        Polynomial.eval a₀ f ∈ maximalIdeal R →
          IsUnit ((Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f))) →
            ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal R

Tactic:
by

Goal state after:
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⟦Γ⟧
h : 0 < (x - 1).orderTop
⊢ IsUnit x

Tactic:
by

Goal state after:
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:
by

Goal state after:
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')⁻¹ʳ
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ I

Tactic:
have hc : ∀ n, c (n + 1) = c n - f.eval (c n) * (f'.eval (c n))⁻¹ʳ := by
        intro n
        simp only [c]

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] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ I
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case mp.hc
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
⊢ u.order + i.order = 0

Tactic:
rw [← order_mul (left_ne_zero_of_mul_eq_one ui) (right_ne_zero_of_mul_eq_one ui), ui, order_one]

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

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✝ : Field R
a : Γ
r : R
⊢ ((single a) r)⁻¹ = (single (-a)) r⁻¹

Tactic:
by

Goal state after:
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')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
⊢ ∀ (n : ℕ), c n ≡ a₀ [SMOD I]

Tactic:
by

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✝ : Field R
a b : Γ
r s : R
⊢ (single a) r / (single b) s = (single (a - b)) (r / s)

Tactic:
by

Goal state after:
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')⁻¹ʳ
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]
⊢ ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')

Tactic:
by

Goal state after:
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
x : R⟦Γ⟧
x0 : x ≠ 0
⊢ x * x⁻¹ = 1

Tactic:
by

Goal state after:
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
⊢ 0⁻¹ = 0

Tactic:
by

Goal state after:
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
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: 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
g : A →ₐ[R] B
⊢ g.toLinearMap ∘ₗ ofConv 1 = ofConv 1

Tactic:
by

Goal state after:
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:
by

Goal state after:
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 : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

Goal state after:
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:
by

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✝ : Field R
m : ℕ
e : Bool
s : ℕ
⊢ (single 0) (OfScientific.ofScientific m e s) = OfScientific.ofScientific m e s

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : HopfAlgebra R A
G : Type u_3
inst✝ : Group G
g : G
a : A
⊢ (antipode R) (single g a) = single g⁻¹ ((antipode R) a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: 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
g : A →ₗc[R] B
⊢ ofConv 1 ∘ₗ g.toLinearMap = ofConv 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : HopfAlgebra R A
G : Type u_3
inst✝ : Group G
⊢ LinearMap.mul' R A[G] ∘ₗ LinearMap.rTensor A[G] (antipode R) ∘ₗ comul = Algebra.linearMap R A[G] ∘ₗ counit

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_3
p : ι → Submodule R M
I : Ideal R
⊢ (submodule fun i ↦ I • p i) = I • submodule p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra.HasGoingUp R S
p q : Ideal R
inst✝² : q.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hle : p ≤ q
⊢ ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra.HasGoingUp R S
p q : Ideal R
inst✝² : q.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hpq : p < q
⊢ ∃ Q, P < Q ∧ Q.IsPrime ∧ Q.LiesOver q

Tactic:
by

Goal state after: