awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
this : lift.{u_1, u_2} (Module.rank F ↥(LinearMap.range (Algebra.linearMap F E))) ≤ lift.{u_2, u_1} (Module.rank F F)
refine_1 : ∀ (this : lift.{u_1, u_2} (Module.rank F ↥1) ≤ lift.{u_2, u_1} (Module.rank F F)), Module.rank F ↥⊥ ≤ 1
refine_1₁ : ∀ (this : lift.{u_1, u_2} (Module.rank F ↥1) ≤ lift.{u_2, u_1} 1), Module.rank F ↥⊥ ≤ 1
refine_1₂ : ∀ (this : lift.{u_1, u_2} (Module.rank F ↥1) ≤ 1), Module.rank F ↥⊥ ≤ 1
refine_1₃ : ∀ (this : Module.rank F ↥1 ≤ 1), Module.rank F ↥⊥ ≤ 1
⊢ Module.rank F ↥⊥ ≤ 1
have refine_1₄ : ∀ (this : Module.rank F ↥((toSubmodule : (a : Subalgebra F E) → Submodule F E) ⊥ : Submodule F E) ≤ 1),
  Module.rank F ↥⊥ ≤ 1
Tactic: rwa [← one_eq_range, rank_self, lift_one, lift_le_one_iff,
      ← Algebra.toSubmodule_bot, rank_toSubmodule] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
this : lift.{u_1, u_2} (Module.rank F ↥(LinearMap.range (Algebra.linearMap F E))) ≤ lift.{u_2, u_1} (Module.rank F F)
refine_1 : ∀ (this : lift.{u_1, u_2} (Module.rank F ↥1) ≤ lift.{u_2, u_1} (Module.rank F F)), Module.rank F ↥⊥ ≤ 1
refine_1₁ : ∀ (this : lift.{u_1, u_2} (Module.rank F ↥1) ≤ lift.{u_2, u_1} 1), Module.rank F ↥⊥ ≤ 1
refine_1₂ : ∀ (this : lift.{u_1, u_2} (Module.rank F ↥1) ≤ 1), Module.rank F ↥⊥ ≤ 1
refine_1₃ : ∀ (this : Module.rank F ↥1 ≤ 1), Module.rank F ↥⊥ ≤ 1
refine_1₄ :
  ∀ (this : Module.rank F ↥((toSubmodule : (a : Subalgebra F E) → Submodule F E) ⊥ : Submodule F E) ≤ 1),
    Module.rank F ↥⊥ ≤ 1
⊢ Module.rank F ↥⊥ ≤ 1
have refine_1₅ : ∀ (this : Module.rank F ↥⊥ ≤ 1), Module.rank F ↥⊥ ≤ 1
Tactic: rwa [← one_eq_range, rank_self, lift_one, lift_le_one_iff,
      ← Algebra.toSubmodule_bot, rank_toSubmodule] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ 1 ≤ Module.rank F ↥⊥
have refine_2 : ∀ (H : ¬1 ≤ Module.rank F ↥⊥), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : ¬1 ≤ Module.rank F ↥⊥
⊢ False
have H₁ : Module.rank F ↥⊥ = 0
Tactic: rw [not_le, Cardinal.lt_one_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ = 0
⊢ False
have this : IsEmpty κ
Tactic: haveI := mk_eq_zero_iff.1 (H ▸ b.mk_eq_rank'')
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ = 0
this : IsEmpty κ
⊢ False
have this₁ : Subsingleton.{u_2 + 1} ↥⊥
Tactic: haveI := b.repr.toEquiv.subsingleton
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥S
⊢ finrank.{u_1, u_2} F ↥S = 1 ↔ S = ⊥
have rw : finrank.{u_1, u_2} F ↥S = 1 ↔ Module.rank F ↥S = 1
Tactic: rw [← Subalgebra.rank_eq_one_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free F E
⊢ Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Module.rank F E = 1
have this : Free.{u_1, u_2} F ↥⊤
Tactic: haveI := Module.Free.of_equiv (Subalgebra.topEquiv (R := F) (A := E)).toLinearEquiv.symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free F E
this : Free.{u_1, u_2} F ↥⊤
⊢ Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Module.rank F E = 1
have rw : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Module.rank F ↥⊤ = 1
Tactic: rw [← rank_top, Subalgebra.rank_eq_one_iff, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free F E
this : Free.{u_1, u_2} F ↥⊤
rw : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Module.rank F ↥⊤ = 1
⊢ Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Module.rank F E = 1
have rw₁ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥
Tactic: rw [← rank_top, Subalgebra.rank_eq_one_iff, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free F E
this : Free.{u_1, u_2} F ↥⊤
rw : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Module.rank F ↥⊤ = 1
rw₁ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥
⊢ Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Module.rank F E = 1
have rw₂ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥ ↔ Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥
Tactic: rw [← rank_top, Subalgebra.rank_eq_one_iff, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free F E
⊢ Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank F E = 1
have this : Free.{u_1, u_2} F ↥⊤
Tactic: haveI := Module.Free.of_equiv (Subalgebra.topEquiv (R := F) (A := E)).toLinearEquiv.symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free F E
this : Free.{u_1, u_2} F ↥⊤
⊢ Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank F E = 1
have rw : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank.{u_1, u_2} F ↥⊤ = 1
Tactic: rw [← finrank_top, ← subalgebra_top_finrank_eq_submodule_top_finrank,
    Subalgebra.finrank_eq_one_iff, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free F E
this : Free.{u_1, u_2} F ↥⊤
rw : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank.{u_1, u_2} F ↥⊤ = 1
⊢ Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank F E = 1
have rw₁ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank.{u_1, u_2} F ↥⊤ = 1
Tactic: rw [← finrank_top, ← subalgebra_top_finrank_eq_submodule_top_finrank,
    Subalgebra.finrank_eq_one_iff, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free F E
this : Free.{u_1, u_2} F ↥⊤
rw : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank.{u_1, u_2} F ↥⊤ = 1
rw₁ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank.{u_1, u_2} F ↥⊤ = 1
⊢ Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank F E = 1
have rw₂ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥
Tactic: rw [← finrank_top, ← subalgebra_top_finrank_eq_submodule_top_finrank,
    Subalgebra.finrank_eq_one_iff, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free F E
this : Free.{u_1, u_2} F ↥⊤
rw : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank.{u_1, u_2} F ↥⊤ = 1
rw₁ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank.{u_1, u_2} F ↥⊤ = 1
rw₂ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥
⊢ Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤ ↔ finrank F E = 1
have rw₃ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥ ↔ Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥
Tactic: rw [← finrank_top, ← subalgebra_top_finrank_eq_submodule_top_finrank,
    Subalgebra.finrank_eq_one_iff, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Free F E
⊢ finrank F E = 1 ↔ Function.Bijective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)
have refine : finrank F E = 1 → Function.Bijective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)
Tactic: refine ⟨?_, Module.finrank_of_bijective_algebraMap⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Free F E
⊢ finrank F E = 1 → Function.Bijective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)
have a : Nontrivial E
Tactic: nontriviality E
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Free F E
h : Nontrivial E
⊢ finrank F E = 1 → Function.Bijective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)
have refine : ∀ (h : finrank F E = 1), Function.Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)
Tactic: refine fun h ↦ ⟨FaithfulSMul.algebraMap_injective F E, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Free F E
h_1 : Nontrivial E
h : finrank F E = 1
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)
have rwa : Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥
Tactic: rwa [Algebra.surjective_algebraMap_iff, eq_comm, Subalgebra.bot_eq_top_iff_finrank_eq_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Free F E
h_1 : Nontrivial E
h : finrank F E = 1
rwa : Eq.{u_2 + 1} (α := Subalgebra F E) ⊤ ⊥
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑(algebraMap F E) : (a : F) → E)
have rwa₁ : Eq.{u_2 + 1} (α := Subalgebra F E) ⊥ ⊤
Tactic: rwa [Algebra.surjective_algebraMap_iff, eq_comm, Subalgebra.bot_eq_top_iff_finrank_eq_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
Goal:
K : Type u
V : Type v
V' : Type v'
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
inst_5 : Nontrivial K
⊢ rank.{u, v, v'} (K := K) (V := V) (V' := V') 0 = 0
have rw : Module.rank K ↥(range.{u, u, v, v'} (R := K) (M := V) (τ₁₂ := RingHom.id K) 0) = 0
Tactic: rw [rank, LinearMap.range_zero, rank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
Goal:
K : Type u
V : Type v
V' : Type v'
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
inst_5 : Nontrivial K
rw : Module.rank K ↥(range.{u, u, v, v'} (R := K) (M := V) (τ₁₂ := RingHom.id K) 0) = 0
⊢ rank.{u, v, v'} (K := K) (V := V) (V' := V') 0 = 0
have rw₁ : Module.rank K ↥⊥ = 0
Tactic: rw [rank, LinearMap.range_zero, rank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
Goal:
K : Type u
V : Type v
V' : Type v'
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
inst_5 : Nontrivial K
rw : Module.rank K ↥(range.{u, u, v, v'} (R := K) (M := V) (τ₁₂ := RingHom.id K) 0) = 0
rw₁ : Module.rank K ↥⊥ = 0
⊢ rank.{u, v, v'} (K := K) (V := V) (V' := V') 0 = 0
have rw₂ : Eq.{v' + 2} (α := Cardinal.{v'}) 0 0
Tactic: rw [rank, LinearMap.range_zero, rank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
Goal:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
inst_5 : AddCommGroup V''
inst_6 : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ (f ∘ₗ g).rank ≤ f.rank
have refine : (f ∘ₗ g).range ≤ f.range
Tactic: refine Submodule.rank_mono ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
Goal:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
inst_5 : AddCommGroup V''
inst_6 : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ (f ∘ₗ g).range ≤ f.range
have rw : Submodule.map f g.range ≤ f.range
Tactic: rw [LinearMap.range_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
Goal:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst : Ring K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
inst_5 : AddCommGroup V''
inst_6 : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ lift.{v', v''} (f ∘ₗ g).rank ≤ lift.{v'', v'} g.rank
have rw : lift.{v', v''} (Module.rank K ↥(Submodule.map f g.range)) ≤ lift.{v'', v'} (Module.rank K ↥g.range)
Tactic: rw [rank, rank, LinearMap.range_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
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 g : V →ₗ[K] V'
⊢ (f + g).rank ≤ Module.rank K ↥(f.range ⊔ g.range)
have refine : (f + g).range ≤ f.range ⊔ g.range
Tactic: refine Submodule.rank_mono ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
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'
⊢ c ≤ f.rank ↔
    ∃ (s : Set V),
      lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
have rcases : ∀ (g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V) (hg : f.rangeRestrict ∘ₗ g = id),
  c ≤ f.rank ↔
    ∃ (s : Set V),
      lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
Tactic: rcases f.rangeRestrict.exists_rightInverse_of_surjective f.range_rangeRestrict with ⟨g, hg⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (hypothesis)
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
⊢ c ≤ f.rank ↔
    ∃ (s : Set V),
      lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
have fg : LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
Tactic: have fg : LeftInverse f.rangeRestrict g := LinearMap.congr_fun hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
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)
⊢ c ≤ f.rank ↔
    ∃ (s : Set V),
      lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
have refine_1 : ∀ (h : c ≤ f.rank),
  ∃ (s : Set V),
    lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
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)
refine_1 :
  ∀ (h : c ≤ f.rank),
    ∃ (s : Set V),
      lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
⊢ c ≤ f.rank ↔
    ∃ (s : Set V),
      lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
have refine_2 : (∃ (s : Set V),
    lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s) →
  c ≤ f.rank
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
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)
h : c ≤ f.rank
⊢ ∃ (s : Set V),
    lift.{v', v} #(↑s : Type v) = lift.{v, v'} c ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
have refine_1 : ∀ (s : Set ↥f.range) (si : LinearIndepOn K _root_.id s) (h : #(↑s : Type v') ≤ f.rank),
  ∃ (s_1 : Set V),
    lift.{v', v} #(↑s_1 : Type v) = lift.{v, v'} #(↑s : Type v') ∧
      LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s_1
Tactic: rcases _root_.le_rank_iff_exists_linearIndependent.1 h with ⟨s, rfl, si⟩
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
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
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set ↥f.range
si : LinearIndepOn K _root_.id s
h : #(↑s : Type v') ≤ f.rank
⊢ ∃ (s_1 : Set V),
    lift.{v', v} #(↑s_1 : Type v) = lift.{v, v'} #(↑s : Type v') ∧
      LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s_1
have refine_1 : LinearIndepOn.{v, u, v'} (ι := V) K (M := V') (⇑f : (a : V) → V') ((⇑g : (a : ↥f.range) → V) '' s)
Tactic: refine ⟨g '' s, Cardinal.mk_image_eq_lift _ _ fg.injective, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (hypothesis)
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
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set ↥f.range
si : LinearIndepOn K _root_.id s
h : #(↑s : Type v') ≤ f.rank
⊢ LinearIndepOn.{v, u, v'} (ι := V) K (M := V') (⇑f : (a : V) → V') ((⇑g : (a : ↥f.range) → V) '' s)
have fg₁ : ∀ (x : ↥f.range), (f : (a : V) → V') ((g : (a : ↥f.range) → V) x : V) = (↑x : V')
Tactic: replace fg : ∀ x, f (g x) = x := by
      intro x
      convert! congr_arg Subtype.val (fg x)
Cleared hypotheses: fg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (hypothesis)
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.{v, u, v'} (ι := V) K (M := V') (⇑f : (a : V) → V') ((⇑g : (a : ↥f.range) → V) '' s)
have si₁ : 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 _)
Cleared hypotheses: si
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (hypothesis)
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
⊢ c ≤ f.rank
have this : 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
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
⊢ c ≤ f.rank
have h : c = #(↑((⇑f.rangeRestrict : (a : V) → ↥f.range) '' s) : Type v')
Tactic: convert! this.id_image.cardinal_le_rank