awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p p' : Submodule R M
⊢ map f p ≤ map f p' ↔ p ≤ p' ⊔ f.ker
have rw : p ≤ comap f (map f p') ↔ p ≤ p' ⊔ f.ker
Tactic: rw [map_le_iff_le_comap, Submodule.comap_map_eq]
-- 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 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p p' : Submodule R M
rw : p ≤ comap f (map f p') ↔ p ≤ p' ⊔ f.ker
⊢ map f p ≤ map f p' ↔ p ≤ p' ⊔ f.ker
have rw₁ : p ≤ p' ⊔ f.ker ↔ p ≤ p' ⊔ f.ker
Tactic: rw [map_le_iff_le_comap, Submodule.comap_map_eq]
-- 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 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.ker = ⊥
p p' : Submodule R M
⊢ map f p ≤ map f p' ↔ p ≤ p'
have rw : p ≤ p' ⊔ f.ker ↔ p ≤ p'
Tactic: rw [LinearMap.map_le_map_iff, hf, sup_bot_eq]
-- 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 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.ker = ⊥
p p' : Submodule R M
rw : p ≤ p' ⊔ f.ker ↔ p ≤ p'
⊢ map f p ≤ map f p' ↔ p ≤ p'
have rw₁ : p ≤ p' ⊔ ⊥ ↔ p ≤ p'
Tactic: rw [LinearMap.map_le_map_iff, hf, sup_bot_eq]
-- 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 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.ker = ⊥
p p' : Submodule R M
rw : p ≤ p' ⊔ f.ker ↔ p ≤ p'
rw₁ : p ≤ p' ⊔ ⊥ ↔ p ≤ p'
⊢ map f p ≤ map f p' ↔ p ≤ p'
have rw₂ : p ≤ p' ↔ p ≤ p'
Tactic: rw [LinearMap.map_le_map_iff, hf, sup_bot_eq]
-- 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 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⊤
p : Submodule R M
⊢ map f p = ⊤ ↔ p ⊔ f.ker = ⊤
have simp_rw : ⊤ ≤ map f p ↔ ⊤ ≤ p ⊔ f.ker
Tactic: simp_rw [← top_le_iff, ← hf, range_eq_map, LinearMap.map_le_map_iff]
-- 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 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⊤
p : Submodule R M
simp_rw : ⊤ ≤ map f p ↔ ⊤ ≤ p ⊔ f.ker
⊢ map f p = ⊤ ↔ p ⊔ f.ker = ⊤
have simp_rw₁ : f.range ≤ map f p ↔ ⊤ ≤ p ⊔ f.ker
Tactic: simp_rw [← top_le_iff, ← hf, range_eq_map, LinearMap.map_le_map_iff]
-- 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 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⊤
p : Submodule R M
simp_rw : ⊤ ≤ map f p ↔ ⊤ ≤ p ⊔ f.ker
simp_rw₁ : f.range ≤ map f p ↔ ⊤ ≤ p ⊔ f.ker
⊢ map f p = ⊤ ↔ p ⊔ f.ker = ⊤
have simp_rw₂ : map f ⊤ ≤ map f p ↔ ⊤ ≤ p ⊔ f.ker
Tactic: simp_rw [← top_le_iff, ← hf, range_eq_map, LinearMap.map_le_map_iff]
-- 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
⊢ Eq (α := R →ₗ[R] M) (toSpanSingleton R M 0) 0
have h : Eq.{u_4 + 1} (α := M) ((toSpanSingleton R M 0 : (a : R) → M) 1 : M) ((0 : (a : R) → M) 1 : M)
Tactic: ext
-- 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
x : M
⊢ Eq (α := R →ₗ[R] M) (toSpanSingleton R M x) 0 ↔ x = 0
have rw : Eq (α := R →ₗ[R] M) (toSpanSingleton R M x) (toSpanSingleton R M 0) ↔ x = 0
Tactic: rw [← toSpanSingleton_zero, (toSpanSingleton_injective R M).eq_iff]
-- 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
x : M
rw : Eq (α := R →ₗ[R] M) (toSpanSingleton R M x) (toSpanSingleton R M 0) ↔ x = 0
⊢ Eq (α := R →ₗ[R] M) (toSpanSingleton R M x) 0 ↔ x = 0
have rw₁ : x = 0 ↔ x = 0
Tactic: rw [← toSpanSingleton_zero, (toSpanSingleton_injective R M).eq_iff]
-- 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
x y : M
⊢ toSpanSingleton R M (x + y) = HAdd.hAdd (α := R →ₗ[R] M) (toSpanSingleton R M x) (toSpanSingleton R M y)
have 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)
Tactic: ext
-- 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 : Type u_8
inst_3 : Monoid S
inst_4 : DistribMulAction S M
inst_5 : SMulCommClass R S M
r : S
x : M
⊢ toSpanSingleton R M (r • x) = HSMul.hSMul (β := R →ₗ[R] M) r (toSpanSingleton R M x)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
e : R
⊢ IsIdempotentElem (M := R →ₗ[R] R) (toSpanSingleton R R e) ↔ IsIdempotentElem e
have simp_rw : (∀ (x : R), x * (e * e) = x * e) ↔ e * e = e
Tactic: simp_rw [IsIdempotentElem, LinearMap.ext_iff, Module.End.mul_apply, toSpanSingleton_apply,
    smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
e : R
h : ∀ (x : R), x * (e * e) = x * e
| e
have rw : e * e
Tactic: rw [← one_mul e, ← h, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
e : R
h : ∀ (x : R), x * (e * e) = x * e
⊢ e * e = e
have conv_rhs : e * e = e
Tactic: conv_rhs => rw [← one_mul e, ← h, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
e : R
h : ∀ (x : R), x * (e * e) = x * e
conv_rhs : e * e = e
⊢ e * e = e
have conv_rhs₁ : e * e = e * e
Tactic: conv_rhs => rw [← one_mul e, ← h, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
e : R
h : e * e = e
x : R
⊢ x * (e * e) = x * e
have rw : x * e = x * e
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
f : Module.End R R
⊢ IsIdempotentElem (M := R) ((f : (a : R) → R) 1 : R) ↔ IsIdempotentElem f
have 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)
Tactic: rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, IsIdempotentElem,
    LinearMap.ext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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 * f : (a : R) → R) x : R) ((f : (a : R) → R) x : R)
have 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)
Tactic: simp_rw [Module.End.mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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
⊢ Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) r : R) : R) ((f : (a : R) → R) r : R)
have rw : Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) (r * 1) : R) : R) ((f : (a : R) → R) (r * 1) : R)
Tactic: rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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)
⊢ Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) r : R) : R) ((f : (a : R) → R) r : R)
have 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)
Tactic: rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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)
⊢ Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) r : R) : R) ((f : (a : R) → R) r : R)
have 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)
Tactic: rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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)
⊢ Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) r : R) : R) ((f : (a : R) → R) r : R)
have 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)
Tactic: rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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)
⊢ Eq (α := R) ((f : (a : R) → R) ((f : (a : R) → R) r : R) : R) ((f : (a : R) → R) r : R)
have rw₄ : HSMul.hSMul (β := R) r ((f : (a : R) → R) 1 : R) = HSMul.hSMul (β := R) r ((f : (a : R) → R) 1 : R)
Tactic: rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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
⊢ f ∘ₗ toSpanSingleton R M x = toSpanSingleton R M₂ ((f : (a : M) → M₂) x)
have 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₂)
Tactic: ext
-- 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 : Submodule R M
x : M
hx : x ∈ N
⊢ submoduleOf (R ∙ x) N = R ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx
have 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
Tactic: ext y
-- 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 : Submodule R M
x : M
hx : x ∈ N
y : ↥N
⊢ y ∈ submoduleOf (R ∙ x) N ↔ Membership.mem (γ := Submodule R ↥N) (R ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx) y
have h : (∃ (a : R), a • x = (↑y : M)) ↔ ∃ (a : R), a • Subtype.mk (p := fun (x : M) ↦ x ∈ N) x hx = y
Tactic: simp_rw [submoduleOf, mem_comap, subtype_apply, mem_span_singleton]
-- 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₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
⊢ 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
have rw : s ⊆ (↑(eqLocus f g) : Set M) ↔ Set.EqOn.{u_4, u_5} (β := M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) s
Tactic: rw [← le_eqLocus, span_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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.{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)
have 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)
Tactic: rw [← toSpanNonzeroSingleton_one R M x h, LinearEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
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)
⊢ 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)
have rw₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [← toSpanNonzeroSingleton_one R M x h, LinearEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (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 : 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)
have refine : (↑(span R (↑s : Set M)) : Set M) ≤ (↑s : Set M)
Tactic: refine le_antisymm ?_ subset_span
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (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
⊢ Eq (α := Submodule R M) (span R (insert 0 s)) (span R s)
have refine : LE.le (α := Submodule R M) (span R (insert 0 s)) (span R s)
Tactic: refine le_antisymm ?_ (Submodule.span_mono (Set.subset_insert 0 s))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (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
⊢ LE.le (α := Submodule R M) (span R (insert 0 s)) (span R s)
have rw : 0 ∈ (↑(span R s) : Set M) ∧ s ⊆ (↑(span R s) : Set M)
Tactic: rw [span_le, Set.insert_subset_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (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
⊢ Eq (α := Submodule R M) (span R (s \ {0})) (span R s)
have pos : ∀ (h : 0 ∈ s), Eq (α := Submodule R M) (span R (s \ {0})) (span R s)
Tactic: by_cases h : 0 ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (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
pos : ∀ (h : 0 ∈ s), Eq (α := Submodule R M) (span R (s \ {0})) (span R s)
⊢ Eq (α := Submodule R M) (span R (s \ {0})) (span R s)
have neg : ∀ (h : 0 ∉ s), Eq (α := Submodule R M) (span R (s \ {0})) (span R s)
Tactic: by_cases h : 0 ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (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
h : 0 ∈ s
⊢ Eq (α := Submodule R M) (span R (s \ {0})) (span R s)
have pos : Eq (α := Submodule R M) (span R (insert 0 (s \ {0}))) (span R s)
Tactic: rw [← span_insert_zero, show insert 0 (s \ {0}) = s by simp [h]]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (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
h : 0 ∈ s
pos : Eq (α := Submodule R M) (span R (insert 0 (s \ {0}))) (span R s)
⊢ Eq (α := Submodule R M) (span R (s \ {0})) (span R s)
have pos₁ : Eq (α := Submodule R M) (span R s) (span R s)
Tactic: rw [← span_insert_zero, show insert 0 (s \ {0}) = s by simp [h]]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (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
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
t : Set N
p :
  (x : M) →
    (y : N) → Membership.mem (γ := Submodule R M) (span R s) x → Membership.mem (γ := Submodule R N) (span R t) y → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : Membership.mem (γ := Submodule R N) (span R t) y), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (span R s) y) (hz : Membership.mem (γ := Submodule R N) (span R t) z),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y) (hz : Membership.mem (γ := Submodule R N) (span R t) z),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left :
  ∀ (r : R) (x : M) (y : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x : M) (y : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y), p x y hx hy → p x (r • y) hx ⋯
a : M
b : N
ha : Membership.mem (γ := Submodule R M) (span R s) a
z : N
hz : z ∈ t
⊢ p a z ha ⋯
have mem : ∀ (x : M) (h : x ∈ s), p x z sorry sorry
Tactic: induction ha using span_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | zero => exact zero_left _ _
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | smul _ _ _ h => exact smul_left _ _ _ _ _ h
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (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
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
t : Set N
p :
  (x : M) →
    (y : N) → Membership.mem (γ := Submodule R M) (span R s) x → Membership.mem (γ := Submodule R N) (span R t) y → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : Membership.mem (γ := Submodule R N) (span R t) y), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (span R s) y) (hz : Membership.mem (γ := Submodule R N) (span R t) z),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y) (hz : Membership.mem (γ := Submodule R N) (span R t) z),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left :
  ∀ (r : R) (x : M) (y : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x : M) (y : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y), p x y hx hy → p x (r • y) hx ⋯
a : M
b : N
ha : Membership.mem (γ := Submodule R M) (span R s) a
z : N
hz : z ∈ t
mem : ∀ (x : M) (h : x ∈ s), p x z ⋯ ⋯
⊢ p a z ha ⋯
have mem₁ : p 0 z sorry sorry
Tactic: induction ha using span_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | zero => exact zero_left _ _
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | smul _ _ _ h => exact smul_left _ _ _ _ _ h
Cleared hypotheses: ha