internlm/Lean-Github huggingface dataset:
Theorem: PowerSeries.isExponential_scale
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 0) f) *
      MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 1) f)

case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 1) = 0

case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0) = 0

case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
simp only [← MvPowerSeries.coe_scale_algHom, ← map_mul, hf.add_mul]
Proof state after:
case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 1) = 0

case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0) = 0

case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Theorem: PowerSeries.isExponential_scale
Proof state before:
case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 1) = 0

case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0) = 0

case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
repeat
  intro d hd
  simp only [Fin.isValue, map_add, MvPowerSeries.coeff_X]
  rw [if_neg]
  intro hd'
  apply hd
  rw [hd']
  simp only [Fin.isValue, Finsupp.sum_single_index]
Proof state after:
case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Theorem: PowerSeries.isExponential_scale
Proof state before:
case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
intro d hd
Proof state after:
case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Theorem: PowerSeries.isExponential_scale
Proof state before:
case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
simp only [Fin.isValue, map_add, MvPowerSeries.coeff_X]
Proof state after:
case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ ((if d = Finsupp.single 0 1 then 1 else 0) + if d = Finsupp.single 1 1 then 1 else 0) = 0
Theorem: PowerSeries.isExponential_scale
Proof state before:
case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ ((if d = Finsupp.single 0 1 then 1 else 0) + if d = Finsupp.single 1 1 then 1 else 0) = 0
Tactic:
rw [if_neg]
Proof state after:
case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ (0 + if d = Finsupp.single 1 1 then 1 else 0) = 0

case hp_lin.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ ¬d = Finsupp.single 0 1
Theorem: PowerSeries.isExponential_scale
Proof state before:
case hp_lin.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ ¬d = Finsupp.single 0 1

case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
intro hd'
Proof state after:
case hp_lin.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
hd' : d = Finsupp.single 0 1
⊢ False

case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Theorem: PowerSeries.isExponential_scale
Proof state before:
case hp_lin.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
hd' : d = Finsupp.single 0 1
⊢ False

case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
apply hd
Proof state after:
case hp_lin.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
hd' : d = Finsupp.single 0 1
⊢ (d.sum fun x n => n) = 1

case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Theorem: PowerSeries.isExponential_scale
Proof state before:
case hp_lin.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
hd' : d = Finsupp.single 0 1
⊢ (d.sum fun x n => n) = 1

case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
rw [hd']
Proof state after:
case hp_lin.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
hd' : d = Finsupp.single 0 1
⊢ ((Finsupp.single 0 1).sum fun x n => n) = 1

case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Theorem: PowerSeries.isExponential_scale
Proof state before:
case hp_lin.hnc
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
hd' : d = Finsupp.single 0 1
⊢ ((Finsupp.single 0 1).sum fun x n => n) = 1

case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
simp only [Fin.isValue, Finsupp.sum_single_index]
Proof state after:
case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (d : Fin 2 →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (MvPowerSeries.coeff R d) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Theorem: PowerSeries.isExponential_scale
Proof state before:
case hp_lin
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
⊢ ((if d = Finsupp.single 0 1 then 1 else 0) + if d = Finsupp.single 1 1 then 1 else 0) = 0
Tactic:
split_ifs with h0 h1 h1
Proof state after:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ 1 + 1 = 0

case neg
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ 1 + 0 = 0

case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ 0 + 1 = 0

case neg
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ 0 + 0 = 0
Theorem: PowerSeries.isExponential_scale
Proof state before:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ 1 + 1 = 0
Tactic:
rw [h1, Finsupp.single_left_inj (by norm_num)] at h0
Proof state after:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : 1 = 0
h1 : d = Finsupp.single 1 1
⊢ 1 + 1 = 0
Theorem: PowerSeries.isExponential_scale
Proof state before:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : 1 = 0
h1 : d = Finsupp.single 1 1
⊢ 1 + 1 = 0
Tactic:
exfalso
Proof state after:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : 1 = 0
h1 : d = Finsupp.single 1 1
⊢ False
Theorem: PowerSeries.isExponential_scale
Proof state before:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : 1 = 0
h1 : d = Finsupp.single 1 1
⊢ False
Tactic:
exact one_ne_zero h0
Proof state after:
no goals
Theorem: PowerSeries.isExponential_scale
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : Finsupp.single 1 1 = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ 1 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: PowerSeries.isExponential_scale
Proof state before:
case neg
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ 1 + 0 = 0
Tactic:
exfalso
Proof state after:
case neg
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ False
Theorem: PowerSeries.isExponential_scale
Proof state before:
case neg
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ False
Tactic:
apply hd
Proof state after:
case neg
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ (d.sum fun x n => n) = 1
Theorem: PowerSeries.isExponential_scale
Proof state before:
case neg
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ (d.sum fun x n => n) = 1
Tactic:
simp only [h0, Fin.isValue, Finsupp.sum_single_index]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_scale
Proof state before:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ 0 + 1 = 0
Tactic:
exfalso
Proof state after:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ False
Theorem: PowerSeries.isExponential_scale
Proof state before:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ False
Tactic:
apply hd
Proof state after:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ (d.sum fun x n => n) = 1
Theorem: PowerSeries.isExponential_scale
Proof state before:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : d = Finsupp.single 1 1
⊢ (d.sum fun x n => n) = 1
Tactic:
simp only [h1, Fin.isValue, Finsupp.sum_single_index]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_scale
Proof state before:
case neg
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
a : A
f : R⟦X⟧
hf : f.IsExponential
d : Fin 2 →₀ ℕ
hd : (d.sum fun x n => n) ≠ 1
h0 : ¬d = Finsupp.single 0 1
h1 : ¬d = Finsupp.single 1 1
⊢ 0 + 0 = 0
Tactic:
simp only [add_zero]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_scale_add
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
r s : A
f : R⟦X⟧
hf : f.IsExponential
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
let a : Fin 2 → PowerSeries R
| 0 => r • X
| 1 => s • X
Proof state after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
⊢ scale (r + s) f = scale r f * scale s f
Theorem: PowerSeries.isExponential_scale_add
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
have ha : MvPowerSeries.SubstDomain a := by
  apply MvPowerSeries.substDomain_of_constantCoeff_zero
  intro i
  simp only [X, a]
  match i with
  | 0 =>
    rw [MvPowerSeries.constantCoeff_smul, MvPowerSeries.constantCoeff_X, smul_zero]
  | 1 =>
    rw [MvPowerSeries.constantCoeff_smul, MvPowerSeries.constantCoeff_X, smul_zero]
Proof state after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
⊢ scale (r + s) f = scale r f * scale s f
Theorem: PowerSeries.isExponential_scale_add
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
have hf' := congr_arg (MvPowerSeries.subst a) hf.add_mul
Proof state after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst a (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    MvPowerSeries.subst a (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s f
Theorem: PowerSeries.isExponential_scale_add
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst a (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    MvPowerSeries.subst a (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
simp only [PowerSeries.subst] at hf'
Proof state after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst a (MvPowerSeries.subst (fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    MvPowerSeries.subst a
      (MvPowerSeries.subst (fun x => MvPowerSeries.X 0) f * MvPowerSeries.subst (fun x => MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s f
Theorem: PowerSeries.isExponential_scale_add
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  MvPowerSeries.subst a (MvPowerSeries.subst (fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    MvPowerSeries.subst a
      (MvPowerSeries.subst (fun x => MvPowerSeries.X 0) f * MvPowerSeries.subst (fun x => MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s f
Tactic:
rw [← MvPowerSeries.coe_substAlgHom ha] at hf'
Proof state after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
r s : A
f : R⟦X⟧
hf : f.IsExponential
a : Fin 2 → R⟦X⟧ :=
  fun x =>
    match x with
    | 0 => r • X
    | 1 => s • X
ha : MvPowerSeries.SubstDomain a
hf' :
  (MvPowerSeries.substAlgHom ha) (MvPowerSeries.subst (fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    (MvPowerSeries.substAlgHom ha)
      (MvPowerSeries.subst (fun x => MvPowerSeries.X 0) f * MvPowerSeries.subst (fun x => MvPowerSeries.X 1) f)
⊢ scale (r + s) f = scale r f * scale s f