awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Eq.{u_4 + 1} (α := M) ((toSpanSingleton R M 0 : (a : R) → M) 1 : M) ((0 : (a : R) → M) 1 : M)
⊢ Eq (α := R →ₗ[R] M) (toSpanSingleton R M 0) 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{u_4 + 1} (α := M) ((toSpanSingleton R M 0 : (a : R) → M) 1 : M) ((0 : (a : R) → M) 1 : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
rw : Eq (α := R →ₗ[R] M) (toSpanSingleton R M x) (toSpanSingleton R M 0) ↔ x = 0
rw₁ rw₂ : x = 0 ↔ x = 0
⊢ Eq (α := R →ₗ[R] M) (toSpanSingleton R M x) 0 ↔ x = 0

Tactic:
rw [← toSpanSingleton_zero, (toSpanSingleton_injective R M).eq_iff]

Premises used: Function.Injective.eq_iff, LinearMap.toSpanSingleton_zero, LinearMap.toSpanSingleton_injective
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
h :
  Eq.{u_4 + 1} (α := M) ((toSpanSingleton R M (x + y) : (a : R) → M) 1 : M)
    ((HAdd.hAdd (α := R →ₗ[R] M) (toSpanSingleton R M x) (toSpanSingleton R M y) : (a : R) → M) 1 : M)
⊢ toSpanSingleton R M (x + y) = HAdd.hAdd (α := R →ₗ[R] M) (toSpanSingleton R M x) (toSpanSingleton R M y)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
⊢ Eq.{u_4 + 1} (α := M) ((toSpanSingleton R M (x + y) : (a : R) → M) 1 : M)
    ((HAdd.hAdd (α := R →ₗ[R] M) (toSpanSingleton R M x) (toSpanSingleton R M y) : (a : R) → M) 1 : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_8
inst_3 : Monoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass R S M
r : S
x : M
h :
  Eq.{u_4 + 1} (α := M) ((toSpanSingleton R M (r • x) : (a : R) → M) 1 : M)
    ((HSMul.hSMul (β := R →ₗ[R] M) r (toSpanSingleton R M x) : (a : R) → M) 1 : M)
⊢ toSpanSingleton R M (r • x) = HSMul.hSMul (β := R →ₗ[R] M) r (toSpanSingleton R M x)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_8
inst_3 : Monoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass R S M
r : S
x : M
⊢ Eq.{u_4 + 1} (α := M) ((toSpanSingleton R M (r • x) : (a : R) → M) 1 : M)
    ((HSMul.hSMul (β := R →ₗ[R] M) r (toSpanSingleton R M x) : (a : R) → M) 1 : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
inst : Semiring R
e : R
simp_rw : (∀ (x : R), x * (e * e) = x * e) ↔ e * e = e
⊢ IsIdempotentElem (M := R →ₗ[R] R) (toSpanSingleton R R e) ↔ IsIdempotentElem e

Tactic:
simp_rw [IsIdempotentElem, LinearMap.ext_iff, Module.End.mul_apply, toSpanSingleton_apply,
    smul_eq_mul, mul_assoc]

Premises used: mul_assoc, LinearMap.ext_iff, LinearMap.toSpanSingleton_apply, IsIdempotentElem, smul_eq_mul, Module.End.mul_apply
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
inst : Semiring R
e : R
h : ∀ (x : R), x * (e * e) = x * e
rw : e * e
| e

Tactic:
rw [← one_mul e, ← h, one_mul]

Premises used: one_mul
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
inst : Semiring R
e : R
h : ∀ (x : R), x * (e * e) = x * e
conv_rhs : e * e = e
conv_rhs₁ : e * e = e * e
⊢ e * e = e

Tactic:
conv_rhs => rw [← one_mul e, ← h, one_mul]

Premises used: one_mul
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
inst : Semiring R
e : R
h : e * e = e
x : R
rw rw₁ : x * e = x * e
⊢ x * (e * e) = x * e

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
inst : Semiring R
e : R
⊢ (∀ (x : R), x * (e * e) = x * e) ↔ e * e = e

Tactic:
exact ⟨fun h ↦ by conv_rhs => rw [← one_mul e, ← h, one_mul], fun h _ ↦ by rw [h]⟩
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
inst : Semiring R
f : Module.End R R
rw :
  Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) 1 : R) : R) ((f : (a : R) → R) 1 : R) ↔
    ∀ (x : R), Eq (α := R) ((f * f : (a : R) → R) x : R) ((f : (a : R) → R) x : R)
⊢ IsIdempotentElem (M := R) ((f : (a : R) → R) 1 : R) ↔ IsIdempotentElem f

Tactic:
rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, IsIdempotentElem,
    LinearMap.ext_iff]

Premises used: LinearMap.ext_iff, IsIdempotentElem, smul_eq_mul, mul_one, map_smul
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
inst : Semiring R
f : Module.End R R
simp_rw :
  Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) 1 : R) : R) ((f : (a : R) → R) 1 : R) ↔
    ∀ (x : R), Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) x : R) : R) ((f : (a : R) → R) x : R)
⊢ Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) 1 : R) : R) ((f : (a : R) → R) 1 : R) ↔
    ∀ (x : R), Eq (α := R) ((f * f : (a : R) → R) x : R) ((f : (a : R) → R) x : R)

Tactic:
simp_rw [Module.End.mul_apply]

Premises used: Module.End.mul_apply
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
inst : Semiring R
f : Module.End R R
h : Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) 1 : R) : R) ((f : (a : R) → R) 1 : R)
r : R
rw : Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) (r * 1) : R) : R) ((f : (a : R) → R) (r * 1) : R)
rw₁ :
  Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) (HSMul.hSMul (β := R) r 1) : R) : R)
    ((f : (a : R) → R) (HSMul.hSMul (β := R) r 1) : R)
rw₂ :
  (f : (a : R) → R) (HSMul.hSMul (β := R) r ((f : (a : R) → R) 1 : R)) =
    HSMul.hSMul (β := R) r ((f : (a : R) → R) 1 : R)
rw₃ :
  HSMul.hSMul (β := R) r ((f : (a : R) → R) ((f : (a : R) → R) 1 : R) : R) =
    HSMul.hSMul (β := R) r ((f : (a : R) → R) 1 : R)
rw₄ rw₅ : HSMul.hSMul (β := R) r ((f : (a : R) → R) 1 : R) = HSMul.hSMul (β := R) r ((f : (a : R) → R) 1 : R)
⊢ Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) r : R) : R) ((f : (a : R) → R) r : R)

Tactic:
rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h]

Premises used: smul_eq_mul, mul_one, map_smul
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
inst : Semiring R
f : Module.End R R
⊢ Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) 1 : R) : R) ((f : (a : R) → R) 1 : R) ↔
    ∀ (x : R), Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) x : R) : R) ((f : (a : R) → R) x : R)

Tactic:
exact ⟨fun h r ↦ by rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h], (· 1)⟩
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Eq (α := Submodule R M) (range (toSpanSingleton R M x)) (R ∙ x)

Tactic:
SetLike.coe_injective (Submodule.span_singleton_eq_range R x).symm

Premises used: SetLike.coe_injective, Submodule.span_singleton_eq_range, Eq.symm
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Eq (α := Submodule R M) (R ∙ x) (range (toSpanSingleton R M x))

Tactic:
range_toSpanSingleton x |>.symm

Premises used: LinearMap.range_toSpanSingleton, Eq.symm
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
x : M
h :
  Eq.{u_5 + 1} (α := M₂) ((f ∘ₗ toSpanSingleton R M x : (a : R) → M₂) 1 : M₂)
    ((toSpanSingleton R M₂ ((f : (a : M) → M₂) x) : (a : R) → M₂) 1 : M₂)
⊢ f ∘ₗ toSpanSingleton R M x = toSpanSingleton R M₂ ((f : (a : M) → M₂) x)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
x : M
⊢ Eq.{u_5 + 1} (α := M₂) ((f ∘ₗ toSpanSingleton R M x : (a : R) → M₂) 1 : M₂)
    ((toSpanSingleton R M₂ ((f : (a : M) → M₂) x) : (a : R) → M₂) 1 : M₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
x : M
hx : x ∈ N
h :
  ∀ (y : ↥N),
    y ∈ submoduleOf (R ∙ x) N ↔ Membership.mem (γ := Submodule R ↥N) (R ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx) y
⊢ submoduleOf (R ∙ x) N = R ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx

Tactic:
ext y
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
x : M
hx : x ∈ N
y : ↥N
h : (∃ (a : R), a • x = (↑y : M)) ↔ ∃ (a : R), a • Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx = y
⊢ y ∈ submoduleOf (R ∙ x) N ↔ Membership.mem (γ := Submodule R ↥N) (R ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx) y

Tactic:
simp_rw [submoduleOf, mem_comap, subtype_apply, mem_span_singleton]

Premises used: Submodule.subtype_apply, Submodule.mem_comap, Submodule.mem_span_singleton, Submodule.submoduleOf
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
x : M
hx : x ∈ N
y : ↥N
⊢ (∃ (a : R), a • x = (↑y : M)) ↔ ∃ (a : R), a • Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx = y

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
inst : Semiring R
x : R
⊢ Eq (α := Submodule R R) (ker (toSpanSingleton R R x)) ⊥ ↔ Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) x

Tactic:
le_bot_iff.symm

Premises used: le_bot_iff, Set.Mem, setOf, Set.preimage, Set.singleton, Iff.symm
-- Module: Mathlib.LinearAlgebra.Span.Basic
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₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
rw : s ⊆ (↑(eqLocus f g) : Set M) ↔ Set.EqOn.{u_4, u_5} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) s
⊢ Set.EqOn.{u_4, u_5} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑(span R s) : Set M) ↔
    Set.EqOn.{u_4, u_5} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) s

Tactic:
rw [← le_eqLocus, span_le]

Premises used: LinearMap.le_eqLocus, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Span.Basic
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₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
⊢ s ⊆ (↑(eqLocus f g) : Set M) ↔ Set.EqOn.{u_4, u_5} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) s

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Span.Basic
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₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
H : Set.EqOn.{u_4, u_5} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) s
⊢ Set.EqOn.{u_4, u_5} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (↑(span R s) : Set M)

Tactic:
eqOn_span_iff.2 H

Premises used: Iff.mpr, LinearMap.eqOn_span_iff
-- Module: Mathlib.LinearAlgebra.Span.Basic
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₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
H : Set.EqOn.{u_4, u_5} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) s
x : M
h : Membership.mem (γ := Submodule R M) (span R s) x
⊢ Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)

Tactic:
eqOn_span' H h

Premises used: LinearMap.eqOn_span'
-- Module: Mathlib.LinearAlgebra.Span.Basic
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₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
hv : Eq (α := Submodule R M) (span R s) ⊤
h : Set.EqOn.{u_4, u_5} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) s
⊢ f = g

Tactic:
DFunLike.ext _ _ fun _ => eqOn_span h (eq_top_iff'.1 hv _)

Premises used: Submodule.eq_top_iff', DFunLike.ext, LinearMap.eqOn_span, Iff.mp
-- Module: Mathlib.LinearAlgebra.Span.Basic
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₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
ι : Sort u_8
v : ι → M
f g : M →ₛₗ[σ₁₂] M₂
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
h : ∀ (i : ι), Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) (v i) : M₂) ((g : (a : M) → M₂) (v i) : M₂)
⊢ f = g

Tactic:
ext_on hv (Set.forall_mem_range.2 h)

Premises used: Iff.mpr, Set.forall_mem_range, LinearMap.ext_on
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : Module.IsTorsionFree R M
x : M
h : x ≠ 0
⊢ Eq (α := Submodule R R) (ker (toSpanSingleton R M x)) ⊥

Tactic:
SetLike.ext fun _ => smul_eq_zero.trans <| or_iff_left_of_imp fun h' => (h h').elim

Premises used: or_iff_left_of_imp, False.elim, SetLike.ext, Iff.trans, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
K : Type u_3
V : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
x : V
hx : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) x : K) (0 : K)
y : V
h : Membership.mem (γ := Submodule K V) ⊤ y
⊢ y - HMul.hMul (α := K) (β := K) ((f : (a : V) → K) y : K) (((f : (a : V) → K) x)⁻¹ : K) • x ∈ f.ker ∧
    HMul.hMul (α := K) (β := K) ((f : (a : V) → K) y : K) (((f : (a : V) → K) x)⁻¹ : K) • x +
        (y - HMul.hMul (α := K) (β := K) ((f : (a : V) → K) y : K) (((f : (a : V) → K) x)⁻¹ : K) • x) =
      y

Tactic:
simp [hx]
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
x : M
h : x ≠ 0
t : R
⊢ ((toSpanNonzeroSingleton R M x h : LinearEquiv.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥(R ∙ x)) : (a : R) → ↥(R ∙ x))
      t =
    Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ x) x_1) (t • x) ⋯

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
x : M
h : x ≠ 0
m : ↥(R ∙ x)
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((symm (toSpanNonzeroSingleton R M x h) : (a : ↥(R ∙ x)) → R) m : R) x = (↑m : M)

Tactic:
congrArg Subtype.val <| apply_symm_apply (toSpanNonzeroSingleton R M x h) m

Premises used: congrArg, LinearEquiv.apply_symm_apply, Subtype.val, LinearEquiv.toSpanNonzeroSingleton
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
x : M
h : x ≠ 0
⊢ Eq (α := ↥(R ∙ x))
    (((toSpanNonzeroSingleton R M x h : LinearEquiv.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥(R ∙ x)) :
        (a : R) → ↥(R ∙ x))
      1)
    (Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ x) x_1) x ⋯)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
x : M
h : x ≠ 0
rw :
  Eq.{u_1 + 1} (α := R)
    ((coord R M x h : (a : ↥(R ∙ x)) → R)
        (((toSpanNonzeroSingleton R M x h : LinearEquiv.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥(R ∙ x)) :
            (a : R) → ↥(R ∙ x))
          1) :
      R)
    (1 : R)
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R)
    ((coord R M x h : (a : ↥(R ∙ x)) → R)
        (Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ x) x_1) x ⋯) :
      R)
    (1 : R)

Tactic:
rw [← toSpanNonzeroSingleton_one R M x h, LinearEquiv.symm_apply_apply]

Premises used: LinearEquiv.symm_apply_apply, LinearEquiv.toSpanNonzeroSingleton_one
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
x : M
h : x ≠ 0
y : ↥(R ∙ x)
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((coord R M x h : (a : ↥(R ∙ x)) → R) y : R) x = (↑y : M)

Tactic:
Subtype.ext_iff.1 <| (toSpanNonzeroSingleton R M x h).apply_symm_apply _

Premises used: Subtype.ext_iff, LinearEquiv.apply_symm_apply, Iff.mp, LinearEquiv.toSpanNonzeroSingleton
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x_1 : M
p p' : Submodule R M
inst_3 : Semiring R₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
F : Type u_8
inst_6 : FunLike F M M₂
inst_7 : SemilinearMapClass F σ₁₂ M M₂
x : R
⊢ IsPrincipal (M := R) (span R {x})

Tactic:
⟨x, rfl⟩

Premises used: Submodule.IsPrincipal.mk, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Submodule R M
inst_3 : S.IsPrincipal
⊢ span R {generator S} = S

Tactic:
(Classical.choose_spec (principal S)).symm

Premises used: Classical.choose_spec, Submodule.IsPrincipal.generator, Eq.symm, Submodule.IsPrincipal.principal
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
s : Set M
⊢ Membership.mem (γ := Submodule R M) (span R s) x ↔ ∀ (p : Submodule R M), s ⊆ (↑p : Set M) → x ∈ p

Tactic:
mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
⊢ s ⊆ (↑(span R s) : Set M)

Tactic:
fun _ h => mem_span.2 fun _ hp => hp h

Premises used: Iff.mpr, Set.Subset, Submodule.mem_span
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x : M
hx : x ∈ s
⊢ Membership.mem (γ := Submodule R M) (span R s) x

Tactic:
subset_span hx

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
p : Submodule R M
⊢ span R s ≤ p ↔ s ⊆ (↑p : Set M)

Tactic:
⟨Subset.trans subset_span, fun ss _ h => mem_span.1 h _ ss⟩

Premises used: Set.Subset.trans, Submodule.mem_span, Iff.intro, Iff.mp, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set M
h : s ⊆ t
⊢ LE.le (α := Submodule R M) (span R s) (span R t)

Tactic:
span_le.2 <| Subset.trans h subset_span

Premises used: Iff.mpr, Set.Subset.trans, Submodule.subset_span, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Monotone.{u_4, u_4} (α := Set M) (β := Submodule R M) (span R)

Tactic:
fun _ _ => span_mono

Premises used: Monotone, Submodule.span_mono
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
s : Set M
h₁ : s ⊆ (↑p : Set M)
h₂ : p ≤ span R s
⊢ span R s = p

Tactic:
le_antisymm (span_le.2 h₁) h₂

Premises used: Iff.mpr, le_antisymm, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ span R (↑p : Set M) = p

Tactic:
span_eq_of_le _ (Subset.refl _) subset_span

Premises used: Set.Subset.refl, Submodule.span_eq_of_le, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set M
hs : s ⊆ (↑(span R t) : Set M)
ht : t ⊆ (↑(span R s) : Set M)
⊢ Eq (α := Submodule R M) (span R s) (span R t)

Tactic:
le_antisymm (span_le.2 hs) (span_le.2 ht)

Premises used: Iff.mpr, le_antisymm, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Span.Defs
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 : SetLike S M
inst_4 : AddSubmonoidClass S M
inst_5 : SMulMemClass S R M
s : S
⊢ (↑(span R (↑s : Set M)) : Set M) = (↑s : Set M)

Tactic:
le_antisymm ?_ subset_span

Premises used: le_antisymm, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Span.Defs
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 : SetLike S M
inst_4 : AddSubmonoidClass S M
inst_5 : SMulMemClass S R M
s : S
refine : (↑(span R (↑s : Set M)) : Set M) ≤ (↑s : Set M)
⊢ (↑(span R (↑s : Set M)) : Set M) = (↑s : Set M)

Tactic:
refine le_antisymm ?_ subset_span

Premises used: le_antisymm, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Span.Defs
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 : SetLike S M
inst_4 : AddSubmonoidClass S M
inst_5 : SMulMemClass S R M
s : S
s' : Submodule R M := { carrier := (↑s : Set M), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ (↑(span R (↑s : Set M)) : Set M) ≤ (↑s : Set M)

Tactic:
span_le (p := s') |>.mpr le_rfl

Premises used: Iff.mpr, le_rfl, Set.Mem, Set.Subset, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Span.Defs
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 : SetLike S M
inst_4 : AddSubmonoidClass S M
inst_5 : SMulMemClass S R M
s : S
s' : Submodule R M := { carrier := (↑s : Set M), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ (↑(span R (↑s : Set M)) : Set M) ≤ (↑s : Set M)

Tactic:
exact span_le (p := s') |>.mpr le_rfl

Premises used: Iff.mpr, le_rfl, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
⊢ Eq (α := Submodule R M) (span R (insert 0 s)) (span R s)

Tactic:
le_antisymm ?_ (Submodule.span_mono (Set.subset_insert 0 s))

Premises used: le_antisymm, Submodule.span_mono, OfNat.ofNat, Set.subset_insert
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
refine : LE.le (α := Submodule R M) (span R (insert 0 s)) (span R s)
⊢ Eq (α := Submodule R M) (span R (insert 0 s)) (span R s)

Tactic:
refine le_antisymm ?_ (Submodule.span_mono (Set.subset_insert 0 s))

Premises used: le_antisymm, Submodule.span_mono, OfNat.ofNat, Set.subset_insert
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
rw : 0 ∈ (↑(span R s) : Set M) ∧ s ⊆ (↑(span R s) : Set M)
⊢ LE.le (α := Submodule R M) (span R (insert 0 s)) (span R s)

Tactic:
rw [span_le, Set.insert_subset_iff]

Premises used: Set.insert_subset_iff, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
⊢ 0 ∈ (↑(span R s) : Set M)

Tactic:
simp only [SetLike.mem_coe, Submodule.zero_mem]

Premises used: Submodule.zero_mem, SetLike.mem_coe
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
⊢ 0 ∈ (↑(span R s) : Set M) ∧ s ⊆ (↑(span R s) : Set M)

Tactic:
exact ⟨by simp only [SetLike.mem_coe, Submodule.zero_mem], Submodule.subset_span⟩