awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
i j : Fin n
hij : LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
⊢ i ≤ j
have by_contra! : ∀ (h : j < i), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h_1 : a ≠ b
σ : Equiv.Perm (Fin n)
h_2 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
i j : Fin n
hij : LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
h : j < i
⊢ False
have hij₁ : LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n)
Tactic: obtain rfl : i = j := σ.injective (le_antisymm hij (hσ h.le))
Cleared hypotheses: j, hij, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h_1 : a ≠ b
σ : Equiv.Perm (Fin n)
h_2 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
i j : Fin n
hij : LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
h : j < i
hij₁ : LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n)
⊢ False
have h₁ : i < i
Tactic: obtain rfl : i = j := σ.injective (le_antisymm hij (hσ h.le))
Cleared hypotheses: j, hij, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
⊢ a = b
have hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
Tactic: have hσ' : Monotone σ.symm := fun i j hij ↦ by
    obtain ⟨i, rfl⟩ := σ.surjective i
    obtain ⟨j, rfl⟩ := σ.surjective j
    simp only [Equiv.symm_apply_apply]
    by_contra! h
    obtain rfl : i = j := σ.injective (le_antisymm hij (hσ h.le))
    simp only [lt_self_iff_false] at h
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
⊢ σ = 1
have H : ∀ (i : Fin n), Eq (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((1 : (a : Fin n) → Fin n) i : Fin n)
Tactic: ext i : 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
⊢ a = b
have x₁ : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ 1
Tactic: obtain rfl : σ = 1 := by
    ext i : 1
    exact DFunLike.congr_fun (Subsingleton.elim (σ.toOrderIso hσ hσ') (OrderIso.refl _)) i
Cleared hypotheses: σ, h_1, h', this, hσ, hσ'
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
x₁ : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ 1
⊢ a = b
have h'₁ : ¬Eq.{u_1 + 1} (α := R)
    (∏ x_1 : Fin n,
      (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R) (x ((b : (a : Fin n) → ι) ((1 : (a : Fin n) → Fin n) x_1 : Fin n))))
    0
Tactic: obtain rfl : σ = 1 := by
    ext i : 1
    exact DFunLike.congr_fun (Subsingleton.elim (σ.toOrderIso hσ hσ') (OrderIso.refl _)) i
Cleared hypotheses: σ, h_1, h', this, hσ, hσ'
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
x₁ : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ 1
h'₁ :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((1 : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
⊢ a = b
have this₁ : Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
  (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑1 : (a : Fin n) → Fin n))
Tactic: obtain rfl : σ = 1 := by
    ext i : 1
    exact DFunLike.congr_fun (Subsingleton.elim (σ.toOrderIso hσ hσ') (OrderIso.refl _)) i
Cleared hypotheses: σ, h_1, h', this, hσ, hσ'
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
x₁ : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ 1
h'₁ :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((1 : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this₁ :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑1 : (a : Fin n) → Fin n))
⊢ a = b
have hσ₁ : Monotone (α := Fin n) (β := Fin n) (⇑1 : (a : Fin n) → Fin n)
Tactic: obtain rfl : σ = 1 := by
    ext i : 1
    exact DFunLike.congr_fun (Subsingleton.elim (σ.toOrderIso hσ hσ') (OrderIso.refl _)) i
Cleared hypotheses: σ, h_1, h', this, hσ, hσ'
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
x₁ : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ 1
h'₁ :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((1 : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this₁ :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑1 : (a : Fin n) → Fin n))
hσ₁ : Monotone (α := Fin n) (β := Fin n) (⇑1 : (a : Fin n) → Fin n)
⊢ a = b
have hσ'₁ : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm 1) : (a : Fin n) → Fin n)
Tactic: obtain rfl : σ = 1 := by
    ext i : 1
    exact DFunLike.congr_fun (Subsingleton.elim (σ.toOrderIso hσ hσ') (OrderIso.refl _)) i
Cleared hypotheses: σ, h_1, h', this, hσ, hσ'
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ 1
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((1 : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑1 : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑1 : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm 1) : (a : Fin n) → Fin n)
⊢ a = b
have h₁ : ∀ (x : Fin n), Eq (α := ι) ((a : (a : Fin n) → ι) x : ι) ((b : (a : Fin n) → ι) x : ι)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
⊢ S = ⊤
have bS_eq : let bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S;
bS = Basis.ofVectorSpace K ↥S
Tactic: set bS := Basis.ofVectorSpace K S with bS_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
⊢ S = ⊤
have this : LinearIndepOn.{v, u, v} (ι := V) K id
  (Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
Tactic: have : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K S) := by
    simpa [bS] using bS.linearIndependent.linearIndepOn_id.image
      (f := Submodule.subtype S) (by simp)
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this :
  LinearIndepOn.{v, u, v} (ι := V) K id
    (Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
⊢ S = ⊤
have b_eq : let b :=
  Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) this;
b =
  Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) this
Tactic: set b := Basis.extend this with b_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this :
  LinearIndepOn.{v, u, v} (ι := V) K id
    (Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
b : Basis
  (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
        (t := Set.univ) ⋯) :
    Type v)
  K V :=
  Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) this
b_eq :
  b =
    Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      this
i2 : Fintype
  (↑(Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) : Type v) :=
  ⋯.fintype (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
⊢ Fintype.card.{v}
      (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
            (t := Set.univ) ⋯) :
        Type v) ≤
    Fintype.card.{v}
      (↑(Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) : Type v)
have rw : Fintype.card.{v}
    (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
          (t := Set.univ) sorry) :
      Type v) ≤
  Fintype.card.{v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v)
Tactic: rw [Set.card_image_of_injective _ Subtype.coe_injective, ← finrank_eq_card_basis bS, ←
            finrank_eq_card_basis b, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this :
  LinearIndepOn.{v, u, v} (ι := V) K id
    (Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
b : Basis
  (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
        (t := Set.univ) ⋯) :
    Type v)
  K V :=
  Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) this
b_eq :
  b =
    Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      this
i2 : Fintype
  (↑(Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) : Type v) :=
  ⋯.fintype (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
rw :
  Fintype.card.{v}
      (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
            (t := Set.univ) ⋯) :
        Type v) ≤
    Fintype.card.{v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v)
⊢ Fintype.card.{v}
      (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
            (t := Set.univ) ⋯) :
        Type v) ≤
    Fintype.card.{v}
      (↑(Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) : Type v)
have rw₁ : Fintype.card.{v}
    (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
          (t := Set.univ) sorry) :
      Type v) ≤
  finrank.{u, v} K ↥S
Tactic: rw [Set.card_image_of_injective _ Subtype.coe_injective, ← finrank_eq_card_basis bS, ←
            finrank_eq_card_basis b, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this :
  LinearIndepOn.{v, u, v} (ι := V) K id
    (Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
b : Basis
  (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
        (t := Set.univ) ⋯) :
    Type v)
  K V :=
  Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) this
b_eq :
  b =
    Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      this
i2 : Fintype
  (↑(Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) : Type v) :=
  ⋯.fintype (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
rw :
  Fintype.card.{v}
      (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
            (t := Set.univ) ⋯) :
        Type v) ≤
    Fintype.card.{v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v)
rw₁ :
  Fintype.card.{v}
      (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
            (t := Set.univ) ⋯) :
        Type v) ≤
    finrank.{u, v} K ↥S
⊢ Fintype.card.{v}
      (↑(this.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
            (t := Set.univ) ⋯) :
        Type v) ≤
    Fintype.card.{v}
      (↑(Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S)) : Type v)
have rw₂ : finrank K V ≤ finrank.{u, v} K ↥S
Tactic: rw [Set.card_image_of_injective _ Subtype.coe_injective, ← finrank_eq_card_basis bS, ←
            finrank_eq_card_basis b, h]