mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
x✝³ : Set α
x✝² : (Set β)ᵒᵈ
h : x✝³ ⊆ (R.rightDual ∘ ⇑ofDual) x✝²
x✝¹ : β
hb : x✝¹ ∈ x✝²
x✝ : α
ha : x✝ ∈ x✝³
⊢ x✝ ∈ x✝³

Tactic:
by

Goal state after:
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ R.leftDual J ∈ R.rightFixedPoints

Tactic:
by

Goal state after:
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
⊢ R.rightDual I ∈ R.leftFixedPoints

Tactic:
apply le_antisymm
  · apply R.gc_leftDual_rightDual.monotone_u; exact R.gc_leftDual_rightDual.l_u_le I
  · exact R.gc_leftDual_rightDual.le_u_l (R.rightDual I)

Goal state after:
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
⊢ R.rightDual I ∈ R.leftFixedPoints

Tactic:
by

Goal state after:
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
J : ↑R.leftFixedPoints
⊢ (fun x ↦
        match x with
        | ⟨I, property⟩ => ⟨R.rightDual I, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨J, property⟩ => ⟨R.leftDual J, ⋯⟩)
        J) =
    J

Tactic:
by

Goal state after:
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
I : ↑R.rightFixedPoints
⊢ (fun x ↦
        match x with
        | ⟨J, property⟩ => ⟨R.leftDual J, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨I, property⟩ => ⟨R.rightDual I, ⋯⟩)
        I) =
    I

Tactic:
by

Goal state after:
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ⊆ J'
⊢ R.rightDual (R.leftDual J) ⊆ J'

Tactic:
by

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
⊢ ∃ f, ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ⊆ I'
⊢ R.leftDual (R.rightDual I) ⊆ I'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s✝ t x y z : α
S : Set α
inst✝ : CompleteLattice α
P Q : Partition s✝
s : α
p p' : Partition s
h : p.parts = p'.parts
⊢ p = p'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : α
inst✝ : CompleteLattice α
P : Partition s
⊢ ⨆ x ∈ P, x = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : α
inst✝ : CompleteLattice α
P : Partition s
hs : s ≠ ⊥
hP : ↑P = ∅
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t x y z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q : Partition s
P : Set α
indep : _root_.sSupIndep P
hsSup : sSup P = s
⊢ ⊥ ∉ P \ {⊥}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t x y z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q : Partition s
P : Set α
indep : _root_.sSupIndep P
hsSup : sSup P = s
⊢ sSup (P \ {⊥}) = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
P : Partition ⊥
x : α
⊢ x ∉ P

Tactic:
by

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t x y z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q : Partition s
P : Partition ⊥
⊢ P = removeBot ∅ ⋯ ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s x : α
inst✝ : CompleteLattice α
P : Partition s
hxP : x ∈ P
⊢ s ≠ ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t x✝ y z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q✝ P Q R : Partition s
hPQ : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hQR : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ R, x ≤ y
x : α
hxP : x ∈ P
⊢ ∃ y ∈ R, x ≤ y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t x y z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q✝ P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
⊢ P = Q

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s x : α
inst✝ : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
⊢ ∃! y, y ∈ Q ∧ x ≤ y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t x✝ y z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q P : Partition s
x : α
hxP : x ∈ P
⊢ ∃ y ∈ removeBot {s} ⋯ ⋯, x ≤ y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : α
inst✝ : CompleteLattice α
hs : s ≠ ⊥
⊢ ↑⊤ = {s}

Tactic:
by

Goal state after:
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
⊢ ¬Disjoint ↑F ↑J₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : α
inst✝ : CompleteLattice α
a : α
⊢ a ∈ ⊤ ↔ a = s ∧ a ≠ ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : α
inst✝ : CompleteLattice α
⊢ ↑⊤ ⊆ {s}

Tactic:
by

Goal state after:
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
J₁F : ¬Disjoint ↑F ↑J₁
⊢ ¬Disjoint ↑F ↑J₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
⊢ _root_.sSupIndep {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
this : sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = sSup ↑P ⊓ sSup ↑Q
⊢ sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = s

Tactic:
by

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
a : α
x✝ : a ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
p : α
hp : p ∈ P
q : α
hq : q ∈ Q
ha : a = p ⊓ q
⊢ a ≤ (p, q).1 ⊓ (p, q).2

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
x✝¹ : α × α
p q : α
x✝ : (p, q) ∈ ↑P ×ˢ ↑Q
hp : (p, q).1 ∈ ↑P
hq : (p, q).2 ∈ ↑Q
⊢ (p, q).1 ⊓ (p, q).2 ≤ p ⊓ q

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
⊢ sSup {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ : ∀ (a : α), ScottContinuousOn ((fun d ↦ Prod.snd '' d) '' D) fun b ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuousOn ((fun d ↦ Prod.fst '' d) '' D) fun a ↦ f (a, b)
h₁' : ∀ (a : α), Monotone fun b ↦ f (a, b)
h₂' : ∀ (b : β), Monotone fun a ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
a : ↑(Prod.fst '' d)
⊢ IsLUB (f '' {↑a} ×ˢ (Prod.snd '' d)) (?m.129 a)

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
a : α
ha : a ∈ removeBot {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} ⋯ ⋯
⊢ ∃ y ∈ P, a ≤ y

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
a : α
ha : a ∈ removeBot {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} ⋯ ⋯
⊢ ∃ y ∈ Q, a ≤ y

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
⊢ ∃ y ∈ removeBot {a | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
J₁F : ¬Disjoint ↑F ↑J₁
J₂F : ¬Disjoint ↑F ↑J₂
c₁ : α
c₁F : c₁ ∈ ↑F
c₁J₁ : c₁ ∈ ↑J₁
c₂ : α
c₂F : c₂ ∈ ↑F
c₂J₂ : c₂ ∈ ↑J₂
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
⊢ (b₁ ⊔ a₁) ⊓ (b₂ ⊔ a₂) ≤ (b ⊔ a₁) ⊓ (b ⊔ a₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
u : Set α
P : Partition u
⊢ x ∈ u ↔ ∃ t ∈ P, x ∈ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
u s t : Set α
P : Partition u
ht : t ∈ P
hs : s ∈ P
hx : x ∈ t ∩ s
hdj : Disjoint t s
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
u : Set α
P : Partition u
⊢ x ∈ u ↔ ∃! t, t ∈ P ∧ x ∈ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
hSP : S ⊆ ↑P
⊢ t ⊆ ⋃₀ S ∧ t ∈ P ↔ t ∈ S

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ : ∀ (a : α), ScottContinuousOn ((fun d ↦ Prod.snd '' d) '' D) fun b ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuousOn ((fun d ↦ Prod.fst '' d) '' D) fun a ↦ f (a, b)
h₁' : ∀ (a : α), Monotone fun b ↦ f (a, b)
h₂' : ∀ (b : β), Monotone fun a ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
⊢ IsLUB (f '' d) (f (p1, p2))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
ht : t ∈ P
hSP : S ⊆ P.parts
⊢ t ⊆ ⋃₀ S ↔ t ∈ S

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α × β → γ
h₁ : ∀ (a : α), ScottContinuous fun b ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuous fun a ↦ f (a, b)
⊢ ScottContinuous f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
a : α
d : Set β
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
c : β
hdc : IsLUB d c
⊢ (fun b ↦ (f a, g b)) '' d = {f a} ×ˢ (g '' d)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
u : Set α
P Q : Partition u
⊢ P.Rel ≤ Q.Rel ↔ P ≤ Q

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x y : α
u t✝ : Set α
P : Partition u
ht : t✝ ∈ P
t : Set α
ht' : t ∈ P
hx : x ∈ t
hy : y ∈ t
h : x ∈ t✝
⊢ y ∈ t✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x y : α
u t✝ : Set α
P : Partition u
ht : t✝ ∈ P
t : Set α
ht' : t ∈ P
hx : x ∈ t
hy : y ∈ t
h : y ∈ t✝
⊢ x ∈ t✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x y : α
u t : Set α
P : Partition u
h : P.Rel x y
ht : t ∈ P
⊢ x ∈ t ↔ y ∈ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
u : Set α
P : Partition u
⊢ P.Rel x x ↔ x ∈ u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s✝ t✝¹ x y z : α
S✝ : Set α
S : Set (Set α)
u s t✝ : Set α
a b c : α
P✝ Q P : Partition u
x✝⁴ x✝³ x✝² : α
x✝¹ : P.Rel x✝⁴ x✝³
x✝ : P.Rel x✝³ x✝²
t : Set α
ht : t ∈ P
ha : x✝⁴ ∈ t
hb : x✝³ ∈ t
t' : Set α
ht' : t' ∈ P
hb' : x✝³ ∈ t'
hc : x✝² ∈ t'
⊢ x✝² ∈ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x y : α
u : Set α
P : Partition u
h : P.Rel x y
⊢ x ∈ u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
u t : Set α
P : Partition u
ht : t ∈ P
hxt : x ∈ t
⊢ t = P.partOf x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
u : Set α
P : Partition u
⊢ x ∈ u ↔ x ∈ P.partOf x ∧ P.partOf x ∈ P

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
b : β
d : Set α
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
c : α
hdc : IsLUB d c
⊢ (fun a ↦ (f a, g b)) '' d = (f '' d) ×ˢ {g b}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
u : Set α
P : Partition u
⊢ (P.partOf x).Nonempty ↔ x ∈ u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
u : Set α
P : Partition u
⊢ P.partOf x = ∅ ↔ x ∉ u

Tactic:
by

Goal state after:
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
⊢ ∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x y : α
u : Set α
P : Partition u
hx : x ∈ u
hy : y ∈ u
⊢ P.Rel x y ↔ P.partOf x = P.partOf y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x y : α
u : Set α
P : Partition u
⊢ P.Rel x y ↔ ∃ (_ : x ∈ u) (_ : y ∈ u), P.partOf x = P.partOf y

Tactic:
by

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
hs : u ⊆ s
⊢ f '' s ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
⊢ ScottContinuous (Prod.map f g)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
ha : a ∈ u
⊢ f a = f b ↔ P.Rel a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.ScottContinuity.Complete

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
h : ScottContinuous f
x✝ : Set α
d₁ : x✝.Nonempty
d₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) x✝
⊢ f (sSup x✝) = sSup (f '' x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ScottContinuity.Complete

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → f (sSup d) = sSup (f '' d)
x✝¹ : Set α
d₁ : x✝¹.Nonempty
d₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) x✝¹
x✝ : α
hda : IsLUB x✝¹ x✝
⊢ IsLUB (f '' x✝¹) (f x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ScottContinuity.Complete

Goal state before:
pp: β : Type u_2
inst✝ : CompleteLinearOrder β
a : β
d : Set β
x✝¹ : d.Nonempty
x✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
⊢ min a (sSup d) = sSup ((fun b ↦ min a b) '' d)

Tactic:
rw [inf_sSup_eq, sSup_image]

Goal state after:
Module: Mathlib.Order.ScottContinuity.Complete

Goal state before:
pp: β : Type u_2
inst✝ : CompleteLinearOrder β
a : β
d : Set β
x✝¹ : d.Nonempty
x✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
⊢ min a (sSup d) = sSup ((fun b ↦ min a b) '' d)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ScottContinuity.Complete

Goal state before:
pp: β : Type u_2
inst✝ : CompleteLinearOrder β
b : β
d : Set β
x✝¹ : d.Nonempty
x✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
⊢ min (sSup d) b = sSup ((fun a ↦ min a b) '' d)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
⊢ f a = f b ↔ a = b ∨ P.Rel a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
a : α
⊢ (∀ (x : α), f a = f x ↔ a = x) ∨ ∀ (x : α), f a = f x ↔ P.Rel a x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
h1 : ∀ (x : α), f a = f x ↔ a = x
⊢ f a = f b → (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
⊢ f a = f b ↔ (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun f
⊢ f (f a) = f a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f g : α → α
hf : P.IsRepFun f
hg : P.IsRepFun g
x : α
⊢ f (g x) = f x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : α
ha : a ∉ u
⊢ f a = a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Std

Goal state before:
pp: case isTrue.isTrue
α : Type u_1
args : OfStdArgs α
this✝⁵ : LE α := args.le
this✝⁴ : LT α := args.lt
this✝³ :
  let this := args.le;
  let this_1 := args.lt;
  Std.LawfulOrderLT α
this✝² :
  let this := args.le;
  Std.IsLinearOrder α
this✝¹ : DecidableLE α := args.decidableLE
this✝ : Std.LawfulOrderLeftLeaningMin α
this : Std.LawfulOrderLeftLeaningMax α
a b : α
h✝¹ : b ≤ a
h✝ : a ≤ b
⊢ a = b

Tactic:
exact Std.le_antisymm ‹_› ‹_›

Goal state after:
Module: Mathlib.Order.Std

Goal state before:
pp: α : Type u_1
args : OfStdArgs α
this✝⁵ : LE α := args.le
this✝⁴ : LT α := args.lt
this✝³ :
  let this := args.le;
  let this_1 := args.lt;
  Std.LawfulOrderLT α
this✝² :
  let this := args.le;
  Std.IsLinearOrder α
this✝¹ : DecidableLE α := args.decidableLE
this✝ : Std.LawfulOrderLeftLeaningMin α
this : Std.LawfulOrderLeftLeaningMax α
a b : α
⊢ max a b = if a ≤ b then b else a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Std

Goal state before:
pp: α : Type u_1
args : OfStdArgs α
this✝⁵ : LE α := args.le
this✝⁴ : LT α := args.lt
this✝³ :
  let this := args.le;
  let this_1 := args.lt;
  Std.LawfulOrderLT α
this✝² :
  let this := args.le;
  Std.IsLinearOrder α
this✝¹ : DecidableLE α := args.decidableLE
this✝ : Std.LawfulOrderLeftLeaningMin α
this : Std.LawfulOrderLeftLeaningMax α
a b : α
⊢ compare a b = compareOfLessAndEq a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
⊢ ∃ f, P.IsRepFun f ∧ ∀ (x : ↑t), f ↑x = f₀ x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
t u : Set α
P : Partition u
h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel x y → x = y
⊢ ∀ (x : ↑t), ↑x ∉ u → ↑x = ↑x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
t u : Set α
P : Partition u
h : ∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel x y → x = y
⊢ ∃ f, P.IsRepFun f ∧ EqOn f id t

Tactic:
by

Goal state after: