awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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₂
suffices : 0 < finrank.{u, v} K ↥f.ker
⊢ f.ker ≠ ⊥

Tactic:
suffices 0 < finrank K (LinearMap.ker f) from Submodule.one_le_finrank_iff.mp this
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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₂
⊢ 0 < finrank.{u, v} K ↥f.ker

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
⊢ finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V

Tactic:
have := finrank_range_add_finrank_ker f
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
rw : f.ker = ⊥ ↔ f.range = ⊤
⊢ Injective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂) ↔
    Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)

Tactic:
rw [← ker_eq_bot, ← range_eq_top]

Premises used: LinearMap.ker_eq_bot, LinearMap.range_eq_top
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
⊢ f.ker = ⊥ ↔ f.range = ⊤

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
refine_1 : ∀ (h : f.ker = ⊥), f.range = ⊤
refine_2 : ∀ (h : f.range = ⊤), f.ker = ⊥
⊢ f.ker = ⊥ ↔ f.range = ⊤

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
h : f.ker = ⊥
⊢ finrank.{u, v'} K ↥f.range = finrank K V₂

Tactic:
rw [h, finrank_bot, add_zero, H] at this

Premises used: finrank_bot, add_zero
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
h : f.ker = ⊥
this₁ : finrank.{u, v'} K ↥f.range = finrank K V₂
⊢ f.ker = ⊥

Tactic:
rw [h, finrank_bot, add_zero, H] at this

Premises used: finrank_bot, add_zero
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank.{u, v'} K ↥f.range = finrank K V₂
h : f.ker = ⊥
⊢ f.range = ⊤

Tactic:
eq_top_of_finrank_eq this

Premises used: Submodule.eq_top_of_finrank_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
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank.{u, v'} K ↥f.range = finrank K V₂
h : f.ker = ⊥
⊢ f.range = ⊤

Tactic:
exact eq_top_of_finrank_eq this

Premises used: Submodule.eq_top_of_finrank_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
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
h : f.range = ⊤
⊢ finrank K V₂ + finrank.{u, v} K ↥f.ker = finrank K V₂

Tactic:
rw [h, finrank_top, H] at this

Premises used: finrank_top
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V
h : f.range = ⊤
this₁ : finrank K V₂ + finrank.{u, v} K ↥f.ker = finrank K V₂
⊢ f.range = ⊤

Tactic:
rw [h, finrank_top, H] at this

Premises used: finrank_top
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank K V₂ + finrank.{u, v} K ↥f.ker = finrank K V₂
h : f.range = ⊤
⊢ f.ker = ⊥

Tactic:
Submodule.finrank_eq_zero.1 (add_right_injective _ this)

Premises used: add_right_injective, Submodule.finrank_eq_zero, Iff.mp
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank K V₂ + finrank.{u, v} K ↥f.ker = finrank K V₂
h : f.range = ⊤
⊢ f.ker = ⊥

Tactic:
exact Submodule.finrank_eq_zero.1 (add_right_injective _ this)

Premises used: add_right_injective, Submodule.finrank_eq_zero, Iff.mp
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
rw : f.ker = ⊥ ↔ Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)
rw₁ :
  Injective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂) ↔
    Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)
rw₂ rw₃ :
  Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂) ↔
    Surjective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)
⊢ f.ker = ⊥ ↔ f.range = ⊤

Tactic:
rw [range_eq_top, ker_eq_bot, injective_iff_surjective_of_finrank_eq_finrank H]

Premises used: LinearMap.injective_iff_surjective_of_finrank_eq_finrank, LinearMap.ker_eq_bot, LinearMap.range_eq_top
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
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₂
hf : Injective.{v + 1, v' + 1} (α := V) (β := V₂) (⇑f : (a : V) → V₂)
hdim : finrank K V = finrank K V₂
x : V
⊢ Eq.{v' + 1} (α := V₂) ((f.linearEquivOfInjective hf hdim : (a : V) → V₂) x : V₂) ((f : (a : V) → V₂) x : V₂)

Tactic:
rfl

Premises used: rfl
-- 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 ↥t
hst : s < t
⊢ comap t.subtype s ≠ ⊤

Tactic:
simp [not_le_of_gt hst]

Premises used: not_le_of_gt
-- 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
⊢ StrictMono (β := ℕ) fun (s : Submodule K V) ↦ finrank.{u, v} K ↥s

Tactic:
fun _ _ => finrank_lt_finrank_of_lt

Premises used: StrictMono, Submodule.finrank_lt_finrank_of_lt
-- 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
U W : Submodule K V
h : IsCompl U W
rw : finrank.{u, v} K ↥⊤ = finrank K V
⊢ finrank.{u, v} K ↥U + finrank.{u, v} K ↥W = finrank K V

Tactic:
rw [← finrank_sup_add_finrank_inf_eq, h.codisjoint.eq_top, h.disjoint.eq_bot, finrank_bot,
    add_zero]

Premises used: Submodule.finrank_sup_add_finrank_inf_eq, finrank_bot, IsCompl.codisjoint, add_zero, IsCompl.disjoint, Disjoint.eq_bot, Codisjoint.eq_top
-- 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
U W : Submodule K V
h : IsCompl U W
⊢ finrank.{u, v} K ↥⊤ = finrank K V

Tactic:
finrank_top _ _

Premises used: Set.Mem, finrank_top
-- 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
U W : Submodule K V
h : IsCompl U W
⊢ finrank.{u, v} K ↥⊤ = finrank K V

Tactic:
exact finrank_top _ _

Premises used: finrank_top
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Fintype ι
inst_4 : FiniteDimensional K V
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
by_contra : ∀ (ne_top : ¬Eq (α := Submodule K V) (span K (Set.range b)) ⊤), False
⊢ Eq (α := Submodule K V) (span K (Set.range b)) ⊤

Tactic:
by_contra ne_top
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Fintype ι
inst_4 : FiniteDimensional K V
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
ne_top : ¬Eq (α := Submodule K V) (span K (Set.range b)) ⊤
⊢ finrank.{u, v} K ↥(span K (Set.range b)) = finrank K V

Tactic:
rw [← finrank_span_eq_card lin_ind] at card_eq

Premises used: finrank_span_eq_card
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Fintype ι
inst_4 : FiniteDimensional K V
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
ne_top : ¬Eq (α := Submodule K V) (span K (Set.range b)) ⊤
card_eq₁ : finrank.{u, v} K ↥(span K (Set.range b)) = finrank K V
⊢ ¬Eq (α := Submodule K V) (span K (Set.range b)) ⊤

Tactic:
rw [← finrank_span_eq_card lin_ind] at card_eq

Premises used: finrank_span_eq_card
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Fintype ι
inst_4 : FiniteDimensional K V
b : ι → V
lin_ind : LinearIndependent K b
card_eq : finrank.{u, v} K ↥(span K (Set.range b)) = finrank K V
ne_top : ¬Eq (α := Submodule K V) (span K (Set.range b)) ⊤
⊢ False

Tactic:
ne_of_lt (Submodule.finrank_lt ne_top) card_eq

Premises used: Submodule.finrank_lt, ne_of_lt
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Fintype ι
inst_4 : FiniteDimensional K V
b : ι → V
lin_ind : LinearIndependent K b
card_eq : finrank.{u, v} K ↥(span K (Set.range b)) = finrank K V
ne_top : ¬Eq (α := Submodule K V) (span K (Set.range b)) ⊤
⊢ False

Tactic:
exact ne_of_lt (Submodule.finrank_lt ne_top) card_eq

Premises used: Submodule.finrank_lt, ne_of_lt
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Fintype ι
inst_4 : Nonempty ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
⊢ Eq (α := Submodule K V) (span K (Set.range b)) ⊤

Tactic:
have : FiniteDimensional K V := .of_finrank_pos <| card_eq ▸ Fintype.card_pos
  lin_ind.span_eq_top_of_card_eq_finrank' card_eq

Premises used: FiniteDimensional.of_finrank_pos, LinearIndependent.span_eq_top_of_card_eq_finrank', Eq.rec, Fintype.card_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
ι : Type u_1
inst_3 : Fintype ι
inst_4 : FiniteDimensional K V
b : ι → V
hb : LinearIndependent K b
hι : Fintype.card ι = finrank K V
⊢ (⇑(basisOfLinearIndependentOfCardEqFinrank' b hb hι) : (a : ι) → V) = b

Tactic:
Basis.coe_mk ..

Premises used: Module.Basis.coe_mk
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Fintype ι
inst_4 : Nonempty ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
⊢ (⇑(basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) : (a : ι) → V) = b

Tactic:
Basis.coe_mk ..

Premises used: Module.Basis.coe_mk
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
inst : DivisionRing K
ι : Type u_1
inst_1 : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : Nonempty ι
⊢ (⇑(basisOfPiSpaceOfLinearIndependent hb) : (a : ι) → ι → K) = b

Tactic:
simp [hι, basisOfPiSpaceOfLinearIndependent]

Premises used: basisOfPiSpaceOfLinearIndependent
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
inst : DivisionRing K
ι : Type u_1
inst_1 : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : ¬Nonempty ι
neg :
  (⇑(have this := ⋯;
        Basis.empty (ι → K)) :
      (a : ι) → ι → K) =
    b
⊢ (⇑(basisOfPiSpaceOfLinearIndependent hb) : (a : ι) → ι → K) = b

Tactic:
rw [basisOfPiSpaceOfLinearIndependent, dif_neg hι]

Premises used: dif_neg, basisOfPiSpaceOfLinearIndependent
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
inst : DivisionRing K
ι : Type u_1
inst_1 : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : ¬Nonempty ι
neg :
  ∀ (i x : ι),
    (have this := ⋯;
          Basis.empty (ι → K) :
          (a : ι) → ι → K)
        i x =
      b i x
⊢ (⇑(have this := ⋯;
        Basis.empty (ι → K)) :
      (a : ι) → ι → K) =
    b

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
inst : DivisionRing K
ι : Type u_1
inst_1 : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : ¬Nonempty ι
i x : ι
⊢ (have this := ⋯;
        Basis.empty (ι → K) :
        (a : ι) → ι → K)
      i x =
    b i x

Tactic:
((not_nonempty_iff.mp hι).false i).elim

Premises used: False.elim, IsEmpty.false
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
inst : DivisionRing K
ι : Type u_1
inst_1 : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : ¬Nonempty ι
i x : ι
⊢ (have this := ⋯;
        Basis.empty (ι → K) :
        (a : ι) → ι → K)
      i x =
    b i x

Tactic:
exact ((not_nonempty_iff.mp hι).false i).elim

Premises used: False.elim, IsEmpty.false
-- 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 : Finset V
hs : s.Nonempty
lin_ind : LinearIndependent.{v, u, v} (ι := ↥s) K (Subtype.val (p := fun (x : V) ↦ x ∈ s))
card_eq : s.card = finrank K V
⊢ Nonempty.{v + 1} ↥s

Tactic:
haveI : Nonempty s := ⟨⟨hs.choose, hs.choose_spec⟩⟩
-- 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 : Finset V
hs : s.Nonempty
lin_ind : LinearIndependent.{v, u, v} (ι := ↥s) K (Subtype.val (p := fun (x : V) ↦ x ∈ s))
card_eq : s.card = finrank K V
this : Nonempty.{v + 1} ↥s
⊢ Eq.{v + 1} (α := (a : ↥s) → V) (⇑(finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq) : (a : ↥s) → V)
    (Subtype.val (p := fun (x : V) ↦ x ∈ s))

Tactic:
simp [finsetBasisOfLinearIndependentOfCardEqFinrank]

Premises used: finsetBasisOfLinearIndependentOfCardEqFinrank
-- 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 : Set V
inst_3 : Nonempty.{v + 1} (↑s : Type v)
inst_4 : Fintype (↑s : Type v)
lin_ind : LinearIndependent.{v, u, v} (ι := { x : V // x ∈ s }) K (Subtype.val (p := fun (x : V) ↦ x ∈ s))
card_eq : s.toFinset.card = finrank K V
⊢ Eq.{v + 1} (α := (a : (↑s : Type v)) → V)
    (⇑(setBasisOfLinearIndependentOfCardEqFinrank (s := s) lin_ind card_eq) : (a : (↑s : Type v)) → V)
    (Subtype.val (p := fun (x : V) ↦ x ∈ s))

Tactic:
simp [setBasisOfLinearIndependentOfCardEqFinrank]

Premises used: setBasisOfLinearIndependentOfCardEqFinrank
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Type u_1
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : SMul K A
inst_6 : IsScalarTower K A V
h : finrank K V = 1
⊢ Nontrivial V

Tactic:
haveI := nontrivial_of_finrank_eq_succ h
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Type u_1
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : SMul K A
inst_6 : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
⊢ IsSimpleOrder.{v} (Submodule A V)

Tactic:
⟨fun S => or_iff_not_imp_left.2 fun hn => ?_⟩

Premises used: Iff.mpr, IsSimpleOrder.mk, Classical.or_iff_not_imp_left
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Type u_1
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : SMul K A
inst_6 : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
refine : ∀ (S : Submodule A V) (hn : ¬S = ⊥), S = ⊤
⊢ IsSimpleOrder.{v} (Submodule A V)

Tactic:
refine ⟨fun S => or_iff_not_imp_left.2 fun hn => ?_⟩
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Type u_1
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : SMul K A
inst_6 : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
S : Submodule A V
hn : ¬S = ⊥
rw :
  ∀ (hn : ¬Eq (α := Submodule K V) (restrictScalars K S) (restrictScalars.{u, u_1, v} K (R := A) ⊥)),
    Eq (α := Submodule K V) (restrictScalars K S) (restrictScalars.{u, u_1, v} K (R := A) ⊤)
⊢ S = ⊤

Tactic:
rw [← restrictScalars_inj K] at hn ⊢

Premises used: Submodule.restrictScalars_inj
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Type u_1
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : SMul K A
inst_6 : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
S : Submodule A V
hn : ¬Eq (α := Submodule K V) (restrictScalars K S) (restrictScalars.{u, u_1, v} K (R := A) ⊥)
⊢ FiniteDimensional K V

Tactic:
haveI : FiniteDimensional _ _ := .of_finrank_eq_succ h
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Type u_1
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : SMul K A
inst_6 : IsScalarTower K A V
h : finrank K V = 1
this_1 : Nontrivial V
S : Submodule A V
hn : ¬Eq (α := Submodule K V) (restrictScalars K S) (restrictScalars.{u, u_1, v} K (R := A) ⊥)
this : FiniteDimensional K V
⊢ Eq (α := Submodule K V) (restrictScalars K S) (restrictScalars.{u, u_1, v} K (R := A) ⊤)

Tactic:
eq_top_of_finrank_eq ((Submodule.finrank_le _).antisymm ?_)

Premises used: Set.univ, Submodule.restrictScalars, setOf, LE.le.antisymm, Submodule.finrank_le, Submodule.eq_top_of_finrank_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
A : Type u_1
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : SMul K A
inst_6 : IsScalarTower K A V
h : finrank K V = 1
this_1 : Nontrivial V
S : Submodule A V
hn : ¬Eq (α := Submodule K V) (restrictScalars K S) (restrictScalars.{u, u_1, v} K (R := A) ⊥)
this : FiniteDimensional K V
refine : finrank K V ≤ finrank.{u, v} K ↥(restrictScalars K S)
⊢ Eq (α := Submodule K V) (restrictScalars K S) (restrictScalars.{u, u_1, v} K (R := A) ⊤)

Tactic:
refine eq_top_of_finrank_eq ((Submodule.finrank_le _).antisymm ?_)

Premises used: LE.le.antisymm, Submodule.finrank_le, Submodule.eq_top_of_finrank_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
A : Type u_1
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : SMul K A
inst_6 : IsScalarTower K A V
h : finrank K V = 1
this_1 : Nontrivial V
S : Submodule A V
hn : ¬Eq (α := Submodule K V) (restrictScalars K S) (restrictScalars.{u, u_1, v} K (R := A) ⊥)
this : FiniteDimensional K V
⊢ finrank K V ≤ finrank.{u, v} K ↥(restrictScalars K S)

Tactic:
simpa only [h, finrank_bot] using Submodule.finrank_strictMono (Ne.bot_lt hn)

Premises used: Submodule.finrank_strictMono, finrank_bot, Ne.bot_lt
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
h : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤
⊢ False

Tactic:
cases hr.symm.trans (Subalgebra.bot_eq_top_iff_finrank_eq_one.1 h)

Premises used: Subalgebra.bot_eq_top_iff_finrank_eq_one, Iff.mp, Eq.symm, Eq.trans
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Ring E
inst_2 : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := ⋯
S : Subalgebra F E
⊢ FiniteDimensional F E

Tactic:
haveI : FiniteDimensional F E := .of_finrank_eq_succ hr