case h
N : ℕ
x✝ : SL(2, ℤ)
⊢ x✝ ∈ Gamma 0 ↔ x✝ ∈ ⊥
N : ℕ
⊢ Gamma 0 = ⊥
ext
case h
N : ℕ
x✝ : SL(2, ℤ)
⊢ ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1 ↔ x✝ = 1
case h
N : ℕ
x✝ : SL(2, ℤ)
⊢ x✝ ∈ Gamma 0 ↔ x✝ ∈ ⊥
simp only [Gamma_mem, coe_matrix_coe, Int.coe_castRingHom, map_apply, Int.cast_id,
  Subgroup.mem_bot]
case h.mp
N : ℕ
x✝ : SL(2, ℤ)
⊢ ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1 → x✝ = 1

case h.mpr
N : ℕ
x✝ : SL(2, ℤ)
⊢ x✝ = 1 → ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
case h
N : ℕ
x✝ : SL(2, ℤ)
⊢ ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1 ↔ x✝ = 1
constructor
case h.mp
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ x✝ = 1
case h.mp
N : ℕ
x✝ : SL(2, ℤ)
⊢ ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1 → x✝ = 1
intro h
case h.mp.a
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
i : Fin 2
⊢ ∀ (j : Fin 2), ↑x✝ i j = ↑1 i j
case h.mp
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ x✝ = 1
ext i
case h.mp.a
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
i j : Fin 2
⊢ ↑x✝ i j = ↑1 i j
case h.mp.a
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
i : Fin 2
⊢ ∀ (j : Fin 2), ↑x✝ i j = ↑1 i j
intro j
case h.mp.a.head.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }

case h.mp.a.head.tail.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }

case h.mp.a.tail.head.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }

case h.mp.a.tail.head.tail.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
case h.mp.a
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
i j : Fin 2
⊢ ↑x✝ i j = ↑1 i j
fin_cases i <;> fin_cases j <;> simp only [h]
no goals
case h.mp.a.head.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }

case h.mp.a.head.tail.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }

case h.mp.a.tail.head.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }

case h.mp.a.tail.head.tail.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
exacts [h.1, h.2.1, h.2.2.1, h.2.2.2]
case h.mpr
N : ℕ
x✝ : SL(2, ℤ)
h : x✝ = 1
⊢ ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
case h.mpr
N : ℕ
x✝ : SL(2, ℤ)
⊢ x✝ = 1 → ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
intro h
no goals
case h.mpr
N : ℕ
x✝ : SL(2, ℤ)
h : x✝ = 1
⊢ ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
simp [h]