mathlib-initiative/mathlib-tactics huggingface dataset:
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 := ⋯ }
⊢ ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst

Tactic:
by

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
⊢ ∀ {w x y z : α}, r w x → r y z → r (w ⊓ y) (x ⊓ z)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : SemilatticeInf X
n m : Nucleus X
x y : X
f g : Nucleus X
h : (fun x ↦ x.toFun) f = (fun x ↦ x.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : SemilatticeInf X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
⊢ (⇑m ⊓ ⇑n) (x ⊓ y) = (⇑m ⊓ ⇑n) x ⊓ (⇑m ⊓ ⇑n) y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : SemilatticeInf X
n✝ m✝ : Nucleus X
x✝ y : X
m n : Nucleus X
x : X
⊢ (⇑m ⊓ ⇑n) ((⇑m ⊓ ⇑n) x) ≤ (⇑m ⊓ ⇑n) x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : SemilatticeInf X
n m : Nucleus X
x y : X
⊢ ∀ (a b : X), a ⊓ b = a ⊓ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : SemilatticeInf X
n m : Nucleus X
x y : X
⊢ ∀ (x : X), x ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝¹ : SemilatticeInf X
n m : Nucleus X
x y : X
inst✝ : OrderTop X
⊢ ∀ (a b : X), ⊤ (a ⊓ b) = ⊤ a ⊓ ⊤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝¹ : SemilatticeInf X
n m : Nucleus X
x y : X
inst✝ : OrderTop X
⊢ ∀ (x : X), ⊤ (⊤ x) ≤ ⊤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝¹ : SemilatticeInf X
n m : Nucleus X
x y : X
inst✝ : OrderTop X
⊢ ∀ (x : X), x ≤ ⊤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝¹ : SemilatticeInf X
n m : Nucleus X
x y : X
inst✝ : OrderTop X
x✝¹ : Nucleus X
x✝ : X
⊢ x✝¹ x✝ ≤ ⊤ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ z✝ : α
h1 : r w x✝
h2 : r y✝ z✝
compatible_left_sup : ∀ {x y t : α}, r x y → r (x ⊔ t) (y ⊔ t)
⊢ r (w ⊔ y✝) (w ⊔ z✝)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
⊢ ∀ {w x y z : α}, r w x → r y z → r (w ⊔ y) (x ⊔ z)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : FunLike F α β
inst✝ : LatticeHomClass F α β
f : F
w✝ x✝² y✝ z✝ : α
x✝¹ : (Setoid.ker ⇑f) w✝ x✝²
x✝ : (Setoid.ker ⇑f) y✝ z✝
⊢ (Setoid.ker ⇑f) (w✝ ⊓ y✝) (x✝² ⊓ z✝)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : FunLike F α β
inst✝ : LatticeHomClass F α β
f : F
w✝ x✝² y✝ z✝ : α
x✝¹ : (Setoid.ker ⇑f) w✝ x✝²
x✝ : (Setoid.ker ⇑f) y✝ z✝
⊢ (Setoid.ker ⇑f) (w✝ ⊔ y✝) (x✝² ⊔ z✝)

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
α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
i : ℕ
a : α i
j : ℕ
b : α j
hne : ⟨i, a⟩ ≠ ⟨j, b⟩
hij : i ≤ j
h2 : π hij b = a
⊢ i ≠ j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : CompleteLattice X
s : Set (Nucleus X)
x y : X
⊢ ⨅ f ∈ s, f (x ⊓ y) = (⨅ f ∈ s, f x) ⊓ ⨅ f ∈ s, f y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : CompleteLattice X
s : Set (Nucleus X)
x : X
⊢ x ≤ ⨅ f ∈ s, f x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : CompleteLattice X
ι : Type u_2
f : ι → Nucleus X
x : X
⊢ (iInf f) x = ⨅ j, (f j) x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : CompleteLattice X
x✝ : Set (Nucleus X)
⊢ sInf x✝ ∈ lowerBounds x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : CompleteLattice X
x✝ : Set (Nucleus X)
⊢ sInf x✝ ∈ upperBounds (lowerBounds x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n (x ⇨ y) ⊓ x ≤ n (x ⇨ y) ⊓ n x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n (x ⇨ y) ⊓ n x = n (y ⊓ x)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n (y ⊓ x) ≤ n y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n (x ⇨ y) ≤ x ⇨ n y

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
α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
i : ℕ
a : α i
j : ℕ
b : α j
hne : ⟨i, a⟩ ≠ ⟨j, b⟩
hij : i ≤ j
h2 : π hij b = a
hle : i + 1 ≤ j
⊢ ⟨i, a⟩.fst ≤ ⟨i + 1, π hle b⟩.fst

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ x ⇨ n (n y) = x ⇨ n y

Tactic:
by

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
w : P
h : w ∈ ↑IF.F
⊢ w ∉ IF.I

Tactic:
← IF.compl_I_eq_F

Goal state after:
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
w : P
h : w ∈ (↑IF.I)ᶜ
⊢ w ∉ IF.I
Module: Mathlib.Order.PrimeIdeal

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
⊢ IsPFilter (↑IF.I)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : SemilatticeInf P
I : Ideal P
hI : I.IsPrime
x y : P
⊢ x ⊓ y ∈ I → x ∈ I ∨ y ∈ I

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
α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
i : ℕ
a : α i
j : ℕ
b : α j
hne : ⟨i, a⟩ ≠ ⟨j, b⟩
hij : i ≤ j
h2 : π hij b = a
hle : i + 1 ≤ j
⊢ π ⋯ ⟨i + 1, π hle b⟩.snd = ⟨i, a⟩.snd

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
⊢ (∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1) → (∀ i ≥ y, l ⊓ m i ≤ n i) → l ≤ m k → l ≤ n k

Tactic:
hlx

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
⊢ (∀ i ≥ y, l ⊓ m i ≤ n i) → l ≤ m k → l ≤ n k
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
i : ℕ
a : α i
j : ℕ
b : α j
hne : ⟨i, a⟩ ≠ ⟨j, b⟩
hij : i ≤ j
h2 : π hij b = a
hle : i + 1 ≤ j
⊢ ⟨i, a⟩.fst + 1 = ⟨i + 1, π hle b⟩.fst

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
α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
i : ℕ
a : α i
j : ℕ
b : α j
hne : ⟨i, a⟩ ≠ ⟨j, b⟩
hij : i ≤ j
h2 : π hij b = a
hle : i + 1 ≤ j
⊢ π hle ⟨j, b⟩.snd = ⟨i + 1, π hle b⟩.snd

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
α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
⊢ IsStronglyAtomic αs

Tactic:
by

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ I.IsPrime

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
α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₀, a₀.fst = 0 ∧ (Ici a₀).Infinite

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
hly : ∀ i ≥ y, l ⊓ m i ≤ n i
hlk : l ≤ m k
⊢ l = l ⊓ m (x ⊔ k) ⊓ (l ⊓ m (y ⊔ k))

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
α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
x✝¹ : αs
i : ℕ
a : α i
j : ℕ
b : α j
x✝ : ⟨i, a⟩ ≤ ⟨j, b⟩
hj : i + 1 = j
w✝ : ⟨i, a⟩.fst ≤ ⟨j, b⟩.fst
h✝ : π w✝ ⟨j, b⟩.snd = ⟨i, a⟩.snd
⊢ π ⋯ (π ⋯ b) = a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
hly : ∀ i ≥ y, l ⊓ m i ≤ n i
hlk : l ≤ m k
⊢ l ⊓ m (x ⊔ k) ⊓ (l ⊓ m (y ⊔ k)) ≤ n (x ⊔ k) ⊓ n (y ⊔ k)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
hly : ∀ i ≥ y, l ⊓ m i ≤ n i
hlk : l ≤ m k
⊢ n (x ⊔ k) ⊓ n (y ⊔ k) = n k

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
⊢ ⨅ y_1, ⨅ (_ : y_1 ≥ x ⊓ y), m y_1 ⇨ n y_1 = (⨅ y, ⨅ (_ : y ≥ x), m y ⇨ n y) ⊓ ⨅ y_1, ⨅ (_ : y_1 ≥ y), m y_1 ⇨ n y_1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
hy : y ≥ x
⊢ m (m y ⇨ n y) ⇨ n (m y ⇨ n y) = m y ⇨ n y

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
α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
x✝¹ : αs
i : ℕ
a : α i
j : ℕ
b : α j
x✝ : ⟨i, a⟩ ≤ ⟨j, b⟩
hj : i + 1 = j
w✝ : ⟨i, a⟩.fst ≤ ⟨j, b⟩.fst
h✝ : π w✝ ⟨j, b⟩.snd = ⟨i, a⟩.snd
⊢ ⟨i + 1, π ⋯ b⟩ = ⟨j, b⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x y : X
m n : Nucleus X
⊢ ∀ (x : X), x ≤ ⨅ y, ⨅ (_ : y ≥ x), m y ⇨ n y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
x✝² n x✝¹ : Nucleus X
h : ∀ (i : X), x✝² i ⊓ n i ≤ x✝¹ i
i j : X
x✝ : i ≤ j
⊢ x✝² i ⊓ n j ≤ x✝² j ⊓ n j

Tactic:
by

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
⊢ I.IsPrime

Tactic:
by

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
⊢ I.IsPrime

Tactic:
by
  rw [isPrime_iff_mem_or_mem]
  intro x y
  contrapose!
  rintro ⟨hx, hynI⟩ hxy
  apply hynI
  let J := I ⊔ principal x
  have hJuniv : (J : Set P) = Set.univ :=
    IsMaximal.maximal_proper (lt_sup_principal_of_notMem ‹_›)
  have hyJ : y ∈ (J : Set P) := Set.eq_univ_iff_forall.mp hJuniv y
  rw [coe_sup_eq] at hyJ
  rcases hyJ with ⟨a, ha, b, hb, hy⟩
  rw [hy]
  refine sup_mem ha (I.lower (le_inf hb ?_) hxy)
  rw [hy]
  exact le_sup_right

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
⊢ ∀ (a : αs), {x | a ⋖ x}.Finite

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
x✝¹ n x✝ : Nucleus X
⊢ x✝¹ ≤ n ⇨ x✝ ↔ x✝¹ ⊓ n ≤ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
⊢ x ∈ I ∨ xᶜ ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n : Nucleus X
x : X
⊢ x ∈ range ⇑n → n x = x

Tactic:
by

Goal state after:
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
x : X
hx : ↑(rangeFactorization (⇑n) x) ≤ x
⊢ ⟨x, ⋯⟩ = rangeFactorization (⇑n) x

Tactic:
by

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
⊢ I.IsPrime

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
α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)
⊢ (f Nat.zero).fst = Nat.zero

Tactic:
by

Goal state after:
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 ⊓ y ⊔ x ⊓ yᶜ ∈ J
⊢ x ∈ ↑J

Tactic:
by

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : I.IsPrime
⊢ I.IsMaximal

Tactic:
by

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal (↑IF.F)ᶜ

Tactic:
by

Goal state after:
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)
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

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
α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
⊢ (f i.succ).fst = i.succ

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}
⊢ ↑I ⊆ ↑I ∧ Disjoint ↑F ↑I

Tactic:
by

Goal state after:
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
a b : X
⊢ rangeFactorization (⇑n) (a ⊓ b) = rangeFactorization (⇑n) a ⊓ rangeFactorization (⇑n) b

Tactic:
by

Goal state after:
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
⊢ rangeFactorization ⇑n ⊤ = ⊤

Tactic:
by

Goal state after:
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
⊢ rangeFactorization (⇑n) (sSup s) = sSup (rangeFactorization ⇑n '' s)

Tactic:
by

Goal state after:
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
⊢ rangeFactorization (⇑n) (sSup s) = sSup (rangeFactorization ⇑n '' s)

Tactic:
by rw [n.giAux.gc.l_sSup, sSup_image]

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 : ℕ
⊢ α i

Tactic:
by

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 ≤ m

Tactic:
by

Goal state after:
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 ≤ m x

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}
IinS : ↑I ∈ S
⊢ ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub

Tactic:
by

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

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

Tactic:
by

Goal state after: