awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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
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)
⊢ ∃ (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

Tactic:
obtain ⟨c, rfl⟩ := (finrank_eq_one_iff_of_nonzero' (f v) n).mp h z

Premises used: Iff.mp, DFunLike.coe, finrank_eq_one_iff_of_nonzero', rfl
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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)
c : K
⊢ ((↑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)
      (c • v) =
    HSMul.hSMul (β := W) c ((f : (a : V) → W) v : W)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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)
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:
exact ⟨c • v, by simp⟩
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
S : Subalgebra F E
⊢ FiniteDimensional.{u_1, u_2} F ↥((toSubmodule : (a : Subalgebra F E) → Submodule F E) S : Submodule F E) ↔
    FiniteDimensional.{u_1, u_2} F ↥S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
S : Subalgebra F E
⊢ FiniteDimensional.{u_1, u_2} F ↥S

Tactic:
FiniteDimensional.of_subalgebra_toSubmodule inferInstance

Premises used: inferInstance, FiniteDimensional.of_subalgebra_toSubmodule
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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)
⊢ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + 0))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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)))
a₁ : LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
⊢ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + (m + 1)))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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 ^ (m + 1) * f ^ k)
⊢ LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (k + (m + 1)))

Tactic:
rw [add_comm, pow_add]

Premises used: pow_add, add_comm
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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 ^ (m + 1) * f ^ k)

Tactic:
apply LinearMap.ker_le_ker_comp

Premises used: LinearMap.ker_le_ker_comp
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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))
a₉ : comap (f ^ m) (LinearMap.ker (f ^ (k + 1))) ≤ comap (f ^ m) (LinearMap.ker (f ^ k.succ))
a₁₀ a₁₁ : comap (f ^ m) (LinearMap.ker (f ^ k.succ)) ≤ comap (f ^ m) (LinearMap.ker (f ^ k.succ))
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ 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]

Premises used: Module.End.mul_eq_comp, add_assoc, pow_add, LinearMap.ker_comp, add_comm, Nat.add_one, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
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₂
f : V →ₗ[K] V₂
w : Function.Injective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)
inst_5 : FiniteDimensional K V₂
⊢ FiniteDimensional K V

Tactic:
Module.Finite.of_injective f w

Premises used: Module.Finite.of_injective
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
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₂
f : V →ₗ[K] V₂
w : Function.Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)
inst_5 : FiniteDimensional K V
⊢ FiniteDimensional K V₂

Tactic:
Module.Finite.of_surjective f w

Premises used: Module.Finite.of_surjective
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
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₂
ι : Type u_1
inst_5 : Finite ι
⊢ FiniteDimensional K (ι → K)

Tactic:
Finite.pi

Premises used: Module.Finite.pi
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
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₂
ι : Type u_1
inst_5 : Finite ι
M : ι → Type u_2
inst_6 : (i : ι) → AddCommGroup (M i)
inst_7 : (i : ι) → Module.{u, u_2} K (M i)
inst_8 : ∀ (i : ι), FiniteDimensional.{u, u_2} K (M i)
⊢ FiniteDimensional K ((i : ι) → M i)

Tactic:
Finite.pi

Premises used: Module.Finite.pi
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type w
inst_3 : Finite ι
h : Basis ι K V
⊢ FiniteDimensional K V

Tactic:
Module.Finite.of_basis h

Premises used: Module.Finite.of_basis
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type w
s : Set ι
h : Basis.{w, u, v} (↑s : Type w) K V
hs : s.Finite
⊢ FiniteDimensional K V

Tactic:
haveI := hs.fintype
  h.finiteDimensional_of_finite

Premises used: Module.Basis.finiteDimensional_of_finite
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
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
S : Submodule K V
⊢ FiniteDimensional.{u, v} K ↥S

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
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
S : Submodule K V
⊢ FiniteDimensional.{u, v} K (V ⧸ S)

Tactic:
Module.Finite.quotient K S

Premises used: Module.Finite.quotient
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : 0 < finrank K V
⊢ FiniteDimensional K V

Tactic:
Module.finite_of_finrank_pos h

Premises used: Module.finite_of_finrank_pos
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : ℕ
hn : finrank K V = n.succ
⊢ FiniteDimensional K V

Tactic:
Module.finite_of_finrank_eq_succ hn

Premises used: Module.finite_of_finrank_eq_succ
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : ℕ
hn : Fact (finrank K V = n + 1)
⊢ FiniteDimensional K V

Tactic:
of_finrank_eq_succ hn.out

Premises used: FiniteDimensional.of_finrank_eq_succ, Fact.out
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fact (finrank K V = 2)
⊢ FiniteDimensional K V

Tactic:
of_fact_finrank_eq_succ 1

Premises used: FiniteDimensional.of_fact_finrank_eq_succ, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
⊢ (↑(finrank K V) : Cardinal.{v}) = Module.rank K V

Tactic:
finrank_eq_rank _ _

Premises used: Module.finrank_eq_rank
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ¬FiniteDimensional K V
⊢ finrank K V = 0

Tactic:
Module.finrank_of_not_finite h

Premises used: Module.finrank_of_not_finite
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Type v
inst_3 : AddCommGroup W
inst_4 : Module K W
n : ℕ
hn : n ≠ 0
hVW : Module.rank K V = n • Module.rank K W
⊢ FiniteDimensional K V ↔ FiniteDimensional K W

Tactic:
Module.finite_iff_of_rank_eq_nsmul hn hVW

Premises used: Module.finite_iff_of_rank_eq_nsmul
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type w
h : Basis ι K V
⊢ (↑(finrank K V) : Cardinal.{w}) = #ι

Tactic:
Module.mk_finrank_eq_card_basis h

Premises used: Module.mk_finrank_eq_card_basis
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
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₂
⊢ FiniteDimensional K K

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Set V
hA : A.Finite
⊢ FiniteDimensional.{u, v} K ↥(span K A)

Tactic:
Module.Finite.span_of_finite K hA

Premises used: Module.Finite.span_of_finite
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
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₂
x : V
⊢ FiniteDimensional.{u, v} K ↥(K ∙ x)

Tactic:
Module.Finite.span_singleton K x

Premises used: Module.Finite.span_singleton
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
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₂
s : Finset V
⊢ FiniteDimensional.{u, v} K ↥(span K (↑s : Set V))

Tactic:
Module.Finite.span_finset K s

Premises used: Module.Finite.span_finset
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
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₂
f : V →ₗ[K] V₂
p : Submodule K V
inst_5 : FiniteDimensional.{u, v} K ↥p
⊢ FiniteDimensional.{u, v'} K ↥(Submodule.map f p)

Tactic:
Module.Finite.map _ _

Premises used: Module.Finite.map
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
Goal:
F : Type u_1
K : Type u_2
A : Type u_3
inst : DivisionRing F
inst_1 : DivisionRing K
inst_2 : AddCommGroup A
inst_3 : Module F K
inst_4 : Module K A
inst_5 : Module F A
inst_6 : IsScalarTower F K A
inst_7 : FiniteDimensional F K
inst_8 : FiniteDimensional K A
⊢ FiniteDimensional F A

Tactic:
Module.Finite.trans K A

Premises used: Module.Finite.trans
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
⊢ s.FG ↔ FiniteDimensional.{u, v} K ↥s

Tactic:
Module.Finite.iff_fg.symm

Premises used: Module.Finite.iff_fg, Iff.symm
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Defs
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₂
f : V ≃ₗ[K] V₂
inst_5 : FiniteDimensional K V
⊢ FiniteDimensional K V₂

Tactic:
Module.Finite.equiv f

Premises used: Module.Finite.equiv
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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 ≠ ⊤
rw : finrank.{u, v} K ↥s < finrank.{u, v} K ↥s + finrank.{u, v} K (V ⧸ s)
⊢ finrank.{u, v} K ↥s < finrank K V

Tactic:
rw [← s.finrank_quotient_add_finrank, add_comm]

Premises used: Submodule.finrank_quotient_add_finrank, add_comm
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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 ≠ ⊤
⊢ Nontrivial.{v} (V ⧸ s)

Tactic:
rw [← Quotient.nontrivial_iff] at h

Premises used: Submodule.Quotient.nontrivial_iff
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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 : Nontrivial.{v} (V ⧸ s)
⊢ finrank.{u, v} K ↥s < finrank.{u, v} K ↥s + finrank.{u, v} K (V ⧸ s)

Tactic:
Nat.lt_add_of_pos_right finrank_pos

Premises used: Set.Mem, Nat.lt_add_of_pos_right, Module.finrank_pos
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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 : Nontrivial.{v} (V ⧸ s)
⊢ finrank.{u, v} K ↥s < finrank.{u, v} K ↥s + finrank.{u, v} K (V ⧸ s)

Tactic:
exact Nat.lt_add_of_pos_right finrank_pos

Premises used: Nat.lt_add_of_pos_right, Module.finrank_pos
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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)) : Cardinal.{v}) + Module.rank K ↥(s ⊓ t) = Module.rank K ↥s + Module.rank K ↥t

Tactic:
rw [← finrank_eq_rank] at key

Premises used: Module.finrank_eq_rank
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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
⊢ 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

Premises used: Module.finrank_eq_rank
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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
⊢ 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

Premises used: Module.finrank_eq_rank
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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
⊢ 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

Premises used: Module.finrank_eq_rank
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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
⊢ 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

Premises used: Module.finrank_eq_rank
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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})
norm_cast norm_cast₁ norm_cast₂ 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
⊢ 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
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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
rw : finrank.{u, v} K ↥(s ⊔ t) ≤ finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t)
⊢ finrank.{u, v} K ↥(s ⊔ t) ≤ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t

Tactic:
rw [← finrank_sup_add_finrank_inf_eq]

Premises used: Submodule.finrank_sup_add_finrank_inf_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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 ⊓ t)

Tactic:
self_le_add_right _ _

Premises used: self_le_add_right
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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 ⊓ t)

Tactic:
exact self_le_add_right _ _

Premises used: self_le_add_right