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

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d e : ℕ
⊢ invOneSubPow S (d + e) = invOneSubPow S d * invOneSubPow S e

Tactic:
[

Goal state after:
S : Type u_1
inst✝ : CommRing S
d e : ℕ
⊢ invOneSubPow S (d + e) = invOneSubPow S d * invOneSubPow S e
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
aux₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
aux₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
aux₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
aux₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
⊢ (∀ (x : α), g ∉ (s x).support) → ∑ᶠ (i : α), (s i).coeff g = 0

Tactic:
[

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
⊢ (∀ (x : α), g ∉ (s x).support) → ∑ᶠ (i : α), (s i).coeff g = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
aux₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
aux₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
subst_mul aux₂,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
aux₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
aux₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
this :
  ∀ (g₁ g₂ : MvPowerSeries (Fin 3) R),
    ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] = fun i ↦ (MvPowerSeries.map f) (![g₁, g₂] i)
⊢ subst ![subst ![X 0, X 1] ((MvPowerSeries.map f) F.toPowerSeries), X 2] ((MvPowerSeries.map f) F.toPowerSeries) =
    subst ![X 0, subst ![X 1, X 2] ((MvPowerSeries.map f) F.toPowerSeries)] ((MvPowerSeries.map f) F.toPowerSeries)

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
f : R →+* S
this :
  ∀ (g₁ g₂ : MvPowerSeries (Fin 3) R),
    ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] = fun i ↦ (MvPowerSeries.map f) (![g₁, g₂] i)
⊢ subst ![subst ![X 0, X 1] ((MvPowerSeries.map f) F.toPowerSeries), X 2] ((MvPowerSeries.map f) F.toPowerSeries) =
    subst ![X 0, subst ![X 1, X 2] ((MvPowerSeries.map f) F.toPowerSeries)] ((MvPowerSeries.map f) F.toPowerSeries)
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✝¹ : PartialOrder Γ
inst✝ : AddCommGroup R
s✝ t : SummableFamily Γ R α
a : α
s : SummableFamily Γ R α
⊢ (⋃ a, (-s a).support).IsPWO

Tactic:
[

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommGroup R
s✝ t : SummableFamily Γ R α
a : α
s : SummableFamily Γ R α
⊢ (⋃ a, (-s a).support).IsPWO
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✝¹ : PartialOrder Γ
inst✝ : AddCommGroup R
s✝ t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
⊢ (⋃ a, ((⇑s - ⇑s') a).support).IsPWO

Tactic:
[

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommGroup R
s✝ t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
⊢ (⋃ a, ((⇑s - ⇑s') a).support).IsPWO
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✝¹ : PartialOrder Γ
inst✝ : AddCommGroup R
s✝ t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
g : Γ
⊢ {a | ((⇑s - ⇑s') a).coeff g ≠ 0}.Finite

Tactic:
[

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommGroup R
s✝ t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
g : Γ
⊢ {a | ((⇑s - ⇑s') a).coeff g ≠ 0}.Finite
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✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ Finite ↑{ab | ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab).coeff g ≠ 0}

Tactic:
apply ((VAddAntidiagonal g (Set.VAddAntidiagonal.finite_of_isPWO s.isPWO_iUnion_support
    t.isPWO_iUnion_support g)).finite_toSet.biUnion'
    (fun gh _ => hasFiniteSupport_smul s t gh)).subset _

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ {ab | ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab).coeff g ≠ 0} ⊆
    ⋃ i ∈ ↑(VAddAntidiagonal g ⋯), Function.support fun i_1 ↦ (s i_1.1).coeff i.1 • (t i_1.2).coeff i.2
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ᶠ (i : α × β), ∑ x ∈ VAddAntidiagonal g ⋯, (s i.1).coeff x.1 • (t i.2).coeff x.2 =
    ∑ x ∈ VAddAntidiagonal g ⋯,
      (∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1) • ∑ i ∈ (t.coeff x.2).support, (t i).coeff x.2

Tactic:
[

Goal state after:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ᶠ (i : α × β), ∑ x ∈ VAddAntidiagonal g ⋯, (s i.1).coeff x.1 • (t i.2).coeff x.2 =
    ∑ x ∈ VAddAntidiagonal g ⋯,
      (∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1) • ∑ i ∈ (t.coeff x.2).support, (t i).coeff x.2
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f g : R⟦ℕ⟧
n : ℕ
m : ℕ × ℕ
h : f.coeff m.1 * g.coeff m.2 ≠ 0
⊢ f.coeff m.1 ≠ 0 ∧ g.coeff m.2 ≠ 0 ∧ m.1 + m.2 = n ↔ m.1 + m.2 = n

Tactic:
rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]

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

Goal state before:
pp: M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective ⇑f₁
hf₁class :
  ∀ (a : M), ArchimedeanClass.mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (f₁ a))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' : StrictMono ⇑f₂'
hf₂class' :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂' a)).orderTop
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
hf₂ : Function.Injective ⇑f₂
hf₂class :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂ a)).orderTop
f₃ : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ →+o Lex ℝ⟦FiniteArchimedeanClass M⟧ :=
  embDomainOrderAddMonoidHom
    (RelIso.toRelEmbedding (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M).symm))
hf₃ : Function.Injective ⇑f₃
hf₃class :
  ∀ (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧),
    (ofLex a).orderTop =
      (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M)).withTopCongr
        (ofLex (f₃ a)).orderTop
a : M
⊢ ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex ((f₃.comp (f₂.comp f₁)) a)).orderTop

Tactic:
[

Goal state after:
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective ⇑f₁
hf₁class :
  ∀ (a : M), ArchimedeanClass.mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (f₁ a))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' : StrictMono ⇑f₂'
hf₂class' :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂' a)).orderTop
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
hf₂ : Function.Injective ⇑f₂
hf₂class :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂ a)).orderTop
f₃ : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ →+o Lex ℝ⟦FiniteArchimedeanClass M⟧ :=
  embDomainOrderAddMonoidHom
    (RelIso.toRelEmbedding (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M).symm))
hf₃ : Function.Injective ⇑f₃
hf₃class :
  ∀ (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧),
    (ofLex a).orderTop =
      (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M)).withTopCongr
        (ofLex (f₃ a)).orderTop
a : M
⊢ ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex ((f₃.comp (f₂.comp f₁)) a)).orderTop
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 Γ
x : PowerSeries R
n : ℕ
⊢ ((ofPowerSeries Γ R) x).coeff ↑n =
    (embDomain Nat.castOrderEmbedding (toPowerSeries.symm x)).coeff (Nat.castOrderEmbedding n)

pp: Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
x : PowerSeries R
n : ℕ
⊢ (embDomain Nat.castOrderEmbedding (toPowerSeries.symm x)).coeff (Nat.castOrderEmbedding n) = (PowerSeries.coeff n) x

Tactic:
· simp [ofPowerSeries_apply]

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
x : PowerSeries R
n : ℕ
⊢ (embDomain Nat.castOrderEmbedding (toPowerSeries.symm x)).coeff (Nat.castOrderEmbedding n) = (PowerSeries.coeff n) x
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
g : Γ
⊢ (s.mul t).hsum.coeff g = ∑ gh ∈ antidiagonal ⋯ ⋯ g, s.hsum.coeff gh.1 * t.hsum.coeff gh.2

Tactic:
[

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
g : Γ
⊢ (s.mul t).hsum.coeff g = ∑ gh ∈ antidiagonal ⋯ ⋯ g, s.hsum.coeff gh.1 * t.hsum.coeff gh.2
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
⊢ ∑ᶠ (i : α), (f i).coeff g = (∑ x ∈ f.support, id (f x)).coeff g

Tactic:
[

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
⊢ ∑ᶠ (i : α), (f i).coeff g = (∑ x ∈ f.support, id (f x)).coeff g
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
n : Γ
hn : n = 1
⊢ (embDomain Nat.castOrderEmbedding (toPowerSeries.symm PowerSeries.X)).coeff 1 = 1

Tactic:
convert! embDomain_coeff (a := 1)

Goal state after:
case e'_2.e'_6
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
n : Γ
hn : n = 1
⊢ 1 = Nat.castOrderEmbedding 1

case e'_3
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
n : Γ
hn : n = 1
⊢ 1 = (toPowerSeries.symm PowerSeries.X).coeff 1
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⟦σ →₀ ℕ⟧
n : σ →₀ ℕ
⊢ (f * g).coeff n = (MvPowerSeries.coeff n) (f.coeff * g.coeff)

Tactic:
[

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 : σ →₀ ℕ
⊢ (f * g).coeff n = (MvPowerSeries.coeff n) (f.coeff * g.coeff)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
⊢ (x ^ n).support ⊆ ↑(AddSubmonoid.closure x.support)

Tactic:
by
  intro g hn
  induction n generalizing g with
  | zero =>
    simp only [pow_zero, mem_support, coeff_one, ne_eq, ite_eq_right_iff, Classical.not_imp] at hn
    simp only [hn, SetLike.mem_coe]
    exact AddSubmonoid.zero_mem _
  | succ n ih =>
    obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset hn
    exact SetLike.mem_coe.2 (AddSubmonoid.add_mem _ (ih hi) (AddSubmonoid.subset_closure hj))

Goal state after:
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⟦σ →₀ ℕ⟧
n : σ →₀ ℕ
m : (σ →₀ ℕ) × (σ →₀ ℕ)
h : f.coeff m.1 * g.coeff m.2 ≠ 0
⊢ f.coeff m.1 ≠ 0 ∧ g.coeff m.2 ≠ 0 ∧ m.1 + m.2 = n ↔ m.1 + m.2 = n

Tactic:
rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]

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
x✝ : IsUnit (Polynomial.eval a₀ (derivative f))
h₁ : Polynomial.eval a₀ f = 0
⊢ ∃ a, f.IsRoot a ∧ a - a₀ = 0

Tactic:
exact ⟨a₀, h₁, sub_self _⟩

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

Goal state after:
Γ : 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
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case inr.refine_2
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h✝ : Nontrivial R
this : x.order = 0
⊢ IsAddUnit x.order

Tactic:
this

Goal state after:
case inr.refine_2
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h✝ : Nontrivial R
this : x.order = 0
⊢ IsAddUnit 0
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case inr
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
h : p ≠ q
⊢ ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q

Tactic:
P.over_def p

Goal state after:
case inr
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 : under R P ≤ q
h : under R P ≠ q
⊢ ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : q.height = 0
⊢ q.height < ↑1

Tactic:
this

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : q.height = 0
⊢ 0 < ↑1
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a (derivative f)) * (b - a) = 0
this : c * (b - a) + Polynomial.eval a (derivative f) ∉ maximalIdeal R
⊢ a = b

Tactic:
notMem_maximalIdeal,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
f : R[X]
a b : R
ha : Polynomial.eval a f = 0
hb : Polynomial.eval b f = 0
h : ¬IsUnit (a - b)
h' : IsUnit (Polynomial.eval a (derivative f))
c : R
h✝ :
  c * (b - a) ^ 2 + Polynomial.eval a (derivative f) * (b - a) + Polynomial.eval a f = Polynomial.eval (a + (b - a)) f
hc : (c * (b - a) + Polynomial.eval a (derivative f)) * (b - a) = 0
this : IsUnit (c * (b - a) + Polynomial.eval a (derivative f))
⊢ a = b
Module: Mathlib.RingTheory.Ideal.UFD

Goal state before:
pp: case neg
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : WfDvdMonoid R
x : R
hx : Prime x
p : Ideal R
inst✝³ : p.IsPrime
hxp : x ∉ p
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
this : Disjoint ↑(Submonoid.powers x) ↑p
hpbot : ¬p = ⊥
hi : Function.Injective ⇑(algebraMap R S)
hpb : map (algebraMap R S) p ≠ ⊥
g : S
hg : map (algebraMap R S) p = S ∙ g
hg0 : g ≠ 0
a : R
n : ℤ
hxa : ¬x ∣ a
hag : selfZPow x S n * (algebraMap R S) a = g
hu : IsUnit (selfZPow x S n)
⊢ Submodule.IsPrincipal p

Tactic:
refine ⟨a, Ideal.eq_of_map_algebraMap_le S x ?_ (by simp [IsPrime.mul_mem_left_iff hxp]) ?_⟩

Goal state after:
case neg.refine_1
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : WfDvdMonoid R
x : R
hx : Prime x
p : Ideal R
inst✝³ : p.IsPrime
hxp : x ∉ p
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
this : Disjoint ↑(Submonoid.powers x) ↑p
hpbot : ¬p = ⊥
hi : Function.Injective ⇑(algebraMap R S)
hpb : map (algebraMap R S) p ≠ ⊥
g : S
hg : map (algebraMap R S) p = S ∙ g
hg0 : g ≠ 0
a : R
n : ℤ
hxa : ¬x ∣ a
hag : selfZPow x S n * (algebraMap R S) a = g
hu : IsUnit (selfZPow x S n)
⊢ map (algebraMap R S) p = map (algebraMap R S) (R ∙ a)

case neg.refine_2
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : WfDvdMonoid R
x : R
hx : Prime x
p : Ideal R
inst✝³ : p.IsPrime
hxp : x ∉ p
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization.Away x S
this : Disjoint ↑(Submonoid.powers x) ↑p
hpbot : ¬p = ⊥
hi : Function.Injective ⇑(algebraMap R S)
hpb : map (algebraMap R S) p ≠ ⊥
g : S
hg : map (algebraMap R S) p = S ∙ g
hg0 : g ≠ 0
a : R
n : ℤ
hxa : ¬x ∣ a
hag : selfZPow x S n * (algebraMap R S) a = g
hu : IsUnit (selfZPow x S n)
⊢ ∀ (y : R), x * y ∈ R ∙ a → y ∈ R ∙ a
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) ⋯
this :
  LinearMap.lTensor (R ⧸ I) (Submodule.subtype J) =
    ↑(TensorProduct.rid R (R ⧸ I)).symm ∘ₗ f ∘ₗ ↑(quotTensorEquivQuotSMul (↥J) I)
⊢ Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) ↔ I ⊓ J = I * J

Tactic:
this

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) ⋯
this :
  LinearMap.lTensor (R ⧸ I) (Submodule.subtype J) =
    ↑(TensorProduct.rid R (R ⧸ I)).symm ∘ₗ f ∘ₗ ↑(quotTensorEquivQuotSMul (↥J) I)
⊢ Function.Injective ⇑(↑(TensorProduct.rid R (R ⧸ I)).symm ∘ₗ f ∘ₗ ↑(quotTensorEquivQuotSMul (↥J) I)) ↔ I ⊓ J = I * J
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Finset 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
hn : s.card ≤ n + 1
w✝ : IsLocalRing R
hp : maximalIdeal R ∈ (span ↑s).minimalPrimes
this : (maximalIdeal R).IsPrime
⊢ (maximalIdeal R).height ≤ ↑(n + 1)

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Finset 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
hn : s.card ≤ n + 1
w✝ : IsLocalRing R
hp : maximalIdeal R ∈ (span ↑s).minimalPrimes
this : (maximalIdeal R).IsPrime
⊢ (maximalIdeal R).height ≤ ↑(n + 1)
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Finset 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
hn : s.card ≤ n + 1
w✝ : IsLocalRing R
hp : maximalIdeal R ∈ (span ↑s).minimalPrimes
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
⊢ ¬↑s ⊆ ↑q

Tactic:
← span_le

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Finset 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
hn : s.card ≤ n + 1
w✝ : IsLocalRing R
hp : maximalIdeal R ∈ (span ↑s).minimalPrimes
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
⊢ ¬span ↑s ≤ q