awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : (↑n : ℕ∞) ≤ s.chainHeight r
h' : ¬n = 0
neg :
  ∀ (t : Set α) (ht₁ : t ⊆ s) (ht₂ : IsChain r t) (ht₃ : (↑n : ℕ∞) ≤ t.encard),
    ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
⊢ ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t

Tactic:
obtain ⟨t, ht₁, ht₂, ht₃⟩ : ∃ t ⊆ s, IsChain r t ∧ n ≤ t.encard := by
      contrapose! h
      refine iSup_lt_iff.mpr ⟨n - 1, ?_, fun m ↦ ENat.le_sub_one_of_lt <| h m.1 m.2.1 m.2.2⟩
      exact_mod_cast Nat.sub_one_lt h'
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : (↑n : ℕ∞) ≤ s.chainHeight r
h' : ¬n = 0
t : Set α
ht₁ : t ⊆ s
ht₂ : IsChain r t
ht₃ : (↑n : ℕ∞) ≤ t.encard
neg : ∀ (u : Set α) (hu₁ : u ⊆ t) (hu₂ : u.encard = (↑n : ℕ∞)), ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
⊢ ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t

Tactic:
obtain ⟨u, hu₁, hu₂⟩ := exists_subset_encard_eq ht₃

Premises used: Set.exists_subset_encard_eq
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : (↑n : ℕ∞) ≤ s.chainHeight r
h' : ¬n = 0
t : Set α
ht₁ : t ⊆ s
ht₂ : IsChain r t
ht₃ : (↑n : ℕ∞) ≤ t.encard
u : Set α
hu₁ : u ⊆ t
hu₂ : u.encard = (↑n : ℕ∞)
⊢ ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t

Tactic:
⟨u, hu₁.trans ht₁, hu₂, ht₂.mono hu₁⟩

Premises used: HasSubset.Subset.trans, IsChain.mono, And.intro, Exists.intro
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : (↑n : ℕ∞) ≤ s.chainHeight r
h' : ¬n = 0
t : Set α
ht₁ : t ⊆ s
ht₂ : IsChain r t
ht₃ : (↑n : ℕ∞) ≤ t.encard
u : Set α
hu₁ : u ⊆ t
hu₂ : u.encard = (↑n : ℕ∞)
⊢ ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t

Tactic:
exact ⟨u, hu₁.trans ht₁, hu₂, ht₂.mono hu₁⟩
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
⊢ ∅ ⊆ s ∧ IsChain r ∅

Tactic:
simp
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
⊢ Nonempty.{max 1 (u_1 + 1)} { t : Set α // t ⊆ s ∧ IsChain r t }

Tactic:
have : Nonempty { t // t ⊆ s ∧ IsChain r t } := ⟨∅, by simp⟩
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
this : Nonempty.{max 1 (u_1 + 1)} { t : Set α // t ⊆ s ∧ IsChain r t }
rwa : s.chainHeight r < ⊤
s₁ : Set α
r₁ : α → α → Prop
rwa₁ : Type u_1
rwa₂ : s.chainHeight r ≠ ⊤
s₂ : Set α
r₂ : α → α → Prop
rwa₃ : Type u_1
rwa₄ : s.chainHeight r ≠ ⊤
s₃ : Set α
r₃ : α → α → Prop
rwa₅ : Type u_1
rwa₆ : s.chainHeight r ≠ ⊤
s₄ : Set α
r₄ : α → α → Prop
rwa₇ : Type u_1
rwa₈ : s.chainHeight r ≠ ⊤
s₅ : Set α
r₅ : α → α → Prop
rwa₉ : Type u_1
⊢ LT.lt (α := ℕ∞) (⨆ (i : { t : Set α // t ⊆ s ∧ IsChain r t }), (↑i : Set α).encard) ⊤

Tactic:
rwa [← chainHeight_eq_iSup, lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top, Set.chainHeight_eq_iSup
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
this : Nonempty.{max 1 (u_1 + 1)} { t : Set α // t ⊆ s ∧ IsChain r t }
obtain :
  ∀ (t : { t : Set α // t ⊆ s ∧ IsChain r t })
    (ht : (↑t : Set α).encard = ⨆ (i : { t : Set α // t ⊆ s ∧ IsChain r t }), (↑i : Set α).encard),
    ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t
⊢ ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t

Tactic:
obtain ⟨t, ht⟩ := exists_eq_iSup_of_lt_top (by rwa [← chainHeight_eq_iSup, lt_top_iff_ne_top])

Premises used: ENat.exists_eq_iSup_of_lt_top
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
this : Nonempty.{max 1 (u_1 + 1)} { t : Set α // t ⊆ s ∧ IsChain r t }
t : { t : Set α // t ⊆ s ∧ IsChain r t }
ht : (↑t : Set α).encard = ⨆ (i : { t : Set α // t ⊆ s ∧ IsChain r t }), (↑i : Set α).encard
⊢ ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t

Tactic:
⟨t.1, t.2.1, ht, t.2.2⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
this : Nonempty.{max 1 (u_1 + 1)} { t : Set α // t ⊆ s ∧ IsChain r t }
t : { t : Set α // t ⊆ s ∧ IsChain r t }
ht : (↑t : Set α).encard = ⨆ (i : { t : Set α // t ⊆ s ∧ IsChain r t }), (↑i : Set α).encard
⊢ ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t

Tactic:
exact ⟨t.1, t.2.1, ht, t.2.2⟩
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.Finite
⊢ ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t

Tactic:
exists_eq_chainHeight_of_chainHeight_ne_top s r (chainHeight_ne_top_of_finite s r h)

Premises used: Set.exists_eq_chainHeight_of_chainHeight_ne_top, Set.chainHeight_ne_top_of_finite
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
hs : t ⊆ s
hc : IsChain r t
⊢ t.encard ≤ s.chainHeight r

Tactic:
le_iSup_iff.mpr fun _ hb ↦ hb ⟨t, hs, hc⟩

Premises used: Set.chainHeight, Iff.mpr, Subtype.mk, And.intro, le_iSup_iff
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hc : IsChain r s
⊢ s.encard = s.chainHeight r

Tactic:
le_antisymm (encard_le_chainHeight_of_isChain _ _ Set.Subset.rfl hc) (chainHeight_le_encard _ _)

Premises used: Set.chainHeight_le_encard, le_antisymm, Set.Subset.rfl, Set.encard_le_chainHeight_of_isChain
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hc : IsChain r s
h : s.chainHeight r ≠ ⊤
⊢ s.Finite

Tactic:
Set.encard_ne_top_iff.mp <| ne_top_of_le_ne_top h <|
    encard_le_chainHeight_of_isChain _ _ (subset_refl _) hc

Premises used: subset_refl, ne_top_of_le_ne_top, Iff.mp, Set.encard_le_chainHeight_of_isChain, Set.encard_ne_top_iff
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
ht : t ⊆ s
he : s.chainHeight r < t.encard
by_contra! : ∀ (hh : IsChain r t), False
⊢ ¬IsChain r t

Tactic:
by_contra! hh
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
ht : t ⊆ s
he : s.chainHeight r < t.encard
hh : IsChain r t
⊢ s.chainHeight r < s.chainHeight r

Tactic:
grw [encard_le_chainHeight_of_isChain _ _ ht hh] at he

Premises used: Set.encard_le_chainHeight_of_isChain
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
ht : t ⊆ s
he : s.chainHeight r < t.encard
hh : IsChain r t
he₁ : s.chainHeight r < s.chainHeight r
⊢ IsChain r t

Tactic:
grw [encard_le_chainHeight_of_isChain _ _ ht hh] at he

Premises used: Set.encard_le_chainHeight_of_isChain
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
ht : t ⊆ s
he : s.chainHeight r < s.chainHeight r
hh : IsChain r t
⊢ False

Tactic:
(lt_self_iff_false _).mp he

Premises used: lt_self_iff_false, Iff.mp
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
ht : t ⊆ s
he : s.chainHeight r < s.chainHeight r
hh : IsChain r t
⊢ False

Tactic:
exact (lt_self_iff_false _).mp he

Premises used: lt_self_iff_false, Iff.mp
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight r = ⊤ ↔ ∀ (n : ℕ), ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t

Tactic:
⟨fun h _ ↦ exists_isChain_of_le_chainHeight _ (le_top.trans_eq h.symm), fun h ↦ ?_⟩

Premises used: LE.le.trans_eq, le_top, Iff.intro, Set.exists_isChain_of_le_chainHeight, Eq.symm
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
refine : ∀ (h : ∀ (n : ℕ), ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t), s.chainHeight r = ⊤
⊢ s.chainHeight r = ⊤ ↔ ∀ (n : ℕ), ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t

Tactic:
refine ⟨fun h _ ↦ exists_isChain_of_le_chainHeight _ (le_top.trans_eq h.symm), fun h ↦ ?_⟩
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : ∀ (n : ℕ), ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
contrapose! : ∀ (h : s.chainHeight r ≠ ⊤), ∃ (n : ℕ), ∀ (t : Set α) (_ : t ⊆ s) (_ : t.encard = (↑n : ℕ∞)), ¬IsChain r t
⊢ s.chainHeight r = ⊤

Tactic:
contrapose! h
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
obtain :
  ∀ (n : ℕ) (hn : (↑n : WithTop ℕ) = s.chainHeight r),
    ∃ (n : ℕ), ∀ (t : Set α) (_ : t ⊆ s) (_ : t.encard = (↑n : ℕ∞)), ¬IsChain r t
⊢ ∃ (n : ℕ), ∀ (t : Set α) (_ : t ⊆ s) (_ : t.encard = (↑n : ℕ∞)), ¬IsChain r t

Tactic:
obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.1 h

Premises used: WithTop.ne_top_iff_exists, Iff.mp
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = s.chainHeight r
⊢ ∃ (n : ℕ), ∀ (t : Set α) (_ : t ⊆ s) (_ : t.encard = (↑n : ℕ∞)), ¬IsChain r t

Tactic:
⟨n + 1, fun l hl he ↦ not_isChain_of_chainHeight_lt_encard r s l hl ?_⟩

Premises used: Set.not_isChain_of_chainHeight_lt_encard, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = s.chainHeight r
refine : ∀ (l : Set α) (hl : l ⊆ s) (he : l.encard = (↑(n + 1) : ℕ∞)), s.chainHeight r < l.encard
⊢ ∃ (n : ℕ), ∀ (t : Set α) (_ : t ⊆ s) (_ : t.encard = (↑n : ℕ∞)), ¬IsChain r t

Tactic:
refine ⟨n + 1, fun l hl he ↦ not_isChain_of_chainHeight_lt_encard r s l hl ?_⟩
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = s.chainHeight r
l : Set α
hl : l ⊆ s
he : l.encard = (↑(n + 1) : ℕ∞)
rw : n < n + 1
⊢ s.chainHeight r < l.encard

Tactic:
rw [← hn, some_eq_coe, he, Nat.cast_lt]

Premises used: ENat.some_eq_coe, Nat.cast_lt
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = s.chainHeight r
l : Set α
hl : l ⊆ s
he : l.encard = (↑(n + 1) : ℕ∞)
⊢ n < n + 1

Tactic:
lt_add_one _

Premises used: lt_add_one
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
n : ℕ
hn : (↑n : WithTop ℕ) = s.chainHeight r
l : Set α
hl : l ⊆ s
he : l.encard = (↑(n + 1) : ℕ∞)
⊢ n < n + 1

Tactic:
exact lt_add_one _

Premises used: lt_add_one
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight r = 0 ↔ s = ∅

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
refine_1 : ∀ (h : s.chainHeight r = 0), s = ∅
refine_2 : s = ∅ → s.chainHeight r = 0
⊢ s.chainHeight r = 0 ↔ s = ∅

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r = 0
⊢ ∀ a ⊆ s, IsChain r a → a = ∅

Tactic:
simp only [chainHeight, iSup_eq_zero, encard_eq_zero, Subtype.forall, and_imp] at h

Premises used: Set.chainHeight, Set.encard_eq_zero, and_imp, Subtype.forall, ENat.iSup_eq_zero
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : ∀ a ⊆ s, IsChain r a → a = ∅
refine_1 : ∀ (x : α), x ∈ s ↔ Membership.mem (γ := Set α) ∅ x
⊢ s = ∅

Tactic:
ext x
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : ∀ a ⊆ s, IsChain r a → a = ∅
x : α
⊢ x ∈ s ↔ Membership.mem (γ := Set α) ∅ x

Tactic:
simpa using h {x}

Premises used: Singleton.singleton
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
⊢ s = ∅ → s.chainHeight r = 0

Tactic:
simp_all [chainHeight]

Premises used: Set.chainHeight
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
⊢ chainHeight ∅ r = 0

Tactic:
chainHeight_eq_zero_iff _ _ |>.mpr rfl

Premises used: Iff.mpr, Set.chainHeight_eq_zero_iff, rfl
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
mp : 1 ≤ s.chainHeight r → s.Nonempty
mpr : s.Nonempty → 1 ≤ s.chainHeight r
⊢ 1 ≤ s.chainHeight r ↔ s.Nonempty

Tactic:
constructor
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : 1 ≤ s.chainHeight r
mp : ∀ (hh : s = ∅), False
⊢ s.Nonempty

Tactic:
by_contra! hh
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : 1 ≤ s.chainHeight r
hh : s = ∅
⊢ False

Tactic:
simp_all [lt_one_iff_eq_zero]

Premises used: ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.Nonempty
mpr : ∀ (hh : s.chainHeight r < 1), False
⊢ 1 ≤ s.chainHeight r

Tactic:
by_contra! hh
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.Nonempty
hh : s.chainHeight r < 1
⊢ False

Tactic:
simp_all [lt_one_iff_eq_zero]

Premises used: ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
inst : IsEmpty α
⊢ s.chainHeight r = 0

Tactic:
chainHeight_eq_zero_iff s r |>.mpr (Subsingleton.elim _ _)

Premises used: Iff.mpr, Subsingleton.elim, Set.chainHeight_eq_zero_iff
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
h : s ⊆ t
⊢ s.chainHeight r ≤ t.chainHeight r

Tactic:
forall_natCast_le_iff_le.mp fun n hn ↦ ?_

Premises used: ENat.forall_natCast_le_iff_le, Iff.mp
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
h : s ⊆ t
refine : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ s.chainHeight r), (↑n : ℕ∞) ≤ t.chainHeight r
⊢ s.chainHeight r ≤ t.chainHeight r

Tactic:
refine forall_natCast_le_iff_le.mp fun n hn ↦ ?_

Premises used: ENat.forall_natCast_le_iff_le, Iff.mp
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
h : s ⊆ t
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight r
obtain : ∀ (a : Set α) (ha₁ : a ⊆ s) (ha₂ : a.encard = (↑n : ℕ∞)) (ha₃ : IsChain r a), (↑n : ℕ∞) ≤ t.chainHeight r
⊢ (↑n : ℕ∞) ≤ t.chainHeight r

Tactic:
obtain ⟨a, ha₁, ha₂, ha₃⟩ := exists_isChain_of_le_chainHeight n hn

Premises used: Set.exists_isChain_of_le_chainHeight
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
h : s ⊆ t
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain r a
⊢ (↑n : ℕ∞) ≤ t.chainHeight r

Tactic:
ha₂ ▸ encard_le_chainHeight_of_isChain _ _ (ha₁.trans h) ha₃

Premises used: Eq.rec, HasSubset.Subset.trans, Set.encard_le_chainHeight_of_isChain
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
h : s ⊆ t
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain r a
⊢ (↑n : ℕ∞) ≤ t.chainHeight r

Tactic:
exact ha₂ ▸ encard_le_chainHeight_of_isChain _ _ (ha₁.trans h) ha₃
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight (flip r) = s.chainHeight r

Tactic:
eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩

Premises used: ENat.eq_of_forall_natCast_le_iff, Iff.intro
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
refine_1 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ s.chainHeight (flip r)), (↑n : ℕ∞) ≤ s.chainHeight r
refine_2 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ s.chainHeight r), (↑n : ℕ∞) ≤ s.chainHeight (flip r)
⊢ s.chainHeight (flip r) = s.chainHeight r

Tactic:
refine eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩

Premises used: ENat.eq_of_forall_natCast_le_iff, Iff.intro
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight (flip r)
refine_1 :
  ∀ (a : Set α) (ha₁ : a ⊆ s) (ha₂ : a.encard = (↑n : ℕ∞)) (ha₃ : IsChain (flip r) a), (↑n : ℕ∞) ≤ s.chainHeight r
⊢ (↑n : ℕ∞) ≤ s.chainHeight r

Tactic:
obtain ⟨a, ha₁, ha₂, ha₃⟩ := exists_isChain_of_le_chainHeight n hn

Premises used: Set.exists_isChain_of_le_chainHeight
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight (flip r)
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain (flip r) a
x : α
hx : x ∈ a
x_1 : α
hy : x_1 ∈ a
hne : x ≠ x_1
⊢ (fun (x y : α) ↦ r x y ∨ r y x) x x_1

Tactic:
simpa [flip, Or.comm] using ha₃ hx hy hne

Premises used: Or.comm, flip
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight (flip r)
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain (flip r) a
⊢ (↑n : ℕ∞) ≤ s.chainHeight r

Tactic:
exact ha₂ ▸ encard_le_chainHeight_of_isChain _ _ ha₁ <|
      fun _ hx _ hy hne ↦ by simpa [flip, Or.comm] using ha₃ hx hy hne
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight r
refine_2 :
  ∀ (a : Set α) (ha₁ : a ⊆ s) (ha₂ : a.encard = (↑n : ℕ∞)) (ha₃ : IsChain r a), (↑n : ℕ∞) ≤ s.chainHeight (flip r)
⊢ (↑n : ℕ∞) ≤ s.chainHeight (flip r)

Tactic:
obtain ⟨a, ha₁, ha₂, ha₃⟩ := exists_isChain_of_le_chainHeight n hn

Premises used: Set.exists_isChain_of_le_chainHeight
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain r a
x : α
hx : x ∈ a
x_1 : α
hy : x_1 ∈ a
hne : x ≠ x_1
⊢ (fun (x y : α) ↦ flip r x y ∨ flip r y x) x x_1

Tactic:
simpa [flip, Or.comm] using ha₃ hx hy hne

Premises used: Or.comm, flip
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain r a
⊢ (↑n : ℕ∞) ≤ s.chainHeight (flip r)

Tactic:
exact ha₂ ▸ encard_le_chainHeight_of_isChain _ _ ha₁ <|
      fun _ hx _ hy hne ↦ by simpa [flip, Or.comm] using ha₃ hx hy hne
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
⊢ chainHeight ((⇑e : (a : α) → β) '' s) r' = s.chainHeight r

Tactic:
eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩

Premises used: ENat.eq_of_forall_natCast_le_iff, Iff.intro
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
refine_1 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'), (↑n : ℕ∞) ≤ s.chainHeight r
refine_2 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ s.chainHeight r), (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
⊢ chainHeight ((⇑e : (a : α) → β) '' s) r' = s.chainHeight r

Tactic:
refine eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩

Premises used: ENat.eq_of_forall_natCast_le_iff, Iff.intro
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
refine_1 :
  ∀ (a : Set β) (ha₁ : a ⊆ (⇑e : (a : α) → β) '' s) (ha₂ : a.encard = (↑n : ℕ∞)) (ha₃ : IsChain r' a),
    (↑n : ℕ∞) ≤ s.chainHeight r
⊢ (↑n : ℕ∞) ≤ s.chainHeight r

Tactic:
obtain ⟨a, ha₁, ha₂, ha₃⟩ := exists_isChain_of_le_chainHeight n hn

Premises used: Set.exists_isChain_of_le_chainHeight
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
a : Set β
ha₁ : a ⊆ (⇑e : (a : α) → β) '' s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain r' a
⊢ a ⊆ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β)

Tactic:
grind
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
a : Set β
ha₁ : a ⊆ (⇑e : (a : α) → β) '' s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain r' a
refine_1 : encard.{u_1} (α := α) ((⇑e : (a : α) → β) ⁻¹' a) ≤ s.chainHeight r
⊢ (↑n : ℕ∞) ≤ s.chainHeight r

Tactic:
rw [← ha₂, ← Set.encard_preimage_of_injective_subset_range e.injective (by grind)]

Premises used: RelEmbedding.injective, Set.encard_preimage_of_injective_subset_range
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
a : Set β
ha₁ : a ⊆ (⇑e : (a : α) → β) '' s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain r' a
⊢ encard.{u_1} (α := α) ((⇑e : (a : α) → β) ⁻¹' a) ≤ s.chainHeight r

Tactic:
encard_le_chainHeight_of_isChain _ _ (preimage_subset ha₁ e.injective.injOn) <|
      ha₃.preimage_relEmbedding e

Premises used: Function.Injective.injOn, RelEmbedding.injective, Set.encard_le_chainHeight_of_isChain, IsChain.preimage_relEmbedding, Set.preimage_subset
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
a : Set β
ha₁ : a ⊆ (⇑e : (a : α) → β) '' s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain r' a
⊢ encard.{u_1} (α := α) ((⇑e : (a : α) → β) ⁻¹' a) ≤ s.chainHeight r

Tactic:
exact encard_le_chainHeight_of_isChain _ _ (preimage_subset ha₁ e.injective.injOn) <|
      ha₃.preimage_relEmbedding e

Premises used: Function.Injective.injOn, RelEmbedding.injective, Set.encard_le_chainHeight_of_isChain, IsChain.preimage_relEmbedding, Set.preimage_subset
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight r
refine_2 :
  ∀ (a : Set α) (ha₁ : a ⊆ s) (ha₂ : a.encard = (↑n : ℕ∞)) (ha₃ : IsChain r a),
    (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
⊢ (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'

Tactic:
obtain ⟨a, ha₁, ha₂, ha₃⟩ := exists_isChain_of_le_chainHeight n hn

Premises used: Set.exists_isChain_of_le_chainHeight
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain r a
refine_2 : encard.{u_2} (α := β) ((⇑e : (a : α) → β) '' a) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'
⊢ (↑n : ℕ∞) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'

Tactic:
rw [← ha₂, ← e.injective.encard_image]

Premises used: RelEmbedding.injective, Function.Injective.encard_image
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain r a
⊢ Subset.{u_2} (α := Set β) ((⇑e : (a : α) → β) '' a) ((⇑e : (a : α) → β) '' s)

Tactic:
grind
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : (↑n : ℕ∞) ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = (↑n : ℕ∞)
ha₃ : IsChain r a
⊢ encard.{u_2} (α := β) ((⇑e : (a : α) → β) '' a) ≤ chainHeight ((⇑e : (a : α) → β) '' s) r'

Tactic:
exact encard_le_chainHeight_of_isChain _ _ (by grind) <| ha₃.image e

Premises used: IsChain.image, Set.encard_le_chainHeight_of_isChain
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ≃r r'
⊢ chainHeight ((⇑e : (a : α) → β) '' s) r' = s.chainHeight r

Tactic:
chainHeight_eq_of_relEmbedding s e.toRelEmbedding

Premises used: Set.chainHeight_eq_of_relEmbedding, RelIso.toRelEmbedding
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
⊢ (chainHeight
      (image (α := { x : α // x ∈ s })
        (⇑(Subtype.relEmbedding (fun (x1 x2 : α) ↦ r x1 x2) fun (x : α) ↦ x ∈ s) : (a : { x : α // x ∈ s }) → α) univ)
      fun (x1 x2 : α) ↦ r x1 x2) =
    chainHeight.{u_1} (α := { x : α // x ∈ s }) univ
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹'o fun (x1 x2 : α) ↦ r x1 x2)

Tactic:
have hc := Set.chainHeight_eq_of_relEmbedding univ <| Subtype.relEmbedding (r · ·) (· ∈ s)
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
hc :
  (chainHeight
      (image (α := { x : α // x ∈ s })
        (⇑(Subtype.relEmbedding (fun (x1 x2 : α) ↦ r x1 x2) fun (x : α) ↦ x ∈ s) : (a : { x : α // x ∈ s }) → α) univ)
      fun (x1 x2 : α) ↦ r x1 x2) =
    chainHeight.{u_1} (α := { x : α // x ∈ s }) univ
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹'o fun (x1 x2 : α) ↦ r x1 x2)
h :
  ∀ (x x_1 : { x : α // x ∈ s }),
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹'o fun (x1 x2 : α) ↦ r x1 x2) x x_1 = r (↑x : α) (↑x_1 : α)
⊢ Eq.{u_1 + 1} (α := (x y : { x : α // x ∈ s }) → Prop)
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹'o fun (x1 x2 : α) ↦ r x1 x2) fun (x y : (↑s : Type u_1)) ↦
    r (↑x : α) (↑y : α)

Tactic:
funext