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

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b / c ↔ c * a < b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b / c < a ↔ b < c * a

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
⊢ a < b / c ↔ c < b / a

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) ↔ WellFounded r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
⊢ a / b < c ↔ a / c < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
e : f a = f b
h : r a b
⊢ s (f a) (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
e : f a = f b
h : r b a
⊢ s (f b) (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
⊢ r ↪r s

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
⊢ ∀ {a b : α ⊕ γ},
    Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } a) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } b) ↔
      Sum.LiftRel r t a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.OrderIso

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a : α
⊢ (mulRight a).symm = mulRight a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Group.OrderIso

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a : α
⊢ (mulLeft a).symm = mulLeft a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Order.Lex

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Lex

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Lex

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Lex

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ (x - a) * (x - b) ≤ 0 ↔ a ≤ x ∧ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
⊢ ∀ {a b : α ⊕ γ},
    Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } a) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } b) ↔ Sum.Lex r t a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
s : β → β → Prop
a : α
h : ¬r a a
⊢ ∀ {a_1 b : β}, Prod.Lex r s ({ toFun := Prod.mk a, inj' := ⋯ } a_1) ({ toFun := Prod.mk a, inj' := ⋯ } b) ↔ s a_1 b

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
b : β
h : ¬s b b
⊢ ∀ {a b_1 : α},
    Prod.Lex r s ({ toFun := fun a ↦ (a, b), inj' := ⋯ } a) ({ toFun := fun a ↦ (a, b), inj' := ⋯ } b_1) ↔ r a b_1

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
⊢ ∀ {a b : α × γ},
    Prod.Lex s u ({ toFun := Prod.map ⇑f ⇑g, inj' := ⋯ } a) ({ toFun := Prod.map ⇑f ⇑g, inj' := ⋯ } b) ↔
      Prod.Lex r t a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ 0 < (x - a) * (x - b) ↔ x < a ∨ b < x

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e₁ : α ≃ β
o₁ : ∀ {a b : α}, s (e₁ a) (e₁ b) ↔ r a b
e₂ : α ≃ β
map_rel_iff'✝ : ∀ {a b : α}, s (e₂ a) (e₂ b) ↔ r a b
h : { toEquiv := e₁, map_rel_iff' := o₁ }.toEquiv = { toEquiv := e₂, map_rel_iff' := map_rel_iff'✝ }.toEquiv
⊢ { toEquiv := e₁, map_rel_iff' := o₁ } = { toEquiv := e₂, map_rel_iff' := map_rel_iff'✝ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ (x - a) * (x - b) < 0 ↔ a < x ∧ x < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ≃r s
a b : β
⊢ r (f.symm a) (f.symm b) ↔ s a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ ∀ (x : β), (e.symm.trans e) x = (RelIso.refl s) x

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ ∀ (x : α), (e.trans e.symm) x = (RelIso.refl r) x

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
h₁ : α = β
h₂ : r ≍ s
a b : α
⊢ s ((Equiv.cast h₁) a) ((Equiv.cast h₁) b) ↔ r a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α β γ : Type u
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
h₁ : α = β
h₁' : β = γ
h₂ : r ≍ s
h₂' : s ≍ t
x : α
⊢ ((RelIso.cast h₁ h₂).trans (RelIso.cast h₁' h₂')) x = (RelIso.cast ⋯ ⋯) x

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : α
y : β
⊢ r x (e.symm y) ↔ s (e x) y

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : β
y : α
⊢ r (e.symm x) y ↔ s x (e y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
e : r ≃r s
f : α → β
g : β → α
hf : f = ⇑e
hg : g = ⇑e.symm
x✝ : α
⊢ g (f x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
e : r ≃r s
f : α → β
g : β → α
hf : f = ⇑e
hg : g = ⇑e.symm
x✝ : β
⊢ f (g x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
e : r ≃r s
f : α → β
g : β → α
hf : f = ⇑e
hg : g = ⇑e.symm
⊢ ∀ {a b : α},
    s ({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a)
        ({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b) ↔
      r a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝ : r ≃r s
⊢ (fun f ↦ ofSurjective ↑f ⋯) ((fun f ↦ ⟨f.toRelEmbedding, ⋯⟩) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ →r s₁
⊢ (fun f₂ ↦ e₂.symm.toRelEmbedding.toRelHom.comp (f₂.comp e₁.toRelEmbedding.toRelHom))
      ((fun f₁ ↦ e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom)) f₁) =
    f₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ →r s₂
⊢ (fun f₁ ↦ e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom))
      ((fun f₂ ↦ e₂.symm.toRelEmbedding.toRelHom.comp (f₂.comp e₁.toRelEmbedding.toRelHom)) f₂) =
    f₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ ↪r s₁
⊢ (fun f₂ ↦ (e₁.toRelEmbedding.trans f₂).trans e₂.symm.toRelEmbedding)
      ((fun f₁ ↦ (e₁.symm.toRelEmbedding.trans f₁).trans e₂.toRelEmbedding) f₁) =
    f₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ ↪r s₂
⊢ (fun f₁ ↦ (e₁.symm.toRelEmbedding.trans f₁).trans e₂.toRelEmbedding)
      ((fun f₂ ↦ (e₁.toRelEmbedding.trans f₂).trans e₂.symm.toRelEmbedding) f₂) =
    f₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ ≃r s₁
⊢ (fun f₂ ↦ (e₁.trans f₂).trans e₂.symm) ((fun f₁ ↦ (e₁.symm.trans f₁).trans e₂) f₁) = f₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ ≃r s₂
⊢ (fun f₁ ↦ (e₁.symm.trans f₁).trans e₂) ((fun f₂ ↦ (e₁.trans f₂).trans e₂.symm) f₂) = f₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r s₁
e₂ : r₂ ≃r s₂
a b : α₁ ⊕ α₂
⊢ Sum.Lex s₁ s₂ ((e₁.sumCongr e₂.toEquiv) a) ((e₁.sumCongr e₂.toEquiv) b) ↔ Sum.Lex r₁ r₂ a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r s₁
e₂ : r₂ ≃r s₂
⊢ ∀ {a b : α₁ × α₂}, Prod.Lex s₁ s₂ ((e₁.prodCongr e₂.toEquiv) a) ((e₁.prodCongr e₂.toEquiv) b) ↔ Prod.Lex r₁ r₂ a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝ : IsEmpty β
⊢ ∀ {a b : α ⊕ β}, r ((Equiv.sumEmpty α β) a) ((Equiv.sumEmpty α β) b) ↔ Sum.Lex r s a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝ : IsEmpty α
⊢ ∀ {a b : α ⊕ β}, s ((Equiv.emptySum α β) a) ((Equiv.emptySum α β) b) ↔ Sum.Lex r s a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
f : α ↪ β
a b : α
⊢ Relation.Map r (⇑f) (⇑f) (f a) (f b) ↔ r a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : β → β → Prop
f : α ↪ β
⊢ ∀ {a b : α}, r (f a) (f b) ↔ (r on ⇑f) a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x1 ≤ x2) ↪r fun x1 x2 ↦ x1 ≤ x2
⊢ ∀ {a b : α}, i.toEmbedding b ≤ i.toEmbedding a ↔ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x2 ≤ x1) ↪r fun x1 x2 ↦ x2 ≤ x1
⊢ ∀ {a b : α}, i.toEmbedding a ≤ i.toEmbedding b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x1 ≤ x2) ≃r fun x1 x2 ↦ x1 ≤ x2
⊢ ∀ {a b : α}, i.toEquiv b ≤ i.toEquiv a ↔ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x2 ≤ x1) ≃r fun x1 x2 ↦ x2 ≤ x1
⊢ ∀ {a b : α}, i.toEquiv a ≤ i.toEquiv b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_6
α : Type u_7
β : Type u_8
inst✝² : LE α
inst✝¹ : LE β
inst✝ : FunLike F α β
⊢ (RelHomClass F (fun x1 x2 ↦ x1 ≤ x2) fun x1 x2 ↦ x1 ≤ x2) = RelHomClass F (fun x1 x2 ↦ x2 ≤ x1) fun x1 x2 ↦ x2 ≤ x1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ EquivLike.inv f b ≤ a ↔ b ≤ f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a b : β
⊢ EquivLike.inv f b ≤ EquivLike.inv f a ↔ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ EquivLike.inv f b < a ↔ b < f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a b : β
⊢ EquivLike.inv f b < EquivLike.inv f a ↔ b < a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f g : α →o β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
⊢ ∀ {a b : α × β →o γ},
    { toFun := fun f ↦ { toFun := fun x ↦ { toFun := Function.curry (⇑f) x, monotone' := ⋯ }, monotone' := ⋯ },
            invFun := fun f ↦ { toFun := Function.uncurry fun x ↦ ⇑(f x), monotone' := ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }
          a ≤
        { toFun := fun f ↦ { toFun := fun x ↦ { toFun := Function.curry (⇑f) x, monotone' := ⋯ }, monotone' := ⋯ },
            invFun := fun f ↦ { toFun := Function.uncurry fun x ↦ ⇑(f x), monotone' := ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
⊢ f.comp id = f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
⊢ id.comp f = f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ fst.prod snd = id

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Preorder γ
inst✝¹ : Preorder δ
ι : Type u_6
π : ι → Type u_7
inst✝ : (i : ι) → Preorder (π i)
p q : α → Prop
h : ∀ (a : α), p a → q a
⊢ ∀ {a b : { x // p x }}, (Subtype.impEmbedding p q h) a ≤ (Subtype.impEmbedding p q h) b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 ↦ x1 < x2) ↪r fun x1 x2 ↦ x1 < x2
⊢ ∀ {a b : α}, f.toEmbedding a ≤ f.toEmbedding b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
f : α ↪o β
⊢ (id α).comp f = f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
f : α ↪o β
⊢ f.comp (id β) = f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
⊢ ∀ {a b : α}, f.toEmbedding a < f.toEmbedding b ↔ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
⊢ Disjoint (f a₁) (f a₂) → Disjoint a₁ a₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : LE γ
inst✝ : LE δ
e : α ≃ β
map_rel_iff' : ∀ {a b : α}, e a ≤ e b ↔ a ≤ b
⊢ ∀ {a b : β}, e.symm a ≤ e.symm b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
⊢ (refl α).trans e = e

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
⊢ e.trans (refl β) = e

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ✝ : Type u_5
inst✝⁷ : LE α✝
inst✝⁶ : LE β✝
inst✝⁵ : LE γ✝
inst✝⁴ : LE δ✝
α : Type ?u.19
β : Type ?u.21
γ : Type ?u.23
δ : Type ?u.25
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : α →o β
⊢ ⇑((fun p ↦ (↑g.symm).comp (p.comp ↑f)) ((fun p ↦ (↑g).comp (p.comp ↑f.symm)) p)) = ⇑p

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ✝ : Type u_5
inst✝⁷ : LE α✝
inst✝⁶ : LE β✝
inst✝⁵ : LE γ✝
inst✝⁴ : LE δ✝
α : Type ?u.19
β : Type ?u.21
γ : Type ?u.23
δ : Type ?u.25
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : γ →o δ
⊢ ⇑((fun p ↦ (↑g).comp (p.comp ↑f.symm)) ((fun p ↦ (↑g.symm).comp (p.comp ↑f)) p)) = ⇑p

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ✝ : Type u_5
inst✝⁷ : LE α✝
inst✝⁶ : LE β✝
inst✝⁵ : LE γ✝
inst✝⁴ : LE δ✝
α : Type ?u.19
β : Type ?u.21
γ : Type ?u.23
δ : Type ?u.25
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : γ →o δ
⊢ ⇑((fun p ↦ (↑g).comp (p.comp ↑f.symm)) ((fun p ↦ (↑g.symm).comp (p.comp ↑f)) p)) = ⇑p

Tactic:
by
    change (g ∘ g.symm) ∘ p ∘ (f ∘ f.symm) = p
    simp only [← OrderIso.coe_trans, Function.id_comp,
               OrderIso.symm_trans_self, OrderIso.coe_refl, Function.comp_id]

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ✝ : Type u_5
inst✝⁷ : LE α✝
inst✝⁶ : LE β✝
inst✝⁵ : LE γ✝
inst✝⁴ : LE δ✝
α : Type ?u.19
β : Type ?u.21
γ : Type ?u.23
δ : Type ?u.25
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α ≃o γ
g : β ≃o δ
p q : α →o β
⊢ { toFun := fun p ↦ (↑g).comp (p.comp ↑f.symm), invFun := fun p ↦ (↑g.symm).comp (p.comp ↑f), left_inv := ⋯,
          right_inv := ⋯ }
        p ≤
      { toFun := fun p ↦ (↑g).comp (p.comp ↑f.symm), invFun := fun p ↦ (↑g.symm).comp (p.comp ↑f), left_inv := ⋯,
          right_inv := ⋯ }
        q ↔
    p ≤ q

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : LE γ
inst✝ : LE δ
x✝ : α ≃o β
⊢ (fun f ↦ ofSurjective ↑f ⋯) ((fun f ↦ ⟨RelIso.toRelEmbedding f, ⋯⟩) x✝) = x✝

Tactic:
by

Goal state after: