Theorem: toSupported_isHomogeneous' (DividedPowers/DPAlgebra/Misc.lean)

State before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
⊢ GalgHom.isHomogeneous' (MvPolynomial (ℕ × M) R) (weightedHomogeneousSubmodule R Prod.fst) (MvPolynomial (ℕ × M) R)
    (weightedHomogeneousSubmodule R Prod.fst) id ((supported R {nm | 0 < nm.1}).val.comp (toSupported R))
Tactic:
have heq : aeval
  ((supported R {nm : ℕ × M | 0 < nm.fst}).val.toFun ∘
      fun nm : ℕ × M =>
        if h : 0 < nm.fst
        then ⟨X nm, variable_mem_supported R nm h⟩
        else 1) =
    (supported R {nm : ℕ × M | 0 < nm.fst}).val.comp (toSupported R) :=
  by
  apply MvPolynomial.algHom_ext
  intro nm
  simp only [toSupported, AlgHom.toFun_eq_coe, Function.comp_apply, AlgHom.coe_comp, aeval_X]
State after:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
⊢ GalgHom.isHomogeneous' (MvPolynomial (ℕ × M) R) (weightedHomogeneousSubmodule R Prod.fst) (MvPolynomial (ℕ × M) R)
    (weightedHomogeneousSubmodule R Prod.fst) id ((supported R {nm | 0 < nm.1}).val.comp (toSupported R))

State before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
⊢ GalgHom.isHomogeneous' (MvPolynomial (ℕ × M) R) (weightedHomogeneousSubmodule R Prod.fst) (MvPolynomial (ℕ × M) R)
    (weightedHomogeneousSubmodule R Prod.fst) id ((supported R {nm | 0 < nm.1}).val.comp (toSupported R))
Tactic:
rw [← heq]
State after:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
⊢ GalgHom.isHomogeneous' (MvPolynomial (ℕ × M) R) (weightedHomogeneousSubmodule R Prod.fst) (MvPolynomial (ℕ × M) R)
    (weightedHomogeneousSubmodule R Prod.fst) id
    (aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1))

State before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
⊢ GalgHom.isHomogeneous' (MvPolynomial (ℕ × M) R) (weightedHomogeneousSubmodule R Prod.fst) (MvPolynomial (ℕ × M) R)
    (weightedHomogeneousSubmodule R Prod.fst) id
    (aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1))
Tactic:
apply GalgHom.isHomogeneous'_aeval (ℕ × M) (MvPolynomial (ℕ × M) R)
  (weightedHomogeneousSubmodule R Prod.fst) Prod.fst (AddMonoidHom.id ℕ)
State after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
⊢ ∀ (s : ℕ × M),
    ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) s ∈
      weightedHomogeneousSubmodule R Prod.fst ((AddMonoidHom.id ℕ) s.1)

State before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
⊢ aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
Tactic:
apply MvPolynomial.algHom_ext
State after:
case hf
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
⊢ ∀ (i : ℕ × M),
    (aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1))
        (X i) =
      ((supported R {nm | 0 < nm.1}).val.comp (toSupported R)) (X i)

State before:
case hf
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
⊢ ∀ (i : ℕ × M),
    (aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1))
        (X i) =
      ((supported R {nm | 0 < nm.1}).val.comp (toSupported R)) (X i)
Tactic:
intro nm
State after:
case hf
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
nm : ℕ × M
⊢ (aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1))
      (X nm) =
    ((supported R {nm | 0 < nm.1}).val.comp (toSupported R)) (X nm)

State before:
case hf
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
nm : ℕ × M
⊢ (aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1))
      (X nm) =
    ((supported R {nm | 0 < nm.1}).val.comp (toSupported R)) (X nm)
Tactic:
simp only [toSupported, AlgHom.toFun_eq_coe, Function.comp_apply, AlgHom.coe_comp, aeval_X]
State after:
no goals

State before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
⊢ ∀ (s : ℕ × M),
    ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) s ∈
      weightedHomogeneousSubmodule R Prod.fst ((AddMonoidHom.id ℕ) s.1)
Tactic:
intro nm
State after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
⊢ ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) nm ∈
    weightedHomogeneousSubmodule R Prod.fst ((AddMonoidHom.id ℕ) nm.1)

State before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
⊢ ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) nm ∈
    weightedHomogeneousSubmodule R Prod.fst ((AddMonoidHom.id ℕ) nm.1)
Tactic:
simp only [mem_weightedHomogeneousSubmodule, AlgHom.toFun_eq_coe, Subalgebra.coe_val,
  Function.comp_apply, AddMonoidHom.id_apply]
State after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
⊢ IsWeightedHomogeneous Prod.fst (↑(if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1)) nm.1

State before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
⊢ IsWeightedHomogeneous Prod.fst (↑(if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1)) nm.1
Tactic:
split_ifs with h
State after:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : 0 < nm.1
⊢ IsWeightedHomogeneous Prod.fst (↑⟨X nm, ⋯⟩) nm.1

case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : ¬0 < nm.1
⊢ IsWeightedHomogeneous Prod.fst (↑1) nm.1

State before:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : 0 < nm.1
⊢ IsWeightedHomogeneous Prod.fst (↑⟨X nm, ⋯⟩) nm.1
Tactic:
apply isWeightedHomogeneous_X
State after:
no goals

State before:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : ¬0 < nm.1
⊢ IsWeightedHomogeneous Prod.fst (↑1) nm.1
Tactic:
simp only [not_lt, le_zero_iff] at h
State after:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : nm.1 = 0
⊢ IsWeightedHomogeneous Prod.fst (↑1) nm.1

State before:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : nm.1 = 0
⊢ IsWeightedHomogeneous Prod.fst (↑1) nm.1
Tactic:
rw [h, OneMemClass.coe_one]
State after:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : nm.1 = 0
⊢ IsWeightedHomogeneous Prod.fst 1 0

State before:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : nm.1 = 0
⊢ IsWeightedHomogeneous Prod.fst 1 0
Tactic:
apply isWeightedHomogeneous_one
State after:
no goals