mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
⊢ IsStronglyAtomic αᵒᵈ

Tactic:
]

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : PredOrder α
⊢ IsStronglyAtomic αᵒᵈ
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⟩
⊢ ↑⟨x, hx⟩ = x

Tactic:
]

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

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (∀ v ∈ ⊤, ∃ r, r • x = v) ↔ ∀ (v : M), ∃ r, r • x = v
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 • x ∈ R ∙ x

Tactic:
]

Goal state after:
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 • x ∈ R ∙ x
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 : Rˣ
⊢ R ∙ r • x = R ∙ x

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : Rˣ
⊢ R ∙ r • x = R ∙ x
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:
]

Goal state after:
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)
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
⊢ R ∙ x ⊔ span R s = R ∙ x ⊔ span R s

Tactic:
]

Goal state after:
Module: Mathlib.Order.Atoms

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

Tactic:
]

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

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w x y z : M
⊢ (∃ a, ∃ z_1 ∈ span R {y, z}, w = a • x + z_1) ↔ ∃ a b c, a • x + b • y + c • z = w
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:
]

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 α
this : (⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ) = b
⊢ (⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ) ≤ sSup {a | IsAtom a ∧ a ≤ ⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ}

Tactic:
]

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
this : (⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ) = b
⊢ (⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ) ≤ sSup {a | IsAtom a ∧ a ≤ ⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ}
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
⊢ 0 = 0

Tactic:
]

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
⊢ m ∈ p ↔ m ∈ p

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
m : M
hm : m ∈ p
h : m = 0
⊢ 0 ∈ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}

Tactic:
]

Goal state after:
case pos
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
m : M
hm : m ∈ p
h : m = 0
⊢ 0 ∈ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
⊢ ∀ b ∈ {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}, b ≤ p

Tactic:
]

Goal state after:
case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
⊢ ∀ b ∈ {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}, b ≤ p
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
w✝ : M
left✝¹ : w✝ ∈ p
left✝ : w✝ ≠ 0
⊢ w✝ ∈ p

Tactic:
]

Goal state after:
case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
w✝ : M
left✝¹ : w✝ ∈ p
left✝ : w✝ ≠ 0
⊢ w✝ ∈ p
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
p : ι → Submodule R M
m : M
⊢ (∀ (b : Submodule R M), (∀ (i : ι), p i ≤ b) → R ∙ m ≤ b) ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
m : M
⊢ (∀ (b : Submodule R M), (∀ (i : ι), p i ≤ b) → R ∙ m ≤ b) ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type ?u.8
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set { a // IsAtom a }
h : ∀ a ∈ Subtype.val '' S, IsAtom a
⊢ Subtype.val '' (fun A ↦ {a | ↑a ≤ A}) ((fun S ↦ sSup (Subtype.val '' S)) S) =
    {a | a ≤ sSup (Subtype.val '' S) ∧ IsAtom a}

Tactic:
]

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type ?u.8
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set { a // IsAtom a }
h : ∀ a ∈ Subtype.val '' S, IsAtom a
⊢ Subtype.val '' (fun A ↦ {a | ↑a ≤ A}) ((fun S ↦ sSup (Subtype.val '' S)) S) =
    {a | a ≤ sSup (Subtype.val '' S) ∧ IsAtom a}
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ x ∈ S

Tactic:
]

Goal state after:
case refine_1.refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ x ∈ S
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ x ∈ R ∙ x

Tactic:
]

Goal state after:
case refine_1.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ x ∈ R ∙ x
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_3.refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ↑X ∪ ↑Y ⊆ S

Tactic:
]

Goal state after:
case refine_3.refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ↑X ∪ ↑Y ⊆ S
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_3.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ∃ y_1 ∈ span R ↑X, ∃ z ∈ span R ↑Y, y_1 + z = x + y

Tactic:
]

Goal state after:
case refine_3.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ∃ y_1 ∈ span R ↑X, ∃ z ∈ span R ↑Y, y_1 + z = x + y
Module: Mathlib.LinearAlgebra.Span.Defs

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

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubgroup, ∃ z ∈ p'.toAddSubgroup, y + z = x
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, ∃ z ∈ span R s, x = a • y + z) ↔ ∃ a, x + a • y ∈ span R s

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, ∃ z ∈ span R s, x = a • y + z) ↔ ∃ a, x + a • y ∈ span R s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ ((t ×ˢ u).inf' ⋯ fun i ↦ id i.1 ⊔ id i.2) ∈ infClosure s

Tactic:
]

Goal state after:
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ ((t ×ˢ u).inf' ⋯ fun i ↦ id i.1 ⊔ id i.2) ∈ infClosure s
Module: Mathlib.Order.SupClosed

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

Tactic:
]

Goal state after:
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : s.Finite
⊢ (supClosure (infClosure s)).Finite
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case intro
ι : Sort u_1
α : Type u_3
inst✝² : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst✝¹ : Finite ι
inst✝ : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
val✝ : Fintype (PLift ι)
⊢ (univ.sup' ⋯ fun i ↦ f i.down) ∈ s

Tactic:
]

Goal state after:
case intro
ι : Sort u_1
α : Type u_3
inst✝² : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst✝¹ : Finite ι
inst✝ : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
val✝ : Fintype (PLift ι)
⊢ (univ.sup' ⋯ fun i ↦ f i.down) ∈ s
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_1.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ s
⊢ ⊤ ≤ ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this✝ : Finite ↑t
this : Nonempty ↑t
⊢ ⨆ a, ↑a ∈ s

Tactic:
]

Goal state after:
α : Type u_3
inst✝ : ConditionallyCompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hts : t ⊆ s
this✝ : Finite ↑t
this : Nonempty ↑t
⊢ ⨆ a, ↑a ∈ s
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2.inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊥ ∈ upperBounds s
⊢ ⊥ ≤ ⊥

pp: case refine_2.inl.hnc
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊥ ∈ upperBounds s
⊢ ⊤ ∉ s

Tactic:
]

Goal state after:
case refine_2.inl.hnc
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊥ ∈ upperBounds s
⊢ ⊤ ∉ s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ sSup (f '' t) ∈ s

Tactic:
]

Goal state after:
α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ sSup (f '' t) ∈ s
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j + r • v i ∈ span R (range v)

Tactic:
]

Goal state after:
case refine_1.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j + r • v i ∈ span R (range v)
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_1.inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊥ ∈ s
⊢ ⊥ ≤ ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
this : Finite ↑t
⊢ ⨆ a, ↑a ∈ s

Tactic:
]

Goal state after:
α : Type u_3
inst✝ : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
this : Finite ↑t
⊢ ⨆ a, ↑a ∈ s
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ lowerBounds s
⊢ ⊤ ≤ ⊤

pp: case refine_2.inr.hnc
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ lowerBounds s
⊢ ⊥ ∉ s

Tactic:
]

Goal state after:
case refine_2.inr.hnc
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ lowerBounds s
⊢ ⊥ ∉ s
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_2.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j + r • v i - r • v i ∈ span R (range (update v j (v j + r • v i)))

Tactic:
]

Goal state after:
case refine_2.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j + r • v i - r • v i ∈ span R (range (update v j (v j + r • v i)))
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
i : ι
f : ι → α
s : Finset ι
hs : s ⊆ {i}
j : ι
hji : j ∈ {i}
hj : j ∉ s
⊢ Disjoint (f j) ⊥

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
i : ι
f : ι → α
s : Finset ι
hs : s ⊆ {i}
j : ι
hji : j ∈ {i}
hj : j ∉ s
⊢ Disjoint (f j) ⊥
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hf : ∀ i ∈ t, f i ∈ s
⊢ sSup (f '' t) ∈ s

Tactic:
]

Goal state after:
α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hf : ∀ i ∈ t, f i ∈ s
⊢ sSup (f '' t) ∈ s
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
b : β
⊢ IsAtom b ↔ IsAtom b

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ Iic (e a) = Iic (e a)

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ Iio (e a) = Iio (e a)

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ Ioo (e a) (e b) = Ioo (e a) (e b)

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ Ioc (e a) (e b) = Ioc (e a) (e b)

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ Icc (e a) (e b) = Icc (e a) (e b)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ span R (range v) = span R (range v)

Tactic:
]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
i : ι'
his : i ∈ s
hi : g i ∈ image g s
hit : g i ∉ image g t
⊢ Disjoint (f (g i)) (t.sup (f ∘ g))

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
i : ι'
his : i ∈ s
hi : g i ∈ image g s
hit : g i ∉ image g t
⊢ Disjoint (f (g i)) (t.sup (f ∘ g))
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ IsAtom ⊤ ↔ IsAtom ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ Disjoint ((f ∘ ⇑g) i) ((map g t).sup f)

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ Disjoint ((f ∘ ⇑g) i) ((map g t).sup f)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ i ∉ t

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ i ∉ t
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ ⇑g)
⊢ (image (⇑g) s).SupIndep f

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ ⇑g)
⊢ (image (⇑g) s).SupIndep f
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ Disjoint (f i) (f j) → Disjoint (f j) (({j, i}.erase j).sup f)

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ Disjoint (f i) (f j) → Disjoint (f j) (({j, i}.erase j).sup f)
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
h_inf : x ≤ a
⊢ x ≤ a

Tactic:
]

Goal state after:
case inr
α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
h_inf : x ≤ a
⊢ x ≤ a
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderTop α
inst✝¹ : IsLowerModularLattice α
inst✝ : IsCoatomistic α
⊢ IsStronglyAtomic αᵒᵈ

Tactic:
]

Goal state after:
α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderTop α
inst✝¹ : IsLowerModularLattice α
inst✝ : IsCoatomistic α
⊢ IsStronglyAtomic αᵒᵈ
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb : IsCompl (⋯.IicOrderIsoIci ⟨a, ay⟩) ⟨b, xb⟩
⊢ IsAtom ⟨a, ay⟩

Tactic:
]

Goal state after:
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb : IsCompl (⋯.IicOrderIsoIci ⟨a, ay⟩) ⟨b, xb⟩
⊢ IsAtom ⟨a, ay⟩
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
ha'b : ⊥ ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨⊥, ha'b⟩
⊢ ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
obtain rfl : a = b := by simpa [codisjoint_bot, ← Subtype.coe_inj] using ha'.codisjoint
      exact False.elim <| hab.ne rfl

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
a' : α
ha'b : a' ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩
d : α
hd : IsAtom d ∧ d ≤ a'
⊢ a ⊓ d ≤ a ⊓ a'

Tactic:
]

Goal state after:
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
a' : α
ha'b : a' ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩
d : α
hd : IsAtom d ∧ d ≤ a'
⊢ a ⊓ d ≤ a ⊓ a'