internlm/Lean-Github huggingface dataset:
Theorem: quotDecompose_left_inv'_aux
Proof 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
⊢ ∀ (i : ι),
    ((coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ
        lof R ι (fun i => ↥(𝒜 i)) i =
      ((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Tactic:
intro i
Proof 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
i : ι
⊢ ((coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ
      lof R ι (fun i => ↥(𝒜 i)) i =
    ((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Theorem: quotDecompose_left_inv'_aux
Proof 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
i : ι
⊢ ((coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ
      lof R ι (fun i => ↥(𝒜 i)) i =
    ((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Tactic:
ext ⟨x, hx⟩
Proof state after:
case H.h.mk
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 : ι
x : A
hx : x ∈ 𝒜 i
⊢ (((coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ
        lof R ι (fun i => ↥(𝒜 i)) i)
      ⟨x, hx⟩ =
    (((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
Theorem: quotDecompose_left_inv'_aux
Proof state before:
case H.h.mk
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 : ι
x : A
hx : x ∈ 𝒜 i
⊢ (((coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ
        lof R ι (fun i => ↥(𝒜 i)) i)
      ⟨x, hx⟩ =
    (((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
Tactic:
simp only [quotCompMap, LinearMap.coe_comp, comp_apply, AlgHom.toLinearMap_apply, lmap'_lof]
Proof state after:
case H.h.mk
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 : ι
x : A
hx : x ∈ 𝒜 i
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))
      ((lof R ι (fun i => ↥(Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))) i)
        ({ toFun := fun u => ⟨(RingQuot.mkAlgHom R rel) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⟨x, hx⟩)) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩))
Theorem: quotDecompose_left_inv'_aux
Proof state before:
case H.h.mk
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 : ι
x : A
hx : x ∈ 𝒜 i
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))
      ((lof R ι (fun i => ↥(Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))) i)
        ({ toFun := fun u => ⟨(RingQuot.mkAlgHom R rel) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⟨x, hx⟩)) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩))
Tactic:
simp only [lof_eq_of, coeLinearMap_of]
Proof state after:
case H.h.mk
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 : ι
x : A
hx : x ∈ 𝒜 i
⊢ ↑({ toFun := fun u => ⟨(RingQuot.mkAlgHom R rel) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⟨x, hx⟩) =
    (RingQuot.mkAlgHom R rel) x
Theorem: quotDecompose_left_inv'_aux
Proof state before:
case H.h.mk
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 : ι
x : A
hx : x ∈ 𝒜 i
⊢ ↑({ toFun := fun u => ⟨(RingQuot.mkAlgHom R rel) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⟨x, hx⟩) =
    (RingQuot.mkAlgHom R rel) x
Tactic:
rfl
Proof state after:
no goals
Theorem: quotDecompose_left_inv'_aux_apply
Proof 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
x : ⨁ (i : ι), ↥(𝒜 i)
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) x) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)
Tactic:
let e := quotDecompose_left_inv'_aux R 𝒜 rel
Proof 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
x : ⨁ (i : ι), ↥(𝒜 i)
e : (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ lmap' (quotCompMap R 𝒜 rel) =
  (RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜 :=
  quotDecompose_left_inv'_aux R 𝒜 rel
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) x) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)
Theorem: quotDecompose_left_inv'_aux_apply
Proof 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
x : ⨁ (i : ι), ↥(𝒜 i)
e : (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ∘ₗ lmap' (quotCompMap R 𝒜 rel) =
  (RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜 :=
  quotDecompose_left_inv'_aux R 𝒜 rel
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) x) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)
Tactic:
simp only [LinearMap.ext_iff, LinearMap.comp_apply, AlgHom.toLinearMap_apply] at e
Proof 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
x : ⨁ (i : ι), ↥(𝒜 i)
e :
  ∀ (x : ⨁ (i : ι), ↥(𝒜 i)),
    (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) x) =
      (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) x) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)
Theorem: quotDecompose_left_inv'_aux_apply
Proof 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
x : ⨁ (i : ι), ↥(𝒜 i)
e :
  ∀ (x : ⨁ (i : ι), ↥(𝒜 i)),
    (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) x) =
      (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)
⊢ (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) x) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)
Tactic:
apply e
Proof state after:
no goals
Theorem: quotDecompose'_apply
Proof 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
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a)
Tactic:
suffices (quotDecompose' R 𝒜 rel).comp (lmap' (quotCompMap R 𝒜 rel)) =
    (RingQuot.mkAlgHom R rel).toLinearMap.comp (coeLinearMap 𝒜) by
  simp only [LinearMap.ext_iff, LinearMap.comp_apply, AlgHom.toLinearMap_apply] at this
  apply this
Proof 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
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel) = (RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜
Theorem: quotDecompose'_apply
Proof 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
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel) = (RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜
Tactic:
apply linearMap_ext
Proof 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
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ ∀ (i : ι),
    (quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
      ((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Theorem: quotDecompose'_apply
Proof 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
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ ∀ (i : ι),
    (quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
      ((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Tactic:
intro i
Proof 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
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ (quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
    ((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Theorem: quotDecompose'_apply
Proof 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
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ (quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
    ((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Tactic:
ext ⟨x, hx⟩
Proof state after:
case H.h.mk
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
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ ((quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩ =
    (((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
Theorem: quotDecompose'_apply
Proof state before:
case H.h.mk
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
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ ((quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩ =
    (((RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
Tactic:
simp only [quotDecompose', LinearMap.coe_comp, comp_apply, AlgHom.toLinearMap_apply,
  lmap'_lof, toModule_lof]
Proof state after:
case H.h.mk
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
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ (quotSubmodule R 𝒜 rel i).subtype ((quotCompMap R 𝒜 rel i) ⟨x, hx⟩) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩))
Theorem: quotDecompose'_apply
Proof state before:
case H.h.mk
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
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
x : A
hx : x ∈ 𝒜 i
⊢ (quotSubmodule R 𝒜 rel i).subtype ((quotCompMap R 𝒜 rel i) ⟨x, hx⟩) =
    (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩))
Tactic:
simp only [lof_eq_of, coeLinearMap_of, quotCompMap, LinearMap.coe_mk,
  AddHom.coe_mk, Submodule.coeSubtype]
Proof state after:
no goals
Theorem: quotDecompose'_apply
Proof 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
a : ⨁ (i : ι), ↥(𝒜 i)
this : quotDecompose' R 𝒜 rel ∘ₗ lmap' (quotCompMap R 𝒜 rel) = (RingQuot.mkAlgHom R rel).toLinearMap ∘ₗ coeLinearMap 𝒜
⊢ (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a)
Tactic:
simp only [LinearMap.ext_iff, LinearMap.comp_apply, AlgHom.toLinearMap_apply] at this
Proof 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
a : ⨁ (i : ι), ↥(𝒜 i)
this :
  ∀ (x : ⨁ (i : ι), ↥(𝒜 i)),
    (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) x) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)
⊢ (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a)
Theorem: quotDecompose'_apply
Proof 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
a : ⨁ (i : ι), ↥(𝒜 i)
this :
  ∀ (x : ⨁ (i : ι), ↥(𝒜 i)),
    (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) x) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) x)
⊢ (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a)
Tactic:
apply this
Proof state after:
no goals
Theorem: lmap'_quotCompMap_apply
Proof 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 𝒜
i : ι
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
    ↑(((lmap' (quotCompMap R 𝒜 rel)) a) i)
Tactic:
simp only [lmap'_apply]
Proof 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 𝒜
i : ι
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
    ↑((quotCompMap R 𝒜 rel i) (a i))
Theorem: lmap'_quotCompMap_apply
Proof 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 𝒜
i : ι
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
    ↑((quotCompMap R 𝒜 rel i) (a i))
Tactic:
congr
Proof state after:
case h.e_6.h.e_self.e_a
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 𝒜
i : ι
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a) = a
Theorem: lmap'_quotCompMap_apply
Proof state before:
case h.e_6.h.e_self.e_a
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 𝒜
i : ι
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a) = a
Tactic:
exact h𝒜.right_inv a
Proof state after:
no goals
Theorem: quotDecompose'_surjective
Proof 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
Proof 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
Theorem: quotDecompose'_surjective
Proof 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
Proof 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
Theorem: quotDecompose'_surjective
Proof 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
Proof 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
Theorem: quotDecompose'_surjective
Proof 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)
Proof 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
Theorem: quotDecompose'_surjective
Proof 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]
Proof 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))
Theorem: quotDecompose'_surjective
Proof 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
Proof state after:
no goals
Theorem: obvious_iff
Proof 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
x y : A
⊢ (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y ↔ RingConGen.Rel rel x y
Tactic:
constructor
Proof state after:
case mp
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
x y : A
⊢ (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y → RingConGen.Rel rel x y

case mpr
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
x y : A
⊢ RingConGen.Rel rel x y → (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y