awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Irreducible
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

Tactic:
rfl
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
h : ∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c
b c : α
ha : b ⊔ c = a
⊢ b = a ∨ c = a

Tactic:
simpa [← ha] using h ha.ge

Premises used: Eq.ge
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a b c : α
ha : SupPrime a
⊢ a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c

Tactic:
⟨fun h => ha.2 h, fun h => h.elim le_sup_of_le_left le_sup_of_le_right⟩

Premises used: le_sup_of_le_left, And.right, le_sup_of_le_right, Iff.intro, Or.elim
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
⊢ ¬SupIrred.{u_2} (α := α) ⊥

Tactic:
isMin_bot.not_supIrred

Premises used: IsMin.not_supIrred, isMin_bot
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
⊢ ¬SupPrime.{u_2} (α := α) ⊥

Tactic:
isMin_bot.not_supPrime

Premises used: IsMin.not_supPrime, isMin_bot
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
ha : SupIrred.{u_2} (α := α) ⊥
⊢ False

Tactic:
not_supIrred_bot ha

Premises used: not_supIrred_bot
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
ha : SupIrred.{u_2} (α := α) ⊥
⊢ False

Tactic:
exact not_supIrred_bot ha

Premises used: not_supIrred_bot
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
ha : SupPrime.{u_2} (α := α) ⊥
⊢ False

Tactic:
not_supPrime_bot ha

Premises used: not_supPrime_bot
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
ha : SupPrime.{u_2} (α := α) ⊥
⊢ False

Tactic:
exact not_supPrime_bot ha

Premises used: not_supPrime_bot
-- Module: Mathlib.Order.Irreducible
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
a : α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : sup ∅ f = a
⊢ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ f i = a

Tactic:
simpa [ha.ne_bot] using h.symm

Premises used: SupIrred.ne_bot, Eq.symm
-- Module: Mathlib.Order.Irreducible
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.insert i s).sup f = a
insert : f i = a ∨ ∃ x ∈ s, f x = a
⊢ ∃ i_1 ∈ Insert.insert i s, f i_1 = a

Tactic:
simp only [exists_mem_insert] at ih ⊢

Premises used: Finset.exists_mem_insert
-- Module: Mathlib.Order.Irreducible
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 ⊔ s.sup f = a

Tactic:
rw [sup_insert] at h

Premises used: Finset.sup_insert
-- Module: Mathlib.Order.Irreducible
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 : f i ⊔ s.sup f = a
⊢ f i = a ∨ ∃ x ∈ s, f x = a

Tactic:
(ha.2 h).imp_right ih

Premises used: And.right, Or.imp_right
-- Module: Mathlib.Order.Irreducible
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 : f i ⊔ s.sup f = a
⊢ f i = a ∨ ∃ x ∈ s, f x = a

Tactic:
exact (ha.2 h).imp_right ih

Premises used: And.right, Or.imp_right
-- Module: Mathlib.Order.Irreducible
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
insert :
  ∀ (i : ι) (s : Finset ι),
    i ∉ s →
      ∀ (ih : ∀ (h : s.sup f = a), ∃ i ∈ s, f i = a) (h : (Insert.insert i s).sup f = a),
        ∃ i_1 ∈ Insert.insert i s, f i_1 = a
⊢ ∃ i ∈ s, 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

Premises used: Finset.sup_insert, Finset.exists_mem_insert, SupIrred.ne_bot, Insert.insert, Eq.symm
-- Module: Mathlib.Order.Irreducible
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
insert :
  ∀ (i : ι) (s : Finset ι),
    i ∉ s →
      ∀ (ih : ∀ (h : s.sup f = a), ∃ i ∈ s, f i = a) (h : (Insert.insert i s).sup f = a),
        ∃ i_1 ∈ Insert.insert i s, f i_1 = a
⊢ ∃ i ∈ s, 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

Premises used: Finset.sup_insert, Finset.exists_mem_insert, SupIrred.ne_bot, Insert.insert, Eq.symm
-- Module: Mathlib.Order.Irreducible
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
a : α
inst_1 : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≤ sup ∅ f ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ a ≤ f i

Tactic:
simp [ha.ne_bot]

Premises used: SupPrime.ne_bot
-- Module: Mathlib.Order.Irreducible
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
a : α
inst_1 : OrderBot α
s_1 : Finset ι
f : ι → α
ha : SupPrime a
i : ι
s : Finset ι
h : 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:
simp only [exists_mem_insert, sup_insert, ha.le_sup, ih]

Premises used: Finset.sup_insert, Finset.exists_mem_insert, SupPrime.le_sup
-- Module: Mathlib.Order.Irreducible
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
insert :
  ∀ (i : ι) (s : Finset ι),
    i ∉ s →
      ∀ (ih : a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i), a ≤ (Insert.insert i s).sup f ↔ ∃ i_1 ∈ Insert.insert i s, a ≤ f i_1
⊢ a ≤ s.sup f ↔ ∃ i ∈ s, 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]

Premises used: SupPrime.ne_bot, Finset.sup_insert, Finset.exists_mem_insert, Insert.insert, SupPrime.le_sup
-- Module: Mathlib.Order.Irreducible
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
insert :
  ∀ (i : ι) (s : Finset ι),
    i ∉ s →
      ∀ (ih : a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i), a ≤ (Insert.insert i s).sup f ↔ ∃ i_1 ∈ Insert.insert i s, a ≤ f i_1
⊢ a ≤ s.sup f ↔ ∃ i ∈ s, 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]

Premises used: SupPrime.ne_bot, Finset.sup_insert, Finset.exists_mem_insert, Insert.insert, SupPrime.le_sup
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
a : α
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
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
apply WellFoundedLT.induction a _

Premises used: WellFoundedLT.induction
-- Module: Mathlib.Order.Irreducible
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
neg : ∀ (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

Tactic:
by_cases ha : SupIrred a

Premises used: SupIrred
-- Module: Mathlib.Order.Irreducible
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
⊢ sup {a} id = a ∧ ∀ ⦃b : α⦄, Membership.mem (γ := Finset α) {a} b → SupIrred b

Tactic:
simp [ha]
-- Module: Mathlib.Order.Irreducible
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

Tactic:
exact ⟨{a}, by simp [ha]⟩
-- Module: Mathlib.Order.Irreducible
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
⊢ IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a

Tactic:
rw [not_supIrred] at ha

Premises used: not_supIrred
-- Module: Mathlib.Order.Irreducible
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
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

Tactic:
obtain ha | ⟨b, c, rfl, hb, hc⟩ := ha

Premises used: rfl
-- Module: Mathlib.Order.Irreducible
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
⊢ sup ∅ id = a ∧ ∀ ⦃b : α⦄, Membership.mem (γ := Finset α) ∅ b → SupIrred b

Tactic:
simp [ha.eq_bot]

Premises used: IsMin.eq_bot
-- Module: Mathlib.Order.Irreducible
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
⊢ ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
exact ⟨∅, by simp [ha.eq_bot]⟩
-- Module: Mathlib.Order.Irreducible
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
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
⊢ ∃ (s : Finset α), s.sup id = b ⊔ c ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
obtain ⟨s, rfl, hs⟩ := ih _ hb

Premises used: rfl
-- Module: Mathlib.Order.Irreducible
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
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
⊢ ∃ (s_1 : Finset α), s_1.sup id = s.sup id ⊔ c ∧ ∀ ⦃b : α⦄, b ∈ s_1 → SupIrred b

Tactic:
obtain ⟨t, rfl, ht⟩ := ih _ hc

Premises used: rfl
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
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:
⟨s ∪ t, sup_union, forall_mem_union.2 ⟨hs, ht⟩⟩

Premises used: Iff.mpr, Finset.sup_union, And.intro, Exists.intro, Union.union, Finset.forall_mem_union
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : WellFoundedLT α
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:
exact ⟨s ∪ t, sup_union, forall_mem_union.2 ⟨hs, ht⟩⟩
-- Module: Mathlib.Order.Irreducible
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
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
⊢ ∃ (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⟩⟩

Premises used: WellFoundedLT.induction, not_supIrred, rfl, SupIrred
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
a : α
ha : IsMax a
⊢ ¬InfIrred a

Tactic:
fun h => h.1 ha

Premises used: And.left, Not
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
a : α
ha : IsMax a
⊢ ¬InfPrime a

Tactic:
fun h => h.1 ha

Premises used: And.left, Not
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
a : α
⊢ ¬InfIrred a ↔ IsMax a ∨ ∃ (b : α) (c : α), b ⊓ c = a ∧ a < b ∧ a < c

Tactic:
@not_supIrred αᵒᵈ _ _

Premises used: InfIrred, not_supIrred, OrderDual, IsMax
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
a : α
⊢ ¬InfPrime a ↔ IsMax a ∨ ∃ (b : α) (c : α), b ⊓ c ≤ a ∧ ¬b ≤ a ∧ ¬c ≤ a

Tactic:
@not_supPrime αᵒᵈ _ _

Premises used: not_supPrime, InfPrime, OrderDual, IsMax
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c ≤ a → b ≤ a ∨ c ≤ a
b c : α
ha : b ⊓ c = a
⊢ b = a ∨ c = a

Tactic:
simpa [← ha] using h ha.le

Premises used: Eq.le
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
a b c : α
ha : InfPrime a
⊢ b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a

Tactic:
⟨fun h => ha.2 h, fun h => h.elim inf_le_of_left_le inf_le_of_right_le⟩

Premises used: inf_le_of_right_le, inf_le_of_left_le, And.right, Iff.intro, Or.elim
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : OrderTop α
⊢ ¬InfIrred.{u_2} (α := α) ⊤

Tactic:
isMax_top.not_infIrred

Premises used: IsMax.not_infIrred, isMax_top
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : OrderTop α
⊢ ¬InfPrime.{u_2} (α := α) ⊤

Tactic:
isMax_top.not_infPrime

Premises used: isMax_top, IsMax.not_infPrime
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : OrderTop α
ha : InfIrred.{u_2} (α := α) ⊤
⊢ False

Tactic:
not_infIrred_top ha

Premises used: not_infIrred_top
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : OrderTop α
ha : InfIrred.{u_2} (α := α) ⊤
⊢ False

Tactic:
exact not_infIrred_top ha

Premises used: not_infIrred_top
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : OrderTop α
ha : InfPrime.{u_2} (α := α) ⊤
⊢ False

Tactic:
not_infPrime_top ha

Premises used: not_infPrime_top
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : OrderTop α
ha : InfPrime.{u_2} (α := α) ⊤
⊢ False

Tactic:
exact not_infPrime_top ha

Premises used: not_infPrime_top
-- Module: Mathlib.Order.Irreducible
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeInf α
a : α
inst_1 : OrderTop α
s : Finset ι
f : ι → α
⊢ InfIrred a → s.inf f = a → ∃ i ∈ s, f i = a

Tactic:
@SupIrred.finset_sup_eq _ αᵒᵈ _ _ _ _ _

Premises used: SupIrred.finset_sup_eq, InfIrred, OrderDual, Finset.inf, IsMax
-- Module: Mathlib.Order.Irreducible
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeInf α
a : α
inst_1 : OrderTop α
s : Finset ι
f : ι → α
ha : InfPrime a
⊢ s.inf f ≤ a ↔ ∃ i ∈ s, f i ≤ a

Tactic:
@SupPrime.le_finset_sup _ αᵒᵈ _ _ _ _ _ ha

Premises used: OrderDual, Finset.inf, SupPrime.le_finset_sup
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : OrderTop α
inst_2 : WellFoundedGT α
a : α
⊢ ∃ (s : Finset α), s.inf id = a ∧ ∀ ⦃b : α⦄, b ∈ s → InfIrred b

Tactic:
exists_supIrred_decomposition (α := αᵒᵈ) _

Premises used: Set.Mem, exists_supIrred_decomposition, setOf, InfIrred, OrderDual, Finset.inf, IsMax
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
⊢ InfIrred (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ SupIrred a

Tactic:
Iff.rfl

Premises used: Iff.rfl, OrderDual, IsMin, SupIrred
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
⊢ InfPrime (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ SupPrime a

Tactic:
Iff.rfl

Premises used: SupPrime, Iff.rfl, OrderDual, IsMin
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : αᵒᵈ
⊢ SupIrred (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ↔ InfIrred a

Tactic:
Iff.rfl

Premises used: Iff.rfl, InfIrred, OrderDual, IsMax
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : αᵒᵈ
⊢ SupPrime (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ↔ InfPrime a

Tactic:
Iff.rfl

Premises used: Iff.rfl, InfPrime, OrderDual, IsMax
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
a : α
⊢ SupIrred (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ InfIrred a

Tactic:
Iff.rfl

Premises used: Iff.rfl, InfIrred, OrderDual, IsMax
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
a : α
⊢ SupPrime (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ InfPrime a

Tactic:
Iff.rfl

Premises used: Iff.rfl, InfPrime, OrderDual, IsMax
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
a : αᵒᵈ
⊢ InfIrred (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ↔ SupIrred a

Tactic:
Iff.rfl

Premises used: Iff.rfl, OrderDual, IsMin, SupIrred
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeInf α
a : αᵒᵈ
⊢ InfPrime (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ↔ SupPrime a

Tactic:
Iff.rfl

Premises used: SupPrime, Iff.rfl, OrderDual, IsMin
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
simp_rw : a ⊓ b ⊔ a ⊓ c = a → a ⊓ b = a ∨ a ⊓ c = a
⊢ a ≤ b ⊔ c → a ≤ b ∨ a ≤ c

Tactic:
simp_rw [← inf_eq_left, inf_sup_left]

Premises used: inf_sup_left, inf_eq_left
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ⊓ b ⊔ a ⊓ c = a → a ⊓ b = a ∨ a ⊓ c = a

Tactic:
@h _ _
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ⊓ b ⊔ a ⊓ c = a → a ⊓ b = a ∨ a ⊓ c = a

Tactic:
exact @h _ _
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
simp_rw : (a ⊔ b) ⊓ (a ⊔ c) = a → a ⊔ b = a ∨ a ⊔ c = a
⊢ b ⊓ c ≤ a → b ≤ a ∨ c ≤ a

Tactic:
simp_rw [← sup_eq_left, sup_inf_left]

Premises used: sup_eq_left, sup_inf_left
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) = a → a ⊔ b = a ∨ a ⊔ c = a

Tactic:
@h _ _
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) = a → a ⊔ b = a ∨ a ⊔ c = a

Tactic:
exact @h _ _
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : LinearOrder α
a : α
⊢ ∀ ⦃b c : α⦄, a ≤ max b c → a ≤ b ∨ a ≤ c

Tactic:
simp
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : LinearOrder α
a : α
⊢ ∀ ⦃b c : α⦄, min b c ≤ a → b ≤ a ∨ c ≤ a

Tactic:
simp
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : LinearOrder α
a x x_1 : α
⊢ max x x_1 = a → x = a ∨ x_1 = a

Tactic:
simpa only [max_eq_iff] using Or.imp And.left And.left

Premises used: And.left, Or.imp, max_eq_iff
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : LinearOrder α
a x x_1 : α
⊢ min x x_1 = a → x = a ∨ x_1 = a

Tactic:
simpa only [min_eq_iff] using Or.imp And.left And.left

Premises used: min_eq_iff, And.left, Or.imp
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
⊢ IsNormal f ↔ StrictMono f ∧ ∀ (o : α), IsSuccLimit o → ∀ (a : β), (∀ b < o, f b ≤ a) → f o ≤ a

Tactic:
simp [isNormal_iff', mem_lowerBounds, mem_upperBounds]

Premises used: mem_lowerBounds, Order.isNormal_iff', mem_upperBounds
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : IsNormal f
⊢ Monotone f

Tactic:
hf.strictMono.monotone

Premises used: StrictMono.monotone, Order.IsNormal.strictMono
-- Module: Mathlib.Order.IsNormal
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)

Tactic:
⟨?_, hf.2 ha⟩

Premises used: Order.IsNormal.mem_lowerBounds_upperBounds_of_isSuccLimit, IsLeast, And.intro, IsLUB