case h.mk
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_1
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := j, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := j, snd := y }
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_1
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
⊢ ↑(Finsupp.basis b).repr
      (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)) =
    single { fst := i, snd := x } 1
ext ⟨j, y⟩
case pos
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_1
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : i = j
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := j, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := j, snd := y }

case neg
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_1
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : ¬i = j
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := j, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := j, snd := y }
case h.mk
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_1
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := j, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := j, snd := y }
by_cases h : i = j
case pos.refl
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_1
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x y : φ i
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := i, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := i, snd := y }
case pos
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_1
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : i = j
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := j, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := j, snd := y }
cases h
no goals
case pos.refl
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_1
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x y : φ i
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := i, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := i, snd := y }
simp only [basis_repr, single_eq_same, Basis.repr_self,
  Finsupp.single_apply_left sigma_mk_injective]
case neg
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_1
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : ¬i = j
this : { fst := i, snd := x } ≠ { fst := j, snd := y }
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := j, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := j, snd := y }
case neg
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_1
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : ¬i = j
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := j, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := j, snd := y }
have : Sigma.mk i x ≠ Sigma.mk j y := fun h' => h <| congrArg (fun s => s.fst) h'
no goals
case neg
R : Type u_2
M : Type u_3
ι : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_1
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : ¬i = j
this : { fst := i, snd := x } ≠ { fst := j, snd := y }
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := j, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := j, snd := y }
simp only [basis_repr, single_apply, h, this, false_and_iff, if_false, LinearEquiv.map_zero,
zero_apply]