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

Goal state before:
pp: case pos
α : 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 b : α
hab : P.Rel a b
h₁ : ∃ b, P.Rel a ↑b
h₂ : ∃ b_1, P.Rel b ↑b_1
⊢ f₀ h₁.choose = f₀ h₂.choose

pp: case neg
α : 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 b : α
hab : P.Rel a b
h₁ : ∃ b, P.Rel a ↑b
h₂ : ¬∃ b_1, P.Rel b ↑b_1
⊢ f₀ h₁.choose = P.rep ⋯

pp: case pos
α : 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 b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ∃ b_1, P.Rel b ↑b_1
⊢ P.rep ⋯ = f₀ h₂.choose

pp: case neg
α : 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 b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ¬∃ b_1, P.Rel b ↑b_1
⊢ P.rep ⋯ = P.rep ⋯

Tactic:
·

Goal state after:
case pos
α : 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 b : α
hab : P.Rel a b
h₁ : ∃ b, P.Rel a ↑b
h₂ : ∃ b_1, P.Rel b ↑b_1
⊢ f₀ h₁.choose = f₀ h₂.choose
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case neg
α : 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 b : α
hab : P.Rel a b
h₁ : ∃ b, P.Rel a ↑b
h₂ : ¬∃ b_1, P.Rel b ↑b_1
⊢ f₀ h₁.choose = P.rep ⋯

pp: case pos
α : 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 b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ∃ b_1, P.Rel b ↑b_1
⊢ P.rep ⋯ = f₀ h₂.choose

pp: case neg
α : 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 b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ¬∃ b_1, P.Rel b ↑b_1
⊢ P.rep ⋯ = P.rep ⋯

Tactic:
·

Goal state after:
case neg
α : 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 b : α
hab : P.Rel a b
h₁ : ∃ b, P.Rel a ↑b
h₂ : ¬∃ b_1, P.Rel b ↑b_1
⊢ f₀ h₁.choose = P.rep ⋯
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case pos
α : 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 b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ∃ b_1, P.Rel b ↑b_1
⊢ P.rep ⋯ = f₀ h₂.choose

pp: case neg
α : 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 b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ¬∃ b_1, P.Rel b ↑b_1
⊢ P.rep ⋯ = P.rep ⋯

Tactic:
·

Goal state after:
case pos
α : 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 b : α
hab : P.Rel a b
h₁ : ¬∃ b, P.Rel a ↑b
h₂ : ∃ b_1, P.Rel b ↑b_1
⊢ P.rep ⋯ = f₀ h₂.choose
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case refine_3.inl
α : 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 : ↑t
ha : ↑a ∉ u
⊢ f ↑a = f₀ a

pp: case refine_3.inr
α : 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 : ↑t
ha : ↑a ∈ u
⊢ f ↑a = f₀ a

Tactic:
·

Goal state after:
case refine_3.inl
α : 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 : ↑t
ha : ↑a ∉ u
⊢ f ↑a = f₀ a
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case pos
α : 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 : ↑t
ha : ↑a ∈ u
h : ∃ b, P.Rel ↑a ↑b
⊢ f₀ h.choose = f₀ a

pp: case neg
α : 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 : ↑t
ha : ↑a ∈ u
h : ¬∃ b, P.Rel ↑a ↑b
⊢ P.rep ⋯ = f₀ a

Tactic:
·

Goal state after:
case pos
α : 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 : ↑t
ha : ↑a ∈ u
h : ∃ b, P.Rel ↑a ↑b
⊢ f₀ h.choose = f₀ a
Module: Mathlib.Order.SuccPred.Tree

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

pp: case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n✝ : ℕ
h : Nat.find ⋯ = n✝ + 1
⊢ Order.pred (Order.pred^[n✝ + 1 - 1] r) = ⊥

Tactic:
·

Goal state after:
case zero
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Nat.find ⋯ = 0
⊢ Order.pred (Order.pred^[0 - 1] r) = ⊥
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n✝ : ℕ
h : Nat.find ⋯ = n✝ + 1
⊢ Order.pred (Order.pred^[n✝ + 1 - 1] r) = ⊥

Tactic:
·

Goal state after:
case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
n✝ : ℕ
h : Nat.find ⋯ = n✝ + 1
⊢ Order.pred (Order.pred^[n✝ + 1 - 1] r) = ⊥
Module: Mathlib.Order.SuccPred.Tree

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

pp: case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ ∀ b < findAtom r, b = ⊥

Tactic:
·

Goal state after:
case left
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ findAtom r ≠ ⊥
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ ∀ b < findAtom r, b = ⊥

Tactic:
·

Goal state after:
case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ ∀ b < findAtom r, b = ⊥
Module: Mathlib.Order.SuccPred.Tree

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

Tactic:
exact hr.1

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

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

pp: case inr
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
oh : t₁.root ≤ v₁ ⊓ v₂
⊢ t₁ = t₂

Tactic:
·

Goal state after:
case inl
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
oh : v₁ ⊓ v₂ < t₁.root
⊢ t₁ = t₂
Module: Mathlib.Order.Sublocale

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

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

Tactic:
·

Goal state after:
case mp
X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a : X
b : ↥S
h : S.restrictAux a ≤ b
⊢ a ≤ ↑b
Module: Mathlib.Order.Sublocale

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

Tactic:
·

Goal state after:
case mpr
X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a : X
b : ↥S
h : a ≤ ↑b
⊢ S.restrictAux a ≤ b
Module: Mathlib.Order.Types.Arithmetic

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

Tactic:
simp only [← type_lex_sum, (OrderIso.sumLexAssoc α β γ).type_congr]

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: case mp
X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
x : X
⊢ x ∈ range ⇑S.toNucleus → x ∈ ↑S

pp: case mpr
X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
x : X
⊢ x ∈ ↑S → x ∈ range ⇑S.toNucleus

Tactic:
·

Goal state after:
case mp
X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
x : X
⊢ x ∈ range ⇑S.toNucleus → x ∈ ↑S
Module: Mathlib.Order.Sublocale

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
x : X
⊢ x ∈ ↑S → x ∈ range ⇑S.toNucleus

Tactic:
·

Goal state after:
case mpr
X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
x : X
⊢ x ∈ ↑S → x ∈ range ⇑S.toNucleus
Module: Mathlib.Order.Sublocale

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

Tactic:
refine le_antisymm (le_sInf_iff.mpr (fun b h1 ↦ ?_)) le_apply

Goal state after:
X : Type u_1
inst✝ : Order.Frame X
n : Nucleus X
a : Set X
h : a ⊆ range ⇑n
b : X
h1 : b ∈ a
⊢ n (sInf a) ≤ b
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : j ≤ i
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)

pp: case inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)

Tactic:
·

Goal state after:
case inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : j ≤ i
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)

Tactic:
·

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet (Set.Ioc n (n + 1) ×ˢ s)

pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ {n + 1} = Set.Ioc n (n + 1)

Tactic:
·

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableSet (Set.Ioc n (n + 1) ×ˢ s)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ {n + 1} = Set.Ioc n (n + 1)

Tactic:
·

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ {n + 1} = Set.Ioc n (n + 1)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet ({⊥} ×ˢ A)

pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (Set.Ioi i ×ˢ A)

Tactic:
·

Goal state after:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet ({⊥} ×ˢ A)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet ∅

pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' {⊥} ×ˢ A = ∅

Tactic:
·

Goal state after:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet ∅
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' {⊥} ×ˢ A = ∅

Tactic:
·

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' {⊥} ×ˢ A = ∅
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (Set.Ioi i ×ˢ A)

Tactic:
·

Goal state after:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (Set.Ioi i ×ˢ A)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inr.inl
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
⊢ MeasurableSet ((fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A)

pp: case inr.inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ MeasurableSet ((fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A)

Tactic:
·

Goal state after:
case inr.inl
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
⊢ MeasurableSet ((fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inr.inl
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
⊢ MeasurableSet ∅

pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A = ∅

Tactic:
·

Goal state after:
case inr.inl
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
⊢ MeasurableSet ∅
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A = ∅

Tactic:
·

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A = ∅
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inr.inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ MeasurableSet ((fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A)

Tactic:
·

Goal state after:
case inr.inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ MeasurableSet ((fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inr.inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ MeasurableSet ({⟨n + 1, ⋯⟩} ×ˢ A)

pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A = {⟨n + 1, ⋯⟩} ×ˢ A

Tactic:
·

Goal state after:
case inr.inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ MeasurableSet ({⟨n + 1, ⋯⟩} ×ˢ A)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A = {⟨n + 1, ⋯⟩} ×ˢ A

Tactic:
·

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A = {⟨n + 1, ⋯⟩} ×ˢ A
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inr.inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ MeasurableSet ((fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A)

Tactic:
· rw [(_ : (fun (p : Set.singleton (n + 1) × Ω) ↦ ((p.1 : ℕ), p.2)) ⁻¹' (Set.Ioi i ×ˢ A)
          = {⟨n + 1, rfl⟩} ×ˢ A)]
      · exact MeasurableSet.prod (MeasurableSet.of_subtype_image trivial) (𝓕.mono hin _ hA)
      · ext p
        simp only [Set.mem_preimage, Set.mem_prod, Set.mem_Ioi, Set.mem_singleton_iff,
          and_congr_left_iff]
        intro hp2
        rw [p.1.2]
        exact ⟨fun _ ↦ by aesop, fun _ ↦ lt_add_one_iff.2 hin⟩

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

Goal state before:
pp: case inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
m' : MeasurableSpace (ι × Ω)
hm'bot : ∀ (A : Set Ω), MeasurableSet A → MeasurableSet ({⊥} ×ˢ A)
hm' : ∀ (i : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i ×ˢ A)
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet ({⊥} ×ˢ A)

pp: case inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
m' : MeasurableSpace (ι × Ω)
hm'bot : ∀ (A : Set Ω), MeasurableSet A → MeasurableSet ({⊥} ×ˢ A)
hm' : ∀ (i : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i ×ˢ A)
i : ι
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet (Set.Ioi i ×ˢ A)

Tactic:
·

Goal state after:
case inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
m' : MeasurableSpace (ι × Ω)
hm'bot : ∀ (A : Set Ω), MeasurableSet A → MeasurableSet ({⊥} ×ˢ A)
hm' : ∀ (i : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i ×ˢ A)
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet ({⊥} ×ˢ A)