no goals
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type ?u.848542
inst✝¹ : CommRing S
R : Type ?u.848548
inst✝ : Field R
g : SL(2, R)
hg : ↑g 1 0 = 0
a b : R
h : a ≠ 0
⊢ det (↑of ![![a, b], ![0, a⁻¹]]) = 1
simp [h]
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type ?u.848542
inst✝¹ : CommRing S
R : Type u_1
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : ↑{ val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } 1 0 = 0
⊢ ∃ a_1 b_1 h,
    { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
      { val := ↑of ![![a_1, b_1], ![0, a_1⁻¹]], property := (_ : det (↑of ![![a_1, b_1], ![0, a_1⁻¹]]) = 1) }
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type ?u.848542
inst✝¹ : CommRing S
R : Type u_1
inst✝ : Field R
g : SL(2, R)
hg : ↑g 1 0 = 0
⊢ ∃ a b h, g = { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) }
induction' g using Matrix.SpecialLinearGroup.fin_two_induction with a b c d h_det
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type ?u.848542
inst✝¹ : CommRing S
R : Type u_1
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
⊢ ∃ a_1 b_1 h,
    { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
      { val := ↑of ![![a_1, b_1], ![0, a_1⁻¹]], property := (_ : det (↑of ![![a_1, b_1], ![0, a_1⁻¹]]) = 1) }
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type ?u.848542
inst✝¹ : CommRing S
R : Type u_1
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : ↑{ val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } 1 0 = 0
⊢ ∃ a_1 b_1 h,
    { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
      { val := ↑of ![![a_1, b_1], ![0, a_1⁻¹]], property := (_ : det (↑of ![![a_1, b_1], ![0, a_1⁻¹]]) = 1) }
replace hg : c = 0 := by simpa using hg
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type ?u.848542
inst✝¹ : CommRing S
R : Type u_1
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ ∃ a_1 b_1 h,
    { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
      { val := ↑of ![![a_1, b_1], ![0, a_1⁻¹]], property := (_ : det (↑of ![![a_1, b_1], ![0, a_1⁻¹]]) = 1) }
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type ?u.848542
inst✝¹ : CommRing S
R : Type u_1
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
⊢ ∃ a_1 b_1 h,
    { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
      { val := ↑of ![![a_1, b_1], ![0, a_1⁻¹]], property := (_ : det (↑of ![![a_1, b_1], ![0, a_1⁻¹]]) = 1) }
have had : a * d = 1 := by rwa [hg, MulZeroClass.mul_zero, sub_zero] at h_det
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type ?u.848542
inst✝¹ : CommRing S
R : Type u_1
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
    { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) }
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type ?u.848542
inst✝¹ : CommRing S
R : Type u_1
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ ∃ a_1 b_1 h,
    { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
      { val := ↑of ![![a_1, b_1], ![0, a_1⁻¹]], property := (_ : det (↑of ![![a_1, b_1], ![0, a_1⁻¹]]) = 1) }
refine' ⟨a, b, left_ne_zero_of_mul_eq_one had, _⟩
no goals
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type ?u.848542
inst✝¹ : CommRing S
R : Type u_1
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
    { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) }
simp_rw [eq_inv_of_mul_eq_one_right had, hg]
no goals
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type ?u.848542
inst✝¹ : CommRing S
R : Type u_1
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : ↑{ val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } 1 0 = 0
⊢ c = 0
simpa using hg
no goals
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type ?u.848542
inst✝¹ : CommRing S
R : Type u_1
inst✝ : Field R
g : SL(2, R)
hg✝ : ↑g 1 0 = 0
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
⊢ a * d = 1
rwa [hg, MulZeroClass.mul_zero, sub_zero] at h_det