-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_conj' (f : M →ₗ[R] M) (e : M ≃ₗ[R] N) : trace R N (e.conj f) = trace R M f

Proof state:
case pos.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis { x // x ∈ s } R M
this✝¹ : Module.Finite R M
this✝ : Free R M
this : Module.Finite R N
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
haveI := (Module.free_def R N).mpr ⟨_, ⟨(b.map e).reindex (e.toEquiv.image _)⟩⟩

Result:
case pos.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis { x // x ∈ s } R M
this✝² : Module.Finite R M
this✝¹ : Free R M
this✝ : Module.Finite R N
this : Free R N
⊢ (trace R N) (e.conj f) = (trace R M) f

Proof state:
case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
obtain ⟨s, ⟨b⟩⟩ := hM

Result:
case pos.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ (trace R N) (e.conj f) = (trace R M) f

Proof state:
case pos.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis { x // x ∈ s } R M
this✝ : Module.Finite R M
this : Free R M
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
haveI := Module.Finite.of_basis (b.map e)

Result:
case pos.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis { x // x ∈ s } R M
this✝¹ : Module.Finite R M
this✝ : Free R M
this : Module.Finite R N
⊢ (trace R N) (e.conj f) = (trace R M) f

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ ¬∃ s, Nonempty (Basis { x // x ∈ s } R N)

Tactic:
rintro ⟨s, ⟨b⟩⟩

Result:
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
s : Finset N
b : Basis { x // x ∈ s } R N
⊢ False

Proof state:
case pos.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
haveI := Module.Finite.of_basis b

Result:
case pos.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis { x // x ∈ s } R M
this : Module.Finite R M
⊢ (trace R N) (e.conj f) = (trace R M) f

Proof state:
case pos.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis { x // x ∈ s } R M
this : Module.Finite R M
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
haveI := (Module.free_def R M).mpr ⟨_, ⟨b⟩⟩

Result:
case pos.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis { x // x ∈ s } R M
this✝ : Module.Finite R M
this : Free R M
⊢ (trace R N) (e.conj f) = (trace R M) f

Proof state:
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
rw [trace, trace, dif_neg hM, dif_neg ?_, zero_apply, zero_apply]

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ ¬∃ s, Nonempty (Basis { x // x ∈ s } R N)

Proof state:
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
s : Finset N
b : Basis { x // x ∈ s } R N
⊢ False

Tactic:
exact hM ⟨s.image e.symm, ⟨(b.map e.symm).reindex
  ((e.symm.toEquiv.image s).trans (Equiv.Set.ofEq Finset.coe_image.symm))⟩⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
by_cases hM : ∃ s : Finset M, Nonempty (Basis s R M)

Result:
case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ (trace R N) (e.conj f) = (trace R M) f

case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ (trace R N) (e.conj f) = (trace R M) f

Proof state:
case pos.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis { x // x ∈ s } R M
this✝² : Module.Finite R M
this✝¹ : Free R M
this✝ : Module.Finite R N
this : Free R N
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
  LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]

Result:
no goals