Theorem: quotDecompose'_surjective (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
h𝒜 : GradedAlgebra 𝒜
⊢ Surjective ⇑(quotDecompose' R 𝒜 rel)
Tactic:
intro x
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
h𝒜 : GradedAlgebra 𝒜
x : RingQuot rel
⊢ ∃ a, (quotDecompose' R 𝒜 rel) a = x

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
h𝒜 : GradedAlgebra 𝒜
x : RingQuot rel
⊢ ∃ a, (quotDecompose' R 𝒜 rel) a = x
Tactic:
obtain ⟨a, rfl⟩ := RingQuot.mkAlgHom_surjective R rel x
State after:
case 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
h𝒜 : GradedAlgebra 𝒜
a : A
⊢ ∃ a_1, (quotDecompose' R 𝒜 rel) a_1 = (RingQuot.mkAlgHom R rel) a

State before:
case 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
h𝒜 : GradedAlgebra 𝒜
a : A
⊢ ∃ a_1, (quotDecompose' R 𝒜 rel) a_1 = (RingQuot.mkAlgHom R rel) a
Tactic:
let e : (coeLinearMap 𝒜) ((decomposeAlgEquiv 𝒜).toLinearMap a) = a :=
  h𝒜.left_inv a
State after:
case 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
h𝒜 : GradedAlgebra 𝒜
a : A
e : (coeLinearMap 𝒜) ((decomposeAlgEquiv 𝒜).toLinearMap a) = a := Decomposition.left_inv a
⊢ ∃ a_1, (quotDecompose' R 𝒜 rel) a_1 = (RingQuot.mkAlgHom R rel) a

State before:
case 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
h𝒜 : GradedAlgebra 𝒜
a : A
e : (coeLinearMap 𝒜) ((decomposeAlgEquiv 𝒜).toLinearMap a) = a := Decomposition.left_inv a
⊢ ∃ a_1, (quotDecompose' R 𝒜 rel) a_1 = (RingQuot.mkAlgHom R rel) a
Tactic:
use (lmap' (quotCompMap R 𝒜 rel)) ((decomposeAlgEquiv 𝒜).toLinearMap a)
State after:
case h
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
h𝒜 : GradedAlgebra 𝒜
a : A
e : (coeLinearMap 𝒜) ((decomposeAlgEquiv 𝒜).toLinearMap a) = a := Decomposition.left_inv a
⊢ (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) ((decomposeAlgEquiv 𝒜).toLinearMap a)) =
    (RingQuot.mkAlgHom R rel) a

State before:
case h
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
h𝒜 : GradedAlgebra 𝒜
a : A
e : (coeLinearMap 𝒜) ((decomposeAlgEquiv 𝒜).toLinearMap a) = a := Decomposition.left_inv a
⊢ (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) ((decomposeAlgEquiv 𝒜).toLinearMap a)) =
    (RingQuot.mkAlgHom R rel) a
Tactic:
conv_rhs => rw [← e]
State after:
case h
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
h𝒜 : GradedAlgebra 𝒜
a : A
e : (coeLinearMap 𝒜) ((decomposeAlgEquiv 𝒜).toLinearMap a) = a := Decomposition.left_inv a
⊢ (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) ((decomposeAlgEquiv 𝒜).toLinearMap a)) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) ((decomposeAlgEquiv 𝒜).toLinearMap a))

State before:
case h
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
h𝒜 : GradedAlgebra 𝒜
a : A
e : (coeLinearMap 𝒜) ((decomposeAlgEquiv 𝒜).toLinearMap a) = a := Decomposition.left_inv a
⊢ (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) ((decomposeAlgEquiv 𝒜).toLinearMap a)) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) ((decomposeAlgEquiv 𝒜).toLinearMap a))
Tactic:
apply quotDecompose_left_inv'_aux_apply
State after:
no goals