internlm/Lean-Github huggingface dataset:
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⟧
e : Fin 2 →₀ ℕ
⊢ MvPowerSeries.SubstDomain fun x => MvPowerSeries.X 0 + MvPowerSeries.X 1
Tactic:
exact MvPowerSeries.substDomain_of_constantCoeff_zero
      (fun _ ↦ by 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⟧
e : Fin 2 →₀ ℕ
x✝ : Unit
⊢ (MvPowerSeries.constantCoeff (Fin 2) R) (MvPowerSeries.X 0 + MvPowerSeries.X 1) = 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 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) =
      (coeff R (e 0)) f * (coeff R (e 1)) f
Tactic:
intro e
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⟧
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 →₀ ℕ
⊢ (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) =
    (coeff R (e 0)) f * (coeff R (e 1)) f
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 →₀ ℕ
⊢ (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) =
    (coeff R (e 0)) f * (coeff R (e 1)) f
Tactic:
rw [MvPowerSeries.coeff_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 : 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 →₀ ℕ
⊢ ∑ p ∈ Finset.antidiagonal e,
      (MvPowerSeries.coeff R p.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R p.2) (subst (MvPowerSeries.X 1) f) =
    (coeff R (e 0)) f * (coeff R (e 1)) f
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 →₀ ℕ
⊢ ∑ p ∈ Finset.antidiagonal e,
      (MvPowerSeries.coeff R p.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R p.2) (subst (MvPowerSeries.X 1) f) =
    (coeff R (e 0)) f * (coeff R (e 1)) f
Tactic:
rw [Finset.sum_eq_single (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))]
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⟧
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 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
    (coeff R (e 0)) f * (coeff R (e 1)) f

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 →₀ ℕ
⊢ ∀ b ∈ Finset.antidiagonal e,
    b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) →
      (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
          (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
        0

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 →₀ ℕ
⊢ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e →
    (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
      0
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 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
    (coeff R (e 0)) f * (coeff R (e 1)) f
Tactic:
apply congr_arg₂
Proof state after:
case hx
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 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) =
    (coeff R (e 0)) f

case hy
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 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
    (coeff R (e 1)) f
Theorem: PowerSeries.isExponential_add_mul_iff
Proof state before:
case hx
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 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) =
    (coeff R (e 0)) f
Tactic:
simp only [coeff_subst_single, Finsupp.single_eq_same, if_pos]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_add_mul_iff
Proof state before:
case hy
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 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
    (coeff R (e 1)) f
Tactic:
simp only [coeff_subst_single, Finsupp.single_eq_same, if_pos]
Proof state after:
no goals
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 →₀ ℕ
⊢ ∀ b ∈ Finset.antidiagonal e,
    b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) →
      (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
          (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
        0
Tactic:
intro b hb hb'
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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ Finset.antidiagonal e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
⊢ (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
    0
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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ Finset.antidiagonal e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
⊢ (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
    0
Tactic:
rw [Finset.mem_antidiagonal] at hb
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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
⊢ (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
    0
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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
⊢ (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
    0
Tactic:
by_contra hmul_ne_zero
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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
⊢ False
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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
⊢ False
Tactic:
rcases ne_zero_of_mul_ne_zero hmul_ne_zero with ⟨h0, h1⟩
Proof state after:
case h₀.intro
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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) ≠ 0
h1 : (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) ≠ 0
⊢ False
Theorem: PowerSeries.isExponential_add_mul_iff
Proof state before:
case h₀.intro
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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : (MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) ≠ 0
h1 : (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) ≠ 0
⊢ False
Tactic:
simp only [Fin.isValue, coeff_subst_single, ne_eq, ite_eq_right_iff,
  not_forall, exists_prop] at h0 h1
Proof state after:
case h₀.intro
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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : b.1 = Finsupp.single 0 (b.1 0) ∧ ¬(coeff R (b.1 0)) f = 0
h1 : b.2 = Finsupp.single 1 (b.2 1) ∧ ¬(coeff R (b.2 1)) f = 0
⊢ False
Theorem: PowerSeries.isExponential_add_mul_iff
Proof state before:
case h₀.intro
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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : b.1 = Finsupp.single 0 (b.1 0) ∧ ¬(coeff R (b.1 0)) f = 0
h1 : b.2 = Finsupp.single 1 (b.2 1) ∧ ¬(coeff R (b.2 1)) f = 0
⊢ False
Tactic:
apply hb'
Proof state after:
case h₀.intro
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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : b.1 = Finsupp.single 0 (b.1 0) ∧ ¬(coeff R (b.1 0)) f = 0
h1 : b.2 = Finsupp.single 1 (b.2 1) ∧ ¬(coeff R (b.2 1)) f = 0
⊢ b = (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
Theorem: PowerSeries.isExponential_add_mul_iff
Proof state before:
case h₀.intro
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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : b.1 = Finsupp.single 0 (b.1 0) ∧ ¬(coeff R (b.1 0)) f = 0
h1 : b.2 = Finsupp.single 1 (b.2 1) ∧ ¬(coeff R (b.2 1)) f = 0
⊢ b = (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
Tactic:
rw [Prod.ext_iff, ← hb, h0.1, h1.1]
Proof state after:
case h₀.intro
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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : b.1 = Finsupp.single 0 (b.1 0) ∧ ¬(coeff R (b.1 0)) f = 0
h1 : b.2 = Finsupp.single 1 (b.2 1) ∧ ¬(coeff R (b.2 1)) f = 0
⊢ Finsupp.single 0 (b.1 0) =
      (Finsupp.single 0 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 0),
          Finsupp.single 1 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 1)).1 ∧
    Finsupp.single 1 (b.2 1) =
      (Finsupp.single 0 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 0),
          Finsupp.single 1 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 1)).2
Theorem: PowerSeries.isExponential_add_mul_iff
Proof state before:
case h₀.intro
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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b.1 + b.2 = e
hb' : b ≠ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1))
hmul_ne_zero :
  ¬(MvPowerSeries.coeff R b.1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R b.2) (subst (MvPowerSeries.X 1) f) =
      0
h0 : b.1 = Finsupp.single 0 (b.1 0) ∧ ¬(coeff R (b.1 0)) f = 0
h1 : b.2 = Finsupp.single 1 (b.2 1) ∧ ¬(coeff R (b.2 1)) f = 0
⊢ Finsupp.single 0 (b.1 0) =
      (Finsupp.single 0 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 0),
          Finsupp.single 1 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 1)).1 ∧
    Finsupp.single 1 (b.2 1) =
      (Finsupp.single 0 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 0),
          Finsupp.single 1 ((Finsupp.single 0 (b.1 0) + Finsupp.single 1 (b.2 1)) 1)).2
Tactic:
simp
Proof state after:
no goals
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 →₀ ℕ
⊢ (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)) ∉ Finset.antidiagonal e →
    (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) *
        (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
      0
Tactic:
intro he
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
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
    0
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
⊢ (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).1) (subst (MvPowerSeries.X 0) f) *
      (MvPowerSeries.coeff R (Finsupp.single 0 (e 0), Finsupp.single 1 (e 1)).2) (subst (MvPowerSeries.X 1) f) =
    0
Tactic:
exfalso
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
⊢ False
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
⊢ False
Tactic:
apply he
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)) ∈ Finset.antidiagonal e