mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
⊢ ∀ ⦃x y : α⦄, x ∈ ∅ → y ∈ ∅ → P.Rel x y → x = y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
⊢ ∃ f, P.IsRepFun f

Tactic:
by

Goal state after:
Module: Mathlib.Order.TeichmullerTukey

Goal state before:
pp: α : Type u_1
F : Set (Set α)
hF : IsOfFiniteCharacter F
x : Set α
xF : x ∈ F
⊢ ∃ m, x ⊆ m ∧ Maximal (fun x ↦ x ∈ F) m

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
⊢ type α ≠ 0 ↔ Nonempty α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: α : Type u
inst✝² : LinearOrder α
inst✝¹ : Nonempty α
inst✝ : Subsingleton α
⊢ type α = 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: o : OrderType.{u_1}
⊢ IsEmpty o.ToType ↔ o = 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: o : OrderType.{u_1}
⊢ Nonempty o.ToType ↔ o ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: δ : Sort v
f : (α : Type u_1) → [LinearOrder α] → δ
c : ∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_1) [inst_1 : LinearOrder β], type α = type β → f α = f β
γ : Type u_1
inst✝ : LinearOrder γ
⊢ (type γ).liftOn f c = f γ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: α : Type u
β : Type v
δ : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : (α : Type u) → [LinearOrder α] → (β : Type v) → [LinearOrder β] → δ
c :
  ∀ (α₁ : Type u) [inst : LinearOrder α₁] (β₁ : Type v) [inst_1 : LinearOrder β₁] (α₂ : Type u)
    [inst_2 : LinearOrder α₂] (β₂ : Type v) [inst_3 : LinearOrder β₂],
    type α₁ = type α₂ → type β₁ = type β₂ → f α₁ β₁ = f α₂ β₂
⊢ (type α).liftOn₂ (type β) f c = f α β

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: o : OrderType.{u_1}
ho : o ≠ 0
⊢ 0 < o

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
⊢ lift.{u_1, u} (type α) = lift.{u_1, u} (type β) ↔ Nonempty (α ≃o β)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
⊢ lift.{u_1, u} (type α) ≤ lift.{u_1, u} (type β) ↔ Nonempty (α ↪o β)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: x✝¹ x✝ : ℕ
⊢ Equiv.ulift.symm x✝¹ ≤ Equiv.ulift.symm x✝ ↔ x✝¹ ≤ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
⊢ findAtom ⊥ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
⊢ Order.pred^[0] r = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
⊢ Order.pred (findAtom r) = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Order.pred^[Nat.find ⋯ - 1] r = ⊥
this : Nat.find ⋯ ≤ Nat.find ⋯ - 1
⊢ Nat.find ⋯ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : findAtom r = ⊥
⊢ r = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : r = ⊥
⊢ findAtom r = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a b : X
s1 s2 : Sublocale X
h : (fun x ↦ x.carrier) s1 = (fun x ↦ x.carrier) s2
⊢ s1 = s2

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S : Sublocale X
f : ι → X
hf : ∀ (i : ι), f i ∈ S
⊢ (range fun i ↦ f i) ⊆ ↑S

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ IsAtom (findAtom r)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
⊢ InfClosed ↑S

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
⊢ ⊤ ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : IsAtom (findAtom r)
nh : r = ⊥
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
inst✝ : OrderBot α
b : α
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
t : RootedTree
a₁ a₂ : SubRootedTree t
h : (fun v ↦ Set.Ici v.root) a₁ = (fun v ↦ Set.Ici v.root) a₂
⊢ a₁ = a₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
r : SubRootedTree t
⊢ ⊥ ∈ r ↔ r.root = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
r : SubRootedTree t
hr : r ∈ t.subtrees
⊢ r.root ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
⊢ t₁.root ≤ v₁ ⊓ v₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a b : X
x : Set ↥S
⊢ Subtype.val '' x ⊆ S.carrier

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S : Sublocale X
f : ι → ↥S
⊢ ↑(⨅ i, f i) = ⨅ i, ↑(f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
⊢ t₁ ≠ t₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a b : X
⊢ ∀ (s : Set ↥S), IsGLB s (sInf s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
a b c : ↥S
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
⊢ v₁ ⊓ v₂ ≤ v₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
a : X
⊢ a ≤ ↑(S.restrictAux a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x : X
hx : ↑(S.restrictAux x) ≤ x
⊢ Subtype.val '' {s | x ≤ ↑s} ⊆ ↑S

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x : X
hx : ↑(S.restrictAux x) ≤ x
⊢ x ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a : X
b : ↥S
h : S.restrictAux a ≤ b
⊢ a ≤ ↑(S.restrictAux a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a : X
b : ↥S
h : a ≤ ↑b
⊢ b ∈ {s | a ≤ ↑s}

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : t₁ ≠ t₂
⊢ Disjoint v₁ v₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a : X
b : ↥S
⊢ S.restrictAux a ≤ b ↔ a ≤ ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x : ↥S
⊢ x ≤ S.restrictAux ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b : X
S : Sublocale X
a : X
h : ↑(S.restrictAux a) ≤ a
⊢ ⟨a, ⋯⟩ = S.restrictAux a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s✝ : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a b : X
s : ↥S
⊢ Sublocale.restrictAux✝ S a ⊓ Sublocale.restrictAux✝ S b ≤ s ↔
    Sublocale.restrictAux✝ S a ≤ Sublocale.restrictAux✝ S b ⇨ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
⊢ t.subtrees.PairwiseDisjoint SetLike.coe

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s✝ : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a b : X
s : ↥S
⊢ Sublocale.restrictAux✝ S a ≤ Sublocale.restrictAux✝ S b ⇨ s ↔ ↑(Sublocale.restrictAux✝ S b) ≤ a ⇨ ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
inst✝ : DecidableEq ↑t
v : ↑t
⊢ v ∈ t.subtreeOf v

Tactic:
by

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
inst✝ : DecidableEq ↑t
v : ↑t
hr : v ≠ ⊥
⊢ t.subtreeOf v ∈ t.subtrees

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s✝ : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a b : X
s : ↥S
⊢ ↑(Sublocale.restrictAux✝ S b) ≤ a ⇨ ↑s ↔ b ≤ a ⇨ ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s✝ : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a b : X
s : ↥S
⊢ b ≤ a ⇨ ↑s ↔ Sublocale.restrictAux✝ S (a ⊓ b) ≤ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
⊢ type (α ⊕ₗ β) = type α + type β

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o₁ o₂ o₃ : OrderType.{u}
α : Type u
x✝² : LinearOrder α
β : Type u
x✝¹ : LinearOrder β
γ : Type u
x✝ : LinearOrder γ
⊢ type α + type β + type γ = type α + (type β + type γ)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a b : X
⊢ sInf {s | a ⊓ b ≤ ↑s} = sInf {s | a ≤ ↑s} ⊓ sInf {s | b ≤ ↑s}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ 0 + type α = type α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ type α + 0 = type α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
⊢ type (Lex (α × β)) = type β * type α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o₁ o₂ o₃ : OrderType.{u}
α : Type u
x✝² : LinearOrder α
β : Type u
x✝¹ : LinearOrder β
γ : Type u
x✝ : LinearOrder γ
⊢ type α * type β * type γ = type α * (type β * type γ)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ 1 * type α = type α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
⊢ sInf {s | ⊤ ≤ ↑s} = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ type α * 1 = type α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
⊢ (type α).card = #α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o₁ o₂ : OrderType.{u_1}
x✝³ : Type u_1
x✝² : LinearOrder x✝³
x✝¹ : Type u_1
x✝ : LinearOrder x✝¹
hle : type x✝³ ≤ type x✝¹
⊢ (type x✝³).card ≤ (type x✝¹).card

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: ⊢ card 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: ⊢ card 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: a b c : OrderType.{u_1}
⊢ a * (b + c) = a * b + a * c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s✝ : Set X
f : ι → X
a b : X
S : Sublocale X
s : Set X
⊢ sInf {s_1 | sSup s ≤ ↑s_1} = sSup ((fun x ↦ sInf {s | x ≤ ↑s}) '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x✝¹ x✝ : X
⊢ ↑(S.restrict (x✝¹ ⊓ x✝)) = ↑(S.restrict x✝¹) ⊓ ↑(S.restrict x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x✝ : X
⊢ ↑(S.restrict ↑(S.restrict x✝)) ≤ ↑(S.restrict x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x✝ : X
⊢ ↑(S.restrict ↑(S.restrict x✝)) ≤ ↑(S.restrict x✝)

Tactic:
by rw [S.giRestrict.gc.l_u_l_eq_l]

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
x : X
hx : x ∈ ↑S
⊢ S.toNucleus x = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
⊢ range ⇑S.toNucleus = ↑S

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S T : Sublocale X
⊢ S.toNucleus ≤ T.toNucleus ↔ T ≤ S

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
n : Nucleus X
a : Set X
h : a ⊆ range ⇑n
⊢ sInf a ∈ range ⇑n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
n : Nucleus X
a b : X
h : b ∈ range ⇑n
⊢ a ⇨ b ∈ range ⇑n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
m n : Nucleus X
⊢ m.toSublocale ≤ n.toSublocale ↔ n ≤ m

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
n : Nucleus X
x y : X
hxy : x ≤ n y
⊢ n x ≤ n y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
n : Nucleus X
x : X
⊢ n.toSublocale.restrict x = ⟨n x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
⊢ Function.LeftInverse (fun s ↦ OrderDual.toDual s.toNucleus) fun n ↦ (OrderDual.ofDual n).toSublocale

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
x : X
⊢ (∃ y, ↑(S.restrict y) = x) → x ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
x : X
hx : x ∈ S
⊢ ↑(S.restrict x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
⊢ (fun n ↦ (OrderDual.ofDual n).toSublocale) ((fun s ↦ OrderDual.toDual s.toNucleus) S) = S

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
⊢ ∀ {a b : (Nucleus X)ᵒᵈ},
    { toFun := fun n ↦ (OrderDual.ofDual n).toSublocale, invFun := fun s ↦ OrderDual.toDual s.toNucleus, left_inv := ⋯,
            right_inv := ⋯ }
          a ≤
        { toFun := fun n ↦ (OrderDual.ofDual n).toSublocale, invFun := fun s ↦ OrderDual.toDual s.toNucleus,
            left_inv := ⋯, right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
a : Sublocale X
s : Set (Sublocale X)
⊢ ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.LocallyFinite

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderTop α
hs : s.Finite
⊢ (↑(upperClosure s)).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.LocallyFinite

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : LocallyFiniteOrderBot α
hs : s.Finite
⊢ (↑(lowerClosure s)).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
⊢ ↑s₂ ⊆ ↑s₁ ∧ ↑t₂ ⊆ ↑t₁ ∨ ↑s₂ = ∅ ∨ ↑t₂ = ∅ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₂ = ⊤ ∨ t₂ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : UpperSet α
t : UpperSet β
⊢ s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
⊢ Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : LowerSet α
t₁ t₂ : LowerSet β
⊢ ↑s₁ ⊆ ↑s₂ ∧ ↑t₁ ⊆ ↑t₂ ∨ ↑s₁ = ∅ ∨ ↑t₁ = ∅ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₁ = ⊥ ∨ t₁ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
t : LowerSet β
⊢ s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : LowerSet α
t₁ t₂ : LowerSet β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
⊢ upperClosure (s ×ˢ t) = upperClosure s ×ˢ upperClosure t

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
⊢ lowerClosure (s ×ˢ t) = lowerClosure s ×ˢ lowerClosure t

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst✝ : (i : ι) → MeasurableSpace (β i)
u : (i : ι) → Ω → β i
i : ι
hf : Adapted f u
⊢ inst✝ i ≤ inst✝ i

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst✝ : (i : ι) → MeasurableSpace (β i)
u : (i : ι) → Ω → β i
i j : ι
hf : Adapted f u
hij : i ≤ j
⊢ inst✝ i ≤ inst✝ i

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝³ : Preorder ι
β : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst✝¹ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝ : ∀ (i : ι), BorelSpace (β i)
hum : ∀ (i : ι), StronglyMeasurable (u i)
⊢ StronglyAdapted (natural u hum) u

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
β : Type u_3
mi : MeasurableSpace ι
mβ : MeasurableSpace β
f : Filtration ι m
b : β
x✝ : ι
⊢ Measurable fun p ↦ (fun x x_1 ↦ b) (↑p.1) p.2

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
h : IsProgressive f u
⊢ Adapted f u

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
t : ι → Ω → ι
h : IsProgressive f u
ht : IsProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
⊢ IsProgressive f fun i ω ↦ u (t i ω) ω

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : OpensMeasurableSpace β
hu : IsProgressive f u
i : ι
⊢ Measurable fun p ↦ (fun t ω ↦ ‖u t ω‖) (↑p.1) p.2

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝² : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝¹ : TopologicalSpace β
u : ι → Ω → β
inst✝ : MeasurableSpace ι
h : IsStronglyProgressive f u
⊢ StronglyAdapted f u

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝⁴ : TopologicalSpace β
u : ι → Ω → β
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
ht : IsStronglyProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
⊢ IsStronglyProgressive f fun i ω ↦ u (t i ω) ω

Tactic:
by

Goal state after: