Theorem: DividedPowerAlgebra.algebraMapInv_eq (DividedPowers/DPAlgebra/Graded/GradeZero.lean)

State before:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
⊢ (algebraMapInv R M) (mk f) = (aeval fun nm => if 0 < nm.1 then 0 else 1) f
Tactic:
rw [← AlgHom.comp_apply]
State after:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
⊢ ((algebraMapInv R M).comp mk) f = (aeval fun nm => if 0 < nm.1 then 0 else 1) f

State before:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
⊢ ((algebraMapInv R M).comp mk) f = (aeval fun nm => if 0 < nm.1 then 0 else 1) f
Tactic:
apply AlgHom.congr_fun
State after:
case H
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
⊢ (algebraMapInv R M).comp mk = aeval fun nm => if 0 < nm.1 then 0 else 1

State before:
case H
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
⊢ (algebraMapInv R M).comp mk = aeval fun nm => if 0 < nm.1 then 0 else 1
Tactic:
ext ⟨n, m⟩
State after:
case H.hf.mk
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
⊢ ((algebraMapInv R M).comp mk) (X (n, m)) = (aeval fun nm => if 0 < nm.1 then 0 else 1) (X (n, m))

State before:
case H.hf.mk
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
⊢ ((algebraMapInv R M).comp mk) (X (n, m)) = (aeval fun nm => if 0 < nm.1 then 0 else 1) (X (n, m))
Tactic:
simp only [algebraMapInv, AlgHom.comp_apply, aeval_X]
State after:
case H.hf.mk
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = if 0 < n then 0 else 1

State before:
case H.hf.mk
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = if 0 < n then 0 else 1
Tactic:
by_cases hn : 0 < n
State after:
case pos
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : 0 < n
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = if 0 < n then 0 else 1

case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : ¬0 < n
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = if 0 < n then 0 else 1

State before:
case pos
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : 0 < n
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = if 0 < n then 0 else 1
Tactic:
simp only [if_pos hn, liftAlgHom_apply, LinearMap.zero_apply, aeval_X]
State after:
case pos
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : 0 < n
⊢ (dividedPowersBot R).dpow n 0 = 0

State before:
case pos
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : 0 < n
⊢ (dividedPowersBot R).dpow n 0 = 0
Tactic:
rw [DividedPowers.dpow_eval_zero _ (ne_of_gt hn)]
State after:
no goals

State before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : ¬0 < n
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = if 0 < n then 0 else 1
Tactic:
rw [if_neg hn]
State after:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : ¬0 < n
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = 1

State before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : ¬0 < n
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = 1
Tactic:
rw [not_lt, le_zero_iff] at hn
State after:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : n = 0
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = 1

State before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
hn : n = 0
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = 1
Tactic:
simp only [hn, liftAlgHom_apply, LinearMap.zero_apply, aeval_X,
  DividedPowers.dpow_zero _ (mem_bot.mpr rfl)]
State after:
no goals