awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
⊢ LinearMap.range (M := Dual.{u_1, u_2} R (M ⧸ W)) W.mkQ.dualMap = W.dualAnnihilator
have h : ∀ (φ : Dual R M),
  Membership.mem (γ := Submodule R (Dual R M)) (LinearMap.range (M := Dual.{u_1, u_2} R (M ⧸ W)) W.mkQ.dualMap) φ ↔
    φ ∈ W.dualAnnihilator
Tactic: ext φ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
φ : Dual R M
⊢ (∃ (y : Dual.{u_1, u_2} R (M ⧸ W)), (W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) y = φ) ↔ φ ∈ W.dualAnnihilator
have h : (∃ (y : Dual.{u_1, u_2} R (M ⧸ W)), (W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) y = φ) → φ ∈ W.dualAnnihilator
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
φ : Dual R M
h : (∃ (y : Dual.{u_1, u_2} R (M ⧸ W)), (W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) y = φ) → φ ∈ W.dualAnnihilator
⊢ (∃ (y : Dual.{u_1, u_2} R (M ⧸ W)), (W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) y = φ) ↔ φ ∈ W.dualAnnihilator
have h₁ : φ ∈ W.dualAnnihilator → ∃ (y : Dual.{u_1, u_2} R (M ⧸ W)), (W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) y = φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
ψ : Dual.{u_1, u_2} R (M ⧸ W)
⊢ Membership.mem (α := Dual R M) W.dualAnnihilator ((W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) ψ : Dual R M)
have this : Membership.mem (α := Dual R M) (γ := Submodule R (Dual R M))
  (LinearMap.range (M := Dual.{u_1, u_2} R (M ⧸ W)) W.mkQ.dualMap)
  ((W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) ψ : Dual R M)
Tactic: have := LinearMap.mem_range_self W.mkQ.dualMap ψ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
φ : Dual R M
hφ : φ ∈ W.dualAnnihilator
⊢ ∃ (y : Dual.{u_1, u_2} R (M ⧸ W)), (W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M) y = φ
have h : (W.mkQ.dualMap : (a : Dual R (M ⧸ W)) → Dual R M)
    ((W.dualCopairing : (a : ↥W.dualAnnihilator) → M ⧸ W →ₗ[R] R)
      (Subtype.mk (p := fun (x : Dual R M) ↦ x ∈ W.dualAnnihilator) φ hφ)) =
  φ
Tactic: exists W.dualCopairing ⟨φ, hφ⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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'
W : Submodule R M
⊢ LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap ⋯ ∘ₗ W.dualCopairing = LinearMap.id
have h : ∀ (x : ↥W.dualAnnihilator) (x_1 : M),
  Eq.{u_1 + 1} (α := R)
    (((↑((LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap sorry ∘ₗ W.dualCopairing :
                  (a : ↥W.dualAnnihilator) → ↥W.dualAnnihilator)
                x) :
            Dual R M) :
          (a : M) → R)
        x_1 :
      R)
    (((↑((LinearMap.id : (a : ↥W.dualAnnihilator) → ↥W.dualAnnihilator) x) : Dual R M) : (a : M) → R) x_1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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'
W : Submodule R M
⊢ W.dualCopairing ∘ₗ LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap ⋯ = LinearMap.id
have h : ∀ (x : Dual.{u_1, u_2} R (M ⧸ W)) (x_1 : M),
  Eq.{u_1 + 1} (α := R)
    (((W.dualCopairing ∘ₗ LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap sorry :
                (a : Dual R (M ⧸ W)) → Dual R (M ⧸ W))
              x ∘ₗ
            W.mkQ :
          (a : M) → R)
        x_1 :
      R)
    (((LinearMap.id : (a : Dual R (M ⧸ W)) → Dual R (M ⧸ W)) x ∘ₗ W.mkQ : (a : M) → R) x_1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
⊢ W.dualAnnihilator = ⊥ ↔ Subsingleton (Dual.{u_1, u_2} R (M ⧸ W))
have rw : W.dualAnnihilator = ⊥ ↔ Subsingleton ↥W.dualAnnihilator
Tactic: rw [W.dualQuotEquivDualAnnihilator.toEquiv.subsingleton_congr, subsingleton_iff_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
rw : W.dualAnnihilator = ⊥ ↔ Subsingleton ↥W.dualAnnihilator
⊢ W.dualAnnihilator = ⊥ ↔ Subsingleton (Dual.{u_1, u_2} R (M ⧸ W))
have rw₁ : W.dualAnnihilator = ⊥ ↔ W.dualAnnihilator = ⊥
Tactic: rw [W.dualQuotEquivDualAnnihilator.toEquiv.subsingleton_congr, subsingleton_iff_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Projective.{u_1, u_2} R (M ⧸ W)
⊢ W.dualAnnihilator = ⊥ ↔ W = ⊤
have rw : Subsingleton (Dual.{u_1, u_2} R (M ⧸ W)) ↔ W = ⊤
Tactic: rw [dualAnnihilator_eq_bot_iff', subsingleton_dual_iff, Quotient.subsingleton_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Projective.{u_1, u_2} R (M ⧸ W)
rw : Subsingleton (Dual.{u_1, u_2} R (M ⧸ W)) ↔ W = ⊤
⊢ W.dualAnnihilator = ⊥ ↔ W = ⊤
have rw₁ : Subsingleton.{u_2 + 1} (M ⧸ W) ↔ W = ⊤
Tactic: rw [dualAnnihilator_eq_bot_iff', subsingleton_dual_iff, Quotient.subsingleton_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Projective.{u_1, u_2} R (M ⧸ W)
rw : Subsingleton (Dual.{u_1, u_2} R (M ⧸ W)) ↔ W = ⊤
rw₁ : Subsingleton.{u_2 + 1} (M ⧸ W) ↔ W = ⊤
⊢ W.dualAnnihilator = ⊥ ↔ W = ⊤
have rw₂ : W = ⊤ ↔ W = ⊤
Tactic: rw [dualAnnihilator_eq_bot_iff', subsingleton_dual_iff, Quotient.subsingleton_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Projective R M
⊢ W.dualAnnihilator = ⊤ ↔ W = ⊥
have refine : ∀ (h : W.dualAnnihilator = ⊤), W = ⊥
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h ▸ dualAnnihilator_bot⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Projective R M
h : W.dualAnnihilator = ⊤
⊢ W = ⊥
have refine : ∀ (v : M) (hv : v ∈ W) (f : Dual R M), Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) v : R) (0 : R)
Tactic: refine W.eq_bot_iff.mpr fun v hv ↦ (forall_dual_apply_eq_zero_iff R v).mp fun f ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R M
inst_3 : Projective R M
h : W.dualAnnihilator = ⊤
v : M
hv : v ∈ W
f : Dual R M
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) v : R) (0 : R)
have refine : f ∈ W.dualAnnihilator
Tactic: refine (mem_dualAnnihilator f).mp ?_ v hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R (Dual R M)
⊢ W.quotDualCoannihilatorToDual.Nondegenerate
have rw : W.quotDualCoannihilatorToDual.ker = ⊥ ∧ W.quotDualCoannihilatorToDual.flip.ker = ⊥
Tactic: rw [Nondegenerate, separatingLeft_iff_ker_eq_bot, separatingRight_iff_flip_ker_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
W : Submodule R (Dual R M)
⊢ W.quotDualCoannihilatorToDual.ker = ⊥ ∧ W.quotDualCoannihilatorToDual.flip.ker = ⊥
have simp_rw : Function.Injective (α := M ⧸ W.dualCoannihilator) (β := ↥W →ₗ[R] R)
    (⇑W.quotDualCoannihilatorToDual : (a : M ⧸ W.dualCoannihilator) → ↥W →ₗ[R] R) ∧
  W.quotDualCoannihilatorToDual.flip.ker = ⊥
Tactic: simp_rw [ker_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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)
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
have rw : Eq (α := Submodule R ↥f.range) (range f.rangeRestrict) ⊤
Tactic: rw [← range_eq_top, range_rangeRestrict]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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)
rw : Eq (α := Submodule R ↥f.range) (range f.rangeRestrict) ⊤
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
have rw₁ : Eq.{u_3 + 1} (α := Submodule R ↥f.range) ⊤ ⊤
Tactic: rw [← range_eq_top, range_rangeRestrict]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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)
⊢ f.dualMap.range = f.ker.dualAnnihilator
have rr_surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
Tactic: have rr_surj : Function.Surjective f.rangeRestrict := by
    rw [← range_eq_top, range_rangeRestrict]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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)
⊢ f.dualMap.range = f.ker.dualAnnihilator
have this : range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict) =
  (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator
Tactic: have := range_dualMap_eq_dualAnnihilator_ker_of_surjective f.rangeRestrict rr_surj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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.dualMap.range = f.ker.dualAnnihilator
have h : f.dualMap.range = range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict)
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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.dualMap.range = range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict)
⊢ f.dualMap.range = f.ker.dualAnnihilator
have h₁ : f.ker.dualAnnihilator = (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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.dualMap.range = range (M := Dual.{u_1, u_3} R ↥f.range) (dualMap f.rangeRestrict)
have h : (f.range.subtype ∘ₗ f.rangeRestrict).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
      _ = _ := ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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)
have h : f.range.subtype.dualMap.range = ⊤
Tactic: rw [← dualMap_comp_dualMap, range_comp_of_range_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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.dualAnnihilator = (ker (M₂ := ↥f.range) f.rangeRestrict).dualAnnihilator
have h : f.ker = ker (M₂ := ↥f.range) f.rangeRestrict
Tactic: apply congr_arg
-- 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₁
this : finrank K ↥(LinearMap.range f) = 1
⊢ finrank.{u_1, u_2} K ↥(LinearMap.ker f) + 1 = finrank K V₁
have 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)
Tactic: rw [← (LinearMap.ker f).finrank_quotient_add_finrank, add_comm, add_left_inj,
    f.quotKerEquivRange.finrank_eq, 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₁
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)
⊢ finrank.{u_1, u_2} K ↥(LinearMap.ker f) + 1 = finrank K V₁
have 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)
Tactic: rw [← (LinearMap.ker f).finrank_quotient_add_finrank, add_comm, add_left_inj,
    f.quotKerEquivRange.finrank_eq, 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₁
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)
⊢ finrank.{u_1, u_2} K ↥(LinearMap.ker f) + 1 = finrank K V₁
have rw₂ : 1 = finrank.{u_1, u_2} K (V₁ ⧸ LinearMap.ker f)
Tactic: rw [← (LinearMap.ker f).finrank_quotient_add_finrank, add_comm, add_left_inj,
    f.quotKerEquivRange.finrank_eq, 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₁
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)
⊢ finrank.{u_1, u_2} K ↥(LinearMap.ker f) + 1 = finrank K V₁
have rw₃ : 1 = finrank K ↥(LinearMap.range f)
Tactic: rw [← (LinearMap.ker f).finrank_quotient_add_finrank, add_comm, add_left_inj,
    f.quotKerEquivRange.finrank_eq, 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₁
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)
⊢ finrank.{u_1, u_2} K ↥(LinearMap.ker f) + 1 = finrank K V₁
have rw₄ : Eq (α := ℕ) 1 1
Tactic: rw [← (LinearMap.ker f).finrank_quotient_add_finrank, add_comm, add_left_inj,
    f.quotKerEquivRange.finrank_eq, 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₁
f : Dual K V₁
hf : f ≠ 0
inst_3 : FiniteDimensional K V₁
⊢ finrank.{u_1, u_2} K ↥(LinearMap.ker f) + 1 = finrank K V₁
have suffices : finrank K ↥(LinearMap.range f) = 1
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]
-- 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₁
⊢ finrank K ↥(LinearMap.range f) = 1
have rw : finrank K ↥⊤ = 1
Tactic: rw [range_eq_top_of_ne_zero hf, finrank_top, finrank_self]
-- 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₁
rw : finrank K ↥⊤ = 1
⊢ finrank K ↥(LinearMap.range f) = 1
have rw₁ : finrank K K = 1
Tactic: rw [range_eq_top_of_ne_zero hf, finrank_top, finrank_self]
-- 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₁
rw : finrank K ↥⊤ = 1
rw₁ : finrank K K = 1
⊢ finrank K ↥(LinearMap.range f) = 1
have rw₂ : Eq (α := ℕ) 1 1
Tactic: rw [range_eq_top_of_ne_zero hf, finrank_top, finrank_self]
-- 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 ≠ ⊥
⊢ IsCompl (LinearMap.ker f) p
have refine : finrank.{u_1, u_2} K ↥⊤ ≤ finrank.{u_1, u_2} K ↥(LinearMap.ker f ⊔ p)
Tactic: refine ⟨hpf, codisjoint_iff.mpr <| eq_of_le_of_finrank_le le_top ?_⟩
-- 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₁
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 ↥⊤ ≤ finrank.{u_1, u_2} K ↥(LinearMap.ker f ⊔ p)
have 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
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]
-- 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
⊢ finrank.{u_1, u_2} K ↥⊤ ≤ finrank.{u_1, u_2} K ↥(LinearMap.ker f ⊔ p)
have rwa : finrank K V₁ ≤ 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]
-- 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)
⊢ finrank.{u_1, u_2} K ↥⊤ ≤ finrank.{u_1, u_2} K ↥(LinearMap.ker f ⊔ p)
have rwa₁ : finrank K V₁ ≤ finrank.{u_1, u_2} K ↥(LinearMap.ker f) + 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 (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
⊢ finrank.{u_1, u_2} K ↥⊤ ≤ finrank.{u_1, u_2} K ↥(LinearMap.ker f ⊔ p)
have 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
Tactic: rwa [finrank_top, this, ← finrank_ker_add_one_of_ne_zero hf, add_le_add_iff_left,
    Submodule.one_le_finrank_iff]