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

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y

Tactic:
·

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y
Module: Mathlib.Order.Basic

Goal state before:
pp: case refine_2.inl
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y

pp: case refine_2.inr
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y

Tactic:
·

Goal state after:
case refine_2.inl
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y
Module: Mathlib.Order.Basic

Goal state before:
pp: case refine_2.inr
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y

Tactic:
·

Goal state after:
case refine_2.inr
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y
Module: Mathlib.Order.Basic

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst < b.fst
h₂ : a.snd ≤ b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)

pp: case inr
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)

Tactic:
·

Goal state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst < b.fst
h₂ : a.snd ≤ b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
Module: Mathlib.Order.Basic

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)

Tactic:
·

Goal state after:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: case pos
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : LE α
H : ∀ (a : α), ∃ b, ¬b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α

pp: case neg
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : LE α
H : ∃ a, ∀ (b : α), b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α

Tactic:
·

Goal state after:
case pos
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : LE α
H : ∀ (a : α), ∃ b, ¬b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: case neg
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : LE α
H : ∃ a, ∀ (b : α), b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α

Tactic:
·

Goal state after:
case neg
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : LE α
H : ∃ a, ∀ (b : α), b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} ↦ next)
x y : C n
H : leRecOn ⋯ (fun {k} ↦ next) x = leRecOn ⋯ (fun {k} ↦ next) y
⊢ x = y

Tactic:
leRecOn_succ hnm,

Goal state after:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} ↦ next)
x y : C n
H : next (leRecOn hnm (fun {k} ↦ next) x) = leRecOn ⋯ (fun {k} ↦ next) y
⊢ x = y
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
⊢ Injective (leRecOn hnm fun {k} ↦ next)

Tactic:
induction hnm with
  | refl =>
    intro x y H
    rwa [leRecOn_self, leRecOn_self] at H
  | step hnm ih =>
    intro x y H
    rw [leRecOn_succ hnm, leRecOn_succ hnm] at H
    exact ih (Hnext _ H)

Goal state after:
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case inl
n m : ℕ
h : n ≤ m
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

pp: case inr
n m : ℕ
h : m < n
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
·

Goal state after:
case inl
n m : ℕ
h : n ≤ m
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case inr
n m : ℕ
h : m < n
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
·

Goal state after:
case inr
n m : ℕ
h : m < n
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case inr.inl
n : ℕ
h : 0 < n
⊢ n ∣ n - 0 ↔ 0 = 0 ∨ n ≤ 0

pp: case inr.inr
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
·

Goal state after:
case inr.inl
n : ℕ
h : 0 < n
⊢ n ∣ n - 0 ↔ 0 = 0 ∨ n ≤ 0
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case inr.inr
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
·

Goal state after:
case inr.inr
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case inl
n m : ℕ
h : m ≤ n
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n

pp: case inr
n m : ℕ
h : n < m
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n

Tactic:
·

Goal state after:
case inl
n m : ℕ
h : m ≤ n
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case inr
n m : ℕ
h : n < m
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n

Tactic:
·

Goal state after:
case inr
n m : ℕ
h : n < m
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case succ.inl
b : ℕ
ha : 0 ≠ 1
⊢ 0 * (b + 1) ≤ 0 ^ (b + 1)

pp: case succ.inr
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
⊢ a * (b + 1) ≤ a ^ (b + 1)

Tactic:
·

Goal state after:
case succ.inl
b : ℕ
ha : 0 ≠ 1
⊢ 0 * (b + 1) ≤ 0 ^ (b + 1)
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case succ.inr
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
⊢ a * (b + 1) ≤ a ^ (b + 1)

Tactic:
·

Goal state after:
case succ.inr
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
⊢ a * (b + 1) ≤ a ^ (b + 1)
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case inl
⊢ 2 * 0 ^ 2 + 1 ≤ 2 ^ (2 * 0)

pp: case inr
k : ℕ
hk : k > 0
⊢ 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)

Tactic:
·

Goal state after:
case inl
⊢ 2 * 0 ^ 2 + 1 ≤ 2 ^ (2 * 0)
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case inr
k : ℕ
hk : k > 0
⊢ 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)

Tactic:
·

Goal state after:
case inr
k : ℕ
hk : k > 0
⊢ 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case a
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ P (a + 1) b

pp: case a
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ P a (b + 1)

Tactic:
·

Goal state after:
case a
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ P (a + 1) b
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case a.inl
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a : ℕ
h : a + 1 < a + 1 + 1
⊢ P (a + 1) (a + 1)

pp: case a.inr
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h✝ : a + 1 < b + 1
h : a + 1 < b
⊢ P (a + 1) b

Tactic:
·

Goal state after:
case a.inl
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a : ℕ
h : a + 1 < a + 1 + 1
⊢ P (a + 1) (a + 1)
Module: Mathlib.Order.Compare

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LT α
a b : α
⊢ lt.swap.Compares a b ↔ lt.Compares b a

pp: case eq
α : Type u_1
inst✝ : LT α
a b : α
⊢ eq.swap.Compares a b ↔ eq.Compares b a

pp: case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.swap.Compares a b ↔ gt.Compares b a

Tactic:
·

Goal state after:
case lt
α : Type u_1
inst✝ : LT α
a b : α
⊢ lt.swap.Compares a b ↔ lt.Compares b a
Module: Mathlib.Order.Compare

Goal state before:
pp: case eq
α : Type u_1
inst✝ : LT α
a b : α
⊢ eq.swap.Compares a b ↔ eq.Compares b a

pp: case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.swap.Compares a b ↔ gt.Compares b a

Tactic:
·

Goal state after:
case eq
α : Type u_1
inst✝ : LT α
a b : α
⊢ eq.swap.Compares a b ↔ eq.Compares b a
Module: Mathlib.Order.Compare

Goal state before:
pp: case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.swap.Compares a b ↔ gt.Compares b a

Tactic:
·

Goal state after:
case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.swap.Compares a b ↔ gt.Compares b a
Module: Mathlib.Order.Compare

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a < b
⊢ o.Compares a b

pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a = b
⊢ o.Compares a b

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a < b
⊢ o.Compares a b
Module: Mathlib.Order.Compare

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a = b
⊢ o.Compares a b

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a = b
⊢ o.Compares a b
Module: Mathlib.Order.Compare

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case inl
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hac : r a c
⊢ r a c

pp: case inr.inl
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
hab : r a b
hbc : r b a
⊢ r a a

pp: case inr.inr
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hca : r c a
⊢ r a c

Tactic:
·

Goal state after:
case inl
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hac : r a c
⊢ r a c
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case inr.inl
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
hab : r a b
hbc : r b a
⊢ r a a

pp: case inr.inr
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hca : r c a
⊢ r a c

Tactic:
·

Goal state after:
case inr.inl
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
hab : r a b
hbc : r b a
⊢ r a a
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case inr.inr
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hca : r c a
⊢ r a c

Tactic:
·

Goal state after:
case inr.inr
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hca : r c a
⊢ r a c
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case ind.ind.inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst < (a', b).fst
hb : x.snd ≤ (a', b).snd
⊢ Acc (fun x1 x2 ↦ x1 < x2) x

pp: case ind.ind.inr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst ≤ (a', b).fst
hb : x.snd < (a', b).snd
⊢ Acc (fun x1 x2 ↦ x1 < x2) x

Tactic:
·

Goal state after:
case ind.ind.inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst < (a', b).fst
hb : x.snd ≤ (a', b).snd
⊢ Acc (fun x1 x2 ↦ x1 < x2) x
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case ind.ind.inr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst ≤ (a', b).fst
hb : x.snd < (a', b).snd
⊢ Acc (fun x1 x2 ↦ x1 < x2) x

Tactic:
·

Goal state after:
case ind.ind.inr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst ≤ (a', b).fst
hb : x.snd < (a', b).snd
⊢ Acc (fun x1 x2 ↦ x1 < x2) x
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : x = ⊤
⊢ ¬P x

pp: case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
⊢ ¬P x

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : x = ⊤
⊢ ¬P x
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
⊢ ¬P x

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
⊢ ¬P x
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case mp
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)

pp: case mpr
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g

Tactic:
·

Goal state after:
case mp
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case mpr
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g

Tactic:
·

Goal state after:
case mpr
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

pp: case neg
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : p x
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

pp: case neg
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : ¬p x
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : p x
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : ¬p x
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : ¬p x
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁

pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i

Tactic:
·

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i

Tactic:
·

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁

pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i

Tactic:
·

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i

Tactic:
·

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i