-- Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
theorem Gamma1_mem (N : ℕ) (A : SL(2, ℤ)) : A ∈ Gamma1 N ↔
    (A 0 0 : ZMod N) = 1 ∧ (A 1 1 : ZMod N) = 1 ∧ (A 1 0 : ZMod N) = 0

Proof state:
case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ ∃ x ∈ ⊤, ((Gamma0 N).subtype.comp (Gamma1' N).subtype) x = A

Tactic:
have hA : A ∈ Gamma0 N := by simp [ha.right.right, Gamma0_mem]

Result:
case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
⊢ ∃ x ∈ ⊤, ((Gamma0 N).subtype.comp (Gamma1' N).subtype) x = A

Proof state:
case mp
N : ℕ
A : SL(2, ℤ)
ha : ∃ x ∈ ⊤, ((Gamma0 N).subtype.comp (Gamma1' N).subtype) x = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Tactic:
obtain ⟨⟨x, hx⟩, hxx⟩ := ha

Result:
case mp.intro.mk
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx : x ∈ Gamma1' N
hxx : ⟨x, hx⟩ ∈ ⊤ ∧ ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx⟩ = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Proof state:
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Tactic:
exact ha

Result:
no goals

Proof state:
case mpr
N : ℕ
A : SL(2, ℤ)
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0 → A ∈ Gamma1 N

Tactic:
intro ha

Result:
case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ A ∈ Gamma1 N

Proof state:
case mp
N : ℕ
A : SL(2, ℤ)
ha : A ∈ Gamma1 N
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Tactic:
simp_rw [Gamma1, Subgroup.mem_map] at ha

Result:
case mp
N : ℕ
A : SL(2, ℤ)
ha : ∃ x ∈ ⊤, ((Gamma0 N).subtype.comp (Gamma1' N).subtype) x = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Proof state:
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
⊢ ⟨A, hA⟩ ∈ Gamma1' N

Tactic:
simp only [Gamma1_to_Gamma0_mem, Subgroup.coe_mk, coe_matrix_coe,
  Int.coe_castRingHom, map_apply]

Result:
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Proof state:
case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
⊢ ∃ x ∈ ⊤, ((Gamma0 N).subtype.comp (Gamma1' N).subtype) x = A

Tactic:
have HA : (⟨A, hA⟩ : Gamma0 N) ∈ Gamma1' N := by
  simp only [Gamma1_to_Gamma0_mem, Subgroup.coe_mk, coe_matrix_coe,
    Int.coe_castRingHom, map_apply]
  exact ha

Result:
case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
HA : ⟨A, hA⟩ ∈ Gamma1' N
⊢ ∃ x ∈ ⊤, ((Gamma0 N).subtype.comp (Gamma1' N).subtype) x = A

Proof state:
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ A ∈ Gamma0 N

Tactic:
simp [ha.right.right, Gamma0_mem]

Result:
no goals

Proof state:
case mp
N : ℕ
A : SL(2, ℤ)
⊢ A ∈ Gamma1 N → ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Tactic:
intro ha

Result:
case mp
N : ℕ
A : SL(2, ℤ)
ha : A ∈ Gamma1 N
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Proof state:
case mp.intro.mk
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx : x ∈ Gamma1' N
hxx : ⟨x, hx⟩ ∈ ⊤ ∧ ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx⟩ = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Tactic:
rw [Gamma1_to_Gamma0_mem] at hx

Result:
case mp.intro.mk
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx : ⟨x, hx✝⟩ ∈ ⊤ ∧ ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩ = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Proof state:
case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ A ∈ Gamma1 N

Tactic:
simp_rw [Gamma1, Subgroup.mem_map]

Result:
case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ ∃ x ∈ ⊤, ((Gamma0 N).subtype.comp (Gamma1' N).subtype) x = A

Proof state:
case mp.intro.mk
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx : ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩ = A
⊢ ↑(↑(((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩) 0 0) = 1 ∧
    ↑(↑(((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩) 1 1) = 1 ∧
      ↑(↑(((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩) 1 0) = 0

Tactic:
convert hx

Result:
no goals

Proof state:
case mp.intro.mk
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx : ⟨x, hx✝⟩ ∈ ⊤ ∧ ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩ = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Tactic:
simp only [Subgroup.mem_top, true_and] at hxx

Result:
case mp.intro.mk
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx : ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩ = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Proof state:
case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
HA : ⟨A, hA⟩ ∈ Gamma1' N
⊢ ∃ x ∈ ⊤, ((Gamma0 N).subtype.comp (Gamma1' N).subtype) x = A

Tactic:
refine ⟨(⟨(⟨A, hA⟩ : Gamma0 N), HA⟩ : (Gamma1' N : Subgroup (Gamma0 N))), ?_⟩

Result:
case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
HA : ⟨A, hA⟩ ∈ Gamma1' N
⊢ ⟨⟨A, hA⟩, HA⟩ ∈ ⊤ ∧ ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨⟨A, hA⟩, HA⟩ = A

Proof state:
case mp.intro.mk
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx : ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩ = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Tactic:
rw [← hxx]

Result:
case mp.intro.mk
N : ℕ
A : SL(2, ℤ)
x : ↥(Gamma0 N)
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx : ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩ = A
⊢ ↑(↑(((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩) 0 0) = 1 ∧
    ↑(↑(((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩) 1 1) = 1 ∧
      ↑(↑(((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨x, hx✝⟩) 1 0) = 0

Proof state:
case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
HA : ⟨A, hA⟩ ∈ Gamma1' N
⊢ ⟨⟨A, hA⟩, HA⟩ ∈ ⊤ ∧ ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⟨⟨A, hA⟩, HA⟩ = A

Tactic:
simp

Result:
no goals

Proof state:
N : ℕ
A : SL(2, ℤ)
⊢ A ∈ Gamma1 N ↔ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

Tactic:
constructor

Result:
case mp
N : ℕ
A : SL(2, ℤ)
⊢ A ∈ Gamma1 N → ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

case mpr
N : ℕ
A : SL(2, ℤ)
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0 → A ∈ Gamma1 N