awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Type u_1
A : Type u_2
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : AddCommGroup W
inst_6 : Module K W
inst_7 : Module A W
inst_8 : LinearMap.CompatibleSMul V W K A
h : finrank K W = 1
f : V →ₗ[A] W
w : f ≠ 0
⊢ Surjective.{v + 1, u_1 + 1} (α := V) (β := W)
    (⇑((↑K :
            {S : Type u_2} →
              {M : Type v} →
                {M₂ : Type u_1} →
                  [inst : Semiring K] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module K M] →
                            [inst_13 : Module K M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
          f) :
      (a : V) → W)
have obtain : ∀ (v : V) (n : Ne.{u_1 + 1} (α := W) ((f : (a : V) → W) v : W) ((0 : (a : V) → W) v : W)),
  Surjective.{v + 1, u_1 + 1} (α := V) (β := W)
    (⇑((↑K :
            {S : Type u_2} →
              {M : Type v} →
                {M₂ : Type u_1} →
                  [inst : Semiring K] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module K M] →
                            [inst_13 : Module K M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
          f) :
      (a : V) → W)
Tactic: obtain ⟨v, n⟩ := DFunLike.ne_iff.mp w
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Type u_1
A : Type u_2
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : AddCommGroup W
inst_6 : Module K W
inst_7 : Module A W
inst_8 : LinearMap.CompatibleSMul V W K A
h : finrank K W = 1
f : V →ₗ[A] W
w : f ≠ 0
v : V
n : Ne.{u_1 + 1} (α := W) ((f : (a : V) → W) v : W) ((0 : (a : V) → W) v : W)
z : W
⊢ ∃ (a : V),
    ((↑K :
              {S : Type u_2} →
                {M : Type v} →
                  {M₂ : Type u_1} →
                    [inst : Semiring K] →
                      [inst_9 : Semiring S] →
                        [inst_10 : AddCommMonoid M] →
                          [inst_11 : AddCommMonoid M₂] →
                            [inst_12 : Module K M] →
                              [inst_13 : Module K M₂] →
                                [inst_14 : Module S M] →
                                  [inst_15 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
            f :
          (a : V) → W)
        a =
      z
have obtain : ∀ (c : K),
  ∃ (a : V),
    ((↑K :
              {S : Type u_2} →
                {M : Type v} →
                  {M₂ : Type u_1} →
                    [inst : Semiring K] →
                      [inst_9 : Semiring S] →
                        [inst_10 : AddCommMonoid M] →
                          [inst_11 : AddCommMonoid M₂] →
                            [inst_12 : Module K M] →
                              [inst_13 : Module K M₂] →
                                [inst_14 : Module S M] →
                                  [inst_15 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
            f :
          (a : V) → W)
        a =
      HSMul.hSMul (β := W) c ((f : (a : V) → W) v : W)
Tactic: obtain ⟨c, rfl⟩ := (finrank_eq_one_iff_of_nonzero' (f v) n).mp h z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + (m + 1)))
have a : LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (k + (m + 1)))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
a : LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (k + (m + 1)))
⊢ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + (m + 1)))
have a₁ : LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (k + (m + 1)))
have a : LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (m + 1) * f ^ k)
Tactic: rw [add_comm, pow_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
have a : LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ (k + m))
Tactic: rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
        Module.End.mul_eq_comp, Module.End.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
        Nat.add_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
a : LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ (k + m))
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
have a₁ : LinearMap.ker (f ^ (k + (1 + m))) ≤ LinearMap.ker (f ^ (k + m))
Tactic: rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
        Module.End.mul_eq_comp, Module.End.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
        Nat.add_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
a : LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ (k + m))
a₁ : LinearMap.ker (f ^ (k + (1 + m))) ≤ LinearMap.ker (f ^ (k + m))
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
have a₂ : LinearMap.ker (f ^ (k + 1 + m)) ≤ LinearMap.ker (f ^ (k + m))
Tactic: rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
        Module.End.mul_eq_comp, Module.End.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
        Nat.add_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
a : LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ (k + m))
a₁ : LinearMap.ker (f ^ (k + (1 + m))) ≤ LinearMap.ker (f ^ (k + m))
a₂ : LinearMap.ker (f ^ (k + 1 + m)) ≤ LinearMap.ker (f ^ (k + m))
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
have a₃ : LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ (k + m))
Tactic: rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
        Module.End.mul_eq_comp, Module.End.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
        Nat.add_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
a : LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ (k + m))
a₁ : LinearMap.ker (f ^ (k + (1 + m))) ≤ LinearMap.ker (f ^ (k + m))
a₂ : LinearMap.ker (f ^ (k + 1 + m)) ≤ LinearMap.ker (f ^ (k + m))
a₃ : LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ (k + m))
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
have a₄ : LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ k * f ^ m)
Tactic: rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
        Module.End.mul_eq_comp, Module.End.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
        Nat.add_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
a : LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ (k + m))
a₁ : LinearMap.ker (f ^ (k + (1 + m))) ≤ LinearMap.ker (f ^ (k + m))
a₂ : LinearMap.ker (f ^ (k + 1 + m)) ≤ LinearMap.ker (f ^ (k + m))
a₃ : LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ (k + m))
a₄ : LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ k * f ^ m)
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
have a₅ : ((f ^ (k + 1)) ∘ₗ f ^ m).ker ≤ LinearMap.ker (f ^ k * f ^ m)
Tactic: rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
        Module.End.mul_eq_comp, Module.End.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
        Nat.add_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
a : LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ (k + m))
a₁ : LinearMap.ker (f ^ (k + (1 + m))) ≤ LinearMap.ker (f ^ (k + m))
a₂ : LinearMap.ker (f ^ (k + 1 + m)) ≤ LinearMap.ker (f ^ (k + m))
a₃ : LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ (k + m))
a₄ : LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ k * f ^ m)
a₅ : ((f ^ (k + 1)) ∘ₗ f ^ m).ker ≤ LinearMap.ker (f ^ k * f ^ m)
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
have a₆ : ((f ^ (k + 1)) ∘ₗ f ^ m).ker ≤ ((f ^ k) ∘ₗ f ^ m).ker
Tactic: rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
        Module.End.mul_eq_comp, Module.End.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
        Nat.add_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
a : LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ (k + m))
a₁ : LinearMap.ker (f ^ (k + (1 + m))) ≤ LinearMap.ker (f ^ (k + m))
a₂ : LinearMap.ker (f ^ (k + 1 + m)) ≤ LinearMap.ker (f ^ (k + m))
a₃ : LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ (k + m))
a₄ : LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ k * f ^ m)
a₅ : ((f ^ (k + 1)) ∘ₗ f ^ m).ker ≤ LinearMap.ker (f ^ k * f ^ m)
a₆ : ((f ^ (k + 1)) ∘ₗ f ^ m).ker ≤ ((f ^ k) ∘ₗ f ^ m).ker
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
have a₇ : comap (f ^ m) (LinearMap.ker (f ^ (k + 1))) ≤ ((f ^ k) ∘ₗ f ^ m).ker
Tactic: rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
        Module.End.mul_eq_comp, Module.End.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
        Nat.add_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
a : LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ (k + m))
a₁ : LinearMap.ker (f ^ (k + (1 + m))) ≤ LinearMap.ker (f ^ (k + m))
a₂ : LinearMap.ker (f ^ (k + 1 + m)) ≤ LinearMap.ker (f ^ (k + m))
a₃ : LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ (k + m))
a₄ : LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ k * f ^ m)
a₅ : ((f ^ (k + 1)) ∘ₗ f ^ m).ker ≤ LinearMap.ker (f ^ k * f ^ m)
a₆ : ((f ^ (k + 1)) ∘ₗ f ^ m).ker ≤ ((f ^ k) ∘ₗ f ^ m).ker
a₇ : comap (f ^ m) (LinearMap.ker (f ^ (k + 1))) ≤ ((f ^ k) ∘ₗ f ^ m).ker
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
have a₈ : comap (f ^ m) (LinearMap.ker (f ^ (k + 1))) ≤ comap (f ^ m) (LinearMap.ker (f ^ k))
Tactic: rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
        Module.End.mul_eq_comp, Module.End.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
        Nat.add_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
a : LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ (k + m))
a₁ : LinearMap.ker (f ^ (k + (1 + m))) ≤ LinearMap.ker (f ^ (k + m))
a₂ : LinearMap.ker (f ^ (k + 1 + m)) ≤ LinearMap.ker (f ^ (k + m))
a₃ : LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ (k + m))
a₄ : LinearMap.ker (f ^ (k + 1) * f ^ m) ≤ LinearMap.ker (f ^ k * f ^ m)
a₅ : ((f ^ (k + 1)) ∘ₗ f ^ m).ker ≤ LinearMap.ker (f ^ k * f ^ m)
a₆ : ((f ^ (k + 1)) ∘ₗ f ^ m).ker ≤ ((f ^ k) ∘ₗ f ^ m).ker
a₇ : comap (f ^ m) (LinearMap.ker (f ^ (k + 1))) ≤ ((f ^ k) ∘ₗ f ^ m).ker
a₈ : comap (f ^ m) (LinearMap.ker (f ^ (k + 1))) ≤ comap (f ^ m) (LinearMap.ker (f ^ k))
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
have a₉ : comap (f ^ m) (LinearMap.ker (f ^ (k + 1))) ≤ comap (f ^ m) (LinearMap.ker (f ^ k.succ))
Tactic: rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
        Module.End.mul_eq_comp, Module.End.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
        Nat.add_one]
-- 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 : Submodule K V
h : s ≠ ⊤
⊢ finrank.{u, v} K ↥s < finrank K V
have rw : finrank.{u, v} K ↥s < finrank.{u, v} K ↥s + finrank.{u, v} K (V ⧸ s)
Tactic: rw [← s.finrank_quotient_add_finrank, add_comm]
-- 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 : FiniteDimensional K V
s : Submodule K V
h : s ≠ ⊤
⊢ finrank.{u, v} K ↥s < finrank.{u, v} K ↥s + finrank.{u, v} K (V ⧸ s)
have h₁ : Nontrivial.{v} (V ⧸ s)
Tactic: rw [← Quotient.nontrivial_iff] at h
Cleared hypotheses: h
-- 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
s t : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥s
inst_4 : FiniteDimensional.{u, v} K ↥t
⊢ finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t) = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
have key : Module.rank K ↥(s ⊔ t) + Module.rank K ↥(s ⊓ t) = Module.rank K ↥s + Module.rank K ↥t
Tactic: have key : Module.rank K ↑(s ⊔ t) + Module.rank K ↑(s ⊓ t) = Module.rank K s + Module.rank K t :=
    rank_sup_add_rank_inf_eq s t
-- 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
s t : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥s
inst_4 : FiniteDimensional.{u, v} K ↥t
key : Module.rank K ↥(s ⊔ t) + Module.rank K ↥(s ⊓ t) = Module.rank K ↥s + Module.rank K ↥t
⊢ finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t) = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
have key₁ : (↑(finrank.{u, v} K ↥(s ⊔ t)) : Cardinal.{v}) + Module.rank K ↥(s ⊓ t) = Module.rank K ↥s + Module.rank K ↥t
Tactic: rw [← finrank_eq_rank] at key
Cleared hypotheses: key
-- 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
s t : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥s
inst_4 : FiniteDimensional.{u, v} K ↥t
key : (↑(finrank.{u, v} K ↥(s ⊔ t)) : Cardinal.{v}) + Module.rank K ↥(s ⊓ t) = Module.rank K ↥s + Module.rank K ↥t
⊢ finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t) = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
have key₁ : HAdd.hAdd (α := Cardinal.{v}) (↑(finrank.{u, v} K ↥(s ⊔ t)) : Cardinal.{v})
    (↑(finrank.{u, v} K ↥(s ⊓ t)) : Cardinal.{v}) =
  Module.rank K ↥s + Module.rank K ↥t
Tactic: rw [← finrank_eq_rank] at key
Cleared hypotheses: key
-- 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
s t : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥s
inst_4 : FiniteDimensional.{u, v} K ↥t
key :
  HAdd.hAdd (α := Cardinal.{v}) (↑(finrank.{u, v} K ↥(s ⊔ t)) : Cardinal.{v})
      (↑(finrank.{u, v} K ↥(s ⊓ t)) : Cardinal.{v}) =
    Module.rank K ↥s + Module.rank K ↥t
⊢ finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t) = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
have key₁ : HAdd.hAdd (α := Cardinal.{v}) (↑(finrank.{u, v} K ↥(s ⊔ t)) : Cardinal.{v})
    (↑(finrank.{u, v} K ↥(s ⊓ t)) : Cardinal.{v}) =
  (↑(finrank.{u, v} K ↥s) : Cardinal.{v}) + Module.rank K ↥t
Tactic: rw [← finrank_eq_rank] at key
Cleared hypotheses: key
-- 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
s t : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥s
inst_4 : FiniteDimensional.{u, v} K ↥t
key :
  HAdd.hAdd (α := Cardinal.{v}) (↑(finrank.{u, v} K ↥(s ⊔ t)) : Cardinal.{v})
      (↑(finrank.{u, v} K ↥(s ⊓ t)) : Cardinal.{v}) =
    (↑(finrank.{u, v} K ↥s) : Cardinal.{v}) + Module.rank K ↥t
⊢ finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t) = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
have key₁ : HAdd.hAdd (α := Cardinal.{v}) (↑(finrank.{u, v} K ↥(s ⊔ t)) : Cardinal.{v})
    (↑(finrank.{u, v} K ↥(s ⊓ t)) : Cardinal.{v}) =
  HAdd.hAdd (α := Cardinal.{v}) (↑(finrank.{u, v} K ↥s) : Cardinal.{v}) (↑(finrank.{u, v} K ↥t) : Cardinal.{v})
Tactic: rw [← finrank_eq_rank] at key
Cleared hypotheses: key
-- 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
s t : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥s
inst_4 : FiniteDimensional.{u, v} K ↥t
key : Module.rank K ↥(s ⊔ t) + Module.rank K ↥(s ⊓ t) = Module.rank K ↥s + Module.rank K ↥t
⊢ finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t) = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
have key₁ : HAdd.hAdd (α := Cardinal.{v}) (↑(finrank.{u, v} K ↥(s ⊔ t)) : Cardinal.{v})
    (↑(finrank.{u, v} K ↥(s ⊓ t)) : Cardinal.{v}) =
  HAdd.hAdd (α := Cardinal.{v}) (↑(finrank.{u, v} K ↥s) : Cardinal.{v}) (↑(finrank.{u, v} K ↥t) : Cardinal.{v})
Tactic: repeat rw [← finrank_eq_rank] at key
Cleared hypotheses: key
-- 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
s t : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥s
inst_4 : FiniteDimensional.{u, v} K ↥t
key :
  HAdd.hAdd (α := Cardinal.{v}) (↑(finrank.{u, v} K ↥(s ⊔ t)) : Cardinal.{v})
      (↑(finrank.{u, v} K ↥(s ⊓ t)) : Cardinal.{v}) =
    HAdd.hAdd (α := Cardinal.{v}) (↑(finrank.{u, v} K ↥s) : Cardinal.{v}) (↑(finrank.{u, v} K ↥t) : Cardinal.{v})
⊢ finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t) = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
have norm_cast : ∀ (key : finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t) = 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 + finrank.{u, v} K ↥t
Tactic: norm_cast at key
Cleared hypotheses: key
-- 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
s t : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥s
inst_4 : FiniteDimensional.{u, v} K ↥t
⊢ finrank.{u, v} K ↥(s ⊔ t) ≤ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
have rw : finrank.{u, v} K ↥(s ⊔ t) ≤ finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t)
Tactic: rw [← finrank_sup_add_finrank_inf_eq]
-- 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
⊢ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t ≤ finrank K V
have rw : finrank.{u, v} K ↥(s ⊔ t) ≤ finrank K V
Tactic: rw [← Submodule.finrank_sup_add_finrank_inf_eq s t, hdisjoint.eq_bot, finrank_bot, add_zero]
-- 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 : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K V ≤ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
hdisjoint : Disjoint s t
⊢ finrank.{u, v} K ↥(s ⊓ t) = 0
have hdisjoint₁ : s ⊓ t = ⊥
Tactic: rw [disjoint_iff_inf_le, le_bot_iff] at hdisjoint
Cleared hypotheses: hdisjoint
-- 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
hdim : finrank K V ≤ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
hdisjoint : s ⊓ t = ⊥
⊢ finrank.{u, v} K ↥(s ⊓ t) = 0
have rw : finrank.{u, v} K ↥⊥ = 0
Tactic: rw [hdisjoint, finrank_bot]
-- 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
hdim : finrank K V ≤ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
hdisjoint : s ⊓ t = ⊥
rw : finrank.{u, v} K ↥⊥ = 0
⊢ finrank.{u, v} K ↥(s ⊓ t) = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [hdisjoint, finrank_bot]
-- 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 : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K V ≤ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
hdisjoint : Disjoint s t
⊢ s ⊔ t = ⊤
have h_finrank_inf : finrank.{u, v} K ↥(s ⊓ t) = 0
Tactic: have h_finrank_inf : finrank K ↑(s ⊓ t) = 0 := by
    rw [disjoint_iff_inf_le, le_bot_iff] at hdisjoint
    rw [hdisjoint, finrank_bot]
-- 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
hdim : finrank K V ≤ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
hdisjoint : Disjoint s t
h_finrank_inf : finrank.{u, v} K ↥(s ⊓ t) = 0
⊢ s ⊔ t = ⊤
have h : finrank.{u, v} K ↥(s ⊔ t) = finrank K V
Tactic: apply eq_top_of_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
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K V ≤ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
hdisjoint : Disjoint s t
h_finrank_inf : finrank.{u, v} K ↥(s ⊓ t) = 0
⊢ finrank.{u, v} K ↥(s ⊔ t) = finrank K V
have hdim₁ : finrank K V = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
Tactic: replace hdim : finrank K V = finrank K s + finrank K t :=
    le_antisymm hdim (finrank_add_finrank_le_of_disjoint hdisjoint)
Cleared hypotheses: hdim