Theorem: DividedPowerAlgebra.grade_one_eq_span' (DividedPowers/DPAlgebra/Graded/GradeOne.lean)

State before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ⊤ = Submodule.span R (Set.range fun m => ⟨dp R 1 m, ⋯⟩)
Tactic:
apply Submodule.map_injective_of_injective (grade R M 1).injective_subtype
State after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Submodule.map (grade R M 1).subtype ⊤ =
    Submodule.map (grade R M 1).subtype (Submodule.span R (Set.range fun m => ⟨dp R 1 m, ⋯⟩))

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Submodule.map (grade R M 1).subtype ⊤ =
    Submodule.map (grade R M 1).subtype (Submodule.span R (Set.range fun m => ⟨dp R 1 m, ⋯⟩))
Tactic:
rw [Submodule.map_subtype_top, Submodule.map_span]
State after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ grade R M 1 = Submodule.span R (⇑(grade R M 1).subtype '' Set.range fun m => ⟨dp R 1 m, ⋯⟩)

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ grade R M 1 = Submodule.span R (⇑(grade R M 1).subtype '' Set.range fun m => ⟨dp R 1 m, ⋯⟩)
Tactic:
simp_rw [grade_one_eq_span R M]
State after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Submodule.span R (Set.range (dp R 1)) = Submodule.span R (⇑(grade R M 1).subtype '' Set.range fun m => ⟨dp R 1 m, ⋯⟩)

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Submodule.span R (Set.range (dp R 1)) = Submodule.span R (⇑(grade R M 1).subtype '' Set.range fun m => ⟨dp R 1 m, ⋯⟩)
Tactic:
rw [← Set.range_comp]
State after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Submodule.span R (Set.range (dp R 1)) = Submodule.span R (Set.range (⇑(grade R M 1).subtype ∘ fun m => ⟨dp R 1 m, ⋯⟩))

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Submodule.span R (Set.range (dp R 1)) = Submodule.span R (Set.range (⇑(grade R M 1).subtype ∘ fun m => ⟨dp R 1 m, ⋯⟩))
Tactic:
rfl
State after:
no goals