Theorem: DividedPowerAlgebra.lift_isHomogeneous (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
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
I : Ideal A
hI : DividedPowers I
hI' : HasGradedDpow 𝒜 hI
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
hφ' : ∀ (m : M), φ m ∈ 𝒜 1
⊢ GalgHom.IsHomogeneous (grade R M) 𝒜 (lift hI φ hφ)
Tactic:
apply liftAux_isHomogeneous
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
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
I : Ideal A
hI : DividedPowers I
hI' : HasGradedDpow 𝒜 hI
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
hφ' : ∀ (m : M), φ m ∈ 𝒜 1
⊢ ∀ (n : ℕ) (m : M), hI.dpow (n, m).1 (φ (n, m).2) ∈ 𝒜 n

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
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
I : Ideal A
hI : DividedPowers I
hI' : HasGradedDpow 𝒜 hI
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
hφ' : ∀ (m : M), φ m ∈ 𝒜 1
⊢ ∀ (n : ℕ) (m : M), hI.dpow (n, m).1 (φ (n, m).2) ∈ 𝒜 n
Tactic:
intro n m
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
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
I : Ideal A
hI : DividedPowers I
hI' : HasGradedDpow 𝒜 hI
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
hφ' : ∀ (m : M), φ m ∈ 𝒜 1
n : ℕ
m : M
⊢ hI.dpow (n, m).1 (φ (n, m).2) ∈ 𝒜 n

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
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
I : Ideal A
hI : DividedPowers I
hI' : HasGradedDpow 𝒜 hI
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
hφ' : ∀ (m : M), φ m ∈ 𝒜 1
n : ℕ
m : M
⊢ hI.dpow (n, m).1 (φ (n, m).2) ∈ 𝒜 n
Tactic:
simpa only [Algebra.id.smul_eq_mul, mul_one] using hI' (φ m) (hφ m) 1 (hφ' m) n
State after:
no goals