awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
p p' : Submodule R M
m : M
mp : (∃ y ∈ p, ∃ z ∈ p', y + z = m) → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr : (∃ u ∈ p, ∃ v ∈ p', m = u + v) → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₁ mp₂ mp₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₁ mpr₂ mpr₃ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₄ mp₅ mp₆ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₄ mpr₅ mpr₆ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₇ mp₈ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
have mp₉ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
Tactic: tauto
-- 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
p p' : Submodule R M
m : M
mp : (∃ y ∈ p, ∃ z ∈ p', y + z = m) → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr : (∃ u ∈ p, ∃ v ∈ p', m = u + v) → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₁ mp₂ mp₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₁ mpr₂ mpr₃ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₄ mp₅ mp₆ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₄ mpr₅ mpr₆ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₇ mp₈ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mp₉ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
have mp₁₀ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
Tactic: tauto
-- 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
p p' : Submodule R M
m : M
mp : (∃ y ∈ p, ∃ z ∈ p', y + z = m) → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr : (∃ u ∈ p, ∃ v ∈ p', m = u + v) → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₁ mp₂ mp₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₁ mpr₂ mpr₃ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₄ mp₅ mp₆ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₄ mpr₅ mpr₆ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₇ mp₈ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mp₉ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
mp₁₀ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₁ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
mp₁₂ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
have mp₁₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p
Tactic: tauto
-- 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
p p' : Submodule R M
m : M
mp : (∃ y ∈ p, ∃ z ∈ p', y + z = m) → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr : (∃ u ∈ p, ∃ v ∈ p', m = u + v) → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₁ mp₂ mp₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₁ mpr₂ mpr₃ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₄ mp₅ mp₆ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₄ mpr₅ mpr₆ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₇ mp₈ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mp₉ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
mp₁₀ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₁ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
mp₁₂ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
have mp₁₄ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
Tactic: tauto
-- 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
p p' : Submodule R M
m : M
mp : (∃ y ∈ p, ∃ z ∈ p', y + z = m) → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr : (∃ u ∈ p, ∃ v ∈ p', m = u + v) → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₁ mp₂ mp₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₁ mpr₂ mpr₃ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₄ mp₅ mp₆ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₄ mpr₅ mpr₆ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₇ mp₈ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mp₉ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
mp₁₀ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₁ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
mp₁₂ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p
mp₁₄ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mp₁₅ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₆ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p
mp₁₇ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mp₁₈ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₉ mp₂₀ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mpr₇ mpr₈ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
have mpr₉ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → w ∈ p ∧ ∃ z ∈ p', w + z = m
Tactic: tauto
-- 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
p p' : Submodule R M
m : M
mp : (∃ y ∈ p, ∃ z ∈ p', y + z = m) → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr : (∃ u ∈ p, ∃ v ∈ p', m = u + v) → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₁ mp₂ mp₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₁ mpr₂ mpr₃ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₄ mp₅ mp₆ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₄ mpr₅ mpr₆ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₇ mp₈ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mp₉ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
mp₁₀ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₁ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
mp₁₂ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p
mp₁₄ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mp₁₅ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₆ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p
mp₁₇ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mp₁₈ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₉ mp₂₀ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mpr₇ mpr₈ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mpr₉ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → w ∈ p ∧ ∃ z ∈ p', w + z = m
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
have mpr₁₀ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → m = w + w_1 → M
Tactic: tauto
-- 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
p p' : Submodule R M
m : M
mp : (∃ y ∈ p, ∃ z ∈ p', y + z = m) → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr : (∃ u ∈ p, ∃ v ∈ p', m = u + v) → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₁ mp₂ mp₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₁ mpr₂ mpr₃ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₄ mp₅ mp₆ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₄ mpr₅ mpr₆ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₇ mp₈ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mp₉ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
mp₁₀ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₁ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
mp₁₂ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p
mp₁₄ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mp₁₅ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₆ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p
mp₁₇ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mp₁₈ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₉ mp₂₀ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mpr₇ mpr₈ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mpr₉ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → w ∈ p ∧ ∃ z ∈ p', w + z = m
mpr₁₀ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → m = w + w_1 → M
mpr₁₁ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → w ∈ p ∧ ∃ z ∈ p', w + z = m
mpr₁₂ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → m = w + w_1 → M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
have mpr₁₃ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → w ∈ p
Tactic: tauto
-- 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
p p' : Submodule R M
m : M
mp : (∃ y ∈ p, ∃ z ∈ p', y + z = m) → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr : (∃ u ∈ p, ∃ v ∈ p', m = u + v) → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₁ mp₂ mp₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₁ mpr₂ mpr₃ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₄ mp₅ mp₆ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₄ mpr₅ mpr₆ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₇ mp₈ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mp₉ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
mp₁₀ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₁ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
mp₁₂ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p
mp₁₄ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mp₁₅ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₆ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p
mp₁₇ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mp₁₈ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₉ mp₂₀ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mpr₇ mpr₈ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mpr₉ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → w ∈ p ∧ ∃ z ∈ p', w + z = m
mpr₁₀ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → m = w + w_1 → M
mpr₁₁ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → w ∈ p ∧ ∃ z ∈ p', w + z = m
mpr₁₂ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → m = w + w_1 → M
mpr₁₃ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → w ∈ p
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
have mpr₁₄ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ z ∈ p', w + z = m
Tactic: tauto
-- 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
p p' : Submodule R M
P : M → Prop
⊢ (∀ x ∈ p ⊔ p', P x) ↔ ∀ x₁ ∈ p, ∀ x₂ ∈ p', P (x₁ + x₂)
have simp : (∀ (x x_1 : M), x_1 ∈ p → ∀ x_2 ∈ p', x_1 + x_2 = x → P x) ↔ ∀ x₁ ∈ p, ∀ x₂ ∈ p', P (x₁ + x₂)
Tactic: simp [mem_sup]
-- 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
x : M
h : x ≠ 0
⊢ ∃ (x_1 : ↥(R ∙ x)) (y : ↥(R ∙ x)), x_1 ≠ y
have h₁ : Ne (α := ↥(R ∙ x)) 0 (Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ x) x_1) x sorry)
Tactic: use 0, ⟨x, Submodule.mem_span_singleton_self x⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (hypothesis)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
h : x ≠ 0
H : Eq (α := ↥(R ∙ x)) 0 (Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ x) x_1) x ⋯)
⊢ False
have H₁ : x = 0
Tactic: rw [eq_comm, Submodule.mk_eq_zero] at H
Cleared hypotheses: 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
x y : M
h : Membership.mem (γ := Submodule R M) (R ∙ y) x
⊢ ∃ (a : R), a • y = x
have refine_1 : ∀ (x : M) (h : Membership.mem (γ := Set M) {y} x), ∃ (a : R), a • y = x
Tactic: refine span_induction ?_ ?_ ?_ ?_ 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
x y : M
h : Membership.mem (γ := Submodule R M) (R ∙ y) x
refine_1 : ∀ (x : M) (h : Membership.mem (γ := Set M) {y} x), ∃ (a : R), a • y = x
⊢ ∃ (a : R), a • y = x
have refine_2 : ∃ (a : R), a • y = 0
Tactic: refine span_induction ?_ ?_ ?_ ?_ 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
x y : M
h : Membership.mem (γ := Submodule R M) (R ∙ y) x
refine_1 : ∀ (x : M) (h : Membership.mem (γ := Set M) {y} x), ∃ (a : R), a • y = x
refine_2 : ∃ (a : R), a • y = 0
⊢ ∃ (a : R), a • y = x
have refine_3 : ∀ (x y_1 : M) (hx : Membership.mem (γ := Submodule R M) (R ∙ y) x)
  (hy : Membership.mem (γ := Submodule R M) (R ∙ y) y_1),
  (∃ (a : R), a • y = x) → (∃ (a : R), a • y = y_1) → ∃ (a : R), a • y = x + y_1
Tactic: refine span_induction ?_ ?_ ?_ ?_ 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
x y : M
h : Membership.mem (γ := Submodule R M) (R ∙ y) x
refine_1 : ∀ (x : M) (h : Membership.mem (γ := Set M) {y} x), ∃ (a : R), a • y = x
refine_2 : ∃ (a : R), a • y = 0
refine_3 :
  ∀ (x y_1 : M) (hx : Membership.mem (γ := Submodule R M) (R ∙ y) x)
    (hy : Membership.mem (γ := Submodule R M) (R ∙ y) y_1),
    (∃ (a : R), a • y = x) → (∃ (a : R), a • y = y_1) → ∃ (a : R), a • y = x + y_1
⊢ ∃ (a : R), a • y = x
have refine_4 : ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (R ∙ y) x),
  (∃ (a : R), a • y = x) → ∃ (a_2 : R), a_2 • y = a • x
Tactic: refine span_induction ?_ ?_ ?_ ?_ 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 : Submodule R M
f : LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥s
hf : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := ↥s) (⇑f : (a : R) → ↥s)
⊢ s = R ∙ (↑((f : (a : R) → ↥s) 1) : M)
have refine : ∀ (x : M) (hx : x ∈ s), ∃ (a : R), HSMul.hSMul (β := M) a (↑((f : (a : R) → ↥s) 1) : M) = x
Tactic: refine le_antisymm (fun x hx ↦ mem_span_singleton.mpr ?_)
    (span_le.mpr <| by rintro _ rfl; exact (f 1).2)
-- 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 : Submodule R M
f : LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥s
hf : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := ↥s) (⇑f : (a : R) → ↥s)
x : M
hx : x ∈ s
⊢ ∃ (a : R), HSMul.hSMul (β := M) a (↑((f : (a : R) → ↥s) 1) : M) = x
have have : ∀ (r : R) (eq : (f : (a : R) → ↥s) r = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx),
  ∃ (a : R), HSMul.hSMul (β := M) a (↑((f : (a : R) → ↥s) 1) : M) = x
Tactic: have ⟨r, eq⟩ := hf ⟨x, hx⟩
-- 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 : Submodule R M
f : LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥s
hf : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := ↥s) (⇑f : (a : R) → ↥s)
x : M
hx : x ∈ s
r : R
eq : (f : (a : R) → ↥s) r = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx
⊢ HSMul.hSMul (β := M) r (↑((f : (a : R) → ↥s) 1) : M) = x
have rw : (↑(HSMul.hSMul (β := ↥s) r ((f : (a : R) → ↥s) 1)) : M) = x
Tactic: rw [← coe_smul, ← map_smul, smul_eq_mul, mul_one, eq]
-- 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 : Submodule R M
f : LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥s
hf : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := ↥s) (⇑f : (a : R) → ↥s)
x : M
hx : x ∈ s
r : R
eq : (f : (a : R) → ↥s) r = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx
rw : (↑(HSMul.hSMul (β := ↥s) r ((f : (a : R) → ↥s) 1)) : M) = x
⊢ HSMul.hSMul (β := M) r (↑((f : (a : R) → ↥s) 1) : M) = x
have rw₁ : (↑((f : (a : R) → ↥s) (HSMul.hSMul (β := R) r 1)) : M) = x
Tactic: rw [← coe_smul, ← map_smul, smul_eq_mul, mul_one, eq]
-- 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 : Submodule R M
f : LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥s
hf : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := ↥s) (⇑f : (a : R) → ↥s)
x : M
hx : x ∈ s
r : R
eq : (f : (a : R) → ↥s) r = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx
rw : (↑(HSMul.hSMul (β := ↥s) r ((f : (a : R) → ↥s) 1)) : M) = x
rw₁ : (↑((f : (a : R) → ↥s) (HSMul.hSMul (β := R) r 1)) : M) = x
⊢ HSMul.hSMul (β := M) r (↑((f : (a : R) → ↥s) 1) : M) = x
have rw₂ : (↑((f : (a : R) → ↥s) (r * 1)) : M) = x
Tactic: rw [← coe_smul, ← map_smul, smul_eq_mul, mul_one, eq]
-- 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 : Submodule R M
f : LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥s
hf : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := ↥s) (⇑f : (a : R) → ↥s)
x : M
hx : x ∈ s
r : R
eq : (f : (a : R) → ↥s) r = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx
rw : (↑(HSMul.hSMul (β := ↥s) r ((f : (a : R) → ↥s) 1)) : M) = x
rw₁ : (↑((f : (a : R) → ↥s) (HSMul.hSMul (β := R) r 1)) : M) = x
rw₂ : (↑((f : (a : R) → ↥s) (r * 1)) : M) = x
⊢ HSMul.hSMul (β := M) r (↑((f : (a : R) → ↥s) 1) : M) = x
have rw₃ : (↑((f : (a : R) → ↥s) r) : M) = x
Tactic: rw [← coe_smul, ← map_smul, smul_eq_mul, mul_one, eq]
-- 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 : Submodule R M
f : LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥s
hf : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := ↥s) (⇑f : (a : R) → ↥s)
x : M
hx : x ∈ s
r : R
eq : (f : (a : R) → ↥s) r = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx
rw : (↑(HSMul.hSMul (β := ↥s) r ((f : (a : R) → ↥s) 1)) : M) = x
rw₁ : (↑((f : (a : R) → ↥s) (HSMul.hSMul (β := R) r 1)) : M) = x
rw₂ : (↑((f : (a : R) → ↥s) (r * 1)) : M) = x
rw₃ : (↑((f : (a : R) → ↥s) r) : M) = x
⊢ HSMul.hSMul (β := M) r (↑((f : (a : R) → ↥s) 1) : M) = x
have rw₄ : (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx) : M) = x
Tactic: rw [← coe_smul, ← map_smul, smul_eq_mul, mul_one, eq]
-- 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
x : M
⊢ Eq (α := Submodule R M) (R ∙ x) ⊤ ↔ ∀ (v : M), ∃ (r : R), r • x = v
have rw : (∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v) ↔ ∀ (v : M), ∃ (r : R), r • x = v
Tactic: rw [eq_top_iff, le_span_singleton_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
x : M
⊢ (∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v) ↔ ∀ (v : M), ∃ (r : R), r • x = v
have mp : (∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v) → ∀ (v : M), ∃ (r : R), r • x = v
Tactic: tauto
-- 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
x : M
mp : (∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v) → ∀ (v : M), ∃ (r : R), r • x = v
⊢ (∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v) ↔ ∀ (v : M), ∃ (r : R), r • x = v
have mpr : (∀ (v : M), ∃ (r : R), r • x = v) → ∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v
Tactic: tauto
-- 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
⊢ Eq (α := Submodule R M) (R ∙ 0) ⊥
have h : ∀ (x : M), Membership.mem (γ := Submodule R M) (R ∙ 0) x ↔ Membership.mem (γ := Submodule R M) ⊥ x
Tactic: ext
-- 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 : Type u_9
inst_3 : SMul S R
inst_4 : SMul S M
inst_5 : IsScalarTower S R M
r : S
x : M
⊢ LE.le (α := Submodule R M) (R ∙ r • x) (R ∙ x)
have rw : Membership.mem (γ := Submodule R M) (R ∙ x) (r • x)
Tactic: rw [span_le, Set.singleton_subset_iff, SetLike.mem_coe]
-- 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
G : Type u_9
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
g : G
x : M
⊢ Eq (α := Submodule R M) (R ∙ g • x) (R ∙ x)
have refine : LE.le (α := Submodule R M) (R ∙ x) (R ∙ g • x)
Tactic: refine le_antisymm (span_singleton_smul_le R g x) ?_
-- 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
G : Type u_9
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
g : G
x : M
⊢ LE.le (α := Submodule R M) (R ∙ x) (R ∙ g • x)
have h : x = g⁻¹ • g • x
Tactic: convert! span_singleton_smul_le R g⁻¹ (g • x)
-- 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
r : R
hr : IsUnit r
x : M
⊢ Eq (α := Submodule R M) (R ∙ r • x) (R ∙ x)
have lift : ∀ (r : Rˣ), Eq (α := Submodule R M) (R ∙ (↑r : R) • x) (R ∙ x)
Tactic: lift r to Rˣ using hr
Cleared hypotheses: r, hr
-- 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
x : M
r : Rˣ
⊢ Eq (α := Submodule R M) (R ∙ (↑r : R) • x) (R ∙ x)
have rw : Eq (α := Submodule R M) (R ∙ r • x) (R ∙ x)
Tactic: rw [← Units.smul_def]
-- 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
x y z : M
hxy : Membership.mem (γ := Submodule R M) (R ∙ y) x
hyz : Membership.mem (γ := Submodule R M) (R ∙ z) y
⊢ Membership.mem (γ := Submodule R M) (R ∙ z) x
have rw : ∀ (hxy : {x} ⊆ (↑(R ∙ y) : Set M)) (hyz : {y} ⊆ (↑(R ∙ z) : Set M)), {x} ⊆ (↑(R ∙ z) : Set M)
Tactic: rw [← SetLike.mem_coe, ← singleton_subset_iff] at *
Cleared hypotheses: hxy, hyz
-- 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
x : M
s : Set M
⊢ Eq (α := Submodule R M) (span R (insert x s)) (R ∙ x ⊔ span R s)
have rw : Eq (α := Submodule R M) (span R ({x} ∪ s)) (R ∙ x ⊔ span R s)
Tactic: rw [insert_eq, span_union]
-- 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
x : M
s : Set M
rw : Eq (α := Submodule R M) (span R ({x} ∪ s)) (R ∙ x ⊔ span R s)
⊢ Eq (α := Submodule R M) (span R (insert x s)) (R ∙ x ⊔ span R s)
have rw₁ : Eq (α := Submodule R M) (R ∙ x ⊔ span R s) (R ∙ x ⊔ span R s)
Tactic: rw [insert_eq, span_union]