Theorem: Rel.IsHomogeneous_of_isPureHomogeneous (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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
⊢ IsHomogeneous 𝒜 rel
Tactic:
intro a b h i
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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i : ι
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) 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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i : ι
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
obtain ⟨j, ha, hb⟩ := hrel h
State after:
case 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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)

State before:
case 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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
by_cases hij : j = i
State after:
case pos
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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)

case neg
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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : ¬j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)

State before:
case pos
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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)

case neg
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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : ¬j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
. rw [← hij]
  simp only [AlgEquiv.toLinearMap_apply, decomposeAlgEquiv_coe, decompose_of_mem_same, ha, hb, h]
State after:
case neg
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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : ¬j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)

State before:
case neg
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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : ¬j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
. simp only [AlgEquiv.toLinearMap_apply, decomposeAlgEquiv_coe, decompose_of_mem_ne _ ha hij,
    decompose_of_mem_ne _ hb hij]
  exact hrel0
State after:
no goals

State before:
case pos
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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
rw [← hij]
State after:
case pos
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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) j) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) j)

State before:
case pos
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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) j) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) j)
Tactic:
simp only [AlgEquiv.toLinearMap_apply, decomposeAlgEquiv_coe, decompose_of_mem_same, ha, hb, h]
State after:
no goals

State before:
case neg
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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : ¬j = i
⊢ rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
simp only [AlgEquiv.toLinearMap_apply, decomposeAlgEquiv_coe, decompose_of_mem_ne _ ha hij,
  decompose_of_mem_ne _ hb hij]
State after:
case neg
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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : ¬j = i
⊢ rel 0 0

State before:
case neg
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
inst✝ : GradedAlgebra 𝒜
hrel : IsPureHomogeneous 𝒜 rel
hrel0 : rel 0 0
a b : A
h : rel a b
i j : ι
ha : a ∈ 𝒜 j
hb : b ∈ 𝒜 j
hij : ¬j = i
⊢ rel 0 0
Tactic:
exact hrel0
State after:
no goals