awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (β i)
a₁ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j i → a₁ j = a₂ j
hi : a₁ i < a₂ i
a : β i
ha₁ : a₁ i < a
ha₂ : a < a₂ i
j : ι
hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i
⊢ a₁ j = Function.update (β := β) a₂ i a j
have refine_1 : a₂ j = Function.update (β := β) a₂ i a j
Tactic: rw [h j hj]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (β i)
a₁ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j i → a₁ j = a₂ j
hi : a₁ i < a₂ i
a : β i
ha₁ : a₁ i < a
ha₂ : a < a₂ i
j : ι
hj : j < i
⊢ a₂ j = Function.update (β := β) a₂ i a j
have refine_1 : a₂ j = a₂ j
Tactic: rw [Function.update_of_ne hj.ne a]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (β i)
a₁ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j i → a₁ j = a₂ j
hi : a₁ i < a₂ i
a : β i
ha₁ : a₁ i < a
ha₂ : a < a₂ i
j : ι
hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i
⊢ Function.update (β := β) a₂ i a j = a₂ j
have refine_3 : a₂ j = a₂ j
Tactic: rw [Function.update_of_ne hj.ne a]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (β i)
a₁ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j i → a₁ j = a₂ j
hi : a₁ i < a₂ i
a : β i
ha₁ : a₁ i < a
ha₂ : a < a₂ i
⊢ ∃ (a : Lex ((i : ι) → β i)), a₁ < a ∧ a < a₂
have refine_1 : ∀ (j : ι) (hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i), a₁ j = Function.update (β := β) a₂ i a j
Tactic: classical
      refine ⟨Function.update a₂ _ a, ⟨i, fun j hj => ?_, ?_⟩, i, fun j hj => ?_, ?_⟩
      · rw [h j hj]
        dsimp only at hj
        rw [Function.update_of_ne hj.ne a]
      · rwa [Function.update_self i a]
      · rw [Function.update_of_ne hj.ne a]
      · rwa [Function.update_self i a]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (β i)
a₁ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j i → a₁ j = a₂ j
hi : a₁ i < a₂ i
a : β i
ha₁ : a₁ i < a
ha₂ : a < a₂ i
refine_1 : ∀ (j : ι) (hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i), a₁ j = Function.update (β := β) a₂ i a j
⊢ ∃ (a : Lex ((i : ι) → β i)), a₁ < a ∧ a < a₂
have refine_2 : (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) (a₁ i) (Function.update (β := β) a₂ i a i)
Tactic: classical
      refine ⟨Function.update a₂ _ a, ⟨i, fun j hj => ?_, ?_⟩, i, fun j hj => ?_, ?_⟩
      · rw [h j hj]
        dsimp only at hj
        rw [Function.update_of_ne hj.ne a]
      · rwa [Function.update_self i a]
      · rw [Function.update_of_ne hj.ne a]
      · rwa [Function.update_self i a]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (β i)
a₁ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j i → a₁ j = a₂ j
hi : a₁ i < a₂ i
a : β i
ha₁ : a₁ i < a
ha₂ : a < a₂ i
refine_1 : ∀ (j : ι) (hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i), a₁ j = Function.update (β := β) a₂ i a j
refine_2 : (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) (a₁ i) (Function.update (β := β) a₂ i a i)
⊢ ∃ (a : Lex ((i : ι) → β i)), a₁ < a ∧ a < a₂
have refine_3 : ∀ (j : ι) (hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i), Function.update (β := β) a₂ i a j = a₂ j
Tactic: classical
      refine ⟨Function.update a₂ _ a, ⟨i, fun j hj => ?_, ?_⟩, i, fun j hj => ?_, ?_⟩
      · rw [h j hj]
        dsimp only at hj
        rw [Function.update_of_ne hj.ne a]
      · rwa [Function.update_self i a]
      · rw [Function.update_of_ne hj.ne a]
      · rwa [Function.update_self i a]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (β i)
a₁ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j i → a₁ j = a₂ j
hi : a₁ i < a₂ i
a : β i
ha₁ : a₁ i < a
ha₂ : a < a₂ i
refine_1 : ∀ (j : ι) (hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i), a₁ j = Function.update (β := β) a₂ i a j
refine_2 : (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) (a₁ i) (Function.update (β := β) a₂ i a i)
refine_3 : ∀ (j : ι) (hj : (fun (x1 x2 : ι) ↦ x1 < x2) j i), Function.update (β := β) a₂ i a j = a₂ j
⊢ ∃ (a : Lex ((i : ι) → β i)), a₁ < a ∧ a < a₂
have refine_4 : (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) (Function.update (β := β) a₂ i a i) (a₂ i)
Tactic: classical
      refine ⟨Function.update a₂ _ a, ⟨i, fun j hj => ?_, ?_⟩, i, fun j hj => ?_, ?_⟩
      · rw [h j hj]
        dsimp only at hj
        rw [Function.update_of_ne hj.ne a]
      · rwa [Function.update_self i a]
      · rw [Function.update_of_ne hj.ne a]
      · rwa [Function.update_self i a]
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → LT (β i)
i : ι
inst_2 : NoMaxOrder.{u_2} (β i)
a : Lex ((i : ι) → β i)
⊢ ∃ (b : Lex ((i : ι) → β i)), a < b
have let : ∀ (b : β i) (hb : a i < b), ∃ (b : Lex ((i : ι) → β i)), a < b
Tactic: let ⟨b, hb⟩ := exists_gt (a i)
-- Lean 4 proof step from Mathlib.Order.PiLex (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder ι
inst_1 : DecidableEq ι
inst_2 : LT α
f : ι → α
i j : ι
h₁ : i ≤ j
h₂ : f i < f j
⊢ LT.lt (α := Colex (ι → α))
    ((toColex : (a : ι → α) → Colex (ι → α)) (f ∘ (⇑(Equiv.swap i j) : (a : ι) → ι)) : Colex (ι → α))
    ((toColex : (a : ι → α) → Colex (ι → α)) f : Colex (ι → α))
have rw : LT.lt (α := Colex (ι → α))
  ((toColex : (a : ι → α) → Colex (ι → α)) (f ∘ (⇑(Equiv.swap j i) : (a : ι) → ι)) : Colex (ι → α))
  ((toColex : (a : ι → α) → Colex (ι → α)) f : Colex (ι → α))
Tactic: rw [Equiv.swap_comm]
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
Goal:
α : Type u_1
r : α → α → Prop
⊢ IsChain r univ ↔ Std.Trichotomous r
have refine : ∀ (h : IsChain r univ) (a b : α), ¬r a b → ¬r b a → a = b
Tactic: refine ⟨fun h => ⟨fun a b => ?_⟩, fun h => @isChain_of_trichotomous _ _ h univ⟩
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
h : IsChain r univ
a b : α
⊢ ¬r a b → ¬r b a → a = b
have this : a ≠ b → r a b ∨ r b a
Tactic: have : a ≠ b → (r a b ∨ r b a) := h trivial trivial
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (hypothesis)
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
⊢ r x y ∨ r y x
have this : (fun (x y : β) ↦ s x y ∨ s y x) (f x) (f y)
Tactic: have := hrc ha hb (fun h ↦ hne (hf h))
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a
have 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
Tactic: rw [IsChain, IsChain, IsChain, pairwise_union_of_symmetric fun _ _ ↦ Or.symm]
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
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
⊢ IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a
have 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
Tactic: rw [IsChain, IsChain, IsChain, pairwise_union_of_symmetric fun _ _ ↦ Or.symm]
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
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
⊢ IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a
have 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
Tactic: rw [IsChain, IsChain, IsChain, pairwise_union_of_symmetric fun _ _ ↦ Or.symm]
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
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
⊢ IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a
have 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
Tactic: rw [IsChain, IsChain, IsChain, pairwise_union_of_symmetric fun _ _ ↦ Or.symm]
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun (x1 x2 : β) ↦ x1 ≤ x2) (range f)
have rw : IsChain (fun (x1 x2 : β) ↦ x1 ≤ x2) (f '' univ)
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
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
⊢ ∃ (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)
have simp : ∃ a ∈ c, r (f b) (f a)
Tactic: simp only [hab, exists_prop, and_self_iff, Subtype.exists]
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
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 : α) (_ : z ∈ s), r a z ∧ r b z ∧ r c z
have 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
Tactic: rcases directedOn_iff_directed.mpr (IsChain.directed hchain) a mem1 b mem2 with ⟨z, mem4, H1, H2⟩
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
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 : α) (_ : z ∈ s), r a z ∧ r b z ∧ r c z
have 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
Tactic: rcases directedOn_iff_directed.mpr (IsChain.directed hchain) z mem4 c mem3 with
    ⟨z', mem5, H3, H4⟩
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (hypothesis)
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
have x₁ : 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
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
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
⊢ (⇑e : (a : α) → β) '' c = t
have rw : c = (⇑e.toEquiv (r := r) (s := s).symm : (a : β) → α) '' t
Tactic: rw [← e.coe_fn_toEquiv, ← e.toEquiv.eq_preimage_iff_image_eq, ← Equiv.image_symm_eq_preimage]
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
⊢ IsEmpty α ↔ s = ∅
have refine : ∀ (h' : s = ∅), IsEmpty α
Tactic: refine ⟨fun _ ↦ s.eq_empty_of_isEmpty, fun h' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
h' : s = ∅
⊢ IsEmpty α
have false : ∀ (a : α), False
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
h' : s = ∅
x : α
⊢ False
have h₁ : ∀ ⦃t : Set α⦄, IsChain r t → ∅ = t
Tactic: simp only [IsMaxChain, h', IsChain.empty, empty_subset, forall_const, true_and] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : ∃ (t : Set α), IsChain r s ∧ SuperChain r s t
⊢ SuperChain r s (SuccChain r s)
have this : 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
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ¬∃ (t : Set α), IsChain r s ∧ SuperChain r s t
⊢ IsChain r (SuccChain r s)
have h₁ : ¬(IsChain r s ∧ ∃ (x : Set α), SuperChain r s x)
Tactic: rw [exists_and_left] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : ¬IsMaxChain r s
⊢ SuperChain r s (SuccChain r s)
have hs₃ : 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₂
Cleared hypotheses: hs₂
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
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
⊢ SuperChain r s (SuccChain r s)
have obtain : ∀ (t : Set α) (ht : IsChain r t) (hst : s ⊆ t ∧ ¬s = t), SuperChain r s (SuccChain r s)
Tactic: obtain ⟨t, ht, hst⟩ := hs₂ hs₁
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : LE α
s_1 t_1 : Flag α
a : α
s t : Flag α
h : s.carrier = t.carrier
⊢ s = t
have mk : ∀ (carrier : Set α) (Chain' : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) carrier)
  (max_chain' : ∀ ⦃s : Set α⦄, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → carrier ⊆ s → carrier = s)
  (h : { carrier := carrier, Chain' := Chain', max_chain' := max_chain' : Flag α }.carrier = t.carrier),
  { carrier := carrier, Chain' := Chain', max_chain' := max_chain' : Flag α } = t
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Order.Preorder.Chain (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : LE α
s t_1 : Flag α
a : α
t : Flag α
carrier : Set α
Chain' : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) carrier
max_chain' : ∀ ⦃s : Set α⦄, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → carrier ⊆ s → carrier = s
h : { carrier := carrier, Chain' := Chain', max_chain' := max_chain' : Flag α }.carrier = t.carrier
⊢ { carrier := carrier, Chain' := Chain', max_chain' := max_chain' : Flag α } = t
have mk : ∀ (carrier_1 : Set α) (Chain'_1 : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) carrier_1)
  (max_chain'_1 : ∀ ⦃s : Set α⦄, IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → carrier_1 ⊆ s → carrier_1 = s)
  (h :
    { carrier := carrier, Chain' := Chain', max_chain' := max_chain' : Flag α }.carrier =
      { carrier := carrier_1, Chain' := Chain'_1, max_chain' := max_chain'_1 : Flag α }.carrier),
  { carrier := carrier, Chain' := Chain', max_chain' := max_chain' : Flag α } =
    { carrier := carrier_1, Chain' := Chain'_1, max_chain' := max_chain'_1 }
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih : ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i
⊢ ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1
have cons : ∀ (j : ι) (hj : MaximalFor (fun (x : ι) ↦ x ∈ s) f j), ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1
Tactic: obtain ⟨j, hj⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun (x : ι) ↦ x ∈ s) f j
⊢ ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1
have pos : ∀ (hji : f j ≤ f i), ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1
Tactic: by_cases hji : f j ≤ f i
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun (x : ι) ↦ x ∈ s) f j
pos : ∀ (hji : f j ≤ f i), ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1
⊢ ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1
have neg : ∀ (hji : ¬f j ≤ f i), ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1
Tactic: by_cases hji : f j ≤ f i
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun (x : ι) ↦ x ∈ s) f j
hji : f j ≤ f i
⊢ ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1
have pos : ∀ ⦃j : ι⦄, (fun (x : ι) ↦ x ∈ cons i s hi) j → f i ≤ f j → f j ≤ f i
Tactic: refine ⟨i, mem_cons_self .., ?_⟩
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun (x : ι) ↦ x ∈ s) f j
hji : f j ≤ f i
⊢ ∀ ⦃j : ι⦄, (fun (x : ι) ↦ x ∈ cons i s hi) j → f i ≤ f j → f j ≤ f i
have pos : ∀ a ∈ s, f i ≤ f a → f a ≤ f i
Tactic: simp only [mem_cons, forall_eq_or_imp, imp_self, true_and]
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Finset ι
hs : s.Nonempty
⊢ ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i
have singleton : ∀ (i : ι), ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) f i_1
Tactic: induction hs using Finset.Nonempty.cons_induction with
  | singleton i => exact ⟨i, by simp⟩
  | @cons i s hi hs ih =>
    obtain ⟨j, hj⟩ := ih
    by_cases hji : f j ≤ f i
    · refine ⟨i, mem_cons_self .., ?_⟩
      simp only [mem_cons, forall_eq_or_imp, imp_self, true_and]
      exact fun k hk hik ↦ _root_.trans (hj.2 hk <| _root_.trans hji hik) hji
    · exact ⟨j, mem_cons_of_mem hj.1, by simpa [hji] using hj.2⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Finset ι
hs : s.Nonempty
singleton : ∀ (i : ι), ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) f i_1
⊢ ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i
have cons : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s) (hs : s.Nonempty) (ih : ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i),
  ∃ (i_1 : ι), MaximalFor (fun (x : ι) ↦ x ∈ cons i s hi) f i_1
Tactic: induction hs using Finset.Nonempty.cons_induction with
  | singleton i => exact ⟨i, by simp⟩
  | @cons i s hi hs ih =>
    obtain ⟨j, hj⟩ := ih
    by_cases hji : f j ≤ f i
    · refine ⟨i, mem_cons_self .., ?_⟩
      simp only [mem_cons, forall_eq_or_imp, imp_self, true_and]
      exact fun k hk hik ↦ _root_.trans (hj.2 hk <| _root_.trans hji hik) hji
    · exact ⟨j, mem_cons_of_mem hj.1, by simpa [hji] using hj.2⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
α : Type u_2
inst : Preorder α
a : α
s : Finset α
ha : a ∈ s
⊢ ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ s) b
have obtain : ∀ (b : α) (hb : b ∈ s) (hab : a ≤ b) (hbmin : ∀ ⦃y : α⦄, y ∈ s → a ≤ y → b ≤ y → y ≤ b),
  ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ s) b
Tactic: obtain ⟨b, hb, hab, hbmin⟩ : ∃ b ∈ s, a ≤ b ∧ _ := by
    simpa [Maximal, and_assoc] using {x ∈ s | a ≤ x}.exists_maximal ⟨a, mem_filter.2 ⟨ha, le_rfl⟩⟩
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
α : Type u_2
inst : Preorder α
a : α
s : Finset α
ha : a ∈ s
⊢ ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ s) b
have obtain : ∃ b ∈ s, a ≤ b ∧ ∀ ⦃y : α⦄, y ∈ s → a ≤ y → b ≤ y → y ≤ b
Tactic: classical
  obtain ⟨b, hb, hab, hbmin⟩ : ∃ b ∈ s, a ≤ b ∧ _ := by
    simpa [Maximal, and_assoc] using {x ∈ s | a ≤ x}.exists_maximal ⟨a, mem_filter.2 ⟨ha, le_rfl⟩⟩
  exact ⟨b, hab, hb, fun c hc hbc ↦ hbmin hc (hab.trans hbc) hbc⟩
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
α : Type u_2
inst : Preorder α
a : α
s : Finset α
ha : a ∈ s
obtain : ∃ b ∈ s, a ≤ b ∧ ∀ ⦃y : α⦄, y ∈ s → a ≤ y → b ≤ y → y ≤ b
⊢ ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ s) b
have obtain₁ : ∀ (b : α) (hb : b ∈ s) (hab : a ≤ b) (hbmin : ∀ ⦃y : α⦄, y ∈ s → a ≤ y → b ≤ y → y ≤ b),
  ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ s) b
Tactic: classical
  obtain ⟨b, hb, hab, hbmin⟩ : ∃ b ∈ s, a ≤ b ∧ _ := by
    simpa [Maximal, and_assoc] using {x ∈ s | a ≤ x}.exists_maximal ⟨a, mem_filter.2 ⟨ha, le_rfl⟩⟩
  exact ⟨b, hab, hb, fun c hc hbc ↦ hbmin hc (hab.trans hbc) hbc⟩
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Set ι
h : s.Finite
hs : s.Nonempty
⊢ ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i
have lift : ∀ (s : Finset ι) (hs : (↑s : Set ι).Nonempty), ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ (↑s : Set ι)) f i
Tactic: lift s to Finset ι using h
Cleared hypotheses: s, h, hs
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
inst_1 : IsTrans α LE.le
f : ι → α
s : Set ι
h : (f '' s).Finite
hs : s.Nonempty
⊢ ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i
have obtain : ∀ (a : ι) (ha : a ∈ s) (hmax : ∀ ⦃j : α⦄, (fun (x : α) ↦ x ∈ f '' s) j → id (f a) ≤ id j → id j ≤ id (f a)),
  ∃ (i : ι), MaximalFor (fun (x : ι) ↦ x ∈ s) f i
Tactic: obtain ⟨_, ⟨a, ha, rfl⟩, hmax⟩ := Finite.exists_maximalFor id (f '' s) h (hs.image f)
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
α : Type u_2
inst : Preorder α
s : Set α
a : α
hs : s.Finite
ha : a ∈ s
⊢ ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ s) b
have lift : ∀ (s : Finset α) (ha : a ∈ (↑s : Set α)), ∃ (b : α), a ≤ b ∧ Maximal (fun (x : α) ↦ x ∈ (↑s : Set α)) b
Tactic: lift s to Finset α using hs
Cleared hypotheses: s, hs, ha
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
α : Type u_2
inst : Preorder α
s : Set α
a : α
hs : s.Finite
ha : a ∈ s
⊢ ∃ b ≤ a, Minimal (fun (x : α) ↦ x ∈ s) b
have lift : ∀ (s : Finset α) (ha : a ∈ (↑s : Set α)), ∃ b ≤ a, Minimal (fun (x : α) ↦ x ∈ (↑s : Set α)) b
Tactic: lift s to Finset α using hs
Cleared hypotheses: s, hs, ha