Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : e t_j = b
hab : a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

pp: case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : e t_j = b
hab : ¬a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

pp: case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : ¬e t_j = b
hab : a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

pp: case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : ¬e t_j = b
hab : ¬a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

pp: case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : e t_j = b
hab : a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

pp: case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : e t_j = b
hab : ¬a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

pp: case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : ¬e t_j = b
hab : a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

pp: case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : ¬e t_j = b
hab : ¬a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

Tactic:
<;>

Goal state after:
case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : e t_j = b
hab : a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : e t_j = b
hab : ¬a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : ¬e t_j = b
hab : a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : ¬e t_j = b
hab : ¬a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : e t_j = b
hab : a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : e t_j = b
hab : ¬a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : ¬e t_j = b
hab : a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : ¬e t_j = b
hab : ¬a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b