Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
hi12 : i1 ≠ i2
i j : ι
h✝¹ : i2 = i₀
h✝ : i1 = i₀
⊢ 1 i j = 1 i j

pp: case neg
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
hi12 : i1 ≠ i2
i j : ι
h✝¹ : i2 = i₀
h✝ : ¬i1 = i₀
⊢ diagonal (fun k ↦ if k = i1 then D i1 else if k = i₀ then (D i1)⁻¹ else 1) i j =
    diagonal (fun k ↦ if k = i1 then D i1 else if k = i₀ then (D i1)⁻¹ else 1) i j

pp: case pos
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
hi12 : i1 ≠ i2
i j : ι
h✝¹ : ¬i2 = i₀
h✝ : i1 = i₀
⊢ diagonal (fun k ↦ if k = i2 then D i2 else if k = i₀ then (D i2)⁻¹ else 1) i j =
    diagonal (fun k ↦ if k = i2 then D i2 else if k = i₀ then (D i2)⁻¹ else 1) i j

pp: case neg
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
hi12 : i1 ≠ i2
i j : ι
h✝¹ : ¬i2 = i₀
h✝ : ¬i1 = i₀
⊢ diagonal
      (fun i ↦
        if i = i2 then if i = i1 then D i1 * D i2 else if i = i₀ then (D i1)⁻¹ * D i2 else D i2
        else if i = i₀ then if i = i1 then D i1 * (D i2)⁻¹ else (D i1)⁻¹ * (D i2)⁻¹ else if i = i1 then D i1 else 1)
      i j =
    diagonal
      (fun i ↦
        if i = i1 then if i = i2 then D i2 * D i1 else if i = i₀ then (D i2)⁻¹ * D i1 else D i1
        else if i = i₀ then if i = i2 then D i2 * (D i1)⁻¹ else (D i2)⁻¹ * (D i1)⁻¹ else if i = i2 then D i2 else 1)
      i j

Tactic:
<;>

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
hi12 : i1 ≠ i2
i j : ι
h✝¹ : i2 = i₀
h✝ : i1 = i₀
⊢ 1 i j = 1 i j

case neg
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
hi12 : i1 ≠ i2
i j : ι
h✝¹ : i2 = i₀
h✝ : ¬i1 = i₀
⊢ diagonal (fun k ↦ if k = i1 then D i1 else if k = i₀ then (D i1)⁻¹ else 1) i j =
    diagonal (fun k ↦ if k = i1 then D i1 else if k = i₀ then (D i1)⁻¹ else 1) i j

case pos
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
hi12 : i1 ≠ i2
i j : ι
h✝¹ : ¬i2 = i₀
h✝ : i1 = i₀
⊢ diagonal (fun k ↦ if k = i2 then D i2 else if k = i₀ then (D i2)⁻¹ else 1) i j =
    diagonal (fun k ↦ if k = i2 then D i2 else if k = i₀ then (D i2)⁻¹ else 1) i j

case neg
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
hi12 : i1 ≠ i2
i j : ι
h✝¹ : ¬i2 = i₀
h✝ : ¬i1 = i₀
⊢ diagonal
      (fun i ↦
        if i = i2 then if i = i1 then D i1 * D i2 else if i = i₀ then (D i1)⁻¹ * D i2 else D i2
        else if i = i₀ then if i = i1 then D i1 * (D i2)⁻¹ else (D i1)⁻¹ * (D i2)⁻¹ else if i = i1 then D i1 else 1)
      i j =
    diagonal
      (fun i ↦
        if i = i1 then if i = i2 then D i2 * D i1 else if i = i₀ then (D i2)⁻¹ * D i1 else D i1
        else if i = i₀ then if i = i2 then D i2 * (D i1)⁻¹ else (D i2)⁻¹ * (D i1)⁻¹ else if i = i2 then D i2 else 1)
      i j