Theorem: DividedPowerAlgebra.mk_comp_toSupported (DividedPowers/DPAlgebra/Graded/Basic.lean)

State before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ mk.comp ((supported R {nm | 0 < nm.1}).val.comp (toSupported R)) = mk
Tactic:
apply MvPolynomial.algHom_ext
State after:
case hf
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ∀ (i : ℕ × M), (mk.comp ((supported R {nm | 0 < nm.1}).val.comp (toSupported R))) (X i) = mk (X i)

State before:
case hf
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ∀ (i : ℕ × M), (mk.comp ((supported R {nm | 0 < nm.1}).val.comp (toSupported R))) (X i) = mk (X i)
Tactic:
rintro ⟨n, m⟩
State after:
case hf.mk
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
⊢ (mk.comp ((supported R {nm | 0 < nm.1}).val.comp (toSupported R))) (X (n, m)) = mk (X (n, m))

State before:
case hf.mk
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
⊢ (mk.comp ((supported R {nm | 0 < nm.1}).val.comp (toSupported R))) (X (n, m)) = mk (X (n, m))
Tactic:
simp only [AlgHom.coe_comp, mkₐ_eq_mk, Subalgebra.coe_val, Function.comp_apply, aeval_X,
  toSupported]
State after:
case hf.mk
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
⊢ mk ↑(if h : 0 < n then ⟨X (n, m), ⋯⟩ else 1) = mk (X (n, m))

State before:
case hf.mk
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
⊢ mk ↑(if h : 0 < n then ⟨X (n, m), ⋯⟩ else 1) = mk (X (n, m))
Tactic:
split_ifs with h
State after:
case pos
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : 0 < n
⊢ mk ↑⟨X (n, m), ⋯⟩ = mk (X (n, m))

case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : ¬0 < n
⊢ mk ↑1 = mk (X (n, m))

State before:
case pos
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : 0 < n
⊢ mk ↑⟨X (n, m), ⋯⟩ = mk (X (n, m))
Tactic:
rfl
State after:
no goals

State before:
case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : ¬0 < n
⊢ mk ↑1 = mk (X (n, m))
Tactic:
simp only [not_lt, le_zero_iff] at h
State after:
case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : n = 0
⊢ mk ↑1 = mk (X (n, m))

State before:
case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : n = 0
⊢ mk ↑1 = mk (X (n, m))
Tactic:
rw [h, OneMemClass.coe_one, map_one]
State after:
case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : n = 0
⊢ 1 = mk (X (0, m))

State before:
case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : n = 0
⊢ 1 = mk (X (0, m))
Tactic:
exact (dp_zero R m).symm
State after:
no goals