awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
v : ι → M
x_1 y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
h : Membership.mem (γ := Submodule R ↥(span R (range v))) ⊤ x
this : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (range v)) (v i)
⊢ Membership.mem (γ := Submodule R ↥(span R (range v)))
    (span R
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯))
    x
have h₁ : image (α := ↥(span R (range v)))
    (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x))
    (range fun (i : ι) ↦
      Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) sorry) =
  range v
Tactic: have h₁ : (((↑) : span R (range v) → M) '' range fun i => ⟨v i, this i⟩) = range v := by
      simp only [← Set.range_comp]
      rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
v : ι → M
x_1 y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
h : Membership.mem (γ := Submodule R ↥(span R (range v))) ⊤ x
this : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (range v)) (v i)
h₁ :
  image (α := ↥(span R (range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x))
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯) =
    range v
⊢ Eq (α := Submodule R M)
    (map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))
      (span R
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (span R (range v))
have rw : Eq (α := Submodule R M)
  (span R
    (image (α := ↥(span R (range v))) (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M)
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) sorry)))
  (span R (range v))
Tactic: rw [← span_image, Submodule.coe_subtype, h₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
v : ι → M
x_1 y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
h : Membership.mem (γ := Submodule R ↥(span R (range v))) ⊤ x
this : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (range v)) (v i)
h₁ :
  image (α := ↥(span R (range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x))
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯) =
    range v
rw :
  Eq (α := Submodule R M)
    (span R
      (image (α := ↥(span R (range v))) (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M)
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (span R (range v))
⊢ Eq (α := Submodule R M)
    (map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))
      (span R
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (span R (range v))
have rw₁ : Eq (α := Submodule R M)
  (span R
    (image (α := ↥(span R (range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x))
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) sorry)))
  (span R (range v))
Tactic: rw [← span_image, Submodule.coe_subtype, h₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
v : ι → M
x_1 y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
h : Membership.mem (γ := Submodule R ↥(span R (range v))) ⊤ x
this : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (range v)) (v i)
h₁ :
  image (α := ↥(span R (range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x))
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯) =
    range v
rw :
  Eq (α := Submodule R M)
    (span R
      (image (α := ↥(span R (range v))) (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M)
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (span R (range v))
rw₁ :
  Eq (α := Submodule R M)
    (span R
      (image (α := ↥(span R (range v)))
        (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x))
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (span R (range v))
⊢ Eq (α := Submodule R M)
    (map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))
      (span R
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (span R (range v))
have rw₂ : Eq (α := Submodule R M) (span R (range v)) (span R (range v))
Tactic: rw [← span_image, Submodule.coe_subtype, h₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
v : ι → M
x_1 y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
h : Membership.mem (γ := Submodule R ↥(span R (range v))) ⊤ x
this : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (range v)) (v i)
h₁ :
  image (α := ↥(span R (range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x))
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯) =
    range v
⊢ Membership.mem (γ := Submodule R ↥(span R (range v)))
    (span R
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯))
    x
have h₂ : Eq (α := Submodule R M)
  (map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))
    (span R
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) sorry)))
  (span R (range v))
Tactic: have h₂ : map (Submodule.subtype (span R (range v))) (span R (range fun i => ⟨v i, this i⟩)) =
        span R (range v) := by
      rw [← span_image, Submodule.coe_subtype, h₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
v : ι → M
x_1 y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
h : Membership.mem (γ := Submodule R ↥(span R (range v))) ⊤ x
this : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (range v)) (v i)
h₁ :
  image (α := ↥(span R (range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x))
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯) =
    range v
h₂ :
  Eq (α := Submodule R M)
    (map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))
      (span R
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (span R (range v))
⊢ Membership.mem (γ := Submodule R M)
    (map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))
      (span R
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (↑x : M)
have rw : Membership.mem (γ := Submodule R M) (span R (range v)) (↑x : M)
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
v : ι → M
x_1 y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
h : Membership.mem (γ := Submodule R ↥(span R (range v))) ⊤ x
this : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (range v)) (v i)
h₁ :
  image (α := ↥(span R (range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x))
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯) =
    range v
h₂ :
  Eq (α := Submodule R M)
    (map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))
      (span R
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (span R (range v))
⊢ Membership.mem (γ := Submodule R ↥(span R (range v)))
    (span R
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯))
    x
have h₃ : Membership.mem (γ := Submodule R M)
  (map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))
    (span R
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) sorry)))
  (↑x : M)
Tactic: have h₃ : (x : M) ∈ map (Submodule.subtype (span R (range v)))
        (span R (Set.range fun i => Subtype.mk (v i) (this i))) := by
      rw [h₂]
      apply Subtype.mem x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
v : ι → M
x_1 y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
h : Membership.mem (γ := Submodule R ↥(span R (range v))) ⊤ x
this : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (range v)) (v i)
h₁ :
  image (α := ↥(span R (range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x))
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯) =
    range v
h₂ :
  Eq (α := Submodule R M)
    (map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))
      (span R
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (span R (range v))
h₃ :
  Membership.mem (γ := Submodule R M)
    (map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))
      (span R
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (↑x : M)
⊢ Membership.mem (γ := Submodule R ↥(span R (range v)))
    (span R
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯))
    x
have rcases : ∀ (y : ↥(span R (range v)))
  (hy₁ :
    Membership.mem (γ := Submodule R ↥(span R (range v)))
      (span R
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) sorry))
      y)
  (hy₂ : (Submodule.subtype (span R (range v)) : (a : ↥(span R (range v))) → M) y = (↑x : M)),
  Membership.mem (γ := Submodule R ↥(span R (range v)))
    (span R
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) sorry))
    x
Tactic: rcases mem_map.1 h₃ with ⟨y, hy₁, hy₂⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
v : ι → M
x_1 y_1 : M
hli : LinearIndependent R v
x : ↥(span R (range v))
h : Membership.mem (γ := Submodule R ↥(span R (range v))) ⊤ x
this : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (range v)) (v i)
h₁ :
  image (α := ↥(span R (range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x))
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯) =
    range v
h₂ :
  Eq (α := Submodule R M)
    (map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))
      (span R
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (span R (range v))
h₃ :
  Membership.mem (γ := Submodule R M)
    (map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))
      (span R
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (↑x : M)
y : ↥(span R (range v))
hy₁ :
  Membership.mem (γ := Submodule R ↥(span R (range v)))
    (span R
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯))
    y
hy₂ : (Submodule.subtype (span R (range v)) : (a : ↥(span R (range v))) → M) y = (↑x : M)
⊢ x = y
have rw : (Submodule.subtype (span R (range v)) : (a : ↥(span R (range v))) → M) y = (↑y : M)
Tactic: rw [Subtype.ext_iff, ← hy₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
v : ι → M
x_1 y_1 : M
hli : LinearIndependent R v
x : ↥(span R (range v))
h : Membership.mem (γ := Submodule R ↥(span R (range v))) ⊤ x
this : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (range v)) (v i)
h₁ :
  image (α := ↥(span R (range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x))
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯) =
    range v
h₂ :
  Eq (α := Submodule R M)
    (map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))
      (span R
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (span R (range v))
h₃ :
  Membership.mem (γ := Submodule R M)
    (map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))
      (span R
        (range fun (i : ι) ↦
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯)))
    (↑x : M)
y : ↥(span R (range v))
hy₁ :
  Membership.mem (γ := Submodule R ↥(span R (range v)))
    (span R
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯))
    y
hy₂ : (Submodule.subtype (span R (range v)) : (a : ↥(span R (range v))) → M) y = (↑x : M)
⊢ Membership.mem (γ := Submodule R ↥(span R (range v)))
    (span R
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯))
    x
have h_x_eq_y : x = y
Tactic: have h_x_eq_y : x = y := by
      rw [Subtype.ext_iff, ← hy₂]
      simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
hli : LinearIndependent R v
i : ι
⊢ Eq.{u_5 + 1} (α := ↥(span R (range v))) ((Basis.span hli : (a : ι) → ↥(span R (range v))) i : ↥(span R (range v)))
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯ :
      ↥(span R (range v)))
have a : (↑((Basis.span hli : (a : ι) → ↥(span R (range v))) i) : M) =
  (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) sorry) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
hli : LinearIndependent R v
i : ι
hi : Membership.mem (γ := Submodule R M) (span R (range v)) (v i)
⊢ Eq (α := ι →₀ R)
    (((Basis.span hli).repr : (a : ↥(span R (range v))) → ι →₀ R)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) hi) :
      ι →₀ R)
    (single i 1 : ι →₀ R)
have rw : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) hi =
  ((Basis.span hli).repr.symm : (a : ι →₀ R) → ↥(span R (range v))) (single i 1)
Tactic: rw [← LinearEquiv.eq_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
hli : LinearIndependent R v
h : Eq (α := Submodule R M) (span R (range v)) (span R (range (-v)))
⊢ Basis.span ⋯ =
    (Basis.span hli).map (LinearEquiv.neg R ≪≫ₗ LinearEquiv.ofEq (span R (range v)) (span R (range (-v))) h)
have a : ∀ (i : ι),
  Eq.{u_8 + 1} (α := M) (↑((Basis.span sorry : (a : ι) → ↥(span R (range (-v)))) i) : M)
    (↑(((Basis.span hli).map (LinearEquiv.neg R ≪≫ₗ LinearEquiv.ofEq (span R (range v)) (span R (range (-v))) h) :
            (a : ι) → ↥(span R (range (-v))))
          i) :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
⊢ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) = w
have apply : w ≤ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
Tactic: apply le_antisymm h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
⊢ Membership.mem (γ := Set M) (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)) x
have by_contra : ∀ (q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)), False
Tactic: by_contra q
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
⊢ False
have e : (linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) = x
Tactic: have e := b.linearCombination_repr x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
e : (sum ((b.repr : (a : M) → ι →₀ R) x) fun (i : ι) (a : R) ↦ HSMul.hSMul (β := M) a ((b : (a : ι) → M) i : M)) = x
u : Embedding.{u_1 + 1, u_5 + 1} ι (↑w : Type u_5) :=
  { toFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) ((b : (a : ι) → M) i) ⋯, inj' := ⋯ }
⊢ False
have e₁ : (sum ((b.repr : (a : M) → ι →₀ R) x) fun (i : ι) (a : R) ↦
    HSMul.hSMul (β := M) a (↑((u : (a : ι) → (↑w : Type u_5)) i) : M)) =
  (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p) : M)
Tactic: change ((b.repr x).sum fun (i : ι) (a : R) ↦ a • (u i : M)) = ((⟨x, p⟩ : w) : M) at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
u : Embedding.{u_1 + 1, u_5 + 1} ι (↑w : Type u_5) :=
  { toFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) ((b : (a : ι) → M) i) ⋯, inj' := ⋯ }
e :
  (sum ((b.repr : (a : M) → ι →₀ R) x) fun (i : ι) (a : R) ↦
      HSMul.hSMul (β := M) a (↑((u : (a : ι) → (↑w : Type u_5)) i) : M)) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p) : M)
⊢ False
have e₁ : (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : (↑w : Type u_5) →₀ R) → M)
    (embDomain u ((b.repr : (a : M) → ι →₀ R) x)) =
  (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p) : M)
Tactic: rw [← Finsupp.sum_embDomain (f := u) (g := fun x r ↦ r • (x : M)),
      ← Finsupp.linearCombination_apply] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
u : Embedding.{u_1 + 1, u_5 + 1} ι (↑w : Type u_5) :=
  { toFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) ((b : (a : ι) → M) i) ⋯, inj' := ⋯ }
e :
  (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : (↑w : Type u_5) →₀ R) → M)
      (embDomain u ((b.repr : (a : M) → ι →₀ R) x)) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p) : M)
⊢ False
have refine : Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p ∉
  Finsupp.support.{u_5, u_3} (M := R) (embDomain u ((b.repr : (a : M) → ι →₀ R) x))
Tactic: refine hi.linearCombination_ne_of_notMem_support _ ?_ e