awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank.{u, v} K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
⊢ finrank.{u, v} K ↥(s ⊔ t) = finrank K V
have h : finrank.{u, v} K ↥(s ⊔ t) = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
Tactic: rw [hdim]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank.{u, v} K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
⊢ finrank.{u, v} K ↥(s ⊔ t) = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
have h : finrank.{u, v} K ↥(s ⊔ t) = finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t)
Tactic: convert! s.finrank_sup_add_finrank_inf_eq t
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank.{u, v} K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
⊢ finrank.{u, v} K ↥(s ⊔ t) = finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t)
have h : finrank.{u, v} K ↥(s ⊔ t) = finrank.{u, v} K ↥(s ⊔ t) + 0
Tactic: rw [h_finrank_inf, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank.{u, v} K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
h : finrank.{u, v} K ↥(s ⊔ t) = finrank.{u, v} K ↥(s ⊔ t) + 0
⊢ finrank.{u, v} K ↥(s ⊔ t) = finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t)
have h₁ : finrank.{u, v} K ↥(s ⊔ t) = finrank.{u, v} K ↥(s ⊔ t)
Tactic: rw [h_finrank_inf, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
⊢ W ⊔ K ∙ v = ⊤ ↔ finrank.{u, v} K (V ⧸ W) = 1
have refine_1 : ∀ (hW : W ⊔ K ∙ v = ⊤), finrank.{u, v} K (V ⧸ W) = 1
Tactic: refine ⟨fun hW ↦ ?_, fun hW ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
refine_1 : ∀ (hW : W ⊔ K ∙ v = ⊤), finrank.{u, v} K (V ⧸ W) = 1
⊢ W ⊔ K ∙ v = ⊤ ↔ finrank.{u, v} K (V ⧸ W) = 1
have refine_2 : ∀ (hW : finrank.{u, v} K (V ⧸ W) = 1), W ⊔ K ∙ v = ⊤
Tactic: refine ⟨fun hW ↦ ?_, fun hW ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
this : W ⊓ K ∙ v = ⊥
⊢ finrank.{u, v} K (V ⧸ W) = 1
have hv₀ : v ≠ 0
Tactic: have hv₀ : v ≠ 0 := by aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
this : W ⊓ K ∙ v = ⊥
hv₀ : v ≠ 0
⊢ finrank.{u, v} K (V ⧸ W) = 1
have aux : finrank.{u, v} K ↥(W ⊔ K ∙ v) + finrank.{u, v} K ↥(W ⊓ K ∙ v) = finrank.{u, v} K ↥W + finrank.{u, v} K ↥(K ∙ v)
Tactic: have aux := finrank_sup_add_finrank_inf_eq W (span K {v})
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
this : W ⊓ K ∙ v = ⊥
hv₀ : v ≠ 0
aux : finrank.{u, v} K ↥(W ⊔ K ∙ v) + finrank.{u, v} K ↥(W ⊓ K ∙ v) = finrank.{u, v} K ↥W + finrank.{u, v} K ↥(K ∙ v)
⊢ finrank.{u, v} K (V ⧸ W) = 1
have aux₁ : finrank.{u, v} K (V ⧸ W) + finrank.{u, v} K ↥W + 0 = finrank.{u, v} K ↥W + 1
Tactic: rw [hW, finrank_span_singleton hv₀, this, finrank_bot, finrank_top,
        ← finrank_quotient_add_finrank W] at aux
Cleared hypotheses: aux
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
⊢ finrank.{u, v} K (V ⧸ W) = 1
have refine_1 : W ⊓ K ∙ v = ⊥
Tactic: suffices W ⊓ span K {v} = ⊥ by
      have hv₀ : v ≠ 0 := by aesop
      have aux := finrank_sup_add_finrank_inf_eq W (span K {v})
      rw [hW, finrank_span_singleton hv₀, this, finrank_bot, finrank_top,
        ← finrank_quotient_add_finrank W] at aux
      lia
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
⊢ W ⊓ K ∙ v = ⊥
have refine_1 : ∀ (w : V) (hw : w ∈ W ⊓ K ∙ v), w = 0
Tactic: refine (Submodule.eq_bot_iff _).mpr fun w hw ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
w : V
hw : w ∈ W ⊓ K ∙ v
⊢ w = 0
have refine_1 : ∀ (t : K) (hw : t • v ∈ W ⊓ K ∙ v) (ht : t • v ∈ W), t • v = 0
Tactic: obtain ⟨ht, t, rfl⟩ : w ∈ W ∧ ∃ t : K, t • v = w := by simpa [mem_span_singleton] using hw
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
t : K
hw : t • v ∈ W ⊓ K ∙ v
ht : t • v ∈ W
⊢ t • v = 0
have refine_1 : ∀ (hw : HSMul.hSMul.{u, v, v} (α := K) 0 v ∈ W ⊓ K ∙ v) (ht : HSMul.hSMul.{u, v, v} (α := K) 0 v ∈ W),
  HSMul.hSMul.{u, v, v} (α := K) 0 v = 0
Tactic: rcases eq_or_ne t 0 with rfl | ht₀
Cleared hypotheses: t, hw, ht
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
t : K
hw : t • v ∈ W ⊓ K ∙ v
ht : t • v ∈ W
refine_1 :
  ∀ (hw : HSMul.hSMul.{u, v, v} (α := K) 0 v ∈ W ⊓ K ∙ v) (ht : HSMul.hSMul.{u, v, v} (α := K) 0 v ∈ W),
    HSMul.hSMul.{u, v, v} (α := K) 0 v = 0
⊢ t • v = 0
have refine_1₁ : ∀ (ht₀ : t ≠ 0), t • v = 0
Tactic: rcases eq_or_ne t 0 with rfl | ht₀
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
t : K
hw : t • v ∈ W ⊓ K ∙ v
ht : t • v ∈ W
ht₀ : t ≠ 0
⊢ t • v = 0
have ht₁ : v ∈ W
Tactic: rw [Submodule.smul_mem_iff _ ht₀] at ht
Cleared hypotheses: ht, ht₀
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : finrank.{u, v} K (V ⧸ W) = 1
⊢ W ⊔ K ∙ v = ⊤
have refine_2 : finrank K V ≤ finrank.{u, v} K ↥W + finrank.{u, v} K ↥(K ∙ v)
Tactic: apply Submodule.eq_top_of_disjoint
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : finrank.{u, v} K (V ⧸ W) = 1
refine_2 : finrank K V ≤ finrank.{u, v} K ↥W + finrank.{u, v} K ↥(K ∙ v)
⊢ W ⊔ K ∙ v = ⊤
have refine_2₁ : Disjoint W (K ∙ v)
Tactic: apply Submodule.eq_top_of_disjoint
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : finrank.{u, v} K (V ⧸ W) = 1
⊢ finrank K V ≤ finrank.{u, v} K ↥W + finrank.{u, v} K ↥(K ∙ v)
have refine_2 : 1 ≤ finrank.{u, v} K ↥(K ∙ v)
Tactic: rw [← W.finrank_quotient_add_finrank, add_comm, add_le_add_iff_left, hW]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
⊢ finrank.{u, v} K ↥(p ⊔ K ∙ v) = finrank.{u, v} K ↥p + 1
have rw : p ⊓ K ∙ v ≤ ⊥
Tactic: rw [← Nat.add_left_inj, finrank_sup_add_finrank_inf_eq, add_assoc,
    Nat.add_left_cancel_iff, finrank_span_singleton (by aesop),
    Nat.left_eq_add, Submodule.finrank_eq_zero, eq_bot_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
x : V
⊢ x ∈ p ⊓ K ∙ v → Membership.mem (γ := Submodule K V) ⊥ x
have simp : (x ∈ p ∧ ∃ (a : K), a • v = x) → Membership.mem (γ := Submodule K V) ⊥ x
Tactic: simp only [mem_inf, mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
x : V
hx : x ∈ p
a : K
hx' : a • v = x
⊢ Membership.mem (γ := Submodule K V) ⊥ x
have hx₁ : a • v ∈ p
Tactic: rw [← hx'] at hx
Cleared hypotheses: hx, hx'
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
x : V
a : K
hx : a • v ∈ p
hx' : a • v = x
⊢ Membership.mem (γ := Submodule K V) ⊥ x
have suffices : a = 0
Tactic: suffices a = 0 by simp [← hx', this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
x : V
a : K
hx : a • v ∈ p
hx' : a • v = x
⊢ a = 0
have contrapose : ∀ (hv : ¬a = 0), v ∈ p
Tactic: contrapose hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
h : W = ⊤
⊢ finrank.{u, v} K ↥W = finrank K V
have rw : finrank.{u, v} K ↥⊤ = finrank K V
Tactic: rw [h, finrank_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
h : W = ⊤
rw : finrank.{u, v} K ↥⊤ = finrank K V
⊢ finrank.{u, v} K ↥W = finrank K V
have rw₁ : finrank K V = finrank K V
Tactic: rw [h, finrank_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
⊢ W = ⊤ ↔ finrank.{u, v} K ↥W = finrank K V
have refine : ∀ (h : finrank.{u, v} K ↥W = finrank K V), W = ⊤
Tactic: refine ⟨fun h ↦ by rw [h, finrank_top], fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
h : finrank.{u, v} K ↥W = finrank K V
⊢ W = ⊤
have apply : finrank.{u, v} K ↥W = finrank.{u, v} K ↥⊤
Tactic: apply eq_of_le_of_finrank_eq le_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
h rw : finrank.{u, v} K ↥W = finrank K V
⊢ finrank.{u, v} K ↥W = finrank.{u, v} K ↥⊤
have rw₁ : finrank K V = finrank K V
Tactic: rw [finrank_top, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
p : Subspace K V
q : Subspace K V₂
f₁ : LinearEquiv.{u, u, v, v'} (RingHom.id K) ↥p ↥q
f₂ : V ≃ₗ[K] V₂
⊢ finrank.{u, v} K (V ⧸ p) = finrank.{u, v'} K (V₂ ⧸ q)
have rw : finrank.{u, v} K (V ⧸ p) + finrank.{u, v} K ↥p = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v} K ↥p
Tactic: rw [← @add_right_cancel_iff _ _ _ (finrank K p), Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₁, Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
p : Subspace K V
q : Subspace K V₂
f₁ : LinearEquiv.{u, u, v, v'} (RingHom.id K) ↥p ↥q
f₂ : V ≃ₗ[K] V₂
rw : finrank.{u, v} K (V ⧸ p) + finrank.{u, v} K ↥p = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v} K ↥p
⊢ finrank.{u, v} K (V ⧸ p) = finrank.{u, v'} K (V₂ ⧸ q)
have rw₁ : finrank K V = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v} K ↥p
Tactic: rw [← @add_right_cancel_iff _ _ _ (finrank K p), Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₁, Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
p : Subspace K V
q : Subspace K V₂
f₁ : LinearEquiv.{u, u, v, v'} (RingHom.id K) ↥p ↥q
f₂ : V ≃ₗ[K] V₂
rw : finrank.{u, v} K (V ⧸ p) + finrank.{u, v} K ↥p = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v} K ↥p
rw₁ : finrank K V = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v} K ↥p
⊢ finrank.{u, v} K (V ⧸ p) = finrank.{u, v'} K (V₂ ⧸ q)
have rw₂ : finrank K V = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v'} K ↥q
Tactic: rw [← @add_right_cancel_iff _ _ _ (finrank K p), Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₁, Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
p : Subspace K V
q : Subspace K V₂
f₁ : LinearEquiv.{u, u, v, v'} (RingHom.id K) ↥p ↥q
f₂ : V ≃ₗ[K] V₂
rw : finrank.{u, v} K (V ⧸ p) + finrank.{u, v} K ↥p = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v} K ↥p
rw₁ : finrank K V = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v} K ↥p
rw₂ : finrank K V = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v'} K ↥q
⊢ finrank.{u, v} K (V ⧸ p) = finrank.{u, v'} K (V₂ ⧸ q)
have rw₃ : finrank K V = finrank K V₂
Tactic: rw [← @add_right_cancel_iff _ _ _ (finrank K p), Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₁, Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
p : Subspace K V
q : Subspace K V₂
f₁ : LinearEquiv.{u, u, v, v'} (RingHom.id K) ↥p ↥q
f₂ : V ≃ₗ[K] V₂
rw : finrank.{u, v} K (V ⧸ p) + finrank.{u, v} K ↥p = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v} K ↥p
rw₁ : finrank K V = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v} K ↥p
rw₂ : finrank K V = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v'} K ↥q
rw₃ : finrank K V = finrank K V₂
⊢ finrank.{u, v} K (V ⧸ p) = finrank.{u, v'} K (V₂ ⧸ q)
have rw₄ : finrank K V₂ = finrank K V₂
Tactic: rw [← @add_right_cancel_iff _ _ _ (finrank K p), Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₁, Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
p q : Subspace K V
f : (V ⧸ p) ≃ₗ[K] ↥q
⊢ finrank.{u, v} K (V ⧸ q) = finrank.{u, v} K ↥p
have rw : finrank.{u, v} K (V ⧸ q) + finrank.{u, v} K ↥q = finrank.{u, v} K ↥p + finrank.{u, v} K ↥q
Tactic: rw [← add_right_cancel_iff, Submodule.finrank_quotient_add_finrank, ← LinearEquiv.finrank_eq f,
      add_comm, Submodule.finrank_quotient_add_finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
p q : Subspace K V
f : (V ⧸ p) ≃ₗ[K] ↥q
rw : finrank.{u, v} K (V ⧸ q) + finrank.{u, v} K ↥q = finrank.{u, v} K ↥p + finrank.{u, v} K ↥q
⊢ finrank.{u, v} K (V ⧸ q) = finrank.{u, v} K ↥p
have rw₁ : ℕ
Tactic: rw [← add_right_cancel_iff, Submodule.finrank_quotient_add_finrank, ← LinearEquiv.finrank_eq f,
      add_comm, Submodule.finrank_quotient_add_finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
p q : Subspace K V
f : (V ⧸ p) ≃ₗ[K] ↥q
rw : finrank.{u, v} K (V ⧸ q) + finrank.{u, v} K ↥q = finrank.{u, v} K ↥p + finrank.{u, v} K ↥q
rw₁ : ℕ
⊢ finrank.{u, v} K (V ⧸ q) = finrank.{u, v} K ↥p
have rw₂ : finrank K V = finrank.{u, v} K ↥p + finrank.{u, v} K ↥q
Tactic: rw [← add_right_cancel_iff, Submodule.finrank_quotient_add_finrank, ← LinearEquiv.finrank_eq f,
      add_comm, Submodule.finrank_quotient_add_finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
p q : Subspace K V
f : (V ⧸ p) ≃ₗ[K] ↥q
rw : finrank.{u, v} K (V ⧸ q) + finrank.{u, v} K ↥q = finrank.{u, v} K ↥p + finrank.{u, v} K ↥q
rw₁ : ℕ
rw₂ : finrank K V = finrank.{u, v} K ↥p + finrank.{u, v} K ↥q
⊢ finrank.{u, v} K (V ⧸ q) = finrank.{u, v} K ↥p
have rw₃ : finrank K V = finrank.{u, v} K ↥p + finrank.{u, v} K (V ⧸ p)
Tactic: rw [← add_right_cancel_iff, Submodule.finrank_quotient_add_finrank, ← LinearEquiv.finrank_eq f,
      add_comm, Submodule.finrank_quotient_add_finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
p q : Subspace K V
f : (V ⧸ p) ≃ₗ[K] ↥q
rw : finrank.{u, v} K (V ⧸ q) + finrank.{u, v} K ↥q = finrank.{u, v} K ↥p + finrank.{u, v} K ↥q
rw₁ : ℕ
rw₂ : finrank K V = finrank.{u, v} K ↥p + finrank.{u, v} K ↥q
rw₃ : finrank K V = finrank.{u, v} K ↥p + finrank.{u, v} K (V ⧸ p)
⊢ finrank.{u, v} K (V ⧸ q) = finrank.{u, v} K ↥p
have rw₄ : finrank K V = finrank.{u, v} K (V ⧸ p) + finrank.{u, v} K ↥p
Tactic: rw [← add_right_cancel_iff, Submodule.finrank_quotient_add_finrank, ← LinearEquiv.finrank_eq f,
      add_comm, Submodule.finrank_quotient_add_finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
p q : Subspace K V
f : (V ⧸ p) ≃ₗ[K] ↥q
rw : finrank.{u, v} K (V ⧸ q) + finrank.{u, v} K ↥q = finrank.{u, v} K ↥p + finrank.{u, v} K ↥q
rw₁ : ℕ
rw₂ : finrank K V = finrank.{u, v} K ↥p + finrank.{u, v} K ↥q
rw₃ : finrank K V = finrank.{u, v} K ↥p + finrank.{u, v} K (V ⧸ p)
rw₄ : finrank K V = finrank.{u, v} K (V ⧸ p) + finrank.{u, v} K ↥p
⊢ finrank.{u, v} K (V ⧸ q) = finrank.{u, v} K ↥p
have rw₅ : finrank K V = finrank K V
Tactic: rw [← add_right_cancel_iff, Submodule.finrank_quotient_add_finrank, ← LinearEquiv.finrank_eq f,
      add_comm, Submodule.finrank_quotient_add_finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
f : V →ₗ[K] V₂
⊢ finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
have rw : finrank.{u, v} K (V ⧸ f.ker) + finrank.{u, v} K ↥f.ker = finrank K V
Tactic: rw [← f.quotKerEquivRange.finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
f : V →ₗ[K] V₂
h : finrank K V₂ < finrank K V
⊢ f.ker ≠ ⊥
have h₁ : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
Tactic: have h₁ := f.finrank_range_add_finrank_ker
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
f : V →ₗ[K] V₂
h : finrank K V₂ < finrank K V
h₁ : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
⊢ f.ker ≠ ⊥
have h₂ : finrank.{u, v'} K ↥f.range ≤ finrank K V₂
Tactic: have h₂ : finrank K (LinearMap.range f) ≤ finrank K V₂ := (LinearMap.range f).finrank_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Lemmas (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
f : V →ₗ[K] V₂
h : finrank K V₂ < finrank K V
h₁ : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
h₂ : finrank.{u, v'} K ↥f.range ≤ finrank K V₂
⊢ f.ker ≠ ⊥
have suffices : 0 < finrank.{u, v} K ↥f.ker
Tactic: suffices 0 < finrank K (LinearMap.ker f) from Submodule.one_le_finrank_iff.mp this