Theorem: quotDecompose_surjective2 (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
⊢ Surjective ⇑(lmap' (quotCompMap R 𝒜 rel))
Tactic:
apply lmap'_surjective (quotCompMap R 𝒜 rel)
State after:
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
⊢ ∀ (i : ι), Surjective ⇑(quotCompMap R 𝒜 rel i)

State before:
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
⊢ ∀ (i : ι), Surjective ⇑(quotCompMap R 𝒜 rel i)
Tactic:
rintro i ⟨x, ⟨a, ha, rfl⟩⟩
State after:
case mk.intro.intro
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
i : ι
a : A
ha : a ∈ ↑(𝒜 i)
⊢ ∃ a_1, (quotCompMap R 𝒜 rel i) a_1 = ⟨(RingQuot.mkAlgHom R rel) a, ⋯⟩

State before:
case mk.intro.intro
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
i : ι
a : A
ha : a ∈ ↑(𝒜 i)
⊢ ∃ a_1, (quotCompMap R 𝒜 rel i) a_1 = ⟨(RingQuot.mkAlgHom R rel) a, ⋯⟩
Tactic:
exact ⟨⟨a, ha⟩, rfl⟩
State after:
no goals