-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem reindex_refl : reindex R s (Equiv.refl ι) = LinearEquiv.refl R _

Proof state:
case a
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
⊢ ↑(reindex R s (Equiv.refl ι)) = ↑(LinearEquiv.refl R (⨂[R] (i : ι), s i))

Tactic:
ext

Result:
case a.H.H
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x✝ : (i : ι) → s i
⊢ ((↑(reindex R s (Equiv.refl ι))).compMultilinearMap (tprod R)) x✝ =
    ((↑(LinearEquiv.refl R (⨂[R] (i : ι), s i))).compMultilinearMap (tprod R)) x✝

Proof state:
case a.H.H
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x✝ : (i : ι) → s i
⊢ ((↑(reindex R s (Equiv.refl ι))).compMultilinearMap (tprod R)) x✝ =
    ((↑(LinearEquiv.refl R (⨂[R] (i : ι), s i))).compMultilinearMap (tprod R)) x✝

Tactic:
simp only [Equiv.refl_symm, Equiv.refl_apply, reindex, domDomCongrLinearEquiv',
  LinearEquiv.coe_symm_mk, LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe,
  LinearEquiv.refl_toLinearMap, LinearMap.id_coe, id_eq]

Result:
case a.H.H
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x✝ : (i : ι) → s i
⊢ (LinearEquiv.ofLinear
        (lift
          { toFun := ⇑(tprod R) ∘ ⇑(Equiv.piCongrLeft' s (Equiv.refl ι)), map_update_add' := ⋯, map_update_smul' := ⋯ })
        (lift
          ({
              toFun := fun f =>
                { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' s (Equiv.refl ι)).symm, map_update_add' := ⋯,
                  map_update_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯,
              invFun := fun f =>
                { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' s (Equiv.refl ι)), map_update_add' := ⋯, map_update_smul' := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }
            (tprod R)))
        ⋯ ⋯)
      ((tprod R) x✝) =
    (tprod R) x✝

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
⊢ reindex R s (Equiv.refl ι) = LinearEquiv.refl R (⨂[R] (i : ι), s i)

Tactic:
apply LinearEquiv.toLinearMap_injective

Result:
case a
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
⊢ ↑(reindex R s (Equiv.refl ι)) = ↑(LinearEquiv.refl R (⨂[R] (i : ι), s i))

Proof state:
case a.H.H
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x✝ : (i : ι) → s i
⊢ (LinearEquiv.ofLinear
        (lift
          { toFun := ⇑(tprod R) ∘ ⇑(Equiv.piCongrLeft' s (Equiv.refl ι)), map_update_add' := ⋯, map_update_smul' := ⋯ })
        (lift
          ({
              toFun := fun f =>
                { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' s (Equiv.refl ι)).symm, map_update_add' := ⋯,
                  map_update_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯,
              invFun := fun f =>
                { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' s (Equiv.refl ι)), map_update_add' := ⋯, map_update_smul' := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }
            (tprod R)))
        ⋯ ⋯)
      ((tprod R) x✝) =
    (tprod R) x✝

Tactic:
erw [lift.tprod]

Result:
case a.H.H
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x✝ : (i : ι) → s i
⊢ { toFun := ⇑(tprod R) ∘ ⇑(Equiv.piCongrLeft' s (Equiv.refl ι)), map_update_add' := ⋯, map_update_smul' := ⋯ } x✝ =
    (tprod R) x✝

Proof state:
case a.H.H
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x✝ : (i : ι) → s i
⊢ { toFun := ⇑(tprod R) ∘ ⇑(Equiv.piCongrLeft' s (Equiv.refl ι)), map_update_add' := ⋯, map_update_smul' := ⋯ } x✝ =
    (tprod R) x✝

Tactic:
congr

Result:
no goals