Theorem: MvPolynomial.coeff_baseChange_apply (DividedPowers/DPAlgebra/BaseChange.lean)

State before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
m : σ →₀ ℕ
φ : S →ₐ[R] S'
f : MvPolynomial σ S
⊢ coeff m ((baseChange φ) f) = φ (coeff m f)
Tactic:
rw [baseChange, AlgHom.coe_mk, coe_eval₂RingHom]
State after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
m : σ →₀ ℕ
φ : S →ₐ[R] S'
f : MvPolynomial σ S
⊢ coeff m (eval₂ (C.comp ↑φ) X f) = φ (coeff m f)

State before:
case h_C
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
r : S
m : σ →₀ ℕ
⊢ coeff m (eval₂ (C.comp ↑φ) X (C r)) = φ (coeff m (C r))
Tactic:
simp only [eval₂_C, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, coeff_C]
State after:
case h_C
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
r : S
m : σ →₀ ℕ
⊢ (if 0 = m then φ r else 0) = φ (if 0 = m then r else 0)

State before:
case h_C
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
r : S
m : σ →₀ ℕ
⊢ (if 0 = m then φ r else 0) = φ (if 0 = m then r else 0)
Tactic:
split_ifs
State after:
case pos
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
r : S
m : σ →₀ ℕ
h✝ : 0 = m
⊢ φ r = φ r

case neg
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
r : S
m : σ →₀ ℕ
h✝ : ¬0 = m
⊢ 0 = φ 0

State before:
case pos
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
r : S
m : σ →₀ ℕ
h✝ : 0 = m
⊢ φ r = φ r
Tactic:
rfl
State after:
no goals

State before:
case neg
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
r : S
m : σ →₀ ℕ
h✝ : ¬0 = m
⊢ 0 = φ 0
Tactic:
rw [map_zero]
State after:
no goals

State before:
case h_add
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
f g : MvPolynomial σ S
hf : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X f) = φ (coeff m f)
hg : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X g) = φ (coeff m g)
m : σ →₀ ℕ
⊢ coeff m (eval₂ (C.comp ↑φ) X (f + g)) = φ (coeff m (f + g))
Tactic:
simp only [eval₂_add, coeff_add, hf, hg, map_add]
State after:
no goals

State before:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
⊢ coeff m (eval₂ (C.comp ↑φ) X (p * X s)) = φ (coeff m (p * X s))
Tactic:
simp only [eval₂_mul, eval₂_X, coeff_mul, map_sum, _root_.map_mul]
State after:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
⊢ ∑ x ∈ Finset.antidiagonal m, coeff x.1 (eval₂ (C.comp ↑φ) X p) * coeff x.2 (X s) =
    ∑ x ∈ Finset.antidiagonal m, φ (coeff x.1 p) * φ (coeff x.2 (X s))

State before:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
⊢ ∑ x ∈ Finset.antidiagonal m, coeff x.1 (eval₂ (C.comp ↑φ) X p) * coeff x.2 (X s) =
    ∑ x ∈ Finset.antidiagonal m, φ (coeff x.1 p) * φ (coeff x.2 (X s))
Tactic:
apply Finset.sum_congr rfl
State after:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
⊢ ∀ x ∈ Finset.antidiagonal m,
    coeff x.1 (eval₂ (C.comp ↑φ) X p) * coeff x.2 (X s) = φ (coeff x.1 p) * φ (coeff x.2 (X s))

State before:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
⊢ ∀ x ∈ Finset.antidiagonal m,
    coeff x.1 (eval₂ (C.comp ↑φ) X p) * coeff x.2 (X s) = φ (coeff x.1 p) * φ (coeff x.2 (X s))
Tactic:
intro x _
State after:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
⊢ coeff x.1 (eval₂ (C.comp ↑φ) X p) * coeff x.2 (X s) = φ (coeff x.1 p) * φ (coeff x.2 (X s))

State before:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
⊢ coeff x.1 (eval₂ (C.comp ↑φ) X p) * coeff x.2 (X s) = φ (coeff x.1 p) * φ (coeff x.2 (X s))
Tactic:
simp only [h x.1, coeff_X']
State after:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
⊢ (φ (coeff x.1 p) * if Finsupp.single s 1 = x.2 then 1 else 0) =
    φ (coeff x.1 p) * φ (if Finsupp.single s 1 = x.2 then 1 else 0)

State before:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
⊢ (φ (coeff x.1 p) * if Finsupp.single s 1 = x.2 then 1 else 0) =
    φ (coeff x.1 p) * φ (if Finsupp.single s 1 = x.2 then 1 else 0)
Tactic:
split_ifs
State after:
case pos
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
h✝ : Finsupp.single s 1 = x.2
⊢ φ (coeff x.1 p) * 1 = φ (coeff x.1 p) * φ 1

case neg
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
h✝ : ¬Finsupp.single s 1 = x.2
⊢ φ (coeff x.1 p) * 0 = φ (coeff x.1 p) * φ 0

State before:
case pos
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
h✝ : Finsupp.single s 1 = x.2
⊢ φ (coeff x.1 p) * 1 = φ (coeff x.1 p) * φ 1
Tactic:
rw [_root_.map_one]
State after:
no goals

State before:
case neg
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
h✝ : ¬Finsupp.single s 1 = x.2
⊢ φ (coeff x.1 p) * 0 = φ (coeff x.1 p) * φ 0
Tactic:
rw [_root_.map_zero]
State after:
no goals