awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
a b : α
h : r a b
⊢ IsChain r {a, b}

Tactic:
IsChain.singleton.insert fun _ hb _ ↦ .inl <| (eq_of_mem_singleton hb).symm.recOn ‹_›

Premises used: Eq.recOn, Set.eq_of_mem_singleton, IsChain.singleton, Or.inl, IsChain.insert, Eq.symm
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
⊢ IsChain r univ ↔ Std.Trichotomous r

Tactic:
⟨fun h => ⟨fun a b => ?_⟩, fun h => @isChain_of_trichotomous _ _ h univ⟩

Premises used: Set.univ, Std.Trichotomous.mk, Iff.intro, isChain_of_trichotomous
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
refine : ∀ (h : IsChain r univ) (a b : α), ¬r a b → ¬r b a → a = b
⊢ IsChain r univ ↔ Std.Trichotomous r

Tactic:
refine ⟨fun h => ⟨fun a b => ?_⟩, fun h => @isChain_of_trichotomous _ _ h univ⟩
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
h : IsChain r univ
a b : α
⊢ a ≠ b → r a b ∨ r b a

Tactic:
have : a ≠ b → (r a b ∨ r b a) := h trivial trivial
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
h : IsChain r univ
a b : α
this : a ≠ b → r a b ∨ r b a
⊢ ¬r a b → ¬r b a → a = b

Tactic:
grind
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
h : ∀ (x y : α), r x y → s (f x) (f y)
c : Set α
hrc : IsChain r c
⊢ IsChain s (f '' c)

Tactic:
fun _ ⟨_, ha₁, ha₂⟩ _ ⟨_, hb₁, hb₂⟩ =>
  ha₂ ▸ hb₂ ▸ fun hxy => (hrc ha₁ hb₁ <| ne_of_apply_ne f hxy).imp (h _ _) (h _ _)

Premises used: _private.0.IsChain.image_of_map_rel.match_1, Eq.rec, Set.Pairwise, ne_of_apply_ne, IsChain, Or.imp
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
x : α
ha : x ∈ f ⁻¹' c
_ : ∀ ⦃y : α⦄, y ∈ f ⁻¹' c → x ≠ y → (fun (x y : α) ↦ r x y ∨ r y x) x y
⊢ ∀ ⦃y : α⦄, y ∈ f ⁻¹' c → x ≠ y → (fun (x y : α) ↦ r x y ∨ r y x) x y

Tactic:
_
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
x : α
ha : x ∈ f ⁻¹' c
y : α
hb : y ∈ f ⁻¹' c
hne : x ≠ y
⊢ (fun (x y : β) ↦ s x y ∨ s y x) (f x) (f y)

Tactic:
have := hrc ha hb (fun h ↦ hne (hf h))
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
x : α
ha : x ∈ f ⁻¹' c
y : α
hb : y ∈ f ⁻¹' c
hne : x ≠ y
this : (fun (x y : β) ↦ s x y ∨ s y x) (f x) (f y)
⊢ r x y ∨ r y x

Tactic:
grind
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
rw :
  ((s ∪ t).Pairwise fun (x y : α) ↦ r x y ∨ r y x) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a
rw₁ :
  ((s ∪ t).Pairwise fun (x y : α) ↦ r x y ∨ r y x) ↔
    (s.Pairwise fun (x y : α) ↦ r x y ∨ r y x) ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a
rw₂ :
  ((s ∪ t).Pairwise fun (x y : α) ↦ r x y ∨ r y x) ↔
    (s.Pairwise fun (x y : α) ↦ r x y ∨ r y x) ∧
      (t.Pairwise fun (x y : α) ↦ r x y ∨ r y x) ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a
rw₃ rw₄ :
  ((s.Pairwise fun (x x_1 : α) ↦ r x x_1 ∨ r x_1 x) ∧
      (t.Pairwise fun (x x_1 : α) ↦ r x x_1 ∨ r x_1 x) ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a) ↔
    (s.Pairwise fun (x y : α) ↦ r x y ∨ r y x) ∧
      (t.Pairwise fun (x y : α) ↦ r x y ∨ r y x) ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a
⊢ IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a

Tactic:
rw [IsChain, IsChain, IsChain, pairwise_union_of_symmetric fun _ _ ↦ Or.symm]

Premises used: Or.symm, IsChain, Set.pairwise_union_of_symmetric
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α → β
hf : Monotone f
hs : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ IsChain (fun (x1 x2 : β) ↦ x1 ≤ x2) (f '' s)

Tactic:
hs.image_of_map_rel _ _ _ (fun _ _ a ↦ hf a)

Premises used: IsChain.image_of_map_rel
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
rw : IsChain (fun (x1 x2 : β) ↦ x1 ≤ x2) (f '' univ)
⊢ IsChain (fun (x1 x2 : β) ↦ x1 ≤ x2) (range f)

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun (x1 x2 : β) ↦ x1 ≤ x2) (f '' univ)

Tactic:
hf.isChain_image (isChain_of_trichotomous _)

Premises used: Monotone.isChain_image, isChain_of_trichotomous
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun (x1 x2 : β) ↦ x1 ≤ x2) (f '' univ)

Tactic:
exact hf.isChain_image (isChain_of_trichotomous _)

Premises used: Monotone.isChain_image, isChain_of_trichotomous
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
h : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ IsChain (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
fun _a ha _b hb hne ↦
  (h ha hb hne).imp hne.lt_of_le hne.lt_of_le'

Premises used: Set.Pairwise, IsChain, Or.imp, Ne.lt_of_le, Ne.lt_of_le'
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
h : IsChain r s
⊢ IsChain r (s \ t)

Tactic:
h.mono Set.diff_subset

Premises used: Set.diff_subset, IsChain.mono
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsChain (fun (x1 x2 : (↑s : Type u_1)) ↦ r (↑x1 : α) (↑x2 : α)) (s ↓∩ t) ↔ IsChain r (s ∩ t)

Tactic:
simp [IsChain, Set.Pairwise]

Premises used: Set.Pairwise, IsChain
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsChain (fun (x1 x2 : (↑s : Type u_1)) ↦ r (↑x1 : α) (↑x2 : α)) univ ↔ IsChain r s

Tactic:
simpa using isChain_preimage_subtypeVal s univ

Premises used: Set.univ, isChain_preimage_subtypeVal
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst : FunLike F α β
inst_1 : RelHomClass F r r'
hs : IsChain r s
φ : F
⊢ IsChain r' ((⇑φ : (a : α) → β) '' s)

Tactic:
hs.image_of_map_rel _ _ _ (fun _ _ h ↦ map_rel φ h)

Premises used: IsChain.image_of_map_rel, RelHomClass.map_rel
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsChain r s
φ : r ↪r r'
⊢ IsChain r' ((⇑φ : (a : α) → β) '' s)

Tactic:
hs.image _

Premises used: IsChain.image
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
t : Set β
ht : IsChain r' t
φ : r ↪r r'
⊢ IsChain r ((⇑φ : (a : α) → β) ⁻¹' t)

Tactic:
ht.preimage _ _ _ φ.injective (fun _ _ h ↦ φ.map_rel_iff.mp h)

Premises used: IsChain.preimage, RelEmbedding.injective, RelEmbedding.map_rel_iff, Iff.mp
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsChain r s
φ : r ≃r r'
⊢ IsChain r' ((⇑φ : (a : α) → β) '' s)

Tactic:
hs.image φ.toRelEmbedding

Premises used: IsChain.image, RelIso.toRelEmbedding
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
t : Set β
hs : IsChain r' t
φ : r ≃r r'
⊢ IsChain r ((⇑φ : (a : α) → β) ⁻¹' t)

Tactic:
hs.preimage_relEmbedding φ.toRelEmbedding

Premises used: RelIso.toRelEmbedding, IsChain.preimage_relEmbedding
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
φ : r ↪r r'
⊢ IsChain r' ((⇑φ : (a : α) → β) '' s) ↔ IsChain r s

Tactic:
⟨fun h => (φ.injective.preimage_image s).subst (h.preimage_relEmbedding φ), fun h => h.image φ⟩

Premises used: RelEmbedding.injective, IsChain.image, Eq.subst, Function.Injective.preimage_image, Iff.intro, IsChain.preimage_relEmbedding
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
φ : r ≃r r'
⊢ IsChain r' ((⇑φ : (a : α) → β) '' s) ↔ IsChain r s

Tactic:
@image_relEmbedding_iff _ _ _ _ _ (φ : r ↪r r')

Premises used: IsChain.image_relEmbedding_iff
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : LE α
inst_1 : LE β
hs : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
φ : α ↪o β
⊢ IsChain (fun (x1 x2 : β) ↦ x1 ≤ x2) ((⇑φ : (a : α) → β) '' s)

Tactic:
image hs _

Premises used: IsChain.image
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
t : Set β
ht : IsChain (fun (x1 x2 : β) ↦ x1 ≤ x2) t
φ : α ↪o β
⊢ IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) ((⇑φ : (a : α) → β) ⁻¹' t)

Tactic:
preimage_relEmbedding ht _

Premises used: IsChain.preimage_relEmbedding
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : LE α
inst_1 : LE β
φ : α ↪o β
⊢ IsChain (fun (x1 x2 : β) ↦ x1 ≤ x2) ((⇑φ : (a : α) → β) '' s) ↔ IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
image_relEmbedding_iff

Premises used: IsChain.image_relEmbedding_iff
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : LE α
inst_1 : LE β
hs : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
φ : α ≃o β
⊢ IsChain (fun (x1 x2 : β) ↦ x1 ≤ x2) ((⇑φ : (a : α) → β) '' s)

Tactic:
image hs _

Premises used: IsChain.image
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : LE α
inst_1 : LE β
φ : α ≃o β
⊢ IsChain (fun (x1 x2 : β) ↦ x1 ≤ x2) ((⇑φ : (a : α) → β) '' s) ↔ IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
image_relEmbedding_iff

Premises used: IsChain.image_relEmbedding_iff
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
t : Set β
ht : IsChain (fun (x1 x2 : β) ↦ x1 ≤ x2) t
φ : α ≃o β
⊢ IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) ((⇑φ : (a : α) → β) ⁻¹' t)

Tactic:
preimage_relEmbedding ht _

Premises used: IsChain.preimage_relEmbedding
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
t : Set β
φ : α ≃o β
⊢ IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) ((⇑φ : (a : α) → β) ⁻¹' t) ↔ IsChain (fun (x1 x2 : β) ↦ x1 ≤ x2) t

Tactic:
⟨fun h => (φ.image_preimage t).subst (h.image φ), fun h => h.preimage_iso _⟩

Premises used: IsChain.preimage_iso, IsChain.image, Eq.subst, Iff.intro, OrderIso.image_preimage
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
x y : α
inst : Std.Refl r
h : IsChain r s
hx : x ∈ s
hy : y ∈ s
⊢ r x y ∨ r y x

Tactic:
(eq_or_ne x y).elim (fun e => Or.inl <| e ▸ refl _) (h hx hy)

Premises used: Eq.rec, eq_or_ne, Or.inl, Or.elim, refl
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Refl r
H : IsChain r s
⊢ DirectedOn r s

Tactic:
fun x hx y hy =>
  ((H.total hx hy).elim fun h => ⟨y, hy, h, refl _⟩) fun h => ⟨x, hx, refl _, h⟩

Premises used: DirectedOn, And.intro, Exists.intro, Or.elim, refl, IsChain.total
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
inst : Std.Refl r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x x_1 : { a : β // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
simp : ∃ a ∈ c, r (f b) (f a)
⊢ ∃ (z : { a : β // a ∈ c }),
    r ((fun (x : { a : β // a ∈ c }) ↦ f (↑x : β)) (Subtype.mk (p := fun (a : β) ↦ a ∈ c) a ha))
        ((fun (x : { a : β // a ∈ c }) ↦ f (↑x : β)) z) ∧
      r ((fun (x : { a : β // a ∈ c }) ↦ f (↑x : β)) (Subtype.mk (p := fun (a : β) ↦ a ∈ c) b hb))
        ((fun (x : { a : β // a ∈ c }) ↦ f (↑x : β)) z)

Tactic:
simp only [hab, exists_prop, and_self_iff, Subtype.exists]

Premises used: Subtype.exists, exists_prop, and_self_iff
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
inst : Std.Refl r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x x_1 : { a : β // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
⊢ ∃ a ∈ c, r (f b) (f a)

Tactic:
⟨b, hb, refl _⟩

Premises used: And.intro, Exists.intro, refl
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
inst : Std.Refl r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x x_1 : { a : β // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
⊢ ∃ a ∈ c, r (f b) (f a)

Tactic:
exact ⟨b, hb, refl _⟩
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Refl r
hchain : IsChain r s
inst_1 : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
rcases : ∀ (z : α) (mem4 : z ∈ s) (H1 : r a z) (H2 : r b z), ∃ (z : α) (_ : z ∈ s), r a z ∧ r b z ∧ r c z
⊢ ∃ (z : α) (_ : z ∈ s), r a z ∧ r b z ∧ r c z

Tactic:
rcases directedOn_iff_directed.mpr (IsChain.directed hchain) a mem1 b mem2 with ⟨z, mem4, H1, H2⟩

Premises used: Iff.mpr, IsChain.directed, directedOn_iff_directed
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Refl r
hchain : IsChain r s
inst_1 : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
z : α
mem4 : z ∈ s
H1 : r a z
H2 : r b z
rcases : ∀ (z' : α) (mem5 : z' ∈ s) (H3 : r z z') (H4 : r c z'), ∃ (z : α) (_ : z ∈ s), r a z ∧ r b z ∧ r c z
⊢ ∃ (z : α) (_ : z ∈ s), r a z ∧ r b z ∧ r c z

Tactic:
rcases directedOn_iff_directed.mpr (IsChain.directed hchain) z mem4 c mem3 with
    ⟨z', mem5, H3, H4⟩

Premises used: Iff.mpr, IsChain.directed, directedOn_iff_directed
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Refl r
hchain : IsChain r s
inst_1 : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
z : α
mem4 : z ∈ s
H1 : r a z
H2 : r b z
z' : α
mem5 : z' ∈ s
H3 : r z z'
H4 : r c z'
⊢ ∃ (z : α) (_ : z ∈ s), r a z ∧ r b z ∧ r c z

Tactic:
⟨z', mem5, _root_.trans H1 H3, _root_.trans H2 H3, H4⟩

Premises used: trans, And.intro, Exists.intro
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Refl r
hchain : IsChain r s
inst_1 : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
z : α
mem4 : z ∈ s
H1 : r a z
H2 : r b z
z' : α
mem5 : z' ∈ s
H3 : r z z'
H4 : r c z'
⊢ ∃ (z : α) (_ : z ∈ s), r a z ∧ r b z ∧ r c z

Tactic:
exact ⟨z', mem5, _root_.trans H1 H3, _root_.trans H2 H3, H4⟩
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x < y
h' : y ≤ x
⊢ y ≤ x

Tactic:
h'
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x < y
h' : y ≤ x
⊢ y ≤ x

Tactic:
exact h'
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x < y
h' : x ≤ y
⊢ y ≤ x

Tactic:
simpa [lt_iff_le_not_ge, h'] using h

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x < y
⊢ x ≤ y ∨ y ≤ x

Tactic:
cases hs.total hx hy with
  | inr h' => exact h'
  | inl h' => simpa [lt_iff_le_not_ge, h'] using h

Premises used: lt_iff_le_not_ge, IsChain.total
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ ¬x < y ↔ y ≤ x

Tactic:
⟨(hs.le_of_not_gt hx hy ·), fun h h' ↦ h'.not_ge h⟩

Premises used: Iff.intro, LT.lt.not_ge, IsChain.le_of_not_gt
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x ≤ y
⊢ y < x

Tactic:
(hs.total hx hy).elim (h · |>.elim) (lt_of_le_not_ge · h)

Premises used: False.elim, lt_of_le_not_ge, Or.elim, IsChain.total
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ ¬x ≤ y ↔ y < x

Tactic:
⟨(hs.lt_of_not_ge hx hy ·), fun h h' ↦ h'.not_gt h⟩

Premises used: IsChain.lt_of_not_ge, LE.le.not_gt, Iff.intro
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
⊢ IsChain r s

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
h : IsMaxChain r s
⊢ ¬SuperChain r s t

Tactic:
fun ht =>
  ht.2.ne <| h.2 ht.1 ht.2.1

Premises used: And.right, And.left, HasSSubset.SSubset.ne, Not
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
s : Set α
inst : LE α
inst_1 : OrderBot α
h : IsMaxChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ ⊥ ∈ s

Tactic:
(h.2 (h.1.insert fun _ _ _ => Or.inl bot_le) <| subset_insert _ _).symm ▸ mem_insert _ _

Premises used: Eq.rec, And.right, And.left, Set.mem_insert, Or.inl, IsChain.insert, Eq.symm, bot_le, Set.subset_insert
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
s : Set α
inst : LE α
inst_1 : OrderTop α
h : IsMaxChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ ⊤ ∈ s

Tactic:
(h.2 (h.1.insert fun _ _ _ => Or.inr le_top) <| subset_insert _ _).symm ▸ mem_insert _ _

Premises used: Eq.rec, And.right, And.left, le_top, Set.mem_insert, IsChain.insert, Eq.symm, Set.subset_insert, Or.inr
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxChain r c
t : Set β
ht : IsChain s t
hf : (⇑e : (a : α) → β) '' c ⊆ t
rw : c = (⇑e.toEquiv (r := r) (s := s).symm : (a : β) → α) '' t
⊢ (⇑e : (a : α) → β) '' c = t

Tactic:
rw [← e.coe_fn_toEquiv, ← e.toEquiv.eq_preimage_iff_image_eq, ← Equiv.image_symm_eq_preimage]

Premises used: Equiv.eq_preimage_iff_image_eq, RelIso.toEquiv, RelIso.coe_fn_toEquiv, Equiv.image_symm_eq_preimage
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxChain r c
t : Set β
ht : IsChain s t
hf : (⇑e : (a : α) → β) '' c ⊆ t
⊢ c = (⇑e.toEquiv (r := r) (s := s).symm : (a : β) → α) '' t

Tactic:
hc.2 (ht.image e.symm) ((e.toEquiv.subset_symm_image _ _).2 hf)

Premises used: Iff.mpr, IsChain.image, RelIso.symm, And.right, Equiv.subset_symm_image, RelIso.toEquiv
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxChain r c
t : Set β
ht : IsChain s t
hf : (⇑e : (a : α) → β) '' c ⊆ t
⊢ c = (⇑e.toEquiv (r := r) (s := s).symm : (a : β) → α) '' t

Tactic:
exact hc.2 (ht.image e.symm) ((e.toEquiv.subset_symm_image _ _).2 hf)

Premises used: Iff.mpr, IsChain.image, RelIso.symm, And.right, Equiv.subset_symm_image, RelIso.toEquiv
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
⊢ IsEmpty α ↔ s = ∅

Tactic:
⟨fun _ ↦ s.eq_empty_of_isEmpty, fun h' ↦ ?_⟩

Premises used: Iff.intro, Set.eq_empty_of_isEmpty
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
refine : ∀ (h' : s = ∅), IsEmpty α
⊢ IsEmpty α ↔ s = ∅

Tactic:
refine ⟨fun _ ↦ s.eq_empty_of_isEmpty, fun h' ↦ ?_⟩
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
h' : s = ∅
false : ∀ (a : α), False
⊢ IsEmpty α

Tactic:
constructor
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
h' : s = ∅
x : α
⊢ ∀ ⦃t : Set α⦄, IsChain r t → ∅ = t

Tactic:
simp only [IsMaxChain, h', IsChain.empty, empty_subset, forall_const, true_and] at h

Premises used: IsMaxChain, IsChain.empty, Set.empty_subset, forall_const, true_and
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h' : s = ∅
x : α
h : ∀ ⦃t : Set α⦄, IsChain r t → ∅ = t
⊢ False

Tactic:
singleton_ne_empty x (h IsChain.singleton).symm

Premises used: IsChain.singleton, Eq.symm, Set.singleton_ne_empty
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h' : s = ∅
x : α
h : ∀ ⦃t : Set α⦄, IsChain r t → ∅ = t
⊢ False

Tactic:
exact singleton_ne_empty x (h IsChain.singleton).symm

Premises used: IsChain.singleton, Eq.symm, Set.singleton_ne_empty
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
⊢ ¬Nonempty α ↔ ¬s.Nonempty

Tactic:
simpa [Set.not_nonempty_iff_eq_empty] using h.isEmpty_iff

Premises used: Set.not_nonempty_iff_eq_empty, IsMaxChain.isEmpty_iff
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
⊢ IsMaxChain (flip r) s

Tactic:
⟨h.isChain.symm, fun _ ht₁ ht₂ ↦ h.2 ht₁.symm ht₂⟩

Premises used: IsChain.symm, IsMaxChain, IsMaxChain.isChain, And.right, And.intro
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : ∃ (t : Set α), IsChain r s ∧ SuperChain r s t
⊢ IsChain r s ∧ SuperChain r s (h.choose (p := fun (t : Set α) ↦ IsChain r s ∧ SuperChain r s t))

Tactic:
have : IsChain r s ∧ SuperChain r s h.choose := h.choose_spec
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : ∃ (t : Set α), IsChain r s ∧ SuperChain r s t
this : IsChain r s ∧ SuperChain r s (h.choose (p := fun (t : Set α) ↦ IsChain r s ∧ SuperChain r s t))
⊢ SuperChain r s (SuccChain r s)

Tactic:
simpa [SuccChain, dif_pos, exists_and_left.mp h] using this.2

Premises used: exists_and_left, dif_pos, SuccChain, And.right, Iff.mp
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ¬∃ (t : Set α), IsChain r s ∧ SuperChain r s t
⊢ ¬(IsChain r s ∧ ∃ (x : Set α), SuperChain r s x)

Tactic:
rw [exists_and_left] at h

Premises used: exists_and_left
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ¬(IsChain r s ∧ ∃ (x : Set α), SuperChain r s x)
⊢ IsChain r (SuccChain r s)

Tactic:
simpa [SuccChain, dif_neg, h] using hs

Premises used: dif_neg, SuccChain
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : ¬IsMaxChain r s
⊢ IsChain r s → ∃ (x : Set α), IsChain r x ∧ s ⊆ x ∧ ¬s = x

Tactic:
simp only [IsMaxChain, _root_.not_and, not_forall, exists_prop] at hs₂

Premises used: IsMaxChain, exists_prop, not_and, Classical.not_forall
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ (x : Set α), IsChain r x ∧ s ⊆ x ∧ ¬s = x
obtain : ∀ (t : Set α) (ht : IsChain r t) (hst : s ⊆ t ∧ ¬s = t), SuperChain r s (SuccChain r s)
⊢ SuperChain r s (SuccChain r s)

Tactic:
obtain ⟨t, ht, hst⟩ := hs₂ hs₁
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ (x : Set α), IsChain r x ∧ s ⊆ x ∧ ¬s = x
t : Set α
ht : IsChain r t
hst : s ⊆ t ∧ ¬s = t
⊢ SuperChain r s (SuccChain r s)

Tactic:
succChain_spec ⟨t, hs₁, ht, ssubset_iff_subset_ne.2 hst⟩

Premises used: Iff.mpr, succChain_spec, And.intro, Exists.intro, ssubset_iff_subset_ne
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ (x : Set α), IsChain r x ∧ s ⊆ x ∧ ¬s = x
t : Set α
ht : IsChain r t
hst : s ⊆ t ∧ ¬s = t
⊢ SuperChain r s (SuccChain r s)

Tactic:
exact succChain_spec ⟨t, hs₁, ht, ssubset_iff_subset_ne.2 hst⟩

Premises used: Iff.mpr, succChain_spec, And.intro, Exists.intro, ssubset_iff_subset_ne
-- Module: Mathlib.Order.Preorder.Chain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : ¬∃ (t : Set α), IsChain r s ∧ SuperChain r s t
⊢ s ⊆ SuccChain r s

Tactic:
simp [SuccChain, h]

Premises used: SuccChain