awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
F : Type u
K : Type v
A : Type w
inst : Semiring F
inst_1 : Semiring K
inst_2 : AddCommMonoid A
inst_3 : Module F K
inst_4 : Module K A
inst_5 : Module F A
inst_6 : IsScalarTower F K A
inst_7 : StrongRankCondition F
inst_8 : StrongRankCondition K
inst_9 : Free F K
inst_10 : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
rw : lift.{w, v} (lift.{v, v} (Module.rank F K)) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
rw₁ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
rw₂ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (lift.{w, w} (Module.rank K A)) =
    lift.{v, w} (Module.rank F A)
rw₃ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{v, w} (Module.rank F A)
rw₄ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{max w v, w} (Module.rank F A)
rw₅ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} #(Prod.{v, w} (Free.ChooseBasisIndex F K) (Free.ChooseBasisIndex K A))
rw₆ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{v, w} #(Free.ChooseBasisIndex K A))
rw₇ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
rw₈ :
  lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
rw₉ :
  lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
have rw₁₀ : lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
  lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
Tactic: rw [← (Module.rank F K).lift_id, ← b.mk_eq_rank, ← (Module.rank K A).lift_id, ← c.mk_eq_rank,
    ← lift_umax.{w, v}, ← (b.smulTower c).mk_eq_rank, mk_prod, lift_mul, lift_lift, lift_lift,
    lift_lift, lift_lift, lift_umax.{v, w}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
F : Type u
K : Type v
A : Type w
inst : Semiring F
inst_1 : Semiring K
inst_2 : AddCommMonoid A
inst_3 : Module F K
inst_4 : Module K A
inst_5 : Module F A
inst_6 : IsScalarTower F K A
inst_7 : StrongRankCondition F
inst_8 : StrongRankCondition K
inst_9 : Free F K
inst_10 : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
rw : lift.{w, v} (lift.{v, v} (Module.rank F K)) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
rw₁ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
rw₂ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (lift.{w, w} (Module.rank K A)) =
    lift.{v, w} (Module.rank F A)
rw₃ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{v, w} (Module.rank F A)
rw₄ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{max w v, w} (Module.rank F A)
rw₅ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} #(Prod.{v, w} (Free.ChooseBasisIndex F K) (Free.ChooseBasisIndex K A))
rw₆ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{v, w} #(Free.ChooseBasisIndex K A))
rw₇ :
  lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
rw₈ :
  lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
rw₉ :
  lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
rw₁₀ :
  lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
    lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
have rw₁₁ : lift.{max v w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A) =
  lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{max v w, w} #(Free.ChooseBasisIndex K A)
Tactic: rw [← (Module.rank F K).lift_id, ← b.mk_eq_rank, ← (Module.rank K A).lift_id, ← c.mk_eq_rank,
    ← lift_umax.{w, v}, ← (b.smulTower c).mk_eq_rank, mk_prod, lift_mul, lift_lift, lift_lift,
    lift_lift, lift_lift, lift_umax.{v, w}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
F : Type u
K : Type v
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : StrongRankCondition F
inst_4 : StrongRankCondition K
inst_5 : Free F K
A : Type v
inst_6 : AddCommMonoid A
inst_7 : Module K A
inst_8 : Module F A
inst_9 : IsScalarTower F K A
inst_10 : Free K A
⊢ Module.rank F K * Module.rank K A = Module.rank F A
have h : Module.rank F K = lift.{v, v} (Module.rank F K)
Tactic: convert! lift_rank_mul_lift_rank F K A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
F : Type u
K : Type v
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : StrongRankCondition F
inst_4 : StrongRankCondition K
inst_5 : Free F K
A : Type v
inst_6 : AddCommMonoid A
inst_7 : Module K A
inst_8 : Module F A
inst_9 : IsScalarTower F K A
inst_10 : Free K A
h : Module.rank F K = lift.{v, v} (Module.rank F K)
⊢ Module.rank F K * Module.rank K A = Module.rank F A
have h₁ : Module.rank K A = lift.{v, v} (Module.rank K A)
Tactic: convert! lift_rank_mul_lift_rank F K A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
F : Type u
K : Type v
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : StrongRankCondition F
inst_4 : StrongRankCondition K
inst_5 : Free F K
A : Type v
inst_6 : AddCommMonoid A
inst_7 : Module K A
inst_8 : Module F A
inst_9 : IsScalarTower F K A
inst_10 : Free K A
h : Module.rank F K = lift.{v, v} (Module.rank F K)
h₁ : Module.rank K A = lift.{v, v} (Module.rank K A)
⊢ Module.rank F K * Module.rank K A = Module.rank F A
have h₂ : Module.rank F A = lift.{v, v} (Module.rank F A)
Tactic: convert! lift_rank_mul_lift_rank F K A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
F : Type u
K : Type v
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : StrongRankCondition F
inst_4 : StrongRankCondition K
inst_5 : Free F K
A : Type v
inst_6 : AddCommMonoid A
inst_7 : Module K A
inst_8 : Module F A
inst_9 : IsScalarTower F K A
inst_10 : Free K A
⊢ Module.rank F K = lift.{v, v} (Module.rank F K)
have h : Module.rank F K = Module.rank F K
Tactic: rw [lift_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
F : Type u
K : Type v
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : StrongRankCondition F
inst_4 : StrongRankCondition K
inst_5 : Free F K
A : Type v
inst_6 : AddCommMonoid A
inst_7 : Module K A
inst_8 : Module F A
inst_9 : IsScalarTower F K A
inst_10 : Free K A
⊢ Module.rank K A = lift.{v, v} (Module.rank K A)
have h : Module.rank K A = Module.rank K A
Tactic: rw [lift_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
F : Type u
K : Type v
inst : Semiring F
inst_1 : Semiring K
inst_2 : Module F K
inst_3 : StrongRankCondition F
inst_4 : StrongRankCondition K
inst_5 : Free F K
A : Type v
inst_6 : AddCommMonoid A
inst_7 : Module K A
inst_8 : Module F A
inst_9 : IsScalarTower F K A
inst_10 : Free K A
⊢ Module.rank F A = lift.{v, v} (Module.rank F A)
have h : Module.rank F A = Module.rank F A
Tactic: rw [lift_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
F : Type u
K : Type v
A : Type w
inst : Semiring F
inst_1 : Semiring K
inst_2 : AddCommMonoid A
inst_3 : Module F K
inst_4 : Module K A
inst_5 : Module F A
inst_6 : IsScalarTower F K A
inst_7 : StrongRankCondition F
inst_8 : StrongRankCondition K
inst_9 : Free F K
inst_10 : Free K A
⊢ HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank F K) : ℕ)
      ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank K A) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
have rw : HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank F K)) : ℕ)
    ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank K A) : ℕ) =
  (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
Tactic: rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul,
    lift_rank_mul_lift_rank, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
F : Type u
K : Type v
A : Type w
inst : Semiring F
inst_1 : Semiring K
inst_2 : AddCommMonoid A
inst_3 : Module F K
inst_4 : Module K A
inst_5 : Module F A
inst_6 : IsScalarTower F K A
inst_7 : StrongRankCondition F
inst_8 : StrongRankCondition K
inst_9 : Free F K
inst_10 : Free K A
rw :
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank F K)) : ℕ)
      ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank K A) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
⊢ HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank F K) : ℕ)
      ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank K A) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
have rw₁ : HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank F K)) : ℕ)
    ((toNat : (a : Cardinal.{max v w}) → ℕ) (lift.{v, w} (Module.rank K A)) : ℕ) =
  (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
Tactic: rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul,
    lift_rank_mul_lift_rank, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
F : Type u
K : Type v
A : Type w
inst : Semiring F
inst_1 : Semiring K
inst_2 : AddCommMonoid A
inst_3 : Module F K
inst_4 : Module K A
inst_5 : Module F A
inst_6 : IsScalarTower F K A
inst_7 : StrongRankCondition F
inst_8 : StrongRankCondition K
inst_9 : Free F K
inst_10 : Free K A
rw :
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank F K)) : ℕ)
      ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank K A) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
rw₁ :
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank F K)) : ℕ)
      ((toNat : (a : Cardinal.{max v w}) → ℕ) (lift.{v, w} (Module.rank K A)) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
⊢ HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank F K) : ℕ)
      ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank K A) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
have rw₂ : Eq (α := ℕ) ((toNat : (a : Cardinal.{max v w}) → ℕ) (lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A)) : ℕ)
  ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A) : ℕ)
Tactic: rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul,
    lift_rank_mul_lift_rank, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
F : Type u
K : Type v
A : Type w
inst : Semiring F
inst_1 : Semiring K
inst_2 : AddCommMonoid A
inst_3 : Module F K
inst_4 : Module K A
inst_5 : Module F A
inst_6 : IsScalarTower F K A
inst_7 : StrongRankCondition F
inst_8 : StrongRankCondition K
inst_9 : Free F K
inst_10 : Free K A
rw :
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank F K)) : ℕ)
      ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank K A) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
rw₁ :
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank F K)) : ℕ)
      ((toNat : (a : Cardinal.{max v w}) → ℕ) (lift.{v, w} (Module.rank K A)) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
rw₂ :
  Eq (α := ℕ)
    ((toNat : (a : Cardinal.{max v w}) → ℕ) (lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A)) : ℕ)
    ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A) : ℕ)
⊢ HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank F K) : ℕ)
      ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank K A) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
have rw₃ : Eq (α := ℕ) ((toNat : (a : Cardinal.{max v w}) → ℕ) (lift.{v, w} (Module.rank F A)) : ℕ)
  ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A) : ℕ)
Tactic: rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul,
    lift_rank_mul_lift_rank, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
F : Type u
K : Type v
A : Type w
inst : Semiring F
inst_1 : Semiring K
inst_2 : AddCommMonoid A
inst_3 : Module F K
inst_4 : Module K A
inst_5 : Module F A
inst_6 : IsScalarTower F K A
inst_7 : StrongRankCondition F
inst_8 : StrongRankCondition K
inst_9 : Free F K
inst_10 : Free K A
rw :
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank F K)) : ℕ)
      ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank K A) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
rw₁ :
  HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{max w v}) → ℕ) (lift.{w, v} (Module.rank F K)) : ℕ)
      ((toNat : (a : Cardinal.{max v w}) → ℕ) (lift.{v, w} (Module.rank K A)) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
rw₂ :
  Eq (α := ℕ)
    ((toNat : (a : Cardinal.{max v w}) → ℕ) (lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A)) : ℕ)
    ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A) : ℕ)
rw₃ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max v w}) → ℕ) (lift.{v, w} (Module.rank F A)) : ℕ)
    ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A) : ℕ)
⊢ HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank F K) : ℕ)
      ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank K A) : ℕ) =
    (toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A)
have rw₄ : Eq (α := ℕ) ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A) : ℕ)
  ((toNat : (a : Cardinal.{w}) → ℕ) (Module.rank F A) : ℕ)
Tactic: rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul,
    lift_rank_mul_lift_rank, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
cnd : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} #ι
⊢ ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')
have a : Nontrivial M
Tactic: nontriviality M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
cnd : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} #ι
h : Nontrivial M
⊢ ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')
have this : Nontrivial R
Tactic: have := Module.nontrivial R M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
cnd : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} #ι
h : Nontrivial M
this : Nontrivial R
⊢ ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')
have rcases : ∀ (w : Set M) (B : Basis (↑w : Type v) R M),
  ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')
Tactic: rcases Module.Free.exists_set R M with ⟨_, ⟨B⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
cnd : lift.{w, v} (Module.rank R M) ≤ lift.{v, w} #ι
h : Nontrivial M
this : Nontrivial R
w : Set M
B : Basis (↑w : Type v) R M
⊢ ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')
have cnd₁ : lift.{w, v} #(↑w : Type v) ≤ lift.{v, w} #ι
Tactic: replace cnd := (Cardinal.lift_le.2 B.linearIndependent.cardinal_le_rank).trans cnd
Cleared hypotheses: cnd
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
h : Nontrivial M
this : Nontrivial R
w : Set M
B : Basis (↑w : Type v) R M
cnd : lift.{w, v} #(↑w : Type v) ≤ lift.{v, w} #ι
⊢ ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')
have cnd₁ : Nonempty (Embedding.{v + 1, w + 1} (↑w : Type v) ι)
Tactic: rw [Cardinal.lift_mk_le'] at cnd
Cleared hypotheses: cnd
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
ι : Type w
v : ι → N'
hv : LinearIndependent R v
h : Nontrivial M
this : Nontrivial R
w : Set M
B : Basis (↑w : Type v) R M
cnd : Nonempty (Embedding.{v + 1, w + 1} (↑w : Type v) ι)
⊢ ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')
have rcases : ∀ (i : (↑w : Type v) → ι) (hi : Injective i),
  ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')
Tactic: rcases cnd with ⟨i, hi⟩
Cleared hypotheses: cnd
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
N' : Type v'
inst_4 : AddCommMonoid N'
inst_5 : Module R N'
cnd : lift.{v', v} (Module.rank R M) < lift.{v, v'} (Module.rank R N')
⊢ ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')
have rcases : ∀ (s : Set N') (hs : lift.{v, v'} #(↑s : Type v') = lift.{v', v} (Module.rank R M)) (hs₂ : LinearIndepOn R id s),
  ∃ (f : M →ₗ[R] N'), Injective.{v + 1, v' + 1} (α := M) (β := N') (⇑f : (a : M) → N')
Tactic: rcases exists_set_linearIndependent_of_lt_lift_rank cnd with ⟨s, hs, hs₂⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
inst_5 : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
⊢ Module.rank R M = #M
have this : Infinite M
Tactic: have : Infinite M := infinite_iff.mpr <| lift_le.mp <| le_trans (by simp) h_lt.le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
inst_5 : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
⊢ Module.rank R M = #M
have h : lift.{max u v, v} #M = lift.{v, max u v} #(Finsupp.{v, u} (ChooseBasisIndex R M) R)
Tactic: have h : lift #M = lift #(ChooseBasisIndex R M →₀ R) := lift_mk_eq'.mpr ⟨(chooseBasis R M).repr⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
inst_5 : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
h : lift.{max u v, v} #M = lift.{v, max u v} #(Finsupp.{v, u} (ChooseBasisIndex R M) R)
⊢ Module.rank R M = #M
have h₁ : lift.{max u v, v} #M = max (lift.{max u v, v} (Module.rank R M)) (lift.{v, u} #R)
Tactic: simp only [mk_finsupp_lift_of_infinite', ← rank_eq_card_chooseBasisIndex, lift_max,
    lift_lift] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
inst_5 : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
h : lift.{max u v, v} #M = max (lift.{max u v, v} (Module.rank R M)) (lift.{v, u} #R)
⊢ Module.rank R M = #M
have refine : ¬lift.{v, u} #R = lift.{max u v, v} #M
Tactic: refine lift_inj.mp ((max_eq_iff.mp h.symm).resolve_right <| not_and_of_not_left _ ?_).left
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
h : lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')
⊢ ∃ (f : M →ₗ[R] M'), Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑f : (a : M) → M')
have rcases : ∀ (w : Set M') (B : Basis (↑w : Type v') R M'),
  ∃ (f : M →ₗ[R] M'), Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑f : (a : M) → M')
Tactic: rcases Module.Free.exists_set R M' with ⟨_, ⟨B⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
⊢ Nonempty (M ≃ₗ[R] M')
have obtain : ∀ (α : Type v) (B : Basis α R M), Nonempty (M ≃ₗ[R] M')
Tactic: obtain ⟨⟨α, B⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : Free R M'
inst_7 : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
⊢ Nonempty (M ≃ₗ[R] M')
have obtain : ∀ (β : Type v') (B' : Basis β R M'), Nonempty (M ≃ₗ[R] M')
Tactic: obtain ⟨⟨β, B'⟩⟩ := Module.Free.exists_basis (R := R) (M := M')