internlm/Lean-Github huggingface dataset:
Theorem: PowerSeries.coeff_subst_single
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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ (MvPowerSeries.coeff R e) (subst (MvPowerSeries.X s) f) = if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0
Tactic:
rw [PowerSeries.coeff_subst (PowerSeries.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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ∑ᶠ (d : ℕ), (coeff R d) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ d) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0
Theorem: PowerSeries.coeff_subst_single
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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ∑ᶠ (d : ℕ), (coeff R d) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ d) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0
Tactic:
rw [finsum_eq_single _ (e s)]
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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ (coeff R (e s)) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ e s) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ∀ (x : ℕ), x ≠ e s → (coeff R x) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ x) = 0
Theorem: PowerSeries.coeff_subst_single
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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ (MvPowerSeries.constantCoeff σ R) (MvPowerSeries.X s) = 0
Tactic:
simp
Proof state after:
no goals
Theorem: PowerSeries.coeff_subst_single
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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ (coeff R (e s)) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ e s) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0
Tactic:
rw [MvPowerSeries.coeff_X_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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ((coeff R (e s)) f • if e = Finsupp.single s (e s) then 1 else 0) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0
Theorem: PowerSeries.coeff_subst_single
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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ((coeff R (e s)) f • if e = Finsupp.single s (e s) then 1 else 0) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0
Tactic:
simp only [Fin.isValue, ↓reduceIte, smul_eq_mul, mul_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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ((coeff R (e s)) f * if e = Finsupp.single s (e s) then 1 else 0) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0
Theorem: PowerSeries.coeff_subst_single
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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ((coeff R (e s)) f * if e = Finsupp.single s (e s) then 1 else 0) =
    if e = Finsupp.single s (e s) then (coeff R (e s)) f else 0
Tactic:
split_ifs with he
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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
he : e = Finsupp.single s (e s)
⊢ (coeff R (e s)) f * 1 = (coeff R (e s)) f

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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
he : ¬e = Finsupp.single s (e s)
⊢ (coeff R (e s)) f * 0 = 0
Theorem: PowerSeries.coeff_subst_single
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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
he : e = Finsupp.single s (e s)
⊢ (coeff R (e s)) f * 1 = (coeff R (e s)) f
Tactic:
rw [mul_one]
Proof state after:
no goals
Theorem: PowerSeries.coeff_subst_single
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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
he : ¬e = Finsupp.single s (e s)
⊢ (coeff R (e s)) f * 0 = 0
Tactic:
rw [mul_zero]
Proof state after:
no goals
Theorem: PowerSeries.coeff_subst_single
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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ∀ (x : ℕ), x ≠ e s → (coeff R x) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ x) = 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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
d : ℕ
hd : d ≠ e s
⊢ (coeff R d) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ d) = 0
Theorem: PowerSeries.coeff_subst_single
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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
d : ℕ
hd : d ≠ e s
⊢ (coeff R d) f • (MvPowerSeries.coeff R e) (MvPowerSeries.X s ^ d) = 0
Tactic:
simp only [MvPowerSeries.coeff_X_pow, smul_eq_mul, mul_ite, mul_one, mul_zero, ite_eq_right_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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
d : ℕ
hd : d ≠ e s
⊢ e = Finsupp.single s d → (coeff R d) f = 0
Theorem: PowerSeries.coeff_subst_single
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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
d : ℕ
hd : d ≠ e s
⊢ e = Finsupp.single s d → (coeff R d) f = 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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
d : ℕ
hd : d ≠ e s
hd' : e = Finsupp.single s d
⊢ (coeff R d) f = 0
Theorem: PowerSeries.coeff_subst_single
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
σ : Type u_4
inst✝¹ : DecidableEq σ
inst✝ : Finite σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
d : ℕ
hd : d ≠ e s
hd' : e = Finsupp.single s d
⊢ (coeff R d) f = 0
Tactic:
simp only [hd', Finsupp.single_eq_same, ne_eq, not_true_eq_false] at hd
Proof state after:
no goals
Theorem: PowerSeries.ne_zero_of_mul_ne_zero
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
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0
Tactic:
constructor
Proof state after:
case left
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
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
⊢ a ≠ 0

case right
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
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
⊢ b ≠ 0
Theorem: PowerSeries.ne_zero_of_mul_ne_zero
Proof state before:
case left
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
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
⊢ a ≠ 0
Tactic:
intro ha
Proof state after:
case left
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
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
ha : a = 0
⊢ False
Theorem: PowerSeries.ne_zero_of_mul_ne_zero
Proof state before:
case left
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
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
ha : a = 0
⊢ False
Tactic:
apply h
Proof state after:
case left
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
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
ha : a = 0
⊢ a * b = 0
Theorem: PowerSeries.ne_zero_of_mul_ne_zero
Proof state before:
case left
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
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
ha : a = 0
⊢ a * b = 0
Tactic:
rw [ha, zero_mul]
Proof state after:
no goals
Theorem: PowerSeries.ne_zero_of_mul_ne_zero
Proof state before:
case right
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
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
⊢ b ≠ 0
Tactic:
intro hb
Proof state after:
case right
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
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
hb : b = 0
⊢ False
Theorem: PowerSeries.ne_zero_of_mul_ne_zero
Proof state before:
case right
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
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
hb : b = 0
⊢ False
Tactic:
apply h
Proof state after:
case right
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
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
hb : b = 0
⊢ a * b = 0
Theorem: PowerSeries.ne_zero_of_mul_ne_zero
Proof state before:
case right
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
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
hb : b = 0
⊢ a * b = 0
Tactic:
rw [hb, mul_zero]
Proof state after:
no goals
Theorem: PowerSeries.forall_congr_curry
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
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
⊢ (∀ (e : Fin 2 → α), p e) ↔ ∀ (u v : α), q u v
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
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
⊢ (∀ (e : Fin 2 → α), p e) → ∀ (u v : α), q u v

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
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
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
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
⊢ (∀ (e : Fin 2 → α), p e) → ∀ (u v : α), q u v
Tactic:
intro H u v
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
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
H : ∀ (e : Fin 2 → α), p e
u v : α
⊢ q u 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
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
H : ∀ (e : Fin 2 → α), p e
u v : α
⊢ q u v
Tactic:
set e : Fin 2 → α := fun
| 0 => u
| 1 => v
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
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
H : ∀ (e : Fin 2 → α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
⊢ q u 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
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
H : ∀ (e : Fin 2 → α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
⊢ q u v
Tactic:
specialize hpq e
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
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 e ↔ q (e 0) (e 1)
⊢ q u 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
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 e ↔ q (e 0) (e 1)
⊢ q u v
Tactic:
simp [e] at 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
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 fun x =>
      match x with
      | 0 => u
      | 1 => v) ↔
    q u v
⊢ q u 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
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 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
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 fun x =>
      match x with
      | 0 => u
      | 1 => v) ↔
    q u v
⊢ p 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
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 fun x =>
      match x with
      | 0 => u
      | 1 => v) ↔
    q u v
⊢ p 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
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
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
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
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
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.forall_congr_curry₀
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
α : Type u_4
inst✝ : Zero α
p : (Fin 2 →₀ α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 →₀ α), p e ↔ q (e 0) (e 1)
⊢ (∀ (e : Fin 2 →₀ α), p e) ↔ ∀ (u v : α), q u v
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
α : Type u_4
inst✝ : Zero α
p : (Fin 2 →₀ α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 →₀ α), p e ↔ q (e 0) (e 1)
⊢ (∀ (e : Fin 2 →₀ α), p e) → ∀ (u v : α), q u v

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
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
hpq : ∀ (e : Fin 2 →₀ α), p e ↔ q (e 0) (e 1)
⊢ (∀ (e : Fin 2 →₀ α), p e) → ∀ (u v : α), q u v
Tactic:
intro H u v
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
hpq : ∀ (e : Fin 2 →₀ α), p e ↔ q (e 0) (e 1)
H : ∀ (e : Fin 2 →₀ α), p e
u v : α
⊢ q u 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
hpq : ∀ (e : Fin 2 →₀ α), p e ↔ q (e 0) (e 1)
H : ∀ (e : Fin 2 →₀ α), p e
u v : α
⊢ q u v
Tactic:
set e : Fin 2 → α := fun
| 0 => u
| 1 => v
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
hpq : ∀ (e : Fin 2 →₀ α), p e ↔ q (e 0) (e 1)
H : ∀ (e : Fin 2 →₀ α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
⊢ q u 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
hpq : ∀ (e : Fin 2 →₀ α), p e ↔ q (e 0) (e 1)
H : ∀ (e : Fin 2 →₀ α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
⊢ q u v
Tactic:
specialize hpq (Finsupp.equivFunOnFinite.symm e)
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 e) ↔ q ((Finsupp.equivFunOnFinite.symm e) 0) ((Finsupp.equivFunOnFinite.symm e) 1)
⊢ q u 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 e) ↔ q ((Finsupp.equivFunOnFinite.symm e) 0) ((Finsupp.equivFunOnFinite.symm e) 1)
⊢ q u v
Tactic:
simp [e] at 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
⊢ q u v