internlm/Lean-Github huggingface dataset:
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
case h.H
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
⊢ (quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i =
    LinearMap.id ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i
Tactic:
ext y
Proof state after:
case h.H.h
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
⊢ ((quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y =
    (LinearMap.id ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
case h.H.h
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
⊢ ((quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y =
    (LinearMap.id ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
obtain ⟨x, hx, hxy⟩ := y.prop
Proof state after:
case h.H.h.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ ((quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y =
    (LinearMap.id ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
case h.H.h.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ ((quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y =
    (LinearMap.id ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
simp only [LinearMap.coe_comp, comp_apply, LinearMap.id_comp, lof_eq_of, coeLinearMap_of]
Proof state after:
case h.H.h.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (quotDecompose R 𝒜 hI) ↑y = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
case h.H.h.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (quotDecompose R 𝒜 hI) ↑y = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
rw [← hxy, Ideal.Quotient.mkₐ_eq_mk, Ideal.quotDecomposeLaux_apply_mk, Ideal.quotDecomposeLaux]
Proof state after:
case h.H.h.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (lmap' (quotCompMap R 𝒜 I) ∘ₗ (decomposeAlgEquiv 𝒜).toLinearMap) x = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
case h.H.h.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (lmap' (quotCompMap R 𝒜 I) ∘ₗ (decomposeAlgEquiv 𝒜).toLinearMap) x = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
simp only [LinearMap.coe_comp, comp_apply]
Proof state after:
case h.H.h.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (lmap' (quotCompMap R 𝒜 I)) ((decomposeAlgEquiv 𝒜).toLinearMap x) = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
case h.H.h.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (lmap' (quotCompMap R 𝒜 I)) ((decomposeAlgEquiv 𝒜).toLinearMap x) = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
change lmap' _ (decompose 𝒜 x) = _
Proof state after:
case h.H.h.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (lmap' (quotCompMap R 𝒜 I)) ((decompose 𝒜) x) = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
case h.H.h.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (lmap' (quotCompMap R 𝒜 I)) ((decompose 𝒜) x) = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
suffices decompose 𝒜 x = lof R ι (fun i => 𝒜 i) i (⟨x, hx⟩ : 𝒜 i) by
  rw [this, lmap'_lof, lof_eq_of]
  apply congr_arg₂ _ rfl
  rw [quotCompMap]
  simp only [Ideal.Quotient.mkₐ_eq_mk, Submodule.coe_mk, LinearMap.coe_mk]
  rw [← Subtype.coe_inj, Subtype.coe_mk, ← hxy]
  simp only [Ideal.Quotient.mkₐ_eq_mk]
  rfl
Proof state after:
case h.H.h.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
case h.H.h.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
Tactic:
conv_lhs => rw [← Subtype.coe_mk x hx]
Proof state after:
case h.H.h.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (decompose 𝒜) ↑⟨x, hx⟩ = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
case h.H.h.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (decompose 𝒜) ↑⟨x, hx⟩ = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
Tactic:
rw [decompose_coe, lof_eq_of]
Proof state after:
no goals
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ (lmap' (quotCompMap R 𝒜 I)) ((decompose 𝒜) x) = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
rw [this, lmap'_lof, lof_eq_of]
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) ((quotCompMap R 𝒜 I i) ⟨x, hx⟩) =
    (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) ((quotCompMap R 𝒜 I i) ⟨x, hx⟩) =
    (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
apply congr_arg₂ _ rfl
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ (quotCompMap R 𝒜 I i) ⟨x, hx⟩ = y
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ (quotCompMap R 𝒜 I i) ⟨x, hx⟩ = y
Tactic:
rw [quotCompMap]
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ { toFun := fun u => ⟨(Quotient.mkₐ R I) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⟨x, hx⟩ = y
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ { toFun := fun u => ⟨(Quotient.mkₐ R I) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⟨x, hx⟩ = y
Tactic:
simp only [Ideal.Quotient.mkₐ_eq_mk, Submodule.coe_mk, LinearMap.coe_mk]
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ { toFun := fun u => ⟨(Quotient.mk I) ↑u, ⋯⟩, map_add' := ⋯ } ⟨x, hx⟩ = y
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ { toFun := fun u => ⟨(Quotient.mk I) ↑u, ⋯⟩, map_add' := ⋯ } ⟨x, hx⟩ = y
Tactic:
rw [← Subtype.coe_inj, Subtype.coe_mk, ← hxy]
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ ↑({ toFun := fun u => ⟨(Quotient.mk I) ↑u, ⋯⟩, map_add' := ⋯ } ⟨x, hx⟩) = (Quotient.mkₐ R I) x
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ ↑({ toFun := fun u => ⟨(Quotient.mk I) ↑u, ⋯⟩, map_add' := ⋯ } ⟨x, hx⟩) = (Quotient.mkₐ R I) x
Tactic:
simp only [Ideal.Quotient.mkₐ_eq_mk]
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ ↑({ toFun := fun u => ⟨(Quotient.mk I) ↑u, ⋯⟩, map_add' := ⋯ } ⟨x, hx⟩) = (Quotient.mk I) x
Theorem: Ideal.quotDecomposition_right_inv'
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
A : Type u_3
inst✝³ : CommRing A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ ↑({ toFun := fun u => ⟨(Quotient.mk I) ↑u, ⋯⟩, map_add' := ⋯ } ⟨x, hx⟩) = (Quotient.mk I) x
Tactic:
rfl
Proof state after:
no goals
Theorem: Ideal.mem_quotSubmodule_iff
Proof state before:
R : Type u_1
inst✝⁵ : CommRing R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
i : ι
g : A ⧸ I
⊢ g ∈ quotSubmodule R 𝒜 I i ↔ ∃ a ∈ 𝒜 i, (Quotient.mk I) a = g
Tactic:
rw [Ideal.quotSubmodule, Submodule.mem_map, Ideal.Quotient.mkₐ_eq_mk]
Proof state after:
no goals
Theorem: Submodule.mem_span_iff_exists_sum
Proof state before:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → M
x : M
⊢ x ∈ span R (Set.range f) ↔ ∃ a, (a.sum fun i c => c • f i) = x
Tactic:
rw [← top_smul (span R (Set.range f)), mem_ideal_smul_span_iff_exists_sum]
Proof state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ ⊤), (a.sum fun i c => c • f i) = x) ↔ ∃ a, (a.sum fun i c => c • f i) = x
Theorem: Submodule.mem_span_iff_exists_sum
Proof state before:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ι), a i ∈ ⊤), (a.sum fun i c => c • f i) = x) ↔ ∃ a, (a.sum fun i c => c • f i) = x
Tactic:
exact exists_congr fun a => ⟨fun ⟨_, h⟩ => h, fun h => ⟨fun i => mem_top, h⟩⟩
Proof state after:
no goals
Theorem: Submodule.mem_span_iff_exists_sum'
Proof state before:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
⊢ x ∈ span R (f '' s) ↔ ∃ a, (a.sum fun i c => c • f ↑i) = x
Tactic:
rw [← top_smul (span R (f '' s)), mem_ideal_smul_span_iff_exists_sum']
Proof state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) ↔ ∃ a, (a.sum fun i c => c • f ↑i) = x
Theorem: Submodule.mem_span_iff_exists_sum'
Proof state before:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) ↔ ∃ a, (a.sum fun i c => c • f ↑i) = x
Tactic:
apply exists_congr
Proof state after:
case h
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
⊢ ∀ (a : ↑s →₀ R), (∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) ↔ (a.sum fun i c => c • f ↑i) = x
Theorem: Submodule.mem_span_iff_exists_sum'
Proof state before:
case h
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
⊢ ∀ (a : ↑s →₀ R), (∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) ↔ (a.sum fun i c => c • f ↑i) = x
Tactic:
intro a
Proof state after:
case h
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) ↔ (a.sum fun i c => c • f ↑i) = x
Theorem: Submodule.mem_span_iff_exists_sum'
Proof state before:
case h
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) ↔ (a.sum fun i c => c • f ↑i) = x
Tactic:
constructor
Proof state after:
case h.mp
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) → (a.sum fun i c => c • f ↑i) = x

case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (a.sum fun i c => c • f ↑i) = x → ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x
Theorem: Submodule.mem_span_iff_exists_sum'
Proof state before:
case h.mp
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) → (a.sum fun i c => c • f ↑i) = x

case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (a.sum fun i c => c • f ↑i) = x → ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x
Tactic:
. rintro ⟨_, h⟩
  exact h
Proof state after:
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (a.sum fun i c => c • f ↑i) = x → ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x
Theorem: Submodule.mem_span_iff_exists_sum'
Proof state before:
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (a.sum fun i c => c • f ↑i) = x → ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x
Tactic:
. intro h
  simp only [mem_top, Subtype.forall, implies_true, exists_prop, true_and]
  exact h
Proof state after:
no goals
Theorem: Submodule.mem_span_iff_exists_sum'
Proof state before:
case h.mp
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x) → (a.sum fun i c => c • f ↑i) = x
Tactic:
rintro ⟨_, h⟩
Proof state after:
case h.mp.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
w✝ : ∀ (i : ↑s), a i ∈ ⊤
h : (a.sum fun i c => c • f ↑i) = x
⊢ (a.sum fun i c => c • f ↑i) = x
Theorem: Submodule.mem_span_iff_exists_sum'
Proof state before:
case h.mp.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
w✝ : ∀ (i : ↑s), a i ∈ ⊤
h : (a.sum fun i c => c • f ↑i) = x
⊢ (a.sum fun i c => c • f ↑i) = x
Tactic:
exact h
Proof state after:
no goals
Theorem: Submodule.mem_span_iff_exists_sum'
Proof state before:
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
⊢ (a.sum fun i c => c • f ↑i) = x → ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x
Tactic:
intro h
Proof state after:
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
h : (a.sum fun i c => c • f ↑i) = x
⊢ ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x