awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Prod (goal)
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : OrderBot α
inst_3 : OrderBot β
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
⊢ (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i
have obtain : ∀ (a : ι) (ha : a ∈ s), (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i
Tactic: obtain ⟨a, ha⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Prod (goal)
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : OrderBot α
inst_3 : OrderBot β
s : Finset ι
t : Finset κ
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
⊢ (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i
have obtain : ∀ (b : κ) (hb : b ∈ t), (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i
Tactic: obtain ⟨b, hb⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Prod (goal)
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : OrderBot α
inst_3 : OrderBot β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i
have simp : (∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2) ↔ (∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2
Tactic: simp only [Prod.map, Finset.sup_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Prod (goal)
Goal:
α : Type u_2
ι : Type u_5
κ : Type u_6
inst : DistribLattice α
inst_1 : OrderBot α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
⊢ s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun (i : ι × κ) ↦ f i.1 ⊓ g i.2
have simp_rw : Eq.{u_2 + 1} (α := α) (s.sup fun (i : ι) ↦ f i ⊓ t.sup g) ((s ×ˢ t).sup fun (i : ι × κ) ↦ f i.1 ⊓ g i.2)
Tactic: simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left, sup_product_left]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Prod (goal)
Goal:
α : Type u_2
ι : Type u_5
κ : Type u_6
inst : DistribLattice α
inst_1 : OrderBot α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
simp_rw : Eq.{u_2 + 1} (α := α) (s.sup fun (i : ι) ↦ f i ⊓ t.sup g) ((s ×ˢ t).sup fun (i : ι × κ) ↦ f i.1 ⊓ g i.2)
⊢ s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun (i : ι × κ) ↦ f i.1 ⊓ g i.2
have simp_rw₁ : Eq.{u_2 + 1} (α := α) (s.sup fun (i : ι) ↦ t.sup fun (i_1 : κ) ↦ f i ⊓ g i_1)
  ((s ×ˢ t).sup fun (i : ι × κ) ↦ f i.1 ⊓ g i.2)
Tactic: simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left, sup_product_left]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Prod (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
s : Finset β
t : Finset γ
h : (s ×ˢ t).Nonempty
f : β × γ → α
⊢ (s ×ˢ t).sup' h f = t.sup' ⋯ fun (i' : γ) ↦ s.sup' ⋯ fun (i : β) ↦ f (i, i')
have rw : Eq.{u_2 + 1} (α := α) (s.sup' sorry fun (i : β) ↦ t.sup' sorry fun (i' : γ) ↦ f (i, i'))
  (t.sup' sorry fun (i' : γ) ↦ s.sup' sorry fun (i : β) ↦ f (i, i'))
Tactic: rw [sup'_product_left, Finset.sup'_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Prod (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : SemilatticeSup α
s : Finset β
t : Finset γ
h : (s ×ˢ t).Nonempty
f : β × γ → α
rw :
  Eq.{u_2 + 1} (α := α) (s.sup' ⋯ fun (i : β) ↦ t.sup' ⋯ fun (i' : γ) ↦ f (i, i'))
    (t.sup' ⋯ fun (i' : γ) ↦ s.sup' ⋯ fun (i : β) ↦ f (i, i'))
⊢ (s ×ˢ t).sup' h f = t.sup' ⋯ fun (i' : γ) ↦ s.sup' ⋯ fun (i : β) ↦ f (i, i')
have rw₁ : Eq.{u_2 + 1} (α := α) (t.sup' sorry fun (c : γ) ↦ s.sup' sorry fun (b : β) ↦ f (b, c))
  (t.sup' sorry fun (i' : γ) ↦ s.sup' sorry fun (i : β) ↦ f (i, i'))
Tactic: rw [sup'_product_left, Finset.sup'_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Prod (goal)
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
⊢ (s.sup' hs f, t.sup' ht g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i
have obtain : ∀ (a : ι) (ha : a ∈ s), (s.sup' sorry f, t.sup' ht g) ≤ i ↔ (s ×ˢ t).sup' sorry (Prod.map f g) ≤ i
Tactic: obtain ⟨a, ha⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Prod (goal)
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Finset ι
t : Finset κ
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
⊢ (s.sup' ⋯ f, t.sup' ht g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i
have obtain : ∀ (b : κ) (hb : b ∈ t), (s.sup' sorry f, t.sup' sorry g) ≤ i ↔ (s ×ˢ t).sup' sorry (Prod.map f g) ≤ i
Tactic: obtain ⟨b, hb⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Prod (goal)
Goal:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ (s.sup' ⋯ f, t.sup' ⋯ g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i
have simp : ((∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2) ↔ ∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2
Tactic: simp only [Prod.map, sup'_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Prod (goal)
Goal:
α : Type u_2
ι : Type u_5
κ : Type u_6
inst : DistribLattice α
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → α
⊢ s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' ⋯ fun (i : ι × κ) ↦ f i.1 ⊓ g i.2
have simp_rw : Eq.{u_2 + 1} (α := α) (s.sup' hs fun (i : ι) ↦ f i ⊓ t.sup' ht g) ((s ×ˢ t).sup' sorry fun (i : ι × κ) ↦ f i.1 ⊓ g i.2)
Tactic: simp_rw [Finset.sup'_inf_distrib_right, Finset.sup'_inf_distrib_left, sup'_product_left]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Prod (goal)
Goal:
α : Type u_2
ι : Type u_5
κ : Type u_6
inst : DistribLattice α
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → α
simp_rw :
  Eq.{u_2 + 1} (α := α) (s.sup' hs fun (i : ι) ↦ f i ⊓ t.sup' ht g) ((s ×ˢ t).sup' ⋯ fun (i : ι × κ) ↦ f i.1 ⊓ g i.2)
⊢ s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' ⋯ fun (i : ι × κ) ↦ f i.1 ⊓ g i.2
have simp_rw₁ : Eq.{u_2 + 1} (α := α) (s.sup' sorry fun (x : ι) ↦ t.sup' ht fun (i : κ) ↦ f x ⊓ g i)
  ((s ×ˢ t).sup' sorry fun (i : ι × κ) ↦ f i.1 ⊓ g i.2)
Tactic: simp_rw [Finset.sup'_inf_distrib_right, Finset.sup'_inf_distrib_left, sup'_product_left]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Union (goal)
Goal:
α : Type u_7
β : Type u_8
inst : DecidableEq β
s : Finset α
t : α → Finset β
⊢ s.sup t = s.biUnion t
have h : ∀ (a : β), a ∈ s.sup t ↔ a ∈ s.biUnion t
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Union (goal)
Goal:
α : Type u_7
β : Type u_8
inst : DecidableEq β
s : Finset α
t : α → Finset β
a : β
⊢ a ∈ s.sup t ↔ a ∈ s.biUnion t
have h : (∃ i ∈ s, a ∈ t i) ↔ a ∈ s.biUnion t
Tactic: rw [mem_sup, mem_biUnion]
-- Lean 4 proof step from Mathlib.Data.Finset.Lattice.Union (goal)
Goal:
α : Type u_7
β : Type u_8
inst : DecidableEq β
s : Finset α
t : α → Finset β
a : β
h : (∃ i ∈ s, a ∈ t i) ↔ a ∈ s.biUnion t
⊢ a ∈ s.sup t ↔ a ∈ s.biUnion t
have h₁ : (∃ i ∈ s, a ∈ t i) ↔ ∃ a_1 ∈ s, a ∈ t a_1
Tactic: rw [mem_sup, mem_biUnion]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
⊢ s = ∅
have obtain : ∀ (a : α) (ha : s.max = (↑a : WithBot α)), s = ∅
Tactic: obtain ⟨a, ha⟩ := max_of_nonempty H
-- Lean 4 proof step from Mathlib.Data.Finset.Max (hypothesis)
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
a : α
ha : s.max = (↑a : WithBot α)
⊢ s = ∅
have ha₁ : ⊥ = (↑a : WithBot α)
Tactic: rw [h] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
⊢ ∀ {a : α}, s.max = (↑a : WithBot α) → a ∈ s
have empty : ∀ {a : α}, Finset.max ∅ = (↑a : WithBot α) → Membership.mem (γ := Finset α) ∅ a
Tactic: induction s using Finset.induction_on with
  | empty => intro _ H; cases H
  | _ => grind [WithBot.coe_eq_coe]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
empty : ∀ {a : α}, Finset.max ∅ = (↑a : WithBot α) → Membership.mem (γ := Finset α) ∅ a
⊢ ∀ {a : α}, s.max = (↑a : WithBot α) → a ∈ s
have insert : ∀ (a : α) (s : Finset α),
  a ∉ s →
    (∀ {a : α}, s.max = (↑a : WithBot α) → a ∈ s) →
      ∀ {a_3 : α}, (insert a s).max = (↑a_3 : WithBot α) → a_3 ∈ insert a s
Tactic: induction s using Finset.induction_on with
  | empty => intro _ H; cases H
  | _ => grind [WithBot.coe_eq_coe]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
h₂ : 1 < #s
⊢ s.min' ⋯ < s.max' ⋯
have rcases : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s) (hab : a ≠ b), s.min' sorry < s.max' sorry
Tactic: rcases one_lt_card.1 h₂ with ⟨a, ha, b, hb, hab⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset αᵒᵈ
⊢ Eq (α := WithTop α) (WithTop.map (⇑ofDual : (a : αᵒᵈ) → α) s.min) (Finset.max (image (⇑ofDual : (a : αᵒᵈ) → α) s))
have rw : Eq (α := WithTop α) (WithTop.map (⇑ofDual : (a : αᵒᵈ) → α) s.min) (s.sup (WithBot.some ∘ (⇑ofDual : (a : αᵒᵈ) → α)))
Tactic: rw [max_eq_sup_withBot, sup_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset αᵒᵈ
⊢ Eq (α := WithBot α) (WithBot.map (⇑ofDual : (a : αᵒᵈ) → α) s.max) (Finset.min (image (⇑ofDual : (a : αᵒᵈ) → α) s))
have rw : Eq (α := WithBot α) (WithBot.map (⇑ofDual : (a : αᵒᵈ) → α) s.max) (s.inf (WithTop.some ∘ (⇑ofDual : (a : αᵒᵈ) → α)))
Tactic: rw [min_eq_inf_withTop, inf_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
⊢ Eq (α := WithTop αᵒᵈ) (WithTop.map (⇑toDual : (a : α) → αᵒᵈ) s.min) (Finset.max (image (⇑toDual : (a : α) → αᵒᵈ) s))
have rw : Eq (α := WithTop αᵒᵈ) (WithTop.map (⇑toDual : (a : α) → αᵒᵈ) s.min) (s.sup (WithBot.some ∘ (⇑toDual : (a : α) → αᵒᵈ)))
Tactic: rw [max_eq_sup_withBot, sup_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Finset α
⊢ Eq (α := WithBot αᵒᵈ) (WithBot.map (⇑toDual : (a : α) → αᵒᵈ) s.max) (Finset.min (image (⇑toDual : (a : α) → αᵒᵈ) s))
have rw : Eq (α := WithBot αᵒᵈ) (WithBot.map (⇑toDual : (a : α) → αᵒᵈ) s.max) (s.inf (WithTop.some ∘ (⇑toDual : (a : α) → αᵒᵈ)))
Tactic: rw [min_eq_inf_withTop, inf_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (↑(insert a s) : Set α) (max a (s.max' H))
have rw : IsGreatest (insert a (↑s : Set α)) (max a (s.max' H))
Tactic: rw [coe_insert]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsLeast (↑(insert a s) : Set α) (min a (s.min' H))
have rw : IsLeast (insert a (↑s : Set α)) (min a (s.min' H))
Tactic: rw [coe_insert]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ (image f s).max' h = f (s.max' ⋯)
have simp : s.sup' sorry (id ∘ f) = f (s.sup' sorry id)
Tactic: simp only [max', sup'_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ (image f s).min' h = f (s.min' ⋯)
have simp : s.inf' sorry (id ∘ f) = f (s.inf' sorry id)
Tactic: simp only [min', inf'_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
⊢ (s.erase x).max ≠ (↑x : WithBot α)
have pos : ∀ (s0 : (s.erase x).Nonempty), (s.erase x).max ≠ (↑x : WithBot α)
Tactic: by_cases! s0 : (s.erase x).Nonempty
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
pos : ∀ (s0 : (s.erase x).Nonempty), (s.erase x).max ≠ (↑x : WithBot α)
⊢ (s.erase x).max ≠ (↑x : WithBot α)
have neg : ∀ (s0 : s.erase x = ∅), (s.erase x).max ≠ (↑x : WithBot α)
Tactic: by_cases! s0 : (s.erase x).Nonempty
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ (s.erase x).max ≠ (↑x : WithBot α)
have pos : (↑((s.erase x).max' s0) : WithBot α) ≠ (↑x : WithBot α)
Tactic: refine ne_of_eq_of_ne (coe_max' s0).symm ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
s0 : s.erase x = ∅
⊢ (s.erase x).max ≠ (↑x : WithBot α)
have neg : ⊥ ≠ (↑x : WithBot α)
Tactic: rw [s0, max_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
⊢ (s.erase x).min ≠ (↑x : WithTop α)
have apply : ¬Eq (α := WithTop αᵒᵈ) (WithTop.map (⇑toDual : (a : α) → αᵒᵈ) (s.erase x).min)
    (WithTop.map (⇑toDual : (a : α) → αᵒᵈ) (↑x : WithTop α))
Tactic: apply mt (congr_arg (WithTop.map toDual))
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
x : α
s : Finset α
⊢ ¬Eq (α := WithTop αᵒᵈ) (WithTop.map (⇑toDual : (a : α) → αᵒᵈ) (s.erase x).min)
      (WithTop.map (⇑toDual : (a : α) → αᵒᵈ) (↑x : WithTop α))
have rw : ¬Eq (α := WithTop αᵒᵈ)
    (Finset.max (erase (image (⇑toDual : (a : α) → αᵒᵈ) s) ((toDual : (a : α) → αᵒᵈ) x)) : WithBot αᵒᵈ)
    ((↑((toDual : (a : α) → αᵒᵈ) x) : WithTop αᵒᵈ) : WithTop αᵒᵈ)
Tactic: rw [map_toDual_min, image_erase toDual.injective, WithTop.map_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ∃ z ∈ t, x < z ∧ z < y
have rcases : ∀ (a : α) (has : a ∈ s) (hxa : x < a) (ha : ∀ z ∈ s, x < z → a ≤ z), ∃ z ∈ t, x < z ∧ z < y
Tactic: rcases exists_next_right ⟨y, hy, hxy⟩ with ⟨a, has, hxa, ha⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
a : α
has : a ∈ s
hxa : x < a
ha : ∀ z ∈ s, x < z → a ≤ z
⊢ ∃ z ∈ t, x < z ∧ z < y
have rcases : ∀ (b : α) (hbt : b ∈ t) (hxb : x < b) (hba : b < a), ∃ z ∈ t, x < z ∧ z < y
Tactic: rcases h x hx a has hxa fun z hzs hz => hz.2.not_ge <| ha _ hzs hz.1 with ⟨b, hbt, hxb, hba⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Max (hypothesis)
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
⊢ #s ≤ #t + 1
have h₁ : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
Tactic: replace h : ∀ᵉ (x ∈ s) (y ∈ s), x < y → ∃ z ∈ t, x < z ∧ z < y := by
    intro x hx y hy hxy
    rcases exists_next_right ⟨y, hy, hxy⟩ with ⟨a, has, hxa, ha⟩
    rcases h x hx a has hxa fun z hzs hz => hz.2.not_ge <| ha _ hzs hz.1 with ⟨b, hbt, hxb, hba⟩
    exact ⟨b, hbt, hxb, hba.trans_le <| ha _ hy hxy⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun (x : α) ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ (↑s : Set α)
y : α
hy : y ∈ (↑s : Set α)
hxy : x < y
⊢ f x < f y
have rcases : ∀ (a : α) (hat : a ∈ t) (hxa : x < a) (hay : a < y), f x < f y
Tactic: rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Max (hypothesis)
Goal:
α : Type u_2
inst : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun (x : α) ↦ {y ∈ t | x < y}.min
⊢ #s ≤ #t + 1
have f_mono : StrictMonoOn f (↑s : Set α)
Tactic: have f_mono : StrictMonoOn f s := by
    intro x hx y hy hxy
    rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩
    calc
      f x ≤ a := min_le (mem_filter.2 ⟨hat, by simpa⟩)
      _ < f y :=
        (Finset.lt_inf_iff <| WithTop.coe_lt_top a).2 fun b hb =>
          WithTop.coe_lt_coe.2 <| hay.trans (by simpa using (mem_filter.1 hb).2)
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DecidableEq α
motive : Finset α → Prop
s : Finset α
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
⊢ motive s
have H : ∀ (s : Finset α) (ih : ∀ s_1 ∈ s, motive (s.erase s_1)), motive s
Tactic: induction s using Finset.eraseInduction with | _ s ih
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
⊢ motive s
have H : ∀ (ih : ∀ (s : α), Membership.mem (γ := Finset α) ∅ s → motive (erase ∅ s)), motive ∅
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hne)
Cleared hypotheses: s, ih
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
H : ∀ (ih : ∀ (s : α), Membership.mem (γ := Finset α) ∅ s → motive (erase ∅ s)), motive ∅
⊢ motive s
have H₁ : ∀ (hne : s.Nonempty), motive s
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hne)
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
⊢ motive s
have H : ∀ (H : s.max' hne ∈ s), motive s
Tactic: have H : s.max' hne ∈ s := max'_mem s hne
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
H : s.max' hne ∈ s
⊢ motive s
have H₁ : motive (Insert.insert (s.max' hne) (s.erase (s.max' hne)))
Tactic: rw [← insert_erase H]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
s : Finset ι
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
⊢ motive s
have H : ∀ (s : Finset ι) (ihs : ∀ s_1 ∈ s, motive (s.erase s_1)), motive s
Tactic: induction s using Finset.eraseInduction with | _ s ihs
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
⊢ motive s
have H : ∀ (hne : image f s = ∅), motive s
Tactic: rcases (s.image f).eq_empty_or_nonempty with (hne | hne)
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
H : ∀ (hne : image f s = ∅), motive s
⊢ motive s
have H₁ : ∀ (hne : (image f s).Nonempty), motive s
Tactic: rcases (s.image f).eq_empty_or_nonempty with (hne | hne)
-- Lean 4 proof step from Mathlib.Data.Finset.Max (hypothesis)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : image f s = ∅
⊢ motive s
have hne₁ : s = ∅
Tactic: simp only [image_eq_empty] at hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
⊢ motive s
have H : ∀ (H : (image f s).max' hne ∈ image f s), motive s
Tactic: have H : (s.image f).max' hne ∈ s.image f := max'_mem (s.image f) hne
-- Lean 4 proof step from Mathlib.Data.Finset.Max (hypothesis)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
H : (image f s).max' hne ∈ image f s
⊢ motive s
have H₁ : ∃ a ∈ s, f a = (image f s).max' hne
Tactic: simp only [mem_image] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
H : ∃ a ∈ s, f a = (image f s).max' hne
⊢ motive s
have H₁ : ∀ (a : ι) (has : a ∈ s) (hfa : f a = (image f s).max' hne), motive s
Tactic: rcases H with ⟨a, has, hfa⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
⊢ motive s
have H : motive (Insert.insert a (s.erase a))
Tactic: rw [← insert_erase has]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
⊢ motive (Insert.insert a (s.erase a))
have H : ∀ (x : ι) (hx : x ∈ s.erase a), f x ≤ f a
Tactic: refine insert _ _ (notMem_erase a s) (fun x hx => ?_) (ihs a has)
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : LinearOrder α
inst_1 : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
x : ι
hx : x ∈ s.erase a
⊢ f x ≤ f a
have H : f x ≤ (image f s).max' hne
Tactic: rw [hfa]
-- Lean 4 proof step from Mathlib.Data.Finset.Max (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
s : Finset β
f : β → α
h : s.Nonempty
⊢ ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x
have obtain : ∀ (y : α) (hy : (image f s).max = (↑y : WithBot α)), ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x
Tactic: obtain ⟨y, hy⟩ := max_of_nonempty (h.image f)