Theorem: DividedPowerAlgebra.mem_grade_iff' (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
n : ℕ
p : DividedPowerAlgebra R M
⊢ p ∈ grade R M n ↔ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p
Tactic:
constructor
State after:
case mp
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 : ℕ
p : DividedPowerAlgebra R M
⊢ p ∈ grade R M n → ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p

case mpr
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 : ℕ
p : DividedPowerAlgebra R M
⊢ (∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p) → p ∈ grade R M n

State before:
case mp
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 : ℕ
p : DividedPowerAlgebra R M
⊢ p ∈ grade R M n → ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p

case mpr
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 : ℕ
p : DividedPowerAlgebra R M
⊢ (∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p) → p ∈ grade R M n
Tactic:
. intro hp
  rw [← Submodule.coe_mk p hp]
  apply surjective_of_supported'
State after:
case mpr
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 : ℕ
p : DividedPowerAlgebra R M
⊢ (∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p) → p ∈ grade R M n

State before:
case mpr
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 : ℕ
p : DividedPowerAlgebra R M
⊢ (∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p) → p ∈ grade R M n
Tactic:
. rintro ⟨q, hq, rfl⟩
  exact ⟨q, hq, rfl⟩
State after:
no goals

State before:
case mp
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 : ℕ
p : DividedPowerAlgebra R M
⊢ p ∈ grade R M n → ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p
Tactic:
intro hp
State after:
case mp
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 : ℕ
p : DividedPowerAlgebra R M
hp : p ∈ grade R M n
⊢ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p

State before:
case mp
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 : ℕ
p : DividedPowerAlgebra R M
hp : p ∈ grade R M n
⊢ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p
Tactic:
rw [← Submodule.coe_mk p hp]
State after:
case mp
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 : ℕ
p : DividedPowerAlgebra R M
hp : p ∈ grade R M n
⊢ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = ↑⟨p, hp⟩

State before:
case mp
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 : ℕ
p : DividedPowerAlgebra R M
hp : p ∈ grade R M n
⊢ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = ↑⟨p, hp⟩
Tactic:
apply surjective_of_supported'
State after:
no goals

State before:
case mpr
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 : ℕ
p : DividedPowerAlgebra R M
⊢ (∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p) → p ∈ grade R M n
Tactic:
rintro ⟨q, hq, rfl⟩
State after:
case mpr.intro.intro
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 : ℕ
q : ↥(supported R {nm | 0 < nm.1})
hq : IsWeightedHomogeneous Prod.fst (↑q) n
⊢ mk ↑q ∈ grade R M n

State before:
case mpr.intro.intro
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 : ℕ
q : ↥(supported R {nm | 0 < nm.1})
hq : IsWeightedHomogeneous Prod.fst (↑q) n
⊢ mk ↑q ∈ grade R M n
Tactic:
exact ⟨q, hq, rfl⟩
State after:
no goals