awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V₁ : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst_3 : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
this : finrank.{u_1, u_2} K ↥(LinearMap.ker f ⊔ p) = finrank.{u_1, u_2} K ↥(LinearMap.ker f) + finrank.{u_1, u_2} K ↥p
rwa : finrank K V₁ ≤ finrank.{u_1, u_2} K ↥(LinearMap.ker f ⊔ p)
rwa₁ : finrank K V₁ ≤ finrank.{u_1, u_2} K ↥(LinearMap.ker f) + finrank.{u_1, u_2} K ↥p
rwa₂ : finrank.{u_1, u_2} K ↥(LinearMap.ker f) + 1 ≤ finrank.{u_1, u_2} K ↥(LinearMap.ker f) + finrank.{u_1, u_2} K ↥p
⊢ finrank.{u_1, u_2} K ↥⊤ ≤ finrank.{u_1, u_2} K ↥(LinearMap.ker f ⊔ p)
have rwa₃ : 1 ≤ finrank.{u_1, u_2} K ↥p
Tactic: rwa [finrank_top, this, ← finrank_ker_add_one_of_ne_zero hf, add_le_add_iff_left,
    Submodule.one_le_finrank_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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
⊢ f = g
have hp : p ≠ ⊥
Tactic: have hp : p ≠ ⊥ := by aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 ≠ ⊥
⊢ Disjoint (LinearMap.ker f) p
have rw : ∀ x ∈ LinearMap.ker f ⊓ p, x = 0
Tactic: rw [disjoint_iff, Submodule.eq_bot_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 ≠ ⊥
y : V₁
hfy : Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) y : K) (0 : K)
hpy : y ∈ p
⊢ y = 0
have obtain : ∀ (t : K) (hfy : Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) (t • x) : K) (0 : K)) (hpy : t • x ∈ p), t • x = 0
Tactic: obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hpy
Cleared hypotheses: y, hfy, hpy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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 ≠ ⊥
t : K
hfy : Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) (t • x) : K) (0 : K)
hpy : t • x ∈ p
⊢ t • x = 0
have ht : t = 0
Tactic: have ht : t = 0 := by simpa [hx] using hfy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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 ≠ ⊥
⊢ f = g
have hpf : Disjoint (LinearMap.ker f) p
Tactic: have hpf : Disjoint (LinearMap.ker f) p := by
    rw [disjoint_iff, Submodule.eq_bot_iff]
    rintro y ⟨hfy : f y = 0, hpy : y ∈ p⟩
    obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hpy
    have ht : t = 0 := by simpa [hx] using hfy
    simp [ht]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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
⊢ f = g
have hf : f ≠ 0
Tactic: have hf : f ≠ 0 := by aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ f = g
have h₁ : ∀ (v : V₁), Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) v : K) ((g : (a : V₁) → K) v : K)
Tactic: ext v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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
v : V₁
⊢ ∃ y ∈ LinearMap.ker f, ∃ z ∈ p, y + z = v
have this : Membership.mem (γ := Submodule K V₁) ⊤ v
Tactic: have : v ∈ (⊤ : Submodule K V₁) := Submodule.mem_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
v : V₁
this : Membership.mem (γ := Submodule K V₁) ⊤ v
⊢ ∃ y ∈ LinearMap.ker f, ∃ z ∈ p, y + z = v
have rwa : ∀ (this : v ∈ LinearMap.ker f ⊔ p), ∃ y ∈ LinearMap.ker f, ∃ z ∈ p, y + z = v
Tactic: rwa [← (isCompl_ker_of_disjoint_of_ne_bot hf hpf hp).sup_eq_top, Submodule.mem_sup] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
v : V₁
this : Membership.mem (γ := Submodule K V₁) ⊤ v
rwa : ∀ (this : v ∈ LinearMap.ker f ⊔ p), ∃ y ∈ LinearMap.ker f, ∃ z ∈ p, y + z = v
⊢ ∃ y ∈ LinearMap.ker f, ∃ z ∈ p, y + z = v
have rwa₁ : ∀ (this : ∃ y ∈ LinearMap.ker f, ∃ z ∈ p, y + z = v), ∃ y ∈ LinearMap.ker f, ∃ z ∈ p, y + z = v
Tactic: rwa [← (isCompl_ker_of_disjoint_of_ne_bot hf hpf hp).sup_eq_top, Submodule.mem_sup] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
v : V₁
⊢ Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) v : K) ((g : (a : V₁) → K) v : K)
have h₁ : ∀ (y : V₁) (hy : y ∈ LinearMap.ker f) (z : V₁) (hz : z ∈ p),
  Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) (y + z) : K) ((g : (a : V₁) → K) (y + z) : K)
Tactic: obtain ⟨y, hy, z, hz, rfl⟩ : ∃ᵉ (y ∈ LinearMap.ker f) (z ∈ p), y + z = v := by
    have : v ∈ (⊤ : Submodule K V₁) := Submodule.mem_top
    rwa [← (isCompl_ker_of_disjoint_of_ne_bot hf hpf hp).sup_eq_top, Submodule.mem_sup] at this
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 : y ∈ LinearMap.ker f
z : V₁
hz : z ∈ p
⊢ Eq.{u_1 + 1} (α := K) ((g : (a : V₁) → K) y : K) (0 : K)
have rwa : y ∈ LinearMap.ker g
Tactic: rwa [← LinearMap.mem_ker, ← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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 : y ∈ LinearMap.ker f
z : V₁
hz : z ∈ p
⊢ Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) (y + z) : K) ((g : (a : V₁) → K) (y + z) : K)
have hy' : Eq.{u_1 + 1} (α := K) ((g : (a : V₁) → K) y : K) (0 : K)
Tactic: have hy' : g y = 0 := by rwa [← LinearMap.mem_ker, ← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 : y ∈ LinearMap.ker f
z : V₁
hz : z ∈ p
hy' : Eq.{u_1 + 1} (α := K) ((g : (a : V₁) → K) y : K) (0 : K)
⊢ Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) y : K) (0 : K)
have rwa : ∀ (hy : Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) y : K) (0 : K)) (z : V₁) (hz : z ∈ p)
  (hy' : Eq.{u_1 + 1} (α := K) ((g : (a : V₁) → K) y : K) (0 : K)),
  Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) y : K) (0 : K)
Tactic: rwa [LinearMap.mem_ker] at hy
Cleared hypotheses: hy, z, hz, hy'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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 : y ∈ LinearMap.ker f
z : V₁
hz : z ∈ p
hy' : Eq.{u_1 + 1} (α := K) ((g : (a : V₁) → K) y : K) (0 : K)
⊢ Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) (y + z) : K) ((g : (a : V₁) → K) (y + z) : K)
have hy₁ : Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) y : K) (0 : K)
Tactic: replace hy : f y = 0 := by rwa [LinearMap.mem_ker] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 z : V₁
hz : z ∈ p
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)
⊢ Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) (y + z) : K) ((g : (a : V₁) → K) (y + z) : K)
have h₁ : ∀ (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: obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₂
⊢ 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₂)
have rw : f.dualMap.range = ⊤ ↔ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₂)
⊢ 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₂)
have rw₁ : f.ker.dualAnnihilator = ⊤ ↔ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₂)
⊢ 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₂)
have rw₂ : f.ker.dualAnnihilator = dualAnnihilator ⊥ ↔
  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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₂)
⊢ 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₂)
have rw₃ : f.ker = ⊥ ↔ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₂)
⊢ 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₂)
have 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₂)
Tactic: rw [← LinearMap.range_eq_top, range_dualMap_eq_dualAnnihilator_ker,
      ← Submodule.dualAnnihilator_bot, Subspace.dualAnnihilator_inj, LinearMap.ker_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₁
⊢ Submodule.dualPairing W = (↑W.quotAnnihilatorEquiv : Dual K V₁ ⧸ dualAnnihilator W →ₗ[K] Dual K ↥W)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₁
⊢ (Submodule.dualPairing W).Nondegenerate
have left : (Submodule.dualPairing W).SeparatingLeft
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ (Submodule.dualPairing W).Nondegenerate
have right : (Submodule.dualPairing W).SeparatingRight
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₁
⊢ (Submodule.dualPairing W).SeparatingLeft
have left : (↑W.quotAnnihilatorEquiv : Dual K V₁ ⧸ dualAnnihilator W →ₗ[K] Dual K ↥W).ker = ⊥
Tactic: rw [LinearMap.separatingLeft_iff_ker_eq_bot, dualPairing_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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)
⊢ x = 0
have right : ∀ (φ : Dual.{u_1, u_2} K ↥W), Eq.{u_1 + 1} (α := K) ((φ : (a : ↥W) → K) x : K) (0 : K)
Tactic: rw [← forall_dual_apply_eq_zero_iff K x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₁
⊢ (dualCopairing W).Nondegenerate
have left : (dualCopairing W).SeparatingLeft
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ (dualCopairing W).Nondegenerate
have right : (dualCopairing W).SeparatingRight
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₁
⊢ (dualCopairing W).SeparatingLeft
have left : (↑(dualQuotEquivDualAnnihilator W).symm : ↥(dualAnnihilator W) →ₗ[K] Dual K (V₁ ⧸ W)).ker = ⊥
Tactic: rw [LinearMap.separatingLeft_iff_ker_eq_bot, dualCopairing_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 : ↥(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
have right : (∀ (x_1 : ↥(dualAnnihilator W)), Eq.{u_1 + 1} (α := K) ((x_1 : (a : V₁) → K) x : K) (0 : K)) → x ∈ W
Tactic: simp only [Quotient.quot_mk_eq_mk, dualCopairing_apply, Quotient.mk_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 : ↥(dualAnnihilator W)), Eq.{u_1 + 1} (α := K) ((x_1 : (a : V₁) → K) x : K) (0 : K)) → x ∈ W
have 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)
Tactic: rw [← forall_mem_dualAnnihilator_apply_eq_zero_iff, SetLike.forall]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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'
have refine : dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
Tactic: refine le_antisymm ?_ (sup_dualAnnihilator_le_inf W W')
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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')
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
have this : F.ker = W ⊓ W'
Tactic: have : LinearMap.ker F = W ⊓ W' := by simp only [F, LinearMap.ker_prod, ker_mkQ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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'
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
have rw : F.dualMap.range ≤ dualAnnihilator W ⊔ dualAnnihilator W'
Tactic: rw [← this, ← LinearMap.range_dualMap_eq_dualAnnihilator_ker]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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')
⊢ 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₁)
have rw : ∃ y ∈ dualAnnihilator W, ∃ z ∈ dualAnnihilator W', y + z = (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁) x
Tactic: rw [Submodule.mem_sup]