internlm/Lean-Github huggingface dataset:
Theorem: PowerSeries.forall_congr_curry₀
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
α : Type u_4
inst✝ : Zero α
p : (Fin 2 →₀ α) → Prop
q : α → α → Prop
H : ∀ (e : Fin 2 →₀ α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
hpq :
  p
      (Finsupp.equivFunOnFinite.symm fun x =>
        match x with
        | 0 => u
        | 1 => v) ↔
    q u v
⊢ q u v
Tactic:
rw [← hpq]
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
α : Type u_4
inst✝ : Zero α
p : (Fin 2 →₀ α) → Prop
q : α → α → Prop
H : ∀ (e : Fin 2 →₀ α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
hpq :
  p
      (Finsupp.equivFunOnFinite.symm fun x =>
        match x with
        | 0 => u
        | 1 => v) ↔
    q u v
⊢ p
    (Finsupp.equivFunOnFinite.symm fun x =>
      match x with
      | 0 => u
      | 1 => v)
Theorem: PowerSeries.forall_congr_curry₀
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
α : Type u_4
inst✝ : Zero α
p : (Fin 2 →₀ α) → Prop
q : α → α → Prop
H : ∀ (e : Fin 2 →₀ α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
hpq :
  p
      (Finsupp.equivFunOnFinite.symm fun x =>
        match x with
        | 0 => u
        | 1 => v) ↔
    q u v
⊢ p
    (Finsupp.equivFunOnFinite.symm fun x =>
      match x with
      | 0 => u
      | 1 => v)
Tactic:
apply H
Proof state after:
no goals
Theorem: PowerSeries.forall_congr_curry₀
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
α : Type u_4
inst✝ : Zero α
p : (Fin 2 →₀ α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 →₀ α), p e ↔ q (e 0) (e 1)
⊢ (∀ (u v : α), q u v) → ∀ (e : Fin 2 →₀ α), p e
Tactic:
intro H e
Proof state after:
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
α : Type u_4
inst✝ : Zero α
p : (Fin 2 →₀ α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 →₀ α), p e ↔ q (e 0) (e 1)
H : ∀ (u v : α), q u v
e : Fin 2 →₀ α
⊢ p e
Theorem: PowerSeries.forall_congr_curry₀
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
α : Type u_4
inst✝ : Zero α
p : (Fin 2 →₀ α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 →₀ α), p e ↔ q (e 0) (e 1)
H : ∀ (u v : α), q u v
e : Fin 2 →₀ α
⊢ p e
Tactic:
rw [hpq]
Proof state after:
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
α : Type u_4
inst✝ : Zero α
p : (Fin 2 →₀ α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 →₀ α), p e ↔ q (e 0) (e 1)
H : ∀ (u v : α), q u v
e : Fin 2 →₀ α
⊢ q (e 0) (e 1)
Theorem: PowerSeries.forall_congr_curry₀
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
α : Type u_4
inst✝ : Zero α
p : (Fin 2 →₀ α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 →₀ α), p e ↔ q (e 0) (e 1)
H : ∀ (u v : α), q u v
e : Fin 2 →₀ α
⊢ q (e 0) (e 1)
Tactic:
apply H
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
he' :
  ∀ (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
⊢ subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f = subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f ↔
    ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff R (p + q)) f = (coeff R p) f * (coeff R q) f
Tactic:
rw [MvPowerSeries.ext_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⟧
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
he' :
  ∀ (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
⊢ (∀ (n : Fin 2 →₀ ℕ),
      (MvPowerSeries.coeff R n) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
        (MvPowerSeries.coeff R n) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f)) ↔
    ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff R (p + q)) f = (coeff R p) f * (coeff R q) 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
he' :
  ∀ (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
⊢ (∀ (n : Fin 2 →₀ ℕ),
      (MvPowerSeries.coeff R n) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
        (MvPowerSeries.coeff R n) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f)) ↔
    ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff R (p + q)) f = (coeff R p) f * (coeff R q) f
Tactic:
convert forall_congr_curry₀ _
Proof state after:
case convert_5
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
he' :
  ∀ (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
⊢ ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
        (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) ↔
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f = (coeff R (e 0)) f * (coeff R (e 1)) f
Theorem: PowerSeries.isExponential_add_mul_iff
Proof state before:
case convert_5
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
he' :
  ∀ (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
⊢ ∀ (e : Fin 2 →₀ ℕ),
    (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
        (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) ↔
      ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f = (coeff R (e 0)) f * (coeff R (e 1)) f
Tactic:
intro e
Proof state after:
case convert_5
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
he' :
  ∀ (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
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) ↔
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f = (coeff R (e 0)) f * (coeff R (e 1)) f
Theorem: PowerSeries.isExponential_add_mul_iff
Proof state before:
case convert_5
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
he' :
  ∀ (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
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f) =
      (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f) ↔
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f = (coeff R (e 0)) f * (coeff R (e 1)) f
Tactic:
rw [he, he']
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 →₀ ℕ),
    (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
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⟧
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
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.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
Tactic:
rw [PowerSeries.subst, MvPowerSeries.coeff_subst _]
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⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff R d) f •
        (MvPowerSeries.coeff R e) (d.prod fun s e => (MvPowerSeries.X 0 + MvPowerSeries.X 1) ^ e) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

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
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 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff R d) f •
        (MvPowerSeries.coeff R e) (d.prod fun s e => (MvPowerSeries.X 0 + MvPowerSeries.X 1) ^ e) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

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:
simp only [Fin.isValue, Finsupp.prod_pow, Finset.univ_unique,
  PUnit.default_eq_unit, Finset.prod_singleton, smul_eq_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⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff R d) f * (MvPowerSeries.coeff R e) ((MvPowerSeries.X 0 + MvPowerSeries.X 1) ^ d PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

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
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 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff R d) f * (MvPowerSeries.coeff R e) ((MvPowerSeries.X 0 + MvPowerSeries.X 1) ^ d PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

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:
simp only [← MvPolynomial.coe_X, ← MvPolynomial.coe_add, ← MvPolynomial.coe_pow, MvPolynomial.coeff_coe]
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⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff R d) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ d PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

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
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 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff R d) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ d PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

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:
rw [finsum_eq_single _ (Finsupp.single () (e 0 + e 1)), mul_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
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ (Finsupp.single () (e 0 + e 1)) PUnit.unit) *
      (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + e 1)) f

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 →₀ ℕ),
    x ≠ Finsupp.single () (e 0 + e 1) →
      (MvPowerSeries.coeff R x) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ x PUnit.unit) = 0

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
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 →₀ ℕ
⊢ MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ (Finsupp.single () (e 0 + e 1)) PUnit.unit) *
      (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f =
    ↑((e 0 + e 1).choose (e 0)) * (coeff R (e 0 + 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⟧
e : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ (Finsupp.single () (e 0 + e 1)) PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0))

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⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f = (coeff R (e 0 + 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⟧
e : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ (Finsupp.single () (e 0 + e 1)) PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0))

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⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f = (coeff R (e 0 + e 1)) f
Tactic:
simp only [Finsupp.single_add, Finsupp.coe_add, Pi.add_apply, Finsupp.single_eq_same]
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⟧
e : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ (e 0 + e 1)) = ↑((e 0 + e 1).choose (e 0))

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⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f = (coeff R (e 0 + 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⟧
e : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ (e 0 + e 1)) = ↑((e 0 + e 1).choose (e 0))

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⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f = (coeff R (e 0 + e 1)) f
Tactic:
simp only [Fin.isValue, coeff_add_pow e _, Finset.mem_antidiagonal, ↓reduceIte, coeff]
Proof state after:
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⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f = (coeff R (e 0 + e 1)) f
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⟧
e : Fin 2 →₀ ℕ
⊢ (MvPowerSeries.coeff R (Finsupp.single () (e 0 + e 1))) f = (coeff R (e 0 + e 1)) f
Tactic:
rfl
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 →₀ ℕ),
    x ≠ Finsupp.single () (e 0 + e 1) →
      (MvPowerSeries.coeff R x) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ x PUnit.unit) = 0
Tactic:
intro d hd'
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⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
⊢ (MvPowerSeries.coeff R d) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ d PUnit.unit) = 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⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
⊢ (MvPowerSeries.coeff R d) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ d PUnit.unit) = 0
Tactic:
simp [coeff_add_pow]
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⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
⊢ e 0 + e 1 = d PUnit.unit → (MvPowerSeries.coeff R d) f * ↑((d PUnit.unit).choose (e 0)) = 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⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
⊢ e 0 + e 1 = d PUnit.unit → (MvPowerSeries.coeff R d) f * ↑((d PUnit.unit).choose (e 0)) = 0
Tactic:
intro hd
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⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ (MvPowerSeries.coeff R d) f * ↑((d PUnit.unit).choose (e 0)) = 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⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ (MvPowerSeries.coeff R d) f * ↑((d PUnit.unit).choose (e 0)) = 0
Tactic:
exfalso
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⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ False
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 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ False
Tactic:
apply hd'
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⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ d = Finsupp.single () (e 0 + e 1)
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 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ d = Finsupp.single () (e 0 + e 1)
Tactic:
ext
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⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ d default = (Finsupp.single () (e 0 + e 1)) default
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⟧
e : Fin 2 →₀ ℕ
d : Unit →₀ ℕ
hd' : d ≠ Finsupp.single () (e 0 + e 1)
hd : e 0 + e 1 = d PUnit.unit
⊢ d default = (Finsupp.single () (e 0 + e 1)) default
Tactic:
simp only [PUnit.default_eq_unit, hd, Finsupp.single_eq_same]
Proof state after:
no goals