mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «1».«0»
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f₀ f₁ f₂ : MvPowerSeries σ R
h₀ : PowerSeries.HasSubst f₀
h₁ : PowerSeries.HasSubst f₁
h₂ : PowerSeries.HasSubst f₂
aux₁ : HasSubst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂]
aux₂ : HasSubst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries]
this : HasSubst ![f₀, f₁, f₂]
⊢ subst ![f₀, f₁, f₂] (![X 1, X 2] ((fun i ↦ i) ⟨0, ⋯⟩)) = ![f₁, f₂] ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1».«1»
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f₀ f₁ f₂ : MvPowerSeries σ R
h₀ : PowerSeries.HasSubst f₀
h₁ : PowerSeries.HasSubst f₁
h₂ : PowerSeries.HasSubst f₂
aux₁ : HasSubst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂]
aux₂ : HasSubst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries]
this : HasSubst ![f₀, f₁, f₂]
⊢ subst ![f₀, f₁, f₂] (![X 1, X 2] ((fun i ↦ i) ⟨1, ⋯⟩)) = ![f₁, f₂] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «1».«0»
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f₀ f₁ f₂ : MvPowerSeries σ R
h₀ : PowerSeries.HasSubst f₀
h₁ : PowerSeries.HasSubst f₁
h₂ : PowerSeries.HasSubst f₂
aux₁ : HasSubst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂]
aux₂ : HasSubst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries]
this : HasSubst ![f₀, f₁, f₂]
⊢ subst ![f₀, f₁, f₂] (![X 1, X 2] ((fun i ↦ i) ⟨0, ⋯⟩)) = ![f₁, f₂] ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f₀ f₁ f₂ : MvPowerSeries σ R
h₀ : PowerSeries.HasSubst f₀
h₁ : PowerSeries.HasSubst f₁
h₂ : PowerSeries.HasSubst f₂
aux₁ : HasSubst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂]
aux₂ : HasSubst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries]
this : HasSubst ![f₀, f₁, f₂]
⊢ subst ![f₀, f₁, f₂] (![X 1, X 2] ((fun i ↦ i) ⟨1, ⋯⟩)) = ![f₁, f₂] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case inl
Γ : 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⟦Γ⟧
hx : ¬0 < x.orderTop
f : PowerSeries R
g : Γ
⊢ ((powerSeriesFamily x f) 0).coeff g = ((powerSeriesFamily 0 f) 0).coeff g

pp: case inr
Γ : 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⟦Γ⟧
hx : ¬0 < x.orderTop
f : PowerSeries R
n : ℕ
g : Γ
hn : n ≠ 0
⊢ ((powerSeriesFamily x f) n).coeff g = ((powerSeriesFamily 0 f) n).coeff g

Tactic:
<;>

Goal state after:
case inl
Γ : 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⟦Γ⟧
hx : ¬0 < x.orderTop
f : PowerSeries R
g : Γ
⊢ ((powerSeriesFamily x f) 0).coeff g = ((powerSeriesFamily 0 f) 0).coeff g

case inr
Γ : 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⟦Γ⟧
hx : ¬0 < x.orderTop
f : PowerSeries R
n : ℕ
g : Γ
hn : n ≠ 0
⊢ ((powerSeriesFamily x f) n).coeff g = ((powerSeriesFamily 0 f) n).coeff g
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos
Γ : 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
f : PowerSeries R
g : Γ
hg : ¬g = 0
n : ℕ
hn : n = 0
⊢ ((powerSeriesFamily 0 f) n).coeff g = 0

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
f : PowerSeries R
g : Γ
hg : ¬g = 0
n : ℕ
hn : ¬n = 0
⊢ ((powerSeriesFamily 0 f) n).coeff g = 0

Tactic:
<;>

Goal state after:
case pos
Γ : 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
f : PowerSeries R
g : Γ
hg : ¬g = 0
n : ℕ
hn : n = 0
⊢ ((powerSeriesFamily 0 f) n).coeff g = 0

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
f : PowerSeries R
g : Γ
hg : ¬g = 0
n : ℕ
hn : ¬n = 0
⊢ ((powerSeriesFamily 0 f) n).coeff g = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «0»
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
F : FormalGroup R
inst✝ : F.IsComm
f g : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
hg : PowerSeries.HasSubst g
⊢ subst ![f, g] (![X 1, X 0] ((fun i ↦ i) ⟨0, ⋯⟩)) = ![g, f] ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
F : FormalGroup R
inst✝ : F.IsComm
f g : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
hg : PowerSeries.HasSubst g
⊢ subst ![f, g] (![X 1, X 0] ((fun i ↦ i) ⟨1, ⋯⟩)) = ![g, f] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
F : FormalGroup R
inst✝ : F.IsComm
f g : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
hg : PowerSeries.HasSubst g
⊢ subst ![f, g] (![X 1, X 0] ((fun i ↦ i) ⟨0, ⋯⟩)) = ![g, f] ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
F : FormalGroup R
inst✝ : F.IsComm
f g : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
hg : PowerSeries.HasSubst g
⊢ subst ![f, g] (![X 1, X 0] ((fun i ↦ i) ⟨1, ⋯⟩)) = ![g, f] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos
Γ : 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⟦Γ⟧
f g : PowerSeries R
n : ℕ
hx : 0 < x.orderTop
⊢ (powerSeriesFamily x (f + g)) n = (powerSeriesFamily x f + powerSeriesFamily x g) n

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⟦Γ⟧
f g : PowerSeries R
n : ℕ
hx : ¬0 < x.orderTop
⊢ (powerSeriesFamily x (f + g)) n = (powerSeriesFamily x f + powerSeriesFamily x g) n

Tactic:
<;>

Goal state after:
case pos
Γ : 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⟦Γ⟧
f g : PowerSeries R
n : ℕ
hx : 0 < x.orderTop
⊢ (powerSeriesFamily x (f + g)) n = (powerSeriesFamily x f + powerSeriesFamily x g) n

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⟦Γ⟧
f g : PowerSeries R
n : ℕ
hx : ¬0 < x.orderTop
⊢ (powerSeriesFamily x (f + g)) n = (powerSeriesFamily x f + powerSeriesFamily x g) n
Module: Mathlib.RingTheory.PowerSeries.Binomial

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ binomialSeries A 0 = 1

Tactic:
by
  simpa using binomialSeries_nat 0

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

Goal state before:
pp: case pos
A : Type u_2
inst✝ : CommRing A
n : ℕ
hn : n = 0
⊢ ↑(↑n).negOnePow • (coeff n) ↑(invOneSubPow A 0) = Ring.choose (-↑0) n • 1

pp: case neg
A : Type u_2
inst✝ : CommRing A
n : ℕ
hn : ¬n = 0
⊢ ↑(↑n).negOnePow • (coeff n) ↑(invOneSubPow A 0) = Ring.choose (-↑0) n • 1

Tactic:
<;>

Goal state after:
case pos
A : Type u_2
inst✝ : CommRing A
n : ℕ
hn : n = 0
⊢ ↑(↑n).negOnePow • (coeff n) ↑(invOneSubPow A 0) = Ring.choose (-↑0) n • 1

case neg
A : Type u_2
inst✝ : CommRing A
n : ℕ
hn : ¬n = 0
⊢ ↑(↑n).negOnePow • (coeff n) ↑(invOneSubPow A 0) = Ring.choose (-↑0) n • 1
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos
Γ : 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
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
he :
  ∃ c ∈ HasAntidiagonal.antidiagonal n,
    (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • ((powers x) n).coeff g ≠ 0
⊢ n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))

Tactic:
simp only [powers_of_orderTop_pos h, HasAntidiagonal.mem_antidiagonal] at he

Goal state after:
case pos
Γ : 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
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
he : ∃ c, c.1 + c.2 = n ∧ (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • (x ^ n).coeff g ≠ 0
⊢ n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : ¬0 < (x - 1).orderTop
r : R
n : ℕ
hn : n = 0
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r)) n = 0 ^ n

pp: case neg
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : ¬0 < (x - 1).orderTop
r : R
n : ℕ
hn : ¬n = 0
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r)) n = 0 ^ n

Tactic:
<;>

Goal state after:
case pos
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : ¬0 < (x - 1).orderTop
r : R
n : ℕ
hn : n = 0
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r)) n = 0 ^ n

case neg
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : ¬0 < (x - 1).orderTop
r : R
n : ℕ
hn : ¬n = 0
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r)) n = 0 ^ n
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
hn : n ≠ k
hr : r = 0
⊢ 0 < (1 + (single g) r - 1).orderTop

pp: case neg
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
hn : n ≠ k
hr : ¬r = 0
⊢ 0 < (1 + (single g) r - 1).orderTop

Tactic:
<;>

Goal state after:
case pos
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
hn : n ≠ k
hr : r = 0
⊢ 0 < (1 + (single g) r - 1).orderTop

case neg
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
hn : n ≠ k
hr : ¬r = 0
⊢ 0 < (1 + (single g) r - 1).orderTop
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:
Classical.not_not

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.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 : α), ¬(s x).coeff g ≠ 0) → ∑ᶠ (i : α), (s i).coeff g = 0

Tactic:
Classical.not_not

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 : α), (s x).coeff g = 0) → ∑ᶠ (i : α), (s i).coeff g = 0
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⟦Γ⟧
g : Γ
j : ι
⊢ j ∈ {a | (Pi.single j x a).coeff g ≠ 0} → j ∈ {j}

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⟦Γ⟧
g : Γ
j : ι
ha : j ≠ i
⊢ j ∈ {a | (Pi.single i x a).coeff g ≠ 0} → j ∈ {i}

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⟦Γ⟧
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.FormalGroup.Basic

Goal state before:
pp: case «0»
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
g₁ g₂ : MvPowerSeries (Fin 3) R
⊢ ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] ((fun i ↦ i) ⟨0, ⋯⟩) =
    (MvPowerSeries.map f) (![g₁, g₂] ((fun i ↦ i) ⟨0, ⋯⟩))

pp: case «1»
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
g₁ g₂ : MvPowerSeries (Fin 3) R
⊢ ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] ((fun i ↦ i) ⟨1, ⋯⟩) =
    (MvPowerSeries.map f) (![g₁, g₂] ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
<;>

Goal state after:
case «0»
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
g₁ g₂ : MvPowerSeries (Fin 3) R
⊢ ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] ((fun i ↦ i) ⟨0, ⋯⟩) =
    (MvPowerSeries.map f) (![g₁, g₂] ((fun i ↦ i) ⟨0, ⋯⟩))

case «1»
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
g₁ g₂ : MvPowerSeries (Fin 3) R
⊢ ![(MvPowerSeries.map f) g₁, (MvPowerSeries.map f) g₂] ((fun i ↦ i) ⟨1, ⋯⟩) =
    (MvPowerSeries.map f) (![g₁, g₂] ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.RingTheory.HahnSeries.HEval

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
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
hg : g = 0
⊢ (if 0 = 0 then r • (if 0 < x.orderTop then x else 0) ^ 0 else 0).coeff g = ((algebraMap R R⟦Γ⟧) r).coeff g

pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
hg : ¬g = 0
⊢ (if 0 = 0 then r • (if 0 < x.orderTop then x else 0) ^ 0 else 0).coeff g = ((algebraMap R R⟦Γ⟧) r).coeff g

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
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
hg : g = 0
⊢ (if 0 = 0 then r • (if 0 < x.orderTop then x else 0) ^ 0 else 0).coeff g = ((algebraMap R R⟦Γ⟧) r).coeff g

case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
hg : ¬g = 0
⊢ (if 0 = 0 then r • (if 0 < x.orderTop then x else 0) ^ 0 else 0).coeff g = ((algebraMap R R⟦Γ⟧) r).coeff g
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⟦Γ⟧
r : R
g : Γ
hg : g = 0
⊢ (coeff 0) (C r) * ((if 0 < x.orderTop then x else 0) ^ 0).coeff g = if g = 0 then r else 0

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
hg : ¬g = 0
⊢ (coeff 0) (C r) * ((if 0 < x.orderTop then x else 0) ^ 0).coeff g = if g = 0 then r else 0

Tactic:
<;>

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
hg : g = 0
⊢ (coeff 0) (C r) * ((if 0 < x.orderTop then x else 0) ^ 0).coeff g = if g = 0 then r else 0

case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
hg : ¬g = 0
⊢ (coeff 0) (C r) * ((if 0 < x.orderTop then x else 0) ^ 0).coeff g = if g = 0 then r else 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ![0, 0] ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ![0, 0] ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ![0, 0] ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ![0, 0] ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)
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 : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal g ⋯
⊢ ∑ᶠ (b : α × β), (s b.1).coeff gh.1 • (t b.2).coeff gh.2 =
    ∑ x ∈ (t.coeff gh.2).support, ∑ i ∈ (s.coeff gh.1).support, (s i).coeff gh.1 • (t x).coeff gh.2

Tactic:
rw [finsum_eq_sum _ (hasFiniteSupport_smul s t gh), ← sum_product_right']

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 : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal g ⋯
⊢ ∑ i ∈ Set.Finite.toFinset ⋯, (s i.1).coeff gh.1 • (t i.2).coeff gh.2 =
    ∑ x ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support, (s x.1).coeff gh.1 • (t x.2).coeff gh.2
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case refine_1
Γ : 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 : Γ'
x✝ : Γ × Γ'
hgh : x✝ ∈ ↑(VAddAntidiagonal g ⋯)
⊢ (fun a ↦ a) x✝ ∈ ↑(VAddAntidiagonal g ⋯)

pp: case refine_2
Γ : 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 : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal g ⋯
hgh : gh ∉ (fun a ↦ a) '' ↑(VAddAntidiagonal g ⋯)
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

Tactic:
· simp_all only [mem_coe, mem_vaddAntidiagonal, mem_support, ne_eq, Set.mem_iUnion, and_true]
    constructor
    · rw [coeff_hsum_eq_sum] at hgh
      have h' := Finset.exists_ne_zero_of_sum_ne_zero hgh.1
      simpa using h'
    · by_contra hi
      simp_all

Goal state after:
case refine_2
Γ : 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 : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal g ⋯
hgh : gh ∉ (fun a ↦ a) '' ↑(VAddAntidiagonal g ⋯)
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: case e'_2.e'_6
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
r : R
⊢ 0 = Nat.castOrderEmbedding 0

pp: case e'_3
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
r : R
⊢ r = (toPowerSeries.symm (PowerSeries.C r)).coeff 0

Tactic:
<;>

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

case e'_3
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
r : R
⊢ r = (toPowerSeries.symm (PowerSeries.C r)).coeff 0
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
r : R
n : Γ
hn : ¬n = 0
x✝ : ℕ
⊢ ¬((if x✝ = 0 then r else 0) ≠ 0 ∧ Nat.castOrderEmbedding x✝ = n)

Tactic:
simp +contextual [Ne.symm hn]

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

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

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

Tactic:
<;>

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: case neg
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
n : Γ
hn : ¬n = 1
x✝ : ℕ
⊢ ¬((if x✝ = 1 then 1 else 0) ≠ 0 ∧ Nat.castOrderEmbedding x✝ = n)

Tactic:
simp +contextual [Ne.symm hn]

Goal state after: