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

Goal state before:
pp: case h₂
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ x ≤ n x

Tactic:
;

Goal state after:
case h₂
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ x ≤ n x
Module: Mathlib.Order.Nucleus

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

Tactic:
;

Goal state after:
case a
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ y ⊓ x ≤ y
Module: Mathlib.Order.Nucleus

Goal state before:
pp: case h₁
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) ≤ n (x ⊔ k)

pp: case h₂
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 (y ⊔ k) ≤ n (y ⊔ k)

Tactic:
;

Goal state after:
case h₁
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) ≤ n (x ⊔ k)

case h₂
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 (y ⊔ k) ≤ n (y ⊔ k)
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: case refl
α : ℕ → 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
b : α (i + 1)
x✝ : ⟨i, a⟩ ≤ ⟨i + 1, b⟩
w✝ : ⟨i, a⟩.fst ≤ ⟨i + 1, b⟩.fst
h✝ : π w✝ ⟨i + 1, b⟩.snd = ⟨i, a⟩.snd
⊢ ⟨i + 1, π ⋯ b⟩ = ⟨i + 1, b⟩

Tactic:
;

Goal state after:
case refl
α : ℕ → 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
b : α (i + 1)
x✝ : ⟨i, a⟩ ≤ ⟨i + 1, b⟩
w✝ : ⟨i, a⟩.fst ≤ ⟨i + 1, b⟩.fst
h✝ : π w✝ ⟨i + 1, b⟩.snd = ⟨i, a⟩.snd
⊢ ⟨i + 1, π ⋯ b⟩ = ⟨i + 1, b⟩
Module: Mathlib.Order.Nucleus

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

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x : X
⊢ n (n x) = n x
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:
;

Goal state after:
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)
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
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
hxcI : xᶜ ∈ I
ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I
⊢ y ∈ I

Tactic:
inf_comm,

Goal state after:
P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
hxcI : xᶜ ∈ I
ass : y ⊓ x ⊔ y ⊓ xᶜ ∈ I
⊢ y ∈ I
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:
;

Goal state after:
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)
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:
;

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
n : Nucleus X
⊢ ↑(rangeFactorization ⇑n ⊤) = ↑⊤
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.Rel.GaloisConnection

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ J ⊆ R.rightDual (R.leftDual J)

Tactic:
;

Goal state after:
case a
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ J ⊆ R.rightDual (R.leftDual J)
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
⊢ (fun b ↦ ∀ ⦃a : α⦄, a ∈ R.rightDual I → (a, b) ∈ R) ≤ I

Tactic:
;

Goal state after:
case a
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
⊢ (fun b ↦ ∀ ⦃a : α⦄, a ∈ R.rightDual I → (a, b) ∈ R) ≤ I
Module: Mathlib.Order.Rel.GaloisConnection

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
hJ : J ∈ R.leftFixedPoints
⊢ (fun x ↦
        match x with
        | ⟨I, property⟩ => ⟨R.rightDual I, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨J, property⟩ => ⟨R.leftDual J, ⋯⟩)
        ⟨J, hJ⟩) =
    ⟨J, hJ⟩
Module: Mathlib.Order.Rel.GaloisConnection

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
R : SetRel α β
I : Set β
hI : I ∈ R.rightFixedPoints
⊢ (fun x ↦
        match x with
        | ⟨J, property⟩ => ⟨R.leftDual J, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨I, property⟩ => ⟨R.rightDual I, ⋯⟩)
        ⟨I, hI⟩) =
    ⟨I, hI⟩
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case mk
α : Type u_1
s✝ t x y z : α
S : Set α
inst✝ : CompleteLattice α
P Q : Partition s✝
s : α
p' : Partition s
parts✝ : Set α
sSupIndep'✝ : sSupIndep parts✝
bot_notMem'✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
h : { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ }.parts = p'.parts
⊢ { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ } = p'

Tactic:
;

Goal state after:
case mk
α : Type u_1
s✝ t x y z : α
S : Set α
inst✝ : CompleteLattice α
P Q : Partition s✝
s : α
p' : Partition s
parts✝ : Set α
sSupIndep'✝ : sSupIndep parts✝
bot_notMem'✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
h : { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ }.parts = p'.parts
⊢ { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ } = p'
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case mk.mk
α : Type u_1
s✝ t x y z : α
S : Set α
inst✝ : CompleteLattice α
P Q : Partition s✝
s : α
parts✝¹ : Set α
sSupIndep'✝¹ : sSupIndep parts✝¹
bot_notMem'✝¹ : ⊥ ∉ parts✝¹
sSup_eq'✝¹ : sSup parts✝¹ = s
parts✝ : Set α
sSupIndep'✝ : sSupIndep parts✝
bot_notMem'✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
h :
  { parts := parts✝¹, sSupIndep' := sSupIndep'✝¹, bot_notMem' := bot_notMem'✝¹, sSup_eq' := sSup_eq'✝¹ }.parts =
    { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ }.parts
⊢ { parts := parts✝¹, sSupIndep' := sSupIndep'✝¹, bot_notMem' := bot_notMem'✝¹, sSup_eq' := sSup_eq'✝¹ } =
    { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
s✝ t x y z : α
S : Set α
inst✝ : CompleteLattice α
P Q : Partition s✝
s : α
parts✝¹ : Set α
sSupIndep'✝¹ : sSupIndep parts✝¹
bot_notMem'✝¹ : ⊥ ∉ parts✝¹
sSup_eq'✝¹ : sSup parts✝¹ = s
parts✝ : Set α
sSupIndep'✝ : sSupIndep parts✝
bot_notMem'✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
h :
  { parts := parts✝¹, sSupIndep' := sSupIndep'✝¹, bot_notMem' := bot_notMem'✝¹, sSup_eq' := sSup_eq'✝¹ }.parts =
    { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ }.parts
⊢ { parts := parts✝¹, sSupIndep' := sSupIndep'✝¹, bot_notMem' := bot_notMem'✝¹, sSup_eq' := sSup_eq'✝¹ } =
    { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ }
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: α : Type u_1
s t x y z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q : Partition s
P : Partition ⊥
x✝ : α
⊢ x✝ ∈ P ↔ x✝ ∈ removeBot ∅ ⋯ ⋯

Tactic:
;

Goal state after:
α : Type u_1
s t x y z : α
S : Set α
inst✝ : CompleteLattice α
P✝ Q : Partition s
P : Partition ⊥
x✝ : α
⊢ x✝ ∈ P ↔ x✝ ∈ removeBot ∅ ⋯ ⋯
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 α) := ⋯
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := ⋯
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := ⋯
J₂ : Ideal α := ⋯
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 : α := ⋯
bJ : b ∈ J
⊢ b₁ ≤ b

pp: case h₁
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := ⋯
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := ⋯
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := ⋯
J₂ : Ideal α := ⋯
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 : α := ⋯
bJ : b ∈ J
⊢ b₂ ≤ b

Tactic:
;

Goal state after:
case h₁
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := ⋯
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := ⋯
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := ⋯
J₂ : Ideal α := ⋯
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 : α := ⋯
bJ : b ∈ J
⊢ b₁ ≤ b

case h₁
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := ⋯
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := ⋯
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := ⋯
J₂ : Ideal α := ⋯
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 : α := ⋯
bJ : b ∈ J
⊢ b₂ ≤ 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 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:
have ⟨q, hq⟩ := hQ ha

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 R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
q : α
hq : q ∈ Q ∧ a ≤ q
⊢ ∃ y ∈ removeBot {a | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y
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
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₂
⊢ a₁ ⊓ a₂ ∉ J

Tactic:
have ba₁a₂F : b ⊔ (a₁ ⊓ a₂) ∈ F := PFilter.mem_of_le ineq (PFilter.inf_mem c₁F c₂F)

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
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
⊢ a₁ ⊓ a₂ ∉ J
Module: Mathlib.Order.Sublocale

Goal state before:
pp: case mk
X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a b : X
s2 : Sublocale X
carrier✝ : Set X
sInf_mem'✝ : ∀ s ⊆ carrier✝, sInf s ∈ carrier✝
himp_mem'✝ : ∀ (a b : X), b ∈ carrier✝ → a ⇨ b ∈ carrier✝
h :
  (fun x ↦ x.carrier) { carrier := carrier✝, sInf_mem' := sInf_mem'✝, himp_mem' := himp_mem'✝ } = (fun x ↦ x.carrier) s2
⊢ { carrier := carrier✝, sInf_mem' := sInf_mem'✝, himp_mem' := himp_mem'✝ } = s2

Tactic:
;

Goal state after:
case mk
X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a b : X
s2 : Sublocale X
carrier✝ : Set X
sInf_mem'✝ : ∀ s ⊆ carrier✝, sInf s ∈ carrier✝
himp_mem'✝ : ∀ (a b : X), b ∈ carrier✝ → a ⇨ b ∈ carrier✝
h :
  (fun x ↦ x.carrier) { carrier := carrier✝, sInf_mem' := sInf_mem'✝, himp_mem' := himp_mem'✝ } = (fun x ↦ x.carrier) s2
⊢ { carrier := carrier✝, sInf_mem' := sInf_mem'✝, himp_mem' := himp_mem'✝ } = s2
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
a : X
ha : a ∈ ↑S
b : X
hb : b ∈ ↑S
⊢ a ⊓ b ∈ ↑S

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
a : X
ha : a ∈ ↑S
b : X
hb : b ∈ ↑S
⊢ a ⊓ b ∈ ↑S
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
a : X
ha : a ∈ ↑S
b : X
hb : b ∈ ↑S
⊢ sInf {a, b} ∈ ↑S

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
a : X
ha : a ∈ ↑S
b : X
hb : b ∈ ↑S
⊢ sInf {a, b} ∈ ↑S
Module: Mathlib.Order.SuccPred.Tree

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
nh : r = ⊥
h : IsAtom ⊥
⊢ False
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
⊢ ∀ x_1 ∈ x, x_1 ∈ Subtype.val ⁻¹' S.carrier

Tactic:
;

Goal state after:
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
⊢ ∀ x_1 ∈ x, x_1 ∈ Subtype.val ⁻¹' S.carrier
Module: Mathlib.Order.Sublocale

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

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
x : X
⊢ x ∈ (fun n ↦ (OrderDual.ofDual n).toSublocale) ((fun s ↦ OrderDual.toDual s.toNucleus) S) ↔ x ∈ S
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 : ι
⊢ OpensMeasurableSpace β

Tactic:
;

Goal state after:
Ω : 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 : ι
⊢ OpensMeasurableSpace β
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 β
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
⊢ (fun i a ↦ ∏ c ∈ s, U c i a) = ∏ c ∈ s, U c

Tactic:
;

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁴ : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
⊢ (fun i a ↦ ∏ c ∈ s, U c i a) = ∏ c ∈ s, U c
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 β
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
i : ι
a : Ω
⊢ ∏ c ∈ s, U c i a = (∏ c ∈ s, U c) i a

Tactic:
;

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁴ : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
i : ι
a : Ω
⊢ ∏ c ∈ s, U c i a = (∏ c ∈ s, U c) i a
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[f (i + 1) + g (i + 1) - (f i + g i) | ↑ℱ i] =ᵐ[μ] μ[f (i + 1) - f i + (g (i + 1) - g i) | ↑ℱ i]

Tactic:
;

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[f (i + 1) + g (i + 1) - (f i + g i) | ↑ℱ i] =ᵐ[μ] μ[f (i + 1) - f i + (g (i + 1) - g i) | ↑ℱ i]
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[f (i + 1) + (g (i + 1) + (-1 • f i + -1 • g i)) | ↑ℱ i] =ᵐ[μ]
    μ[f (i + 1) + (g (i + 1) + (-1 • f i + -1 • g i)) | ↑ℱ i]

Tactic:
;

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[f (i + 1) + (g (i + 1) + (-1 • f i + -1 • g i)) | ↑ℱ i] =ᵐ[μ]
    μ[f (i + 1) + (g (i + 1) + (-1 • f i + -1 • g i)) | ↑ℱ i]