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
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
ι : Type u_1
inst_5 : Unique ι
h_1 : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h_1
h : Ne.{u + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) (0 : K)
w : V
apply_fun :
  Eq.{u + 1} (α := K)
    ((Finsupp.uniqueEquiv default : (a : ι →₀ K) → K)
        ((b.repr : (a : V) → ι →₀ K)
          ((fun (f : ι →₀ K) ↦ HSMul.hSMul.{u, v, v} (α := K) ((f : (a : ι) → K) default : K) v)
            ((fun (w : V) ↦
                (Finsupp.single default
                    (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default : K)
                      ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) :
                  ι →₀ K))
              w))) :
      K)
    ((Finsupp.uniqueEquiv default : (a : ι →₀ K) → K) ((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : K)
⊢ Eq (α := ι →₀ K)
    ((b.repr : (a : V) → ι →₀ K)
        ((fun (f : ι →₀ K) ↦ HSMul.hSMul.{u, v, v} (α := K) ((f : (a : ι) → K) default : K) v)
          ((fun (w : V) ↦
              (Finsupp.single default
                  (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default : K)
                    ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) :
                ι →₀ K))
            w)) :
      ι →₀ K)
    ((b.repr : (a : V) → ι →₀ K) w : ι →₀ K)

Tactic:
apply_fun Finsupp.uniqueEquiv default

Premises used: Inhabited.default, Finsupp.uniqueEquiv
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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 : Unique ι
h_1 : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h_1
h : Ne.{u + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) (0 : K)
w : V
simp :
  HMul.hMul (α := K) (β := K)
      ((RingHom.id K : (a : K) → K)
          (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default : K)
            ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) :
        K)
      ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) =
    (((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default
⊢ Eq.{u + 1} (α := K)
    ((Finsupp.uniqueEquiv default : (a : ι →₀ K) → K)
        ((b.repr : (a : V) → ι →₀ K)
          ((fun (f : ι →₀ K) ↦ HSMul.hSMul.{u, v, v} (α := K) ((f : (a : ι) → K) default : K) v)
            ((fun (w : V) ↦
                (Finsupp.single default
                    (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default : K)
                      ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) :
                  ι →₀ K))
              w))) :
      K)
    ((Finsupp.uniqueEquiv default : (a : ι →₀ K) → K) ((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : K)

Tactic:
simp only [map_smulₛₗ, Finsupp.coe_smul, Finsupp.single_eq_same,
          smul_eq_mul, Pi.smul_apply, Finsupp.uniqueEquiv_apply]

Premises used: Finsupp.single_eq_same, MulActionSemiHomClass.map_smulₛₗ, Finsupp.coe_smul, Finsupp.uniqueEquiv_apply, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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 : Unique ι
h_1 : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h_1
h : Ne.{u + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) (0 : K)
w : V
⊢ HMul.hMul (α := K) (β := K)
      ((RingHom.id K : (a : K) → K)
          (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default : K)
            ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) :
        K)
      ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) =
    (((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default

Tactic:
div_mul_cancel₀ _ h

Premises used: div_mul_cancel₀
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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 : Unique ι
h_1 : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h_1
h : Ne.{u + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) (0 : K)
w : V
⊢ HMul.hMul (α := K) (β := K)
      ((RingHom.id K : (a : K) → K)
          (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default : K)
            ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) :
        K)
      ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) =
    (((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default

Tactic:
exact div_mul_cancel₀ _ h

Premises used: div_mul_cancel₀
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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 : Unique ι
h_1 : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h_1
h : Ne.{u + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) (0 : K)
f : ι →₀ K
h₁ :
  Eq.{u + 1} (α := K)
    (((fun (w : V) ↦
              (Finsupp.single default
                  (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default : K)
                    ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) :
                ι →₀ K))
            ((fun (f : ι →₀ K) ↦ HSMul.hSMul.{u, v, v} (α := K) ((f : (a : ι) → K) default : K) v) f) :
          (a : ι) → K)
        default :
      K)
    ((f : (a : ι) → K) default : K)
⊢ (fun (w : V) ↦
        (Finsupp.single default
            (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default : K)
              ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) :
          ι →₀ K))
      ((fun (f : ι →₀ K) ↦ HSMul.hSMul.{u, v, v} (α := K) ((f : (a : ι) → K) default : K) v) f) =
    f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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 : Unique ι
h_1 : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h_1
h : Ne.{u + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) (0 : K)
f : ι →₀ K
h₁ :
  HDiv.hDiv (β := K)
      (HMul.hMul (α := K) (β := K) ((f : (a : ι) → K) default : K)
        ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K))
      ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) =
    (f : (a : ι) → K) default
⊢ Eq.{u + 1} (α := K)
    (((fun (w : V) ↦
              (Finsupp.single default
                  (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default : K)
                    ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) :
                ι →₀ K))
            ((fun (f : ι →₀ K) ↦ HSMul.hSMul.{u, v, v} (α := K) ((f : (a : ι) → K) default : K) v) f) :
          (a : ι) → K)
        default :
      K)
    ((f : (a : ι) → K) default : K)

Tactic:
simp only [map_smulₛₗ, Finsupp.coe_smul, Finsupp.single_eq_same,
          RingHom.id_apply, smul_eq_mul, Pi.smul_apply]

Premises used: Finsupp.single_eq_same, RingHom.id_apply, MulActionSemiHomClass.map_smulₛₗ, Finsupp.coe_smul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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 : Unique ι
h_1 : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h_1
h : Ne.{u + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) (0 : K)
f : ι →₀ K
⊢ HDiv.hDiv (β := K)
      (HMul.hMul (α := K) (β := K) ((f : (a : ι) → K) default : K)
        ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K))
      ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) =
    (f : (a : ι) → K) default

Tactic:
mul_div_cancel_right₀ _ h

Premises used: mul_div_cancel_right₀
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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 : Unique ι
h_1 : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h_1
h : Ne.{u + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) (0 : K)
f : ι →₀ K
⊢ HDiv.hDiv (β := K)
      (HMul.hMul (α := K) (β := K) ((f : (a : ι) → K) default : K)
        ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K))
      ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) =
    (f : (a : ι) → K) default

Tactic:
exact mul_div_cancel_right₀ _ h

Premises used: mul_div_cancel_right₀
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Unique ι
h : finrank K V = 1
v : V
hv : v ≠ 0
i : ι
refl : (basisSingleton ι h v hv : (a : ι) → V) default = v
⊢ (basisSingleton ι h v hv : (a : ι) → V) i = v

Tactic:
cases Unique.uniq ‹Unique ι› i

Premises used: Unique.uniq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Unique ι
h : finrank K V = 1
v : V
hv : v ≠ 0
⊢ (basisSingleton ι h v hv : (a : ι) → V) default = v

Tactic:
simp [basisSingleton]

Premises used: FiniteDimensional.basisSingleton
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Unique ι
h : finrank K V = 1
v : V
hv : v ≠ 0
rw : Eq (α := Set V) (singleton (α := V) ((basisSingleton ι h v hv : (a : ι) → V) default : V)) {v}
rw₁ rw₂ : Eq (α := Set V) {v} {v}
⊢ Eq (α := Set V) (Set.range.{v, u_1 + 1} (ι := ι) (⇑(basisSingleton ι h v hv) : (a : ι) → V)) {v}

Tactic:
rw [Set.range_unique, basisSingleton_apply]

Premises used: FiniteDimensional.basisSingleton_apply, Set.range_unique
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : ℕ
h : Module.rank K V = (↑n : Cardinal.{v})
⊢ FiniteDimensional K V

Tactic:
Module.finite_of_rank_eq_nat h

Premises used: Module.finite_of_rank_eq_nat
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : Module.rank K V = 0
⊢ FiniteDimensional K V

Tactic:
Module.finite_of_rank_eq_zero h

Premises used: Module.finite_of_rank_eq_zero
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : Module.rank K V = 1
⊢ FiniteDimensional K V

Tactic:
Module.finite_of_rank_eq_one h

Premises used: Module.finite_of_rank_eq_one
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ Module.rank 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
S₁ S₂ : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥S₂
h : S₁ ≤ S₂
⊢ FiniteDimensional.{u, v} K ↥S₁

Tactic:
(isNoetherian_of_le h).finite

Premises used: Module.IsNoetherian.finite
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S₁ S₂ : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥S₁
⊢ FiniteDimensional.{u, v} K ↥(S₁ ⊓ S₂)

Tactic:
finiteDimensional_of_le inf_le_left

Premises used: inf_le_left, Submodule.finiteDimensional_of_le
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S₁ S₂ : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥S₂
⊢ FiniteDimensional.{u, v} K ↥(S₁ ⊓ S₂)

Tactic:
finiteDimensional_of_le inf_le_right

Premises used: inf_le_right, Submodule.finiteDimensional_of_le
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S₁ S₂ : Submodule K V
h₁ : FiniteDimensional.{u, v} K ↥S₁
h₂ : FiniteDimensional.{u, v} K ↥S₂
⊢ FiniteDimensional.{u, v} K ↥(S₁ ⊔ S₂)

Tactic:
finite_sup _ _

Premises used: Set.Mem, setOf, Submodule.finite_sup
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
s : Finset ι
S : ι → Submodule K V
inst_3 : ∀ (i : ι), FiniteDimensional.{u, v} K ↥(S i)
⊢ FiniteDimensional.{u, v} K ↥(s.sup S)

Tactic:
Submodule.finite_finset_sup _ _

Premises used: Set.Mem, setOf, Submodule.finite_finset_sup
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Sort u_1
inst_3 : Finite ι
S : ι → Submodule K V
inst_4 : ∀ (i : ι), FiniteDimensional.{u, v} K ↥(S i)
⊢ FiniteDimensional.{u, v} K ↥(⨆ (i : ι), S i)

Tactic:
Submodule.finite_iSup _

Premises used: Set.Mem, setOf, Submodule.finite_iSup
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Finite ι
inst_4 : FiniteDimensional K V
⊢ FiniteDimensional K (ι →₀ V)

Tactic:
Module.Finite.finsupp

Premises used: Module.Finite.finsupp
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S₁ S₂ : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥S₂
hle : S₁ ≤ S₂
hd : finrank.{u, v} K ↥S₂ ≤ finrank.{u, v} K ↥S₁
⊢ finrank.{u, v} K ↥S₂ ≤ finrank.{u, v} K ↥(comap S₂.subtype S₁)

Tactic:
rw [← LinearEquiv.finrank_eq (Submodule.comapSubtypeEquivOfLe hle)] at hd

Premises used: LinearEquiv.finrank_eq, Submodule.comapSubtypeEquivOfLe
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S₁ S₂ : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥S₂
hle : S₁ ≤ S₂
hd : finrank.{u, v} K ↥S₂ ≤ finrank.{u, v} K ↥(comap S₂.subtype S₁)
⊢ S₁ = S₂

Tactic:
le_antisymm hle (Submodule.comap_subtype_eq_top.1
    (eq_top_of_finrank_eq (le_antisymm (comap (Submodule.subtype S₂) S₁).finrank_le hd)))

Premises used: Submodule.comap_subtype_eq_top, le_antisymm, Submodule.comap, Iff.mp, Submodule.subtype, Submodule.finrank_le, Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S₁ S₂ : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥S₂
hle : S₁ ≤ S₂
hd : finrank.{u, v} K ↥S₂ ≤ finrank.{u, v} K ↥(comap S₂.subtype S₁)
⊢ S₁ = S₂

Tactic:
exact le_antisymm hle (Submodule.comap_subtype_eq_top.1
    (eq_top_of_finrank_eq (le_antisymm (comap (Submodule.subtype S₂) S₁).finrank_le hd)))

Premises used: Submodule.comap_subtype_eq_top, le_antisymm, Submodule.comap, Iff.mp, Submodule.subtype, Submodule.finrank_le, Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S₁ S₂ : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥S₂
hle : S₁ ≤ S₂
hd : finrank.{u, v} K ↥S₁ = finrank.{u, v} K ↥S₂
⊢ S₁ = S₂

Tactic:
eq_of_le_of_finrank_le hle hd.ge

Premises used: Eq.ge, Submodule.eq_of_le_of_finrank_le
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Ring L
inst_2 : Algebra K L
F E : Subalgebra K L
hfin : FiniteDimensional.{u_1, u_2} K ↥E
h_le : F ≤ E
h_finrank : finrank.{u_1, u_2} K ↥E ≤ finrank.{u_1, u_2} K ↥F
⊢ F = E

Tactic:
haveI : Module.Finite K (Subalgebra.toSubmodule E) := hfin
  toSubmodule_injective <| Submodule.eq_of_le_of_finrank_le h_le h_finrank

Premises used: Subalgebra.toSubmodule_injective, Submodule.eq_of_le_of_finrank_le
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Ring L
inst_2 : Algebra K L
F E : Subalgebra K L
hfin : FiniteDimensional.{u_1, u_2} K ↥E
h_le : F ≤ E
h_finrank : finrank.{u_1, u_2} K ↥F = finrank.{u_1, u_2} K ↥E
⊢ F = E

Tactic:
eq_of_le_of_finrank_le h_le h_finrank.ge

Premises used: Eq.ge, Subalgebra.eq_of_le_of_finrank_le
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
hinj : Injective (α := V) (β := V) (⇑f : (a : V) → V)
⊢ Module.rank K ↥f.range = Module.rank K V

Tactic:
have h := rank_range_of_injective _ hinj
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
hinj : Injective (α := V) (β := V) (⇑f : (a : V) → V)
h : Module.rank K ↥f.range = Module.rank K V
⊢ finrank.{u, v} K ↥f.range = finrank K V

Tactic:
rw [← finrank_eq_rank, ← finrank_eq_rank, Nat.cast_inj] at h

Premises used: Nat.cast_inj, Module.finrank_eq_rank
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
hinj : Injective (α := V) (β := V) (⇑f : (a : V) → V)
h : finrank.{u, v} K ↥f.range = finrank K V
⊢ Surjective (α := V) (β := V) (⇑f : (a : V) → V)

Tactic:
range_eq_top.1 (eq_top_of_finrank_eq h)

Premises used: LinearMap.range_eq_top, Iff.mp, Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
hinj : Injective (α := V) (β := V) (⇑f : (a : V) → V)
h : finrank.{u, v} K ↥f.range = finrank K V
⊢ Surjective (α := V) (β := V) (⇑f : (a : V) → V)

Tactic:
exact range_eq_top.1 (eq_top_of_finrank_eq h)

Premises used: LinearMap.range_eq_top, Iff.mp, Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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₂
hf : f.range = ⊤
⊢ FiniteDimensional K V₂

Tactic:
Module.Finite.of_surjective f <| range_eq_top.1 hf

Premises used: Module.Finite.of_surjective, LinearMap.range_eq_top, Iff.mp
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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₂
⊢ FiniteDimensional.{u, v'} K ↥f.range

Tactic:
Module.Finite.range f

Premises used: Module.Finite.range
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
⊢ Injective (α := V) (β := V) (⇑f : (a : V) → V) ↔ Surjective (α := V) (β := V) (⇑f : (a : V) → V)

Tactic:
⟨surjective_of_injective, fun hsurj =>
    let ⟨g, hg⟩ := f.exists_rightInverse_of_surjective (range_eq_top.2 hsurj)
    have : Function.RightInverse g f := LinearMap.ext_iff.1 hg
    (leftInverse_of_surjective_of_rightInverse (surjective_of_injective this.injective)
        this).injective⟩

Premises used: Function.LeftInverse.injective, Iff.mpr, LinearMap.exists_rightInverse_of_surjective, LinearMap.ext_iff, LinearMap.range_eq_top, Iff.intro, Iff.mp, _private.0.LinearMap.injective_iff_surjective.match_1, LinearMap.surjective_of_injective, Function.leftInverse_of_surjective_of_rightInverse, Function.Injective, DFunLike.coe, Function.RightInverse.injective
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
rw :
  Injective.{v + 1, v + 1} (α := (↑(↑p : Set V) : Type v)) (β := V)
      ((↑p : Set V).restrict (π := fun (a : V) ↦ V) (⇑f : (a : V) → V)) ↔
    Surjective (Set.MapsTo.restrict (⇑f : (a : V) → V) (↑p : Set V) (↑p : Set V) h)
⊢ Set.InjOn (β := V) (⇑f : (a : V) → V) (↑p : Set V) ↔ Set.SurjOn (⇑f : (a : V) → V) (↑p : Set V) (↑p : Set V)

Tactic:
rw [Set.injOn_iff_injective, ← Set.MapsTo.restrict_surjective_iff h]

Premises used: Set.injOn_iff_injective, Set.MapsTo.restrict_surjective_iff
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
change :
  Injective (α := ↥p) (β := V) (⇑(f.domRestrict p) : (a : ↥p) → V) ↔
    Surjective (α := ↥p) (β := ↥p) (⇑(f.restrict h) : (a : ↥p) → ↥p)
⊢ Injective.{v + 1, v + 1} (α := (↑(↑p : Set V) : Type v)) (β := V)
      ((↑p : Set V).restrict (π := fun (a : V) ↦ V) (⇑f : (a : V) → V)) ↔
    Surjective (Set.MapsTo.restrict (⇑f : (a : V) → V) (↑p : Set V) (↑p : Set V) h)

Tactic:
change Injective (f.domRestrict p) ↔ Surjective (f.restrict h)

Premises used: LinearMap.restrict, LinearMap.domRestrict, Function.Injective, DFunLike.coe, Function.Surjective
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
⊢ Injective (α := ↥p) (β := V) (⇑(f.domRestrict p) : (a : ↥p) → V) ↔
    Surjective (α := ↥p) (β := ↥p) (⇑(f.restrict h) : (a : ↥p) → ↥p)

Tactic:
simp [disjoint_iff, ← injective_iff_surjective]

Premises used: disjoint_iff, LinearMap.injective_iff_surjective
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
rw : f.ker = ⊥ ↔ Surjective (α := V) (β := V) (⇑f : (a : V) → V)
rw₁ : Injective (α := V) (β := V) (⇑f : (a : V) → V) ↔ Surjective (α := V) (β := V) (⇑f : (a : V) → V)
rw₂ rw₃ : Surjective (α := V) (β := V) (⇑f : (a : V) → V) ↔ Surjective (α := V) (β := V) (⇑f : (a : V) → V)
⊢ f.ker = ⊥ ↔ f.range = ⊤

Tactic:
rw [range_eq_top, ker_eq_bot, injective_iff_surjective]

Premises used: LinearMap.ker_eq_bot, LinearMap.injective_iff_surjective, LinearMap.range_eq_top
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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₂
⊢ IsStablyFiniteRing K

Tactic:
isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd.mpr fun n ↦ ⟨fun {f g} hfg ↦ ?_⟩

Premises used: Iff.mpr, IsDedekindFiniteMonoid.mk, isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd