awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf :
  Function.Surjective (α := Dual R M') (β := Dual.{u_1, u_3} R ↥f.range)
    (⇑f.range.subtype.dualMap : (a : Dual R M') → Dual R ↥f.range)
rr_surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
this :
  range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict) =
    (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator
⊢ (f.range.subtype ∘ₗ f.rangeRestrict).dualMap.range = range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict)

Tactic:
?_
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf :
  Function.Surjective (α := Dual R M') (β := Dual.{u_1, u_3} R ↥f.range)
    (⇑f.range.subtype.dualMap : (a : Dual R M') → Dual R ↥f.range)
rr_surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
this :
  range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict) =
    (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator
h :
  (f.range.subtype ∘ₗ f.rangeRestrict).dualMap.range = range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict)
⊢ f.dualMap.range = range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict)

Tactic:
calc
      _ = range ((range f).subtype.comp f.rangeRestrict).dualMap := by simp
      _ = _ := ?_

Premises used: LinearMap.range, LinearMap.rangeRestrict, LinearMap.comp, Submodule.subtype, LinearMap.dualMap
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf :
  Function.Surjective (α := Dual R M') (β := Dual.{u_1, u_3} R ↥f.range)
    (⇑f.range.subtype.dualMap : (a : Dual R M') → Dual R ↥f.range)
rr_surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
this :
  range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict) =
    (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator
h : f.range.subtype.dualMap.range = ⊤
⊢ (f.range.subtype ∘ₗ f.rangeRestrict).dualMap.range = range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict)

Tactic:
rw [← dualMap_comp_dualMap, range_comp_of_range_eq_top]

Premises used: LinearMap.range_comp_of_range_eq_top, LinearMap.dualMap_comp_dualMap
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf :
  Function.Surjective (α := Dual R M') (β := Dual.{u_1, u_3} R ↥f.range)
    (⇑f.range.subtype.dualMap : (a : Dual R M') → Dual R ↥f.range)
rr_surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
this :
  range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict) =
    (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator
h h₁ h₂ h₃ :
  Function.Surjective (α := Dual R M') (β := Dual.{u_1, u_3} R ↥f.range)
    (⇑f.range.subtype.dualMap : (a : Dual R M') → Dual R ↥f.range)
⊢ f.range.subtype.dualMap.range = ⊤

Tactic:
rwa [range_eq_top]

Premises used: LinearMap.range_eq_top
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf :
  Function.Surjective (α := Dual R M') (β := Dual.{u_1, u_3} R ↥f.range)
    (⇑f.range.subtype.dualMap : (a : Dual R M') → Dual R ↥f.range)
rr_surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
this :
  range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict) =
    (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator
h : f.ker = ker (M₂ := ↥f.range) f.rangeRestrict
⊢ f.ker.dualAnnihilator = (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf :
  Function.Surjective (α := Dual R M') (β := Dual.{u_1, u_3} R ↥f.range)
    (⇑f.range.subtype.dualMap : (a : Dual R M') → Dual R ↥f.range)
rr_surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
this :
  range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict) =
    (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator
⊢ f.ker = ker (M₂ := ↥f.range) f.rangeRestrict

Tactic:
(ker_rangeRestrict f).symm

Premises used: LinearMap.ker_rangeRestrict, Eq.symm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf :
  Function.Surjective (α := Dual R M') (β := Dual.{u_1, u_3} R ↥f.range)
    (⇑f.range.subtype.dualMap : (a : Dual R M') → Dual R ↥f.range)
rr_surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
this :
  range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict) =
    (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator
⊢ f.ker = ker (M₂ := ↥f.range) f.rangeRestrict

Tactic:
exact (ker_rangeRestrict f).symm

Premises used: LinearMap.ker_rangeRestrict, Eq.symm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_4
V₁ : Type u_5
inst : DivisionSemiring K
inst_1 : AddCommMonoid V₁
inst_2 : Module K V₁
f : Dual K V₁
hf : f ≠ 0
⊢ LinearMap.range f = ⊤

Tactic:
LinearMap.range_eq_top.mpr (LinearMap.surjective hf)

Premises used: Iff.mpr, LinearMap.range_eq_top, LinearMap.surjective
-- 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₁
f : Dual K V₁
hf : f ≠ 0
inst_3 : FiniteDimensional K V₁
this : finrank K ↥(LinearMap.range f) = 1
rw :
  finrank.{u_1, u_2} K ↥(LinearMap.ker f) + 1 =
    finrank.{u_1, u_2} K (V₁ ⧸ LinearMap.ker f) + finrank.{u_1, u_2} K ↥(LinearMap.ker f)
rw₁ :
  1 + finrank.{u_1, u_2} K ↥(LinearMap.ker f) =
    finrank.{u_1, u_2} K (V₁ ⧸ LinearMap.ker f) + finrank.{u_1, u_2} K ↥(LinearMap.ker f)
rw₂ : 1 = finrank.{u_1, u_2} K (V₁ ⧸ LinearMap.ker f)
rw₃ : 1 = finrank K ↥(LinearMap.range f)
rw₄ rw₅ : Eq (α := ℕ) 1 1
⊢ finrank.{u_1, u_2} K ↥(LinearMap.ker f) + 1 = finrank K V₁

Tactic:
rw [← (LinearMap.ker f).finrank_quotient_add_finrank, add_comm, add_left_inj,
    f.quotKerEquivRange.finrank_eq, this]

Premises used: Submodule.finrank_quotient_add_finrank, LinearMap.ker, LinearEquiv.finrank_eq, add_left_inj, add_comm, LinearMap.quotKerEquivRange
-- 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₁
f : Dual K V₁
hf : f ≠ 0
inst_3 : FiniteDimensional K V₁
suffices : finrank K ↥(LinearMap.range f) = 1
⊢ finrank.{u_1, u_2} K ↥(LinearMap.ker f) + 1 = finrank K V₁

Tactic:
suffices finrank K (LinearMap.range f) = 1 by
    rw [← (LinearMap.ker f).finrank_quotient_add_finrank, add_comm, add_left_inj,
    f.quotKerEquivRange.finrank_eq, this]
-- 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₁
f : Dual K V₁
hf : f ≠ 0
inst_3 : FiniteDimensional K V₁
rw : finrank K ↥⊤ = 1
rw₁ : finrank K K = 1
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ finrank K ↥(LinearMap.range f) = 1

Tactic:
rw [range_eq_top_of_ne_zero hf, finrank_top, finrank_self]

Premises used: finrank_top, Module.finrank_self, Module.Dual.range_eq_top_of_ne_zero
-- 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₁
f : Dual K V₁
hf : f ≠ 0
inst_3 : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
⊢ IsCompl (LinearMap.ker f) p

Tactic:
⟨hpf, codisjoint_iff.mpr <| eq_of_le_of_finrank_le le_top ?_⟩

Premises used: Iff.mpr, Submodule.eq_of_le_of_finrank_le, codisjoint_iff, le_top, IsCompl.mk
-- 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₁
f : Dual K V₁
hf : f ≠ 0
inst_3 : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
refine : finrank.{u_1, u_2} K ↥⊤ ≤ finrank.{u_1, u_2} K ↥(LinearMap.ker f ⊔ p)
⊢ IsCompl (LinearMap.ker f) p

Tactic:
refine ⟨hpf, codisjoint_iff.mpr <| eq_of_le_of_finrank_le le_top ?_⟩
-- 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₁
f : Dual K V₁
hf : f ≠ 0
inst_3 : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
⊢ 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

Tactic:
simp [← Submodule.finrank_sup_add_finrank_inf_eq (LinearMap.ker f) p, hpf.eq_bot]

Premises used: Submodule.finrank_sup_add_finrank_inf_eq, LinearMap.ker, Disjoint.eq_bot
-- 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₁
f : Dual K V₁
hf : f ≠ 0
inst_3 : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
⊢ 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

Tactic:
have : finrank K ↑(LinearMap.ker f ⊔ p) = finrank K (LinearMap.ker f) + finrank K p := by
    simp [← Submodule.finrank_sup_add_finrank_inf_eq (LinearMap.ker f) p, hpf.eq_bot]
-- 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₁
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
rwa₃ : 1 ≤ finrank.{u_1, u_2} K ↥p
rwa₄ rwa₅ rwa₆ rwa₇ : p ≠ ⊥
⊢ finrank.{u_1, u_2} K ↥⊤ ≤ finrank.{u_1, u_2} K ↥(LinearMap.ker f ⊔ p)

Tactic:
rwa [finrank_top, this, ← finrank_ker_add_one_of_ne_zero hf, add_le_add_iff_left,
    Submodule.one_le_finrank_iff]

Premises used: add_le_add_iff_left, Submodule.one_le_finrank_iff, finrank_top, Module.Dual.finrank_ker_add_one_of_ne_zero
-- 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
⊢ p ≠ ⊥

Tactic:
aesop
-- 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
⊢ p ≠ ⊥

Tactic:
have hp : p ≠ ⊥ := by aesop
-- 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 ≠ ⊥
rw : ∀ x ∈ LinearMap.ker f ⊓ p, x = 0
⊢ Disjoint (LinearMap.ker f) p

Tactic:
rw [disjoint_iff, Submodule.eq_bot_iff]

Premises used: disjoint_iff, Submodule.eq_bot_iff
-- 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 ≠ ⊥
y : V₁
hfy : Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) y : K) (0 : K)
hpy : y ∈ p
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
⊢ y = 0

Tactic:
obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hpy

Premises used: Submodule.mem_span_singleton, Iff.mp, rfl
-- 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 ≠ ⊥
t : K
hfy : Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) (t • x) : K) (0 : K)
hpy : t • x ∈ p
⊢ t = 0

Tactic:
simpa [hx] using hfy
-- 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 ≠ ⊥
t : K
hfy : Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) (t • x) : K) (0 : K)
hpy : t • x ∈ p
⊢ t = 0

Tactic:
have ht : t = 0 := by simpa [hx] using hfy
-- 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 ≠ ⊥
t : K
hfy : Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) (t • x) : K) (0 : K)
hpy : t • x ∈ p
ht : t = 0
⊢ t • x = 0

Tactic:
simp [ht]
-- 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 ≠ ⊥
⊢ 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]
-- 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
⊢ f ≠ 0

Tactic:
aesop
-- 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
⊢ f ≠ 0

Tactic:
have hf : f ≠ 0 := by aesop
-- 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
h₁ : ∀ (v : V₁), Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) v : K) ((g : (a : V₁) → K) v : K)
⊢ f = g

Tactic:
ext v
-- 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
v : V₁
⊢ Membership.mem (γ := Submodule K V₁) ⊤ v

Tactic:
have : v ∈ (⊤ : Submodule K V₁) := Submodule.mem_top
-- 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
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : ∃ y ∈ LinearMap.ker f, ∃ z ∈ p, y + z = v), ∃ 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

Premises used: IsCompl.sup_eq_top, Module.Dual.isCompl_ker_of_disjoint_of_ne_bot, Submodule.mem_sup
-- 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
v : V₁
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)
⊢ Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) v : K) ((g : (a : V₁) → K) v : 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

Premises used: LinearMap.ker, rfl
-- 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 : y ∈ LinearMap.ker f
z : V₁
hz : z ∈ p
rwa : y ∈ LinearMap.ker g
rwa₁ rwa₂ rwa₃ rwa₄ : y ∈ LinearMap.ker f
⊢ Eq.{u_1 + 1} (α := K) ((g : (a : V₁) → K) y : K) (0 : K)

Tactic:
rwa [← LinearMap.mem_ker, ← h]

Premises used: LinearMap.mem_ker
-- 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 : y ∈ LinearMap.ker f
z : V₁
hz : z ∈ p
⊢ 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]
-- 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 : y ∈ LinearMap.ker f
z : V₁
hz : z ∈ p
hy' : Eq.{u_1 + 1} (α := K) ((g : (a : V₁) → K) y : K) (0 : K)
rwa rwa₁ rwa₂ 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)
⊢ Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) y : K) (0 : K)

Tactic:
rwa [LinearMap.mem_ker] at hy

Premises used: LinearMap.mem_ker
-- 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 : 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)

Tactic:
replace hy : f y = 0 := by rwa [LinearMap.mem_ker] at hy
-- 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 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)
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)
⊢ Eq.{u_1 + 1} (α := K) ((f : (a : V₁) → K) (y + z) : K) ((g : (a : V₁) → K) (y + z) : K)

Tactic:
obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hz

Premises used: Submodule.mem_span_singleton, Iff.mp, rfl