case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
⊢ A ∈ Gamma1' N → ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0

case mpr
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0 → A ∈ Gamma1' N
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
⊢ A ∈ Gamma1' N ↔ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
constructor
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
⊢ A ∈ Gamma1' N → ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
intro ha
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑A ∈ Gamma0 N
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
have hA := A.property
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑(↑↑A 1 0) = 0
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑A ∈ Gamma0 N
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
rw [Gamma0_mem] at hA
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑(↑↑A 1 0) = 0
adet : ↑(det ↑↑A) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑(↑↑A 1 0) = 0
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
have adet := Gamma0_det N A
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑(↑↑A 1 0) = 0
adet : ↑(↑↑A 0 0 * ↑↑A 1 1 - ↑↑A 0 1 * ↑↑A 1 0) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑(↑↑A 1 0) = 0
adet : ↑(det ↑↑A) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
rw [Matrix.det_fin_two] at adet
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
hA : ↑(↑↑A 1 0) = 0
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) * ↑(↑↑A 1 1) - ↑(↑↑A 0 1) * ↑(↑↑A 1 0) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑(↑↑A 1 0) = 0
adet : ↑(↑↑A 0 0 * ↑↑A 1 1 - ↑↑A 0 1 * ↑↑A 1 0) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
simp only [Gamma0Map, coe_matrix_coe, Int.coe_castRingHom, map_apply, Gamma1_mem',
  MonoidHom.coe_mk, OneHom.coe_mk, Int.cast_sub, Int.cast_mul] at *
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
hA : ↑(↑↑A 1 0) = 0
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) * 1 - ↑(↑↑A 0 1) * 0 = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
hA : ↑(↑↑A 1 0) = 0
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) * ↑(↑↑A 1 1) - ↑(↑↑A 0 1) * ↑(↑↑A 1 0) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
rw [hA, ha] at adet
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
hA : ↑(↑↑A 1 0) = 0
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
hA : ↑(↑↑A 1 0) = 0
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) * 1 - ↑(↑↑A 0 1) * 0 = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
simp only [mul_one, MulZeroClass.mul_zero, sub_zero] at adet
no goals
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
hA : ↑(↑↑A 1 0) = 0
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
simp only [adet, hA, ha, eq_self_iff_true, and_self_iff]
case mpr
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
⊢ A ∈ Gamma1' N
case mpr
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0 → A ∈ Gamma1' N
intro ha
case mpr
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
⊢ ↑{ toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } A = 1
case mpr
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
⊢ A ∈ Gamma1' N
simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, coe_matrix_coe,
  Int.coe_castRingHom, map_apply]
no goals
case mpr
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
⊢ ↑{ toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } A = 1
exact ha.2.1