-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_smul [Module.Free A M] (c : A) (f : M →ₗ[A] M) :
    LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

Proof state:
case pos
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module.Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
this : Module.Finite A M
⊢ LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

Tactic:
simp only [← det_toMatrix (Module.finBasis A M), LinearEquiv.map_smul,
  Fintype.card_fin, Matrix.det_smul]

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✝ : Module.Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
this : Module.finrank A M = 0
⊢ LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

Tactic:
simp [coe_det, H, this]

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✝ : Module.Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

Tactic:
have : Module.finrank A M = 0 := finrank_eq_zero_of_not_exists_basis H

Result:
case neg
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module.Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
this : Module.finrank A M = 0
⊢ LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module.Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
⊢ LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

Tactic:
by_cases H : ∃ s : Finset M, Nonempty (Basis s A M)

Result:
case pos
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module.Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

case neg
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module.Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module.Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ Module.Finite A M

Tactic:
rcases H with ⟨s, ⟨hs⟩⟩

Result:
case intro.intro
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module.Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
s : Finset M
hs : Basis { x // x ∈ s } A M
⊢ Module.Finite A M

Proof state:
case pos
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module.Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

Tactic:
have : Module.Finite A M := by
  rcases H with ⟨s, ⟨hs⟩⟩
  exact Module.Finite.of_basis hs

Result:
case pos
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module.Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
this : Module.Finite A M
⊢ LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

Proof state:
case intro.intro
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module.Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
s : Finset M
hs : Basis { x // x ∈ s } A M
⊢ Module.Finite A M

Tactic:
exact Module.Finite.of_basis hs

Result:
no goals

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module.Free A M
c : A
f : M →ₗ[A] M
⊢ LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

Tactic:
nontriviality A

Result:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module.Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
⊢ LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

Proof state:
case neg
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module.Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f

Tactic:
classical
  have : Module.finrank A M = 0 := finrank_eq_zero_of_not_exists_basis H
  simp [coe_det, H, this]

Result:
no goals