-- Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
theorem Gamma1_to_Gamma0_mem {N} (A : Gamma0 N) :
    A ∈ Gamma1' N ↔
    ((A.1 0 0 : ℤ) : ZMod N) = 1 ∧ ((A.1 1 1 : ℤ) : ZMod N) = 1
      ∧ ((A.1 1 0 : ℤ) : ZMod N) = 0

Proof state:
case mp
N : ℕ
A : ↥(Gamma0 N)
ha : A ∈ Gamma1' N
adet : ↑(↑↑A).det = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0

Tactic:
rw [Matrix.det_fin_two] at adet

Result:
case mp
N : ℕ
A : ↥(Gamma0 N)
ha : A ∈ Gamma1' N
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

Proof state:
N : ℕ
A : ↥(Gamma0 N)
ha : A ∈ Gamma1' N
⊢ ↑(↑↑A).det = 1

Tactic:
simp only [A.1.property, Int.cast_one]

Result:
no goals

Proof state:
N : ℕ
A : ↥(Gamma0 N)
⊢ A ∈ Gamma1' N ↔ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0

Tactic:
constructor

Result:
case mp
N : ℕ
A : ↥(Gamma0 N)
⊢ A ∈ Gamma1' N → ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0

case mpr
N : ℕ
A : ↥(Gamma0 N)
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0 → A ∈ Gamma1' N

Proof state:
case mp
N : ℕ
A : ↥(Gamma0 N)
ha : A ∈ Gamma1' N
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0

Tactic:
have adet : (A.1.1.det : ZMod N) = 1 := by simp only [A.1.property, Int.cast_one]

Result:
case mp
N : ℕ
A : ↥(Gamma0 N)
ha : A ∈ Gamma1' N
adet : ↑(↑↑A).det = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0

Proof state:
case mpr
N : ℕ
A : ↥(Gamma0 N)
ha : ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
⊢ { toFun := fun g => ↑(↑↑g 1 1), map_one' := ⋯ } A = 1

Tactic:
exact ha.2.1

Result:
no goals

Proof state:
case mpr
N : ℕ
A : ↥(Gamma0 N)
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0 → A ∈ Gamma1' N

Tactic:
intro ha

Result:
case mpr
N : ℕ
A : ↥(Gamma0 N)
ha : ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
⊢ A ∈ Gamma1' N

Proof state:
case mp
N : ℕ
A : ↥(Gamma0 N)
⊢ A ∈ Gamma1' N → ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0

Tactic:
intro ha

Result:
case mp
N : ℕ
A : ↥(Gamma0 N)
ha : A ∈ Gamma1' N
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0

Proof state:
case mp
N : ℕ
A : ↥(Gamma0 N)
ha : A ∈ Gamma1' N
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

Tactic:
simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, OneHom.coe_mk, Int.cast_sub,
  Int.cast_mul] at *

Result:
case mp
N : ℕ
A : ↥(Gamma0 N)
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

Proof state:
case mp
N : ℕ
A : ↥(Gamma0 N)
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

Tactic:
simpa only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, OneHom.coe_mk, Int.cast_sub,
  Int.cast_mul, ha, Gamma0_mem.mp A.property, and_self_iff, and_true, mul_one, mul_zero,
  sub_zero] using adet

Result:
no goals

Proof state:
case mpr
N : ℕ
A : ↥(Gamma0 N)
ha : ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
⊢ A ∈ Gamma1' N

Tactic:
simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, coe_matrix_coe,
  Int.coe_castRingHom, map_apply]

Result:
case mpr
N : ℕ
A : ↥(Gamma0 N)
ha : ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
⊢ { toFun := fun g => ↑(↑↑g 1 1), map_one' := ⋯ } A = 1