awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
a : #ι ≤ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
⊢ #ι = ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
have a₁ : ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v) ≤ #ι
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ #ι ≤ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
have trans : #ι ≤
  #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range (ι := ι) (⇑v : (a : ι) → M)) sorry) : Set M) :
      Type v)
Tactic: trans
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
trans :
  #ι ≤
    #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range (ι := ι) (⇑v : (a : ι) → M)) ⋯) : Set M) :
        Type v)
⊢ #ι ≤ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
have trans₁ : #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range (ι := ι) (⇑v : (a : ι) → M)) sorry) : Set M) :
      Type v) ≤
  ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
Tactic: trans
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
trans :
  #ι ≤
    #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range (ι := ι) (⇑v : (a : ι) → M)) ⋯) : Set M) :
        Type v)
trans₁ :
  #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range (ι := ι) (⇑v : (a : ι) → M)) ⋯) : Set M) :
        Type v) ≤
    ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
⊢ #ι ≤ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
have trans₂ : Cardinal.{v}
Tactic: trans
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range (ι := ι) (⇑v : (a : ι) → M)) ⋯) : Set M) :
        Type v) ≤
    ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v)
have apply : { s : Set M // LinearIndepOn R id s }
Tactic: apply le_ciSup Cardinal.bddAbove_of_small
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ LinearIndependent R (M := M) fun (x : (↑(range (ι := ι) (⇑v : (a : ι) → M)) : Type v)) ↦ id (↑x : M)
have h : ∀ (x : (↑(range (ι := ι) (⇑v : (a : ι) → M)) : Type v)),
  id (↑x : M) = (v.reindexRange : (a : (↑(range (⇑v : (a : ι) → M)) : Type v)) → M) x
Tactic: convert! v.reindexRange.linearIndependent
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v) ≤ #ι
have a : ∀ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) ≤ #ι
Tactic: apply ciSup_le'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Fintype ι
h : Basis ι R M
⊢ Module.rank R M = (↑(Fintype.card ι) : Cardinal.{v})
have this : Nontrivial R
Tactic: haveI := nontrivial_of_invariantBasisNumber R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Fintype ι
h : Basis ι R M
this : Nontrivial R
⊢ Module.rank R M = (↑(Fintype.card ι) : Cardinal.{v})
have rw : #(↑(range.{v, w + 1} (ι := ι) (⇑h : (a : ι) → M)) : Type v) = (↑(Fintype.card ι) : Cardinal.{v})
Tactic: rw [← h.mk_range_eq_rank, Cardinal.mk_fintype, Set.card_range_of_injective h.injective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Fintype ι
h : Basis ι R M
this : Nontrivial R
rw : #(↑(range.{v, w + 1} (ι := ι) (⇑h : (a : ι) → M)) : Type v) = (↑(Fintype.card ι) : Cardinal.{v})
⊢ Module.rank R M = (↑(Fintype.card ι) : Cardinal.{v})
have rw₁ : Eq.{v + 2} (α := Cardinal.{v})
  (↑(Fintype.card.{v} (↑(range.{v, w + 1} (ι := ι) (⇑h : (a : ι) → M)) : Type v)) : Cardinal.{v})
  (↑(Fintype.card ι) : Cardinal.{v})
Tactic: rw [← h.mk_range_eq_rank, Cardinal.mk_fintype, Set.card_range_of_injective h.injective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Fintype ι
h : Basis ι R M
this : Nontrivial R
rw : #(↑(range.{v, w + 1} (ι := ι) (⇑h : (a : ι) → M)) : Type v) = (↑(Fintype.card ι) : Cardinal.{v})
rw₁ :
  Eq.{v + 2} (α := Cardinal.{v})
    (↑(Fintype.card.{v} (↑(range.{v, w + 1} (ι := ι) (⇑h : (a : ι) → M)) : Type v)) : Cardinal.{v})
    (↑(Fintype.card ι) : Cardinal.{v})
⊢ Module.rank R M = (↑(Fintype.card ι) : Cardinal.{v})
have rw₂ : Eq.{v + 2} (α := Cardinal.{v}) (↑(Fintype.card ι) : Cardinal.{v}) (↑(Fintype.card ι) : Cardinal.{v})
Tactic: rw [← h.mk_range_eq_rank, Cardinal.mk_fintype, Set.card_range_of_injective h.injective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Fintype ι
h : Basis ι R M
⊢ Module.rank R M = (↑(Fintype.card ι) : Cardinal.{v})
have haveI : ∀ (this : Nontrivial R), Module.rank R M = (↑(Fintype.card ι) : Cardinal.{v})
Tactic: classical
  haveI := nontrivial_of_invariantBasisNumber R
  rw [← h.mk_range_eq_rank, Cardinal.mk_fintype, Set.card_range_of_injective h.injective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
v : Basis ι R M
⊢ Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} (Module.rank R M)
have this : Nontrivial R
Tactic: haveI := nontrivial_of_invariantBasisNumber R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
v : Basis ι R M
this : Nontrivial R
⊢ Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} (Module.rank R M)
have rw : Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
Tactic: rw [← v.mk_range_eq_rank, Cardinal.mk_range_eq_of_injective v.injective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
v : Basis ι R M
this : Nontrivial R
rw : Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} #(↑(range.{v, w + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type v)
⊢ Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} (Module.rank R M)
have rw₁ : Cardinal.lift.{v, w} #ι = Cardinal.lift.{v, w} #ι
Tactic: rw [← v.mk_range_eq_rank, Cardinal.mk_range_eq_of_injective v.injective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
v : ι → M
hv : LinearIndependent R v
⊢ Module.rank R ↥(span R (range v)) = #(↑(range v) : Type v)
have this : Nontrivial R
Tactic: haveI := nontrivial_of_invariantBasisNumber R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
v : ι → M
hv : LinearIndependent R v
this : Nontrivial R
⊢ Module.rank R ↥(span R (range v)) = #(↑(range v) : Type v)
have rw : Cardinal.lift.{w, v} (Module.rank R ↥(span R (range v))) = Cardinal.lift.{w, v} #(↑(range v) : Type v)
Tactic: rw [← Cardinal.lift_inj, ← (Basis.span hv).mk_eq_rank,
    Cardinal.mk_range_eq_of_injective (@LinearIndependent.injective ι R M v _ _ _ _ hv)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
v : ι → M
hv : LinearIndependent R v
this : Nontrivial R
rw : Cardinal.lift.{w, v} (Module.rank R ↥(span R (range v))) = Cardinal.lift.{w, v} #(↑(range v) : Type v)
⊢ Module.rank R ↥(span R (range v)) = #(↑(range v) : Type v)
have rw₁ : Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} #(↑(range v) : Type v)
Tactic: rw [← Cardinal.lift_inj, ← (Basis.span hv).mk_eq_rank,
    Cardinal.mk_range_eq_of_injective (@LinearIndependent.injective ι R M v _ _ _ _ hv)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
v : ι → M
hv : LinearIndependent R v
this : Nontrivial R
rw : Cardinal.lift.{w, v} (Module.rank R ↥(span R (range v))) = Cardinal.lift.{w, v} #(↑(range v) : Type v)
rw₁ : Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} #(↑(range v) : Type v)
⊢ Module.rank R ↥(span R (range v)) = #(↑(range v) : Type v)
have rw₂ : Cardinal.lift.{v, w} #ι = Cardinal.lift.{v, w} #ι
Tactic: rw [← Cardinal.lift_inj, ← (Basis.span hv).mk_eq_rank,
    Cardinal.mk_range_eq_of_injective (@LinearIndependent.injective ι R M v _ _ _ _ hv)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R id s
⊢ Module.rank R ↥(span R s) = #(↑s : Type v)
have rw : Module.rank R ↥(span R (range (ι := Subtype (Membership.mem s)) (Subtype.val (p := Membership.mem s)))) =
  #(↑(range (ι := Subtype (Membership.mem s)) (Subtype.val (p := Membership.mem s))) : Type v)
Tactic: rw [← @setOf_mem_eq _ s, ← Subtype.range_coe_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
v : ι → M
s : Set ι
hs : LinearIndepOn R v s
⊢ (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (v '' s))) = s.encard
have rw : (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) = s.encard
Tactic: rw [image_eq_range, ← hs.injOn.encard_image, ← toENat_cardinalMk, image_eq_range,
    ← rank_span hs.linearIndependent]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
v : ι → M
s : Set ι
hs : LinearIndepOn R v s
rw :
  (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) = s.encard
⊢ (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (v '' s))) = s.encard
have rw₁ : (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) =
  (v '' s).encard
Tactic: rw [image_eq_range, ← hs.injOn.encard_image, ← toENat_cardinalMk, image_eq_range,
    ← rank_span hs.linearIndependent]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
v : ι → M
s : Set ι
hs : LinearIndepOn R v s
rw :
  (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) = s.encard
rw₁ :
  (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) =
    (v '' s).encard
⊢ (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (v '' s))) = s.encard
have rw₂ : Eq (α := ℕ∞)
  ((toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) : ℕ∞)
  ((toENat : (a : Cardinal.{v}) → ℕ∞) #(↑(v '' s) : Type v) : ℕ∞)
Tactic: rw [image_eq_range, ← hs.injOn.encard_image, ← toENat_cardinalMk, image_eq_range,
    ← rank_span hs.linearIndependent]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
v : ι → M
s : Set ι
hs : LinearIndepOn R v s
rw :
  (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) = s.encard
rw₁ :
  (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) =
    (v '' s).encard
rw₂ :
  Eq (α := ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) : ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) #(↑(v '' s) : Type v) : ℕ∞)
⊢ (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (v '' s))) = s.encard
have rw₃ : Eq (α := ℕ∞)
  ((toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) : ℕ∞)
  ((toENat : (a : Cardinal.{v}) → ℕ∞) #(↑(range fun (x : (↑s : Type w)) ↦ v (↑x : ι)) : Type v) : ℕ∞)
Tactic: rw [image_eq_range, ← hs.injOn.encard_image, ← toENat_cardinalMk, image_eq_range,
    ← rank_span hs.linearIndependent]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
v : ι → M
s : Set ι
hs : LinearIndepOn R v s
rw :
  (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) = s.encard
rw₁ :
  (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) =
    (v '' s).encard
rw₂ :
  Eq (α := ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) : ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) #(↑(v '' s) : Type v) : ℕ∞)
rw₃ :
  Eq (α := ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) : ℕ∞)
    ((toENat : (a : Cardinal.{v}) → ℕ∞) #(↑(range fun (x : (↑s : Type w)) ↦ v (↑x : ι)) : Type v) : ℕ∞)
⊢ (toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (v '' s))) = s.encard
have rw₄ : Eq (α := ℕ∞)
  ((toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) : ℕ∞)
  ((toENat : (a : Cardinal.{v}) → ℕ∞) (Module.rank R ↥(span R (range fun (x : (↑s : Type w)) ↦ v (↑x : ι)))) : ℕ∞)
Tactic: rw [image_eq_range, ← hs.injOn.encard_image, ← toENat_cardinalMk, image_eq_range,
    ← rank_span hs.linearIndependent]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
⊢ Fintype.card m = Fintype.card n
have obtain : ∀ (a : ↥I) (ha : a ≠ 0), Fintype.card m = Fintype.card n
Tactic: obtain ⟨a, ha⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr hI)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
a : ↥I
ha : a ≠ 0
⊢ LinearIndependent.{u_4, u_2, u_3} R (M := ↥I) fun (i : n) ↦ HSMul.hSMul (α := S) ((b : (a : n) → S) i : S) a
have hb : LinearIndependent.{u_4, u_2, u_3} (ι := n) R (M := S) (⇑b : (a : n) → S)
Tactic: have hb := b.linearIndependent
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
a : ↥I
ha : a ≠ 0
hb : LinearIndependent.{u_4, u_2, u_3} (ι := n) R (M := S) (⇑b : (a : n) → S)
⊢ LinearIndependent.{u_4, u_2, u_3} R (M := ↥I) fun (i : n) ↦ HSMul.hSMul (α := S) ((b : (a : n) → S) i : S) a
have rw : ∀
  (hb :
    ∀ (g : n → R),
      Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0 → ∀ (i : n), g i = 0)
  (g : n → R),
  Eq.{u_3 + 1} (α := ↥I) (∑ i : n, g i • HSMul.hSMul (α := S) ((b : (a : n) → S) i : S) a) 0 → ∀ (i : n), g i = 0
Tactic: rw [Fintype.linearIndependent_iff] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
a : ↥I
ha : a ≠ 0
hb :
  ∀ (g : n → R),
    Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0 → ∀ (i : n), g i = 0
g : n → R
hg : Eq.{u_3 + 1} (α := ↥I) (∑ i : n, g i • HSMul.hSMul (α := S) ((b : (a : n) → S) i : S) a) 0
⊢ ∀ (i : n), g i = 0
have apply : Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0
Tactic: apply hb g
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
a : ↥I
ha : a ≠ 0
hb :
  ∀ (g : n → R),
    Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0 → ∀ (i : n), g i = 0
g : n → R
hg : Eq.{u_3 + 1} (α := ↥I) (∑ i : n, g i • HSMul.hSMul (α := S) ((b : (a : n) → S) i : S) a) 0
⊢ Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0
have hg₁ : Eq.{u_3 + 1} (α := S) (∑ i : n, HSMul.hSMul (β := S) (g i) ((b : (a : n) → S) i : S)) 0 ∨ a = 0
Tactic: simp only [← smul_assoc, ← Finset.sum_smul, smul_eq_zero] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (hypothesis)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : Ring S
inst_3 : IsDomain S
inst_4 : Algebra R S
n : Type u_4
m : Type u_5
inst_5 : Fintype n
inst_6 : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis.{u_5, u_2, u_3} m R ↥I
a : ↥I
ha : a ≠ 0
⊢ Fintype.card m = Fintype.card n
have this : LinearIndependent.{u_4, u_2, u_3} R (M := ↥I) fun (i : n) ↦ HSMul.hSMul (α := S) ((b : (a : n) → S) i : S) a
Tactic: have : LinearIndependent R fun i => b i • a := by
    have hb := b.linearIndependent
    rw [Fintype.linearIndependent_iff] at hb ⊢
    intro g hg
    apply hb g
    simp only [← smul_assoc, ← Finset.sum_smul, smul_eq_zero] at hg
    exact hg.resolve_right ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
⊢ 0 < Module.rank R M ↔ Nontrivial M
have refine : ∀ (h : 0 < Module.rank R M), Nontrivial M
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ rank_pos_of_free⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
h : 0 < Module.rank R M
⊢ Nontrivial M
have rw : ¬Subsingleton M
Tactic: rw [← not_subsingleton_iff_nontrivial]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
⊢ Module.rank R M = 0 ↔ Subsingleton M
have rw : Module.rank R M = 0 ↔ ¬Nontrivial M
Tactic: rw [← not_nontrivial_iff_subsingleton, iff_not_comm,
    ← Module.rank_pos_iff_of_free (R := R), pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
rw : Module.rank R M = 0 ↔ ¬Nontrivial M
⊢ Module.rank R M = 0 ↔ Subsingleton M
have rw₁ : Nontrivial M ↔ ¬Module.rank R M = 0
Tactic: rw [← not_nontrivial_iff_subsingleton, iff_not_comm,
    ← Module.rank_pos_iff_of_free (R := R), pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
rw : Module.rank R M = 0 ↔ ¬Nontrivial M
rw₁ : Nontrivial M ↔ ¬Module.rank R M = 0
⊢ Module.rank R M = 0 ↔ Subsingleton M
have rw₂ : 0 < Module.rank R M ↔ ¬Module.rank R M = 0
Tactic: rw [← not_nontrivial_iff_subsingleton, iff_not_comm,
    ← Module.rank_pos_iff_of_free (R := R), pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
rw : Module.rank R M = 0 ↔ ¬Nontrivial M
rw₁ : Nontrivial M ↔ ¬Module.rank R M = 0
rw₂ : 0 < Module.rank R M ↔ ¬Module.rank R M = 0
⊢ Module.rank R M = 0 ↔ Subsingleton M
have rw₃ : Module.rank R M ≠ 0 ↔ ¬Module.rank R M = 0
Tactic: rw [← not_nontrivial_iff_subsingleton, iff_not_comm,
    ← Module.rank_pos_iff_of_free (R := R), pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.StrongRankCondition (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : StrongRankCondition R
h : Basis ι R M
⊢ finrank R M = Nat.card ι
have rw : finrank R M = (toNat : (a : Cardinal.{w}) → ℕ) #ι
Tactic: rw [Nat.card, ← toNat_lift.{v}, h.mk_eq_rank, toNat_lift, finrank]