Theorem: EqvGenIsHomogeneous_of (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 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
⊢ Rel.IsHomogeneous 𝒜 (EqvGen rel)
Tactic:
intro a b h
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 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a b : A
h : EqvGen rel a b
⊢ ∀ (i : ι), EqvGen 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 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a b : A
h : EqvGen rel a b
⊢ ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
induction h with
| rel a b h => exact fun i => EqvGen.rel _ _ (hr h i)
| refl a => exact fun i => EqvGen.refl _
| symm a b _ k => exact fun i => EqvGen.symm _ _ (k i)
| trans a b c _ _ k k' => exact fun i => EqvGen.trans _ _ _ (k i) (k' i)
State after:
no goals

State before:
case rel
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 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝ b✝ a b : A
h : rel a b
⊢ ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
exact fun i => EqvGen.rel _ _ (hr h i)
State after:
no goals

State before:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝ b a : A
⊢ ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i)
Tactic:
exact fun i => EqvGen.refl _
State after:
no goals

State before:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝¹ b✝ a b : A
a✝ : EqvGen rel a b
k : ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
⊢ ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i)
Tactic:
exact fun i => EqvGen.symm _ _ (k i)
State after:
no goals

State before:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c : A
a✝¹ : EqvGen rel a b
a✝ : EqvGen rel b c
k : ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i)
⊢ ∀ (i : ι), EqvGen rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i)
Tactic:
exact fun i => EqvGen.trans _ _ _ (k i) (k' i)
State after:
no goals