awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : M
a : R
x : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
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)
⊢ 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) (a • x) ⋯) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (a • x) ⋯) :
      N)
have mpr : HSMul.hSMul (β := N) a
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N) =
  HSMul.hSMul (β := N) a
    ((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: erw [f.map_smul a ⟨x, hx⟩, g.map_smul a ⟨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_1 : M
a : R
x : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
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)
⊢ HSMul.hSMul (β := N) a
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N) =
    HSMul.hSMul (β := N) a
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
have mpr : HSMul.hSMul (β := N) a
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N) =
  HSMul.hSMul (β := N) a
    ((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: rw [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
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)
have mpr : ∀ (x : M) (hx : x ∈ S),
  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 sorry) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x sorry) :
      N)
Tactic: induction hx using span_induction with
    | mem x hx => exact h ⟨x, hx⟩
    | zero => erw [map_zero, map_zero]
    | add x y hx hy hx' hy' =>
        erw [f.map_add ⟨x, hx⟩ ⟨y, hy⟩, g.map_add ⟨x, hx⟩ ⟨y, hy⟩]
        rw [hx', hy']
    | smul a x hx hx' =>
        erw [f.map_smul a ⟨x, hx⟩, g.map_smul a ⟨x, hx⟩]
        rw [hx']
Cleared hypotheses: 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
hx : Membership.mem (γ := Submodule R M) (span R S) x
mpr :
  ∀ (x : M) (hx : x ∈ S),
    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 ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x ⋯) :
        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 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)
have mpr₁ : 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 sorry) :
    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: induction hx using span_induction with
    | mem x hx => exact h ⟨x, hx⟩
    | zero => erw [map_zero, map_zero]
    | add x y hx hy hx' hy' =>
        erw [f.map_add ⟨x, hx⟩ ⟨y, hy⟩, g.map_add ⟨x, hx⟩ ⟨y, hy⟩]
        rw [hx', hy']
    | smul a x hx hx' =>
        erw [f.map_smul a ⟨x, hx⟩, g.map_smul a ⟨x, hx⟩]
        rw [hx']
Cleared hypotheses: 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
hx : Membership.mem (γ := Submodule R M) (span R S) x
mpr :
  ∀ (x : M) (hx : x ∈ S),
    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 ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x ⋯) :
        N)
mpr₁ :
  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)
⊢ 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)
have mpr₂ : ∀ (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) sorry) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (x + y) sorry) :
      N)
Tactic: induction hx using span_induction with
    | mem x hx => exact h ⟨x, hx⟩
    | zero => erw [map_zero, map_zero]
    | add x y hx hy hx' hy' =>
        erw [f.map_add ⟨x, hx⟩ ⟨y, hy⟩, g.map_add ⟨x, hx⟩ ⟨y, hy⟩]
        rw [hx', hy']
    | smul a x hx hx' =>
        erw [f.map_smul a ⟨x, hx⟩, g.map_smul a ⟨x, hx⟩]
        rw [hx']
Cleared hypotheses: 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
f g : M →ₗ[R] N
S : Set M
hM : Eq (α := Submodule R M) (span R S) ⊤
⊢ f = g ↔
    ∀ (s : (↑S : Type u_4)), Eq.{u_8 + 1} (α := N) ((f : (a : M) → N) (↑s : M) : N) ((g : (a : M) → N) (↑s : M) : N)
have h : f = g ↔
  Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤)
Tactic: convert!
    linearMap_eq_iff_of_eq_span (f.comp (Submodule.subtype _)) (g.comp (Submodule.subtype _))
      hM.symm
-- 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
f g : M →ₗ[R] N
S : Set M
hM : Eq (α := Submodule R M) (span R S) ⊤
⊢ f = g ↔
    Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤)
have h : f = g →
  Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤)
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
f g : M →ₗ[R] N
S : Set M
hM : Eq (α := Submodule R M) (span R S) ⊤
h :
  f = g →
    Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤)
⊢ f = g ↔
    Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤)
have h₁ : Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤) →
  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
f g : M →ₗ[R] N
S : Set M
hM : Eq (α := Submodule R M) (span R S) ⊤
h : Eq (α := LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥⊤) N) (f ∘ₗ Submodule.subtype ⊤) (g ∘ₗ Submodule.subtype ⊤)
⊢ f = g
have h₁ : ∀ (x : M), Eq.{u_8 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
Tactic: ext x
-- 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
s : Set M
r : R
hr : IsUnit r
⊢ Eq (α := Submodule R M) (span R (r • s)) (span R s)
have a : LE.le (α := Submodule R M) (span R (r • s)) (span R s)
Tactic: apply le_antisymm
-- 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
s : Set M
r : R
hr : IsUnit r
a : LE.le (α := Submodule R M) (span R (r • s)) (span R s)
⊢ Eq (α := Submodule R M) (span R (r • s)) (span R s)
have a₁ : LE.le (α := Submodule R M) (span R s) (span R (r • s))
Tactic: apply le_antisymm
-- 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
s : Set M
r : R
hr : IsUnit r
⊢ LE.le (α := Submodule R M) (span R s) (span R (r • s))
have h : s = (↑hr.unit⁻¹ : R) • r • s
Tactic: convert! span_smul_le (r • s) ((hr.unit⁻¹ :) : R)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
x y : ↥p
hxy :
  Eq (α := ↥(span S (↑p : Set M))) ((inclusionSpan S p : (a : ↥p) → ↥(span S (↑p : Set M))) x : ↥(span S (↑p : Set M)))
    ((inclusionSpan S p : (a : ↥p) → ↥(span S (↑p : Set M))) y : ↥(span S (↑p : Set M)))
⊢ x = y
have hxy₁ : Eq.{u_4 + 1} (α := M) (↑((inclusionSpan S p : (a : ↥p) → ↥(span S (↑p : Set M))) x) : M)
  (↑((inclusionSpan S p : (a : ↥p) → ↥(span S (↑p : Set M))) y) : M)
Tactic: rw [Subtype.ext_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
⊢ image (α := ↥(span S (↑p : Set M))) (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
      (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M)))) =
    (↑p : Set M)
have h : ∀ (x : M),
  Membership.mem (γ := Set M)
      (image (α := ↥(span S (↑p : Set M)))
        (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
        (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M)))))
      x ↔
    x ∈ (↑p : Set M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
⊢ Eq (α := Submodule S ↥(span S (↑p : Set M)))
    (span S (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))) ⊤
have this : image (α := ↥(span S (↑p : Set M))) (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
    (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M)))) =
  (↑p : Set M)
Tactic: have : (span S (p : Set M)).subtype '' range (inclusionSpan S p) = p := by
    ext; simpa [Subtype.ext_iff] using fun h ↦ subset_span h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
this :
  image (α := ↥(span S (↑p : Set M))) (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
      (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M)))) =
    (↑p : Set M)
⊢ Eq (α := Submodule S ↥(span S (↑p : Set M)))
    (span S (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))) ⊤
have a : Eq (α := Submodule S M)
  (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M)))
    (span S (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))))
  (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M))) ⊤)
Tactic: apply map_injective_of_injective (span S (p : Set M)).injective_subtype
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
this :
  image (α := ↥(span S (↑p : Set M))) (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
      (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M)))) =
    (↑p : Set M)
⊢ Eq (α := Submodule S M)
    (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M)))
      (span S (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))))
    (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M))) ⊤)
have a : Eq (α := Submodule S M)
  (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M)))
    (span S (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))))
  (span S (↑p : Set M))
Tactic: rw [map_subtype_top, map_span, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
this :
  image (α := ↥(span S (↑p : Set M))) (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
      (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M)))) =
    (↑p : Set M)
a :
  Eq (α := Submodule S M)
    (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M)))
      (span S (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))))
    (span S (↑p : Set M))
⊢ Eq (α := Submodule S M)
    (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M)))
      (span S (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))))
    (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M))) ⊤)
have a₁ : Eq (α := Submodule S M)
  (span S
    (image (α := ↥(span S (↑p : Set M))) (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
      (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))))
  (span S (↑p : Set M))
Tactic: rw [map_subtype_top, map_span, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
this :
  image (α := ↥(span S (↑p : Set M))) (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
      (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M)))) =
    (↑p : Set M)
a :
  Eq (α := Submodule S M)
    (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M)))
      (span S (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))))
    (span S (↑p : Set M))
a₁ :
  Eq (α := Submodule S M)
    (span S
      (image (α := ↥(span S (↑p : Set M)))
        (⇑(Submodule.subtype (span S (↑p : Set M))) : (a : ↥(span S (↑p : Set M))) → M)
        (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))))
    (span S (↑p : Set M))
⊢ Eq (α := Submodule S M)
    (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M)))
      (span S (range (ι := ↥p) (⇑(inclusionSpan S p) : (a : ↥p) → ↥(span S (↑p : Set M))))))
    (map (M := ↥(span S (↑p : Set M))) (Submodule.subtype (span S (↑p : Set M))) ⊤)
have a₂ : Eq (α := Submodule S M) (span S (↑p : Set M)) (span S (↑p : Set M))
Tactic: rw [map_subtype_top, map_span, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S (↑p : Set M)
this : map q.subtype (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) = q
⊢ Eq (α := Submodule S ↥(restrictScalars R q))
    (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) ⊤
have a : map q.subtype (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) = map q.subtype ⊤
Tactic: apply map_injective_of_injective q.injective_subtype
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S (↑p : Set M)
this : map q.subtype (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) = q
⊢ map q.subtype (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) = map q.subtype ⊤
have a : q = map q.subtype ⊤
Tactic: rw [this, q.map_subtype_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S (↑p : Set M)
this : map q.subtype (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) = q
a : q = map q.subtype ⊤
⊢ map q.subtype (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) = map q.subtype ⊤
have a₁ : q = q
Tactic: rw [this, q.map_subtype_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : SMul R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S (↑p : Set M)
⊢ Eq (α := Submodule S ↥(restrictScalars R q))
    (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) ⊤
have suffices : map q.subtype (span S (range (ι := ↥p) (⇑(inclusion h₁) : (a : ↥p) → ↥(restrictScalars R q)))) = q
Tactic: suffices (span S (range (inclusion h₁))).map q.subtype = q by
    apply map_injective_of_injective q.injective_subtype
    rw [this, q.map_subtype_top]