awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
fx : M → R
tx : Finset M
ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
b₁ : M
h₁ : b₁ ∈ tx
b₂ : M
h₂ : b₂ ∈ ty
⊢ fx b₁ * HMul.hMul (β := R) (star (fy b₂)) (star ((((B : (a : M) → M →ₗ[R] R) b₁ : M →ₗ[R] R) : (a : M) → R) b₂) : R) =
    fx b₁ * HMul.hMul (β := R) (star (fy b₂)) ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) b₁ : R)
have obtain : ∀ (i : ι) (h₁ : Membership.mem (α := M) tx ((b : (a : ι) → M) i : M)),
  fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (star (fy b₂))
        (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) b₂) : R) =
    fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (star (fy b₂))
        ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: obtain ⟨i, rfl⟩ := ix h₁
Cleared hypotheses: b₁, h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
fx : M → R
tx : Finset M
ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
b₂ : M
h₂ : b₂ ∈ ty
i : ι
h₁ : Membership.mem (α := M) tx ((b : (a : ι) → M) i : M)
⊢ fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (star (fy b₂))
        (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) b₂) : R) =
    fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (star (fy b₂))
        ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
have obtain : ∀ (j : ι) (h₂ : Membership.mem (α := M) ty ((b : (a : ι) → M) j : M)),
  fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (star (fy ((b : (a : ι) → M) j)))
        (star
            ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
          R) =
    fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (star (fy ((b : (a : ι) → M) j)))
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: obtain ⟨j, rfl⟩ := iy h₂
Cleared hypotheses: b₂, h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
fx : M → R
tx : Finset M
ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
i : ι
h₁ : Membership.mem (α := M) tx ((b : (a : ι) → M) i : M)
j : ι
h₂ : Membership.mem (α := M) ty ((b : (a : ι) → M) j : M)
⊢ fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (star (fy ((b : (a : ι) → M) j)))
        (star
            ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
          R) =
    fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (star (fy ((b : (a : ι) → M) j)))
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
have rw : fx ((b : (a : ι) → M) i) *
    HMul.hMul (β := R) (star (fy ((b : (a : ι) → M) j)))
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R) =
  fx ((b : (a : ι) → M) i) *
    HMul.hMul (β := R) (star (fy ((b : (a : ι) → M) j)))
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
Goal:
R : Type u_1
M : Type u_2
n : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Fintype n
inst_5 : DecidableEq n
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
⊢ B.IsSymm ↔
    Matrix.IsHermitian.{u_1, u_3} (α := R) (n := n) ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B)
have rw : (∀ (b_1 a : n),
    Eq.{u_1 + 1} (α := R)
      (star
          ((((B : (a : M) → M →ₗ[R] R) ((b : (a : n) → M) a) : M →ₗ[R] R) : (a : M) → R) ((b : (a : n) → M) b_1 : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : n) → M) b_1) : M →ₗ[R] R) : (a : M) → R) ((b : (a : n) → M) a : M) : R)) ↔
  ∀ (i j : n),
    Eq.{u_1 + 1} (α := R) (star ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B j i) : R)
      ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B i j : R)
Tactic: rw [isSymm_iff_basis b, Matrix.IsHermitian.ext_iff, forall_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
⊢ B.IsPosSemidef ↔
    Matrix.PosSemidef.{u_3, u_4} (n := n) (R := R) ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B)
have rw : B.IsSymm ∧ B.IsNonneg ↔
  Matrix.IsHermitian.{u_4, u_3} (α := R) (n := n) ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) ∧
    ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
Tactic: rw [isPosSemidef_def, Matrix.posSemidef_iff_dotProduct_mulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
⊢ B.IsSymm ∧ B.IsNonneg ↔
    Matrix.IsHermitian.{u_4, u_3} (α := R) (n := n) ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) ∧
      ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
have apply : B.IsNonneg ↔ ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
Tactic: apply and_congr (B.isSymm_iff_isHermitian_toMatrix b)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
⊢ B.IsNonneg ↔
    ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
have rw : (∀ (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)) ↔
  ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
Tactic: rw [isNonneg_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
⊢ (∀ (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)) ↔
    ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
have refine_1 : ∀ (h : ∀ (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R))
  (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
Tactic: refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
refine_1 :
  ∀ (h : ∀ (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R))
    (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
⊢ (∀ (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)) ↔
    ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
have refine_2 : ∀ (h : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x)
  (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
Tactic: refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : M), LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x : n → R
⊢ 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
have refine_1 : LE.le.{u_4} (α := R) (0 : R)
  ((((B : (a : M) → M →ₗ[R] R) ((b.equivFun.symm : (a : n → R) → M) x) : M →ₗ[R] R) : (a : M) → R)
      ((b.equivFun.symm : (a : n → R) → M) x : M) :
    R)
Tactic: rw [star_dotProduct_toMatrix₂_mulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Star (goal)
Goal:
M : Type u_2
n : Type u_3
inst : AddCommMonoid M
inst_1 : Fintype n
inst_2 : DecidableEq n
R : Type u_4
inst_3 : CommRing R
inst_4 : StarRing R
inst_5 : PartialOrder R
inst_6 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ Matrix.mulVec ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B) x
x : M
⊢ LE.le.{u_4} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
have refine_2 : LE.le.{u_4} (α := R) 0
  (dotProduct.{u_4, u_3} (m := n) (star (⇑((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R))
    (Matrix.mulVec (n := n) ((toMatrix₂ b b : (a : M →ₗ⋆[R] M →ₗ[R] R) → Matrix n n R) B)
      (⇑((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R)))
Tactic: rw [apply_eq_star_dotProduct_toMatrix₂_mulVec b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
s : Set M₂
⊢ span R ((⇑f : (a : M) → M₂) ⁻¹' s) ≤ comap f (span R₂ s)
have rw : Subset.{u_4} (α := Set M) ((⇑f : (a : M) → M₂) ⁻¹' s) ((⇑f : (a : M) → M₂) ⁻¹' (↑(span R₂ s) : Set M₂))
Tactic: rw [span_le, comap_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
V : Submodule R M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥V) N
S : Set M
hV : V = span R S
⊢ f = g ↔
    ∀ (s : (↑S : Type u_4)),
      Eq.{u_8 + 1} (α := N) ((f : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
        ((g : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
have mp : f = g →
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N) ((f : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) sorry) : N)
      ((g : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) sorry) : N)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
V : Submodule R M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥V) N
S : Set M
hV : V = span R S
mp :
  f = g →
    ∀ (s : (↑S : Type u_4)),
      Eq.{u_8 + 1} (α := N) ((f : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
        ((g : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
⊢ f = g ↔
    ∀ (s : (↑S : Type u_4)),
      Eq.{u_8 + 1} (α := N) ((f : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
        ((g : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
have mpr : (∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N) ((f : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) sorry) : N)
      ((g : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) sorry) : N)) →
  f = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
V : Submodule R M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥V) N
S : Set M
hV : V = span R S
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N) ((f : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
      ((g : (a : ↥V) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ V) (↑s : M) ⋯) : N)
⊢ f = g
have mpr : ∀ (f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N)
  (h :
    ∀ (s : (↑S : Type u_4)),
      Eq.{u_8 + 1} (α := N)
        ((f : (a : ↥(span R S)) → N)
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) sorry) :
          N)
        ((g : (a : ↥(span R S)) → N)
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) sorry) :
          N)),
  f = g
Tactic: subst hV
Cleared hypotheses: V, f, g, hV, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
⊢ f = g
have mpr : ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x),
  Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
Tactic: suffices ∀ (x : M) (hx : x ∈ span R S), f ⟨x, hx⟩ = g ⟨x, hx⟩ by
      ext ⟨x, hx⟩
      exact this x hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
x : M
⊢ Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) 0 ⋯) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) 0 ⋯) :
      N)
have mpr : Eq.{u_8 + 1} (α := N) (0 : N)
  ((g : (a : ↥(span R S)) → N) (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) 0 sorry) :
    N)
Tactic: erw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
x : M
mpr :
  Eq.{u_8 + 1} (α := N) (0 : N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) 0 ⋯) :
      N)
⊢ Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) 0 ⋯) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) 0 ⋯) :
      N)
have mpr₁ : Eq.{u_8 + 1} (α := N) 0 0
Tactic: erw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
x_1 x y : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
hy : Membership.mem (γ := Submodule R M) (span R S) y
hx' :
  Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
hy' :
  Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
      N)
⊢ Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (x + y) ⋯) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (x + y) ⋯) :
      N)
have mpr : HAdd.hAdd (α := N) (β := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
      N) =
  HAdd.hAdd (α := N) (β := N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
      N)
Tactic: erw [f.map_add ⟨x, hx⟩ ⟨y, hy⟩, g.map_add ⟨x, hx⟩ ⟨y, hy⟩]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
x_1 x y : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
hy : Membership.mem (γ := Submodule R M) (span R S) y
hx' :
  Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
hy' :
  Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
      N)
⊢ HAdd.hAdd (α := N) (β := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
        N) =
    HAdd.hAdd (α := N) (β := N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
        N)
have mpr : HAdd.hAdd (α := N) (β := N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
      N) =
  HAdd.hAdd (α := N) (β := N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
      N)
Tactic: rw [hx', hy']