[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ ¬SupIrred a ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
[PROOFSTEP]
rw [SupIrred, not_and_or]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a) ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
[PROOFSTEP]
push_neg
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ (IsMin a ∨ Exists fun ⦃b⦄ => Exists fun ⦃c⦄ => b ⊔ c = a ∧ b ≠ a ∧ c ≠ a) ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
[PROOFSTEP]
rw [exists₂_congr]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ ∀ (a_1 b : α), a_1 ⊔ b = a ∧ a_1 ≠ a ∧ b ≠ a ↔ a_1 ⊔ b = a ∧ a_1 < a ∧ b < a
[PROOFSTEP]
simp (config := { contextual := true }) [@eq_comm _ _ a]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ ¬SupPrime a ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
[PROOFSTEP]
rw [SupPrime, not_and_or]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
[PROOFSTEP]
push_neg
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b c : α
⊢ (IsMin a ∨ Exists fun ⦃b⦄ => Exists fun ⦃c⦄ => a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c) ↔
    IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeSup α
a b✝ c✝ : α
h : ∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c
b c : α
ha : b ⊔ c = a
⊢ b = a ∨ c = a
[PROOFSTEP]
simpa [← ha] using h ha.ge
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
⊢ a ≠ ⊥
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred ⊥
⊢ False
[PROOFSTEP]
exact not_supIrred_bot ha
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≠ ⊥
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime ⊥
⊢ False
[PROOFSTEP]
exact not_supPrime_bot ha
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : sup s f = a
⊢ ∃ i, i ∈ s ∧ f i = a
[PROOFSTEP]
classical
induction' s using Finset.induction with i s _ ih
· simpa [ha.ne_bot] using h.symm
simp only [exists_prop, exists_mem_insert] at ih ⊢
rw [sup_insert] at h 
exact (ha.2 h).imp_right ih
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h : sup s f = a
⊢ ∃ i, i ∈ s ∧ f i = a
[PROOFSTEP]
induction' s using Finset.induction with i s _ ih
[GOAL]
case empty
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupIrred a
h✝ : sup s f = a
h : sup ∅ f = a
⊢ ∃ i, i ∈ ∅ ∧ f i = a
[PROOFSTEP]
simpa [ha.ne_bot] using h.symm
[GOAL]
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
h✝ : sup s✝ f = a
i : ι
s : Finset ι
a✝ : ¬i ∈ s
ih : sup s f = a → ∃ i, i ∈ s ∧ f i = a
h : sup (insert i s) f = a
⊢ ∃ i_1, i_1 ∈ insert i s ∧ f i_1 = a
[PROOFSTEP]
simp only [exists_prop, exists_mem_insert] at ih ⊢
[GOAL]
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
h✝ : sup s✝ f = a
i : ι
s : Finset ι
a✝ : ¬i ∈ s
ih : sup s f = a → ∃ i, i ∈ s ∧ f i = a
h : sup (insert i s) f = a
⊢ f i = a ∨ ∃ x, x ∈ s ∧ f x = a
[PROOFSTEP]
rw [sup_insert] at h 
[GOAL]
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupIrred a
h✝ : sup s✝ f = a
i : ι
s : Finset ι
a✝ : ¬i ∈ s
ih : sup s f = a → ∃ i, i ∈ s ∧ f i = a
h : f i ⊔ sup s f = a
⊢ f i = a ∨ ∃ x, x ∈ s ∧ f x = a
[PROOFSTEP]
exact (ha.2 h).imp_right ih
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≤ sup s f ↔ ∃ i, i ∈ s ∧ a ≤ f i
[PROOFSTEP]
classical
induction' s using Finset.induction with i s _ ih
· simp [ha.ne_bot]
· simp only [exists_prop, exists_mem_insert, sup_insert, ha.le_sup, ih]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≤ sup s f ↔ ∃ i, i ∈ s ∧ a ≤ f i
[PROOFSTEP]
induction' s using Finset.induction with i s _ ih
[GOAL]
case empty
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≤ sup ∅ f ↔ ∃ i, i ∈ ∅ ∧ a ≤ f i
[PROOFSTEP]
simp [ha.ne_bot]
[GOAL]
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a b c : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupPrime a
i : ι
s : Finset ι
a✝ : ¬i ∈ s
ih : a ≤ sup s f ↔ ∃ i, i ∈ s ∧ a ≤ f i
⊢ a ≤ sup (insert i s) f ↔ ∃ i_1, i_1 ∈ insert i s ∧ a ≤ f i_1
[PROOFSTEP]
simp only [exists_prop, exists_mem_insert, sup_insert, ha.le_sup, ih]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
⊢ ∃ s, sup s id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
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⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
⊢ ∃ s, sup s id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
apply WellFoundedLT.induction a _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
⊢ ∀ (x : α),
    (∀ (y : α), y < x → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) →
      ∃ s, sup s id = x ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
clear a
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
⊢ ∀ (x : α),
    (∀ (y : α), y < x → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b) →
      ∃ s, sup s id = x ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
rintro a ih
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
ih : ∀ (y : α), y < a → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
⊢ ∃ s, sup s id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
by_cases ha : SupIrred a
[GOAL]
case pos
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
ih : ∀ (y : α), y < a → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : SupIrred a
⊢ ∃ s, sup s id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
exact ⟨{ a }, by simp [ha]⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
ih : ∀ (y : α), y < a → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : SupIrred a
⊢ sup {a} id = a ∧ ∀ ⦃b : α⦄, b ∈ {a} → SupIrred b
[PROOFSTEP]
simp [ha]
[GOAL]
case neg
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
ih : ∀ (y : α), y < a → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : ¬SupIrred a
⊢ ∃ s, sup s id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
rw [not_supIrred] at ha 
[GOAL]
case neg
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
ih : ∀ (y : α), y < a → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
⊢ ∃ s, sup s id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
obtain ha | ⟨b, c, rfl, hb, hc⟩ := ha
[GOAL]
case neg.inl
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
ih : ∀ (y : α), y < a → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a
⊢ ∃ s, sup s id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
exact ⟨∅, by simp [ha.eq_bot]⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a✝ b c : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
a : α
ih : ∀ (y : α), y < a → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a
⊢ sup ∅ id = a ∧ ∀ ⦃b : α⦄, b ∈ ∅ → SupIrred b
[PROOFSTEP]
simp [ha.eq_bot]
[GOAL]
case neg.inr.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a b✝ c✝ : α
inst✝¹ : OrderBot α
s : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
b c : α
ih : ∀ (y : α), y < b ⊔ c → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
hb : b < b ⊔ c
hc : c < b ⊔ c
⊢ ∃ s, sup s id = b ⊔ c ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
[PROOFSTEP]
obtain ⟨s, rfl, hs⟩ := ih _ hb
[GOAL]
case neg.inr.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a b c✝ : α
inst✝¹ : OrderBot α
s✝ : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
c : α
s : Finset α
hs : ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ih : ∀ (y : α), y < sup s id ⊔ c → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
hb : sup s id < sup s id ⊔ c
hc : c < sup s id ⊔ c
⊢ ∃ s_1, sup s_1 id = sup s id ⊔ c ∧ ∀ ⦃b : α⦄, b ∈ s_1 → SupIrred b
[PROOFSTEP]
obtain ⟨t, rfl, ht⟩ := ih _ hc
[GOAL]
case neg.inr.intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝² : SemilatticeSup α
a b c : α
inst✝¹ : OrderBot α
s✝ : Finset ι
f : ι → α
inst✝ : WellFoundedLT α
s : Finset α
hs : ∀ ⦃b : α⦄, b ∈ s → SupIrred b
t : Finset α
ht : ∀ ⦃b : α⦄, b ∈ t → SupIrred b
ih : ∀ (y : α), y < sup s id ⊔ sup t id → ∃ s, sup s id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
hb : sup s id < sup s id ⊔ sup t id
hc : sup t id < sup s id ⊔ sup t id
⊢ ∃ s_1, sup s_1 id = sup s id ⊔ sup t id ∧ ∀ ⦃b : α⦄, b ∈ s_1 → SupIrred b
[PROOFSTEP]
exact ⟨s ∪ t, sup_union, forall_mem_union.2 ⟨hs, ht⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : SemilatticeInf α
a b✝ c✝ : α
h : ∀ ⦃b c : α⦄, b ⊓ c ≤ a → b ≤ a ∨ c ≤ a
b c : α
ha : b ⊓ c = a
⊢ b = a ∨ c = a
[PROOFSTEP]
simpa [← ha] using h ha.le
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeInf α
a b c : α
inst✝ : OrderTop α
s : Finset ι
f : ι → α
ha : InfIrred a
⊢ a ≠ ⊤
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeInf α
b c : α
inst✝ : OrderTop α
s : Finset ι
f : ι → α
ha : InfIrred ⊤
⊢ False
[PROOFSTEP]
exact not_infIrred_top ha
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeInf α
a b c : α
inst✝ : OrderTop α
s : Finset ι
f : ι → α
ha : InfPrime a
⊢ a ≠ ⊤
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeInf α
b c : α
inst✝ : OrderTop α
s : Finset ι
f : ι → α
ha : InfPrime ⊤
⊢ False
[PROOFSTEP]
exact not_infPrime_top ha
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : DistribLattice α
a b✝ c✝ : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ≤ b ⊔ c → a ≤ b ∨ a ≤ c
[PROOFSTEP]
simp_rw [← inf_eq_left, inf_sup_left]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : DistribLattice α
a b✝ c✝ : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ⊓ b ⊔ a ⊓ c = a → a ⊓ b = a ∨ a ⊓ c = a
[PROOFSTEP]
exact @h _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : DistribLattice α
a b✝ c✝ : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ b ⊓ c ≤ a → b ≤ a ∨ c ≤ a
[PROOFSTEP]
simp_rw [← sup_eq_left, sup_inf_left]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : DistribLattice α
a b✝ c✝ : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) = a → a ⊔ b = a ∨ a ⊔ c = a
[PROOFSTEP]
exact @h _ _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ ∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ ∀ ⦃b c : α⦄, b ⊓ c ≤ a → b ≤ a ∨ c ≤ a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : LinearOrder α
a x✝¹ x✝ : α
⊢ x✝¹ ⊔ x✝ = a → x✝¹ = a ∨ x✝ = a
[PROOFSTEP]
simpa only [sup_eq_max, max_eq_iff] using Or.imp And.left And.left
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : LinearOrder α
a x✝¹ x✝ : α
⊢ x✝¹ ⊓ x✝ = a → x✝¹ = a ∨ x✝ = a
[PROOFSTEP]
simpa only [inf_eq_min, min_eq_iff] using Or.imp And.left And.left
