awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
hLK : #↥L < #K
this_2 : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K
s : Finset ιK
rep_e :
  Eq (α := ℕ → K)
    (∑ a ∈ s, HSMul.hSMul (α := K) (β := ℕ → K) ((c : (a : ιK) → K) a : K) ((bK : (a : ιK) → ℕ → K) a : ℕ → K))
    (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
f : (i : ℕ) → (j : ↥s) → ↥L :=
  fun (i : ℕ) (j : ↥s) ↦ Subtype.mk (p := fun (x : K) ↦ x ∈ L) ((bK : (a : ιK) → ℕ → K) (↑j : ιK) i) ⋯
this_3 : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
i_1 : ℕ
hi_1 : i_1 ∈ t
hgi : g i_1 ≠ 0
i : ιK
hi : i ∈ s
eq0 :
  Eq (α := K) (∑ x ∈ t, (L.subtype : (a : ↥L) → K) ((g x • f x) (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)
    ((L.subtype : (a : ↥L) → K) (0 (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)
this : SMulCommClass (↥L)ᵐᵒᵖ K K
⊢ HSMul.hSMul (α := K) (β := K) ((c : (a : ιK) → K) i : K)
      (∑ x ∈ t, HSMul.hSMul (β := K) (g x) ((bK : (a : ιK) → ℕ → K) i x : K)) =
    0
have inr : HSMul.hSMul (α := K) (β := K) ((c : (a : ιK) → K) i : K)
    ((L.subtype : (a : ↥L) → K) (0 (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K) =
  0
Tactic: erw [eq0, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this_1 : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun (i : ιK × ℕ) ↦ (bK : (a : ιK) → ℕ → K) i.1 i.2)
hLK : #↥L < #K
this_2 : Module (↥L)ᵐᵒᵖ K := Module.compHom (R := Kᵐᵒᵖ) K ((RingHom.op : (a : ↥L →+* K) → (↥L)ᵐᵒᵖ →+* Kᵐᵒᵖ) L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K
s : Finset ιK
rep_e :
  Eq (α := ℕ → K)
    (∑ a ∈ s, HSMul.hSMul (α := K) (β := ℕ → K) ((c : (a : ιK) → K) a : K) ((bK : (a : ιK) → ℕ → K) a : ℕ → K))
    (Function.comp (β := ιL) (⇑bL : (a : ιL) → K) (⇑e : (a : ℕ) → ιL))
f : (i : ℕ) → (j : ↥s) → ↥L :=
  fun (i : ℕ) (j : ↥s) ↦ Subtype.mk (p := fun (x : K) ↦ x ∈ L) ((bK : (a : ιK) → ℕ → K) (↑j : ιK) i) ⋯
this_3 : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
i_1 : ℕ
hi_1 : i_1 ∈ t
hgi : g i_1 ≠ 0
i : ιK
hi : i ∈ s
eq0 :
  Eq (α := K) (∑ x ∈ t, (L.subtype : (a : ↥L) → K) ((g x • f x) (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)
    ((L.subtype : (a : ↥L) → K) (0 (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K)
this : SMulCommClass (↥L)ᵐᵒᵖ K K
inr :
  HSMul.hSMul (α := K) (β := K) ((c : (a : ιK) → K) i : K)
      ((L.subtype : (a : ↥L) → K) (0 (Subtype.mk (p := fun (x : ιK) ↦ x ∈ s) i hi)) : K) =
    0
⊢ HSMul.hSMul (α := K) (β := K) ((c : (a : ιK) → K) i : K)
      (∑ x ∈ t, HSMul.hSMul (β := K) (g x) ((bK : (a : ιK) → ℕ → K) i x : K)) =
    0
have inr₁ : Eq.{u + 1} (α := K) 0 0
Tactic: erw [eq0, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
⊢ Module.rank K (ι → K) = #(ι → K)
have obtain : ∀ (ιK : Type (max u v)) (bK : Module.Basis ιK K (ι → K)), Module.rank K (ι → K) = #(ι → K)
Tactic: obtain ⟨⟨ιK, bK⟩⟩ := Module.Free.exists_basis (R := K) (M := ι → K)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)
have obtain : ∀ (e : ℕ ↪ ι), Module.rank K (ι → K) = #(ι → K)
Tactic: obtain ⟨e⟩ := lift_mk_le'.mp ((aleph0_le_mk_iff.mpr hι).trans_eq (lift_uzero #ι).symm)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (hypothesis)
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
⊢ Module.rank K (ι → K) = #(ι → K)
have this : lift.{max u v, u} (Module.rank K (ℕ → K)) ≤ lift.{u, max u v} (Module.rank K (ι → K))
Tactic: have := LinearMap.lift_rank_le_of_injective _ <|
    LinearMap.funLeft_injective_of_surjective K K _ (invFun_surjective e.injective)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (hypothesis)
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{max u v, u} (Module.rank K (ℕ → K)) ≤ lift.{u, max u v} (Module.rank K (ι → K))
⊢ Module.rank K (ι → K) = #(ι → K)
have this₁ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
Tactic: rw [lift_umax.{u, v}, lift_id'.{u, v}] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (hypothesis)
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)
have key : lift.{v, u} (max ℵ₀ #K) ≤ Module.rank K (ι → K)
Tactic: have key := (lift_le.{v}.mpr <| max_aleph0_card_le_rank_fun_nat K).trans this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (hypothesis)
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : lift.{v, u} (max ℵ₀ #K) ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)
have key₁ : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
Tactic: rw [lift_max, lift_aleph0, max_le_iff] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ Infinite ιK
have rw : ℵ₀ ≤ Module.rank K (ι → K)
Tactic: rw [← aleph0_le_mk_iff, bK.mk_eq_rank'']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (hypothesis)
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)
have this₁ : Infinite ιK
Tactic: haveI : Infinite ιK := by
    rw [← aleph0_le_mk_iff, bK.mk_eq_rank'']; exact key.1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this_1 : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
this : Infinite ιK
⊢ Module.rank K (ι → K) = #(ι → K)
have rw : lift.{v, u} #K ≤ Module.rank K (ι → K)
Tactic: rw [bK.repr.toEquiv.cardinal_eq, mk_finsupp_lift_of_infinite,
      lift_umax.{u, v}, lift_id'.{u, v}, bK.mk_eq_rank'', eq_comm, max_eq_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
V : Type u_1
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
have obtain : ∀ (ι : Type u_1) (b : Module.Basis ι K V), Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
Tactic: obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
V : Type u_1
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type u_1
b : Module.Basis ι K V
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
have rw : ∀ (h : Infinite ι) (b : Module.Basis ι K V), Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
Tactic: rw [← b.mk_eq_rank'', aleph0_le_mk_iff] at h
Cleared hypotheses: h, b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
V : Type u_1
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
h : Infinite ι
b : Module.Basis ι K V
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
have have : ∀ (e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] (i : ι) → Kᵐᵒᵖ), Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
Tactic: have e := (b.constr Kᵐᵒᵖ (M' := K)).symm.trans
    (LinearEquiv.piCongrRight fun _ ↦ MulOpposite.opLinearEquiv Kᵐᵒᵖ)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
V : Type u_1
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] (i : ι) → Kᵐᵒᵖ
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
have rw : Module.rank Kᵐᵒᵖ ((i : ι) → Kᵐᵒᵖ) = #((i : ι) → Kᵐᵒᵖ)
Tactic: rw [e.rank_eq, e.toEquiv.cardinal_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
have obtain : ∀ (ι : Type u_2) (b : Module.Basis ι K V), Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
Tactic: obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type u_2
b : Module.Basis ι K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
have rw : ∀ (h : Infinite ι) (b : Module.Basis ι K V), Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
Tactic: rw [← b.mk_eq_rank'', aleph0_le_mk_iff] at h
Cleared hypotheses: h, b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_2
h : Infinite ι
b : Module.Basis ι K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
have have : ∀ (e : (V →ₗ[K] K) ≃ₗ[K] ι → K), Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
Tactic: have e := (b.constr K (M' := K)).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_2
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[K] ι → K
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
have rw : Module.rank K (ι → K) = #(ι → K)
Tactic: rw [e.rank_eq, e.toEquiv.cardinal_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
have obtain : ∀ (ι : Type v) (b : Module.Basis ι K V), lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
Tactic: obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
have rw : lift.{u, v} #ι < lift.{v, u} #K ^ lift.{u, v} #ι
Tactic: rw [← b.mk_eq_rank'', rank_dual_eq_card_dual_of_aleph0_le_rank' h,
      ← (b.constr ℕ (M' := K)).toEquiv.cardinal_eq, mk_arrow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
⊢ lift.{u, v} #ι < lift.{v, u} #K ^ lift.{u, v} #ι
have hb : 1 < lift.{v, u} #K
Tactic: apply cantor'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
⊢ 1 < lift.{v, u} #K
have hb : Nontrivial K
Tactic: rw [one_lt_lift_iff, one_lt_iff_nontrivial]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
V : Type v
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank K (V →ₗ[K] K)
have rw : lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
Tactic: rw [rank_dual_eq_card_dual_of_aleph0_le_rank h, ← rank_dual_eq_card_dual_of_aleph0_le_rank' h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
have h₁ : Module.rank K V = lift.{u, u} (Module.rank K V)
Tactic: convert! lift_rank_lt_rank_dual' h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K : Type u
inst : DivisionRing K
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V = lift.{u, u} (Module.rank K V)
have h₁ : Module.rank K V = Module.rank K V
Tactic: rw [lift_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K V : Type u
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V < Module.rank K (V →ₗ[K] K)
have h₁ : Module.rank K V = lift.{u, u} (Module.rank K V)
Tactic: convert! lift_rank_lt_rank_dual h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.ErdosKaplansky (goal)
Goal:
K V : Type u
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V = lift.{u, u} (Module.rank K V)
have h₁ : Module.rank K V = Module.rank K V
Tactic: rw [lift_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R (M := M) fun (i : ↥s) ↦ (↑i : M)) → s.card ≤ n
s : Set M
li : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ s }) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ #(↑s : Type v) ≤ (↑n : Cardinal.{v})
have H₁ : ∀ (s_1 : Finset (↑s : Type v)), s_1.card ≤ n
Tactic: apply Cardinal.card_le_of
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R (M := M) fun (i : ↥s) ↦ (↑i : M)) → s.card ≤ n
s : Set M
li : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ s }) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
t : Finset (↑s : Type v)
⊢ t.card ≤ n
have H₁ : (Finset.map (Embedding.subtype fun (x : M) ↦ x ∈ s) t).card ≤ n
Tactic: rw [← Finset.card_map (Embedding.subtype (· ∈ s))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R (M := M) fun (i : ↥s) ↦ (↑i : M)) → s.card ≤ n
s : Set M
li : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ s }) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
t : Finset (↑s : Type v)
⊢ (Finset.map (Embedding.subtype fun (x : M) ↦ x ∈ s) t).card ≤ n
have H₁ : LinearIndependent R (M := M) fun (i : ↥(Finset.map (Embedding.subtype fun (x : M) ↦ x ∈ s) t)) ↦ (↑i : M)
Tactic: apply H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R (M := M) fun (i : ↥s) ↦ (↑i : M)) → s.card ≤ n
⊢ Module.rank R M ≤ (↑n : Cardinal.{v})
have rw : LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
  (↑n : Cardinal.{v})
Tactic: rw [Module.rank_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R (M := M) fun (i : ↥s) ↦ (↑i : M)) → s.card ≤ n
⊢ LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
    (↑n : Cardinal.{v})
have h : ∀ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) ≤ (↑n : Cardinal.{v})
Tactic: apply ciSup_le'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Module.rank R M = 0 ↔ ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Nontrivial R
⊢ Module.rank R M = 0 ↔ ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
have mp : Module.rank R M = 0 → ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Nontrivial R
mp : Module.rank R M = 0 → ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
⊢ Module.rank R M = 0 ↔ ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
have mpr : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0) → Module.rank R M = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Nontrivial R
⊢ Module.rank R M = 0 → ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
have mp : (∃ (x : M), ∀ (a : R) (_ : a ≠ 0), a • x ≠ 0) → Module.rank R M ≠ 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Nontrivial R
x : M
hx : ∀ (a : R) (_ : a ≠ 0), a • x ≠ 0
⊢ Module.rank R M ≠ 0
have mp : 1 ≤ Module.rank R M
Tactic: rw [← Cardinal.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Nontrivial R
x : M
hx : ∀ (a : R) (_ : a ≠ 0), a • x ≠ 0
⊢ 1 ≤ Module.rank R M
have this : LinearIndependent.{0, u_1, u_2} R (M := M) fun (x_1 : Unit) ↦ x
Tactic: have : LinearIndependent R (fun _ : Unit ↦ x) :=
      linearIndependent_iff.mpr (fun l hl ↦ Finsupp.unique_ext <| not_not.mp fun H ↦
        hx _ H ((Finsupp.linearCombination_unique _ _ _).symm.trans hl))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Nontrivial R
h : ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
⊢ Module.rank R M = 0
have mpr : LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type u_2)) 0
Tactic: rw [← nonpos_iff_eq_zero, Module.rank_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Nontrivial R
h : ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
⊢ LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type u_2)) 0
have mpr : ∀ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type u_2) ≤ 0
Tactic: apply ciSup_le'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Nontrivial R
h : ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type u_2) ≤ 0
have mpr : ¬Nonempty.{u_2 + 1} (↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type u_2)
Tactic: rw [nonpos_iff_eq_zero, Cardinal.mk_eq_zero_iff, ← not_nonempty_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Nontrivial R
h : ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : (↑s : Type u_2)
⊢ False
have mpr : ∀ (a : R) (ha : a ≠ 0) (ha' : a • (↑i : M) = 0), False
Tactic: obtain ⟨a, ha, ha'⟩ := h i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Nontrivial R
h : ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : (↑s : Type u_2)
a : R
ha : a ≠ 0
ha' : a • (↑i : M) = 0
⊢ False
have mpr : a = 0
Tactic: apply ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
⊢ Module.rank R M = 0 ↔ ∀ (x : M), x = 0
have simp_rw : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0) ↔ ∀ (x : M), x = 0
Tactic: simp_rw [rank_eq_zero_iff, smul_eq_zero, and_or_left, not_and_self_iff, false_or,
    exists_and_right, and_iff_right (exists_ne (0 : R))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
simp_rw : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0) ↔ ∀ (x : M), x = 0
⊢ Module.rank R M = 0 ↔ ∀ (x : M), x = 0
have simp_rw₁ : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ (a = 0 ∨ x = 0)) ↔ ∀ (x : M), x = 0
Tactic: simp_rw [rank_eq_zero_iff, smul_eq_zero, and_or_left, not_and_self_iff, false_or,
    exists_and_right, and_iff_right (exists_ne (0 : R))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
simp_rw : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0) ↔ ∀ (x : M), x = 0
simp_rw₁ : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ (a = 0 ∨ x = 0)) ↔ ∀ (x : M), x = 0
⊢ Module.rank R M = 0 ↔ ∀ (x : M), x = 0
have simp_rw₂ : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a = 0 ∨ a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0
Tactic: simp_rw [rank_eq_zero_iff, smul_eq_zero, and_or_left, not_and_self_iff, false_or,
    exists_and_right, and_iff_right (exists_ne (0 : R))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
simp_rw : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0) ↔ ∀ (x : M), x = 0
simp_rw₁ : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ (a = 0 ∨ x = 0)) ↔ ∀ (x : M), x = 0
simp_rw₂ : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a = 0 ∨ a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0
⊢ Module.rank R M = 0 ↔ ∀ (x : M), x = 0
have simp_rw₃ : (∀ (x : M), ∃ (a : R), False ∨ a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0
Tactic: simp_rw [rank_eq_zero_iff, smul_eq_zero, and_or_left, not_and_self_iff, false_or,
    exists_and_right, and_iff_right (exists_ne (0 : R))]