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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
b : β
⊢ f₁ (f₂ b) = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
⊢ g₁ (g₂ d) = d

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
⊢ motive (min a b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb : a ≤ b → motive b
⊢ motive (max a b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ min a b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ min a b ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min a (min b c) = min b (min a c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ min a a = a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ b < a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b ≠ Ordering.gt ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b ≠ Ordering.lt ↔ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ cmp a b = compare a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ c a b : α
⊢ compare a b = (compare b a).swap

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c a✝ b✝ c✝ : α
h₁ : (compare a✝ b✝).isLE = true
h₂ : (compare b✝ c✝).isLE = true
⊢ (compare a✝ c✝).isLE = true

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ∀ {a b : α}, compare a b = Ordering.eq ↔ (a == b) = true

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ∀ {x y : α}, compare x y = Ordering.lt ↔ x < y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ∀ {x y : α}, (compare x y).isLE = true ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Lean.Meta.CongrTheorems

Goal state before:
pp: α β : Sort u
inst✝ : FastSubsingleton α
h₂ : α = β
a : α
b : β
⊢ a ≍ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α : Type u_1
inst✝ : LT α
T : Std.Trichotomous LT.lt
a b : αᵒᵈ
⊢ ¬a < b → ¬b < a → a = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝ : LinearOrder α
a b : αᵒᵈ
⊢ compare a b = compareOfLessAndEq a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α : Type u_1
a b : α
⊢ toDual a = toDual b ↔ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α : Type u_1
a b : αᵒᵈ
⊢ ofDual a = ofDual b ↔ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α : Type u_1
inst✝ : LT α
⊢ DenselyOrdered αᵒᵈ → DenselyOrdered α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder β
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMinOrder (π i)
a : (i : ι) → π i
⊢ ∃ b, b < a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : NoBotOrder α
a : α
⊢ ∃ b, b < a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝ : LE α
⊢ NoBotOrder α ↔ ∀ (x : α), ¬IsBot x

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CongrExclamation

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

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: α : Sort u_1
x y : α
p : x ≍ y → Prop
h : ∀ (he : x = y), p ⋯
he : x ≍ y
⊢ p he

Tactic:
by

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j = i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ NoMinOrder α ↔ ∀ (x : α), ¬IsMin x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ ¬IsMin a ↔ ∃ b, b < a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: x y : Prop
p : x = y → Prop
h : ∀ (he : x ↔ y), p ⋯
he : x = y
⊢ p he

Tactic:
by

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : Nontrivial α
ha : IsBot a
⊢ ¬IsMax a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.ULift

Goal state before:
pp: α : Type u_1
a b : α
x✝ : { down := a }.down = { down := b }.down
⊢ { down := a } = { down := b }

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.ULift

Goal state before:
pp: α : Type u_1
a b : ULift α
h : a = b
⊢ a.down = b.down

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.ULift

Goal state before:
pp: α : Sort u_1
a b : α
x✝ : { down := a }.down = { down := b }.down
⊢ { down := a } = { down := b }

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.ULift

Goal state before:
pp: α : Sort u_1
a b : PLift α
h : a = b
⊢ a.down = b.down

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.GCongr.Core

Goal state before:
pp: declName : Name
stx : Syntax
kind : AttributeKind
prio : Nat
strict forGrw : Bool
cinfo : ConstantInfo
xs : Array Expr
type : Expr
c : Name
us✝ : List Level
i✝ i : Nat
h : i + 1 ≤ xs.size
⊢ i < xs.size

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.GCongr.Core

Goal state before:
pp: declName : Name
stx : Syntax
kind : AttributeKind
prio : Nat
strict forGrw : Bool
cinfo : ConstantInfo
xs : Array Expr
type : Expr
c : Name
us✝ : List Level
i✝ i : Nat
h : i + 1 ≤ xs.size
⊢ i ≤ xs.size

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f a (f b c) ≤ f (f a b) c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x y x' y' : α
ltc : x < y ↔ x' < y'
gtc : y < x ↔ y' < x'
⊢ x = y ↔ x' = y'

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ min a b = if a < b then a else b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ max a b = if a < b then b else a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝ a a
le_trans✝¹ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
⊢ A_lt = B_lt

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
le✝¹ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝¹ a a
le_trans✝¹ : ∀ (a b c : α), le✝¹ a b → le✝¹ b c → le✝¹ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝¹ a b ∧ ¬le✝¹ b a
le✝ B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
⊢ { le := le✝¹, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := A_iff }.toLE =
      { le := le✝, lt := B_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := B_iff }.toLE →
    { le := le✝¹, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := A_iff } =
      { le := le✝, lt := B_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := B_iff }

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
⊢ Injective (@toPreorder α)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), A_le a a
le_trans✝ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm✝ : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total✝ : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge✝ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
B_min_def : ∀ (a b : α), B_min a b = if A_le a b then a else b
B_max_def : ∀ (a b : α), B_max a b = if A_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
⊢ A_min = B_min

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), A_le a a
le_trans✝ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm✝ : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total✝ : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge✝ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
B_max_def : ∀ (a b : α), B_max a b = if A_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
⊢ A_max = B_max

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), A_le a a
le_trans✝ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm✝ : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total✝ : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge✝ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
B_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
⊢ A_compare = B_compare

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_le B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), B_le a a
le_trans✝ : ∀ (a b c : α), B_le a b → B_le b c → B_le a c
lt_iff_le_not_ge✝ : ∀ (a b : α), B_lt a b ↔ B_le a b ∧ ¬B_le b a
le_antisymm✝ : ∀ (a b : α), B_le a b → B_le b a → a = b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_total✝ : ∀ (a b : α), B_le a b ∨ B_le b a
B_decidableLE : DecidableLE α
B_decidableEq : DecidableEq α
B_decidableLT : DecidableLT α
B_min_def : ∀ (a b : α), B_min a b = if B_le a b then a else b
B_max_def : ∀ (a b : α), B_max a b = if B_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
⊢ { le := A_le, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := lt_iff_le_not_ge✝¹,
          le_antisymm := le_antisymm✝¹, min := A_min, max := A_max, compare := A_compare, le_total := le_total✝¹,
          toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT,
          min_def := A_min_def, max_def := A_max_def,
          compare_eq_compareOfLessAndEq := A_compare_canonical }.toPartialOrder =
      { le := B_le, lt := B_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := lt_iff_le_not_ge✝,
          le_antisymm := le_antisymm✝, min := B_min, max := B_max, compare := B_compare, le_total := le_total✝,
          toDecidableLE := B_decidableLE, toDecidableEq := B_decidableEq, toDecidableLT := B_decidableLT,
          min_def := B_min_def, max_def := B_max_def,
          compare_eq_compareOfLessAndEq := B_compare_canonical }.toPartialOrder →
    { le := A_le, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := lt_iff_le_not_ge✝¹,
        le_antisymm := le_antisymm✝¹, min := A_min, max := A_max, compare := A_compare, le_total := le_total✝¹,
        toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT,
        min_def := A_min_def, max_def := A_max_def, compare_eq_compareOfLessAndEq := A_compare_canonical } =
      { le := B_le, lt := B_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := lt_iff_le_not_ge✝,
        le_antisymm := le_antisymm✝, min := B_min, max := B_max, compare := B_compare, le_total := le_total✝,
        toDecidableLE := B_decidableLE, toDecidableEq := B_decidableEq, toDecidableLT := B_decidableLT,
        min_def := B_min_def, max_def := B_max_def, compare_eq_compareOfLessAndEq := B_compare_canonical }

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A B : Preorder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
⊢ A = B

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A B : LinearOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 ↦ x1 < x2)ᶜ = fun x1 x2 ↦ x1 ≥ x2

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 ↦ x1 ≤ x2)ᶜ = fun x1 x2 ↦ x1 > x2

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 ↦ x1 > x2)ᶜ = fun x1 x2 ↦ x1 ≤ x2

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 ↦ x1 ≥ x2)ᶜ = fun x1 x2 ↦ x1 < x2

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
⊢ IsEquiv α (fun x1 x2 ↦ x1 ≠ x2)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
π : ι → Type u_4
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
⊢ x < y ↔ x ≤ y ∧ ∃ i, x i < y i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
a b : (i : ι) → π i
inst✝ : Nonempty ι
h : a ≺ b
⊢ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
π : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ update x i a ≤ update y i b ↔ a ≤ b ∧ ∀ (j : ι), j ≠ i → x j ≤ y j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
π : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x : (i : ι) → π i
i : ι
a b : π i
⊢ update x i a ≤ update x i b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
π : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x : (i : ι) → π i
i : ι
a : π i
⊢ x ≤ update x i a ↔ x i ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
π : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x : (i : ι) → π i
i : ι
a : π i
⊢ x < update x i a ↔ x i < a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ const β a ≤ const β b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ const β a < const β b ↔ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝² : Preorder β
inst✝¹ : LE α
inst✝ : LT α
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
x✝¹ x✝ : α
⊢ x✝¹ < x✝ ↔ x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ x✝¹ ≤ x✝ ∨ x✝ ≤ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ x✝¹ ⊓ x✝ = if x✝¹ ≤ x✝ then x✝¹ else x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ x✝¹ ⊔ x✝ = if x✝¹ ≤ x✝ then x✝ else x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝⁸ : LinearOrder β
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Max α
inst✝⁴ : Min α
inst✝³ : Ord α
inst✝² : DecidableEq α
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x✝¹ x✝ : α
⊢ Ord.compare x✝¹ x✝ = compareOfLessAndEq x✝¹ x✝

Tactic:
by

Goal state after: