internlm/Lean-Github huggingface dataset:
Theorem: obvious_iff
Proof state before:
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
Tactic:
. intro h
  suffices ∀ x, Quot.mk (RingQuot.Rel rel) x = ((RingQuot.mkRingHom rel) x).toQuot by
    rw [← RingQuot.eqvGen_rel_eq, ← Quot.eq, this x, this y, h]
  intro x
  simp only [RingQuot.mkRingHom]
  rfl
Proof state after:
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
Theorem: obvious_iff
Proof state before:
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
Tactic:
. intro h
  induction h with
  | of x y h => exact RingQuot.mkRingHom_rel h
  | refl x => exact rfl
  | symm _ k => exact k.symm
  | trans h h' k k' => rw [k, k']
  | add _ _ k k' => simp only [map_add, k, k']
  | mul _ _ k k' => simp only [map_mul, k, k']
Proof state after:
no goals
Theorem: obvious_iff
Proof state before:
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
Tactic:
intro h
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
h : (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
⊢ RingConGen.Rel rel x y
Theorem: obvious_iff
Proof state before:
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
h : (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
⊢ RingConGen.Rel rel x y
Tactic:
suffices ∀ x, Quot.mk (RingQuot.Rel rel) x = ((RingQuot.mkRingHom rel) x).toQuot by
  rw [← RingQuot.eqvGen_rel_eq, ← Quot.eq, this x, this y, h]
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
h : (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
⊢ ∀ (x : A), Quot.mk (RingQuot.Rel rel) x = ((RingQuot.mkRingHom rel) x).toQuot
Theorem: obvious_iff
Proof state before:
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
h : (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
⊢ ∀ (x : A), Quot.mk (RingQuot.Rel rel) x = ((RingQuot.mkRingHom rel) x).toQuot
Tactic:
intro x
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
h : (RingQuot.mkRingHom rel) x✝ = (RingQuot.mkRingHom rel) y
x : A
⊢ Quot.mk (RingQuot.Rel rel) x = ((RingQuot.mkRingHom rel) x).toQuot
Theorem: obvious_iff
Proof state before:
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
h : (RingQuot.mkRingHom rel) x✝ = (RingQuot.mkRingHom rel) y
x : A
⊢ Quot.mk (RingQuot.Rel rel) x = ((RingQuot.mkRingHom rel) x).toQuot
Tactic:
simp only [RingQuot.mkRingHom]
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
h : (RingQuot.mkRingHom rel) x✝ = (RingQuot.mkRingHom rel) y
x : A
⊢ Quot.mk (RingQuot.Rel rel) x =
    ({ toFun := fun x => { toQuot := Quot.mk (RingQuot.Rel rel) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        x).toQuot
Theorem: obvious_iff
Proof state before:
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
h : (RingQuot.mkRingHom rel) x✝ = (RingQuot.mkRingHom rel) y
x : A
⊢ Quot.mk (RingQuot.Rel rel) x =
    ({ toFun := fun x => { toQuot := Quot.mk (RingQuot.Rel rel) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        x).toQuot
Tactic:
rfl
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
h : (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
this : ∀ (x : A), Quot.mk (RingQuot.Rel rel) x = ((RingQuot.mkRingHom rel) x).toQuot
⊢ RingConGen.Rel rel x y
Tactic:
rw [← RingQuot.eqvGen_rel_eq, ← Quot.eq, this x, this y, h]
Proof state after:
no goals
Theorem: obvious_iff
Proof state before:
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
Tactic:
intro h
Proof state after:
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
h : RingConGen.Rel rel x y
⊢ (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
Theorem: obvious_iff
Proof state before:
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
h : RingConGen.Rel rel x y
⊢ (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
Tactic:
induction h with
| of x y h => exact RingQuot.mkRingHom_rel h
| refl x => exact rfl
| symm _ k => exact k.symm
| trans h h' k k' => rw [k, k']
| add _ _ k k' => simp only [map_add, k, k']
| mul _ _ k k' => simp only [map_mul, k, k']
Proof state after:
no goals
Theorem: obvious_iff
Proof state before:
case mpr.of
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✝ x y : A
h : rel x y
⊢ (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) y
Tactic:
exact RingQuot.mkRingHom_rel h
Proof state after:
no goals
Theorem: obvious_iff
Proof state before:
case mpr.refl
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 x : A
⊢ (RingQuot.mkRingHom rel) x = (RingQuot.mkRingHom rel) x
Tactic:
exact rfl
Proof state after:
no goals
Theorem: obvious_iff
Proof state before:
case mpr.symm
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 x✝ y✝ : A
a✝ : RingConGen.Rel rel x✝ y✝
k : (RingQuot.mkRingHom rel) x✝ = (RingQuot.mkRingHom rel) y✝
⊢ (RingQuot.mkRingHom rel) y✝ = (RingQuot.mkRingHom rel) x✝
Tactic:
exact k.symm
Proof state after:
no goals
Theorem: obvious_iff
Proof state before:
case mpr.trans
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 x✝ y✝ z✝ : A
h : RingConGen.Rel rel x✝ y✝
h' : RingConGen.Rel rel y✝ z✝
k : (RingQuot.mkRingHom rel) x✝ = (RingQuot.mkRingHom rel) y✝
k' : (RingQuot.mkRingHom rel) y✝ = (RingQuot.mkRingHom rel) z✝
⊢ (RingQuot.mkRingHom rel) x✝ = (RingQuot.mkRingHom rel) z✝
Tactic:
rw [k, k']
Proof state after:
no goals
Theorem: obvious_iff
Proof state before:
case mpr.add
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 w✝ x✝ y✝ z✝ : A
a✝¹ : RingConGen.Rel rel w✝ x✝
a✝ : RingConGen.Rel rel y✝ z✝
k : (RingQuot.mkRingHom rel) w✝ = (RingQuot.mkRingHom rel) x✝
k' : (RingQuot.mkRingHom rel) y✝ = (RingQuot.mkRingHom rel) z✝
⊢ (RingQuot.mkRingHom rel) (w✝ + y✝) = (RingQuot.mkRingHom rel) (x✝ + z✝)
Tactic:
simp only [map_add, k, k']
Proof state after:
no goals
Theorem: obvious_iff
Proof state before:
case mpr.mul
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 w✝ x✝ y✝ z✝ : A
a✝¹ : RingConGen.Rel rel w✝ x✝
a✝ : RingConGen.Rel rel y✝ z✝
k : (RingQuot.mkRingHom rel) w✝ = (RingQuot.mkRingHom rel) x✝
k' : (RingQuot.mkRingHom rel) y✝ = (RingQuot.mkRingHom rel) z✝
⊢ (RingQuot.mkRingHom rel) (w✝ * y✝) = (RingQuot.mkRingHom rel) (x✝ * z✝)
Tactic:
simp only [map_mul, k, k']
Proof state after:
no goals
Theorem: quotDecompose_injective
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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
x y : A
hxy : (RingQuot.mkAlgHom R rel) x = (RingQuot.mkAlgHom R rel) y
i : ι
⊢ (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' x) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' y) i)
Tactic:
rw [← AlgHom.coe_toRingHom, RingQuot.mkAlgHom_coe R rel, obvious_iff] at hxy ⊢
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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
x y : A
hxy : RingConGen.Rel rel x y
i : ι
⊢ RingConGen.Rel rel ↑((Decomposition.decompose' x) i) ↑((Decomposition.decompose' y) i)
Theorem: quotDecompose_injective
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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
x y : A
hxy : RingConGen.Rel rel x y
i : ι
⊢ RingConGen.Rel rel ↑((Decomposition.decompose' x) i) ↑((Decomposition.decompose' y) i)
Tactic:
exact RingConGen.RelIsHomogeneous_of 𝒜 _ hrel hxy i
Proof state after:
no goals
Theorem: quotDecompose_surjective2
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
⊢ Surjective ⇑(lmap' (quotCompMap R 𝒜 rel))
Tactic:
apply lmap'_surjective (quotCompMap 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
⊢ ∀ (i : ι), Surjective ⇑(quotCompMap R 𝒜 rel i)
Theorem: quotDecompose_surjective2
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
⊢ ∀ (i : ι), Surjective ⇑(quotCompMap R 𝒜 rel i)
Tactic:
rintro i ⟨x, ⟨a, ha, rfl⟩⟩
Proof 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, ⋯⟩
Theorem: quotDecompose_surjective2
Proof 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⟩
Proof state after:
no goals
Theorem: quotDecompose'_injective
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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
⊢ Injective ⇑(quotDecompose' R 𝒜 rel)
Tactic:
intro x y hxy
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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
x y : ⨁ (i : ι), ↥(quotSubmodule R 𝒜 rel i)
hxy : (quotDecompose' R 𝒜 rel) x = (quotDecompose' R 𝒜 rel) y
⊢ x = y
Theorem: quotDecompose'_injective
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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
x y : ⨁ (i : ι), ↥(quotSubmodule R 𝒜 rel i)
hxy : (quotDecompose' R 𝒜 rel) x = (quotDecompose' R 𝒜 rel) y
⊢ x = y
Tactic:
obtain ⟨a, ha, rfl⟩ := quotDecompose_surjective2 R 𝒜 rel x
Proof state after:
case intro.refl
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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
y : ⨁ (i : ι), ↥(quotSubmodule R 𝒜 rel i)
a : ⨁ (i : ι), ↥(𝒜 i)
hxy : (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) a) = (quotDecompose' R 𝒜 rel) y
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = y
Theorem: quotDecompose'_injective
Proof state before:
case intro.refl
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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
y : ⨁ (i : ι), ↥(quotSubmodule R 𝒜 rel i)
a : ⨁ (i : ι), ↥(𝒜 i)
hxy : (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) a) = (quotDecompose' R 𝒜 rel) y
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = y
Tactic:
obtain ⟨b, hb, rfl⟩ := quotDecompose_surjective2 R 𝒜 rel y
Proof state after:
case intro.refl.intro.refl
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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy :
  (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) a) =
    (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) b)
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = (lmap' (quotCompMap R 𝒜 rel)) b
Theorem: quotDecompose'_injective
Proof state before:
case intro.refl.intro.refl
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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy :
  (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) a) =
    (quotDecompose' R 𝒜 rel) ((lmap' (quotCompMap R 𝒜 rel)) b)
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = (lmap' (quotCompMap R 𝒜 rel)) b
Tactic:
simp only [quotDecompose'_apply] at hxy
Proof state after:
case intro.refl.intro.refl
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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = (lmap' (quotCompMap R 𝒜 rel)) b
Theorem: quotDecompose'_injective
Proof state before:
case intro.refl.intro.refl
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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = (lmap' (quotCompMap R 𝒜 rel)) b
Tactic:
let hxy' := quotDecompose_injective R 𝒜 rel hrel hxy
Proof state after:
case intro.refl.intro.refl
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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
hxy' : ∀ (i : ι),
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) b)) i) :=
  quotDecompose_injective R 𝒜 rel (fun {a b} => hrel) hxy
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = (lmap' (quotCompMap R 𝒜 rel)) b
Theorem: quotDecompose'_injective
Proof state before:
case intro.refl.intro.refl
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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
hxy' : ∀ (i : ι),
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) b)) i) :=
  quotDecompose_injective R 𝒜 rel (fun {a b} => hrel) hxy
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = (lmap' (quotCompMap R 𝒜 rel)) b
Tactic:
apply DFinsupp.ext
Proof state after:
case intro.refl.intro.refl.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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
hxy' : ∀ (i : ι),
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) b)) i) :=
  quotDecompose_injective R 𝒜 rel (fun {a b} => hrel) hxy
⊢ ∀ (i : ι), ((lmap' (quotCompMap R 𝒜 rel)) a) i = ((lmap' (quotCompMap R 𝒜 rel)) b) i
Theorem: quotDecompose'_injective
Proof state before:
case intro.refl.intro.refl.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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
hxy' : ∀ (i : ι),
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) b)) i) :=
  quotDecompose_injective R 𝒜 rel (fun {a b} => hrel) hxy
⊢ ∀ (i : ι), ((lmap' (quotCompMap R 𝒜 rel)) a) i = ((lmap' (quotCompMap R 𝒜 rel)) b) i
Tactic:
intro i
Proof state after:
case intro.refl.intro.refl.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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
hxy' : ∀ (i : ι),
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) b)) i) :=
  quotDecompose_injective R 𝒜 rel (fun {a b} => hrel) hxy
i : ι
⊢ ((lmap' (quotCompMap R 𝒜 rel)) a) i = ((lmap' (quotCompMap R 𝒜 rel)) b) i
Theorem: quotDecompose'_injective
Proof state before:
case intro.refl.intro.refl.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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
hxy' : ∀ (i : ι),
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) b)) i) :=
  quotDecompose_injective R 𝒜 rel (fun {a b} => hrel) hxy
i : ι
⊢ ((lmap' (quotCompMap R 𝒜 rel)) a) i = ((lmap' (quotCompMap R 𝒜 rel)) b) i
Tactic:
specialize hxy' i
Proof state after:
case intro.refl.intro.refl.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 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) b)) i)
⊢ ((lmap' (quotCompMap R 𝒜 rel)) a) i = ((lmap' (quotCompMap R 𝒜 rel)) b) i