awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Iic (↑a : WithTop α) = Iic (↑a : WithTop α)
rw₁ : Iic (↑a : WithTop α) ∩ range some = Iic (↑a : WithTop α)
rw₂ : Iic (↑a : WithTop α) ∩ Iio ⊤ = Iic (↑a : WithTop α)
⊢ some '' Iic a = Iic (↑a : WithTop α)
have rw₃ : Iic (↑a : WithTop α) = Iic (↑a : WithTop α)
Tactic: rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iic_subset_Iio.2 <| coe_lt_top a)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ some '' Icc a b = Icc (↑a : WithTop α) (↑b : WithTop α)
have rw : some '' some ⁻¹' Icc (↑a : WithTop α) (↑b : WithTop α) = Icc (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Icc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Icc (↑a : WithTop α) (↑b : WithTop α) = Icc (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Icc a b = Icc (↑a : WithTop α) (↑b : WithTop α)
have rw₁ : Icc (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Icc (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Icc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Icc (↑a : WithTop α) (↑b : WithTop α) = Icc (↑a : WithTop α) (↑b : WithTop α)
rw₁ : Icc (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Icc (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Icc a b = Icc (↑a : WithTop α) (↑b : WithTop α)
have rw₂ : Icc (↑a : WithTop α) (↑b : WithTop α) ∩ Iio ⊤ = Icc (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Icc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Icc (↑a : WithTop α) (↑b : WithTop α) = Icc (↑a : WithTop α) (↑b : WithTop α)
rw₁ : Icc (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Icc (↑a : WithTop α) (↑b : WithTop α)
rw₂ : Icc (↑a : WithTop α) (↑b : WithTop α) ∩ Iio ⊤ = Icc (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Icc a b = Icc (↑a : WithTop α) (↑b : WithTop α)
have rw₃ : Icc (↑a : WithTop α) (↑b : WithTop α) = Icc (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Icc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ some '' Ico a b = Ico (↑a : WithTop α) (↑b : WithTop α)
have rw : some '' some ⁻¹' Ico (↑a : WithTop α) (↑b : WithTop α) = Ico (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ico_subset_Iio_self <| Iio_subset_Iio le_top)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Ico (↑a : WithTop α) (↑b : WithTop α) = Ico (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Ico a b = Ico (↑a : WithTop α) (↑b : WithTop α)
have rw₁ : Ico (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Ico (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ico_subset_Iio_self <| Iio_subset_Iio le_top)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Ico (↑a : WithTop α) (↑b : WithTop α) = Ico (↑a : WithTop α) (↑b : WithTop α)
rw₁ : Ico (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Ico (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Ico a b = Ico (↑a : WithTop α) (↑b : WithTop α)
have rw₂ : Ico (↑a : WithTop α) (↑b : WithTop α) ∩ Iio ⊤ = Ico (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ico_subset_Iio_self <| Iio_subset_Iio le_top)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Ico (↑a : WithTop α) (↑b : WithTop α) = Ico (↑a : WithTop α) (↑b : WithTop α)
rw₁ : Ico (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Ico (↑a : WithTop α) (↑b : WithTop α)
rw₂ : Ico (↑a : WithTop α) (↑b : WithTop α) ∩ Iio ⊤ = Ico (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Ico a b = Ico (↑a : WithTop α) (↑b : WithTop α)
have rw₃ : Ico (↑a : WithTop α) (↑b : WithTop α) = Ico (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ico_subset_Iio_self <| Iio_subset_Iio le_top)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ some '' Ioc a b = Ioc (↑a : WithTop α) (↑b : WithTop α)
have rw : some '' some ⁻¹' Ioc (↑a : WithTop α) (↑b : WithTop α) = Ioc (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Ioc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Ioc (↑a : WithTop α) (↑b : WithTop α) = Ioc (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Ioc a b = Ioc (↑a : WithTop α) (↑b : WithTop α)
have rw₁ : Ioc (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Ioc (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Ioc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Ioc (↑a : WithTop α) (↑b : WithTop α) = Ioc (↑a : WithTop α) (↑b : WithTop α)
rw₁ : Ioc (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Ioc (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Ioc a b = Ioc (↑a : WithTop α) (↑b : WithTop α)
have rw₂ : Ioc (↑a : WithTop α) (↑b : WithTop α) ∩ Iio ⊤ = Ioc (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Ioc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Ioc (↑a : WithTop α) (↑b : WithTop α) = Ioc (↑a : WithTop α) (↑b : WithTop α)
rw₁ : Ioc (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Ioc (↑a : WithTop α) (↑b : WithTop α)
rw₂ : Ioc (↑a : WithTop α) (↑b : WithTop α) ∩ Iio ⊤ = Ioc (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Ioc a b = Ioc (↑a : WithTop α) (↑b : WithTop α)
have rw₃ : Ioc (↑a : WithTop α) (↑b : WithTop α) = Ioc (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Ioc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ some '' Ioo a b = Ioo (↑a : WithTop α) (↑b : WithTop α)
have rw : some '' some ⁻¹' Ioo (↑a : WithTop α) (↑b : WithTop α) = Ioo (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Iio_self <| Iio_subset_Iio le_top)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Ioo (↑a : WithTop α) (↑b : WithTop α) = Ioo (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Ioo a b = Ioo (↑a : WithTop α) (↑b : WithTop α)
have rw₁ : Ioo (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Ioo (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Iio_self <| Iio_subset_Iio le_top)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Ioo (↑a : WithTop α) (↑b : WithTop α) = Ioo (↑a : WithTop α) (↑b : WithTop α)
rw₁ : Ioo (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Ioo (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Ioo a b = Ioo (↑a : WithTop α) (↑b : WithTop α)
have rw₂ : Ioo (↑a : WithTop α) (↑b : WithTop α) ∩ Iio ⊤ = Ioo (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Iio_self <| Iio_subset_Iio le_top)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Ioo (↑a : WithTop α) (↑b : WithTop α) = Ioo (↑a : WithTop α) (↑b : WithTop α)
rw₁ : Ioo (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Ioo (↑a : WithTop α) (↑b : WithTop α)
rw₂ : Ioo (↑a : WithTop α) (↑b : WithTop α) ∩ Iio ⊤ = Ioo (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Ioo a b = Ioo (↑a : WithTop α) (↑b : WithTop α)
have rw₃ : Ioo (↑a : WithTop α) (↑b : WithTop α) = Ioo (↑a : WithTop α) (↑b : WithTop α)
Tactic: rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Iio_self <| Iio_subset_Iio le_top)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Ioi (↑a : WithTop α) = some '' Ioi a ∪ {⊤}
have h : ∀ (x : WithTop α), x ∈ Ioi (↑a : WithTop α) ↔ x ∈ some '' Ioi a ∪ {⊤}
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
x : WithTop α
⊢ x ∈ Ioi (↑a : WithTop α) ↔ x ∈ some '' Ioi a ∪ {⊤}
have h : ⊤ ∈ Ioi (↑a : WithTop α) ↔ ⊤ ∈ some '' Ioi a ∪ {⊤}
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
x : WithTop α
h : ⊤ ∈ Ioi (↑a : WithTop α) ↔ ⊤ ∈ some '' Ioi a ∪ {⊤}
⊢ x ∈ Ioi (↑a : WithTop α) ↔ x ∈ some '' Ioi a ∪ {⊤}
have h₁ : ∀ (a_1 : α), (↑a_1 : WithTop α) ∈ Ioi (↑a : WithTop α) ↔ (↑a_1 : WithTop α) ∈ some '' Ioi a ∪ {⊤}
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Ici (↑a : WithTop α) = some '' Ici a ∪ {⊤}
have h : ∀ (x : WithTop α), x ∈ Ici (↑a : WithTop α) ↔ x ∈ some '' Ici a ∪ {⊤}
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
x : WithTop α
⊢ x ∈ Ici (↑a : WithTop α) ↔ x ∈ some '' Ici a ∪ {⊤}
have h : ⊤ ∈ Ici (↑a : WithTop α) ↔ ⊤ ∈ some '' Ici a ∪ {⊤}
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
x : WithTop α
h : ⊤ ∈ Ici (↑a : WithTop α) ↔ ⊤ ∈ some '' Ici a ∪ {⊤}
⊢ x ∈ Ici (↑a : WithTop α) ↔ x ∈ some '' Ici a ∪ {⊤}
have h₁ : ∀ (a_1 : α), (↑a_1 : WithTop α) ∈ Ici (↑a : WithTop α) ↔ (↑a_1 : WithTop α) ∈ some '' Ici a ∪ {⊤}
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
⊢ ¬SupIrred a ↔ IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a
have rw : (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a) ↔ IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a
Tactic: rw [SupIrred, not_and_or]
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a) ↔ IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a
have push : (IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b ≠ a ∧ c ≠ a) ↔ IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a
Tactic: push Not
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
⊢ (IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b ≠ a ∧ c ≠ a) ↔ IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a
have rw : ∀ (a_1 b : α), a_1 ⊔ b = a ∧ a_1 ≠ a ∧ b ≠ a ↔ a_1 ⊔ b = a ∧ a_1 < a ∧ b < a
Tactic: rw [exists₂_congr]
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
⊢ ¬SupPrime a ↔ IsMin a ∨ ∃ (b : α) (c : α), a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
have rw : (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c) ↔ IsMin a ∨ ∃ (b : α) (c : α), a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
Tactic: rw [SupPrime, not_and_or]
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c) ↔ IsMin a ∨ ∃ (b : α) (c : α), a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
have push : (IsMin a ∨ ∃ (b : α) (c : α), a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c) ↔ IsMin a ∨ ∃ (b : α) (c : α), a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
Tactic: push Not
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
a : α
inst_1 : OrderBot α
s_1 : Finset ι
f : ι → α
ha : SupIrred a
i : ι
s : Finset ι
h_1 : i ∉ s
ih : ∀ (h : s.sup f = a), ∃ i ∈ s, f i = a
h : (insert i s).sup f = a
⊢ ∃ i_1 ∈ insert i s, f i_1 = a
have insert : f i = a ∨ ∃ x ∈ s, f x = a
Tactic: simp only [exists_mem_insert] at ih ⊢
-- Lean 4 proof step from Mathlib.Order.Irreducible (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
a : α
inst_1 : OrderBot α
s_1 : Finset ι
f : ι → α
ha : SupIrred a
i : ι
s : Finset ι
h_1 : i ∉ s
ih : ∀ (h : s.sup f = a), ∃ i ∈ s, f i = a
h : (insert i s).sup f = a
⊢ f i = a ∨ ∃ x ∈ s, f x = a
have h₁ : f i ⊔ s.sup f = a
Tactic: rw [sup_insert] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
a : α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : s.sup f = a
⊢ ∃ i ∈ s, f i = a
have empty : ∀ (h : sup ∅ f = a), ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ f i = a
Tactic: induction s using Finset.induction with
  | empty => simpa [ha.ne_bot] using h.symm
  | insert i s _ ih =>
    simp only [exists_mem_insert] at ih ⊢
    rw [sup_insert] at h
    exact (ha.2 h).imp_right ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
a : α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : s.sup f = a
empty : ∀ (h : sup ∅ f = a), ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ f i = a
⊢ ∃ i ∈ s, f i = a
have insert : ∀ (i : ι) (s : Finset ι),
  i ∉ s → ∀ (ih : ∀ (h : s.sup f = a), ∃ i ∈ s, f i = a) (h : (insert i s).sup f = a), ∃ i_1 ∈ insert i s, f i_1 = a
Tactic: induction s using Finset.induction with
  | empty => simpa [ha.ne_bot] using h.symm
  | insert i s _ ih =>
    simp only [exists_mem_insert] at ih ⊢
    rw [sup_insert] at h
    exact (ha.2 h).imp_right ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
a : α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : s.sup f = a
⊢ ∃ i ∈ s, f i = a
have empty : ∀ (h : sup ∅ f = a), ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ f i = a
Tactic: classical
  induction s using Finset.induction with
  | empty => simpa [ha.ne_bot] using h.symm
  | insert i s _ ih =>
    simp only [exists_mem_insert] at ih ⊢
    rw [sup_insert] at h
    exact (ha.2 h).imp_right ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
a : α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : s.sup f = a
empty : ∀ (h : sup ∅ f = a), ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ f i = a
⊢ ∃ i ∈ s, f i = a
have insert : ∀ (i : ι) (s : Finset ι),
  i ∉ s → ∀ (ih : ∀ (h : s.sup f = a), ∃ i ∈ s, f i = a) (h : (insert i s).sup f = a), ∃ i_1 ∈ insert i s, f i_1 = a
Tactic: classical
  induction s using Finset.induction with
  | empty => simpa [ha.ne_bot] using h.symm
  | insert i s _ ih =>
    simp only [exists_mem_insert] at ih ⊢
    rw [sup_insert] at h
    exact (ha.2 h).imp_right ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
a : α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i
have empty : a ≤ sup ∅ f ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ a ≤ f i
Tactic: induction s using Finset.induction with
  | empty => simp [ha.ne_bot]
  | insert i s _ ih => simp only [exists_mem_insert, sup_insert, ha.le_sup, ih]
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
a : α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
empty : a ≤ sup ∅ f ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ a ≤ f i
⊢ a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i
have insert : ∀ (i : ι) (s : Finset ι),
  i ∉ s → ∀ (ih : a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i), a ≤ (insert i s).sup f ↔ ∃ i_1 ∈ insert i s, a ≤ f i_1
Tactic: induction s using Finset.induction with
  | empty => simp [ha.ne_bot]
  | insert i s _ ih => simp only [exists_mem_insert, sup_insert, ha.le_sup, ih]
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
a : α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i
have empty : a ≤ sup ∅ f ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ a ≤ f i
Tactic: classical
  induction s using Finset.induction with
  | empty => simp [ha.ne_bot]
  | insert i s _ ih => simp only [exists_mem_insert, sup_insert, ha.le_sup, ih]
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
a : α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
empty : a ≤ sup ∅ f ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ a ≤ f i
⊢ a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i
have insert : ∀ (i : ι) (s : Finset ι),
  i ∉ s → ∀ (ih : a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i), a ≤ (insert i s).sup f ↔ ∃ i_1 ∈ insert i s, a ≤ f i_1
Tactic: classical
  induction s using Finset.induction with
  | empty => simp [ha.ne_bot]
  | insert i s _ ih => simp only [exists_mem_insert, sup_insert, ha.le_sup, ih]
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
have apply : ∀ (x : α),
  (∀ y < x, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) →
    ∃ (s : Finset α), s.sup id = x ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
Tactic: apply WellFoundedLT.induction a _
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
have pos : ∀ (ha : SupIrred a), ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
Tactic: by_cases ha : SupIrred a
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
pos : ∀ (ha : SupIrred a), ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
have neg : ∀ (ha : ¬SupIrred a), ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
Tactic: by_cases ha : SupIrred a
-- Lean 4 proof step from Mathlib.Order.Irreducible (hypothesis)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : ¬SupIrred a
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
have ha₁ : IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a
Tactic: rw [not_supIrred] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
have neg : ∀ (ha : IsMin a), ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
Tactic: obtain ha | ⟨b, c, rfl, hb, hc⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a
neg : ∀ (ha : IsMin a), ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
have neg₁ : ∀ (b c : α) (ih : ∀ y < b ⊔ c, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) (hb : b < b ⊔ c)
  (hc : c < b ⊔ c), ∃ (s : Finset α), s.sup id = b ⊔ c ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
Tactic: obtain ha | ⟨b, c, rfl, hb, hc⟩ := ha
Cleared hypotheses: a, ih, ha
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
b c : α
ih : ∀ y < b ⊔ c, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
hb : b < b ⊔ c
hc : c < b ⊔ c
⊢ ∃ (s : Finset α), s.sup id = b ⊔ c ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
have neg : ∀ (s : Finset α) (hs : ∀ ⦃b : α⦄, b ∈ s → SupIrred b)
  (ih : ∀ y < s.sup id ⊔ c, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b)
  (hb : s.sup id < s.sup id ⊔ c) (hc : c < s.sup id ⊔ c),
  ∃ (s_1 : Finset α), s_1.sup id = s.sup id ⊔ c ∧ ∀ ⦃b : α⦄, b ∈ s_1 → SupIrred b
Tactic: obtain ⟨s, rfl, hs⟩ := ih _ hb
Cleared hypotheses: b, ih, hb, hc
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
c : α
s : Finset α
hs : ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ih : ∀ y < s.sup id ⊔ c, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
hb : s.sup id < s.sup id ⊔ c
hc : c < s.sup id ⊔ c
⊢ ∃ (s_1 : Finset α), s_1.sup id = s.sup id ⊔ c ∧ ∀ ⦃b : α⦄, b ∈ s_1 → SupIrred b
have neg : ∀ (t : Finset α) (ht : ∀ ⦃b : α⦄, b ∈ t → SupIrred b)
  (ih : ∀ y < s.sup id ⊔ t.sup id, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b)
  (hb : s.sup id < s.sup id ⊔ t.sup id) (hc : t.sup id < s.sup id ⊔ t.sup id),
  ∃ (s_1 : Finset α), s_1.sup id = s.sup id ⊔ t.sup id ∧ ∀ ⦃b : α⦄, b ∈ s_1 → SupIrred b
Tactic: obtain ⟨t, rfl, ht⟩ := ih _ hc
Cleared hypotheses: c, ih, hb, hc
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
have apply : ∀ (x : α),
  (∀ y < x, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) →
    ∃ (s : Finset α), s.sup id = x ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
Tactic: classical
  apply WellFoundedLT.induction a _
  clear a
  rintro a ih
  by_cases ha : SupIrred a
  · exact ⟨{a}, by simp [ha]⟩
  rw [not_supIrred] at ha
  obtain ha | ⟨b, c, rfl, hb, hc⟩ := ha
  · exact ⟨∅, by simp [ha.eq_bot]⟩
  obtain ⟨s, rfl, hs⟩ := ih _ hb
  obtain ⟨t, rfl, ht⟩ := ih _ hc
  exact ⟨s ∪ t, sup_union, forall_mem_union.2 ⟨hs, ht⟩⟩