[GOAL]
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ det (adjugate ↑A) = 1
[PROOFSTEP]
rw [det_adjugate, A.prop, one_pow]
[GOAL]
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A B : SpecialLinearGroup n R
⊢ det (↑A * ↑B) = 1
[PROOFSTEP]
rw [det_mul, A.prop, B.prop, one_mul]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
A B : SpecialLinearGroup n R
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
⊢ det ↑g ≠ 0
[PROOFSTEP]
rw [g.det_coe]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
A B : SpecialLinearGroup n R
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
⊢ 1 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
A B : SpecialLinearGroup n R
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
i : n
h : ↑g i = 0
⊢ ∀ (j : n), ↑g i j = 0
[PROOFSTEP]
simp [h]
[GOAL]
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
src✝¹ : Monoid (SpecialLinearGroup n R) := monoid
src✝ : Inv (SpecialLinearGroup n R) := hasInv
A : SpecialLinearGroup n R
⊢ A⁻¹ * A = 1
[PROOFSTEP]
ext1
[GOAL]
case a
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
src✝¹ : Monoid (SpecialLinearGroup n R) := monoid
src✝ : Inv (SpecialLinearGroup n R) := hasInv
A : SpecialLinearGroup n R
i✝ j✝ : n
⊢ ↑(A⁻¹ * A) i✝ j✝ = ↑1 i✝ j✝
[PROOFSTEP]
simp [adjugate_mul]
[GOAL]
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ comp (↑Matrix.toLin' ↑A) (↑Matrix.toLin' ↑A⁻¹) = LinearMap.id
[PROOFSTEP]
rw [← toLin'_mul, ← coe_mul, mul_right_inv, coe_one, toLin'_one]
[GOAL]
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ comp (↑Matrix.toLin' ↑A⁻¹) (↑Matrix.toLin' ↑A) = LinearMap.id
[PROOFSTEP]
rw [← toLin'_mul, ← coe_mul, mul_left_inv, coe_one, toLin'_one]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : SpecialLinearGroup n R
⊢ det (↑(RingHom.mapMatrix f) ↑g) = 1
[PROOFSTEP]
rw [← f.map_det]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : SpecialLinearGroup n R
⊢ ↑f (det ↑g) = 1
[PROOFSTEP]
simp [g.prop]
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Fact (Even (Fintype.card n))
g : SpecialLinearGroup n R
⊢ det (-↑g) = 1
[PROOFSTEP]
simpa [(@Fact.out <| Even <| Fintype.card n).neg_one_pow, g.det_coe] using det_smul (↑ₘg) (-1)
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
⊢ det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1
[PROOFSTEP]
rw [Matrix.det_fin_two, mul_comm]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
⊢ vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 1 1 * vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 0 0 -
      vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 0 1 * vecCons ![↑A 1 1, -↑A 0 1] ![![-↑A 1 0, ↑A 0 0]] 1 0 =
    1
[PROOFSTEP]
simp only [cons_val_zero, cons_val_one, head_cons, mul_neg, neg_mul, neg_neg]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
[PROOFSTEP]
have := A.2
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
this : det ↑A = 1
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
[PROOFSTEP]
rw [Matrix.det_fin_two] at this 
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
this : ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
[PROOFSTEP]
convert this
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
⊢ A⁻¹ =
    { val := ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]],
      property := (_ : det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1) }
[PROOFSTEP]
ext
[GOAL]
case a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
i✝ j✝ : Fin 2
⊢ ↑A⁻¹ i✝ j✝ =
    ↑{ val := ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]],
          property := (_ : det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1) }
      i✝ j✝
[PROOFSTEP]
have := Matrix.adjugate_fin_two A.1
[GOAL]
case a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
i✝ j✝ : Fin 2
this : adjugate ↑A = ↑of ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]]
⊢ ↑A⁻¹ i✝ j✝ =
    ↑{ val := ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]],
          property := (_ : det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1) }
      i✝ j✝
[PROOFSTEP]
rw [coe_inv, this]
[GOAL]
case a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
A : SL(2, R)
i✝ j✝ : Fin 2
this : adjugate ↑A = ↑of ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]]
⊢ ↑of ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] i✝ j✝ =
    ↑{ val := ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]],
          property := (_ : det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1) }
      i✝ j✝
[PROOFSTEP]
rfl
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
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
[PROOFSTEP]
rwa [det_fin_two_of]
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
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
[PROOFSTEP]
obtain ⟨m, hm⟩ := g
[GOAL]
case mk
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
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 }
[PROOFSTEP]
convert h (m 0 0) (m 0 1) (m 1 0) (m 1 1) (by rwa [det_fin_two] at hm )
[GOAL]
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
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
[PROOFSTEP]
rwa [det_fin_two] at hm 
[GOAL]
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_1
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]]
[PROOFSTEP]
ext i j
[GOAL]
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_1
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
[PROOFSTEP]
fin_cases i
[GOAL]
case h.e'_1.h.e'_3.a.h.head
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
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
j : Fin 2
⊢ m { val := 0, isLt := (_ : 0 < 2) } j = ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case h.e'_1.h.e'_3.a.h.tail.head
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
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
j : Fin 2
⊢ m { val := 1, isLt := (_ : (fun a => a < 2) 1) } j =
    ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case h.e'_1.h.e'_3.a.h.head.head
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
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 { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
rfl
[GOAL]
case h.e'_1.h.e'_3.a.h.head.tail.head
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
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 { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] { val := 0, isLt := (_ : 0 < 2) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
rfl
[GOAL]
case h.e'_1.h.e'_3.a.h.tail.head.head
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
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 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
rfl
[GOAL]
case h.e'_1.h.e'_3.a.h.tail.head.tail.head
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
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 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![m 0 0, m 0 1], ![m 1 0, m 1 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
rfl
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
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
[PROOFSTEP]
simp [h]
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
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) }
[PROOFSTEP]
induction' g using Matrix.SpecialLinearGroup.fin_two_induction with a b c d h_det
[GOAL]
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
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) }
[PROOFSTEP]
replace hg : c = 0 := by simpa using hg
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
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
[PROOFSTEP]
simpa using hg
[GOAL]
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
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) }
[PROOFSTEP]
have had : a * d = 1 := by rwa [hg, mul_zero, sub_zero] at h_det 
[GOAL]
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
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
[PROOFSTEP]
rwa [hg, mul_zero, sub_zero] at h_det 
[GOAL]
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
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) }
[PROOFSTEP]
refine' ⟨a, b, left_ne_zero_of_mul_eq_one had, _⟩
[GOAL]
case h
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
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) }
[PROOFSTEP]
simp_rw [eq_inv_of_mul_eq_one_right had, hg]
[GOAL]
⊢ det (↑of ![![0, -1], ![1, 0]]) = 1
[PROOFSTEP]
norm_num [Matrix.det_fin_two_of]
[GOAL]
⊢ det (↑of ![![1, 1], ![0, 1]]) = 1
[PROOFSTEP]
norm_num [Matrix.det_fin_two_of]
[GOAL]
⊢ ↑T⁻¹ = ↑of ![![1, -1], ![0, 1]]
[PROOFSTEP]
simp [coe_inv, coe_T, adjugate_fin_two]
[GOAL]
n : ℤ
⊢ ↑(T ^ n) = ↑of ![![1, n], ![0, 1]]
[PROOFSTEP]
induction' n using Int.induction_on with n h n h
[GOAL]
case hz
⊢ ↑(T ^ 0) = ↑of ![![1, 0], ![0, 1]]
[PROOFSTEP]
rw [zpow_zero, coe_one, Matrix.one_fin_two]
[GOAL]
case hp
n : ℕ
h : ↑(T ^ ↑n) = ↑of ![![1, ↑n], ![0, 1]]
⊢ ↑(T ^ (↑n + 1)) = ↑of ![![1, ↑n + 1], ![0, 1]]
[PROOFSTEP]
simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]
  -- Porting note: was congrm !![_, _; _, _]
[GOAL]
case hp
n : ℕ
h : ↑(T ^ ↑n) = ↑of ![![1, ↑n], ![0, 1]]
⊢ ↑of ![![1 * 1 + ↑n * 0, 1 * 1 + ↑n * 1], ![0 * 1 + 1 * 0, 0 * 1 + 1 * 1]] = ↑of ![![1, ↑n + 1], ![0, 1]]
[PROOFSTEP]
ring_nf
[GOAL]
case hn
n : ℕ
h : ↑(T ^ (-↑n)) = ↑of ![![1, -↑n], ![0, 1]]
⊢ ↑(T ^ (-↑n - 1)) = ↑of ![![1, -↑n - 1], ![0, 1]]
[PROOFSTEP]
simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]
  -- Porting note: was congrm !![_, _; _, _]
[GOAL]
case hn
n : ℕ
h : ↑(T ^ (-↑n)) = ↑of ![![1, -↑n], ![0, 1]]
⊢ ↑of ![![1 * 1 + -↑n * 0, 1 * -1 + -↑n * 1], ![0 * 1 + 1 * 0, 0 * -1 + 1 * 1]] = ↑of ![![1, -↑n - 1], ![0, 1]]
[PROOFSTEP]
ring_nf
[GOAL]
n : ℤ
g : SL(2, ℤ)
⊢ ↑(T ^ n * g) 1 = ↑g 1
[PROOFSTEP]
ext j
[GOAL]
case h
n : ℤ
g : SL(2, ℤ)
j : Fin 2
⊢ ↑(T ^ n * g) 1 j = ↑g 1 j
[PROOFSTEP]
simp [coe_T_zpow, Matrix.vecMul, Matrix.dotProduct, Fin.sum_univ_succ, vecTail]
[GOAL]
g : SL(2, ℤ)
⊢ ↑(T * g) 1 = ↑g 1
[PROOFSTEP]
simpa using T_pow_mul_apply_one 1 g
[GOAL]
g : SL(2, ℤ)
⊢ ↑(T⁻¹ * g) 1 = ↑g 1
[PROOFSTEP]
simpa using T_pow_mul_apply_one (-1) g
