awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
S : Type u'
inst_2 : Ring S
M : Type v
N : Type v'
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[(↑e₁ : R →+* S)] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
I' : Submodule R R := Submodule.map (↑e₁.symm.toSemilinearEquiv : S →ₛₗ[(↑e₁.symm : S →+* R)] R) I
e : ↥I' ≃ₛₗ[(↑e₁ : R →+* S)] ↥I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
f : ↥I' →ₗ[R] M := (↑e₂.symm : N →ₛₗ[(↑e₁.symm : S →+* R)] M) ∘ₛₗ g ∘ₛₗ (↑e : ↥I' →ₛₗ[(↑e₁ : R →+* S)] ↥I)
hf :
  ∀ (x : R) (hx : x ∈ I'),
    Eq.{v + 1} (α := M) ((f : (a : ↥I') → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I') x hx) : M)
      ((e₂.symm : (a : N) → M)
          ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) ((e₁ : (a : R) → S) x) ⋯ : ↥I) : N) :
        M)
f' : R →ₗ[R] M
hf' :
  ∀ (x : R) (mem : x ∈ I'),
    Eq.{v + 1} (α := M) ((f' : (a : R) → M) x : M)
      ((f : (a : ↥I') → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I') x mem) : M)
⊢ ∀ (x : S) (mem : x ∈ I),
    Eq.{v' + 1} (α := N)
      (((↑e₂ : M →ₛₗ[(↑e₁ : R →+* S)] N) ∘ₛₗ f' ∘ₛₗ (↑e₁.toSemilinearEquiv.symm : S →ₛₗ[(↑e₁.symm : S →+* R)] R) :
            (a : S) → N)
          x :
        N)
      ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) x mem) : N)

Tactic:
simp_all [I']
-- Module: Mathlib.Algebra.Module.Injective
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
S : Type u'
inst_2 : Ring S
M : Type v
N : Type v'
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[(↑e₁ : R →+* S)] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
I' : Submodule R R := Submodule.map (↑e₁.symm.toSemilinearEquiv : S →ₛₗ[(↑e₁.symm : S →+* R)] R) I
e : ↥I' ≃ₛₗ[(↑e₁ : R →+* S)] ↥I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
f : ↥I' →ₗ[R] M := (↑e₂.symm : N →ₛₗ[(↑e₁.symm : S →+* R)] M) ∘ₛₗ g ∘ₛₗ (↑e : ↥I' →ₛₗ[(↑e₁ : R →+* S)] ↥I)
hf :
  ∀ (x : R) (hx : x ∈ I'),
    Eq.{v + 1} (α := M) ((f : (a : ↥I') → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I') x hx) : M)
      ((e₂.symm : (a : N) → M)
          ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) ((e₁ : (a : R) → S) x) ⋯ : ↥I) : N) :
        M)
f' : R →ₗ[R] M
hf' :
  ∀ (x : R) (mem : x ∈ I'),
    Eq.{v + 1} (α := M) ((f' : (a : R) → M) x : M)
      ((f : (a : ↥I') → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I') x mem) : M)
⊢ ∃ (g' : S →ₗ[S] N),
    ∀ (x : S) (mem : x ∈ I),
      Eq.{v' + 1} (α := N) ((g' : (a : S) → N) x : N)
        ((g : (a : ↥I) → N) (Subtype.mk (p := fun (x : S) ↦ x ∈ I) x mem) : N)

Tactic:
exact ⟨e₂.toLinearMap ∘ₛₗ f' ∘ₛₗ e₁.toSemilinearEquiv.symm.toLinearMap, by simp_all [I']⟩
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
rw : M.FG
⊢ Module.Finite.{u_1, u_3} R ↥M

Tactic:
rw [Module.Finite.iff_fg]

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
⊢ M.FG

Tactic:
IsLattice.fg

Premises used: Submodule.IsLattice.fg
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
⊢ M.FG

Tactic:
exact IsLattice.fg

Premises used: Submodule.IsLattice.fg
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
a : Aˣ
obtain :
  ∀ (s : Finset V) [IsLattice A (span R (↑s : Set V))], (HSMul.hSMul (β := Submodule R V) a (span R (↑s : Set V))).FG
⊢ (a • M).FG

Tactic:
obtain ⟨s, rfl⟩ := IsLattice.fg (M := M)

Premises used: Submodule.IsLattice.fg, rfl
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
a : Aˣ
s : Finset V
inst_7 : IsLattice A (span R (↑s : Set V))
rw : FG (span R (a • (↑s : Set V)))
⊢ (HSMul.hSMul (β := Submodule R V) a (span R (↑s : Set V))).FG

Tactic:
rw [Submodule.smul_span]

Premises used: Submodule.smul_span
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
a : Aˣ
s : Finset V
inst_7 : IsLattice A (span R (↑s : Set V))
⊢ Finite.{u_3 + 1} (↑(a • (↑s : Set V)) : Type u_3)

Tactic:
have : Finite (a • (s : Set V) : Set V) := Finite.Set.finite_image _ _
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
a : Aˣ
s : Finset V
inst_7 : IsLattice A (span R (↑s : Set V))
this : Finite.{u_3 + 1} (↑(a • (↑s : Set V)) : Type u_3)
⊢ FG (span R (a • (↑s : Set V)))

Tactic:
Submodule.fg_span (Set.toFinite (a • (s : Set V)))

Premises used: Set.toFinite, SetLike.coe, HSMul.hSMul, Submodule.fg_span
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
a : Aˣ
s : Finset V
inst_7 : IsLattice A (span R (↑s : Set V))
this : Finite.{u_3 + 1} (↑(a • (↑s : Set V)) : Type u_3)
⊢ FG (span R (a • (↑s : Set V)))

Tactic:
exact Submodule.fg_span (Set.toFinite (a • (s : Set V)))

Premises used: Set.toFinite, SetLike.coe, HSMul.hSMul, Submodule.fg_span
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
a : Aˣ
rw : HSMul.hSMul (β := Submodule A V) a ⊤ = ⊤
⊢ Eq (α := Submodule A V) (span A (↑(a • M) : Set V)) ⊤

Tactic:
rw [Submodule.coe_pointwise_smul, ← Submodule.smul_span, IsLattice.span_eq_top]

Premises used: Submodule.coe_pointwise_smul, Submodule.IsLattice.span_eq_top, Submodule.smul_span
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
a : Aˣ
h : ∀ (x : V), x ∈ HSMul.hSMul (β := Submodule A V) a ⊤ ↔ Membership.mem (γ := Submodule A V) ⊤ x
⊢ HSMul.hSMul (β := Submodule A V) a ⊤ = ⊤

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
a : Aˣ
x : V
⊢ x ∈ HSMul.hSMul (β := Submodule A V) a ⊤ ↔ Membership.mem (γ := Submodule A V) ⊤ x

Tactic:
⟨fun _ ↦ trivial, fun _ ↦ ?_⟩

Premises used: trivial, Iff.intro
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
a : Aˣ
x : V
h : Membership.mem (γ := Submodule A V) ⊤ x → x ∈ HSMul.hSMul (β := Submodule A V) a ⊤
⊢ x ∈ HSMul.hSMul (β := Submodule A V) a ⊤ ↔ Membership.mem (γ := Submodule A V) ⊤ x

Tactic:
refine ⟨fun _ ↦ trivial, fun _ ↦ ?_⟩
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
a : Aˣ
x : V
h : Membership.mem (γ := Submodule A V) ⊤ x
⊢ x = a • a⁻¹ • x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
a : Aˣ
x : V
h_1 : Membership.mem (γ := Submodule A V) ⊤ x
h : a • a⁻¹ • x ∈ HSMul.hSMul (β := Submodule A V) a ⊤
⊢ x ∈ HSMul.hSMul (β := Submodule A V) a ⊤

Tactic:
rw [show x = a • a⁻¹ • x by simp]
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
a : Aˣ
x : V
h : Membership.mem (γ := Submodule A V) ⊤ x
⊢ Membership.mem (γ := Submodule A V) ⊤ (a⁻¹ • x)

Tactic:
trivial
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
a : Aˣ
x : V
h : Membership.mem (γ := Submodule A V) ⊤ x
⊢ a • a⁻¹ • x ∈ HSMul.hSMul (β := Submodule A V) a ⊤

Tactic:
exact Submodule.smul_mem_pointwise_smul _ _ _ (by trivial)

Premises used: Submodule.smul_mem_pointwise_smul
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M N : Submodule R V
hle : M ≤ N
inst_7 : IsLattice A M
hfg : N.FG
rw rw₁ : LE.le.{u_3} (α := Submodule A V) ⊤ ⊤
⊢ LE.le (α := Submodule A V) ⊤ (span A (↑M : Set V))

Tactic:
rw [IsLattice.span_eq_top]

Premises used: Submodule.IsLattice.span_eq_top
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M_1 M N : Submodule R V
inst_7 : IsLattice A M
inst_8 : IsLattice A N
⊢ IsLattice A (M ⊔ N)

Tactic:
of_le_of_isLattice_of_fg A le_sup_left (Submodule.FG.sup IsLattice.fg IsLattice.fg)

Premises used: Submodule.IsLattice.of_le_of_isLattice_of_fg, le_sup_left, Submodule.IsLattice.fg, Submodule.FG.sup
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
obtain :
  ∀ (s : Set M) (hs : Cardinal.mk (↑s : Type u) = Module.rank R M)
    (hli : LinearIndependent.{u, u_1, u} (ι := (↑s : Type u)) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))),
    Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤
⊢ Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤

Tactic:
obtain ⟨s, hs, hli⟩ := exists_set_linearIndependent R M

Premises used: exists_set_linearIndependent
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hs : Cardinal.mk (↑s : Type u) = Module.rank R M
hli : LinearIndependent.{u, u_1, u} (ι := (↑s : Type u)) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ LinearIndependent (ι := (↑s : Type u)) R (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))

Tactic:
replace hli := hli.map' f (LinearMap.ker_eq_bot.mpr hf)
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hs : Cardinal.mk (↑s : Type u) = Module.rank R M
hli : LinearIndependent (ι := (↑s : Type u)) R (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))

Tactic:
rw [LinearIndependent.iff_fractionRing (R := R) (K := K)] at hli

Premises used: LinearIndependent.iff_fractionRing
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hs : Cardinal.mk (↑s : Type u) = Module.rank R M
hli : LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ Cardinal.mk (↑s : Type u) = Module.rank K N

Tactic:
replace hs : Cardinal.mk s = Module.rank K N :=
    le_antisymm (LinearIndependent.cardinal_le_rank hli) (hs ▸ h)
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
hs : Cardinal.mk (↑s : Type u) = Module.rank K N
⊢ ∃ (h : Fintype (↑s : Type u)), Fintype.card.{u} (↑s : Type u) = finrank K N

Tactic:
rw [← Module.finrank_eq_rank, Cardinal.mk_eq_nat_iff_fintype] at hs

Premises used: Module.finrank_eq_rank, Cardinal.mk_eq_nat_iff_fintype
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
hs : ∃ (h : Fintype (↑s : Type u)), Fintype.card.{u} (↑s : Type u) = finrank K N
obtain :
  ∀ (hfin : Fintype (↑s : Type u)) (hcard : Fintype.card.{u} (↑s : Type u) = finrank K N),
    Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤
⊢ Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤

Tactic:
obtain ⟨hfin, hcard⟩ := hs
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
hfin : Fintype (↑s : Type u)
hcard : Fintype.card.{u} (↑s : Type u) = finrank K N
a : (↑s : Type u)
⊢ (fun (x : (↑s : Type u)) ↦ ((f : (a : M) → N) (↑x : M) : N)) a ∈ (↑f.range : Set N)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
hfin : Fintype (↑s : Type u)
hcard : Fintype.card.{u} (↑s : Type u) = finrank K N
⊢ (Set.range fun (x : (↑s : Type u)) ↦ (f : (a : M) → N) (↑x : M)) ⊆ (↑f.range : Set N)

Tactic:
have hsubset : Set.range (fun x : s ↦ f x.val) ⊆ (LinearMap.range f : Set N) := by
    rintro x ⟨a, rfl⟩
    simp
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
hfin : Fintype (↑s : Type u)
hcard : Fintype.card.{u} (↑s : Type u) = finrank K N
hsubset : (Set.range fun (x : (↑s : Type u)) ↦ (f : (a : M) → N) (↑x : M)) ⊆ (↑f.range : Set N)
rw :
  LE.le (α := Submodule K N)
    (span K (Set.range (ι := (↑s : Type u)) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))))
    (span K (↑f.range : Set N))
⊢ Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤

Tactic:
rw [eq_top_iff, ← LinearIndependent.span_eq_top_of_card_eq_finrank' hli hcard]

Premises used: eq_top_iff, LinearIndependent.span_eq_top_of_card_eq_finrank'
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
hfin : Fintype (↑s : Type u)
hcard : Fintype.card.{u} (↑s : Type u) = finrank K N
hsubset : (Set.range fun (x : (↑s : Type u)) ↦ (f : (a : M) → N) (↑x : M)) ⊆ (↑f.range : Set N)
⊢ LE.le (α := Submodule K N)
    (span K (Set.range (ι := (↑s : Type u)) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))))
    (span K (↑f.range : Set N))

Tactic:
Submodule.span_mono hsubset

Premises used: Set.Mem, setOf, Submodule.span_mono
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
hfin : Fintype (↑s : Type u)
hcard : Fintype.card.{u} (↑s : Type u) = finrank K N
hsubset : (Set.range fun (x : (↑s : Type u)) ↦ (f : (a : M) → N) (↑x : M)) ⊆ (↑f.range : Set N)
⊢ LE.le (α := Submodule K N)
    (span K (Set.range (ι := (↑s : Type u)) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))))
    (span K (↑f.range : Set N))

Tactic:
exact Submodule.span_mono hsubset

Premises used: Submodule.span_mono
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst_8 : IsLattice K M
b : Basis.{u_4, u_1, u_3} κ R ↥M
rw :
  ∀ (s : Finset κ) (g : κ → R),
    Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (↑((b : (a : κ) → ↥M) i) : V)) 0 → ∀ i ∈ s, g i = 0
⊢ LinearIndependent.{u_4, u_2, u_3} K (M := V) fun (i : κ) ↦ (↑((b : (a : κ) → ↥M) i) : V)

Tactic:
rw [← LinearIndependent.iff_fractionRing (R := R), linearIndependent_iff']

Premises used: linearIndependent_iff', LinearIndependent.iff_fractionRing
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst_8 : IsLattice K M
b : Basis.{u_4, u_1, u_3} κ R ↥M
s : Finset κ
g : κ → R
hs : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (↑((b : (a : κ) → ↥M) i) : V)) 0
⊢ Eq.{u_3 + 1} (α := ↥M) (∑ i ∈ s, HSMul.hSMul (β := ↥M) (g i) ((b : (a : κ) → ↥M) i : ↥M)) 0

Tactic:
simp_rw [← Submodule.coe_smul_of_tower, ← Submodule.coe_sum, Submodule.coe_eq_zero] at hs

Premises used: Submodule.coe_sum, Submodule.coe_smul_of_tower, Submodule.coe_eq_zero
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst_8 : IsLattice K M
b : Basis.{u_4, u_1, u_3} κ R ↥M
s : Finset κ
g : κ → R
hs : Eq.{u_3 + 1} (α := ↥M) (∑ i ∈ s, HSMul.hSMul (β := ↥M) (g i) ((b : (a : κ) → ↥M) i : ↥M)) 0
⊢ ∀ i ∈ s, g i = 0

Tactic:
linearIndependent_iff'.mp b.linearIndependent s g hs

Premises used: linearIndependent_iff', Module.Basis.linearIndependent, Iff.mp
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst_8 : IsLattice K M
b : Basis.{u_4, u_1, u_3} κ R ↥M
s : Finset κ
g : κ → R
hs : Eq.{u_3 + 1} (α := ↥M) (∑ i ∈ s, HSMul.hSMul (β := ↥M) (g i) ((b : (a : κ) → ↥M) i : ↥M)) 0
⊢ ∀ i ∈ s, g i = 0

Tactic:
exact linearIndependent_iff'.mp b.linearIndependent s g hs

Premises used: linearIndependent_iff', Module.Basis.linearIndependent, Iff.mp