Theorem: LinearEquiv.dualAnnihilator_map_eq (Matroid/ForMathlib/LinearAlgebra/Dual.lean)

State before:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
⊢ (map e U).dualAnnihilator = map e.symm.dualMap U.dualAnnihilator
Tactic:
ext x
State after:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ x ∈ (map e U).dualAnnihilator ↔ x ∈ map e.symm.dualMap U.dualAnnihilator

State before:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ x ∈ (map e U).dualAnnihilator ↔ x ∈ map e.symm.dualMap U.dualAnnihilator
Tactic:
simp only [mem_dualAnnihilator, mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
  dualMap_apply_symm]
State after:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ (∀ a ∈ U, x (e a) = 0) ↔ ∃ y, (∀ w ∈ U, y w = 0) ∧ y ∘ₗ ↑e.symm = x

State before:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ (∀ a ∈ U, x (e a) = 0) ↔ ∃ y, (∀ w ∈ U, y w = 0) ∧ y ∘ₗ ↑e.symm = x
Tactic:
refine ⟨fun h ↦ ⟨e.dualMap x, h, by ext; simp⟩, ?_⟩
State after:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ (∃ y, (∀ w ∈ U, y w = 0) ∧ y ∘ₗ ↑e.symm = x) → ∀ a ∈ U, x (e a) = 0

State before:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
⊢ (∃ y, (∀ w ∈ U, y w = 0) ∧ y ∘ₗ ↑e.symm = x) → ∀ a ∈ U, x (e a) = 0
Tactic:
rintro ⟨y, hy, rfl⟩ x hxu
State after:
case h.intro.intro
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
y : Module.Dual R M
hy : ∀ w ∈ U, y w = 0
x : M
hxu : x ∈ U
⊢ (y ∘ₗ ↑e.symm) (e x) = 0

State before:
case h.intro.intro
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
y : Module.Dual R M
hy : ∀ w ∈ U, y w = 0
x : M
hxu : x ∈ U
⊢ (y ∘ₗ ↑e.symm) (e x) = 0
Tactic:
simpa using hy x hxu
State after:
no goals

State before:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
h : ∀ a ∈ U, x (e a) = 0
⊢ e.dualMap x ∘ₗ ↑e.symm = x
Tactic:
ext
State after:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
h : ∀ a ∈ U, x (e a) = 0
x✝ : M'
⊢ (e.dualMap x ∘ₗ ↑e.symm) x✝ = x x✝

State before:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
e : M ≃ₗ[R] M'
U : Submodule R M
x : Module.Dual R M'
h : ∀ a ∈ U, x (e a) = 0
x✝ : M'
⊢ (e.dualMap x ∘ₗ ↑e.symm) x✝ = x x✝
Tactic:
simp
State after:
no goals