-- Mathlib/Order/Irreducible.lean
theorem exists_supIrred_decomposition (a : α) :
    ∃ s : Finset α, s.sup id = a ∧ ∀ ⦃b⦄, b ∈ s → SupIrred b

Proof state:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
⊢ ∀ (x : α),
    (∀ y < x, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) → ∃ s, s.sup id = x ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
rintro a ih

Result:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Proof state:
case neg.inl
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
exact ⟨∅, by simp [ha.eq_bot]⟩

Result:
no goals

Proof state:
case neg.inr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : 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, 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, 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⟩⟩

Result:
no goals

Proof state:
case neg
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : ¬SupIrred a
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
rw [not_supIrred] at ha

Result:
case neg
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Proof state:
case neg
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

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

Result:
case neg.inl
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

case neg.inr.intro.intro.intro.intro
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
b c : α
ih : ∀ y < b ⊔ c, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
hb : b < b ⊔ c
hc : c < b ⊔ c
⊢ ∃ s, s.sup id = b ⊔ c ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Proof state:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a
⊢ ∅.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ ∅ → SupIrred b

Tactic:
simp [ha.eq_bot]

Result:
no goals

Proof state:
case neg.inr.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
c : α
s : Finset α
hs : ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ih : ∀ y < s.sup id ⊔ c, ∃ s, 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, s_1.sup id = s.sup id ⊔ c ∧ ∀ ⦃b : α⦄, b ∈ s_1 → SupIrred b

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

Result:
case neg.inr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : 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, 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, s_1.sup id = s.sup id ⊔ t.sup id ∧ ∀ ⦃b : α⦄, b ∈ s_1 → SupIrred b

Proof state:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
apply WellFoundedLT.induction a _

Result:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
⊢ ∀ (x : α),
    (∀ y < x, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) → ∃ s, s.sup id = x ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Proof state:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
⊢ ∀ (x : α),
    (∀ y < x, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) → ∃ s, s.sup id = x ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
clear a

Result:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
⊢ ∀ (x : α),
    (∀ y < x, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) → ∃ s, s.sup id = x ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Proof state:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
by_cases ha : SupIrred a

Result:
case pos
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : SupIrred a
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

case neg
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : ¬SupIrred a
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Proof state:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : SupIrred a
⊢ {a}.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ {a} → SupIrred b

Tactic:
simp [ha]

Result:
no goals

Proof state:
case pos
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : SupIrred a
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
exact ⟨{a}, by simp [ha]⟩

Result:
no goals

Proof state:
case neg.inr.intro.intro.intro.intro
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
b c : α
ih : ∀ y < b ⊔ c, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
hb : b < b ⊔ c
hc : c < b ⊔ c
⊢ ∃ s, s.sup id = b ⊔ c ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

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

Result:
case neg.inr.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
c : α
s : Finset α
hs : ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ih : ∀ y < s.sup id ⊔ c, ∃ s, 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, s_1.sup id = s.sup id ⊔ c ∧ ∀ ⦃b : α⦄, b ∈ s_1 → SupIrred b