-- Mathlib/NumberTheory/Modular.lean
theorem bottom_row_surj {R : Type*} [CommRing R] :
    Set.SurjOn (fun g : SL(2, R) => (↑g : Matrix (Fin 2) (Fin 2) R) 1) Set.univ
      {cd | IsCoprime (cd 0) (cd 1)}

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
⊢ cd ∈ (fun g => ↑g 1) '' Set.univ

Tactic:
have det_A_1 : det A = 1 := by
  convert gcd_eqn
  rw [det_fin_two]
  simp [A, (by ring : a * cd 1 + b₀ * cd 0 = b₀ * cd 0 + a * cd 1)]

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
det_A_1 : A.det = 1
⊢ cd ∈ (fun g => ↑g 1) '' Set.univ

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ Set.SurjOn (fun g => ↑g 1) Set.univ {cd | IsCoprime (cd 0) (cd 1)}

Tactic:
rintro cd ⟨b₀, a, gcd_eqn⟩

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
⊢ cd ∈ (fun g => ↑g 1) '' Set.univ

Proof state:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
⊢ A.det = b₀ * cd 0 + a * cd 1

Tactic:
rw [det_fin_two]

Result:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
⊢ A 0 0 * A 1 1 - A 0 1 * A 1 0 = b₀ * cd 0 + a * cd 1

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
⊢ cd ∈ (fun g => ↑g 1) '' Set.univ

Tactic:
let A := of ![![a, -b₀], cd]

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
⊢ cd ∈ (fun g => ↑g 1) '' Set.univ

Proof state:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
⊢ A 0 0 * A 1 1 - A 0 1 * A 1 0 = b₀ * cd 0 + a * cd 1

Tactic:
simp [A, (by ring : a * cd 1 + b₀ * cd 0 = b₀ * cd 0 + a * cd 1)]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
⊢ a * cd 1 + b₀ * cd 0 = b₀ * cd 0 + a * cd 1

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
⊢ A.det = 1

Tactic:
convert gcd_eqn

Result:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
⊢ A.det = b₀ * cd 0 + a * cd 1

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
det_A_1 : A.det = 1
⊢ (fun g => ↑g 1) ⟨A, det_A_1⟩ = cd

Tactic:
ext

Result:
case intro.intro.h
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
det_A_1 : A.det = 1
x✝ : Fin 2
⊢ (fun g => ↑g 1) ⟨A, det_A_1⟩ x✝ = cd x✝

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
det_A_1 : A.det = 1
⊢ cd ∈ (fun g => ↑g 1) '' Set.univ

Tactic:
refine ⟨⟨A, det_A_1⟩, Set.mem_univ _, ?_⟩

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
det_A_1 : A.det = 1
⊢ (fun g => ↑g 1) ⟨A, det_A_1⟩ = cd

Proof state:
case intro.intro.h
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
det_A_1 : A.det = 1
x✝ : Fin 2
⊢ (fun g => ↑g 1) ⟨A, det_A_1⟩ x✝ = cd x✝

Tactic:
simp [A]

Result:
no goals