no goals
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.785760
inst✝ : CommRing S
P : SL(2, R) → Prop
a b c d : R
hdet : a * d - b * c = 1
⊢ det (↑of ![![a, b], ![c, d]]) = 1
rwa [det_fin_two_of]
case mk
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.785760
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
⊢ P { val := m, property := hm }
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.785760
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
g : SL(2, R)
⊢ P g
obtain ⟨m, hm⟩ := g
case h.e'_1.h.e'_3
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.785760
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
⊢ m = ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]]
case mk
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.785760
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
⊢ P { val := m, property := hm }
convert h (m 0 0) (m 0 1) (m 1 0) (m 1 1) (by rwa [det_fin_two] at hm)
case h.e'_1.h.e'_3.a.h
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.785760
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
i j : Fin 2
⊢ m i j = ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] i j
case h.e'_1.h.e'_3
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.785760
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
⊢ m = ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]]
ext (i j)
no goals
case h.e'_1.h.e'_3.a.h
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.785760
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
i j : Fin 2
⊢ m i j = ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] i j
fin_cases i <;> fin_cases j <;> rfl
no goals
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type ?u.785760
inst✝ : CommRing S
P : SL(2, R) → Prop
h :
  ∀ (a b c d : R) (hdet : a * d - b * c = 1),
    P { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
m : Matrix (Fin 2) (Fin 2) R
hm : det m = 1
⊢ m 0 0 * m 1 1 - m 0 1 * m 1 0 = 1
rwa [det_fin_two] at hm