awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsStrictOrder α r
x y : α
h : r x y
e : y = x
⊢ r x x

Tactic:
rw [e] at h
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsStrictOrder α r
x y : α
h : r x y
e : y = x
h₁ : r x x
⊢ y = x

Tactic:
rw [e] at h
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsStrictOrder α r
x y : α
h : r x x
e : y = x
⊢ False

Tactic:
irrefl _ h

Premises used: irrefl
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsStrictOrder α r
x y : α
h : r x x
e : y = x
⊢ False

Tactic:
exact irrefl _ h

Premises used: irrefl
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : IsStrictTotalOrder α r
⊢ IsStrictTotalOrder α (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : IsOrderConnected α r
a b c : α
h₁ : ¬r a b
h₂ : ¬r b c
⊢ ¬(r a b ∨ r b c)

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : Std.Asymm r
inst_1 : IsOrderConnected α r
⊢ IsStrictWeakOrder α r

Tactic:
{ @Std.Asymm.irrefl α r _ with
    trans := fun _ _ c h₁ h₂ => (IsOrderConnected.conn _ c _ h₁).resolve_right (asymm h₂),
    incomp_trans := fun _ _ _ ⟨h₁, h₂⟩ ⟨h₃, h₄⟩ =>
      ⟨IsOrderConnected.neg_trans h₁ h₃, IsOrderConnected.neg_trans h₄ h₂⟩ }

Premises used: Std.Asymm.irrefl, IsStrictWeakOrder.mk, And, IsOrderConnected.neg_trans, And.intro, _private.0.isStrictWeakOrder_of_isOrderConnected.match_1, Not
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsStrictTotalOrder α r
⊢ IsOrderConnected α r

Tactic:
⟨fun _ _ _ h ↦ (trichotomous _ _).imp_right
    fun o ↦ o.elim (fun e ↦ e ▸ h) fun h' ↦ _root_.trans h' h⟩

Premises used: IsOrderConnected.mk, trichotomous, Or.imp_right
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
inst : Std.Trichotomous r
f : β → α
h : Injective f
⊢ Std.Trichotomous (InvImage r f)

Tactic:
⟨fun {a b} hab hba ↦ h <| Std.Trichotomous.trichotomous (f a) (f b) hab hba⟩

Premises used: Std.Trichotomous.mk, Std.Trichotomous.trichotomous
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
h : WellFoundedRelation α
⊢ IsWellFounded α rel

Tactic:
{ h with }

Premises used: IsWellFounded.mk, WellFoundedRelation.wf
-- Module: Mathlib.Order.RelClasses
Goal:
α : Sort u_1
inst : WellFoundedRelation α
a b : α
⊢ rel a b → ¬rel b a

Tactic:
fun hab hba => WellFoundedRelation.asymmetric hba hab

Premises used: Not
-- Module: Mathlib.Order.RelClasses
Goal:
α : Sort u_1
inst : WellFoundedRelation α
a b c : α
⊢ rel a b → rel b c → ¬rel c a

Tactic:
fun hab hbc hca => WellFoundedRelation.asymmetric₃ hca hab hbc

Premises used: Not
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
ra : α → α → Prop
rb : β → β → Prop
ha : WellFounded ra
hb : WellFounded rb
⊢ WellFounded (Prod.Lex ra rb)

Tactic:
(Prod.lex ⟨_, ha⟩ ⟨_, hb⟩).wf

Premises used: WellFoundedRelation.wf
-- Module: Mathlib.Order.RelClasses
Goal:
α : Sort u_1
β : α → Sort u_2
r : α → α → Prop
s : (a : α) → β a → β a → Prop
ha : WellFounded r
hb : ∀ (x : α), WellFounded (s x)
⊢ WellFounded (Lex (β := β) r s)

Tactic:
WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) hb b

Premises used: PSigma.Lex, PSigma.lexAccessible, WellFounded.apply, Acc, WellFounded.intro, _private.0.WellFounded.psigma_lex.match_1
-- Module: Mathlib.Order.RelClasses
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
s : β → β → Prop
ha : WellFounded r
hb : WellFounded s
⊢ WellFounded (RevLex r s)

Tactic:
WellFounded.intro fun ⟨a, b⟩ => revLexAccessible (apply hb b) (WellFounded.apply ha) a

Premises used: PSigma.RevLex, WellFounded.apply, Acc, WellFounded.intro, PSigma.revLexAccessible, _private.0.WellFounded.psigma_revLex.match_1
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
s : β → β → Prop
hb : WellFounded s
⊢ WellFounded (SkipLeft α s)

Tactic:
psigma_revLex emptyWf.wf hb

Premises used: WellFounded.psigma_revLex, PSigma.SkipLeft, WellFoundedRelation.wf
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : IsWellFounded α r
motive : α → Prop
a : α
ind : ∀ (x : α), (∀ (y : α), r y x → motive y) → motive x
⊢ motive a

Tactic:
wf.induction _ ind

Premises used: IsWellFounded.wf, WellFounded.induction
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : IsWellFounded α r
⊢ ∀ (a : α), Acc r a

Tactic:
wf.apply

Premises used: WellFounded.apply, IsWellFounded.wf
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : IsWellFounded α r
motive : α → Sort u_1
ind : (x : α) → ((y : α) → r y x → motive y) → motive x
⊢ ∀ (x : α), fix r (motive := motive) ind x = ind x fun (y : α) (x : r y x) ↦ fix r (motive := motive) ind y

Tactic:
wf.fix_eq ind

Premises used: IsWellFounded.wf, IsWellFounded.fix, WellFounded.fix_eq
-- Module: Mathlib.Order.RelClasses
Goal:
α : Sort u_1
r : α → α → Prop
h : WellFounded r
a b : α
⊢ r a b → ¬r b a

Tactic:
@WellFoundedRelation.asymmetric _ ⟨_, h⟩ _ _

Premises used: WellFoundedRelation.asymmetric
-- Module: Mathlib.Order.RelClasses
Goal:
α : Sort u_1
r : α → α → Prop
h : WellFounded r
a b c : α
⊢ r a b → r b c → ¬r c a

Tactic:
@WellFoundedRelation.asymmetric₃ _ ⟨_, h⟩ _ _ _

Premises used: WellFoundedRelation.asymmetric₃
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsWellFounded α r
⊢ Std.Asymm r

Tactic:
⟨IsWellFounded.wf.asymmetric⟩

Premises used: IsWellFounded.wf, WellFounded.asymmetric, Std.Asymm.mk
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
i : IsWellFounded α r
⊢ IsWellFounded α (Relation.TransGen r)

Tactic:
⟨i.wf.transGen⟩

Premises used: IsWellFounded.mk, IsWellFounded.wf, WellFounded.transGen
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : LT α
inst_1 : WellFoundedLT α
⊢ WellFounded fun (x1 x2 : α) ↦ x1 < x2

Tactic:
IsWellFounded.wf

Premises used: IsWellFounded.wf
-- Module: Mathlib.Order.RelClasses
Goal:
α_1 : Type u
β : Type v
r : α_1 → α_1 → Prop
s : β → β → Prop
α : Type u_1
inst : LT α
h : WellFoundedLT α
⊢ WellFoundedGT.{u_1} αᵒᵈ

Tactic:
h

Premises used: OrderDual
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u_1
inst : LT α
⊢ WellFoundedGT.{u_1} αᵒᵈ ↔ WellFoundedLT α

Tactic:
⟨fun h => ⟨h.wf⟩, fun h => ⟨h.wf⟩⟩

Premises used: IsWellFounded.mk, IsWellFounded.wf, Iff.intro
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
inl : ∀ (hac : r a c), r a c
inr : ∀ (hbc : r b a), r a a
inr₁ : ∀ (hca : r c a), r a c
⊢ r a c

Tactic:
rcases trichotomous_of r a c with (hac | rfl | hca)

Premises used: trichotomous_of, rfl
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hac : r a c
⊢ r a c

Tactic:
hac
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hac : r a c
⊢ r a c

Tactic:
exact hac
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsWellOrder α r
a b : α
hab : r a b
hbc : r b a
⊢ r a a

Tactic:
asymm_of r hab hbc |>.elim

Premises used: asymm_of, False.elim
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsWellOrder α r
a b : α
hab : r a b
hbc : r b a
⊢ r a a

Tactic:
exact asymm_of r hab hbc |>.elim

Premises used: asymm_of, False.elim
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hca : r c a
⊢ r a c

Tactic:
IsWellFounded.wf.asymmetric₃ a b c hab hbc hca |>.elim

Premises used: False.elim, IsWellFounded.wf, WellFounded.asymmetric₃
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hca : r c a
⊢ r a c

Tactic:
exact IsWellFounded.wf.asymmetric₃ a b c hab hbc hca |>.elim

Premises used: False.elim, IsWellFounded.wf, WellFounded.asymmetric₃
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : LT α
inst_1 : WellFoundedLT α
motive : α → Prop
a : α
ind : ∀ (x : α), (∀ (y : α), y < x → motive y) → motive x
⊢ motive a

Tactic:
IsWellFounded.induction _ _ ind

Premises used: IsWellFounded.induction
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : LT α
inst_1 : WellFoundedLT α
⊢ ∀ (a : α), Acc (fun (x1 x2 : α) ↦ x1 < x2) a

Tactic:
IsWellFounded.apply _

Premises used: IsWellFounded.apply
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : LT α
inst_1 : WellFoundedLT α
motive : α → Sort u_1
ind : (x : α) → ((y : α) → y < x → motive y) → motive x
⊢ ∀ (x : α), fix (motive := motive) ind x = ind x fun (y : α) (x : y < x) ↦ fix (motive := motive) ind y

Tactic:
IsWellFounded.fix_eq _ ind

Premises used: IsWellFounded.fix_eq, WellFoundedLT.fix
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Subsingleton α
⊢ IsWellOrder α emptyRelation

Tactic:
Subsingleton.isWellOrder _

Premises used: Subsingleton.isWellOrder
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellFounded α r
inst_1 : IsWellFounded β s
⊢ IsWellFounded (α × β) (Prod.Lex r s)

Tactic:
⟨IsWellFounded.wf.prod_lex IsWellFounded.wf⟩

Premises used: IsWellFounded.mk, IsWellFounded.wf, WellFounded.prod_lex
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
x x_1 : α × β
a₁ : α
a₂ : β
b₁ : α
b₂ : β
hab : ¬Prod.Lex r s (a₁, a₂) (b₁, b₂)
hba : ¬Prod.Lex r s (b₁, b₂) (a₁, a₂)
obtain : ∀ (hab : ¬Prod.Lex r s (a₁, a₂) (a₁, b₂)) (hba : ¬Prod.Lex r s (a₁, b₂) (a₁, a₂)), (a₁, a₂) = (a₁, b₂)
⊢ (a₁, a₂) = (b₁, b₂)

Tactic:
obtain rfl := Std.Trichotomous.trichotomous a₁ b₁
      (mt (Prod.Lex.left a₂ b₂) hab) (mt (Prod.Lex.left b₂ a₂) hba)

Premises used: mt, Prod.Lex.left, Std.Trichotomous.trichotomous, rfl
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
x x_1 : α × β
a₁ : α
a₂ b₂ : β
hab : ¬Prod.Lex r s (a₁, a₂) (a₁, b₂)
hba : ¬Prod.Lex r s (a₁, b₂) (a₁, a₂)
obtain : ∀ (hab hba : ¬Prod.Lex r s (a₁, a₂) (a₁, a₂)), (a₁, a₂) = (a₁, a₂)
⊢ (a₁, a₂) = (a₁, b₂)

Tactic:
obtain rfl := Std.Trichotomous.trichotomous a₂ b₂
      (mt (Prod.Lex.right a₁) hab) (mt (Prod.Lex.right a₁) hba)

Premises used: mt, Prod.Lex.right, Std.Trichotomous.trichotomous, rfl
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
x x_1 : α × β
a₁ : α
a₂ : β
hab hba : ¬Prod.Lex r s (a₁, a₂) (a₁, a₂)
⊢ (a₁, a₂) = (a₁, a₂)

Tactic:
rfl
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : IsWellFounded α r
f : β → α
⊢ IsWellFounded β (InvImage r f)

Tactic:
⟨InvImage.wf f IsWellFounded.wf⟩

Premises used: IsWellFounded.mk, IsWellFounded.wf, InvImage.wf
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
f : α → ℕ
⊢ IsWellFounded α (InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) f)

Tactic:
⟨(measure f).wf⟩

Premises used: IsWellFounded.mk, WellFoundedRelation.wf
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
inst : IsWellFounded α r
s : α → α → Prop
h : Subrelation s r
⊢ IsWellFounded α s

Tactic:
⟨h.wf IsWellFounded.wf⟩

Premises used: IsWellFounded.mk, IsWellFounded.wf, Subrelation.wf
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
suffices : ∀ (a a' : α), a' ≤ a → ∀ (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
⊢ WellFounded fun (x1 x2 : α × β) ↦ x1 < x2

Tactic:
suffices h : ∀ a, ∀ a' ≤ a, ∀ b, Acc (· < ·) (a', b) from ⟨fun x => h x.1 x.1 le_rfl x.2⟩
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
a a' : α
ha : a' ≤ a
b : β
ind :
  ∀ (a : α) (iha : ∀ (y : α), y < a → ∀ (a' : α) (ha : a' ≤ y) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b))
    (a' : α) (ha : a' ≤ a) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
⊢ Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)

Tactic:
induction a using WellFoundedLT.induction generalizing a' b with | ind a iha

Premises used: WellFoundedLT.induction
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α) (ha : a' ≤ y) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
a' : α
ha : a' ≤ a
b : β
ind :
  ∀ (b : β) (ihb : ∀ (y : β), y < b → ∀ (a' : α) (ha : a' ≤ a), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', y)) (a' : α)
    (ha : a' ≤ a), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
⊢ Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)

Tactic:
induction b using WellFoundedLT.induction generalizing a' with | ind b ihb

Premises used: WellFoundedLT.induction
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α) (ha : a' ≤ y) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α) (ha : a' ≤ a), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
⊢ Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)

Tactic:
Acc.intro (a', b) fun x hx => ?_

Premises used: Prod.mk, Acc.intro
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α) (ha : a' ≤ y) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α) (ha : a' ≤ a), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
ind : ∀ (x : α × β) (hx : x < (a', b)), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) x
⊢ Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)

Tactic:
refine Acc.intro (a', b) fun x hx => ?_

Premises used: Prod.mk, Acc.intro
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α) (ha : a' ≤ y) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α) (ha : a' ≤ a), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ind : ∀ (ha' : x.fst < (a', b).fst) (hb : x.snd ≤ (a', b).snd), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) x
ind₁ : ∀ (ha' : x.fst ≤ (a', b).fst) (hb : x.snd < (a', b).snd), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) x
⊢ Acc (fun (x1 x2 : α × β) ↦ x1 < x2) x

Tactic:
obtain ⟨ha', hb⟩ | ⟨ha', hb⟩ := Prod.lt_iff.1 hx

Premises used: Prod.lt_iff, Iff.mp
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α) (ha : a' ≤ y) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α) (ha : a' ≤ a), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst < (a', b).fst
hb : x.snd ≤ (a', b).snd
⊢ Acc (fun (x1 x2 : α × β) ↦ x1 < x2) x

Tactic:
iha x.1 (ha'.trans_le ha) x.1 le_rfl x.2

Premises used: le_rfl, Prod.fst, LT.lt.trans_le, Prod.snd
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α) (ha : a' ≤ y) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α) (ha : a' ≤ a), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst < (a', b).fst
hb : x.snd ≤ (a', b).snd
⊢ Acc (fun (x1 x2 : α × β) ↦ x1 < x2) x

Tactic:
exact iha x.1 (ha'.trans_le ha) x.1 le_rfl x.2

Premises used: le_rfl, Prod.fst, LT.lt.trans_le, Prod.snd
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α) (ha : a' ≤ y) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α) (ha : a' ≤ a), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst ≤ (a', b).fst
hb : x.snd < (a', b).snd
⊢ Acc (fun (x1 x2 : α × β) ↦ x1 < x2) x

Tactic:
ihb x.2 hb x.1 (ha'.trans ha)

Premises used: Prod.fst, LE.le.trans, Prod.snd
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
inst_3 : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α) (ha : a' ≤ y) (b : β), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α) (ha : a' ≤ a), Acc (fun (x1 x2 : α × β) ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst ≤ (a', b).fst
hb : x.snd < (a', b).snd
⊢ Acc (fun (x1 x2 : α × β) ↦ x1 < x2) x

Tactic:
exact ihb x.2 hb x.1 (ha'.trans ha)

Premises used: Prod.fst, LE.le.trans, Prod.snd
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
s : Set α
⊢ ¬Bounded r s ↔ Unbounded r s

Tactic:
simp only [Bounded, Unbounded, not_forall, not_exists, exists_prop]

Premises used: Set.Bounded, not_exists, exists_prop, Set.Unbounded, Classical.not_forall
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r : α → α → Prop
s : Set α
rw : ¬Bounded r s ↔ Unbounded r s
rw₁ rw₂ : Unbounded r s ↔ Unbounded r s
⊢ ¬Unbounded r s ↔ Bounded r s

Tactic:
rw [not_iff_comm, not_bounded_iff]

Premises used: Set.not_bounded_iff, not_iff_comm
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : IsEmpty α
r : α → α → Prop
s : Set α
⊢ Unbounded r s

Tactic:
isEmptyElim

Premises used: isEmptyElim, Set.Unbounded
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Std.Refl r
f : β → α
⊢ Std.Refl (f ⁻¹'o r)

Tactic:
⟨fun _ => refl_of r _⟩

Premises used: refl_of, Std.Refl.mk
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl r
f : β → α
⊢ Std.Irrefl (f ⁻¹'o r)

Tactic:
⟨fun _ => irrefl_of r _⟩

Premises used: irrefl_of, Std.Irrefl.mk
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Std.Symm r
f : β → α
⊢ Std.Symm (f ⁻¹'o r)

Tactic:
⟨fun _ _ ↦ symm_of r⟩

Premises used: Std.Symm.mk, symm_of
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Std.Asymm r
f : β → α
⊢ Std.Asymm (f ⁻¹'o r)

Tactic:
⟨fun _ _ ↦ asymm_of r⟩

Premises used: asymm_of, Std.Asymm.mk
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : IsTrans α r
f : β → α
⊢ IsTrans β (f ⁻¹'o r)

Tactic:
⟨fun _ _ _ => trans_of r⟩

Premises used: IsTrans.mk, trans_of
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst : Std.Total r
f : β → α
⊢ Std.Total (f ⁻¹'o r)

Tactic:
⟨fun _ _ => total_of r _ _⟩

Premises used: total_of, Std.Total.mk
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
inst : Std.Antisymm r
f : β → α
hf : Injective f
⊢ Std.Antisymm (f ⁻¹'o r)

Tactic:
⟨fun _ _ h₁ h₂ ↦ hf <| antisymm_of r h₁ h₂⟩

Premises used: antisymm_of, Std.Antisymm.mk
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r s : α → α → Prop
inst : IsNonstrictStrictOrder α r s
a b : α
⊢ s a b ↔ r a b ∧ ¬r b a

Tactic:
IsNonstrictStrictOrder.right_iff_left_not_left _ _

Premises used: IsNonstrictStrictOrder.right_iff_left_not_left
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
r s : α → α → Prop
inst : IsNonstrictStrictOrder α r s
a b : α
⊢ s a b ↔ r a b ∧ ¬r b a

Tactic:
right_iff_left_not_left

Premises used: right_iff_left_not_left
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
β : Type v
r : α → α → Prop
s_1 : β → β → Prop
s : α → α → Prop
inst : IsNonstrictStrictOrder α r s
⊢ Std.Irrefl s

Tactic:
⟨fun _ h => ((right_iff_left_not_left_of r s).1 h).2 ((right_iff_left_not_left_of r s).1 h).1⟩

Premises used: right_iff_left_not_left_of, Std.Irrefl.mk, And.right, And.left, Iff.mp
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
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 : HasSubset α
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 : HasSubset α
inst_1 : Std.Refl fun (x1 x2 : α) ↦ x1 ⊆ x2
a : α
⊢ a ⊆ a

Tactic:
refl _

Premises used: refl
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
a : α
inst_1 : Std.Refl fun (x1 x2 : α) ↦ x1 ⊆ x2
⊢ a ⊆ a

Tactic:
refl _

Premises used: refl
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
a b : α
inst_1 : Std.Refl fun (x1 x2 : α) ↦ x1 ⊆ x2
⊢ a = b → a ⊆ b

Tactic:
fun h => h ▸ subset_rfl

Premises used: Eq.rec, subset_rfl
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
a b : α
inst_1 : Std.Refl fun (x1 x2 : α) ↦ x1 ⊆ x2
⊢ a = b → b ⊆ a

Tactic:
fun h => h ▸ subset_rfl

Premises used: Eq.rec, subset_rfl
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
a b : α
inst_1 : Std.Refl fun (x1 x2 : α) ↦ x1 ⊆ x2
⊢ ¬a ⊆ b → a ≠ b

Tactic:
mt subset_of_eq

Premises used: mt, subset_of_eq
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
a b : α
inst_1 : Std.Refl fun (x1 x2 : α) ↦ x1 ⊆ x2
⊢ ¬a ⊆ b → b ≠ a

Tactic:
mt superset_of_eq

Premises used: mt, superset_of_eq
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
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 : HasSubset α
a b : α
inst_1 : Std.Antisymm fun (x1 x2 : α) ↦ x1 ⊆ x2
⊢ a ⊆ b → b ⊆ a → a = b

Tactic:
antisymm

Premises used: antisymm
-- Module: Mathlib.Order.RelClasses
Goal:
α : Type u
inst : HasSubset α
a b : α
inst_1 : Std.Antisymm fun (x1 x2 : α) ↦ x1 ⊆ x2
⊢ a ⊆ b → b ⊆ a → b = a

Tactic:
antisymm'

Premises used: antisymm'
-- 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 ↔ a ⊆ b ∧ b ⊆ a

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

Premises used: Eq.subset, And.right, And.left, HasSubset.Subset.antisymm, And.intro, Iff.intro, Eq.superset