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

Goal state before:
pp: case inl
Γ : 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
ι : Type ?u.21
inst✝ : DecidableEq ι
x : R⟦Γ⟧
a : ι
this : (Pi.single a x a).support.IsPWO
⊢ (Pi.single a x a).support ⊆ (Pi.single a x a).support

pp: case inr
Γ : 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
ι : Type ?u.21
inst✝ : DecidableEq ι
i : ι
x : R⟦Γ⟧
this : (Pi.single i x i).support.IsPWO
a : ι
ha : a ≠ i
⊢ (Pi.single i x a).support ⊆ (Pi.single i x i).support

Tactic:
·

Goal state after:
case inl
Γ : 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
ι : Type ?u.21
inst✝ : DecidableEq ι
x : R⟦Γ⟧
a : ι
this : (Pi.single a x a).support.IsPWO
⊢ (Pi.single a x a).support ⊆ (Pi.single a x a).support
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case inr
Γ : 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
ι : Type ?u.21
inst✝ : DecidableEq ι
i : ι
x : R⟦Γ⟧
this : (Pi.single i x i).support.IsPWO
a : ι
ha : a ≠ i
⊢ (Pi.single i x a).support ⊆ (Pi.single i x i).support

Tactic:
·

Goal state after:
case inr
Γ : 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
ι : Type ?u.21
inst✝ : DecidableEq ι
i : ι
x : R⟦Γ⟧
this : (Pi.single i x i).support.IsPWO
a : ι
ha : a ≠ i
⊢ (Pi.single i x a).support ⊆ (Pi.single i x i).support
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
ι : Type ?u.21
inst✝ : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
j : ι
⊢ j ∈ {a | (Pi.single i x a).coeff g ≠ 0} → j ∈ {i}

Tactic:
obtain rfl | ha := eq_or_ne j i

Goal state after:
case inl
Γ : 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
ι : Type ?u.21
inst✝ : DecidableEq ι
x : R⟦Γ⟧
g : Γ
j : ι
⊢ j ∈ {a | (Pi.single j x a).coeff g ≠ 0} → j ∈ {j}

case inr
Γ : 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
ι : Type ?u.21
inst✝ : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
j : ι
ha : j ≠ i
⊢ j ∈ {a | (Pi.single i x a).coeff g ≠ 0} → j ∈ {i}
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case inl
Γ : 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
ι : Type ?u.20
inst✝ : Finite ι
x : R⟦Γ⟧
h✝ : IsEmpty ι
⊢ (⋃ a, x.support).IsPWO

pp: case inr
Γ : 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
ι : Type ?u.20
inst✝ : Finite ι
x : R⟦Γ⟧
h✝ : Nonempty ι
⊢ (⋃ a, x.support).IsPWO

Tactic:
·

Goal state after:
case inl
Γ : 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
ι : Type ?u.20
inst✝ : Finite ι
x : R⟦Γ⟧
h✝ : IsEmpty ι
⊢ (⋃ a, x.support).IsPWO
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case inr
Γ : 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
ι : Type ?u.20
inst✝ : Finite ι
x : R⟦Γ⟧
h✝ : Nonempty ι
⊢ (⋃ a, x.support).IsPWO

Tactic:
·

Goal state after:
case inr
Γ : 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
ι : Type ?u.20
inst✝ : Finite ι
x : R⟦Γ⟧
h✝ : Nonempty ι
⊢ (⋃ a, x.support).IsPWO
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : ¬0 < x.orderTop
⊢ (powerSeriesFamily x (a * b)).hsum = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum

Tactic:
·

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : ¬0 < x.orderTop
⊢ (powerSeriesFamily x (a * b)).hsum = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ (coeff (single 0 1)) F.toPowerSeries • (coeff (single () 1)) ((single 0 1).prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) =
    1

pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ∀ (x : Fin (Nat.succ 0).succ →₀ ℕ),
    x ≠ single 0 1 → (coeff x) F.toPowerSeries • (coeff (single () 1)) (x.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

pp: case ha
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ HasSubst ![PowerSeries.X, 0]

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ (coeff (single 0 1)) F.toPowerSeries • (coeff (single () 1)) ((single 0 1).prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) =
    1
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ∀ (x : Fin (Nat.succ 0).succ →₀ ℕ),
    x ≠ single 0 1 → (coeff x) F.toPowerSeries • (coeff (single () 1)) (x.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

pp: case ha
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ HasSubst ![PowerSeries.X, 0]

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ∀ (x : Fin (Nat.succ 0).succ →₀ ℕ),
    x ≠ single 0 1 → (coeff x) F.toPowerSeries • (coeff (single () 1)) (x.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0
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 α
g : Γ
⊢ {a | (-s a).coeff g ≠ 0}.Finite

Tactic:
simp only [coeff_neg', Pi.neg_apply, Ne, neg_eq_zero]

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 α
g : Γ
⊢ {a | ¬(s a).coeff g = 0}.Finite
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

pp: case neg
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : ¬d 1 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ((powerSeriesFamily x f).coeff 0) 0 = (coeff 0) f

pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ∀ (x_1 : ℕ), x_1 ≠ 0 → ((powerSeriesFamily x f).coeff 0) x_1 = 0

Tactic:
·

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ((powerSeriesFamily x f).coeff 0) 0 = (coeff 0) f
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ∀ (x_1 : ℕ), x_1 ≠ 0 → ((powerSeriesFamily x f).coeff 0) x_1 = 0

Tactic:
·

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ ∀ (x_1 : ℕ), x_1 ≠ 0 → ((powerSeriesFamily x f).coeff 0) x_1 = 0
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : 0 < x.orderTop
⊢ ↑0 < ((powers x) n).orderTop

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : ¬0 < x.orderTop
⊢ ↑0 < ((powers x) n).orderTop

Tactic:
·

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : 0 < x.orderTop
⊢ ↑0 < ((powers x) n).orderTop
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
hd₀ : d 0 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

pp: case neg
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
hd₀ : ¬d 0 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
hd₀ : d 0 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : ¬0 < x.orderTop
⊢ ↑0 < ((powers x) n).orderTop

Tactic:
·

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : ¬0 < x.orderTop
⊢ ↑0 < ((powers x) n).orderTop
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case ha
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ HasSubst ![PowerSeries.X, 0]

Tactic:
·

Goal state after:
case ha
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ HasSubst ![PowerSeries.X, 0]
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ subst (fun s ↦ subst (fun x ↦ subst ![PowerSeries.X, 0] F.toPowerSeries) (![PowerSeries.X, 0] s)) F.toPowerSeries =
    subst ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] F.toPowerSeries

pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ HasSubst ![PowerSeries.X, 0]

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ subst (fun s ↦ subst (fun x ↦ subst ![PowerSeries.X, 0] F.toPowerSeries) (![PowerSeries.X, 0] s)) F.toPowerSeries =
    subst ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] F.toPowerSeries
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ subst (fun x ↦ subst ![PowerSeries.X, 0] F.toPowerSeries) (![PowerSeries.X, 0] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ subst (fun x ↦ subst ![PowerSeries.X, 0] F.toPowerSeries) (![PowerSeries.X, 0] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
·

Goal state after:
case «0»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ subst (fun x ↦ subst ![PowerSeries.X, 0] F.toPowerSeries) (![PowerSeries.X, 0] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] ((fun i ↦ i) ⟨0, ⋯⟩)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case refine_1
Γ : 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 : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
⊢ gh ∈ VAddAntidiagonal g ⋯

pp: case refine_2
Γ : 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 : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
h : gh ∉ VAddAntidiagonal g ⋯
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0

Tactic:
·

Goal state after:
case refine_1
Γ : 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 : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
⊢ gh ∈ VAddAntidiagonal g ⋯
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ subst (fun x ↦ subst ![PowerSeries.X, 0] F.toPowerSeries) (![PowerSeries.X, 0] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
·

Goal state after:
case «1»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ subst (fun x ↦ subst ![PowerSeries.X, 0] F.toPowerSeries) (![PowerSeries.X, 0] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case refine_1
Γ : 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 : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
⊢ gh ∈ VAddAntidiagonal g ⋯

Tactic:
simp_all only [mem_vaddAntidiagonal, Function.mem_support, Set.mem_iUnion, mem_support]
    exact ⟨Exists.intro a.1 hgh.1, Exists.intro a.2 hgh.2.1, trivial⟩

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

Goal state before:
pp: case refine_2
Γ : 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 : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
h : gh ∉ VAddAntidiagonal g ⋯
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0

Tactic:
·

Goal state after:
case refine_2
Γ : 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 : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
h : gh ∉ VAddAntidiagonal g ⋯
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ HasSubst ![PowerSeries.X, 0]

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ HasSubst ![PowerSeries.X, 0]
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case pos
Γ : 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 : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
h : gh ∉ VAddAntidiagonal g ⋯
hs : (s a.1).coeff gh.1 = 0
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0

pp: case neg
Γ : 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 : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
h : gh ∉ VAddAntidiagonal g ⋯
hs : ¬(s a.1).coeff gh.1 = 0
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0

Tactic:
·

Goal state after:
case pos
Γ : 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 : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
h : gh ∉ VAddAntidiagonal g ⋯
hs : (s a.1).coeff gh.1 = 0
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case neg
Γ : 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 : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
h : gh ∉ VAddAntidiagonal g ⋯
hs : ¬(s a.1).coeff gh.1 = 0
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0

Tactic:
·

Goal state after:
case neg
Γ : 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 : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal g ⋯
h : gh ∉ VAddAntidiagonal g ⋯
hs : ¬(s a.1).coeff gh.1 = 0
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ (coeff (single 1 1)) F.toPowerSeries • (coeff (single () 1)) ((single 1 1).prod fun s e ↦ ![0, PowerSeries.X] s ^ e) =
    1

pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ∀ (x : Fin (Nat.succ 0).succ →₀ ℕ),
    x ≠ single 1 1 → (coeff x) F.toPowerSeries • (coeff (single () 1)) (x.prod fun s e ↦ ![0, PowerSeries.X] s ^ e) = 0

pp: case ha
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ HasSubst ![0, PowerSeries.X]

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ (coeff (single 1 1)) F.toPowerSeries • (coeff (single () 1)) ((single 1 1).prod fun s e ↦ ![0, PowerSeries.X] s ^ e) =
    1
Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module ℚ M
inst✝ : IsOrderedModule ℚ M
⊢ Nonempty (HahnEmbedding.Seed ℚ M ℝ)

Tactic:
obtain ⟨strata⟩ : Nonempty (HahnEmbedding.ArchimedeanStrata ℚ M) := inferInstance

Goal state after:
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module ℚ M
inst✝ : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
⊢ Nonempty (HahnEmbedding.Seed ℚ M ℝ)
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ∀ (x : Fin (Nat.succ 0).succ →₀ ℕ),
    x ≠ single 1 1 → (coeff x) F.toPowerSeries • (coeff (single () 1)) (x.prod fun s e ↦ ![0, PowerSeries.X] s ^ e) = 0

pp: case ha
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ HasSubst ![0, PowerSeries.X]

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ∀ (x : Fin (Nat.succ 0).succ →₀ ℕ),
    x ≠ single 1 1 → (coeff x) F.toPowerSeries • (coeff (single () 1)) (x.prod fun s e ↦ ![0, PowerSeries.X] s ^ e) = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 1 1
hd₁ : d 0 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![0, PowerSeries.X] s ^ e) = 0

pp: case neg
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 1 1
hd₁ : ¬d 0 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![0, PowerSeries.X] s ^ e) = 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 1 1
hd₁ : d 0 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![0, PowerSeries.X] s ^ e) = 0
Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding

Goal state before:
pp: case h₁
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module ℚ M
inst✝ : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ
hf : ∀ (c : FiniteArchimedeanClass M), Function.Injective ⇑(f c)
c : FiniteArchimedeanClass M
⊢ Monotone ⇑(f c).toRatLinearMap

pp: case h₂
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module ℚ M
inst✝ : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ
hf : ∀ (c : FiniteArchimedeanClass M), Function.Injective ⇑(f c)
c : FiniteArchimedeanClass M
⊢ Function.Injective ⇑(f c).toRatLinearMap

Tactic:
·

Goal state after:
case h₁
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module ℚ M
inst✝ : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ
hf : ∀ (c : FiniteArchimedeanClass M), Function.Injective ⇑(f c)
c : FiniteArchimedeanClass M
⊢ Monotone ⇑(f c).toRatLinearMap