-- Mathlib/LinearAlgebra/Dual.lean
theorem dualAnnihilator_inf_eq (W W' : Subspace K V₁) :
    (W ⊓ W').dualAnnihilator = W.dualAnnihilator ⊔ W'.dualAnnihilator

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
have : LinearMap.ker F = W ⊓ W' := by simp only [F, LinearMap.ker_prod, ker_mkQ]

Result:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
φ : Dual K V₁
⊢ φ ∈ LinearMap.range F.dualMap → φ ∈ dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
rw [LinearMap.mem_range]

Result:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
φ : Dual K V₁
⊢ (∃ y, F.dualMap y = φ) → φ ∈ dualAnnihilator W ⊔ dualAnnihilator W'

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
φ : Dual K V₁
⊢ (∃ y, F.dualMap y = φ) → φ ∈ dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
rintro ⟨x, rfl⟩

Result:
case intro
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
x : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')
⊢ F.dualMap x ∈ dualAnnihilator W ⊔ dualAnnihilator W'

Proof state:
case right
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a' : ↥(dualAnnihilator W)
b' : ↥(dualAnnihilator W')
⊢ ↑a' + ↑b' =
    F.dualMap
      ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W'))
        ((dualQuotEquivDualAnnihilator W).symm a', (dualQuotEquivDualAnnihilator W').symm b'))

Tactic:
rfl

Result:
no goals

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
let F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (Submodule.mkQ W).prod (Submodule.mkQ W')

Result:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'

Proof state:
case intro.intro.mk
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a : Dual K (V₁ ⧸ W)
b : Dual K (V₁ ⧸ W')
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W', y + z = F.dualMap ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')) (a, b))

Tactic:
obtain ⟨a', rfl⟩ := (dualQuotEquivDualAnnihilator W).symm.surjective a

Result:
case intro.intro.mk.intro
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
b : Dual K (V₁ ⧸ W')
a' : ↥(dualAnnihilator W)
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W',
      y + z = F.dualMap ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')) ((dualQuotEquivDualAnnihilator W).symm a', b))

Proof state:
case intro.intro.mk.intro
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
b : Dual K (V₁ ⧸ W')
a' : ↥(dualAnnihilator W)
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W',
      y + z = F.dualMap ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')) ((dualQuotEquivDualAnnihilator W).symm a', b))

Tactic:
obtain ⟨b', rfl⟩ := (dualQuotEquivDualAnnihilator W').symm.surjective b

Result:
case intro.intro.mk.intro.intro
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a' : ↥(dualAnnihilator W)
b' : ↥(dualAnnihilator W')
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W',
      y + z =
        F.dualMap
          ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W'))
            ((dualQuotEquivDualAnnihilator W).symm a', (dualQuotEquivDualAnnihilator W').symm b'))

Proof state:
case intro
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
x : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')
⊢ F.dualMap x ∈ dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
rw [Submodule.mem_sup]

Result:
case intro
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
x : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')
⊢ ∃ y ∈ dualAnnihilator W, ∃ z ∈ dualAnnihilator W', y + z = F.dualMap x

Proof state:
case intro.intro.mk.intro.intro
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a' : ↥(dualAnnihilator W)
b' : ↥(dualAnnihilator W')
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W',
      y + z =
        F.dualMap
          ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W'))
            ((dualQuotEquivDualAnnihilator W).symm a', (dualQuotEquivDualAnnihilator W').symm b'))

Tactic:
use a', a'.property, b', b'.property

Result:
case right
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a' : ↥(dualAnnihilator W)
b' : ↥(dualAnnihilator W')
⊢ ↑a' + ↑b' =
    F.dualMap
      ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W'))
        ((dualQuotEquivDualAnnihilator W).symm a', (dualQuotEquivDualAnnihilator W').symm b'))

Proof state:
case intro
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
x : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')
⊢ ∃ y ∈ dualAnnihilator W, ∃ z ∈ dualAnnihilator W', y + z = F.dualMap x

Tactic:
obtain ⟨⟨a, b⟩, rfl⟩ := (dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')).surjective x

Result:
case intro.intro.mk
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a : Dual K (V₁ ⧸ W)
b : Dual K (V₁ ⧸ W')
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W', y + z = F.dualMap ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')) (a, b))