awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
s : Set ↥f.range
si : LinearIndepOn K _root_.id s
h : #(↑s : Type v') ≤ f.rank
fg : ∀ (x : ↥f.range), (f : (a : V) → V') ((g : (a : ↥f.range) → V) x : V) = (↑x : V')
⊢ LinearIndepOn K (M := V') (fun (x : ↥f.range) ↦ (f : (a : V) → V') ((g : (a : ↥f.range) → V) x : V)) s

Tactic:
simpa only [fg] using si.map' _ (ker_subtype _)

Premises used: Submodule.ker_subtype, LinearIndependent.map'
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
s : Set ↥f.range
si : LinearIndepOn K _root_.id s
h : #(↑s : Type v') ≤ f.rank
fg : ∀ (x : ↥f.range), (f : (a : V) → V') ((g : (a : ↥f.range) → V) x : V) = (↑x : V')
⊢ LinearIndepOn K (M := V') (fun (x : ↥f.range) ↦ (f : (a : V) → V') ((g : (a : ↥f.range) → V) x : V)) s

Tactic:
replace si : LinearIndepOn K (fun x => f (g x)) s := by
      simpa only [fg] using si.map' _ (ker_subtype _)
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
s : Set ↥f.range
h : #(↑s : Type v') ≤ f.rank
fg : ∀ (x : ↥f.range), (f : (a : V) → V') ((g : (a : ↥f.range) → V) x : V) = (↑x : V')
si : LinearIndepOn K (M := V') (fun (x : ↥f.range) ↦ (f : (a : V) → V') ((g : (a : ↥f.range) → V) x : V)) s
⊢ LinearIndepOn.{v, u, v'} (ι := V) K (M := V') (⇑f : (a : V) → V') ((⇑g : (a : ↥f.range) → V) '' s)

Tactic:
si.image_of_comp

Premises used: LinearIndepOn.image_of_comp
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
s : Set ↥f.range
h : #(↑s : Type v') ≤ f.rank
fg : ∀ (x : ↥f.range), (f : (a : V) → V') ((g : (a : ↥f.range) → V) x : V) = (↑x : V')
si : LinearIndepOn K (M := V') (fun (x : ↥f.range) ↦ (f : (a : V) → V') ((g : (a : ↥f.range) → V) x : V)) s
⊢ LinearIndepOn.{v, u, v'} (ι := V) K (M := V') (⇑f : (a : V) → V') ((⇑g : (a : ↥f.range) → V) '' s)

Tactic:
exact si.image_of_comp

Premises used: LinearIndepOn.image_of_comp
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set V
hsc : lift.{v', v} #(↑s : Type v) = lift.{v, v'} c
si : LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
⊢ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s

Tactic:
si
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set V
hsc : lift.{v', v} #(↑s : Type v) = lift.{v, v'} c
si : LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
⊢ LinearIndependent.{v, u, v'} (ι := (↑s : Type v)) K (M := V')
    (Function.comp (β := ↥f.range) (⇑f.range.subtype : (a : ↥f.range) → V') fun (x : (↑s : Type v)) ↦
      ((f.rangeRestrict : LinearMap.{u, u, v, v'} (RingHom.id K) V ↥f.range) : (a : V) → ↥f.range) (↑x : V))

Tactic:
convert! si
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set V
hsc : lift.{v', v} #(↑s : Type v) = lift.{v, v'} c
si : LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
⊢ LinearIndepOn.{v, u, v'} K (M := ↥f.range) (⇑f.rangeRestrict : (a : V) → ↥f.range) s

Tactic:
have : LinearIndepOn K f.rangeRestrict s :=
      LinearIndependent.of_comp (LinearMap.range f).subtype (by convert! si)
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set V
hsc : lift.{v', v} #(↑s : Type v) = lift.{v, v'} c
si : LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
this : LinearIndepOn.{v, u, v'} K (M := ↥f.range) (⇑f.rangeRestrict : (a : V) → ↥f.range) s
⊢ #(↑((⇑f.rangeRestrict : (a : V) → ↥f.range) '' s) : Type v') ≤ Module.rank K ↥f.range

Tactic:
this.id_image.cardinal_le_rank

Premises used: LinearIndependent.cardinal_le_rank, LinearIndepOn.id_image
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set V
hsc : lift.{v', v} #(↑s : Type v) = lift.{v, v'} c
si : LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
this : LinearIndepOn.{v, u, v'} K (M := ↥f.range) (⇑f.rangeRestrict : (a : V) → ↥f.range) s
h : c = #(↑((⇑f.rangeRestrict : (a : V) → ↥f.range) '' s) : Type v')
⊢ c ≤ f.rank

Tactic:
convert! this.id_image.cardinal_le_rank

Premises used: LinearIndependent.cardinal_le_rank, LinearIndepOn.id_image
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set V
hsc : lift.{v', v} #(↑s : Type v) = lift.{v, v'} c
si : LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
this : LinearIndepOn.{v, u, v'} K (M := ↥f.range) (⇑f.rangeRestrict : (a : V) → ↥f.range) s
h : InjOn.{v, v'} (β := ↥f.range) (⇑f.rangeRestrict : (a : V) → ↥f.range) s
⊢ c = #(↑((⇑f.rangeRestrict : (a : V) → ↥f.range) '' s) : Type v')

Tactic:
rw [← Cardinal.lift_inj, ← hsc, Cardinal.mk_image_eq_of_injOn_lift]

Premises used: Cardinal.mk_image_eq_of_injOn_lift, Cardinal.lift_inj
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set V
hsc : lift.{v', v} #(↑s : Type v) = lift.{v, v'} c
si : LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
this : LinearIndepOn.{v, u, v'} K (M := ↥f.range) (⇑f.rangeRestrict : (a : V) → ↥f.range) s
⊢ InjOn.{v, v'} (β := ↥f.range) (⇑f.rangeRestrict : (a : V) → ↥f.range) s

Tactic:
injOn_iff_injective.2 this.injective

Premises used: Iff.mpr, Set.injOn_iff_injective, LinearIndependent.injective
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set V
hsc : lift.{v', v} #(↑s : Type v) = lift.{v, v'} c
si : LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
this : LinearIndepOn.{v, u, v'} K (M := ↥f.range) (⇑f.rangeRestrict : (a : V) → ↥f.range) s
⊢ InjOn.{v, v'} (β := ↥f.range) (⇑f.rangeRestrict : (a : V) → ↥f.range) s

Tactic:
exact injOn_iff_injective.2 this.injective

Premises used: Iff.mpr, Set.injOn_iff_injective, LinearIndependent.injective
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
n : ℕ
f : V →ₗ[K] V'
simp :
  (∃ (s : Set V),
      (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s) ↔
    ∃ (s : Finset V),
      s.card = n ∧
        LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)
⊢ (↑n : Cardinal.{v'}) ≤ f.rank ↔
    ∃ (s : Finset V),
      s.card = n ∧
        LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)

Tactic:
simp only [le_rank_iff_exists_linearIndependent, Cardinal.lift_natCast, Cardinal.lift_eq_nat_iff,
    Cardinal.mk_set_eq_nat_iff_finset]

Premises used: LinearMap.le_rank_iff_exists_linearIndependent, Cardinal.lift_natCast, Cardinal.mk_set_eq_nat_iff_finset, Cardinal.lift_eq_nat_iff
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
n : ℕ
f : V →ₗ[K] V'
mp :
  (∃ (s : Set V),
      (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s) →
    ∃ (s : Finset V),
      s.card = n ∧
        LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)
mpr :
  (∃ (s : Finset V),
      s.card = n ∧
        LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)) →
    ∃ (s : Set V),
      (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
⊢ (∃ (s : Set V),
      (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s) ↔
    ∃ (s : Finset V),
      s.card = n ∧
        LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
f : V →ₗ[K] V'
t : Finset V
si : LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') (↑t : Set V)
⊢ ∃ (s : Finset V),
    s.card = t.card ∧
      LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)

Tactic:
⟨t, rfl, si⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
f : V →ₗ[K] V'
t : Finset V
si : LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') (↑t : Set V)
⊢ ∃ (s : Finset V),
    s.card = t.card ∧
      LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)

Tactic:
exact ⟨t, rfl, si⟩
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
f : V →ₗ[K] V'
s : Finset V
si : LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)
⊢ ∃ (s_1 : Set V),
    (∃ (t : Finset V), (↑t : Set V) = s_1 ∧ t.card = s.card) ∧
      LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s_1

Tactic:
⟨s, ⟨s, rfl, rfl⟩, si⟩

Premises used: SetLike.coe, And.intro, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.LinearMap
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
f : V →ₗ[K] V'
s : Finset V
si : LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)
⊢ ∃ (s_1 : Set V),
    (∃ (t : Finset V), (↑t : Set V) = s_1 ∧ t.card = s.card) ∧
      LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s_1

Tactic:
exact ⟨s, ⟨s, rfl, rfl⟩, si⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
inl : Subsingleton R → Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)
inr : Nontrivial R → Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Subsingleton R
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)

Tactic:
simp only [rank_subsingleton, lift_one]

Premises used: Cardinal.lift_one, rank_subsingleton
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Nontrivial R
inr : Cardinal.lift.{uM, uN} (Module.rank R N) ≤ Cardinal.lift.{uN, uM} (Module.rank R M)
inr₁ : Cardinal.lift.{uN, uM} (Module.rank R M) ≤ Cardinal.lift.{uM, uN} (Module.rank R N)
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Nontrivial R
inr :
  ⨆ (i : { s : Set N // LinearIndepOn R id s }), Cardinal.lift.{uM, uN} #(↑(↑i : Set N) : Type uN) ≤
    Cardinal.lift.{uN, uM} (Module.rank R M)
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) ≤ Cardinal.lift.{uN, uM} (Module.rank R M)

Tactic:
rw [Module.rank_def, lift_iSup bddAbove_of_small]

Premises used: Module.rank_def, Cardinal.lift_iSup, Cardinal.bddAbove_of_small
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Nontrivial R
inr :
  ⨆ (i : { s : Set M // LinearIndepOn R id s }), Cardinal.lift.{uN, uM} #(↑(↑i : Set M) : Type uM) ≤
    Cardinal.lift.{uM, uN} (Module.rank R N)
⊢ Cardinal.lift.{uN, uM} (Module.rank R M) ≤ Cardinal.lift.{uM, uN} (Module.rank R N)

Tactic:
rw [Module.rank_def, lift_iSup bddAbove_of_small]

Premises used: Module.rank_def, Cardinal.lift_iSup, Cardinal.bddAbove_of_small
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Nontrivial R
inr :
  ∀ (i : { s : Set N // LinearIndepOn R id s }),
    Cardinal.lift.{uM, uN} #(↑(↑i : Set N) : Type uN) ≤ Cardinal.lift.{uN, uM} (Module.rank R M)
⊢ ⨆ (i : { s : Set N // LinearIndepOn R id s }), Cardinal.lift.{uM, uN} #(↑(↑i : Set N) : Type uN) ≤
    Cardinal.lift.{uN, uM} (Module.rank R M)

Tactic:
apply ciSup_le'

Premises used: ciSup_le'
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Nontrivial R
inr :
  ∀ (i : { s : Set M // LinearIndepOn R id s }),
    Cardinal.lift.{uN, uM} #(↑(↑i : Set M) : Type uM) ≤ Cardinal.lift.{uM, uN} (Module.rank R N)
⊢ ⨆ (i : { s : Set M // LinearIndepOn R id s }), Cardinal.lift.{uN, uM} #(↑(↑i : Set M) : Type uM) ≤
    Cardinal.lift.{uM, uN} (Module.rank R N)

Tactic:
apply ciSup_le'

Premises used: ciSup_le'
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Nontrivial R
s : Set N
hs : LinearIndepOn R id s
⊢ Cardinal.lift.{uM, uN} #(↑(↑(Subtype.mk (p := fun (s : Set N) ↦ LinearIndepOn R id s) s hs) : Set N) : Type uN) ≤
    Cardinal.lift.{uN, uM} (Module.rank R M)

Tactic:
(IsLocalizedModule.linearIndependent_lift p f hs).choose_spec.cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank, Exists.choose_spec, IsLocalizedModule.linearIndependent_lift
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Nontrivial R
s : Set M
hs : LinearIndepOn R id s
⊢ Cardinal.lift.{uN, uM} #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type uM) ≤
    Cardinal.lift.{uM, uN} (Module.rank R N)

Tactic:
hs.of_isLocalizedModule_of_isRegular p f (le_nonZeroDivisors_iff_isRegular.mp hp)
      |>.cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank, LinearIndependent.of_isLocalizedModule_of_isRegular, le_nonZeroDivisors_iff_isRegular, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Nontrivial R
s : Set N
hs : LinearIndepOn R id s
⊢ Cardinal.lift.{uM, uN} #(↑(↑(Subtype.mk (p := fun (s : Set N) ↦ LinearIndepOn R id s) s hs) : Set N) : Type uN) ≤
    Cardinal.lift.{uN, uM} (Module.rank R M)

Tactic:
exacts [(IsLocalizedModule.linearIndependent_lift p f hs).choose_spec.cardinal_lift_le_rank,
    hs.of_isLocalizedModule_of_isRegular p f (le_nonZeroDivisors_iff_isRegular.mp hp)
      |>.cardinal_lift_le_rank]

Premises used: LinearIndependent.cardinal_lift_le_rank, Exists.choose_spec, IsLocalizedModule.linearIndependent_lift
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
⊢ finrank R N = finrank R M

Tactic:
simpa using congr_arg toNat (lift_rank_eq p f hp)

Premises used: Cardinal.toNat, IsLocalizedModule.lift_rank_eq, congr_arg, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submonoid R
hp : p ≤ R⁰
N : Type uM
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
⊢ Module.rank R N = Module.rank R M

Tactic:
simpa using lift_rank_eq p f hp

Premises used: IsLocalizedModule.lift_rank_eq
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
inl : Subsingleton R → Module.rank S N = Module.rank R N
inr : Nontrivial R → Module.rank S N = Module.rank R N
⊢ Module.rank S N = Module.rank R N

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
h : Subsingleton R
⊢ Subsingleton S

Tactic:
have := (algebraMap R S).codomain_trivial
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
h : Subsingleton R
this : Subsingleton S
⊢ Module.rank S N = Module.rank R N

Tactic:
simp only [rank_subsingleton]

Premises used: rank_subsingleton
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
h : Nontrivial R
⊢ Function.Injective.{uR + 1, uS + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
have inj := IsLocalization.injective S hp
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
h : Nontrivial R
inj : Function.Injective.{uR + 1, uS + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
inr : Module.rank S N ≤ Module.rank R N
inr₁ : Module.rank R N ≤ Module.rank S N
⊢ Module.rank S N = Module.rank R N

Tactic:
apply le_antisymm

Premises used: le_antisymm