R : Type ?u.616312
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.616903
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.617445
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.618421
inst✝¹ : Fintype κ
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P (det (↑(toMatrix b b) f))
h1 : P 1
⊢ P
    (↑(if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then
          detAux (Trunc.mk (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose H } A M))))
        else 1)
      f)
R : Type ?u.616312
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.616903
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.617445
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.618421
inst✝¹ : Fintype κ
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P (det (↑(toMatrix b b) f))
h1 : P 1
⊢ P (↑LinearMap.det f)
rw [LinearMap.det_def]
case inl
R : Type ?u.616312
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.616903
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.617445
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.618421
inst✝¹ : Fintype κ
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P (det (↑(toMatrix b b) f))
h1 : P 1
h : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ P (↑(detAux (Trunc.mk (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose h } A M))))) f)

case inr
R : Type ?u.616312
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.616903
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.617445
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.618421
inst✝¹ : Fintype κ
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P (det (↑(toMatrix b b) f))
h1 : P 1
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ P (↑1 f)
R : Type ?u.616312
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.616903
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.617445
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.618421
inst✝¹ : Fintype κ
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P (det (↑(toMatrix b b) f))
h1 : P 1
⊢ P
    (↑(if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then
          detAux (Trunc.mk (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose H } A M))))
        else 1)
      f)
split_ifs with h
case h.e'_1
R : Type ?u.616312
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.616903
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.617445
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.618421
inst✝¹ : Fintype κ
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P (det (↑(toMatrix b b) f))
h1 : P 1
h : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ ↑(detAux (Trunc.mk (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose h } A M))))) f =
    det
      (↑(toMatrix (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose h } A M)))
            (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose h } A M))))
        f)
case inl
R : Type ?u.616312
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.616903
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.617445
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.618421
inst✝¹ : Fintype κ
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P (det (↑(toMatrix b b) f))
h1 : P 1
h : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ P (↑(detAux (Trunc.mk (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose h } A M))))) f)
convert hb _ h.choose_spec.some
no goals
case h.e'_1
R : Type ?u.616312
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.616903
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.617445
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.618421
inst✝¹ : Fintype κ
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P (det (↑(toMatrix b b) f))
h1 : P 1
h : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ ↑(detAux (Trunc.mk (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose h } A M))))) f =
    det
      (↑(toMatrix (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose h } A M)))
            (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose h } A M))))
        f)
convert detAux_def'' (Trunc.mk h.choose_spec.some) h.choose_spec.some f
no goals
case inr
R : Type ?u.616312
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.616903
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.617445
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.618421
inst✝¹ : Fintype κ
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis { x // x ∈ s } A M), P (det (↑(toMatrix b b) f))
h1 : P 1
h : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ P (↑1 f)
exact h1