mathlib-initiative/mathlib-tactics huggingface dataset:
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
  simp_rw [IsAtom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]

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
⊢ ↑(p ⊔ p') = ↑p + ↑p'

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
⊢ SupClosed ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
a : α
⊢ SupClosed {a}

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
⊢ SupClosed univ

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F β α
inst✝ : SupHomClass F β α
hs : SupClosed s
f : F
a : β
ha : a ∈ ⇑f ⁻¹' s
b : β
hb : b ∈ ⇑f ⁻¹' s
⊢ a ⊔ b ∈ ⇑f ⁻¹' s

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
hs : SupClosed s
f : F
⊢ SupClosed (⇑f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
⊢ SupClosed (range ⇑f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
hs : SupClosed s
ha : a ∈ upperBounds s
⊢ SupClosed (insert a s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
⊢ SupClosed (insert a s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ max a b ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t : Set α
a✝ b : α
s : Set α
a : α
ha : a ∈ s
⊢ ↑{a} ⊆ s ∧ {a}.sup' ⋯ id = a

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✝ : OrderTop A
K : A
⊢ IsCoatom K ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤

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
⊢ (p ⊔ p').toAddSubmonoid = p.toAddSubmonoid ⊔ p'.toAddSubmonoid

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s t : Set α
a b : α
⊢ ∀ (x : Set α), SupClosed {a | ∃ t, ∃ (ht : t.Nonempty), ↑t ⊆ x ∧ t.sup' ht id = a}

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s t : Set α
a b : α
⊢ ∀ ⦃x y : Set α⦄, x ⊆ y → SupClosed y → {a | ∃ t, ∃ (ht : t.Nonempty), ↑t ⊆ x ∧ t.sup' ht id = a} ⊆ y

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
⊢ supClosure ∅ = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
a : α
⊢ supClosure {a} = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
⊢ supClosure Set.univ = Set.univ

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
K L : A
⊢ K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
⊢ upperBounds s ⊆ upperBounds (supClosure 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
p p' : Submodule R M
⊢ p ⊔ p' = ⊤ ↔ ∀ (m : M), ∃ u ∈ p, ∃ v ∈ p', m = u + v

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
⊢ IsLUB (supClosure s) a ↔ IsLUB s 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
P : M → Prop
⊢ (∀ x ∈ p ⊔ p', P x) ↔ ∀ x₁ ∈ p, ∀ x₂ ∈ p', P (x₁ + x₂)

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
P : M → Prop
⊢ (∃ x ∈ p ⊔ p', P x) ↔ ∃ x₁ ∈ p, ∃ x₂ ∈ p', P (x₁ + x₂)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
hs : s.Finite
⊢ (supClosure s).Finite

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
K L : A
⊢ K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : Coframe α
s : Set α
a : α
ha : IsCoatom a
⊢ sInf s ≤ a ↔ ∃ b ∈ s, b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
a : α
b : ↑(Ici a)
⊢ IsAtom b ↔ a ⋖ ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
b : α
a : ↑(Iic b)
⊢ IsCoatom a ↔ ↑a ⋖ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ a ⋖ b ↔ IsAtom ⟨b, h⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ a ⋖ b ↔ IsCoatom ⟨a, h⟩

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
h : x ≠ 0
⊢ ∃ x_1 y, x_1 ≠ 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 y : M
h : x ∈ R ∙ y
⊢ 1 • y = y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b : α
ha : IsAtom a
⊢ ¬Disjoint a 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
x y : M
h : x ∈ R ∙ y
⊢ 0 • y = 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b : α
ha : IsAtom a
hb : IsAtom b
hab : a ≠ b
⊢ Disjoint 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
x y : M
h : x ∈ R ∙ y
a b : R
⊢ (a + b) • y = a • y + b • y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderTop α
a b : α
ha : IsCoatom a
⊢ ¬Codisjoint a b ↔ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderTop α
a b : α
ha : IsCoatom a
hb : IsCoatom b
hab : a ≠ b
⊢ Codisjoint a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
h : IsCoatomic αᵒᵈ
b : α
⊢ b = ⊥ ∨ ∃ a, IsAtom 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
x y : M
h : x ∈ R ∙ y
a b : R
⊢ (a * b) • y = a • b • y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
h : IsAtomic α
b : αᵒᵈ
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
⊢ supClosure s ×ˢ supClosure t ⊆ supClosure (s ×ˢ t)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : IsAtomic αᵒᵈ
b : α
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : IsCoatomic α
b : αᵒᵈ
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : Preorder α
⊢ IsStronglyAtomic αᵒᵈ ↔ IsStronglyCoatomic α

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 y : M
h : x ∈ R ∙ y
⊢ ∃ a, a • y = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : Preorder α
⊢ IsStronglyCoatomic αᵒᵈ ↔ IsStronglyAtomic α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
⊢ IsStronglyCoatomic αᵒᵈ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : IsStronglyCoatomic α
⊢ IsStronglyAtomic αᵒᵈ

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
y : M
a : R
⊢ 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 y : M
⊢ (∃ a, a • y = x) → x ∈ R ∙ y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝¹ : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α✝¹
α✝ : Type u_4
a✝ b : α✝
inst✝³ : Preorder α✝
α : Type u_5
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsStronglyAtomic α
a : α
⊢ a = ⊥ ∨ ∃ a_1, IsAtom a_1 ∧ a_1 ≤ 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 : Submodule R M
v₀ : M
⊢ s ≤ R ∙ v₀ ↔ ∀ v ∈ s, ∃ r, r • v₀ = v

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : ⟨c, hc⟩ < ⟨d, hd⟩
x : α
hcx : c ⋖ x
hxd : x ≤ d
⊢ ⟨c, hc⟩ < ⟨x, ⋯⟩

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 : Submodule R M
f : R →ₗ[R] ↥s
hf : Surjective ⇑f
⊢ {↑(f 1)} ⊆ ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : ⟨c, hc⟩ < ⟨d, hd⟩
x : α
hcx : c ⋖ x
hxd : x ≤ d
y : ↑s
hy : ⟨c, hc⟩ < y
hy' : y < ⟨x, ⋯⟩
⊢ c < ?m.88 y hy hy'

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : ⟨c, hc⟩ < ⟨d, hd⟩
x : α
hcx : c ⋖ x
hxd : x ≤ d
y : ↑s
hy : ⟨c, hc⟩ < y
hy' : y < ⟨x, ⋯⟩
⊢ ↑y < x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
⊢ ∀ (a b : ↑s), a < b → ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝³ : PartialOrder α✝
α : Type u_4
a b : α
inst✝² : Preorder α
inst✝¹ : IsStronglyAtomic α
s : Set α
inst✝ : s.OrdConnected
⊢ s.OrdConnected

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : IsStronglyCoatomic α
s : Set α
h : s.OrdConnected
⊢ s.OrdConnected

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : PredOrder α
⊢ IsStronglyCoatomic α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
h : WellFounded fun x1 x2 ↦ x1 < x2
a b : α
hab : a < b
⊢ ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
refine ⟨WellFounded.min h (Set.Ioc a b) ⟨b, hab,rfl.le⟩, ?_⟩
    have hmem := (WellFounded.min_mem h (Set.Ioc a b) ⟨b, hab,rfl.le⟩)
    exact ⟨⟨hmem.1,fun c hac hlt ↦ WellFounded.not_lt_min h
      (Set.Ioc a b) ⟨hac, hlt.le.trans hmem.2⟩ hlt⟩, hmem.2⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
h : WellFounded fun x1 x2 ↦ x1 < x2
a b : α
hab : a < b
⊢ ∃ x, a ⋖ x ∧ x ≤ 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 : Submodule R M
f : R →ₗ[R] ↥s
hf : Surjective ⇑f
x : M
hx : x ∈ s
r : R
eq : f r = ⟨x, hx⟩
⊢ r • ↑(f 1) = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
hbot : ¬x ⊓ yᶜ = ⊥
a : α
ha : IsAtom a
hle : a ≤ x ⊓ yᶜ
hx : a ≤ x
hy' : a ≤ yᶜ
hy : a ≤ y
this : a ≤ y ⊓ yᶜ
⊢ 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 : Submodule R M
f : R →ₗ[R] ↥s
hf : Surjective ⇑f
⊢ s = R ∙ ↑(f 1)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
this : x ⊓ yᶜ = ⊥
⊢ y = yᶜᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
⊢ x ≤ y ↔ ∀ (a : α), IsAtom a → a ≤ x → a ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : x = y
⊢ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ x)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
⊢ x = y ↔ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : Lattice α
s : Set α
p : (a : α) → a ∈ latticeClosure s → Prop
mem : ∀ (a : α) (has : a ∈ s), p a ⋯
sup : ∀ (a : α) (has : a ∈ latticeClosure s) (b : α) (hbs : b ∈ latticeClosure s), p a has → p b hbs → p (a ⊔ b) ⋯
inf : ∀ (a : α) (has : a ∈ latticeClosure s) (b : α) (hbs : b ∈ latticeClosure s), p a has → p b hbs → p (a ⊓ b) ⋯
a : α
has : a ∈ latticeClosure s
⊢ p a has

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
⊢ R ∙ x = ⊤ ↔ ∀ (v : M), ∃ r, r • x = v

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type ?u.8
inst✝¹ : CompleteBooleanAlgebra α
inst✝ : IsAtomic α
ι✝ : Type ?u.8
κ✝ : ι✝ → Type ?u.8
f : (a : ι✝) → κ✝ a → α
a : α
ha : IsAtom a
⊢ a ≤ ⨅ a, ⨆ b, f a b ↔ a ≤ ⨆ g, ⨅ a, f a (g 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
⊢ R ∙ 0 = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : Lattice α
⊢ latticeClosure ∅ = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
h : IsCoatomistic αᵒᵈ
b : α
⊢ ∃ s, IsLUB s b ∧ ∀ a ∈ s, IsAtom a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
h : IsAtomistic α
b : αᵒᵈ
⊢ ∃ s, IsGLB s b ∧ ∀ a ∈ s, IsCoatom a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : IsAtomistic αᵒᵈ
b : α
⊢ ∃ s, IsGLB s b ∧ ∀ a ∈ s, IsCoatom a

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : Lattice α
a : α
⊢ latticeClosure {a} = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : IsCoatomistic α
b : αᵒᵈ
⊢ ∃ s, IsLUB s b ∧ ∀ a ∈ s, IsAtom a

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : Lattice α
⊢ latticeClosure Set.univ = Set.univ

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 : Type u_9
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
r : S
x : M
⊢ R ∙ r • x ≤ R ∙ x

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
G : Type u_9
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
g : G
x : M
⊢ R ∙ g • x = R ∙ x

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
r : R
hr : IsUnit r
x : M
⊢ R ∙ r • x = R ∙ x

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 y z : M
hxy : x ∈ R ∙ y
hyz : y ∈ R ∙ z
⊢ x ∈ R ∙ z

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
b : α
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
b : α
⊢ IsLUB {a | IsAtom a ∧ a ≤ b} b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : IsAtomistic α
inst✝ : OrderTop α
⊢ IsLUB {a | IsAtom 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
s : Set M
⊢ span R (insert x s) = R ∙ x ⊔ span R s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
h : a = b
⊢ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ 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
x : M
s : Set M
y : M
⊢ x ∈ span R (insert y s) ↔ ∃ a, ∃ z ∈ span R s, x = a • 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 y z : M
⊢ z ∈ span R {x, y} ↔ ∃ a b, a • x + b • y = z

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
⊢ a = b ↔ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : IsCoatomistic α
b : α
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : CompleteLattice α
⊢ IsAtomistic α ↔ ∀ (b : α), ∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : CompleteLattice α
⊢ IsCoatomistic α ↔ ∀ (b : α), ∃ s, b = sInf s ∧ ∀ a ∈ s, 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
x y z : M
a b c : R
⊢ a • x + b • y + c • z = a • x + (b • y + c • z)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ (⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ) = 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
w x y z : M
⊢ w ∈ span R {x, y, z} ↔ ∃ a b c, a • x + b • y + c • z = w

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
⊢ R ∙ x = ⊥ ↔ x = 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
⊢ span R 0 = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
h : ¬(⨅ a, b ⊓ bif g a then a else aᶜ) = ⊥
⊢ (⨅ a, b ⊓ bif g a then a else aᶜ) ≤ ⨅ a, b ⊓ bif g a then a else 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
m : M
p : Submodule R M
⊢ R ∙ m ≤ p ↔ m ∈ p

Tactic:
by

Goal state after: