awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : { x : α // Membership.mem (γ := Set α) {b : α | ReflTransGen r b a} x }
h' : a = (↑b : α)
⊢ Acc (TransGen r) (↑b : α)
have inl : ∀ (h : Acc (TransGen r) (↑b : α)) (h' : a = (↑b : α)), Acc (TransGen r) (↑b : α)
Tactic: rwa [h'] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
α : Type u_6
r : α → α → Prop
a : α
⊢ [Acc r a, WellFoundedOn {b : α | ReflTransGen r b a} r, WellFoundedOn {b : α | TransGen r b a} r].TFAE
have tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
Tactic: tfae_have 1 → 2 := by
    refine fun h => ⟨fun b => InvImage.accessible Subtype.val ?_⟩
    rw [← acc_transGen_iff] at h ⊢
    obtain h' | h' := reflTransGen_iff_eq_or_transGen.1 b.2
    · rwa [h'] at h
    · exact h.inv h'
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
⊢ [Acc r a, WellFoundedOn {b : α | ReflTransGen r b a} r, WellFoundedOn {b : α | TransGen r b a} r].TFAE
have tfae_2_to_3 : ∀ (a_1 : WellFoundedOn {b : α | ReflTransGen r b a} r), WellFoundedOn {b : α | TransGen r b a} r
Tactic: tfae_have 2 → 3 := fun h => h.subset fun _ => TransGen.to_reflTransGen
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
tfae_2_to_3 : ∀ (a_1 : WellFoundedOn {b : α | ReflTransGen r b a} r), WellFoundedOn {b : α | TransGen r b a} r
⊢ ∀ (a_1 : WellFoundedOn {b : α | TransGen r b a} r), Acc r a
have refine : ∀ (h : WellFoundedOn {b : α | TransGen r b a} r) (b : α) (hb : r b a),
  Fibration (α := { x : α // Membership.mem (γ := Set α) {b : α | TransGen r b a} x })
    (Subrel r fun (x : α) ↦ Membership.mem (γ := Set α) {b : α | TransGen r b a} x) r
    (Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Set α) {b : α | TransGen r b a} x))
Tactic: refine fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
tfae_2_to_3 : ∀ (a_1 : WellFoundedOn {b : α | ReflTransGen r b a} r), WellFoundedOn {b : α | TransGen r b a} r
⊢ [Acc r a, WellFoundedOn {b : α | ReflTransGen r b a} r, WellFoundedOn {b : α | TransGen r b a} r].TFAE
have tfae_3_to_1 : ∀ (a_1 : WellFoundedOn {b : α | TransGen r b a} r), Acc r a
Tactic: tfae_have 3 → 1 := by
    refine fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_)
    exact fun ⟨c, hc⟩ d h => ⟨⟨d, .head h hc⟩, h, rfl⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
⊢ s.WellFoundedOn r ↔
    ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
have simp : Nonempty.{u_2 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s) ↔
  ∃ (x : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ∀ (n : ℕ), Membership.mem (α := α) s ((x : (a : ℕ) → α) n : α)
Tactic: simp only [wellFoundedOn_iff, RelEmbedding.wellFounded_iff_isEmpty, ← not_exists, ←
    not_nonempty_iff, not_iff_not]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
⊢ Nonempty.{u_2 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s) ↔
    ∃ (x : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ∀ (n : ℕ), Membership.mem (α := α) s ((x : (a : ℕ) → α) n : α)
have mp : Nonempty.{u_2 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s) →
  ∃ (x : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ∀ (n : ℕ), Membership.mem (α := α) s ((x : (a : ℕ) → α) n : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
mp :
  Nonempty.{u_2 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s) →
    ∃ (x : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ∀ (n : ℕ), Membership.mem (α := α) s ((x : (a : ℕ) → α) n : α)
⊢ Nonempty.{u_2 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s) ↔
    ∃ (x : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ∀ (n : ℕ), Membership.mem (α := α) s ((x : (a : ℕ) → α) n : α)
have mpr : (∃ (x : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ∀ (n : ℕ), Membership.mem (α := α) s ((x : (a : ℕ) → α) n : α)) →
  Nonempty.{u_2 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf :
  ∀ {a b : ℕ},
    r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ∧
        Membership.mem (α := α) s ((f : (a : ℕ) → α) a : α) ∧ Membership.mem (α := α) s ((f : (a : ℕ) → α) b : α) ↔
      a > b
⊢ ∃ (x : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ∀ (n : ℕ), Membership.mem (α := α) s ((x : (a : ℕ) → α) n : α)
have H : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
Tactic: have H : ∀ n, f n ∈ s := fun n => (hf.2 n.lt_succ_self).2.2
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf :
  ∀ {a b : ℕ},
    r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ∧
        Membership.mem (α := α) s ((f : (a : ℕ) → α) a : α) ∧ Membership.mem (α := α) s ((f : (a : ℕ) → α) b : α) ↔
      a > b
H : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
⊢ ∃ (x : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ∀ (n : ℕ), Membership.mem (α := α) s ((x : (a : ℕ) → α) n : α)
have mp : ∀ {a b : ℕ}, r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ↔ a > b
Tactic: refine ⟨⟨f, ?_⟩, H⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ↔ a > b
hfs : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
⊢ Nonempty.{u_2 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s)
have mpr : ∀ {a b : ℕ},
  r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ∧
      Membership.mem (α := α) s ((f : (a : ℕ) → α) a : α) ∧ Membership.mem (α := α) s ((f : (a : ℕ) → α) b : α) ↔
    a > b
Tactic: refine ⟨⟨f, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s t : Set α
hs : s.WellFoundedOn r
ht : t.WellFoundedOn r
⊢ (s ∪ t).WellFoundedOn r
have rw : ∀ (hs : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α))
  (ht : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) t ((f : (a : ℕ) → α) n : α))
  (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) (s ∪ t) ((f : (a : ℕ) → α) n : α)
Tactic: rw [wellFoundedOn_iff_no_descending_seq] at *
Cleared hypotheses: hs, ht
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
ht : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) t ((f : (a : ℕ) → α) n : α)
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r
hf : ∀ (n : ℕ), Membership.mem (α := α) (s ∪ t) ((f : (a : ℕ) → α) n : α)
⊢ False
have inl : ∀ (g : ℕ ↪o ℕ) (hg : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) ((g : (a : ℕ) → ℕ) n : ℕ) : α)), False
Tactic: rcases Nat.exists_subseq_of_forall_mem_union f hf with ⟨g, hg | hg⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
ht : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) t ((f : (a : ℕ) → α) n : α)
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r
hf : ∀ (n : ℕ), Membership.mem (α := α) (s ∪ t) ((f : (a : ℕ) → α) n : α)
inl :
  ∀ (g : ℕ ↪o ℕ) (hg : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) ((g : (a : ℕ) → ℕ) n : ℕ) : α)), False
⊢ False
have inr : ∀ (g : ℕ ↪o ℕ) (hg : ∀ (n : ℕ), Membership.mem (α := α) t ((f : (a : ℕ) → α) ((g : (a : ℕ) → ℕ) n : ℕ) : α)), False
Tactic: rcases Nat.exists_subseq_of_forall_mem_union f hf with ⟨g, hg | hg⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x : α // x ∈ s ∪ t }
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)
have inl : ∀ (g : ℕ ↪o ℕ) (hgs : ∀ (n : ℕ), (↑(f ((g : (a : ℕ) → ℕ) n)) : α) ∈ s),
  ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)
Tactic: obtain ⟨g, hgs | hgt⟩ := Nat.exists_subseq_of_forall_mem_union _ fun x ↦ (f x).2
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x : α // x ∈ s ∪ t }
inl :
  ∀ (g : ℕ ↪o ℕ) (hgs : ∀ (n : ℕ), (↑(f ((g : (a : ℕ) → ℕ) n)) : α) ∈ s),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)
have inr : ∀ (g : ℕ ↪o ℕ) (hgt : ∀ (n : ℕ), (↑(f ((g : (a : ℕ) → ℕ) n)) : α) ∈ t),
  ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)
Tactic: obtain ⟨g, hgs | hgt⟩ := Nat.exists_subseq_of_forall_mem_union _ fun x ↦ (f x).2
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x : α // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), (↑(f ((g : (a : ℕ) → ℕ) n)) : α) ∈ s
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)
have inl : ∀ (m n : ℕ) (hlt : m < n) (hr : r (↑(f ((g : (a : ℕ) → ℕ) m)) : α) (↑(f ((g : (a : ℕ) → ℕ) n)) : α)),
  ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)
Tactic: rcases hs.exists_lt hgs with ⟨m, n, hlt, hr⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x : α // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), (↑(f ((g : (a : ℕ) → ℕ) n)) : α) ∈ t
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)
have inr : ∀ (m n : ℕ) (hlt : m < n) (hr : r (↑(f ((g : (a : ℕ) → ℕ) m)) : α) (↑(f ((g : (a : ℕ) → ℕ) n)) : α)),
  ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)
Tactic: rcases ht.exists_lt hgt with ⟨m, n, hlt, hr⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : s.PartiallyWellOrderedOn r
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
⊢ (f '' s).PartiallyWellOrderedOn r'
have rw : ∀ (hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n))
  (hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)) (f_1 : ℕ → β),
  (∀ (n : ℕ), f_1 n ∈ f '' s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r' (f_1 m) (f_1 n)
Tactic: rw [partiallyWellOrderedOn_iff_exists_lt] at *
Cleared hypotheses: hs, hf
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
hg' : ∀ (n : ℕ), g' n ∈ f '' s
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r' (g' m) (g' n)
have choose : ∀ (g : (n : ℕ) → α) (hgs : ∀ (n : ℕ), g n ∈ s) (heq : ∀ (n : ℕ), f (g n) = g' n),
  ∃ (m : ℕ) (n : ℕ), m < n ∧ r' (g' m) (g' n)
Tactic: choose g hgs heq using hg'
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
g : (n : ℕ) → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = g' n
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r' (g' m) (g' n)
have obtain : ∀ (heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n), ∃ (m : ℕ) (n : ℕ), m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
Tactic: obtain rfl : f ∘ g = g' := funext heq
Cleared hypotheses: g', heq
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g : (n : ℕ) → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
have obtain : ∀ (m n : ℕ) (hlt : m < n) (hmn : r (g m) (g n)), ∃ (m : ℕ) (n : ℕ), m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
Tactic: obtain ⟨m, n, hlt, hmn⟩ := hs g hgs
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
⊢ s.Finite
have by_contra! : ∀ (hi : s.Infinite), False
Tactic: by_contra! hi
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
hi : s.Infinite
⊢ False
have obtain : ∀ (m n : ℕ) (hmn : m < n)
  (h :
    Subrel r (fun (x : α) ↦ x ∈ s) ((Infinite.natEmbedding s hi : (a : ℕ) → (↑s : Type u_2)) m)
      ((Infinite.natEmbedding s hi : (a : ℕ) → (↑s : Type u_2)) n)),
  False
Tactic: obtain ⟨m, n, hmn, h⟩ := hp (hi.natEmbedding _)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
⊢ s.PartiallyWellOrderedOn r ↔ ∀ t ⊆ s, IsAntichain r t → t.Finite
have refine : (∀ t ⊆ s, IsAntichain r t → t.Finite) → s.PartiallyWellOrderedOn r
Tactic: refine ⟨fun h t ht hrt => hrt.finite_of_partiallyWellOrderedOn (h.mono ht), ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
⊢ (∀ t ⊆ s, IsAntichain r t → t.Finite) → s.PartiallyWellOrderedOn r
have rw : (∀ t ⊆ s, IsAntichain r t → t.Finite) → ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
Tactic: rw [partiallyWellOrderedOn_iff_exists_lt]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
have by_contra! : ∀ (H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
⊢ False
have refine_1 : ∀ (m n : ℕ) (hmn : f m = f n), m = n
Tactic: refine infinite_range_of_injective (fun m n hmn => ?_) (hs _ (range_subset_iff.2 hf) ?_)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
refine_1 : ∀ (m n : ℕ) (hmn : f m = f n), m = n
⊢ False
have refine_2 : IsAntichain r (range f)
Tactic: refine infinite_range_of_injective (fun m n hmn => ?_) (hs _ (range_subset_iff.2 hf) ?_)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
⊢ m = n
have refine_1 : ∀ (h : m < n), m = n
Tactic: obtain h | h | h := lt_trichotomy m n
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
refine_1 : ∀ (h : m < n), m = n
⊢ m = n
have refine_1₁ : ∀ (h : m = n), m = n
Tactic: obtain h | h | h := lt_trichotomy m n
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
refine_1 : ∀ (h : m < n), m = n
refine_1₁ : ∀ (h : m = n), m = n
⊢ m = n
have refine_1₂ : ∀ (h : n < m), m = n
Tactic: obtain h | h | h := lt_trichotomy m n
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ m = n
have refine_1 : r (f m) (f n)
Tactic: refine (H _ _ h ?_).elim
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ r (f m) (f n)
have refine_1 : r (f n) (f n)
Tactic: rw [hmn]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ m = n
have refine_1 : r (f n) (f m)
Tactic: refine (H _ _ h ?_).elim
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ r (f n) (f m)
have refine_1 : r (f n) (f n)
Tactic: rw [hmn]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m ≠ f n
⊢ rᶜ (f m) (f n)
have refine_2 : ∀ (h : m < n), rᶜ (f m) (f n)
Tactic: obtain h | h := (ne_of_apply_ne _ hmn).lt_or_gt
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m ≠ f n
refine_2 : ∀ (h : m < n), rᶜ (f m) (f n)
⊢ rᶜ (f m) (f n)
have refine_2₁ : ∀ (h : n < m), rᶜ (f m) (f n)
Tactic: obtain h | h := (ne_of_apply_ne _ hmn).lt_or_gt
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : IsPreorder α r
⊢ s.PartiallyWellOrderedOn r ↔
    ∀ (f : ℕ → α),
      (∀ (n : ℕ), f n ∈ s) → ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
have mpr : (∀ (f : ℕ → α),
    (∀ (n : ℕ), f n ∈ s) → ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) →
  s.PartiallyWellOrderedOn r
Tactic: use PartiallyWellOrderedOn.exists_monotone_subseq
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : IsPreorder α r
⊢ (∀ (f : ℕ → α),
      (∀ (n : ℕ), f n ∈ s) →
        ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) →
    s.PartiallyWellOrderedOn r
have mpr : (∀ (f : ℕ → α),
    (∀ (n : ℕ), f n ∈ s) → ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) →
  ∀ (f : ℕ → { x : α // x ∈ s }),
    ∃ (g : ℕ ↪o ℕ),
      ∀ (m n : ℕ), m ≤ n → Subrel r (fun (x : α) ↦ x ∈ s) (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
Tactic: rw [PartiallyWellOrderedOn, wellQuasiOrdered_iff_exists_monotone_subseq]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
⊢ (s ×ˢ t).PartiallyWellOrderedOn fun (x y : α × β) ↦ r x.1 y.1 ∧ r' x.2 y.2
have rw : ∀ (f : ℕ → α × β), (∀ (n : ℕ), f n ∈ s ×ˢ t) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2
Tactic: rw [partiallyWellOrderedOn_iff_exists_lt]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2
have obtain : ∀ (g₁ : ℕ ↪o ℕ) (h₁ : ∀ (m n : ℕ), m ≤ n → r (f ((g₁ : (a : ℕ) → ℕ) m)).1 (f ((g₁ : (a : ℕ) → ℕ) n)).1),
  ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2
Tactic: obtain ⟨g₁, h₁⟩ := hs.exists_monotone_subseq fun n => (hf n).1
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r (f ((g₁ : (a : ℕ) → ℕ) m)).1 (f ((g₁ : (a : ℕ) → ℕ) n)).1
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2
have obtain : ∀ (m n : ℕ) (hlt : m < n) (hle : r' (f ((g₁ : (a : ℕ) → ℕ) m)).2 (f ((g₁ : (a : ℕ) → ℕ) n)).2),
  ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2
Tactic: obtain ⟨m, n, hlt, hle⟩ := ht.exists_lt fun n => (hf _).2
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : ι → Type u_6
inst : Finite ι
r : (i : ι) → α i → α i → Prop
inst_1 : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
⊢ (pi (α := α) univ s).PartiallyWellOrderedOn fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
have haveI : ∀ (this : Fintype ι), (pi (α := α) univ s).PartiallyWellOrderedOn fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_6
inst : Finite ι
r : (i : ι) → α i → α i → Prop
inst_1 : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this : Fintype ι
⊢ (pi (α := α) univ s).PartiallyWellOrderedOn fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
have this₁ : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
Tactic: haveI : IsPreorder (∀ i, α i) (fun a b : ∀ i, α i => ∀ i, r i (a i) (b i)) :=
    { refl a i := refl (a i)
      trans a b c hab hbc i := _root_.trans (hab i) (hbc i) }