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

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n m : Nucleus X
x y : X
a : ↑(range ⇑n)
s : Set ↑(range ⇑n)
⊢ n (↑a ⊓ sSup (Subtype.val '' s)) ≤ ↑(rangeFactorization (⇑n) (sSup (Subtype.val '' range fun x ↦ a ⊓ ↑x)))

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : Frame X
n m : Nucleus X
x y : X
a : ↑(range ⇑n)
s : Set ↑(range ⇑n)
⊢ n (↑a ⊓ sSup (Subtype.val '' s)) ≤ ↑(rangeFactorization (⇑n) (sSup (Subtype.val '' range fun x ↦ a ⊓ ↑x)))
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : I.IsPrime
J : Ideal P
hIJ : I < J
x y : P
hyJ : y ∈ ↑J
hyI : y ∉ ↑I
ass : x ∈ J
⊢ x ∈ ↑J

Tactic:
]

Goal state after:
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : I.IsPrime
J : Ideal P
hIJ : I < J
x y : P
hyJ : y ∈ ↑J
hyI : y ∉ ↑I
ass : x ∈ J
⊢ x ∈ ↑J
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal ↑IF.I

Tactic:
]

Goal state after:
P : Type u_1
inst✝ : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal ↑IF.I
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
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst = 0
ha₀inf : (Ici a₀).Infinite
hfin : ∀ (a : αs), {x | a ⋖ x}.Finite
f : ℕ ↪o αs
hf0 : f 0 = a₀
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
i : ℕ
ih : (f i).fst = i
⊢ i + 1 = i.succ

Tactic:
]

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
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst = 0
ha₀inf : (Ici a₀).Infinite
hfin : ∀ (a : αs), {x | a ⋖ x}.Finite
f : ℕ ↪o αs
hf0 : f 0 = a₀
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
hr : ∀ (i : ℕ), (f i).fst = i
i : ℕ
⊢ α (f i).fst

Tactic:
]

Goal state after:
α : ℕ → 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
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst = 0
ha₀inf : (Ici a₀).Infinite
hfin : ∀ (a : αs), {x | a ⋖ x}.Finite
f : ℕ ↪o αs
hf0 : f 0 = a₀
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
hr : ∀ (i : ℕ), (f i).fst = i
i : ℕ
⊢ α (f i).fst
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
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst = 0
ha₀inf : (Ici a₀).Infinite
hfin : ∀ (a : αs), {x | a ⋖ x}.Finite
f : ℕ ↪o αs
hf0 : f 0 = a₀
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
hr : ∀ (i : ℕ), (f i).fst = i
i : ℕ
⊢ α i

Tactic:
rw [← hr i]

Goal state after:
α : ℕ → 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
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst = 0
ha₀inf : (Ici a₀).Infinite
hfin : ∀ (a : αs), {x | a ⋖ x}.Finite
f : ℕ ↪o αs
hf0 : f 0 = a₀
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
hr : ∀ (i : ℕ), (f i).fst = i
i : ℕ
⊢ α (f i).fst
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
n : Nucleus X
s : Set X
⊢ ⨆ a ∈ s, rangeFactorization (⇑n) a = ⨆ a ∈ s, rangeFactorization (⇑n) a

Tactic:
]

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n m : Nucleus X
h : ⇑n ∘ ⇑m = ⇑m
⊢ ⇑n ≤ ⇑n ∘ ⇑m

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : Frame X
n m : Nucleus X
h : ⇑n ∘ ⇑m = ⇑m
⊢ ⇑n ≤ ⇑n ∘ ⇑m
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n m : Nucleus X
h : range ⇑m ⊆ range ⇑n
x : X
⊢ n x ≤ n (m x)

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : Frame X
n m : Nucleus X
h : range ⇑m ⊆ range ⇑n
x : X
⊢ n x ≤ n (m x)
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
hJ : J ∈ R.leftFixedPoints
⊢ J = J

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
hI : I ∈ R.rightFixedPoints
⊢ R.leftDual (R.rightDual I) = I

Tactic:
hI

Goal state after:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
hI : I ∈ R.rightFixedPoints
⊢ I = I
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
hI : I ∈ R.rightFixedPoints
⊢ I = I

Tactic:
]

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) ⊆ R.rightDual (R.leftDual J')

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
R : SetRel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ⊆ J'
⊢ R.rightDual (R.leftDual J) ⊆ R.rightDual (R.leftDual J')
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: case h
α : 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
⊢ ∀ {x y : α}, x ⊓ y ∈ J → x ∈ J ∨ y ∈ J

Tactic:
]

Goal state after:
case h
α : 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
⊢ ∀ {x y : α}, x ⊓ y ∈ J → x ∈ J ∨ y ∈ J
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) ⊆ R.leftDual (R.rightDual I')

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
R : SetRel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ⊆ I'
⊢ R.leftDual (R.rightDual I) ⊆ R.leftDual (R.rightDual I')
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 β
⊢ ∀ i ∈ Y, ⨅ x ∈ X, f x i ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y

Tactic:
]

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
⊢ ∀ i ∈ Y, ⨅ x ∈ X, f x i ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
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 : F
hy : y ∈ Y
⊢ ∀ i ∈ X, ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f i y

Tactic:
]

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
⊢ ∀ i ∈ X, ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f i y
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case refine_1
α : 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
x : α
h : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
hx' : x ∈ P
hyx' : y ≤ x
⊢ y ∈ Q

Tactic:
]

Goal state after:
case refine_1
α : 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
x : α
h : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
hx' : x ∈ P
hyx' : y ≤ x
⊢ y ∈ Q
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case refine_2
α : 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
x : α
h : x ∈ Q
y : α
hy : y ∈ P
hxy : x ≤ y
hx' : x ∈ Q
hyx' : y ≤ x
⊢ y ∈ P

Tactic:
]

Goal state after:
case refine_2
α : 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
x : α
h : x ∈ Q
y : α
hy : y ∈ P
hxy : x ≤ y
hx' : x ∈ Q
hyx' : y ≤ x
⊢ y ∈ P
Module: Mathlib.Order.Partition.Basic

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

Tactic:
]

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
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a y ≤ ⨆ y ∈ Y, f a y

Tactic:
]

Goal state after:
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
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a y ≤ ⨆ y ∈ Y, f a y
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 | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}.PairwiseDisjoint id

Tactic:
]

Goal state after:
α✝ : 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 | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}.PairwiseDisjoint id
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
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, f x b ≤ f x b

Tactic:
]

Goal state after:
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
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, f x b ≤ f x b
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
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b ↔ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b

Tactic:
]

Goal state after:
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
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b ↔ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
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} = ⨆ p ∈ ↑P ×ˢ ↑Q, p.1 ⊓ p.2

Tactic:
]

Goal state after:
α✝ : 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} = ⨆ p ∈ ↑P ×ˢ ↑Q, p.1 ⊓ p.2
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 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b

Tactic:
]

Goal state after:
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 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
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 ((fun x ↦ f (↑a, x)) '' Prod.snd '' d) (?m.129 a)

Tactic:
]

Goal state after:
α : 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 ((fun x ↦ f (↑a, x)) '' Prod.snd '' d) (?m.129 a)
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case left.a
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 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ ⨆ y ∈ Y, f a y

Tactic:
]

Goal state after:
case left.a
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 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ ⨆ y ∈ Y, f a y
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 {x | ∃ y, (fun b ↦ f (↑y, b)) (p1, p2).2 = x} (f (p1, p2))

Tactic:
]

Goal state after:
α : 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 {x | ∃ y, (fun b ↦ f (↑y, b)) (p1, p2).2 = x} (f (p1, p2))
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case a
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 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, f x b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y

Tactic:
]

Goal state after:
case a
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 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, f x b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
Module: Mathlib.Order.Partition.Basic

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

Tactic:
]

Goal state after:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : ∃ t ∈ ↑P, x ∈ t
⊢ ∃ t ∈ P, x ∈ t
Module: Mathlib.Order.Partition.Basic

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

Tactic:
]

Goal state after:
α : Type u_1
x : α
u : Set α
P : Partition u
hx : ∃ t ∈ ↑P, x ∈ t
⊢ ∃! t, t ∈ P ∧ x ∈ t
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 ∧ t ∈ P

Tactic:
]

Goal state after:
α : Type u_1
S : Set (Set α)
u t : Set α
P : Partition u
ht : t ∈ P
hSP : S ⊆ P.parts
⊢ t ⊆ ⋃₀ S ↔ t ⊆ ⋃₀ S ∧ t ∈ P
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case right.a
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 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f a y

Tactic:
]

Goal state after:
case right.a
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 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f a y
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:
]

Goal state after:
α : 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
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:
]

Goal state after:
α : 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
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:
]

Goal state after:
α : 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'
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: case h
α : 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
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
ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂
ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F
ha₁a₂ : a₁ ⊓ a₂ ∈ J
⊢ ∃ x ∈ ↑F, x ∈ Jset

Tactic:
]

Goal state after:
case h
α : 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
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
ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂
ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F
ha₁a₂ : a₁ ⊓ a₂ ∈ J
⊢ ∃ x ∈ ↑F, x ∈ Jset
Module: Mathlib.Order.Partition.Basic

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

pp: α : Type u_1
x : α
u : Set α
P : Partition u
⊢ Partition u

Tactic:
]

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case a
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 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, f x b ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y

Tactic:
]

Goal state after:
case a
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 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, f x b ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y
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
x✝ : P.Rel x y
t : Set α
htP : t ∈ P
hxt : x ∈ t
hyt : y ∈ t
⊢ y ∈ t

Tactic:
]

Goal state after:
α : Type u_1
x y : α
u : Set α
P : Partition u
hx : x ∈ u
hy : y ∈ u
x✝ : P.Rel x y
t : Set α
htP : t ∈ P
hxt : x ∈ t
hyt : y ∈ t
⊢ y ∈ t
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
hab : f a = f b
⊢ P.Rel b (f b)

Tactic:
]

Goal state after:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
ha : a ∈ u
hab : f a = f b
⊢ P.Rel b (f b)
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
hab : f a = b
hb : b ∉ u
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
ha : a ∈ u
hab : f a = b
hb : b ∉ u
⊢ False
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✝) = f (sSup x✝)

Tactic:
]

Goal state after: