awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
simp :
  range.{u_5, u_1 + 1} (ι := ι)
      (comp (β := ↥(span R (range v)))
        (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x)) fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯) =
    range v
⊢ 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

Tactic:
simp only [← Set.range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
⊢ range.{u_5, u_1 + 1} (ι := ι)
      (comp (β := ↥(span R (range v)))
        (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x)) fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯) =
    range v

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
⊢ 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

Tactic:
have h₁ : (((↑) : span R (range v) → M) '' range fun i => ⟨v i, this i⟩) = range v := by
      simp only [← Set.range_comp]
      rfl
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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))
rw₂ rw₃ : Eq (α := Submodule R M) (span R (range v)) (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))

Tactic:
rw [← span_image, Submodule.coe_subtype, h₁]

Premises used: Submodule.coe_subtype, Submodule.span_image
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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))

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₁]
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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))
rw : Membership.mem (γ := Submodule R M) (span R (range v)) (↑x : M)
⊢ 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)

Tactic:
rw [h₂]
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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) (span R (range v)) (↑x : M)

Tactic:
apply Subtype.mem x

Premises used: Subtype.mem
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)

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
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
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) ⋯))
        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
⊢ 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

Tactic:
rcases mem_map.1 h₃ with ⟨y, hy₁, hy₂⟩

Premises used: Submodule.mem_map, Iff.mp
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
rw : (Submodule.subtype (span R (range v)) : (a : ↥(span R (range v))) → M) y = (↑y : M)
⊢ x = y

Tactic:
rw [Subtype.ext_iff, ← hy₂]

Premises used: Subtype.ext_iff
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
⊢ (Submodule.subtype (span R (range v)) : (a : ↥(span R (range v))) → M) y = (↑y : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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

Tactic:
have h_x_eq_y : x = y := by
      rw [Subtype.ext_iff, ← hy₂]
      simp
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
h_x_eq_y : x = y
rwa rwa₁ rwa₂ rwa₃ :
  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
⊢ 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

Tactic:
rwa [h_x_eq_y]
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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 : ι
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) ⋯) : M)
⊢ 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)))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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 : ι
⊢ (↑((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) ⋯) : M)

Tactic:
congr_arg ((↑) : span R (range v) → M) <| Basis.mk_apply _ _ _

Premises used: Module.Basis.mk_apply, congr_arg, Subtype.val
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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 : ι
⊢ (↑((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) ⋯) : M)

Tactic:
exact congr_arg ((↑) : span R (range v) → M) <| Basis.mk_apply _ _ _

Premises used: Module.Basis.mk_apply, congr_arg, Subtype.val
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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 : ι
⊢ (↑((Basis.span hli : (a : ι) → ↥(span R (range v))) i) : M) = v i

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
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)
⊢ 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)

Tactic:
rw [← LinearEquiv.eq_symm_apply]

Premises used: LinearEquiv.eq_symm_apply
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
⊢ 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:
simp [Basis.span]

Premises used: Module.Basis.span
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)))
a :
  ∀ (i : ι),
    Eq.{u_8 + 1} (α := M) (↑((Basis.span ⋯ : (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)
⊢ Basis.span ⋯ =
    (Basis.span hli).map (LinearEquiv.neg R ≪≫ₗ LinearEquiv.ofEq (span R (range v)) (span R (range (-v))) h)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)))
i : ι
⊢ Eq.{u_8 + 1} (α := M) (↑((Basis.span ⋯ : (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:
simp