case h₀
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1489579
m : Type u_4
n : Type u_5
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
⊢ ∀ (b : n), b ∈ Finset.univ → b ≠ j → (if b = j then 1 else 0) • ↑v₁ b = 0

case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1489579
m : Type u_4
n : Type u_5
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
⊢ ¬j ∈ Finset.univ → (if j = j then 1 else 0) • ↑v₁ j = 0
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1489579
m : Type u_4
n : Type u_5
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
⊢ ↑(toMatrix v₁ v₂) f i j = ↑(↑v₂.repr (↑f (↑v₁ j))) i
rw [LinearMap.toMatrix, LinearEquiv.trans_apply, LinearMap.toMatrix'_apply,
  LinearEquiv.arrowCongr_apply, Basis.equivFun_symm_apply, Finset.sum_eq_single j, if_pos rfl,
  one_smul, Basis.equivFun_apply]
case h₀
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1489579
m : Type u_4
n : Type u_5
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j j' : n
a✝ : j' ∈ Finset.univ
hj' : j' ≠ j
⊢ (if j' = j then 1 else 0) • ↑v₁ j' = 0
case h₀
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1489579
m : Type u_4
n : Type u_5
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
⊢ ∀ (b : n), b ∈ Finset.univ → b ≠ j → (if b = j then 1 else 0) • ↑v₁ b = 0
intro j' _ hj'
no goals
case h₀
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1489579
m : Type u_4
n : Type u_5
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j j' : n
a✝ : j' ∈ Finset.univ
hj' : j' ≠ j
⊢ (if j' = j then 1 else 0) • ↑v₁ j' = 0
rw [if_neg hj', zero_smul]
case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1489579
m : Type u_4
n : Type u_5
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
hj : ¬j ∈ Finset.univ
⊢ (if j = j then 1 else 0) • ↑v₁ j = 0
case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1489579
m : Type u_4
n : Type u_5
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
⊢ ¬j ∈ Finset.univ → (if j = j then 1 else 0) • ↑v₁ j = 0
intro hj
case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1489579
m : Type u_4
n : Type u_5
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
hj : ¬j ∈ Finset.univ
this : j ∈ Finset.univ
⊢ (if j = j then 1 else 0) • ↑v₁ j = 0
case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1489579
m : Type u_4
n : Type u_5
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
hj : ¬j ∈ Finset.univ
⊢ (if j = j then 1 else 0) • ↑v₁ j = 0
have := Finset.mem_univ j
no goals
case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type ?u.1489579
m : Type u_4
n : Type u_5
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
hj : ¬j ∈ Finset.univ
this : j ∈ Finset.univ
⊢ (if j = j then 1 else 0) • ↑v₁ j = 0
contradiction