-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem coord_unitsSMul (e : Basis ι R₂ M) (w : ι → R₂ˣ) (i : ι) :
    (unitsSMul e w).coord i = (w i)⁻¹ • e.coord i

Proof state:
ι : Type u_1
R₂ : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i : ι
⊢ (e.unitsSMul w).coord i = (w i)⁻¹ • e.coord i

Tactic:
apply e.ext

Result:
ι : Type u_1
R₂ : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i : ι
⊢ ∀ (i_1 : ι), ((e.unitsSMul w).coord i) (e i_1) = ((w i)⁻¹ • e.coord i) (e i_1)

Proof state:
ι : Type u_1
R₂ : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i : ι
⊢ ∀ (i_1 : ι), ((e.unitsSMul w).coord i) (e i_1) = ((w i)⁻¹ • e.coord i) (e i_1)

Tactic:
intro j

Result:
ι : Type u_1
R₂ : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ ((e.unitsSMul w).coord i) (e j) = ((w i)⁻¹ • e.coord i) (e j)

Proof state:
ι : Type u_1
R₂ : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ (↑(w j)⁻¹ • if j = i then 1 else 0) = ↑(w i)⁻¹ • if j = i then 1 else 0

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals

Proof state:
case h.e_6.h
ι : Type u_1
R₂ : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ e j = (w j)⁻¹ • (e.unitsSMul w) j

Tactic:
simp [Basis.unitsSMul, ← mul_smul]

Result:
no goals

Proof state:
ι : Type u_1
R₂ : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ ((e.unitsSMul w).coord i) (e j) = ((w i)⁻¹ • e.coord i) (e j)

Tactic:
trans ((unitsSMul e w).coord i) ((w j)⁻¹ • (unitsSMul e w) j)

Result:
ι : Type u_1
R₂ : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ ((e.unitsSMul w).coord i) (e j) = ((e.unitsSMul w).coord i) ((w j)⁻¹ • (e.unitsSMul w) j)

ι : Type u_1
R₂ : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ ((e.unitsSMul w).coord i) ((w j)⁻¹ • (e.unitsSMul w) j) = ((w i)⁻¹ • e.coord i) (e j)

Proof state:
ι : Type u_1
R₂ : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ ((e.unitsSMul w).coord i) (e j) = ((e.unitsSMul w).coord i) ((w j)⁻¹ • (e.unitsSMul w) j)

Tactic:
congr

Result:
case h.e_6.h
ι : Type u_1
R₂ : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ e j = (w j)⁻¹ • (e.unitsSMul w) j

Proof state:
ι : Type u_1
R₂ : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ ((e.unitsSMul w).coord i) ((w j)⁻¹ • (e.unitsSMul w) j) = ((w i)⁻¹ • e.coord i) (e j)

Tactic:
simp only [Basis.coord_apply, LinearMap.smul_apply, Basis.repr_self, Units.smul_def,
  map_smul, Finsupp.single_apply]

Result:
ι : Type u_1
R₂ : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ (↑(w j)⁻¹ • if j = i then 1 else 0) = ↑(w i)⁻¹ • if j = i then 1 else 0