awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
apply apply₁ apply₂ :
  ∀ (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
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
have pos : ∀ (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
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⟩⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
apply apply₁ apply₂ :
  ∀ (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
pos :
  ∀ (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
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
have neg : ∀ (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
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⟩⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
apply apply₁ apply₂ :
  ∀ (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
pos :
  ∀ (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
neg neg₁ :
  ∀ (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
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
have neg₂ : ∀ (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
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⟩⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
apply apply₁ apply₂ :
  ∀ (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
pos :
  ∀ (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
neg neg₁ :
  ∀ (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
neg₂ :
  ∀ (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
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
have neg₃ : ∀ (a : α) (ih : ∀ y < a, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) (ha : IsMin a),
  ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃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⟩⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
apply apply₁ apply₂ :
  ∀ (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
pos :
  ∀ (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
neg neg₁ :
  ∀ (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
neg₂ :
  ∀ (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
neg₃ :
  ∀ (a : α) (ih : ∀ y < a, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) (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: 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⟩⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
apply apply₁ apply₂ :
  ∀ (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
pos :
  ∀ (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
neg neg₁ :
  ∀ (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
neg₂ :
  ∀ (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
neg₃ :
  ∀ (a : α) (ih : ∀ y < a, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) (ha : IsMin a),
    ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
neg₄ 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
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
have neg₆ : ∀ (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
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⟩⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
apply apply₁ apply₂ :
  ∀ (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
pos :
  ∀ (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
neg neg₁ :
  ∀ (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
neg₂ :
  ∀ (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
neg₃ :
  ∀ (a : α) (ih : ∀ y < a, ∃ (s : Finset α), s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) (ha : IsMin a),
    ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
neg₄ 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
neg₆ :
  ∀ (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
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
have neg₇ : ∀ (s : Finset α) (hs : ∀ ⦃b : α⦄, b ∈ s → SupIrred b) (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: 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⟩⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ≤ b ⊔ c → a ≤ b ∨ a ≤ c
have simp_rw : a ⊓ b ⊔ a ⊓ c = a → a ⊓ b = a ∨ a ⊓ c = a
Tactic: simp_rw [← inf_eq_left, inf_sup_left]
-- Lean 4 proof step from Mathlib.Order.Irreducible (goal)
Goal:
α : Type u_2
inst : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ b ⊓ c ≤ a → b ≤ a ∨ c ≤ a
have simp_rw : (a ⊔ b) ⊓ (a ⊔ c) = a → a ⊔ b = a ∨ a ⊔ c = a
Tactic: simp_rw [← sup_eq_left, sup_inf_left]
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : IsNormal f
a : α
ha : IsSuccLimit a
⊢ IsLUB (f '' Iio a) (f a)
have refine : f a ∈ upperBounds (f '' Iio a)
Tactic: refine ⟨?_, hf.2 ha⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ IsSuccLimit (f a)
have refine_1 : ¬IsMin (f a)
Tactic: refine ⟨?_, fun b hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
refine_1 : ¬IsMin (f a)
⊢ IsSuccLimit (f a)
have refine_2 : ∀ (b : β) (hb : b ⋖ f a), False
Tactic: refine ⟨?_, fun b hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ ¬IsMin (f a)
have refine_1 : ∀ (b : α) (hb : b < a), ¬IsMin (f a)
Tactic: obtain ⟨b, hb⟩ := not_isMin_iff.1 ha.not_isMin
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
hb : b ⋖ f a
⊢ False
have refine_2 : ∀ (c : α) (hc : c < a) (hc' : b < f c), False
Tactic: obtain ⟨c, hc, hc'⟩ := (hf.lt_iff_exists_lt ha).1 hb.lt
-- Lean 4 proof step from Mathlib.Order.IsNormal (hypothesis)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
hb : b ⋖ f a
c : α
hc : c < a
hc' : b < f c
⊢ False
have hc'₁ : f a ≤ f c
Tactic: have hc' := hb.ge_of_gt hc'
-- Lean 4 proof step from Mathlib.Order.IsNormal (hypothesis)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
hb : b ⋖ f a
c : α
hc : c < a
hc'_1 : b < f c
hc' : f a ≤ f c
⊢ False
have hc'₁ : a ≤ c
Tactic: rw [hf.strictMono.le_iff_le] at hc'
Cleared hypotheses: hc'
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
⊢ IsLUB (f '' s) (f a)
have refine_1 : f a ∈ upperBounds (f '' s)
Tactic: refine ⟨?_, fun b hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
refine_1 : f a ∈ upperBounds (f '' s)
⊢ IsLUB (f '' s) (f a)
have refine_2 : ∀ (b : β) (hb : b ∈ upperBounds (f '' s)), f a ≤ b
Tactic: refine ⟨?_, fun b hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
⊢ f a ≤ b
have pos : ∀ (ha : a ∈ s), f a ≤ b
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
pos : ∀ (ha : a ∈ s), f a ≤ b
⊢ f a ≤ b
have neg : ∀ (ha : a ∉ s), f a ≤ b
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Order.IsNormal (hypothesis)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
⊢ f a ≤ b
have ha' : IsSuccLimit a
Tactic: have ha' := hs.isSuccLimit_of_notMem hs' ha
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
ha' : IsSuccLimit a
⊢ f a ≤ b
have neg : ∀ a' < a, f a' ≤ b
Tactic: rw [le_iff_forall_le hf ha']
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
ha' : IsSuccLimit a
c : α
hc : c < a
⊢ f c ≤ b
have neg : ∀ (d : α) (hd : d ∈ s) (hcd : c < d) (hda : d ≤ a), f c ≤ b
Tactic: obtain ⟨d, hd, hcd, hda⟩ := hs.exists_between hc
-- Lean 4 proof step from Mathlib.Order.IsNormal (hypothesis)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
ha' : IsSuccLimit a
c : α
hc : c < a
d : α
hd : d ∈ s
hcd : c < d
hda : d ≤ a
⊢ f c ≤ b
have hb₁ : ∀ ⦃x : α⦄, x ∈ s → f x ≤ b
Tactic: simp_rw [mem_upperBounds, forall_mem_image] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2
a : α
ha : IsSuccLimit a
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (lowerBounds (upperBounds ((⇑f : (a : α) → β) '' Iio a)))
    ((f : (a : α) → β) a : β)
have rw : Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (lowerBounds (upperBounds (Iio ((f : (a : α) → β) a))) : Set β)
  ((f : (a : α) → β) a : β)
Tactic: rw [f.image_Iio]
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
⊢ IsNormal (g ∘ f)
have refine : ∀ {a : α} (ha : IsSuccLimit a) (b : γ) (hb : b ∈ upperBounds (g ∘ f '' Iio a)), (g ∘ f) a ≤ b
Tactic: refine ⟨hg.strictMono.comp hf.strictMono, fun ha b hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
a : α
ha : IsSuccLimit a
b : γ
hb : b ∈ upperBounds (g ∘ f '' Iio a)
⊢ (g ∘ f) a ≤ b
have hb₁ : ∀ ⦃x : α⦄, x ∈ Iio a → g (f x) ≤ b
Tactic: simp_rw [Function.comp_apply, mem_upperBounds, forall_mem_image] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
a : α
⊢ IsNormal.{u_1, u_2} (β := (↑(Iio (f a)) : Type u_2)) fun (x : (↑(Iio a) : Type u_1)) ↦
    Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑x : α)) ⋯
have rw : (StrictMono.{u_1, u_2} (β := (↑(Iio (f a)) : Type u_2)) fun (x : (↑(Iio a) : Type u_1)) ↦
    Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑x : α)) sorry) ∧
  ∀ (o : (↑(Iio a) : Type u_1)),
    IsSuccLimit o →
      ∀ (a_2 : (↑(Iio (f a)) : Type u_2)),
        (∀ b < o, Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑b : α)) sorry ≤ a_2) →
          Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑o : α)) sorry ≤ a_2
Tactic: rw [isNormal_iff]
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
a : α
⊢ (StrictMono.{u_1, u_2} (β := (↑(Iio (f a)) : Type u_2)) fun (x : (↑(Iio a) : Type u_1)) ↦
      Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑x : α)) ⋯) ∧
    ∀ (o : (↑(Iio a) : Type u_1)),
      IsSuccLimit o →
        ∀ (a_2 : (↑(Iio (f a)) : Type u_2)),
          (∀ b < o, Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑b : α)) ⋯ ≤ a_2) →
            Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑o : α)) ⋯ ≤ a_2
have refine : ∀ (b : (↑(Iio a) : Type u_1)) (hb : IsSuccLimit b) (c : (↑(Iio (f a)) : Type u_2))
  (hc : ∀ b_1 < b, Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑b_1 : α)) sorry ≤ c),
  (↑c : β) ∈ upperBounds (f '' Iio (↑b : α))
Tactic: refine ⟨fun x y h ↦ hf.strictMono h, fun b hb c hc ↦ hf.2 (hb.subtypeVal (isLowerSet_Iio _)) ?_⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst_2 : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
have unfold : f (sSup (range fun (i : ι) ↦ g i)) = sSup (range fun (i : ι) ↦ f (g i))
Tactic: unfold iSup
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst_2 : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
⊢ f (sSup (range fun (i : ι) ↦ g i)) = sSup (range fun (i : ι) ↦ f (g i))
have h : (range fun (i : ι) ↦ f (g i)) = f '' range g
Tactic: convert! map_sSup hf (range_nonempty g) hg
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst_2 : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
⊢ (range fun (i : ι) ↦ f (g i)) = f '' range g
have h : ∀ (x : β), Membership.mem (γ := Set β) (range fun (i : ι) ↦ f (g i)) x ↔ x ∈ f '' range g
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
⊢ ⨆ (n : ℕ), f^[n] a ∈ Function.fixedPoints f
have rw : Eq.{u_1 + 1} (α := α) (⨆ (i : ℕ), f (f^[i] a)) (⨆ (n : ℕ), f^[n] a)
Tactic: rw [f.mem_fixedPoints_iff, hf.map_iSup hf']
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ℕ), f (f^[i] a)) (⨆ (n : ℕ), f^[n] a)
have a₁ : LE.le.{u_1} (α := α) (⨆ (i : ℕ), f (f^[i] a)) (⨆ (n : ℕ), f^[n] a)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
a₁ : LE.le.{u_1} (α := α) (⨆ (i : ℕ), f (f^[i] a)) (⨆ (n : ℕ), f^[n] a)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ℕ), f (f^[i] a)) (⨆ (n : ℕ), f^[n] a)
have a₂ : LE.le.{u_1} (α := α) (⨆ (n : ℕ), f^[n] a) (⨆ (i : ℕ), f (f^[i] a))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
⊢ LE.le.{u_1} (α := α) (⨆ (i : ℕ), f (f^[i] a)) (⨆ (n : ℕ), f^[n] a)
have a₁ : ∀ (n : ℕ), f (f^[n] a) ≤ ⨆ (n : ℕ), f^[n] a
Tactic: refine ciSup_le fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
⊢ LE.le.{u_1} (α := α) (⨆ (n : ℕ), f^[n] a) (⨆ (i : ℕ), f (f^[i] a))
have a₁ : ∀ (n : ℕ), f^[n] a ≤ ⨆ (i : ℕ), f (f^[i] a)
Tactic: refine ciSup_le fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
n : ℕ
⊢ f (f^[n] a) ≤ ⨆ (n : ℕ), f^[n] a
have a₁ : f^[n.succ] a ≤ ⨆ (n : ℕ), f^[n] a
Tactic: rw [← f.iterate_succ_apply']
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
n : ℕ
⊢ f^[n] a ≤ ⨆ (i : ℕ), f (f^[i] a)
have a₁ : f (f^[n] a) ≤ ⨆ (i : ℕ), f (f^[i] a)
Tactic: apply hf.strictMono.le_apply.trans