Theorem: RingConGen.RelIsHomogeneous_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 𝒜 (Rel 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 : Rel rel a b
⊢ ∀ (i : ι), Rel 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 : Rel rel a b
⊢ ∀ (i : ι), Rel rel ↑(((decomposeAlgEquiv 𝒜).toLinearMap a) i) ↑(((decomposeAlgEquiv 𝒜).toLinearMap b) i)
Tactic:
induction h with
| of x y h => exact fun i =>  RingConGen.Rel.of _ _ (hr h i)
| refl x => exact fun _ => RingConGen.Rel.refl _
| symm _ h' => exact fun i => RingConGen.Rel.symm (h' i)
| trans _ _ k k' => exact fun i => RingConGen.Rel.trans (k i) (k' i)
| add _ _  k k' =>
  intro i
  simp only [map_add]
  exact RingConGen.Rel.add (k i) (k' i)
| @mul a b c d _ _ k k' =>
  intro n
  simp only [AlgEquiv.toLinearMap_apply, map_mul, coe_mul_apply_eq_dfinsupp_sum]
  apply rel_of_dfinsupp_sum_of_rel_add (RingConGen.Rel.refl 0) (RingConGen.Rel.add)
    (Φy 𝒜 n (decomposeAlgEquiv 𝒜 c)) (Φy 𝒜 n (decomposeAlgEquiv 𝒜 d))
  intro i
  apply rel_of_dfinsupp_sum_of_rel_add (RingConGen.Rel.refl 0) (RingConGen.Rel.add)
  intro j
  dsimp only [Φ]
  by_cases hn : i + j = n
  . simp only [if_pos hn]
    exact RingConGen.Rel.mul (k i) (k' j)
  . simp only [if_neg hn]
    exact RingConGen.Rel.refl _
State after:
no goals

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

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

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

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)
State after:
no goals

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

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

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

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

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

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

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 [Φ]
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))

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
    (({ 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:
by_cases hn : i + j = n
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 => 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))

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

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 _
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 𝒜
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]
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))

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

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 => 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))
Tactic:
exact RingConGen.Rel.refl _
State after:
no goals