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
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x_1 : ↥(⨆ i ∈ s, p i)
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x
h :
  Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
this :
  Membership.mem (γ := Submodule R M)
    (map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i))
      (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)))
    x
obtain :
  ∀ (y : ↥(⨆ i ∈ s, p i))
    (hy : Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)) y)
    (hx :
      Membership.mem (α := M) (γ := Submodule R M) (⨆ i ∈ s, p i)
        ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y : M)),
    Membership.mem (α := ↥(⨆ i ∈ s, p i)) (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x)
            ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y) hx :
          ↥(⨆ i ∈ s, p i)) →
      ∀
        (this :
          Membership.mem (α := M) (γ := Submodule R M)
            (map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i))
              (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)))
            ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y : M)),
        Membership.mem (α := ↥(⨆ i ∈ s, p i)) (γ := Submodule R ↥(⨆ i ∈ s, p i))
          (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i))
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x)
              ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y) hx :
            ↥(⨆ i ∈ s, p i))
⊢ Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i))
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)

Tactic:
obtain ⟨y, hy, rfl⟩ := Submodule.mem_map.mp this

Premises used: Submodule.mem_map, Iff.mp, rfl
-- 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
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x y : ↥(⨆ i ∈ s, p i)
hy : Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)) y
hx :
  Membership.mem (α := M) (γ := Submodule R M) (⨆ i ∈ s, p i)
    ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y : M)
h :
  Membership.mem (α := ↥(⨆ i ∈ s, p i)) (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x)
        ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y) hx :
      ↥(⨆ i ∈ s, p i))
this :
  Membership.mem (α := M) (γ := Submodule R M)
    (map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i))
      (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)))
    ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y : M)
⊢ Membership.mem (α := ↥(⨆ i ∈ s, p i)) (γ := Submodule R ↥(⨆ i ∈ s, p i))
    (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i))
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x)
        ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y) hx :
      ↥(⨆ i ∈ s, p i))

Tactic:
hy

Premises used: Set.Mem
-- 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
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x y : ↥(⨆ i ∈ s, p i)
hy : Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)) y
hx :
  Membership.mem (α := M) (γ := Submodule R M) (⨆ i ∈ s, p i)
    ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y : M)
h :
  Membership.mem (α := ↥(⨆ i ∈ s, p i)) (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x)
        ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y) hx :
      ↥(⨆ i ∈ s, p i))
this :
  Membership.mem (α := M) (γ := Submodule R M)
    (map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i))
      (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)))
    ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y : M)
⊢ Membership.mem (α := ↥(⨆ i ∈ s, p i)) (γ := Submodule R ↥(⨆ i ∈ s, p i))
    (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i))
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x)
        ((Submodule.subtype (⨆ i ∈ s, p i) : (a : ↥(⨆ i ∈ s, p i)) → M) y) hx :
      ↥(⨆ i ∈ s, p i))

Tactic:
exact hy
-- 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
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x_1 : ↥(⨆ i ∈ s, p i)
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x
h :
  Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
suffices :
  Membership.mem (γ := Submodule R M)
    (map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i))
      (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)))
    x
⊢ Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i))
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)

Tactic:
suffices x ∈ (⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype).map (⨆ i ∈ s, (p i)).subtype by
    obtain ⟨y, hy, rfl⟩ := Submodule.mem_map.mp this
    exact hy
-- 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
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x_1 : ↥(⨆ i ∈ s, p i)
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x
h :
  Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
this :
  ∀ i ∈ s,
    map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i)) (comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)) = p i
⊢ Membership.mem (γ := Submodule R M)
    (map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i))
      (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)))
    x

Tactic:
simpa only [map_iSup, biSup_congr this]

Premises used: Submodule.map_iSup, biSup_congr
-- 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
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x_1 : ↥(⨆ i ∈ s, p i)
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x
h :
  Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
suffices :
  ∀ i ∈ s,
    map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i)) (comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)) = p i
⊢ Membership.mem (γ := Submodule R M)
    (map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i))
      (⨆ i ∈ s, comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)))
    x

Tactic:
suffices ∀ i ∈ s, (comap (⨆ i ∈ s, p i).subtype (p i)).map (⨆ i ∈ s, p i).subtype = p i by
    simpa only [map_iSup, biSup_congr this]
-- 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
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x_1 : ↥(⨆ i ∈ s, p i)
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x
h :
  Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
i : ι
hi : i ∈ s
rw : p i ≤ ⨆ i ∈ s, p i
⊢ map (M := ↥(⨆ i ∈ s, p i)) (Submodule.subtype (⨆ i ∈ s, p i)) (comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i)) = p i

Tactic:
rw [map_comap_eq, range_subtype, inf_eq_right]

Premises used: Submodule.map_comap_eq, inf_eq_right, Submodule.range_subtype
-- 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
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x_1 : ↥(⨆ i ∈ s, p i)
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x
h :
  Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
i : ι
hi : i ∈ s
⊢ p i ≤ ⨆ i ∈ s, p i

Tactic:
le_biSup p hi

Premises used: Set.Mem, setOf, le_biSup
-- 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
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x_1 : ↥(⨆ i ∈ s, p i)
x : M
hx : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x
h :
  Membership.mem (γ := Submodule R ↥(⨆ i ∈ s, p i)) ⊤
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) x) x hx)
i : ι
hi : i ∈ s
⊢ p i ≤ ⨆ i ∈ s, p i

Tactic:
exact le_biSup p hi

Premises used: le_biSup
-- 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₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
N : Submodule R M
f : LinearMap.{u_1, u_2, u_4, u_5} σ₁₂ (↥N) M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : sSup s = N
⊢ ⨆ a ∈ s, a = N

Tactic:
rw [sSup_eq_iSup] at hs

Premises used: sSup_eq_iSup
-- 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₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
N : Submodule R M
f : LinearMap.{u_1, u_2, u_4, u_5} σ₁₂ (↥N) M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : ⨆ a ∈ s, a = N
rw : Eq.{u_4 + 1} (α := Submodule R ↥N) (⨆ a ∈ s, comap N.subtype a) ⊤
rw₁ : Eq.{u_4 + 1} (α := Submodule R ↥(⨆ a ∈ s, a)) (⨆ a ∈ s, comap (Submodule.subtype (⨆ a ∈ s, a)) a) ⊤
rw₂ rw₃ : Eq.{u_4 + 1} (α := Submodule R ↥(⨆ a ∈ s, a)) ⊤ ⊤
⊢ sSup (comap N.subtype '' s) = ⊤

Tactic:
rw [sSup_image, ← hs, biSup_comap_subtype_eq_top]

Premises used: Submodule.biSup_comap_subtype_eq_top, sSup_image
-- 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
p : Submodule R M
s : Set ↥p
⊢ span R (Subtype.val (p := fun (x : M) ↦ x ∈ p) '' s) = p ↔ Eq (α := Submodule R ↥p) (span R s) ⊤

Tactic:
simp [← (Submodule.map_injective_of_injective p.injective_subtype).eq_iff, Submodule.map_span]

Premises used: Function.Injective.eq_iff, Submodule.injective_subtype, Submodule.map_span, Submodule.map_injective_of_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
ι : Type u_9
p : Submodule R M
s : ι → M
hs : ∀ (i : ι), s i ∈ p
⊢ Eq.{u_4 + 1} (α := Submodule R ↥p) (span R (range fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ p) (s i) ⋯)) ⊤ ↔
    span R (range s) = p

Tactic:
simp [← span_val_image_eq_iff, ← Set.range_comp, Function.comp_def]

Premises used: Set.range_comp, Submodule.span_val_image_eq_iff, Function.comp_def
-- 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₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst_6 : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hp : p ≤ f.range
rw : map f (comap f p) ≤ q ↔ p ≤ q
rw₁ rw₂ : p ≤ q ↔ p ≤ q
⊢ comap f p ≤ comap f q ↔ p ≤ q

Tactic:
rw [← Submodule.map_le_iff_le_comap, Submodule.map_comap_eq_of_le hp]

Premises used: Submodule.map_comap_eq_of_le, Submodule.map_le_iff_le_comap
-- 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₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst_6 : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
hp : p ≤ f.range
hq : q ≤ f.range
a : map f (comap f (p ⊔ q)) = map f (comap f p ⊔ comap f q)
⊢ comap f (p ⊔ q) = comap f p ⊔ comap f q

Tactic:
apply map_injective_of_injective hf

Premises used: Submodule.map_injective_of_injective
-- 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₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst_6 : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
hp : p ≤ f.range
hq : q ≤ f.range
a : p ⊔ q ≤ f.range
⊢ map f (comap f (p ⊔ q)) = map f (comap f p ⊔ comap f q)

Tactic:
rw [map_sup, map_comap_eq_self, map_comap_eq_self hp, map_comap_eq_self hq]

Premises used: Submodule.map_comap_eq_self, Submodule.map_sup
-- 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₂
σ₁₂ : R →+* R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst_6 : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
hp : p ≤ f.range
hq : q ≤ f.range
⊢ p ⊔ q ≤ f.range

Tactic:
simp [sup_le_iff, hp, hq]

Premises used: sup_le_iff
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
h : ∀ (x : M), x ∈ (s ⊔ t) ⊓ p ↔ x ∈ s ⊔ t ⊓ p
⊢ (s ⊔ t) ⊓ p = s ⊔ t ⊓ p

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
h : (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p ↔ ∃ y ∈ s, ∃ (z : M), (z ∈ t ∧ z ∈ p) ∧ y + z = x
⊢ x ∈ (s ⊔ t) ⊓ p ↔ x ∈ s ⊔ t ⊓ p

Tactic:
simp only [mem_sup, mem_inf]

Premises used: Submodule.mem_inf, Submodule.mem_sup
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
h : (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p → ∃ y ∈ s, ∃ (z : M), (z ∈ t ∧ z ∈ p) ∧ y + z = x
h₁ : (∃ y ∈ s, ∃ (z : M), (z ∈ t ∧ z ∈ p) ∧ y + z = x) → (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p
⊢ (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p ↔ ∃ y ∈ s, ∃ (z : M), (z ∈ t ∧ z ∈ p) ∧ y + z = x

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx : y + z = x
⊢ ∃ y ∈ s, ∃ (z : M), (z ∈ t ∧ z ∈ p) ∧ y + z = x

Tactic:
⟨y, hy, z, ⟨hz, ?_⟩, hyzx⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx : y + z = x
h : z ∈ p
⊢ ∃ y ∈ s, ∃ (z : M), (z ∈ t ∧ z ∈ p) ∧ y + z = x

Tactic:
refine ⟨y, hy, z, ⟨hz, ?_⟩, hyzx⟩
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx : y + z = x
⊢ z = -y + x

Tactic:
rw [← add_right_inj, neg_add_cancel_left] at hyzx

Premises used: add_right_inj, neg_add_cancel_left
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
hx : x ∈ p
y : M
hy : y ∈ s
z : M
hz : z ∈ t
hyzx_1 : y + z = x
hyzx : z = -y + x
⊢ z ∈ p

Tactic:
simpa [hyzx] using p.add_mem (neg_le.mp hnsp hy) hx

Premises used: Iff.mp, Submodule.add_mem, Submodule.neg_le
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x y : M
hy : y ∈ s
z : M
hyzx : y + z = x
hz : z ∈ t
hz' : z ∈ p
⊢ (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p

Tactic:
⟨⟨y, hy, z, hz, hyzx⟩, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x y : M
hy : y ∈ s
z : M
hyzx : y + z = x
hz : z ∈ t
hz' : z ∈ p
h : x ∈ p
⊢ (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p

Tactic:
refine ⟨⟨y, hy, z, hz, hyzx⟩, ?_⟩
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x y : M
hy : y ∈ s
z : M
hyzx : y + z = x
hz : z ∈ t
hz' : z ∈ p
⊢ x ∈ p

Tactic:
simpa [← hyzx] using p.add_mem (hsp hy) hz'

Premises used: Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t p : Submodule R M
hps : p ≤ s
hnps : -p ≤ s
rw : p ⊔ s ⊓ t = s ⊓ (t ⊔ p)
rw₁ : p ⊔ t ⊓ s = s ⊓ (t ⊔ p)
rw₂ : (p ⊔ t) ⊓ s = s ⊓ (t ⊔ p)
rw₃ : s ⊓ (p ⊔ t) = s ⊓ (t ⊔ p)
rw₄ rw₅ : s ⊓ (t ⊔ p) = s ⊓ (t ⊔ p)
⊢ s ⊓ t ⊔ p = s ⊓ (t ⊔ p)

Tactic:
rw [sup_comm, inf_comm, ← sup_inf_assoc_of_le_of_neg_le t hps hnps, inf_comm, sup_comm]

Premises used: Submodule.sup_inf_assoc_of_le_of_neg_le, inf_comm, sup_comm
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
a : LE.le (α := Submodule R M) (span R (-s)) (-span R s)
a₁ : LE.le (α := Submodule R M) (-span R s) (span R (-s))
⊢ Eq (α := Submodule R M) (span R (-s)) (-span R s)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
a : s ⊆ (↑(span R s) : Set M)
⊢ LE.le (α := Submodule R M) (span R (-s)) (-span R s)

Tactic:
rw [span_le, coe_set_neg, ← Set.neg_subset, neg_neg]

Premises used: neg_neg, Set.neg_subset, Submodule.span_le, Submodule.coe_set_neg
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
⊢ s ⊆ (↑(span R s) : Set M)

Tactic:
subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
⊢ s ⊆ (↑(span R s) : Set M)

Tactic:
exact subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
a : -s ⊆ (↑(span R (-s)) : Set M)
⊢ LE.le (α := Submodule R M) (-span R s) (span R (-s))

Tactic:
rw [neg_le, span_le, coe_set_neg, ← Set.neg_subset]

Premises used: Set.neg_subset, Submodule.span_le, Submodule.coe_set_neg, Submodule.neg_le
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
⊢ -s ⊆ (↑(span R (-s)) : Set M)

Tactic:
subset_span

Premises used: Set.Mem, setOf, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_8
M : Type u_9
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
⊢ -s ⊆ (↑(span R (-s)) : Set M)

Tactic:
exact subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
M : Type u_11
inst : AddCommGroup M
s : Set M
⊢ Eq (α := Submodule ℤ M)
    ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) (AddSubgroup.closure s) : Submodule ℤ M)
    (span ℤ s : Submodule ℤ M)

Tactic:
(Submodule.span_le.mpr AddSubgroup.subset_closure).antisymm'
    ((Submodule.span ℤ s).toAddSubgroup.closure_le.mpr Submodule.subset_span)

Premises used: Iff.mpr, LE.le.antisymm', Int, Submodule.toAddSubgroup, Submodule.span, Submodule.subset_span, Submodule.span_le, AddSubgroup.closure_le
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_10
M : Type u_11
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
⊢ Eq (α := Submodule R M) (span R (-s)) (span R s)

Tactic:
simp [span_neg_eq_neg]

Premises used: Submodule.span_neg_eq_neg
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R_1 : Type u_1
R₂ : Type u_2
K : Type u_3
M_1 : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
R_2 : Type u_8
M_2 : Type u_9
inst : Semiring R_2
inst_1 : AddCommGroup M_2
inst_2 : Module R_2 M_2
R : Type u_10
M : Type u_11
inst_3 : Ring R
inst_4 : AddCommGroup M
inst_5 : Module R M
x x_1 x_2 : Submodule R M
hxy : x ≤ x_2
x_3 : M
h : x_3 ∈ (x ⊔ x_1) ⊓ x_2
⊢ -x ≤ x_2

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R_1 : Type u_1
R₂ : Type u_2
K : Type u_3
M_1 : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
R_2 : Type u_8
M_2 : Type u_9
inst : Semiring R_2
inst_1 : AddCommGroup M_2
inst_2 : Module R_2 M_2
R : Type u_10
M : Type u_11
inst_3 : Ring R
inst_4 : AddCommGroup M
inst_5 : Module R M
x x_1 x_2 : Submodule R M
hxy : x ≤ x_2
x_3 : M
h : x_3 ∈ (x ⊔ x_1) ⊓ x_2
rwa rwa₁ rwa₂ rwa₃ : x_3 ∈ (x ⊔ x_1) ⊓ x_2
⊢ x_3 ∈ x ⊔ x_1 ⊓ x_2

Tactic:
rwa [← sup_inf_assoc_of_le_of_neg_le _ hxy (by simpa)]

Premises used: Submodule.sup_inf_assoc_of_le_of_neg_le
-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_10
M : Type u_11
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p q r : Submodule R M
h₁ : IsCompl q r
h₂ : q ≤ p
⊢ IsCompl (comap p.subtype q) (comap p.subtype r)

Tactic:
simpa [p.mapIic.isCompl_iff, Iic.isCompl_iff] using Iic.isCompl_inf_inf_of_isCompl_of_le h₁ h₂

Premises used: Submodule.mapIic, Set.Iic.isCompl_inf_inf_of_isCompl_of_le, Set.Iic.isCompl_iff, OrderIso.isCompl_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 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ comap f (map f p) = p ⊔ f.ker

Tactic:
le_antisymm ?_ (sup_le (le_comap_map _ _) (comap_mono bot_le))

Premises used: Submodule.comap_mono, Submodule.le_comap_map, le_antisymm, sup_le, bot_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 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
refine : comap f (map f p) ≤ p ⊔ f.ker
⊢ comap f (map f p) = p ⊔ f.ker

Tactic:
refine le_antisymm ?_ (sup_le (le_comap_map _ _) (comap_mono bot_le))

Premises used: Submodule.comap_mono, Submodule.le_comap_map, le_antisymm, sup_le, bot_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 : Semiring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
x y : M
hy : y ∈ (↑p : Set M)
e : Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) ((f : (a : M) → M₂) x : M₂)
⊢ x - y ∈ f.ker

Tactic:
simpa using sub_eq_zero.2 e.symm

Premises used: Iff.mpr, sub_eq_zero, Eq.symm