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))

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_pos hn]
  exact RingConGen.Rel.mul (k i) (k' j)
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 => 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))