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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
⊢ (none.elim (h x y) fun j ↦ h (f j) (g j)) = h (none.elim x f) (none.elim y g)

pp: case some
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
val✝ : γ
⊢ ((some val✝).elim (h x y) fun j ↦ h (f j) (g j)) = h ((some val✝).elim x f) ((some val✝).elim y g)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
⊢ (none.elim (h x y) fun j ↦ h (f j) (g j)) = h (none.elim x f) (none.elim y g)

case some
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
val✝ : γ
⊢ ((some val✝).elim (h x y) fun j ↦ h (f j) (g j)) = h ((some val✝).elim x f) ((some val✝).elim y g)
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
val✝ : α
⊢ Sum.elim (a * a') (b * b') (inl val✝) = (Sum.elim a b * Sum.elim a' b') (inl val✝)

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
val✝ : β
⊢ Sum.elim (a * a') (b * b') (inr val✝) = (Sum.elim a b * Sum.elim a' b') (inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
val✝ : α
⊢ Sum.elim (a * a') (b * b') (inl val✝) = (Sum.elim a b * Sum.elim a' b') (inl val✝)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
val✝ : β
⊢ Sum.elim (a * a') (b * b') (inr val✝) = (Sum.elim a b * Sum.elim a' b') (inr val✝)
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
x₁ : α
y₁ : β
x₂ : α
y₂ : β
⊢ (x₁, y₁) = (x₂, y₂) → ⦃P : Sort u_5⦄ → (x₁ = x₂ → y₁ = y₂ → P) → P

Tactic:
intros h P w
  cases h
  exact w rfl rfl

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
val✝ : α
⊢ Sum.elim (a / a') (b / b') (inl val✝) = (Sum.elim a b / Sum.elim a' b') (inl val✝)

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
val✝ : β
⊢ Sum.elim (a / a') (b / b') (inr val✝) = (Sum.elim a b / Sum.elim a' b') (inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
val✝ : α
⊢ Sum.elim (a / a') (b / b') (inl val✝) = (Sum.elim a b / Sum.elim a' b') (inl val✝)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
val✝ : β
⊢ Sum.elim (a / a') (b / b') (inr val✝) = (Sum.elim a b / Sum.elim a' b') (inr val✝)
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
f : α → α
g : β → β
⊢ (map f g)^[0] = map f^[0] g^[0]

pp: case succ
α : Type u_1
β : Type u_2
f : α → α
g : β → β
n✝ : ℕ
a✝ : (map f g)^[n✝] = map f^[n✝] g^[n✝]
⊢ (map f g)^[n✝ + 1] = map f^[n✝ + 1] g^[n✝ + 1]

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
f : α → α
g : β → β
⊢ (map f g)^[0] = map f^[0] g^[0]

case succ
α : Type u_1
β : Type u_2
f : α → α
g : β → β
n✝ : ℕ
a✝ : (map f g)^[n✝] = map f^[n✝] g^[n✝]
⊢ (map f g)^[n✝ + 1] = map f^[n✝ + 1] g^[n✝ + 1]
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
i : α
a : β
h : r i i
⊢ False

pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
i : α
a : β
h : s a a
⊢ False

Tactic:
<;>

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
i : α
a : β
h : r i i
⊢ False

case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
i : α
a : β
h : s a a
⊢ False
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ min a b = if b ≤ a then b else a

pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ min a b = if b ≤ a then b else a

pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b < a
⊢ min a b = if b ≤ a then b else a

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ min a b = if b ≤ a then b else a

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ min a b = if b ≤ a then b else a

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b < a
⊢ min a b = if b ≤ a then b else a
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ max a b = if b ≤ a then a else b

pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ max a b = if b ≤ a then a else b

pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b < a
⊢ max a b = if b ≤ a then a else b

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ max a b = if b ≤ a then a else b

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ max a b = if b ≤ a then a else b

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b < a
⊢ max a b = if b ≤ a then a else b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a ≤ a

pp: case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b ≤ a

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a ≤ a

case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b ≤ a
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a ≤ b

pp: case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b ≤ b

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a ≤ b

case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b ≤ b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h✝ : a ≤ b
⊢ c ≤ a

pp: case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h✝ : ¬a ≤ b
⊢ c ≤ b

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h✝ : a ≤ b
⊢ c ≤ a

case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h✝ : ¬a ≤ b
⊢ c ≤ b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
h✝ : b ≤ c
⊢ a < min b c

pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
h✝ : c ≤ b
⊢ a < min b c

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
h✝ : b ≤ c
⊢ a < min b c

case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
h✝ : c ≤ b
⊢ a < min b c
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ Ordering.lt.Compares a b

pp: case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ Ordering.eq.Compares a b

pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ Ordering.gt.Compares a b

Tactic:
<;>

Goal state after:
case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ Ordering.lt.Compares a b

case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ Ordering.eq.Compares a b

case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ Ordering.gt.Compares a b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ c a b : α
h✝ : compare b a = Ordering.lt
⊢ compare a b = Ordering.lt.swap

pp: case eq
α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ c a b : α
h✝ : compare b a = Ordering.eq
⊢ compare a b = Ordering.eq.swap

pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ c a b : α
h✝ : compare b a = Ordering.gt
⊢ compare a b = Ordering.gt.swap

Tactic:
<;>

Goal state after:
case lt
α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ c a b : α
h✝ : compare b a = Ordering.lt
⊢ compare a b = Ordering.lt.swap

case eq
α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ c a b : α
h✝ : compare b a = Ordering.eq
⊢ compare a b = Ordering.eq.swap

case gt
α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ c a b : α
h✝ : compare b a = Ordering.gt
⊢ compare a b = Ordering.gt.swap
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: case refl
α : Sort u
β β' : Sort v
h' : ∀ (a : α), β = β'
⊢ ((x : α) → (fun x ↦ β) x) = (α → β')

Tactic:
rw [funext h']

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬a ≤ b ∨ ¬¬b ≤ a ↔ ¬a ≤ b ∨ b ≤ a

Tactic:
Classical.not_not

Goal state after:
α : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬a ≤ b ∨ b ≤ a ↔ ¬a ≤ b ∨ b ≤ a
Module: Mathlib.Order.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
hab : a ≤ b
⊢ p (min a b)

pp: case inr
α : Type u_2
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
hba : b ≤ a
⊢ p (min a b)

Tactic:
<;>

Goal state after:
case inl
α : Type u_2
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
hab : a ≤ b
⊢ p (min a b)

case inr
α : Type u_2
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
hba : b ≤ a
⊢ p (min a b)
Module: Mathlib.Order.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
⊢ False

pp: case inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
⊢ False

Tactic:
<;>

Goal state after:
case inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
⊢ False

case inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case inl.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
⊢ False

pp: case inl.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
⊢ False

pp: case inr.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
⊢ False

pp: case inr.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
⊢ False

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
⊢ False

case inl.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
⊢ False

case inr.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
⊢ False

case inr.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
⊢ False
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: case false
⊢ (false.toNat == 1) = false

pp: case true
⊢ (true.toNat == 1) = true

Tactic:
<;>

Goal state after:
case false
⊢ (false.toNat == 1) = false

case true
⊢ (true.toNat == 1) = true
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: case false
b₁ : Bool
h : false ≤ b₁
⊢ false.toNat ≤ b₁.toNat

pp: case true
b₁ : Bool
h : true ≤ b₁
⊢ true.toNat ≤ b₁.toNat

Tactic:
<;>

Goal state after:
case false
b₁ : Bool
h : false ≤ b₁
⊢ false.toNat ≤ b₁.toNat

case true
b₁ : Bool
h : true ≤ b₁
⊢ true.toNat ≤ b₁.toNat
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: case false.false
h : false ≤ false
⊢ false.toNat ≤ false.toNat

pp: case false.true
h : false ≤ true
⊢ false.toNat ≤ true.toNat

pp: case true.false
h : true ≤ false
⊢ true.toNat ≤ false.toNat

pp: case true.true
h : true ≤ true
⊢ true.toNat ≤ true.toNat

Tactic:
<;>

Goal state after:
case false.false
h : false ≤ false
⊢ false.toNat ≤ false.toNat

case false.true
h : false ≤ true
⊢ false.toNat ≤ true.toNat

case true.false
h : true ≤ false
⊢ true.toNat ≤ false.toNat

case true.true
h : true ≤ true
⊢ true.toNat ≤ true.toNat
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: case false
f : Bool → Bool
x : Bool
h₁ : f true = false
⊢ f (f (f x)) = f x

pp: case true
f : Bool → Bool
x : Bool
h₁ : f true = true
⊢ f (f (f x)) = f x

Tactic:
<;>

Goal state after:
case false
f : Bool → Bool
x : Bool
h₁ : f true = false
⊢ f (f (f x)) = f x

case true
f : Bool → Bool
x : Bool
h₁ : f true = true
⊢ f (f (f x)) = f x
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: case false.false
f : Bool → Bool
x : Bool
h₁ : f true = false
h₂ : f false = false
⊢ f (f (f x)) = f x

pp: case false.true
f : Bool → Bool
x : Bool
h₁ : f true = false
h₂ : f false = true
⊢ f (f (f x)) = f x

pp: case true.false
f : Bool → Bool
x : Bool
h₁ : f true = true
h₂ : f false = false
⊢ f (f (f x)) = f x

pp: case true.true
f : Bool → Bool
x : Bool
h₁ : f true = true
h₂ : f false = true
⊢ f (f (f x)) = f x

Tactic:
<;>

Goal state after:
case false.false
f : Bool → Bool
x : Bool
h₁ : f true = false
h₂ : f false = false
⊢ f (f (f x)) = f x

case false.true
f : Bool → Bool
x : Bool
h₁ : f true = false
h₂ : f false = true
⊢ f (f (f x)) = f x

case true.false
f : Bool → Bool
x : Bool
h₁ : f true = true
h₂ : f false = false
⊢ f (f (f x)) = f x

case true.true
f : Bool → Bool
x : Bool
h₁ : f true = true
h₂ : f false = true
⊢ f (f (f x)) = f x
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: case isTrue
α : Type u
inst✝¹ : Top α
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
ha : ∀ (h : p), a h ≠ ⊤
hb : ∀ (h : ¬p), b h ≠ ⊤
h✝ : p
⊢ a h✝ ≠ ⊤

pp: case isFalse
α : Type u
inst✝¹ : Top α
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
ha : ∀ (h : p), a h ≠ ⊤
hb : ∀ (h : ¬p), b h ≠ ⊤
h✝ : ¬p
⊢ b h✝ ≠ ⊤

Tactic:
<;>

Goal state after:
case isTrue
α : Type u
inst✝¹ : Top α
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
ha : ∀ (h : p), a h ≠ ⊤
hb : ∀ (h : ¬p), b h ≠ ⊤
h✝ : p
⊢ a h✝ ≠ ⊤

case isFalse
α : Type u
inst✝¹ : Top α
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
ha : ∀ (h : p), a h ≠ ⊤
hb : ∀ (h : ¬p), b h ≠ ⊤
h✝ : ¬p
⊢ b h✝ ≠ ⊤
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: case e_toOrderTop
α : Type u
β : Type v
inst✝ : PartialOrder α
toOrderTop✝¹ : OrderTop α
toOrderBot✝¹ : OrderBot α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
⊢ toOrderTop✝¹ = toOrderTop✝

pp: case e_toOrderBot
α : Type u
β : Type v
inst✝ : PartialOrder α
toOrderTop✝¹ : OrderTop α
toOrderBot✝¹ : OrderBot α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
⊢ toOrderBot✝¹ = toOrderBot✝

Tactic:
<;>

Goal state after:
case e_toOrderTop
α : Type u
β : Type v
inst✝ : PartialOrder α
toOrderTop✝¹ : OrderTop α
toOrderBot✝¹ : OrderBot α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
⊢ toOrderTop✝¹ = toOrderTop✝

case e_toOrderBot
α : Type u
β : Type v
inst✝ : PartialOrder α
toOrderTop✝¹ : OrderTop α
toOrderBot✝¹ : OrderBot α
toOrderTop✝ : OrderTop α
toOrderBot✝ : OrderBot α
⊢ toOrderBot✝¹ = toOrderBot✝
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case inr.inr.refine_1
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ 0 < n - m

pp: case inr.inr.refine_2
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ n - m < n

Tactic:
<;>

Goal state after:
case inr.inr.refine_1
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ 0 < n - m

case inr.inr.refine_2
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ n - m < n
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n : ℕ
⊢ ¬0 = 1

pp: m n : ℕ
⊢ 1 < 2

Tactic:
<;>

Goal state after:
m n : ℕ
⊢ ¬0 = 1

m n : ℕ
⊢ 1 < 2
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case zero
motive : (m : ℕ) → 0 ≤ m → Sort u_1
refl : motive 0 ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : 0 ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec refl le_succ_of_le ⋯ = refl

pp: case succ
n✝ : ℕ
motive : (m : ℕ) → n✝ + 1 ≤ m → Sort u_1
refl : motive (n✝ + 1) ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n✝ + 1 ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec refl le_succ_of_le ⋯ = refl

Tactic:
<;>

Goal state after:
case zero
motive : (m : ℕ) → 0 ≤ m → Sort u_1
refl : motive 0 ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : 0 ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec refl le_succ_of_le ⋯ = refl

case succ
n✝ : ℕ
motive : (m : ℕ) → n✝ + 1 ≤ m → Sort u_1
refl : motive (n✝ + 1) ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n✝ + 1 ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec refl le_succ_of_le ⋯ = refl
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case refl
m n k : ℕ
hmn : m ≤ n
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
⊢ decreasingInduction of_succ self ⋯ =
    decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self ⋯) hmn

Tactic:
rw [decreasingInduction_self]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case pos
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : x ≤ y
⊢ (cmpLE x y).swap = cmpLE y x

pp: case neg
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : ¬x ≤ y
⊢ (cmpLE x y).swap = cmpLE y x

Tactic:
<;>

Goal state after:
case pos
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : x ≤ y
⊢ (cmpLE x y).swap = cmpLE y x

case neg
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : ¬x ≤ y
⊢ (cmpLE x y).swap = cmpLE y x
Module: Mathlib.Order.Compare

Goal state before:
pp: case pos
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : x ≤ y
yx : y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x

pp: case neg
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : x ≤ y
yx : ¬y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x

pp: case pos
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : ¬x ≤ y
yx : y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x

pp: case neg
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x

Tactic:
<;>

Goal state after:
case pos
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : x ≤ y
yx : y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x

case neg
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : x ≤ y
yx : ¬y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x

case pos
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : ¬x ≤ y
yx : y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x

case neg
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x
Module: Mathlib.Order.Compare

Goal state before:
pp: case pos
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : x ≤ y
⊢ cmpLE x y = cmp x y

pp: case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : ¬x ≤ y
⊢ cmpLE x y = cmp x y

Tactic:
<;>

Goal state after:
case pos
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : x ≤ y
⊢ cmpLE x y = cmp x y

case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : ¬x ≤ y
⊢ cmpLE x y = cmp x y
Module: Mathlib.Order.Compare

Goal state before:
pp: case pos
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : x ≤ y
yx : y ≤ x
⊢ cmpLE x y = cmp x y

pp: case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : x ≤ y
yx : ¬y ≤ x
⊢ cmpLE x y = cmp x y

pp: case pos
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : y ≤ x
⊢ cmpLE x y = cmp x y

pp: case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ cmpLE x y = cmp x y

Tactic:
<;>

Goal state after:
case pos
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : x ≤ y
yx : y ≤ x
⊢ cmpLE x y = cmp x y

case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : x ≤ y
yx : ¬y ≤ x
⊢ cmpLE x y = cmp x y

case pos
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : y ≤ x
⊢ cmpLE x y = cmp x y

case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ cmpLE x y = cmp x y
Module: Mathlib.Order.Compare

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (cmp a b).Compares a b

pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ (cmp a b).Compares a b

pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b < a
⊢ (cmp a b).Compares a b

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (cmp a b).Compares a b

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ (cmp a b).Compares a b

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b < a
⊢ (cmp a b).Compares a b
Module: Mathlib.Order.Compare

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : a < b
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : ¬a < b
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : a < b
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
h : ¬a < b
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq