English
In the PiTensorProduct construction of a graded monoid, two dependent pairs of tensor products are equal if their indices coincide and the contents agree after a canonical reindexing; hence equality is determined by the index and the reindexed content.
Русский
В произведении PiTensorProduct для градуированного моноида два зависимых пары тензорных произведений равны, если их индексы совпадают и содержимое совпадает после канонического перенумеровки; следовательно равенство определяется индексом и переразмеренным содержимым.
LaTeX
$$$\\forall a,b:\\,\\text{GradedMonoid}\\, (fun i => ⨂[R] _ : ι_i, M),\\; (h : a.fst = b.fst),\\; reindex_R (fun _ \\mapsto M) (Equiv.cast \\circ congr_arg ι) a.snd = b.snd \\Rightarrow a = b$$$
Lean4
/-- Two dependent pairs of tensor products are equal if their index is equal and the contents
are equal after a canonical reindexing. -/
@[ext (iff := false)]
theorem gradedMonoid_eq_of_reindex_cast {ιι : Type*} {ι : ιι → Type*} :
∀ {a b : GradedMonoid fun ii => ⨂[R] _ : ι ii, M} (h : a.fst = b.fst),
reindex R (fun _ ↦ M) (Equiv.cast <| congr_arg ι h) a.snd = b.snd → a = b
| ⟨ai, a⟩, ⟨bi, b⟩ => fun (hi : ai = bi) (h : reindex R (fun _ ↦ M) _ a = b) =>
by
subst hi
simp_all
