internlm/Lean-Github huggingface dataset:
Theorem: PowerSeries.isExponential_add_mul_iff
Proof state before:
case h₁
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
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
⊢ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∈ Finset.antidiagonal e
Tactic:
simp only [Finset.mem_antidiagonal]
Proof state after:
case h₁
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
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
⊢ Finsupp.single 0 (e 0) + Finsupp.single 1 (e 1) = e
Theorem: PowerSeries.isExponential_add_mul_iff
Proof state before:
case h₁
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
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
⊢ Finsupp.single 0 (e 0) + Finsupp.single 1 (e 1) = e
Tactic:
ext i
Proof state after:
case h₁.h
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
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
i : Fin 2
⊢ (Finsupp.single 0 (e 0) + Finsupp.single 1 (e 1)) i = e i
Theorem: PowerSeries.isExponential_add_mul_iff
Proof state before:
case h₁.h
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
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
i : Fin 2
⊢ (Finsupp.single 0 (e 0) + Finsupp.single 1 (e 1)) i = e i
Tactic:
match i with
| 0 => simp
| 1 => simp
Proof state after:
no goals
Theorem: PowerSeries.isExponential_add_mul_iff
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
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
i : Fin 2
⊢ (Finsupp.single 0 (e 0) + Finsupp.single 1 (e 1)) 0 = e 0
Tactic:
simp
Proof state after:
no goals
Theorem: PowerSeries.isExponential_add_mul_iff
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
f : R⟦X⟧
he✝ :
  ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f
e : Fin 2 →₀ ℕ
he : (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e
i : Fin 2
⊢ (Finsupp.single 0 (e 0) + Finsupp.single 1 (e 1)) 1 = e 1
Tactic:
simp
Proof state after:
no goals
Theorem: PowerSeries.isExponential_iff
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
f : R⟦X⟧
⊢ f.IsExponential ↔
    (constantCoeff R) f = 1 ∧ ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff R (p + q)) f = (coeff R p) f * (coeff R q) f
Tactic:
rw [← isExponential_add_mul_iff]
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
f : R⟦X⟧
⊢ f.IsExponential ↔
    (constantCoeff R) f = 1 ∧
      subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f = subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f
Theorem: PowerSeries.isExponential_iff
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
f : R⟦X⟧
⊢ f.IsExponential ↔
    (constantCoeff R) f = 1 ∧
      subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f = subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f
Tactic:
constructor
Proof state after:
case mp
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
f : R⟦X⟧
⊢ f.IsExponential →
    (constantCoeff R) f = 1 ∧
      subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f = subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f

case mpr
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
f : R⟦X⟧
⊢ (constantCoeff R) f = 1 ∧
      subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f = subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f →
    f.IsExponential
Theorem: PowerSeries.isExponential_iff
Proof state before:
case mp
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
f : R⟦X⟧
⊢ f.IsExponential →
    (constantCoeff R) f = 1 ∧
      subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f = subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f
Tactic:
exact fun hf ↦ ⟨hf.constantCoeff, hf.add_mul⟩
Proof state after:
no goals
Theorem: PowerSeries.isExponential_iff
Proof state before:
case mpr
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
f : R⟦X⟧
⊢ (constantCoeff R) f = 1 ∧
      subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f = subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f →
    f.IsExponential
Tactic:
exact fun hf ↦ {
  constantCoeff := hf.1
  add_mul := hf.2 }
Proof state after:
no goals
Theorem: PowerSeries.isExponential_one
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
⊢ subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) 1 = subst (MvPowerSeries.X 0) 1 * subst (MvPowerSeries.X 1) 1
Tactic:
rw [← Polynomial.coe_one]
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
⊢ subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) ↑1 = subst (MvPowerSeries.X 0) ↑1 * subst (MvPowerSeries.X 1) ↑1
Theorem: PowerSeries.isExponential_one
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
⊢ subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) ↑1 = subst (MvPowerSeries.X 0) ↑1 * subst (MvPowerSeries.X 1) ↑1
Tactic:
rw [subst_coe (substDomain_of_constantCoeff_zero (by simp))]
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
⊢ (Polynomial.aeval (MvPowerSeries.X 0 + MvPowerSeries.X 1)) 1 =
    subst (MvPowerSeries.X 0) ↑1 * subst (MvPowerSeries.X 1) ↑1
Theorem: PowerSeries.isExponential_one
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
⊢ (Polynomial.aeval (MvPowerSeries.X 0 + MvPowerSeries.X 1)) 1 =
    subst (MvPowerSeries.X 0) ↑1 * subst (MvPowerSeries.X 1) ↑1
Tactic:
rw [subst_coe (substDomain_of_constantCoeff_zero (by simp))]
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
⊢ (Polynomial.aeval (MvPowerSeries.X 0 + MvPowerSeries.X 1)) 1 =
    (Polynomial.aeval (MvPowerSeries.X 0)) 1 * subst (MvPowerSeries.X 1) ↑1
Theorem: PowerSeries.isExponential_one
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
⊢ (Polynomial.aeval (MvPowerSeries.X 0 + MvPowerSeries.X 1)) 1 =
    (Polynomial.aeval (MvPowerSeries.X 0)) 1 * subst (MvPowerSeries.X 1) ↑1
Tactic:
rw [subst_coe (substDomain_of_constantCoeff_zero (by simp))]
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
⊢ (Polynomial.aeval (MvPowerSeries.X 0 + MvPowerSeries.X 1)) 1 =
    (Polynomial.aeval (MvPowerSeries.X 0)) 1 * (Polynomial.aeval (MvPowerSeries.X 1)) 1
Theorem: PowerSeries.isExponential_one
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
⊢ (Polynomial.aeval (MvPowerSeries.X 0 + MvPowerSeries.X 1)) 1 =
    (Polynomial.aeval (MvPowerSeries.X 0)) 1 * (Polynomial.aeval (MvPowerSeries.X 1)) 1
Tactic:
simp only [map_one, mul_one]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_one
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
⊢ (MvPowerSeries.constantCoeff (Fin 2) R) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 0
Tactic:
simp
Proof state after:
no goals
Theorem: PowerSeries.isExponential_one
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
⊢ (MvPowerSeries.constantCoeff (Fin 2) R) (MvPowerSeries.X 0) = 0
Tactic:
simp
Proof state after:
no goals
Theorem: PowerSeries.isExponential_one
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
⊢ (MvPowerSeries.constantCoeff (Fin 2) R) (MvPowerSeries.X 1) = 0
Tactic:
simp
Proof state after:
no goals
Theorem: PowerSeries.isExponential_one
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
⊢ (constantCoeff R) 1 = 1
Tactic:
simp only [map_one]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_mul
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
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) (f * g) =
    subst (MvPowerSeries.X 0) (f * g) * subst (MvPowerSeries.X 1) (f * g)
Tactic:
repeat
  rw [← coe_substAlgHom (substDomain_of_constantCoeff_zero (by simp))]
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
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ (substAlgHom ⋯) (f * g) = (substAlgHom ⋯) (f * g) * (substAlgHom ⋯) (f * g)
Theorem: PowerSeries.isExponential_mul
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
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ (substAlgHom ⋯) (f * g) = (substAlgHom ⋯) (f * g) * (substAlgHom ⋯) (f * g)
Tactic:
simp only [map_mul, coe_substAlgHom, hf.add_mul, hg.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
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f *
      (subst (MvPowerSeries.X 0) g * subst (MvPowerSeries.X 1) g) =
    subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 0) g *
      (subst (MvPowerSeries.X 1) f * subst (MvPowerSeries.X 1) g)
Theorem: PowerSeries.isExponential_mul
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
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f *
      (subst (MvPowerSeries.X 0) g * subst (MvPowerSeries.X 1) g) =
    subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 0) g *
      (subst (MvPowerSeries.X 1) f * subst (MvPowerSeries.X 1) g)
Tactic:
ring
Proof state after:
no goals
Theorem: PowerSeries.isExponential_mul
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
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ (substAlgHom ⋯) (f * g) = (substAlgHom ⋯) (f * g) * subst (MvPowerSeries.X 1) (f * g)
Tactic:
rw [← coe_substAlgHom (substDomain_of_constantCoeff_zero (by simp))]
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
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ (substAlgHom ⋯) (f * g) = (substAlgHom ⋯) (f * g) * (substAlgHom ⋯) (f * g)
Theorem: PowerSeries.isExponential_mul
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
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ (MvPowerSeries.constantCoeff (Fin 2) R) (MvPowerSeries.X 1) = 0
Tactic:
simp
Proof state after:
no goals
Theorem: PowerSeries.isExponential_mul
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
f g : R⟦X⟧
hf : f.IsExponential
hg : g.IsExponential
⊢ (constantCoeff R) (f * g) = 1
Tactic:
simp only [map_mul, hf.constantCoeff, hg.constantCoeff, mul_one]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_npow
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
f : R⟦X⟧
hf : f.IsExponential
n : ℕ
⊢ (f ^ n).IsExponential
Tactic:
induction n with
| zero =>
  simp only [Nat.zero_eq, pow_zero]
  exact isExponential_one
| succ n hn =>
  rw [pow_succ]
  exact isExponential_mul hn hf
Proof state after:
no goals
Theorem: PowerSeries.isExponential_npow
Proof state before:
case zero
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
f : R⟦X⟧
hf : f.IsExponential
⊢ (f ^ 0).IsExponential
Tactic:
simp only [Nat.zero_eq, pow_zero]
Proof state after:
case zero
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
f : R⟦X⟧
hf : f.IsExponential
⊢ IsExponential 1
Theorem: PowerSeries.isExponential_npow
Proof state before:
case zero
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
f : R⟦X⟧
hf : f.IsExponential
⊢ IsExponential 1
Tactic:
exact isExponential_one
Proof state after:
no goals
Theorem: PowerSeries.isExponential_npow
Proof state before:
case succ
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
f : R⟦X⟧
hf : f.IsExponential
n : ℕ
hn : (f ^ n).IsExponential
⊢ (f ^ (n + 1)).IsExponential
Tactic:
rw [pow_succ]
Proof state after:
case succ
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
f : R⟦X⟧
hf : f.IsExponential
n : ℕ
hn : (f ^ n).IsExponential
⊢ (f ^ n * f).IsExponential
Theorem: PowerSeries.isExponential_npow
Proof state before:
case succ
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
f : R⟦X⟧
hf : f.IsExponential
n : ℕ
hn : (f ^ n).IsExponential
⊢ (f ^ n * f).IsExponential
Tactic:
exact isExponential_mul hn hf
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
⊢ (constantCoeff R) (scale a f) = 1
Tactic:
rw [← coeff_zero_eq_constantCoeff, coeff_scale]
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ a ^ 0 • (coeff R 0) f = 1
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
⊢ a ^ 0 • (coeff R 0) f = 1
Tactic:
simp only [pow_zero, coeff_zero_eq_constantCoeff, one_smul,
  hf.constantCoeff]
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
⊢ subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) (scale a f) =
    subst (MvPowerSeries.X 0) (scale a f) * subst (MvPowerSeries.X 1) (scale a f)
Tactic:
rw [subst_linear_subst_scalar_comm]
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
a : A
f : R⟦X⟧
hf : f.IsExponential
⊢ MvPowerSeries.scale (Function.const (Fin 2) a) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
    subst (MvPowerSeries.X 0) (scale a f) * subst (MvPowerSeries.X 1) (scale a 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 0 + MvPowerSeries.X 1) = 0
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) =
    subst (MvPowerSeries.X 0) (scale a f) * subst (MvPowerSeries.X 1) (scale a 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 0 + MvPowerSeries.X 1) = 0
Tactic:
rw [subst_linear_subst_scalar_comm]
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
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) * subst (MvPowerSeries.X 1) (scale a 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 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:
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) * subst (MvPowerSeries.X 1) (scale a 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 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:
rw [subst_linear_subst_scalar_comm]
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
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