internlm/Lean-Github huggingface dataset:
Theorem: RingConGen.RelIsHomogeneous_of
Proof 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 x✝ y✝ : A
a✝ : Rel rel x✝ y✝
h' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap x✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap y✝) i)
⊢ ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap y✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap x✝) i)
Tactic:
exact fun i => RingConGen.Rel.symm (h' i)
Proof state after:
no goals
Theorem: RingConGen.RelIsHomogeneous_of
Proof 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 x✝ y✝ z✝ : A
a✝¹ : Rel rel x✝ y✝
a✝ : Rel rel y✝ z✝
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap x✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap y✝) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap y✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap z✝) i)
⊢ ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap x✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap z✝) i)
Tactic:
exact fun i => RingConGen.Rel.trans (k i) (k' i)
Proof state after:
no goals
Theorem: RingConGen.RelIsHomogeneous_of
Proof state before:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a b w✝ x✝ y✝ z✝ : A
a✝¹ : Rel rel w✝ x✝
a✝ : Rel rel y✝ z✝
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap w✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap x✝) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap y✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap z✝) i)
⊢ ∀ (i : ι),
    Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap (w✝ + y✝)) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap (x✝ + z✝)) i)
Tactic:
intro i
Proof state after:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a b w✝ x✝ y✝ z✝ : A
a✝¹ : Rel rel w✝ x✝
a✝ : Rel rel y✝ z✝
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap w✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap x✝) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap y✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap z✝) i)
i : ι
⊢ Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap (w✝ + y✝)) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap (x✝ + z✝)) i)
Theorem: RingConGen.RelIsHomogeneous_of
Proof state before:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a b w✝ x✝ y✝ z✝ : A
a✝¹ : Rel rel w✝ x✝
a✝ : Rel rel y✝ z✝
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap w✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap x✝) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap y✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap z✝) i)
i : ι
⊢ Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap (w✝ + y✝)) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap (x✝ + z✝)) i)
Tactic:
simp only [map_add]
Proof state after:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a b w✝ x✝ y✝ z✝ : A
a✝¹ : Rel rel w✝ x✝
a✝ : Rel rel y✝ z✝
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap w✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap x✝) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap y✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap z✝) i)
i : ι
⊢ Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap w✝ + (decomposeAlgEquiv 𝒜).toLinearMap y✝) i)
    ↑(((decomposeAlgEquiv 𝒜).toLinearMap x✝ + (decomposeAlgEquiv 𝒜).toLinearMap z✝) i)
Theorem: RingConGen.RelIsHomogeneous_of
Proof state before:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a b w✝ x✝ y✝ z✝ : A
a✝¹ : Rel rel w✝ x✝
a✝ : Rel rel y✝ z✝
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap w✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap x✝) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap y✝) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap z✝) i)
i : ι
⊢ Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap w✝ + (decomposeAlgEquiv 𝒜).toLinearMap y✝) i)
    ↑(((decomposeAlgEquiv 𝒜).toLinearMap x✝ + (decomposeAlgEquiv 𝒜).toLinearMap z✝) i)
Tactic:
exact RingConGen.Rel.add (k i) (k' i)
Proof state after:
no goals
Theorem: RingConGen.RelIsHomogeneous_of
Proof state before:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
⊢ ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap (a * c)) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap (b * d)) i)
Tactic:
intro n
Proof state after:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n : ι
⊢ Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap (a * c)) n) ↑(((decomposeAlgEquiv 𝒜).toLinearMap (b * d)) n)
Theorem: RingConGen.RelIsHomogeneous_of
Proof state before:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n : ι
⊢ Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap (a * c)) n) ↑(((decomposeAlgEquiv 𝒜).toLinearMap (b * d)) n)
Tactic:
simp only [AlgEquiv.toLinearMap_apply, map_mul, coe_mul_apply_eq_dfinsupp_sum]
Proof state after:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n : ι
⊢ Rel rel
    (DFinsupp.sum ((decomposeAlgEquiv 𝒜) a) fun i ri =>
      DFinsupp.sum ((decomposeAlgEquiv 𝒜) c) fun j rj => if i + j = n then ↑ri * ↑rj else 0)
    (DFinsupp.sum ((decomposeAlgEquiv 𝒜) b) fun i ri =>
      DFinsupp.sum ((decomposeAlgEquiv 𝒜) d) fun j rj => if i + j = n then ↑ri * ↑rj else 0)
Theorem: RingConGen.RelIsHomogeneous_of
Proof state before:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n : ι
⊢ Rel rel
    (DFinsupp.sum ((decomposeAlgEquiv 𝒜) a) fun i ri =>
      DFinsupp.sum ((decomposeAlgEquiv 𝒜) c) fun j rj => if i + j = n then ↑ri * ↑rj else 0)
    (DFinsupp.sum ((decomposeAlgEquiv 𝒜) b) fun i ri =>
      DFinsupp.sum ((decomposeAlgEquiv 𝒜) d) fun j rj => if i + j = n then ↑ri * ↑rj else 0)
Tactic:
apply rel_of_dfinsupp_sum_of_rel_add (RingConGen.Rel.refl 0) (RingConGen.Rel.add)
  (Φy 𝒜 n (decomposeAlgEquiv 𝒜 c)) (Φy 𝒜 n (decomposeAlgEquiv 𝒜 d))
Proof state after:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n : ι
⊢ ∀ (i : ι),
    Rel rel ((Φy 𝒜 n ((decomposeAlgEquiv 𝒜) c) i) (((decomposeAlgEquiv 𝒜) a) i))
      ((Φy 𝒜 n ((decomposeAlgEquiv 𝒜) d) i) (((decomposeAlgEquiv 𝒜) b) i))
Theorem: RingConGen.RelIsHomogeneous_of
Proof state before:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n : ι
⊢ ∀ (i : ι),
    Rel rel ((Φy 𝒜 n ((decomposeAlgEquiv 𝒜) c) i) (((decomposeAlgEquiv 𝒜) a) i))
      ((Φy 𝒜 n ((decomposeAlgEquiv 𝒜) d) i) (((decomposeAlgEquiv 𝒜) b) i))
Tactic:
intro i
Proof state after:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n i : ι
⊢ Rel rel ((Φy 𝒜 n ((decomposeAlgEquiv 𝒜) c) i) (((decomposeAlgEquiv 𝒜) a) i))
    ((Φy 𝒜 n ((decomposeAlgEquiv 𝒜) d) i) (((decomposeAlgEquiv 𝒜) b) i))
Theorem: RingConGen.RelIsHomogeneous_of
Proof state before:
case 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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n i : ι
⊢ Rel rel ((Φy 𝒜 n ((decomposeAlgEquiv 𝒜) c) i) (((decomposeAlgEquiv 𝒜) a) i))
    ((Φy 𝒜 n ((decomposeAlgEquiv 𝒜) d) i) (((decomposeAlgEquiv 𝒜) b) i))
Tactic:
apply rel_of_dfinsupp_sum_of_rel_add (RingConGen.Rel.refl 0) (RingConGen.Rel.add)
Proof state after:
case mul.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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n i : ι
⊢ ∀ (i_1 : ι),
    Rel rel (((Φ 𝒜 n i i_1) (((decomposeAlgEquiv 𝒜) a) i)) (((decomposeAlgEquiv 𝒜) c) i_1))
      (((Φ 𝒜 n i i_1) (((decomposeAlgEquiv 𝒜) b) i)) (((decomposeAlgEquiv 𝒜) d) i_1))
Theorem: RingConGen.RelIsHomogeneous_of
Proof state before:
case mul.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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n i : ι
⊢ ∀ (i_1 : ι),
    Rel rel (((Φ 𝒜 n i i_1) (((decomposeAlgEquiv 𝒜) a) i)) (((decomposeAlgEquiv 𝒜) c) i_1))
      (((Φ 𝒜 n i i_1) (((decomposeAlgEquiv 𝒜) b) i)) (((decomposeAlgEquiv 𝒜) d) i_1))
Tactic:
intro j
Proof state after:
case mul.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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n i j : ι
⊢ Rel rel (((Φ 𝒜 n i j) (((decomposeAlgEquiv 𝒜) a) i)) (((decomposeAlgEquiv 𝒜) c) j))
    (((Φ 𝒜 n i j) (((decomposeAlgEquiv 𝒜) b) i)) (((decomposeAlgEquiv 𝒜) d) j))
Theorem: RingConGen.RelIsHomogeneous_of
Proof state before:
case mul.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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n i j : ι
⊢ Rel rel (((Φ 𝒜 n i j) (((decomposeAlgEquiv 𝒜) a) i)) (((decomposeAlgEquiv 𝒜) c) j))
    (((Φ 𝒜 n i j) (((decomposeAlgEquiv 𝒜) b) i)) (((decomposeAlgEquiv 𝒜) d) j))
Tactic:
dsimp only [Φ]
Proof state after:
case mul.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
inst✝ : GradedAlgebra 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n i j : ι
⊢ Rel rel
    (({ toFun := fun x => { toFun := fun y => if i + j = n then ↑x * ↑y else 0, map_zero' := ⋯, map_add' := ⋯ },
          map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) a) i))
      (((decomposeAlgEquiv 𝒜) c) j))
    (({ toFun := fun x => { toFun := fun y => if i + j = n then ↑x * ↑y else 0, map_zero' := ⋯, map_add' := ⋯ },
          map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) b) i))
      (((decomposeAlgEquiv 𝒜) d) j))
Theorem: RingConGen.RelIsHomogeneous_of
Proof 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 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n i j : ι
hn : ¬i + j = n
⊢ Rel rel
    (({ toFun := fun x => { toFun := fun y => if i + j = n then ↑x * ↑y else 0, map_zero' := ⋯, map_add' := ⋯ },
          map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) a) i))
      (((decomposeAlgEquiv 𝒜) c) j))
    (({ toFun := fun x => { toFun := fun y => if i + j = n then ↑x * ↑y else 0, map_zero' := ⋯, map_add' := ⋯ },
          map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) b) i))
      (((decomposeAlgEquiv 𝒜) d) j))
Tactic:
. simp only [if_neg hn]
  exact RingConGen.Rel.refl _
Proof state after:
no goals
Theorem: RingConGen.RelIsHomogeneous_of
Proof 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 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n i j : ι
hn : i + j = n
⊢ Rel rel
    (({ toFun := fun x => { toFun := fun y => if i + j = n then ↑x * ↑y else 0, map_zero' := ⋯, map_add' := ⋯ },
          map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) a) i))
      (((decomposeAlgEquiv 𝒜) c) j))
    (({ toFun := fun x => { toFun := fun y => if i + j = n then ↑x * ↑y else 0, map_zero' := ⋯, map_add' := ⋯ },
          map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) b) i))
      (((decomposeAlgEquiv 𝒜) d) j))
Tactic:
simp only [if_pos hn]
Proof 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 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n i j : ι
hn : i + j = n
⊢ Rel rel
    (({ toFun := fun x => { toFun := fun y => ↑x * ↑y, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) a) i))
      (((decomposeAlgEquiv 𝒜) c) j))
    (({ toFun := fun x => { toFun := fun y => ↑x * ↑y, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) b) i))
      (((decomposeAlgEquiv 𝒜) d) j))
Theorem: RingConGen.RelIsHomogeneous_of
Proof 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 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n i j : ι
hn : i + j = n
⊢ Rel rel
    (({ toFun := fun x => { toFun := fun y => ↑x * ↑y, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) a) i))
      (((decomposeAlgEquiv 𝒜) c) j))
    (({ toFun := fun x => { toFun := fun y => ↑x * ↑y, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) b) i))
      (((decomposeAlgEquiv 𝒜) d) j))
Tactic:
exact RingConGen.Rel.mul (k i) (k' j)
Proof state after:
no goals
Theorem: RingConGen.RelIsHomogeneous_of
Proof 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 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n i j : ι
hn : ¬i + j = n
⊢ Rel rel
    (({ toFun := fun x => { toFun := fun y => if i + j = n then ↑x * ↑y else 0, map_zero' := ⋯, map_add' := ⋯ },
          map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) a) i))
      (((decomposeAlgEquiv 𝒜) c) j))
    (({ toFun := fun x => { toFun := fun y => if i + j = n then ↑x * ↑y else 0, map_zero' := ⋯, map_add' := ⋯ },
          map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) b) i))
      (((decomposeAlgEquiv 𝒜) d) j))
Tactic:
simp only [if_neg hn]
Proof 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 𝒜
hr : Rel.IsHomogeneous 𝒜 rel
a✝² b✝ a b c d : A
a✝¹ : Rel rel a b
a✝ : Rel rel c d
k : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
k' : ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap c) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap d) i)
n i j : ι
hn : ¬i + j = n
⊢ Rel rel
    (({ toFun := fun x => { toFun := fun y => 0, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) a) i))
      (((decomposeAlgEquiv 𝒜) c) j))
    (({ toFun := fun x => { toFun := fun y => 0, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
        (((decomposeAlgEquiv 𝒜) b) i))
      (((decomposeAlgEquiv 𝒜) d) j))