awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
a b : α
inst_1 : Std.Refl fun (x1 x2 : α) ↦ x1 ⊆ x2
inst_2 : Std.Antisymm fun (x1 x2 : α) ↦ x1 ⊆ x2
⊢ a = b ↔ b ⊆ a ∧ a ⊆ b

Tactic:
⟨fun h => ⟨h.superset, h.subset⟩, fun h => h.1.antisymm' h.2⟩

Premises used: Eq.subset, And.right, And.left, And.intro, Iff.intro, HasSubset.Subset.antisymm', Eq.superset
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSSubset α
a b c : α
hab : a = b
hbc rwa rwa₁ rwa₂ rwa₃ : b ⊂ c
⊢ a ⊂ c

Tactic:
rwa [hab]
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSSubset α
a b c : α
hab : a ⊂ b
hbc : b = c
rwa rwa₁ rwa₂ rwa₃ : a ⊂ b
⊢ a ⊂ c

Tactic:
rwa [← hbc]
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSSubset α
inst_1 : Std.Irrefl fun (x1 x2 : α) ↦ x1 ⊂ x2
a : α
⊢ ¬a ⊂ a

Tactic:
irrefl _

Premises used: irrefl
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSSubset α
inst_1 : Std.Irrefl fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
⊢ a ⊂ b → a ≠ b

Tactic:
ne_of_irrefl

Premises used: ne_of_irrefl
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSSubset α
inst_1 : Std.Irrefl fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
⊢ a ⊂ b → b ≠ a

Tactic:
ne_of_irrefl'

Premises used: ne_of_irrefl'
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSSubset α
inst_1 : IsTrans α fun (x1 x2 : α) ↦ x1 ⊂ x2
a b c : α
⊢ a ⊂ b → b ⊂ c → a ⊂ c

Tactic:
_root_.trans

Premises used: trans
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSSubset α
inst_1 : Std.Asymm fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
⊢ a ⊂ b → ¬b ⊂ a

Tactic:
asymm

Premises used: asymm
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
⊢ a ⊂ b ↔ a ⊆ b ∧ ¬b ⊆ a

Tactic:
right_iff_left_not_left

Premises used: right_iff_left_not_left
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
h : a ⊂ b
⊢ a ⊆ b

Tactic:
(ssubset_iff_subset_not_subset.1 h).1

Premises used: ssubset_iff_subset_not_subset, And.left, Iff.mp
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
h : a ⊂ b
⊢ ¬b ⊆ a

Tactic:
(ssubset_iff_subset_not_subset.1 h).2

Premises used: ssubset_iff_subset_not_subset, And.right, Iff.mp
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
h : a ⊆ b
⊢ ¬b ⊂ a

Tactic:
fun h' => not_subset_of_ssubset h' h

Premises used: not_subset_of_ssubset, Not
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
h₁ : a ⊆ b
h₂ : ¬b ⊆ a
⊢ a ⊂ b

Tactic:
ssubset_iff_subset_not_subset.2 ⟨h₁, h₂⟩

Premises used: Iff.mpr, ssubset_iff_subset_not_subset, And.intro
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b c : α
inst_3 : IsTrans α fun (x1 x2 : α) ↦ x1 ⊆ x2
h₁ : a ⊆ b
h₂ : b ⊂ c
⊢ a ⊂ c

Tactic:
(h₁.trans h₂.subset).ssubset_of_not_subset fun h => h₂.not_subset <| h.trans h₁

Premises used: HasSubset.Subset.trans, HasSubset.Subset.ssubset_of_not_subset, HasSSubset.SSubset.subset, HasSSubset.SSubset.not_subset
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b c : α
inst_3 : IsTrans α fun (x1 x2 : α) ↦ x1 ⊆ x2
h₁ : a ⊂ b
h₂ : b ⊆ c
⊢ a ⊂ c

Tactic:
(h₁.subset.trans h₂).ssubset_of_not_subset fun h => h₁.not_subset <| h₂.trans h

Premises used: HasSubset.Subset.trans, HasSubset.Subset.ssubset_of_not_subset, HasSSubset.SSubset.subset, HasSSubset.SSubset.not_subset
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
inst_3 : Std.Antisymm fun (x1 x2 : α) ↦ x1 ⊆ x2
h₁ : a ⊆ b
h₂ : a ≠ b
⊢ a ⊂ b

Tactic:
h₁.ssubset_of_not_subset <| mt h₁.antisymm h₂

Premises used: mt, HasSubset.Subset.ssubset_of_not_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
inst_3 : Std.Antisymm fun (x1 x2 : α) ↦ x1 ⊆ x2
h₁ : a ≠ b
h₂ : a ⊆ b
⊢ a ⊂ b

Tactic:
ssubset_of_subset_of_ne h₂ h₁

Premises used: ssubset_of_subset_of_ne
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
inst_3 : Std.Antisymm fun (x1 x2 : α) ↦ x1 ⊆ x2
h : a ⊆ b
⊢ a = b ∨ a ⊂ b

Tactic:
(em (b ⊆ a)).imp h.antisymm h.ssubset_of_not_subset

Premises used: em, HasSubset.Subset.ssubset_of_not_subset, HasSubset.Subset, HasSubset.Subset.antisymm, Or.imp
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
inst_3 : Std.Antisymm fun (x1 x2 : α) ↦ x1 ⊆ x2
h : a ⊆ b
⊢ a ⊂ b ∨ a = b

Tactic:
(eq_or_ssubset_of_subset h).symm

Premises used: Or.symm, eq_or_ssubset_of_subset
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
inst_3 : Std.Antisymm fun (x1 x2 : α) ↦ x1 ⊆ x2
hab : a ⊆ b
hba : ¬a ⊂ b
⊢ a = b

Tactic:
(eq_or_ssubset_of_subset hab).resolve_right hba

Premises used: eq_or_ssubset_of_subset, Or.resolve_right
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
inst_3 : Std.Antisymm fun (x1 x2 : α) ↦ x1 ⊆ x2
hab : a ⊆ b
hba : ¬a ⊂ b
⊢ b = a

Tactic:
((eq_or_ssubset_of_subset hab).resolve_right hba).symm

Premises used: eq_or_ssubset_of_subset, Or.resolve_right, Eq.symm
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
inst_3 : Std.Antisymm fun (x1 x2 : α) ↦ x1 ⊆ x2
⊢ a ⊂ b ↔ a ⊆ b ∧ a ≠ b

Tactic:
⟨fun h => ⟨h.subset, h.ne⟩, fun h => h.1.ssubset_of_ne h.2⟩

Premises used: HasSSubset.SSubset.subset, And.right, And.left, HasSSubset.SSubset.ne, And.intro, Iff.intro, HasSubset.Subset.ssubset_of_ne
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
a b : α
inst_3 : Std.Refl fun (x1 x2 : α) ↦ x1 ⊆ x2
inst_4 : Std.Antisymm fun (x1 x2 : α) ↦ x1 ⊆ x2
⊢ a ⊆ b ↔ a ⊂ b ∨ a = b

Tactic:
⟨fun h => h.ssubset_or_eq, fun h => h.elim subset_of_ssubset subset_of_eq⟩

Premises used: subset_of_eq, HasSubset.Subset.ssubset_or_eq, subset_of_ssubset, Iff.intro, Or.elim
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
inst_3 : IsTrans α fun (x1 x2 : α) ↦ x1 ⊆ x2
a b c d : α
h₁ : c ⊆ a
h₂ : b ⊆ d
⊢ a ⊂ b → c ⊂ d

Tactic:
fun h => (h₁.trans_ssubset h).trans_subset h₂

Premises used: HasSubset.Subset.trans_ssubset, HasSSubset.SSubset.trans_subset
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
inst_1 : HasSSubset α
inst_2 : IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ⊆ x2) fun (x1 x2 : α) ↦ x1 ⊂ x2
inst_3 : IsTrans α fun (x1 x2 : α) ↦ x1 ⊆ x2
a b c d : α
h₁ : a ⊆ c
h₂ : d ⊆ b
⊢ a ⊃ b → c ⊃ d

Tactic:
ssubset_imp_ssubset h₂ h₁

Premises used: GCongr.ssubset_imp_ssubset
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
⊢ Std.Refl fun (x1 x2 : α) ↦ x1 ≤ x2

Tactic:
⟨le_refl⟩

Premises used: le_refl, Std.Refl.mk
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u_1
inst_1 : LE α
inst : Refl fun (x1 x2 : α) ↦ x1 ≥ x2
a : α
⊢ a ≤ a

Tactic:
@Std.Refl.refl α (· ≥ ·) inst a

Premises used: Std.Refl.refl
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
⊢ IsTrans α fun (x1 x2 : α) ↦ x1 ≤ x2

Tactic:
⟨@le_trans _ _⟩

Premises used: IsTrans.mk, le_trans
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
⊢ Std.Irrefl fun (x1 x2 : α) ↦ x1 < x2

Tactic:
⟨lt_irrefl⟩

Premises used: lt_irrefl, Std.Irrefl.mk
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
⊢ IsTrans α fun (x1 x2 : α) ↦ x1 < x2

Tactic:
⟨@lt_trans _ _⟩

Premises used: IsTrans.mk, lt_trans
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
⊢ Std.Asymm fun (x1 x2 : α) ↦ x1 < x2

Tactic:
⟨@lt_asymm _ _⟩

Premises used: lt_asymm, Std.Asymm.mk
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
⊢ Std.Antisymm fun (x1 x2 : α) ↦ x1 < x2

Tactic:
Std.Asymm.antisymm _

Premises used: Std.Asymm.antisymm
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
⊢ IsNonstrictStrictOrder α (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x1 x2 : α) ↦ x1 < x2

Tactic:
⟨@lt_iff_le_not_ge _ _⟩

Premises used: lt_iff_le_not_ge, IsNonstrictStrictOrder.mk
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : PartialOrder α
⊢ Std.Antisymm fun (x1 x2 : α) ↦ x1 ≤ x2

Tactic:
⟨@le_antisymm _ _⟩

Premises used: le_antisymm, Std.Antisymm.mk
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : LinearOrder α
⊢ Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2

Tactic:
⟨le_total⟩

Premises used: le_total, Std.Total.mk
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : LinearOrder α
⊢ ∀ (a b : α), ¬a < b → ¬b < a → a = b

Tactic:
grind
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : LinearOrder α
⊢ Std.Trichotomous fun (x1 x2 : α) ↦ x1 ≤ x2

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : Preorder α
⊢ IsTrans α LE.le

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : Preorder α
⊢ IsTrans α LT.lt

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : LE α
h : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ Std.Total fun (x1 x2 : αᵒᵈ) ↦ x1 ≤ x2

Tactic:
inferInstanceAs <| @Std.Total α <| swap (· ≤ ·)

Premises used: _private.0.OrderDual.total_le._proof_1
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
⊢ WellFoundedLT ℕ

Tactic:
⟨Nat.lt_wfRel.wf⟩

Premises used: IsWellFounded.mk, WellFoundedRelation.wf
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst : FunLike F α β
inst_1 : RelHomClass F r s
f : F
a : α
generalize : ∀ (b : β) (h : (f : (a : α) → β) a = b), Acc s b → Acc r a
⊢ Acc s ((f : (a : α) → β) a) → Acc r a

Tactic:
generalize h : f a = b

Premises used: DFunLike.coe
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst : FunLike F α β
inst_1 : RelHomClass F r s
f : F
b x : β
H : ∀ (y : β), s y x → Acc s y
IH : ∀ (y : β), s y x → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a
a : α
h : (f : (a : α) → β) a = x
⊢ Acc r a

Tactic:
?_
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst : FunLike F α β
inst_1 : RelHomClass F r s
f : F
a : α
b : β
h : (f : (a : α) → β) a = b
ac : Acc s b
intro :
  ∀ (x : β) (H : ∀ (y : β), s y x → Acc s y) (IH : ∀ (y : β), s y x → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a)
    (a : α) (h : (f : (a : α) → β) a = x), Acc r a
⊢ Acc r a

Tactic:
induction ac generalizing a with | intro _ H IH => ?_
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst : FunLike F α β
inst_1 : RelHomClass F r s
f : F
b x : β
H : ∀ (y : β), s y x → Acc s y
IH : ∀ (y : β), s y x → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a
a : α
h : (f : (a : α) → β) a = x
⊢ ∀ (y : β), s y ((f : (a : α) → β) a) → Acc s y

Tactic:
subst h
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst : FunLike F α β
inst_1 : RelHomClass F r s
f : F
b x : β
H : ∀ (y : β), s y x → Acc s y
IH : ∀ (y : β), s y x → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a
a : α
h : (f : (a : α) → β) a = x
H₁ : ∀ (y : β), s y ((f : (a : α) → β) a) → Acc s y
⊢ ∀ (y : β), s y ((f : (a : α) → β) a) → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a

Tactic:
subst h
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst : FunLike F α β
inst_1 : RelHomClass F r s
f : F
b : β
a : α
H : ∀ (y : β), s y ((f : (a : α) → β) a) → Acc s y
IH : ∀ (y : β), s y ((f : (a : α) → β) a) → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a
⊢ Acc r a

Tactic:
⟨_, fun a' h => IH (f a') (map_rel f h) _ rfl⟩

Premises used: RelHomClass.map_rel, DFunLike.coe, rfl, Acc.intro
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst : FunLike F α β
inst_1 : RelHomClass F r s
f : F
b : β
a : α
H : ∀ (y : β), s y ((f : (a : α) → β) a) → Acc s y
IH : ∀ (y : β), s y ((f : (a : α) → β) a) → ∀ (a : α) (h : (f : (a : α) → β) a = y), Acc r a
⊢ Acc r a

Tactic:
exact ⟨_, fun a' h => IH (f a') (map_rel f h) _ rfl⟩
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst : FunLike F α β
inst_1 : RelHomClass F r s
f : F
inst_2 : IsWellFounded β s
⊢ IsWellFounded α r

Tactic:
⟨RelHomClass.wellFounded f IsWellFounded.wf⟩

Premises used: RelHomClass.wellFounded, IsWellFounded.mk, IsWellFounded.wf
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f g : r →r s
h :
  Eq (α := (a : α) → β) ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) f)
    ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) g)
mk :
  ∀ (toFun : α → β) (map_rel' : ∀ {a b : α}, r a b → s (toFun a) (toFun b))
    (h :
      Eq (α := (a : α) → β)
        ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) (RelHom.mk (r := r) (s := s) toFun @map_rel'))
        ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) g)),
    RelHom.mk (r := r) (s := s) toFun @map_rel' = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
g : r →r s
toFun : α → β
map_rel' : ∀ {a b : α}, r a b → s (toFun a) (toFun b)
h :
  Eq (α := (a : α) → β) ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) (RelHom.mk (r := r) (s := s) toFun @map_rel'))
    ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) g)
mk :
  ∀ (toFun_1 : α → β) (map_rel'_1 : ∀ {a b : α}, r a b → s (toFun_1 a) (toFun_1 b))
    (h :
      Eq (α := (a : α) → β)
        ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) (RelHom.mk (r := r) (s := s) toFun @map_rel'))
        ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) (RelHom.mk (r := r) (s := s) toFun_1 @map_rel'_1))),
    RelHom.mk (r := r) (s := s) toFun @map_rel' = RelHom.mk (r := r) (s := s) toFun_1 @map_rel'_1
⊢ RelHom.mk (r := r) (s := s) toFun @map_rel' = g

Tactic:
cases g
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
toFun : α → β
map_rel' : ∀ {a b : α}, r a b → s (toFun a) (toFun b)
toFun_1 : α → β
map_rel'_1 : ∀ {a b : α}, r a b → s (toFun_1 a) (toFun_1 b)
h :
  Eq (α := (a : α) → β) ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) (mk (r := r) (s := s) toFun @map_rel'))
    ((fun (o : r →r s) ↦ o.toFun (r := r) (s := s)) (mk (r := r) (s := s) toFun_1 @map_rel'_1))
⊢ mk (r := r) (s := s) toFun @map_rel' = mk (r := r) (s := s) toFun_1 @map_rel'_1

Tactic:
congr
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r →r s
a b : α
⊢ r a b → s ((f : (a : α) → β) a) ((f : (a : α) → β) b)

Tactic:
f.map_rel'

Premises used: RelHom.map_rel'
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r →r s
⊢ f.toFun (r := r) (s := s) = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
h : ∀ {a b : α}, r a b → s (f a) (f b)
⊢ (⇑(mk (r := r) (s := s) f @h) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
⊢ Injective (β := (a : α) → β) fun (f : r →r s) ↦ (⇑f : (a : α) → β)

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f g : r →r s
h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
inl : ∀ (h : r x y), x = y
inr : ∀ (h : x = y), x = y
inr₁ : ∀ (h : r y x), x = y
⊢ x = y

Tactic:
rcases trichotomous_of r x y with (h | h | h)

Premises used: trichotomous_of
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
⊢ s (f x) (f y)

Tactic:
have := hf h
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f x) (f y)
⊢ s (f y) (f y)

Tactic:
rw [hxy] at this
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f y) (f y)
inl : False
⊢ x = y

Tactic:
exfalso
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f y) (f y)
⊢ False

Tactic:
irrefl_of s (f y) this

Premises used: irrefl_of
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f y) (f y)
⊢ False

Tactic:
exact irrefl_of s (f y) this

Premises used: irrefl_of
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : x = y
⊢ x = y

Tactic:
h
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : x = y
⊢ x = y

Tactic:
exact h
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
⊢ s (f y) (f x)

Tactic:
have := hf h
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f x)
⊢ s (f y) (f y)

Tactic:
rw [hxy] at this
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f y)
inr : False
⊢ x = y

Tactic:
exfalso
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f y)
⊢ False

Tactic:
irrefl_of s (f y) this

Premises used: irrefl_of
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f y)
⊢ False

Tactic:
exact irrefl_of s (f y) this

Premises used: irrefl_of
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl s
f : r →r s
⊢ Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
_root_.injective_of_increasing r s f f.map_rel

Premises used: injective_of_increasing, RelHom.map_rel, DFunLike.coe
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ r (surjInv hf a) (surjInv hf b)

Tactic:
simpa only [o, surjInv_eq hf] using h

Premises used: Function.surjInv_eq
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_5
β : Type u_6
f : α → β
s : β → β → Prop
hs : Equivalence s
⊢ Equivalence (f ⁻¹'o s)

Tactic:
⟨fun _ => hs.1 _, fun h => hs.2 h, fun h₁ h₂ => hs.3 h₁ h₂⟩

Premises used: Equivalence.symm, Equivalence.refl, Equivalence.trans, Equivalence.mk
-- Module: Mathlib.Order.RelIso.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f g : r ↪r s
h :
  Eq (α := (a : α) → β) ((fun (x : r ↪r s) ↦ x.toEmbedding (r := r) (s := s).toFun) f)
    ((fun (x : r ↪r s) ↦ x.toEmbedding (r := r) (s := s).toFun) g)
rcases :
  ∀ (toFun : α → β) (inj' : Injective toFun)
    (map_rel_iff' :
      ∀ {a b : α},
        s (({ toFun := toFun, inj' := inj' : α ↪ β } : (a : α) → β) a)
            (({ toFun := toFun, inj' := inj' : α ↪ β } : (a : α) → β) b) ↔
          r a b)
    (h :
      Eq (α := (a : α) → β)
        ((fun (x : r ↪r s) ↦ x.toEmbedding (r := r) (s := s).toFun)
          (mk (r := r) (s := s) { toFun := toFun, inj' := inj' } @map_rel_iff'))
        ((fun (x : r ↪r s) ↦ x.toEmbedding (r := r) (s := s).toFun) g)),
    mk (r := r) (s := s) { toFun := toFun, inj' := inj' : α ↪ β } @map_rel_iff' = g
⊢ f = g

Tactic:
rcases f with ⟨⟨⟩⟩