mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ⨆ i, p i = span R (⋃ i, ↑(p 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
ι : Sort u_9
p : ι → Submodule R M
h : ι → Prop
⊢ ⨆ i, ⨆ (_ : h i), p i = span R (⋃ i, ⋃ (_ : h i), ↑(p i))

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 : α
⊢ ∃ s, b = sSup s ∧ ∀ a ∈ s, 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
p : Submodule R M
⊢ p = sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}

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
I : Submodule R M
a : M
⊢ I < I ⊔ R ∙ a ↔ a ∉ I

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
⊢ S = {a | a ≤ sSup S ∧ IsAtom a}

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✝ : CompleteAtomicBooleanAlgebra α
A : α
⊢ (fun S ↦ sSup (Subtype.val '' S)) ((fun A ↦ {a | ↑a ≤ A}) A) = A

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✝ : CompleteAtomicBooleanAlgebra α
S : Set { a // IsAtom a }
⊢ ∀ a ∈ Subtype.val '' S, 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
ι : Sort u_9
p : ι → Submodule R M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N

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)
m : M
⊢ m ∈ sSup s ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N

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✝ : CompleteAtomicBooleanAlgebra α
S : Set { a // IsAtom a }
⊢ (fun A ↦ {a | ↑a ≤ A}) ((fun S ↦ sSup (Subtype.val '' S)) S) = S

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✝ : CompleteAtomicBooleanAlgebra α
a b : α
⊢ { toFun := fun A ↦ {a | ↑a ≤ A}, invFun := fun S ↦ sSup (Subtype.val '' S), left_inv := ⋯, right_inv := ⋯ } a ⊆
      { toFun := fun A ↦ {a | ↑a ≤ A}, invFun := fun S ↦ sSup (Subtype.val '' S), left_inv := ⋯, right_inv := ⋯ } b ↔
    a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i : IsSimpleOrder αᵒᵈ
⊢ IsSimpleOrder α

Tactic:
exact
      { exists_pair_ne := @exists_pair_ne αᵒᵈ _
        eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.toDual a)) }

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
⊢ IsSimpleOrder α ↔ IsSimpleOrder αᵒᵈ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊥ ≠ ⊤

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✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type u_4
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ IsSimpleOrder α

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✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a : α
⊢ a ≤ a

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✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a b c : α
⊢ a ≤ b → b ≤ c → a ≤ c

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✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
a b : α
⊢ a ≤ b ∨ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x y z : α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ IsAtomic αᵒᵈ

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
x : M
hx : x ∈ span R S
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ span R ↑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 M
ht : ↑∅ ⊆ ↑(span R s)
⊢ ↑∅ ⊆ s ∧ ↑∅ ⊆ ↑(span R ↑∅)

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
a : M
t : Finset M
hat : a ∉ t
IH : ↑t ⊆ ↑(span R s) → ∃ T, ↑T ⊆ s ∧ ↑t ⊆ ↑(span R ↑T)
ht : ↑(insert a t) ⊆ ↑(span R s)
⊢ ↑t ⊆ ↑(span R s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x : α
⊢ (fun x ↦ Bool.casesOn x ⊥ ⊤) ((fun x ↦ decide (x = ⊤)) 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
s : Set M
a : M
t : Finset M
hat : a ∉ t
IH : ↑t ⊆ ↑(span R s) → ∃ T, ↑T ⊆ s ∧ ↑t ⊆ ↑(span R ↑T)
ht : ↑(insert a t) ⊆ ↑(span R s)
T : Finset M
hTs : ↑T ⊆ s
htT : ↑t ⊆ ↑(span R ↑T)
T' : Finset M
hT's : ↑T' ⊆ s
haT' : a ∈ span R ↑T'
⊢ ↑(T ∪ T') ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x : Bool
⊢ (fun x ↦ decide (x = ⊤)) ((fun x ↦ Bool.casesOn x ⊥ ⊤) 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
s : Set M
t : Finset M
ht : ↑t ⊆ ↑(span R s)
⊢ ∃ T, ↑T ⊆ s ∧ ↑t ⊆ ↑(span R ↑T)

Tactic:
by

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
p p' : Submodule R M
⊢ (p ⊔ p').toAddSubgroup = p.toAddSubgroup ⊔ p'.toAddSubgroup

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a b : α
⊢ equivBool a ≤ equivBool b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ f '' latticeClosure s = latticeClosure (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : Lattice α
s : Set α
⊢ ⇑ofDual ⁻¹' latticeClosure s = latticeClosure (⇑ofDual ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊓ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊔ f b
⊢ f '' latticeClosure s = latticeClosure (f '' s)

Tactic:
by

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
y : M
s : Set M
a : R
z : M
hz : z ∈ span R s
⊢ a • y + z + -a • y ∈ span R s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x : α
⊢ (x ⊓ if x = ⊥ then ⊤ else ⊥) ≤ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

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

Tactic:
by

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
x y : M
s : Set M
a : R
h : x + a • y ∈ span R s
⊢ x = -a • y + (x + a • y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x : α
⊢ ⊤ ≤ x ⊔ if x = ⊥ then ⊤ else ⊥

Tactic:
by

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
x y : M
s : Set M
⊢ x ∈ span R (insert y s) ↔ ∃ a, x + a • y ∈ span R s

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
s : Set α
t : Set β
⊢ latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x y : α
⊢ (if x = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = x ⊓ if y = ⊥ then ⊤ else ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_3
inst✝² : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst✝¹ : Finite ι
inst✝ : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ i, f i ∈ s

Tactic:
by

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
⊢ ∀ (i : ↑t), ↑i ∈ s

Tactic:
by

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
⊢ sSup t ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
⊢ IsLUB s (if ⊤ ∈ s then ⊤ else ⊥)

Tactic:
by

Goal state after:
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
⊢ (f '' t).Nonempty

Tactic:
by

Goal state after:
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
⊢ f '' t ⊆ s

Tactic:
by

Goal state after:
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
⊢ ⨆ i ∈ t, f i ∈ s

Tactic:
by

Goal state after:
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
⊢ update v j (v j + r • v i) j ∈ span R (range v)

Tactic:
rw [update_self]

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.SupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_3
inst✝¹ : CompleteLattice α
f : ι → α
s : Set α
inst✝ : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ i, f i ∈ s

Tactic:
by

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
⊢ ∀ (i : ↑t), ↑i ∈ s

Tactic:
by

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
⊢ sSup t ∈ s

Tactic:
by

Goal state after:
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
⊢ f '' t ⊆ s

Tactic:
by

Goal state after:
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) (s.sup f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
⊢ IsGLB s (if ⊥ ∈ s then ⊥ else ⊤)

Tactic:
by

Goal state after:
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
⊢ ⨆ i ∈ t, f i ∈ s

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✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
h : b = ⊥
⊢ IsLUB ∅ b ∧ ∀ a ∈ ∅, IsAtom a

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✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
h : b = ⊤
⊢ IsLUB {⊤} b ∧ ∀ a ∈ {⊤}, IsAtom a

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✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ IsAtomistic αᵒᵈ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
f : β ↪o α
hbot : f ⊥ = ⊥
b : β
hb : IsAtom (f b)
⊢ IsAtom b

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
⊢ f i ≤ t.sup f ↔ i ∈ t

Tactic:
by

Goal state after:
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
a : α
⊢ IsAtom (l 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✝³ : 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 (update v j (v j + r • v i))) = span R (range v)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Order

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsTrans α r
ι : Type u_1
hι : Nonempty ι
f : ι → α
D : Directed r f
s : Finset ι
z x✝ : ι
⊢ x✝ ∈ 0 → r (f x✝) (f z)

Tactic:
by

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 β
b : β
⊢ ⇑e ⁻¹' Iic b = Iic (e.symm b)

Tactic:
by

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 β
b : β
⊢ ⇑e ⁻¹' Iio b = Iio (e.symm b)

Tactic:
by

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 : β
⊢ ⇑e ⁻¹' Icc a b = Icc (e.symm a) (e.symm b)

Tactic:
by

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 : β
⊢ ⇑e ⁻¹' Ico a b = Ico (e.symm a) (e.symm b)

Tactic:
by

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 : β
⊢ ⇑e ⁻¹' Ioo a b = Ioo (e.symm a) (e.symm b)

Tactic:
by

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 : α
⊢ ⇑e '' Iic a = Iic (e a)

Tactic:
by

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 : α
⊢ ⇑e '' Iio a = Iio (e a)

Tactic:
by

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 : α
⊢ ⇑e '' Ioo a b = Ioo (e a) (e b)

Tactic:
by

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 : α
⊢ ⇑e '' Ioc a b = Ioc (e a) (e b)

Tactic:
by

Goal state after:
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 (u b) ↔ IsAtom b

Tactic:
by

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 : α
⊢ ⇑e '' Icc a b = Icc (e a) (e b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
x y : ↑(Iic ⊤)
⊢ (Equiv.subtypeUnivEquiv ⋯) x ≤ (Equiv.subtypeUnivEquiv ⋯) y ↔ x ≤ y

Tactic:
by

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 (update v j (v j - r • v i))) = span R (range v)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
⊢ IsCoatom (u b) ↔ IsCoatom b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

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

Tactic:
by

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)
⊢ (image g s).SupIndep f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

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

Tactic:
by

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 : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ g i ∉ map g t

Tactic:
by

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 : ι → α
s : Finset ι'
g : ι' ↪ ι
⊢ (map g s).SupIndep f ↔ s.SupIndep (f ∘ ⇑g)

Tactic:
by

Goal state after:
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
this : Disjoint (f i) (f j) → Disjoint (f j) (({i, j}.erase j).sup f)
⊢ {i, j}.SupIndep f ↔ Disjoint (f i) (f j)

Tactic:
by

Goal state after:
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
⊢ {i, j}.SupIndep f ↔ Disjoint (f i) (f j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : Bool → α
⊢ true ≠ false

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
⊢ IsPrincipal R ↥p ↔ p.IsPrincipal

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : Fin 2 → α
⊢ 0 ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
⊢ (s.attach.SupIndep fun a ↦ f ↑a) ↔ s.SupIndep f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : 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
⊢ ⊥ ≤ x ⊓ a

Tactic:
by

Goal state after: