awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) x : K) ((g : (a : V₁) → K) x : K)
hx : Ne.{u_1 + 1} (α := K) ((f : (a : V₁) → K) x : K) (0 : K)
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
y : V₁
hy' : Eq.{u_1 + 1} (α := K) ((g : (a : V₁) → K) y : K) (0 : K)
hy : Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) y : K) (0 : K)
t : K
hz : t • x ∈ p
⊢ Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) (y + t • x) : K) ((g : (a : V₁) → K) (y + t • x) : K)

Tactic:
simp [h', hy, hy']
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
⊢ SeparatingLeft (R := K) (R₂ := K) (M := K) (M₁ := V →ₗ[K] K) id

Tactic:
separatingLeft_iff_ker_eq_bot.mpr ker_id

Premises used: Iff.mpr, LinearMap.ker_id, LinearMap.separatingLeft_iff_ker_eq_bot
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
⊢ SeparatingRight (M₂ := Dual K V) (Dual.eval K V)

Tactic:
id_separatingLeft

Premises used: LinearMap.SeparatingRight, LinearMap.id_separatingLeft
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
⊢ SeparatingRight (R := K) (R₂ := K) (M := K) (M₁ := V →ₗ[K] K) id

Tactic:
fun x => (forall_dual_apply_eq_zero_iff K x).mp

Premises used: Module.forall_dual_apply_eq_zero_iff, LinearMap.SeparatingRight, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
⊢ SeparatingLeft (M₂ := Dual K V) (Dual.eval K V)

Tactic:
id_separatingRight

Premises used: LinearMap.id_separatingRight, LinearMap.SeparatingLeft
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
⊢ Nondegenerate (R := K) (R₂ := K) (M := K) (M₁ := V →ₗ[K] K) id

Tactic:
⟨id_separatingLeft, id_separatingRight⟩

Premises used: LinearMap.id_separatingRight, LinearMap.id_separatingLeft, And.intro, LinearMap.Nondegenerate
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
⊢ Nondegenerate (M₂ := Dual K V) (Dual.eval K V)

Tactic:
⟨eval_separatingLeft, eval_separatingRight⟩

Premises used: LinearMap.eval_separatingLeft, LinearMap.eval_separatingRight, And.intro, LinearMap.Nondegenerate
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_3
V₁ : Type u_4
V₂ : Type u_5
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)
⊢ Function.Surjective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁)

Tactic:
fun φ ↦
  have ⟨f', hf'⟩ := f.exists_leftInverse_of_injective (ker_eq_bot.mpr hf)
  ⟨φ.comp f', ext fun x ↦ congr(φ <| $hf' x)⟩

Premises used: Iff.mpr, _private.0.LinearMap.dualMap_surjective_of_injective.match_1, LinearMap.ext, congrArg, LinearMap.ker_eq_bot, Exists, LinearMap.exists_leftInverse_of_injective, id, LinearMap.comp, Exists.intro, Eq, DFunLike.coe, LinearMap.dualMap, Function.Surjective
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_3
V₁ : Type u_4
V₂ : Type u_5
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ f.dualMap.range = f.ker.dualAnnihilator

Tactic:
range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective f <|
    dualMap_surjective_of_injective (range f).injective_subtype

Premises used: LinearMap.dualMap_surjective_of_injective, LinearMap.range, Submodule.injective_subtype, LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_3
V₁ : Type u_4
V₂ : Type u_5
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
rw : f.dualMap.range = ⊤ ↔ Function.Injective.{u_4 + 1, u_5 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)
rw₁ : f.ker.dualAnnihilator = ⊤ ↔ Function.Injective.{u_4 + 1, u_5 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)
rw₂ :
  f.ker.dualAnnihilator = dualAnnihilator ⊥ ↔
    Function.Injective.{u_4 + 1, u_5 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)
rw₃ : f.ker = ⊥ ↔ Function.Injective.{u_4 + 1, u_5 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)
rw₄ rw₅ :
  Function.Injective.{u_4 + 1, u_5 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂) ↔
    Function.Injective.{u_4 + 1, u_5 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)
⊢ Function.Surjective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁) ↔
    Function.Injective.{u_4 + 1, u_5 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)

Tactic:
rw [← LinearMap.range_eq_top, range_dualMap_eq_dualAnnihilator_ker,
      ← Submodule.dualAnnihilator_bot, Subspace.dualAnnihilator_inj, LinearMap.ker_eq_bot]

Premises used: LinearMap.ker_eq_bot, LinearMap.range_dualMap_eq_dualAnnihilator_ker, LinearMap.range_eq_top, Subspace.dualAnnihilator_inj, Submodule.dualAnnihilator_bot
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W : Subspace K V₁
h :
  ∀ (x : Dual K V₁) (x_1 : ↥W),
    Eq.{u_1 + 1} (α := K)
      ((((Submodule.dualPairing W ∘ₗ (dualAnnihilator W).mkQ : (a : Dual K V₁) → ↥W →ₗ[K] K) x :
              LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥W) K) :
            (a : ↥W) → K)
          x_1 :
        K)
      (((((↑W.quotAnnihilatorEquiv : Dual K V₁ ⧸ dualAnnihilator W →ₗ[K] Dual K ↥W) ∘ₗ (dualAnnihilator W).mkQ :
                  (a : Dual K V₁) → ↥W →ₗ[K] K)
                x :
              LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥W) K) :
            (a : ↥W) → K)
          x_1 :
        K)
⊢ Submodule.dualPairing W = (↑W.quotAnnihilatorEquiv : Dual K V₁ ⧸ dualAnnihilator W →ₗ[K] Dual K ↥W)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W : Subspace K V₁
x : Dual K V₁
x_1 : ↥W
⊢ Eq.{u_1 + 1} (α := K)
    ((((Submodule.dualPairing W ∘ₗ (dualAnnihilator W).mkQ : (a : Dual K V₁) → ↥W →ₗ[K] K) x :
            LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥W) K) :
          (a : ↥W) → K)
        x_1 :
      K)
    (((((↑W.quotAnnihilatorEquiv : Dual K V₁ ⧸ dualAnnihilator W →ₗ[K] Dual K ↥W) ∘ₗ (dualAnnihilator W).mkQ :
                (a : Dual K V₁) → ↥W →ₗ[K] K)
              x :
            LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥W) K) :
          (a : ↥W) → K)
        x_1 :
      K)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W : Subspace K V₁
left : (Submodule.dualPairing W).SeparatingLeft
right : (Submodule.dualPairing W).SeparatingRight
⊢ (Submodule.dualPairing W).Nondegenerate

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W : Subspace K V₁
left : (↑W.quotAnnihilatorEquiv : Dual K V₁ ⧸ dualAnnihilator W →ₗ[K] Dual K ↥W).ker = ⊥
⊢ (Submodule.dualPairing W).SeparatingLeft

Tactic:
rw [LinearMap.separatingLeft_iff_ker_eq_bot, dualPairing_eq]

Premises used: LinearMap.separatingLeft_iff_ker_eq_bot, Subspace.dualPairing_eq
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W : Subspace K V₁
⊢ (↑W.quotAnnihilatorEquiv : Dual K V₁ ⧸ dualAnnihilator W →ₗ[K] Dual K ↥W).ker = ⊥

Tactic:
apply LinearEquiv.ker

Premises used: LinearEquiv.ker
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W : Subspace K V₁
x : ↥W
h :
  ∀ (x_1 : Dual K V₁ ⧸ dualAnnihilator W),
    Eq.{u_1 + 1} (α := K)
      ((((Submodule.dualPairing W : (a : Dual K V₁ ⧸ dualAnnihilator W) → ↥W →ₗ[K] K) x_1 :
              LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥W) K) :
            (a : ↥W) → K)
          x :
        K)
      (0 : K)
right : ∀ (φ : Dual.{u_1, u_2} K ↥W), Eq.{u_1 + 1} (α := K) ((φ : (a : ↥W) → K) x : K) (0 : K)
⊢ x = 0

Tactic:
rw [← forall_dual_apply_eq_zero_iff K x]

Premises used: Module.forall_dual_apply_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W : Subspace K V₁
x : ↥W
h :
  ∀ (x_1 : Dual K V₁ ⧸ dualAnnihilator W),
    Eq.{u_1 + 1} (α := K)
      ((((Submodule.dualPairing W : (a : Dual K V₁ ⧸ dualAnnihilator W) → ↥W →ₗ[K] K) x_1 :
              LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥W) K) :
            (a : ↥W) → K)
          x :
        K)
      (0 : K)
φ : Dual.{u_1, u_2} K ↥W
⊢ Eq.{u_1 + 1} (α := K) ((φ : (a : ↥W) → K) x : K) (0 : K)

Tactic:
simpa only [Submodule.dualPairing_apply, dualLift_of_subtype] using
      h (Submodule.Quotient.mk (W.dualLift φ))

Premises used: Subspace.dualLift_of_subtype, Submodule.dualPairing_apply, Submodule.Quotient.mk, Subspace.dualLift, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W : Subspace K V₁
left : (dualCopairing W).SeparatingLeft
right : (dualCopairing W).SeparatingRight
⊢ (dualCopairing W).Nondegenerate

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W : Subspace K V₁
left : (↑(dualQuotEquivDualAnnihilator W).symm : ↥(dualAnnihilator W) →ₗ[K] Dual K (V₁ ⧸ W)).ker = ⊥
⊢ (dualCopairing W).SeparatingLeft

Tactic:
rw [LinearMap.separatingLeft_iff_ker_eq_bot, dualCopairing_eq]

Premises used: Submodule.dualCopairing_eq, LinearMap.separatingLeft_iff_ker_eq_bot
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W : Subspace K V₁
⊢ (↑(dualQuotEquivDualAnnihilator W).symm : ↥(dualAnnihilator W) →ₗ[K] Dual K (V₁ ⧸ W)).ker = ⊥

Tactic:
apply LinearEquiv.ker

Premises used: LinearEquiv.ker
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W : Subspace K V₁
y : V₁ ⧸ W
x : V₁
right : (∀ (x_1 : ↥(dualAnnihilator W)), Eq.{u_1 + 1} (α := K) ((x_1 : (a : V₁) → K) x : K) (0 : K)) → x ∈ W
⊢ (∀ (x_1 : ↥(dualAnnihilator W)),
      Eq.{u_1 + 1} (α := K)
        ((((dualCopairing W : (a : ↥(dualAnnihilator W)) → V₁ ⧸ W →ₗ[K] K) x_1 :
                LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (V₁ ⧸ W) K) :
              (a : V₁ ⧸ W) → K)
            (Quot.mk (⇑(quotientRel W) : V₁ → V₁ → Prop) x) :
          K)
        (0 : K)) →
    Eq (α := V₁ ⧸ W) (Quot.mk (⇑(quotientRel W) : V₁ → V₁ → Prop) x) 0

Tactic:
simp only [Quotient.quot_mk_eq_mk, dualCopairing_apply, Quotient.mk_eq_zero]

Premises used: Submodule.dualCopairing_apply, Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W : Subspace K V₁
y : V₁ ⧸ W
x : V₁
right :
  (∀ (x_1 : Dual K V₁) (h : x_1 ∈ dualAnnihilator W),
      Eq.{u_1 + 1} (α := K) ((Subtype.mk (p := fun (x : Dual K V₁) ↦ x ∈ dualAnnihilator W) x_1 h : (a : V₁) → K) x : K)
        (0 : K)) →
    ∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V₁) → K) x : K) (0 : K)
⊢ (∀ (x_1 : ↥(dualAnnihilator W)), Eq.{u_1 + 1} (α := K) ((x_1 : (a : V₁) → K) x : K) (0 : K)) → x ∈ W

Tactic:
rw [← forall_mem_dualAnnihilator_apply_eq_zero_iff, SetLike.forall]

Premises used: Subspace.forall_mem_dualAnnihilator_apply_eq_zero_iff, SetLike.forall
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W : Subspace K V₁
y : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : Dual K V₁) (h : x_1 ∈ dualAnnihilator W),
      Eq.{u_1 + 1} (α := K) ((Subtype.mk (p := fun (x : Dual K V₁) ↦ x ∈ dualAnnihilator W) x_1 h : (a : V₁) → K) x : K)
        (0 : K)) →
    ∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V₁) → K) x : K) (0 : K)

Tactic:
id

Premises used: Set.Mem, id
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W : Subspace K V₁
y : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : Dual K V₁) (h : x_1 ∈ dualAnnihilator W),
      Eq.{u_1 + 1} (α := K) ((Subtype.mk (p := fun (x : Dual K V₁) ↦ x ∈ dualAnnihilator W) x_1 h : (a : V₁) → K) x : K)
        (0 : K)) →
    ∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V₁) → K) x : K) (0 : K)

Tactic:
exact id

Premises used: id
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W W' : Subspace K V₁
⊢ dualAnnihilator (W ⊓ W') = dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
le_antisymm ?_ (sup_dualAnnihilator_le_inf W W')

Premises used: le_antisymm, Submodule.sup_dualAnnihilator_le_inf
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W W' : Subspace K V₁
refine : dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
⊢ dualAnnihilator (W ⊓ W') = dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
refine le_antisymm ?_ (sup_dualAnnihilator_le_inf W W')

Premises used: le_antisymm, Submodule.sup_dualAnnihilator_le_inf
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
⊢ F.ker = W ⊓ W'

Tactic:
simp only [F, LinearMap.ker_prod, ker_mkQ]

Premises used: LinearMap.ker_prod, Submodule.ker_mkQ
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
⊢ F.ker = W ⊓ W'

Tactic:
have : LinearMap.ker F = W ⊓ W' := by simp only [F, LinearMap.ker_prod, ker_mkQ]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
rw : F.dualMap.range ≤ dualAnnihilator W ⊔ dualAnnihilator W'
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
rw [← this, ← LinearMap.range_dualMap_eq_dualAnnihilator_ker]

Premises used: LinearMap.range_dualMap_eq_dualAnnihilator_ker
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
x : Dual.{u_1, u_2} K ((V₁ ⧸ W) × V₁ ⧸ W')
rw :
  ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W', y + z = (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁) x
⊢ Membership.mem (α := Dual K V₁) (dualAnnihilator W ⊔ dualAnnihilator W')
    ((F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁) x : Dual K V₁)

Tactic:
rw [Submodule.mem_sup]

Premises used: Submodule.mem_sup
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
x : Dual.{u_1, u_2} K ((V₁ ⧸ W) × V₁ ⧸ W')
obtain :
  ∀ (a : Dual.{u_1, u_2} K (V₁ ⧸ W)) (b : Dual.{u_1, u_2} K (V₁ ⧸ W')),
    ∃ y ∈ dualAnnihilator W,
      ∃ z ∈ dualAnnihilator W',
        y + z =
          (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
            ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
                (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
              (a, b))
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W', y + z = (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁) x

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

Premises used: Module.dualProdDualEquivDual, LinearEquiv.surjective, HasQuotient.Quotient, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
a : Dual.{u_1, u_2} K (V₁ ⧸ W)
b : Dual.{u_1, u_2} K (V₁ ⧸ W')
obtain :
  ∀ (a' : ↥(dualAnnihilator W)),
    ∃ y ∈ dualAnnihilator W,
      ∃ z ∈ dualAnnihilator W',
        y + z =
          (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
            ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
                (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
              (((dualQuotEquivDualAnnihilator W).symm : (a : ↥(dualAnnihilator W)) → Dual K (V₁ ⧸ W)) a', b))
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W',
      y + z =
        (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
          ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
              (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
            (a, b))

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

Premises used: LinearEquiv.symm, LinearEquiv.surjective, Submodule.dualQuotEquivDualAnnihilator, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
b : Dual.{u_1, u_2} K (V₁ ⧸ W')
a' : ↥(dualAnnihilator W)
obtain :
  ∀ (b' : ↥(dualAnnihilator W')),
    ∃ y ∈ dualAnnihilator W,
      ∃ z ∈ dualAnnihilator W',
        y + z =
          (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
            ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
                (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
              (((dualQuotEquivDualAnnihilator W).symm : (a : ↥(dualAnnihilator W)) → Dual K (V₁ ⧸ W)) a',
                ((dualQuotEquivDualAnnihilator W').symm : (a : ↥(dualAnnihilator W')) → Dual K (V₁ ⧸ W')) b'))
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W',
      y + z =
        (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
          ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
              (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
            (((dualQuotEquivDualAnnihilator W).symm : (a : ↥(dualAnnihilator W)) → Dual K (V₁ ⧸ W)) a', b))

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

Premises used: LinearEquiv.symm, LinearEquiv.surjective, Submodule.dualQuotEquivDualAnnihilator, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
a' : ↥(dualAnnihilator W)
b' : ↥(dualAnnihilator W')
right :
  (↑a' : Dual K V₁) + (↑b' : Dual K V₁) =
    (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
      ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
          (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
        (((dualQuotEquivDualAnnihilator W).symm : (a : ↥(dualAnnihilator W)) → Dual K (V₁ ⧸ W)) a',
          ((dualQuotEquivDualAnnihilator W').symm : (a : ↥(dualAnnihilator W')) → Dual K (V₁ ⧸ W')) b'))
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W',
      y + z =
        (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
          ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
              (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
            (((dualQuotEquivDualAnnihilator W).symm : (a : ↥(dualAnnihilator W)) → Dual K (V₁ ⧸ W)) a',
              ((dualQuotEquivDualAnnihilator W').symm : (a : ↥(dualAnnihilator W')) → Dual K (V₁ ⧸ W')) b'))

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

Premises used: Subtype.property
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
a' : ↥(dualAnnihilator W)
b' : ↥(dualAnnihilator W')
⊢ (↑a' : Dual K V₁) + (↑b' : Dual K V₁) =
    (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
      ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
          (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
        (((dualQuotEquivDualAnnihilator W).symm : (a : ↥(dualAnnihilator W)) → Dual K (V₁ ⧸ W)) a',
          ((dualQuotEquivDualAnnihilator W').symm : (a : ↥(dualAnnihilator W')) → Dual K (V₁ ⧸ W')) b'))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
ι : Type u_4
inst_3 : Finite ι
W : ι → Subspace K V₁
revert :
  ∀ {ι : Type u_4} [Finite ι] (W : ι → Subspace K V₁),
    Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : ι), W i)) (⨆ (i : ι), dualAnnihilator (W i))
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : ι), W i)) (⨆ (i : ι), dualAnnihilator (W i))

Tactic:
revert ι
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
of_equiv :
  ∀ {α β : Type u_4} (a : α ≃ β),
    (∀ (W : α → Subspace K V₁),
        Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : α), W i)) (⨆ (i : α), dualAnnihilator (W i))) →
      ∀ (W : β → Subspace K V₁),
        Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : β), W i)) (⨆ (i : β), dualAnnihilator (W i))
h_empty :
  ∀ (W : PEmpty.{u_4 + 1} → Subspace K V₁),
    Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : PEmpty.{u_4 + 1}), W i))
      (⨆ (i : PEmpty.{u_4 + 1}), dualAnnihilator (W i))
h_option :
  ∀ {α : Type u_4} [Fintype α],
    (∀ (W : α → Subspace K V₁),
        Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : α), W i)) (⨆ (i : α), dualAnnihilator (W i))) →
      ∀ (W : Option α → Subspace K V₁),
        Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : Option α), W i))
          (⨆ (i : Option α), dualAnnihilator (W i))
⊢ ∀ {ι : Type u_4} [Finite ι] (W : ι → Subspace K V₁),
    Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : ι), W i)) (⨆ (i : ι), dualAnnihilator (W i))

Tactic:
apply Finite.induction_empty_option

Premises used: Finite.induction_empty_option