awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M'_1 : Type u_7
M''_1 : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'_1
inst_4 : Module R_1 M'_1
ι : Type u_10
R_2 : Type u_11
M_2 : Type u_12
inst_5 : Semiring R_2
inst_6 : AddCommMonoid M_2
inst_7 : Module R_2 M_2
b_1 : Basis ι R_2 M_2
inst_8 : Module R_2 M'_1
i_1 : ι
M'' : Type u_13
b'_1 : Basis ι' R_2 M'_1
e : ι ≃ ι'
inst_9 : AddCommMonoid M''
inst_10 : Module R_2 M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst_11 : CommSemiring R
inst_12 : AddCommMonoid M
inst_13 : Module R M
inst_14 : AddCommMonoid M'
inst_15 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst_16 : SMulCommClass R R M'
f : M → M'
g : M' → M
hf :
  ∀ (i : ι),
    Membership.mem (γ := Set M') (range.{u_16, u_2 + 1} (ι := ι') (⇑b' : (a : ι') → M')) (f ((b : (a : ι) → M) i))
hg :
  ∀ (i : ι'),
    Membership.mem (γ := Set M) (range.{u_15, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) (g ((b' : (a : ι') → M') i))
hgf : ∀ (i : ι), g (f ((b : (a : ι) → M) i)) = (b : (a : ι) → M) i
hfg : ∀ (i : ι'), f (g ((b' : (a : ι') → M') i)) = (b' : (a : ι') → M') i
i : ι'
i' : ι
hi' : (b : (a : ι) → M) i' = g ((b' : (a : ι') → M') i)
rw :
  Eq.{u_16 + 1} (α := M')
    ((((b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) : M →ₗ[R] M') : (a : M) → M')
        ((((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) : M' →ₗ[R] M) : (a : M') → M)
            ((b' : (a : ι') → M') i : M') :
          M) :
      M')
    ((LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M') : M')
rw₁ :
  Eq.{u_16 + 1} (α := M')
    ((((b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) : M →ₗ[R] M') : (a : M) → M')
        ((g ∘ (⇑b' : (a : ι') → M')) i) :
      M')
    ((LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M') : M')
rw₂ :
  Eq.{u_16 + 1} (α := M')
    ((((b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) : M →ₗ[R] M') : (a : M) → M')
        (g ((b' : (a : ι') → M') i)) :
      M')
    ((LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M') : M')
rw₃ :
  Eq.{u_16 + 1} (α := M')
    ((((b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) : M →ₗ[R] M') : (a : M) → M')
        ((b : (a : ι) → M) i' : M) :
      M')
    ((LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M') : M')
rw₄ : (f ∘ (⇑b : (a : ι) → M)) i' = (LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M')
⊢ Eq.{u_16 + 1} (α := M')
    (((b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) ∘ₗ
            (b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) :
          (a : M') → M')
        ((b' : (a : ι') → M') i : M') :
      M')
    ((LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M') : M')
have rw₅ : f ((b : (a : ι) → M) i') = (LinearMap.id : (a : M') → M') ((b' : (a : ι') → M') i : M')
Tactic: rw [LinearMap.comp_apply, b'.constr_basis, Function.comp_apply, ← hi', b.constr_basis,
              Function.comp_apply, hi', hfg, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
ι' : Type u_17
inst_3 : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
| ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
have rw : (((b.repr : (a : M) → ι →₀ R)
        (∑ i : ι',
          HSMul.hSMul.{u_14, u_15, u_15} (α := R) (β := M)
            ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) i : R) ((b' : (a : ι') → M) i : M)) :
      (a : ι) → R)
    i :
  R)
Tactic: rw [← b'.sum_repr x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
ι' : Type u_17
inst_3 : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ Eq.{u_14 + 1} (α := R)
    (∑ j : ι',
        HMul.hMul (α := R) (β := R)
          ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
          ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) :
      R)
    ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
have conv_rhs : Eq.{u_14 + 1} (α := R)
  (∑ j : ι',
      HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
        ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) :
    R)
  (((b.repr : (a : M) → ι →₀ R)
          (∑ i : ι',
            HSMul.hSMul.{u_14, u_15, u_15} (α := R) (β := M)
              ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) i : R) ((b' : (a : ι') → M) i : M)) :
        (a : ι) → R)
      i :
    R)
Tactic: conv_rhs => rw [← b'.sum_repr x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
ι' : Type u_17
inst_3 : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ Eq.{u_14 + 1} (α := R)
    (∑ j : ι',
        HMul.hMul (α := R) (β := R)
          ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
          ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) :
      R)
    (((b.repr : (a : M) → ι →₀ R)
            (∑ i : ι',
              HSMul.hSMul.{u_14, u_15, u_15} (α := R) (β := M)
                ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) i : R) ((b' : (a : ι') → M) i : M)) :
          (a : ι) → R)
        i :
      R)
have simp_rw : Eq.{u_14 + 1} (α := R)
  (∑ j : ι',
    HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
      ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R))
  (∑ k : ι',
    (HSMul.hSMul (α := R) (β := ι →₀ R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) k : R)
          ((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) k) : ι →₀ R) :
        (a : ι) → R)
      i)
Tactic: simp_rw [map_sum, map_smul, Finset.sum_apply']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
ι' : Type u_17
inst_3 : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ Eq.{u_14 + 1} (α := R)
    (∑ j : ι',
      HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
        ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R))
    (∑ k : ι',
      (HSMul.hSMul (α := R) (β := ι →₀ R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) k : R)
            ((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) k) : ι →₀ R) :
          (a : ι) → R)
        i)
have refine : ∀ (j : ι'),
  Membership.mem (γ := Finset ι') Finset.univ j →
    HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
        ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) =
      (HSMul.hSMul (α := R) (β := ι →₀ R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
            ((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) :
          (a : ι) → R)
        i
Tactic: refine Finset.sum_congr rfl fun j _ => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
ι' : Type u_17
inst_3 : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
j : ι'
h : Membership.mem (γ := Finset ι') Finset.univ j
⊢ HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
      ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) =
    (HSMul.hSMul (α := R) (β := ι →₀ R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
          ((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) :
        (a : ι) → R)
      i
have rw : HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
    ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) =
  HSMul.hSMul (α := R) (β := R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
    ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
Tactic: rw [Finsupp.smul_apply, smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
ι' : Type u_17
inst_3 : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
j : ι'
h : Membership.mem (γ := Finset ι') Finset.univ j
rw :
  HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
      ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) =
    HSMul.hSMul (α := R) (β := R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
      ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
⊢ HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
      ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) =
    (HSMul.hSMul (α := R) (β := ι →₀ R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
          ((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) :
        (a : ι) → R)
      i
have rw₁ : HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
    ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) =
  HMul.hMul (α := R) (β := R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
    ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
Tactic: rw [Finsupp.smul_apply, smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
ι' : Type u_17
inst_3 : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
j : ι'
h : Membership.mem (γ := Finset ι') Finset.univ j
rw :
  HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
      ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) =
    HSMul.hSMul (α := R) (β := R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
      ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
rw₁ :
  HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
      ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) =
    HMul.hMul (α := R) (β := R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
      ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
⊢ HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
      ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) =
    (HSMul.hSMul (α := R) (β := ι →₀ R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
          ((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) :
        (a : ι) → R)
      i
have rw₂ : HMul.hMul (α := R) (β := R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
    ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R) =
  HMul.hMul (α := R) (β := R) ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R)
    ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
Tactic: rw [Finsupp.smul_apply, smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
inst_3 : Fintype ι
⊢ Eq (α := (a : M) → R) (⇑b.sumCoords : (a : M) → R) (⇑(∑ i : ι, b.coord i) : (a : M) → R)
have h : ∀ (m : M), Eq.{u_11 + 1} (α := R) ((b.sumCoords : (a : M) → R) m : R) ((∑ i : ι, b.coord i : (a : M) → R) m : R)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
⊢ Eq (α := (a : M) → R) (⇑b.sumCoords : (a : M) → R) fun (m : M) ↦ ∑ᶠ (i : ι), (b.coord i : (a : M) → R) m
have h : ∀ (m : M), Eq.{u_11 + 1} (α := R) ((b.sumCoords : (a : M) → R) m : R) (∑ᶠ (i : ι), (b.coord i : (a : M) → R) m : R)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι' : Type u_2
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
e : ι ≃ ι'
⊢ (b.reindex e).sumCoords = b.sumCoords
have h : ∀ (x : M), Eq.{u_11 + 1} (α := R) (((b.reindex e).sumCoords : (a : M) → R) x : R) ((b.sumCoords : (a : M) → R) x : R)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι' : Type u_2
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
e : ι ≃ ι'
x : M
⊢ Eq.{u_11 + 1} (α := R) (((b.reindex e).sumCoords : (a : M) → R) x : R) ((b.sumCoords : (a : M) → R) x : R)
have h : Eq.{u_11 + 1} (α := R)
  (sum (M := R) (mapDomain.{u_10, u_2, u_11} (α := ι) (⇑e : (a : ι) → ι') ((b.repr : (a : M) → ι →₀ R) x))
    fun (x : ι') ↦ id)
  (sum (M := R) ((b.repr : (a : M) → ι →₀ R) x) fun (x : ι) ↦ id)
Tactic: simp only [coe_sumCoords, repr_reindex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} (Module.rank R M)
have rw : lift.{v, w} #ι ≤ lift.{w, v} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
Tactic: rw [Module.rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
have refine : lift.{v, w} #ι ≤
  lift.{w, v} #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) (range v) sorry) : Set M) : Type v)
Tactic: refine le_trans ?_ (lift_le.mpr <| le_ciSup bddAbove_of_small ⟨_, hv.linearIndepOn_id⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : Cardinal.{w}
h : lift.{v, w} c < lift.{w, v} (Module.rank R M)
⊢ ∃ (s : Set M), lift.{w, v} #(↑s : Type v) = lift.{v, w} c ∧ LinearIndepOn R id s
have rcases : ∀ (c' : Cardinal.{v}) (hc' : c' < Module.rank R M) (hcc' : lift.{w, v} c' = lift.{v, w} c),
  ∃ (s : Set M), lift.{w, v} #(↑s : Type v) = lift.{v, w} c ∧ LinearIndepOn R id s
Tactic: rcases Cardinal.lt_lift_iff.mp h with ⟨c', hc', hcc'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : Cardinal.{w}
h : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
⊢ ∃ (s : Set M), lift.{w, v} #(↑s : Type v) = lift.{v, w} c ∧ LinearIndepOn R id s
have rcases : ∀ (s : Set M) (hs : LinearIndepOn R id s)
  (h : c' < #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v)),
  ∃ (s : Set M), lift.{w, v} #(↑s : Type v) = lift.{v, w} c ∧ LinearIndepOn R id s
Tactic: rcases exists_lt_of_lt_ciSup (by simpa [← hcc', Module.rank_def] using h) with ⟨⟨s, hs⟩, h⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : Cardinal.{w}
h_1 : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
s : Set M
hs : LinearIndepOn R id s
h : c' < #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v)
⊢ ∃ (s : Set M), lift.{w, v} #(↑s : Type v) = lift.{v, w} c ∧ LinearIndepOn R id s
have rcases : ∀ (t : Set M) (hst : t ⊆ (↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M))
  (ht : #(↑t : Type v) = c'), ∃ (s : Set M), lift.{w, v} #(↑s : Type v) = lift.{v, w} c ∧ LinearIndepOn R id s
Tactic: rcases Cardinal.le_mk_iff_exists_subset.mp h.le with ⟨t, hst, ht⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
le : (↑n : Cardinal.{v}) ≤ Module.rank R M
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
have contrapose! : ∀ (le : ∀ (s : Finset M) (_ : s.card = n), ¬LinearIndepOn R id (↑s : Set M)), Module.rank R M < (↑n : Cardinal.{v})
Tactic: contrapose! le
Cleared hypotheses: le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
le : ∀ (s : Finset M) (_ : s.card = n), ¬LinearIndepOn R id (↑s : Set M)
⊢ Module.rank R M < (↑n : Cardinal.{v})
have zero : ∀ (le : ∀ (s : Finset M) (_ : s.card = 0), ¬LinearIndepOn R id (↑s : Set M)), Module.rank R M < (↑0 : Cardinal.{v})
Tactic: obtain _ | n := n
Cleared hypotheses: n, le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
le : ∀ (s : Finset M) (_ : s.card = n), ¬LinearIndepOn R id (↑s : Set M)
zero :
  ∀ (le : ∀ (s : Finset M) (_ : s.card = 0), ¬LinearIndepOn R id (↑s : Set M)), Module.rank R M < (↑0 : Cardinal.{v})
⊢ Module.rank R M < (↑n : Cardinal.{v})
have succ : ∀ (n : ℕ) (le : ∀ (s : Finset M) (_ : s.card = n + 1), ¬LinearIndepOn R id (↑s : Set M)),
  Module.rank R M < (↑(n + 1) : Cardinal.{v})
Tactic: obtain _ | n := n
Cleared hypotheses: n, le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
le : ∀ (s : Finset M) (_ : s.card = n + 1), ¬LinearIndepOn R id (↑s : Set M)
⊢ Module.rank R M < (↑(n + 1) : Cardinal.{v})
have succ : ∀ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) ≤ (↑n : Cardinal.{v})
Tactic: rw [Module.rank, Nat.cast_add_one, lt_natCast_add_one_iff, ciSup_le_iff bddAbove_of_small]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
le : ∀ (s : Finset M) (_ : s.card = n + 1), ¬LinearIndepOn R id (↑s : Set M)
s : { s : Set M // LinearIndepOn R id s }
⊢ #(↑(↑s : Set M) : Type v) ≤ (↑n : Cardinal.{v})
have succ : ∀ (le : (↑n : Cardinal.{v}) < #(↑(↑s : Set M) : Type v)),
  ∃ (s : Finset M), s.card = n + 1 ∧ LinearIndepOn R id (↑s : Set M)
Tactic: contrapose! le
Cleared hypotheses: le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
s : { s : Set M // LinearIndepOn R id s }
le : (↑n : Cardinal.{v}) < #(↑(↑s : Set M) : Type v)
⊢ ∃ (s : Finset M), s.card = n + 1 ∧ LinearIndepOn R id (↑s : Set M)
have le₁ : (↑(n + 1) : Cardinal.{v}) ≤ #(↑(↑s : Set M) : Type v)
Tactic: rw [← natCast_add_one_le_iff, ← Nat.cast_add_one] at le
Cleared hypotheses: le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
s : { s : Set M // LinearIndepOn R id s }
le : (↑(n + 1) : Cardinal.{v}) ≤ #(↑(↑s : Set M) : Type v)
⊢ ∃ (s : Finset M), s.card = n + 1 ∧ LinearIndepOn R id (↑s : Set M)
have succ : ∀ (t : Finset (↑(↑s : Set M) : Type v)) (ht : n + 1 = t.card),
  ∃ (s : Finset M), s.card = n + 1 ∧ LinearIndepOn R id (↑s : Set M)
Tactic: have ⟨t, ht⟩ := exists_finset_eq_card le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
⊢ (↑n : Cardinal.{v}) ≤ Module.rank R M ↔ ∃ (v : Fin n → M), LinearIndependent R v
have refine_1 : (∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)) →
  ∀ (s : Finset M) (s_card : s.card = n) (s_ind : LinearIndepOn R id (↑s : Set M)),
    ∃ (v : Fin n → M), LinearIndependent R v
Tactic: refine le_rank_iff_exists_finset.trans ⟨fun ⟨s, s_card, s_ind⟩ ↦ ?_, fun ⟨v, v_ind⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
refine_1 :
  (∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)) →
    ∀ (s : Finset M) (s_card : s.card = n) (s_ind : LinearIndepOn R id (↑s : Set M)),
      ∃ (v : Fin n → M), LinearIndependent R v
⊢ (↑n : Cardinal.{v}) ≤ Module.rank R M ↔ ∃ (v : Fin n → M), LinearIndependent R v
have refine_2 : (∃ (v : Fin n → M), LinearIndependent R v) →
  ∀ (v : Fin n → M) (v_ind : LinearIndependent R v), ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
Tactic: refine le_rank_iff_exists_finset.trans ⟨fun ⟨s, s_card, s_ind⟩ ↦ ?_, fun ⟨v, v_ind⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
h : ∃ (v : Fin n → M), LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
have refine_2 : LinearIndepOn R id (↑(Finset.map { toFun := v, inj' := sorry : Fin n ↪ M } Finset.univ) : Set M)
Tactic: refine ⟨.map ⟨_, v_ind.injective⟩ .univ, by simp, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
⊢ (↑n : Cardinal.{v}) ≤ Module.rank R M ↔
    ∃ (f : (Fin n → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
have refine : (∃ (v : Fin n → M), LinearIndependent R v) →
  ∀ (v : Fin n → M) (v_ind : LinearIndependent R v),
    ∃ (f : (Fin n → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
Tactic: refine le_rank_iff.trans ⟨fun ⟨v, v_ind⟩ ↦ ?_, fun ⟨f, f_inj⟩ ↦
    ⟨_, (Module.Basis.ofEquivFun <| .refl ..).linearIndependent.map_injOn f f_inj.injOn⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
h : ∃ (v : Fin n → M), LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
⊢ ∃ (f : (Fin n → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
have this : Injective.{max 1 (u + 1), v + 1} (α := Fin n → R) (β := M)
  (comp (β := Fin n →₀ R) (⇑(Finsupp.linearCombination R v) : (a : Fin n →₀ R) → M)
    (⇑(LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R (Fin n))) : (a : Fin n → R) → Fin n →₀ R))
Tactic: have := Injective.comp v_ind (Finsupp.linearEquivFunOnFinite R ..).symm.injective