-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_cases [DecidableEq M] {P : A → Prop} (f : M →ₗ[A] M)
    (hb : ∀ (s : Finset M) (b : Basis s A M), P (Matrix.det (toMatrix b b f))) (h1 : P 1) :
    P (LinearMap.det f)

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P ((toMatrix b b) f).det
h1 : P 1
⊢ P (LinearMap.det f)

Tactic:
rw [LinearMap.det_def]

Result:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P ((toMatrix b b) f).det
h1 : P 1
⊢ P ((if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then detAux (Trunc.mk ⋯.some) else 1) f)

Proof state:
case pos
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P ((toMatrix b b) f).det
h1 : P 1
h : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ P ((detAux (Trunc.mk ⋯.some)) f)

Tactic:
convert hb _ h.choose_spec.some

Result:
case h.e'_1
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P ((toMatrix b b) f).det
h1 : P 1
h : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ (detAux (Trunc.mk ⋯.some)) f = ((toMatrix ⋯.some ⋯.some) f).det

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P ((toMatrix b b) f).det
h1 : P 1
⊢ P ((if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then detAux (Trunc.mk ⋯.some) else 1) f)

Tactic:
split_ifs with h

Result:
case pos
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P ((toMatrix b b) f).det
h1 : P 1
h : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ P ((detAux (Trunc.mk ⋯.some)) f)

case neg
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P ((toMatrix b b) f).det
h1 : P 1
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ P (1 f)

Proof state:
case h.e'_1
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P ((toMatrix b b) f).det
h1 : P 1
h : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ (detAux (Trunc.mk ⋯.some)) f = ((toMatrix ⋯.some ⋯.some) f).det

Tactic:
convert detAux_def'' (Trunc.mk h.choose_spec.some) h.choose_spec.some f

Result:
no goals

Proof state:
case neg
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P ((toMatrix b b) f).det
h1 : P 1
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ P (1 f)

Tactic:
exact h1

Result:
no goals