mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case succ.cons_cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
IH : sublistsLen (n + 1) l₁✝ <+ sublistsLen (n + 1) l₂✝
⊢ sublistsLen (n + 1) (a :: l₁✝) <+ sublistsLen (n + 1) (a :: l₂✝)

Tactic:
simpa using

Goal state after:
case succ.cons_cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
IH : sublistsLen (n + 1) l₁✝ <+ sublistsLen (n + 1) l₂✝
⊢ sublistsLen (n + 1) l₁✝ ++ map (cons a) (sublistsLen n l₁✝) <+
    sublistsLen (n + 1) l₂✝ ++ map (cons a) (sublistsLen n l₂✝)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
h✝ : l.Nodup
l₁ l₂ : List α
h : ((Lex fun x1 x2 ↦ x1 ≠ x2) on reverse) l₁ l₂
⊢ l₁ ≠ l₂

Tactic:
simpa using

Goal state after:
α : Type u
l : List α
h✝ : l.Nodup
l₁ l₂ : List α
h : ((Lex fun x1 x2 ↦ x1 ≠ x2) on reverse) l₁ l₂
⊢ ¬l₁ = l₂
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : (l₁, l₂) ∈ [].sublists.zip [].sublists.reverse
⊢ l₁ = [] ∧ l₂ = []

Tactic:
simpa using

Goal state after:
α : Type u
l₁ l₂ : List α
h : (l₁, l₂) ∈ [].sublists.zip [].sublists.reverse
⊢ l₁ = [] ∧ l₂ = []
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset α
⊢ IsLUB (↑s) (s.sup id)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset α
⊢ IsLUB (↑s) (s.sup id)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
t : Finset γ
f : β → γ → α
a : α
⊢ (s.sup fun b ↦ t.sup (f b)) ≤ a ↔ (t.sup fun c ↦ s.sup fun b ↦ f b c) ≤ a

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
t : Finset γ
f : β → γ → α
a : α
⊢ (∀ b ∈ s, ∀ b_1 ∈ t, f b b_1 ≤ a) ↔ ∀ b ∈ t, ∀ b_1 ∈ s, f b_1 b ≤ a
Module: Mathlib.Data.Set.Finite.Powerset

Goal state before:
pp: α : Type u
a : Set α
h : a.Finite
s : Set α
⊢ s ∈ {b | b ⊆ a} ↔ s ∈ ↑(Finset.map Finset.coeEmb.toEmbedding h.toFinset.powerset)

Tactic:
simpa using

Goal state after:
α : Type u
a : Set α
h : a.Finite
s : Set α
⊢ s ⊆ a → s.Finite
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s t : Finset α
a : α
ht : t ∈ s.powerset
h : a ∉ s
⊢ a ∉ t

Tactic:
apply mt _ h
  apply mem_powerset.1 ht

Goal state after:
Module: Mathlib.Data.Set.Finite.Range

Goal state before:
pp: α : Type u
β : Type v
s : Set α
hs : s.Finite
F : (i : α) → i ∈ s → β
this : Finite ↑s
⊢ {y | ∃ x, ∃ (hx : x ∈ s), F x hx = y}.Finite

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
s : Set α
hs : s.Finite
F : (i : α) → i ∈ s → β
this : Finite ↑s
⊢ {y | ∃ x, ∃ (hx : x ∈ s), F x hx = y}.Finite
Module: Mathlib.Data.Set.Finite.Range

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
hsu : u ⊆ f '' s
⊢ ∃ t ⊆ s, ∃ (_ : t.Finite), f '' t = u

Tactic:
have : Finite u := Finite.to_subtype hu
  choose g hg hg' using hsu
  let g' (x : u) : α := g x.property
  exact ⟨range g', fun a ha ↦ by aesop, finite_range _, by aesop⟩

Goal state after:
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq (Finset α)
s : Finset α
⊢ s.powerset = (range (#s + 1)).biUnion fun i ↦ powersetCard i s

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq (Finset α)
s : Finset α
⊢ s.powerset = (range (#s + 1)).biUnion fun i ↦ powersetCard i s
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case ex
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∃ x ∈ s, y ∈ f x

Tactic:
simpa using

Goal state after:
case ex
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∃ x ∈ s, y ∈ f x
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
a b : Finset α
r : ℕ
hab : #a = #b
hr₀ : r ≠ 0
hra : r ≤ #a
h : powersetCard r a = powersetCard r b
⊢ a = b

Tactic:
simpa using

Goal state after:
α : Type u_1
a b : Finset α
r : ℕ
hab : #a = #b
hr₀ : r ≠ 0
hra : r ≤ #a
h : powersetCard r a = powersetCard r b
⊢ a = b
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : c ∉ t
⊢ ((∀ b ∈ t, f b < a) → t.sup f < a) → (∀ b ∈ cons c t hc, f b < a) → (cons c t hc).sup f < a

Tactic:
simpa using

Goal state after:
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : c ∉ t
⊢ ((∀ b ∈ t, f b < a) → t.sup f < a) → (f c < a ∧ ∀ b ∈ t, f b < a) → f c < a ∧ t.sup f < a
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case insert.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
⊢ max (f a) (s.sup f) ∈ f '' ↑(insert a s)

Tactic:
| inr hs =>

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SemilatticeSup α
s : Finset β
t : Finset γ
hs : s.Nonempty
ht : t.Nonempty
f : β → γ → α
a : α
⊢ (s.sup' hs fun b ↦ t.sup' ht (f b)) ≤ a ↔ (t.sup' ht fun c ↦ s.sup' hs fun b ↦ f b c) ≤ a

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SemilatticeSup α
s : Finset β
t : Finset γ
hs : s.Nonempty
ht : t.Nonempty
f : β → γ → α
a : α
⊢ (∀ b ∈ s, ∀ b_1 ∈ t, f b b_1 ≤ a) ↔ ∀ b ∈ t, ∀ b_1 ∈ s, f b_1 b ≤ a
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hdg : Directed (fun x1 x2 ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : IsEmpty ι
⊢ iSup f ≤ iSup g

Tactic:
iSup_of_empty',

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hdg : Directed (fun x1 x2 ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : IsEmpty ι
⊢ sSup ∅ ≤ iSup g
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ (range fun i ↦ f ⟨i, ⋯⟩) = range f

Tactic:
apply Subset.antisymm

Goal state after:
case h₁
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ (range fun i ↦ f ⟨i, ⋯⟩) ⊆ range f

case h₂
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ range f ⊆ range fun i ↦ f ⟨i, ⋯⟩
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Nonempty ι
f : ι → α
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hf : BddAbove (range f)
x✝ : α
⊢ x✝ ∈ Ici (⨆ i, f i) ↔ x✝ ∈ ⋂ i, Ici (f i)

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Nonempty ι
f : ι → α
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hf : BddAbove (range f)
x✝ : α
⊢ ⨆ i, f i ≤ x✝ ↔ ∀ (i : ι), f i ≤ x✝
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hne : s.Nonempty
hbdd : BddAbove s
⊢ l (sSup s) = ⨆ x, l ↑x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hne : s.Nonempty
hbdd : BddAbove s
⊢ l (sSup s) = sSup (l '' s)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
s : Set (Set α)
hs : s.Finite
H : ∀ t ∈ s, t.Finite
⊢ (⋃₀ s).Finite

Tactic:
simpa using

Goal state after:
α : Type u
s : Set (Set α)
hs : s.Finite
H : ∀ t ∈ s, t.Finite
⊢ (⋃ i ∈ s, i).Finite
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∈ s
⊢ ↑(⨆ (_ : i ∈ s), f i) ≤ ⨆ i ∈ s, ↑(f i)

Tactic:
simpa using

Goal state after:
case pos
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∈ s
⊢ ↑(f i) ≤ ⨆ i ∈ s, ↑(f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∉ s
⊢ ↑(⨆ (_ : i ∈ s), f i) ≤ ⨆ i ∈ s, ↑(f i)

Tactic:
simpa using

Goal state after:
case neg
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∉ s
⊢ ↑⊥ ≤ ⨆ i ∈ s, ↑(f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: ι : Type u_5
s : Set ι
hs : s.Nonempty
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
⊢ ↑(⨆ i ∈ s, f i) = ⨆ i ∈ s, ↑(f i)

Tactic:
rcases hs with ⟨j, hj⟩
  have : Nonempty ι := Nonempty.intro j
  refine le_antisymm ((WithBot.coe_iSup (OrderTop.bddAbove _)).trans_le <|
    iSup_le_iff.mpr fun i ↦ ?_) <| iSup_le_iff.mpr <| fun _ ↦ iSup_le_iff.mpr <|
      fun hi ↦ WithBot.coe_le_coe.mpr (le_biSup _ hi)
  by_cases h : i ∈ s
  · simpa only [iSup_pos h] using by apply le_biSup _ h
  · simpa only [iSup_neg h] using le_trans (by simp) (le_biSup _ hj)

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
⊢ ↑(⨅ i ∈ s, f i) ≤ ⨅ i ∈ s, ↑(f i)

Tactic:
simpa using

Goal state after:
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
⊢ ∀ i ∈ s, ⨅ i ∈ s, f i ≤ f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
i : ι
h : i ∈ s
⊢ ⨅ i ∈ s, ↑(f i) ≤ ↑(⨅ (_ : i ∈ s), f i)

Tactic:
simpa using

Goal state after:
case pos
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
i : ι
h : i ∈ s
⊢ ⨅ i ∈ s, ↑(f i) ≤ ↑(f i)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
⊢ ∀ (x : ↑s), ∃ i, ↑x ∈ t i

Tactic:
simpa using

Goal state after:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
⊢ ∀ a ∈ s, ∃ i, a ∈ t i
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ ↑s, f i ∈ f '' ↑s

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ∃ x ∈ s, f x = ⨆ i ∈ s, f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : IsEmpty ι
⊢ iSup f ≤ iSup g

Tactic:
iSup_of_empty',

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : IsEmpty ι
⊢ sSup ∅ ≤ iSup g
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ i ∈ ↑s, f i ∈ f '' ↑s

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ∃ x ∈ s, f x = ⨅ i ∈ s, f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h✝ : IsEmpty ι
⊢ ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x

Tactic:
simp [iSup_of_empty']

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝⁴ : Finite ι
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirectedOrder ι'
inst✝ : Order.Frame α
f : ι → ι' → α
hf : ∀ (i : ι), Monotone (f i)
⊢ ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j

Tactic:
simpa using

Goal state after:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝⁴ : Finite ι
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirectedOrder ι'
inst✝ : Order.Frame α
f : ι → ι' → α
hf : ∀ (i : ι), Monotone (f i)
⊢ ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝ : IsEmpty β
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

Tactic:
simp [iSup_of_empty']

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : IsEmpty γ
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

Tactic:
simp [iSup_of_empty']

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type v
κ : ι → Sort w
inst✝¹ : Nonempty ((a : ι) → κ a)
inst✝ : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
h : ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α), ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)
this : Nonempty ((a : ι) → PLift (κ a))
⊢ ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)

Tactic:
simpa using

Goal state after:
α : Type u
ι : Type v
κ : ι → Sort w
inst✝¹ : Nonempty ((a : ι) → κ a)
inst✝ : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
h : ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α), ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)
this : Nonempty ((a : ι) → PLift (κ a))
⊢ ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
x✝ : α
⊢ x✝ ∈ Iic (⨅ i, f i) ↔ x✝ ∈ ⋂ i, Iic (f i)

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
x✝ : α
⊢ x✝ ≤ ⨅ i, f i ↔ ∀ (i : ι), x✝ ≤ f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : IsEmpty (Subtype p)
⊢ iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Tactic:
iSup_of_empty',

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : IsEmpty (Subtype p)
⊢ sSup ∅ = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, sSup ∅ ≤ f x
⊢ ⨆ x ∈ l, f x ∈ map f l

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, sSup ∅ ≤ f x
⊢ ∃ a ∈ l, f a = ⨆ x ∈ l, f x
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, sSup ∅ ≤ f x
⊢ ∃ x ∈ l.toFinset, sSup ∅ ≤ f x

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, sSup ∅ ≤ f x
⊢ ∃ x ∈ l, sSup ∅ ≤ f x
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, f x ≤ sInf ∅
⊢ ⨅ x ∈ l, f x ∈ map f l

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, f x ≤ sInf ∅
⊢ ∃ a ∈ l, f a = ⨅ x ∈ l, f x
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, f x ≤ sInf ∅
⊢ ∃ x ∈ l.toFinset, f x ≤ sInf ∅

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, f x ≤ sInf ∅
⊢ ∃ x ∈ l, f x ≤ sInf ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ x ∈ s, f x ∈ map f s

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ∃ a ∈ s, f a = ⨆ x ∈ s, f x
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ∃ x ∈ s.toFinset, sSup ∅ ≤ f x

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ∃ x ∈ s, sSup ∅ ≤ f x
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ x ∈ s, f x ∈ map f s

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ∃ a ∈ s, f a = ⨅ x ∈ s, f x
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ∃ x ∈ s.toFinset, f x ≤ sInf ∅

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ∃ x ∈ s, f x ≤ sInf ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ x ∈ s, f x ∈ map f s

Tactic:
classical
  simpa using s.toFinset.ciInf_mem_image f (by simpa using h)

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
s : Set α
⊢ (s \ ⋃ x, Ioo ↑x.1 ↑x.2).Finite

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : LinearOrder α
s : Set α
⊢ (s \ ⨆ i ∈ s, ⨆ i_1 ∈ s, Ioo i i_1).Finite
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j ↦ f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ x, f ↑x
this : Nonempty ↑c
⊢ ∃ i ∈ c, ↑s ⊆ f i

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j ↦ f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ x, f ↑x
this : Nonempty ↑c
⊢ ∃ i ∈ c, ↑s ⊆ f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
l : List ι
f : ι → α
h : l ≠ []
⊢ ∃ x ∈ l, sSup ∅ ≤ f x

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
l : List ι
f : ι → α
h : l ≠ []
⊢ ∃ x, x ∈ l
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Multiset ι
f : ι → α
h : s ≠ 0
⊢ ∃ x ∈ s, sSup ∅ ≤ f x

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Multiset ι
f : ι → α
h : s ≠ 0
⊢ ∃ x, x ∈ s
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
⊢ BddAbove (range fun i ↦ g ↑i)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
⊢ ∃ x, ∀ a ∈ s, g (f a) ≤ x
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
t : ↑(f '' s)
ht : g ↑t = g (f ↑⟨i, h⟩)
⊢ BddAbove (g '' f '' s)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
t : ↑(f '' s)
ht : g ↑t = g (f ↑⟨i, h⟩)
⊢ ∃ x, ∀ a ∈ s, g (f a) ≤ x
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : Exists p
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
have : Nonempty <| Exists p := ⟨h⟩
    refine ciSup_le fun ⟨i, hi⟩ ↦ le_ciSup₂ (f := fun _ _ ↦ _) ⟨f ⟨i, hi⟩, ?_⟩ i hi
    rintro _ ⟨_, ⟨j, rfl⟩, ⟨hj, rfl⟩⟩
    rfl

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → t ⊆ s → P s
h : Minimal P s
x : α
hxs : x ∈ s
hx : P (s.erase x)
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → t ⊆ s → P s
h : Minimal P s
x : α
hxs : x ∈ s
hx : P (s.erase x)
⊢ False
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
⊢ ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x

Tactic:
simpa using! _root_.iSup_union

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : IsEmpty ι
f : ι → α
⊢ ⨆ i, f i = ⊥

Tactic:
iSup_of_empty',

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : IsEmpty ι
f : ι → α
⊢ sSup ∅ = ⊥
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : IsEmpty ι
f : ι → α
⊢ ⨆ i, f i = ⊥

Tactic:
rw [iSup_of_empty', csSup_empty]

Goal state after: