mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : SetLike S M
inst✝¹ : AddSubmonoidClass S M
inst✝ : SMulMemClass S R M
s : S
⊢ ↑(span R ↑s) = ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SemilatticeSup α
s : Finset β
t : Finset γ
h : (s ×ˢ t).Nonempty
f : β × γ → α
⊢ (s ×ˢ t).sup' h f = t.sup' ⋯ fun i' ↦ s.sup' ⋯ fun i ↦ f (i, i')

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ Icc a (b ⊔ a) = Icc a (a ⊔ b)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ 0 ∈ ↑(span R s)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R (insert 0 s) = span R s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ ((∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2) → ∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
c : ↑(Ioo (a ⊓ b) a)
⊢ ↑((fun c ↦ ⟨a ⊓ ↑c, ⋯⟩) ((fun c ↦ ⟨↑c ⊔ b, ⋯⟩) c)) = ↑c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
⊢ (s.sup' hs f, t.sup' ht g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
c : ↑(Ioo b (a ⊔ b))
⊢ ↑((fun c ↦ ⟨↑c ⊔ b, ⋯⟩) ((fun c ↦ ⟨a ⊓ ↑c, ⋯⟩) c)) = ↑c

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R (s \ {0}) = span R s

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ Ioo (a ⊓ b) b = Ioo (b ⊓ a) b

Tactic:
rw [inf_comm]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: α : Type u_2
ι : Type u_5
κ : Type u_6
inst✝ : DistribLattice α
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → α
⊢ s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' ⋯ fun i ↦ f i.1 ⊓ g i.2

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ Ioo (a ⊓ b) b = Ioo (b ⊓ a) b

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
mem : ∀ (x : M) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul : ∀ (a : R) (x : M) (hx : x ∈ span R s), p x hx → p (a • x) ⋯
x : M
hx : x ∈ span R s
⊢ p x hx

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ Ioo a (b ⊔ a) = Ioo a (a ⊔ b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Preorder α
⊢ Function.Injective fun c ↦ ⇑c.toOrderHom

Tactic:
by

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
c : ClosureOperator α
x : α
⊢ x ∈ range ⇑c → x ∈ {x | c.IsClosed x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
c : ClosureOperator α
⊢ {x | c.IsClosed x} = range ⇑c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
c : ClosureOperator α
x y : α
hy : c.IsClosed y
⊢ c x ≤ y ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
c₁ c₂ : ClosureOperator α
h : ∀ (x : α), c₁.IsClosed x ↔ c₂.IsClosed x
x : α
⊢ IsGLB {y | x ≤ y ∧ c₁.IsClosed y} (c₂ x)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
⊢ c = ofPred (⇑c) c.IsClosed ⋯ ⋯ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ a ⋖ a ⊔ b → a ⊓ b ⋖ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ c (x ⊔ y) ≤ c (c x ⊔ y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ c (x ⊔ c y) = c (x ⊔ y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ a ⊓ b ⋖ a → b ⋖ a ⊔ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₀ : Codisjoint a b
h₁ : Disjoint b c
h₂ : a ≤ c
⊢ c ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ c (c x ⊔ c y) = c (x ⊔ y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : CompleteLattice α
c : ClosureOperator α
p : α → Prop
hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)
a : α
⊢ a ≤ ⨅ b, ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
u : β → α
l₁ : α → β
gc'✝¹ : GaloisConnection l₁ u
l₂ : α → β
gc'✝ : GaloisConnection l₂ u
h : { toFun := l₁, gc' := gc'✝¹ }.toFun = { toFun := l₂, gc' := gc'✝ }.toFun
⊢ { toFun := l₁, gc' := gc'✝¹ } = { toFun := l₂, gc' := gc'✝ }

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
h : ∀ (x y z : α), x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z
x✝ y z : α
xz : x✝ ≤ z
⊢ (x✝ ⊔ y) ⊓ z ≤ x✝ ⊔ y ⊓ z

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
x✝ y z : α
xz : x✝ ≤ z
⊢ (x✝ ⊔ y) ⊓ z ≤ x✝ ⊔ y ⊓ z

Tactic:
by

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
β : Type u_4
inst✝¹ : SetLike α β
inst✝ : Preorder α
l : LowerAdjoint SetLike.coe
s : Set β
x : β
⊢ x ∈ l.toFun s ↔ ∀ (S : α), s ⊆ ↑S → x ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
β : Type u_4
inst✝¹ : SetLike α β
inst✝ : Preorder α
l : LowerAdjoint SetLike.coe
x y : α
⊢ l.toFun (↑(l.toFun ↑x) ∪ ↑y) = l.toFun (↑x ∪ ↑y)

Tactic:
closure_union_closure_left

Goal state after:
α : Type u_1
β : Type u_4
inst✝¹ : SetLike α β
inst✝ : Preorder α
l : LowerAdjoint SetLike.coe
x y : α
⊢ l.toFun (↑x ∪ ↑y) = l.toFun (↑x ∪ ↑y)
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
β : Type u_4
inst✝¹ : SetLike α β
inst✝ : Preorder α
l : LowerAdjoint SetLike.coe
x y : α
⊢ l.toFun (↑(l.toFun ↑x) ∪ ↑(l.toFun ↑y)) = l.toFun (↑x ∪ ↑y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
⊢ ⋯.closureOperator = c

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ Disjoint a (b ⊔ c)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
s : Set M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
t : Set N
p : (x : M) → (y : N) → x ∈ span R s → y ∈ span R t → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : y ∈ span R t), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : x ∈ span R s), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : x ∈ span R s) (hy : y ∈ span R s) (hz : z ∈ span R t),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : x ∈ span R s) (hy : y ∈ span R t) (hz : z ∈ span R t),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p (r • x) y ⋯ hy
smul_right : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p x (r • y) hx ⋯
a : M
b : N
ha : a ∈ span R s
hb : b ∈ span R t
⊢ p a b ha hb

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint (a ⊔ b) c

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).toAddSubmonoid = closure (univ • s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h₁ : Disjoint a (b ⊔ c)
h₂ : Disjoint b (c ⊔ a)
⊢ Disjoint c (a ⊔ b)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
v : M
⊢ v ∈ span R s ↔ v ∈ closure (univ • s)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
⊢ ∀ (x y : M) (hx : x ∈ closure (univ • s)) (hy : y ∈ closure (univ • s)), p x ⋯ → p y ⋯ → p (x + y) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ IsCompl ⟨a ⊓ b, ⋯⟩ ⟨a ⊓ c, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
⊢ p x hx

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ (span ℕ s).toAddSubmonoid = AddSubmonoid.closure s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
s : AddSubmonoid M
⊢ (span ℕ ↑s).toAddSubmonoid = s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: M : Type u_9
inst✝ : AddCommGroup M
s : AddSubgroup M
⊢ (span ℤ ↑s).toAddSubgroup = s

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
⊢ ∃ b', b ⊓ b' = a ∧ b ⊔ b' = c

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set M
hst : Disjoint (span R s) (span R t)
⊢ Disjoint (s \ {0}) t

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ ⊥ ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set M
hst : Disjoint (span R s) (span R t)
h0s : 0 ∉ s
⊢ Disjoint s t

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
⊢ span R (⋂ S ∈ s, ↑S) = sInf s

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ ∃ a', Disjoint a a' ∧ a ⊔ a' = b

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Set M)
⊢ span R (⋃₀ s) = sSup (span R '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ b ≤ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ ∃ b', b ⊓ b' = a ∧ Codisjoint b b'

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
⊢ span R (⋃ S ∈ s, ↑S) = sSup s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq M
α : Type u_9
s : Finset α
f : ↥s → Finset M
⊢ span R ↑(s.attach.biUnion f) = ⨆ x, span R ↑(f x)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : IsModularLattice α
a b c : α
inst✝² : BoundedOrder α
inst✝¹ : ComplementedLattice α
inst✝ : Fact (a ≤ b)
x✝ : ↑(Icc a b)
x : α
ha : a ≤ x
hb : x ≤ b
⊢ ∃ b_1, IsCompl ⟨x, ⋯⟩ b_1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
⊢ p ⊔ span R s = span R (↑p ∪ s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
⊢ ∃ b, IsCompl ⟨x, hx⟩ b

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
⊢ span R s ⊔ p = span R (s ∪ ↑p)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R s = ⨆ x ∈ s, R ∙ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Ici a)
x : α
hx : x ∈ Ici a
⊢ ∃ b, IsCompl ⟨x, hx⟩ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
a b : α
hab : Disjoint a b
⊢ ∃ a', a ≤ a' ∧ IsCompl a' b

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
v : ι → M
⊢ span R (range v) = ⨆ i, R ∙ v i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ span R (r • s) ≤ span R s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Sort u_9
inst✝ : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ iSup S ↔ ∃ i, x ∈ S i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
z : M
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p
⊢ 0 ∈ p'

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p
⊢ y + 0 = y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p'
⊢ 0 ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p'
⊢ 0 + y = y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ 0 ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ 0 ∈ p' ∧ 0 + 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
y₁ : M
hy₁ : y₁ ∈ p
z₁ : M
hz₁ : z₁ ∈ p'
y₂ : M
hy₂ : y₂ ∈ p
z₂ : M
hz₂ : z₂ ∈ p'
⊢ y₁ + y₂ + (z₁ + z₂) = y₁ + z₁ + (y₂ + z₂)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
a : R
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx✝ : y + z ∈ span R (↑p ∪ ↑p')
⊢ a • y + a • z = a • (y + z)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : OrderBot α
a b : α
⊢ b < a → b = ⊥ ↔ b ≠ ⊥ → b ≤ a → a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a x : α
h : IsAtom a
⊢ x ≤ a ↔ x = ⊥ ∨ x = a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
ha : IsAtom a
hba : b ≤ a
⊢ b = ⊥ → b ≠ a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ p ⊔ p'
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a : α
⊢ Iio a = {⊥} ↔ IsAtom a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a : α
⊢ ⊥ ⋖ a ↔ IsAtom a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬a ≤ f i
i : ι
x : α
hxa : x ≤ a
hxf : x ≤ f i
hx : ¬x = ⊥
⊢ ¬x = a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) → x ∈ p ⊔ p'

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y z, ↑y + ↑z = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : Frame α
f : ι → α
a : α
ha : IsAtom a
⊢ a ≤ iSup f ↔ ∃ i, a ≤ f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : Frame α
s : Set α
a : α
ha : IsAtom a
⊢ a ≤ sSup s ↔ ∃ b ∈ s, a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
a b : α
ha : IsCoatom a
hab : a ≤ b
⊢ b = ⊤ → b ≠ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
a : α
⊢ Ioi a = {⊤} ↔ IsCoatom a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
z : M
⊢ (∃ y ∈ p, ∃ z_1 ∈ p', y + z_1 = z) ↔ ∃ x y, x ∈ p ∧ y ∈ p' ∧ x + y = z

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
⊢ Codisjoint p p' ↔ ∀ (z : M), ∃ x y, x ∈ p ∧ y ∈ p' ∧ x + y = z

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderBot A
K : A
⊢ IsAtom K ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥

Tactic:
by

Goal state after: