-- Mathlib/LinearAlgebra/SymplecticGroup.lean
theorem symplectic_det (hA : A ∈ symplecticGroup l R) : IsUnit <| det A

Proof state:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : (A * J l R * Aᵀ).det = (J l R).det
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Tactic:
simp only [det_mul, det_transpose] at hA

Result:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A.det * (J l R).det * A.det = (J l R).det
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Proof state:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ (J l R).det * (A.det * A.det) = (J l R).det * 1

Tactic:
rw [mul_one]

Result:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ IsUnit A.det

Tactic:
rw [isUnit_iff_exists_inv]

Result:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ ∃ b, A.det * b = 1

Proof state:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A.det * (J l R).det * A.det = (J l R).det
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Tactic:
rw [mul_comm A.det, mul_assoc] at hA

Result:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : (J l R).det * (A.det * A.det) = (J l R).det
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ ∃ b, A.det * b = 1

Tactic:
use A.det

Result:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ A.det * A.det = 1

Proof state:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Tactic:
rw [mem_iff] at hA

Result:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Proof state:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Tactic:
apply_fun det at hA

Result:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : (A * J l R * Aᵀ).det = (J l R).det
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Proof state:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : (J l R).det * (A.det * A.det) = (J l R).det
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Tactic:
exact hA

Result:
no goals

Proof state:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ A.det * A.det = 1

Tactic:
refine (isUnit_det_J l R).mul_left_cancel ?_

Result:
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ (J l R).det * (A.det * A.det) = (J l R).det * 1