mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case empty
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
⊢ a ∈ ∅.sup f ↔ ∃ i ∈ ∅, a ∈ f i

pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : a ∈ s✝.sup f ↔ ∃ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).sup f ↔ ∃ i ∈ cons a✝¹ s✝ h✝, a ∈ f i

Tactic:
<;>

Goal state after:
case empty
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
⊢ a ∈ ∅.sup f ↔ ∃ i ∈ ∅, a ∈ f i

case cons
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : a ∈ s✝.sup f ↔ ∃ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).sup f ↔ ∃ i ∈ cons a✝¹ s✝ h✝, a ∈ f i
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : ConditionallyCompletePartialOrderSup α
p : Prop
inst✝ : Decidable p
f : p → α
H : p
⊢ ⨆ (h : p), f h = if h : p then f h else sSup ∅

pp: case neg
α : Type u_1
inst✝¹ : ConditionallyCompletePartialOrderSup α
p : Prop
inst✝ : Decidable p
f : p → α
H : ¬p
⊢ ⨆ (h : p), f h = if h : p then f h else sSup ∅

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝¹ : ConditionallyCompletePartialOrderSup α
p : Prop
inst✝ : Decidable p
f : p → α
H : p
⊢ ⨆ (h : p), f h = if h : p then f h else sSup ∅

case neg
α : Type u_1
inst✝¹ : ConditionallyCompletePartialOrderSup α
p : Prop
inst✝ : Decidable p
f : p → α
H : ¬p
⊢ ⨆ (h : p), f h = if h : p then f h else sSup ∅
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
h✝ : a = ⊤
⊢ untopD ⊤ (map Subtype.val ⊤) = a

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
h✝ : ¬a = ⊤
⊢ untopD ⊤ (map Subtype.val ↑⟨a, h✝⟩) = a

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
h✝ : a = ⊤
⊢ untopD ⊤ (map Subtype.val ⊤) = a

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
h✝ : ¬a = ⊤
⊢ untopD ⊤ (map Subtype.val ↑⟨a, h✝⟩) = a
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ⊤ ∈ Ioi ↑a ↔ ⊤ ∈ some '' Ioi a ∪ {⊤}

pp: case coe
α : Type u_1
inst✝ : Preorder α
a a✝ : α
⊢ ↑a✝ ∈ Ioi ↑a ↔ ↑a✝ ∈ some '' Ioi a ∪ {⊤}

Tactic:
<;>

Goal state after:
case top
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ⊤ ∈ Ioi ↑a ↔ ⊤ ∈ some '' Ioi a ∪ {⊤}

case coe
α : Type u_1
inst✝ : Preorder α
a a✝ : α
⊢ ↑a✝ ∈ Ioi ↑a ↔ ↑a✝ ∈ some '' Ioi a ∪ {⊤}
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ⊤ ∈ Ici ↑a ↔ ⊤ ∈ some '' Ici a ∪ {⊤}

pp: case coe
α : Type u_1
inst✝ : Preorder α
a a✝ : α
⊢ ↑a✝ ∈ Ici ↑a ↔ ↑a✝ ∈ some '' Ici a ∪ {⊤}

Tactic:
<;>

Goal state after:
case top
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ⊤ ∈ Ici ↑a ↔ ⊤ ∈ some '' Ici a ∪ {⊤}

case coe
α : Type u_1
inst✝ : Preorder α
a a✝ : α
⊢ ↑a✝ ∈ Ici ↑a ↔ ↑a✝ ∈ some '' Ici a ∪ {⊤}
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t st : Finset ι
a : α
x✝ : a ∈ Set.range fun x ↦ ⨆ (_ : x ∈ st), f x
i : ι
ha : (fun x ↦ ⨆ (_ : x ∈ st), f x) i = a
h : i ∈ st
⊢ (fun x ↦ ⨆ (_ : x ∈ st), f x) i ≤ st.sup f

pp: case neg
ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t st : Finset ι
a : α
x✝ : a ∈ Set.range fun x ↦ ⨆ (_ : x ∈ st), f x
i : ι
ha : (fun x ↦ ⨆ (_ : x ∈ st), f x) i = a
h : i ∉ st
⊢ (fun x ↦ ⨆ (_ : x ∈ st), f x) i ≤ st.sup f

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t st : Finset ι
a : α
x✝ : a ∈ Set.range fun x ↦ ⨆ (_ : x ∈ st), f x
i : ι
ha : (fun x ↦ ⨆ (_ : x ∈ st), f x) i = a
h : i ∈ st
⊢ (fun x ↦ ⨆ (_ : x ∈ st), f x) i ≤ st.sup f

case neg
ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t st : Finset ι
a : α
x✝ : a ∈ Set.range fun x ↦ ⨆ (_ : x ∈ st), f x
i : ι
ha : (fun x ↦ ⨆ (_ : x ∈ st), f x) i = a
h : i ∉ st
⊢ (fun x ↦ ⨆ (_ : x ∈ st), f x) i ≤ st.sup f
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
⊢ g (f ↑⟨i, h⟩) ≤ ⨆ i, g ↑i

Tactic:
obtain ⟨t, ht⟩ : ∃ t : f '' s, g t = g (f (Subtype.mk i h)) := by
      have : f i ∈ f '' s := Set.mem_image_of_mem _ h
      exact ⟨⟨f i, this⟩, by simp⟩

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⟩)
⊢ g (f ↑⟨i, h⟩) ≤ ⨆ i, g ↑i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg.inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
h✝ : IsEmpty ι
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

pp: case neg.inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
h✝ : Nonempty ι
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
<;>

Goal state after:
case neg.inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
h✝ : IsEmpty ι
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

case neg.inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
h✝ : Nonempty ι
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
hq : q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
hq : ¬q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
hq : q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
hq : ¬q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
hq : q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
hq : ¬q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

case pos
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
hq : q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
hq : ¬q
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
hq : q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
hq : ¬q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
hq : q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
hq : ¬q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
hq : q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
hq : ¬q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
hq : q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
hq : ¬q
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)
Module: Mathlib.Data.Set.Sigma

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

pp: case neg
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∉ s₁
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

case neg
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∉ s₁
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁
Module: Mathlib.Data.Set.Sigma

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
h₂ : x.snd ∈ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

pp: case neg
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
h₂ : x.snd ∉ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

pp: case pos
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∉ s₁
h₂ : x.snd ∈ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

pp: case neg
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∉ s₁
h₂ : x.snd ∉ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
h₂ : x.snd ∈ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

case neg
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
h₂ : x.snd ∉ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

case pos
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∉ s₁
h₂ : x.snd ∈ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

case neg
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∉ s₁
h₂ : x.snd ∉ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h✝ : Nonempty ι
hf : ¬BddAbove (range f)
⊢ e (⨆ i, f i) = ⨆ i, e (f i)

Tactic:
· have hfe : ¬ BddAbove (range fun i ↦ e (f i)) := by
      simpa [Set.Nonempty, BddAbove, upperBounds, e.surjective.forall] using hf
    simp [map_bot, hf, hfe]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
classical
  simp only [CovBy, Pi.lt_def, not_and, and_imp, forall_exists_index, not_exists] at h
  obtain ⟨⟨hab, ⟨i, hi⟩⟩, h⟩ := h
  refine ⟨i, fun j hj ↦ ?_⟩
  let c : (i : ι) → α i := Function.update a i (b i)
  have h₁ : c ≤ b := by simpa [update_le_iff, c] using fun k hk ↦ hab k
  have h₂ : ¬ c j < b j := h (by simp [c, hi.le]) i (by simpa [c]) h₁ j
  exact ⟨hab j, by simpa [lt_iff_le_not_ge, hab j, c, hj] using h₂⟩

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

Goal state before:
pp: α : Type u
β : Type v
f : α ↪ β
s : Finset α
t : Finset β
⊢ map f s ⊆ t ↔ s ⊆ t.preimage ⇑f ⋯

Tactic:
rw [map_eq_image, image_subset_iff_subset_preimage]

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

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) ≠ ∅ ↔ ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅

pp: case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ ∅ ≠ ∅ ↔ ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) ≠ ∅ ↔ ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅

case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ ∅ ≠ ∅ ↔ ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ #(map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd)) = #(f (h ▸ a.snd) b.snd)

pp: case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ #∅ = 0

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ #(map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd)) = #(f (h ▸ a.snd) b.snd)

case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ #∅ = 0
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case zero
α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n ↦ Nat.recOn n ⋯.choose fun x a ↦ ⋯.choose
⊢ f 0 ∈ s

pp: case succ
α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n ↦ Nat.recOn n ⋯.choose fun x a ↦ ⋯.choose
n✝ : ℕ
⊢ f (n✝ + 1) ∈ s

Tactic:
<;>

Goal state after:
case zero
α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n ↦ Nat.recOn n ⋯.choose fun x a ↦ ⋯.choose
⊢ f 0 ∈ s

case succ
α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n ↦ Nat.recOn n ⋯.choose fun x a ↦ ⋯.choose
n✝ : ℕ
⊢ f (n✝ + 1) ∈ s
Module: Mathlib.Order.Minimal

Goal state before:
pp: case inl
α : Type u_2
x : α
inst✝ : Preorder α
h : ∅.Subsingleton
⊢ Minimal (fun x ↦ x ∈ ∅) x ↔ x ∈ ∅

pp: case inr
α : Type u_2
x✝ : α
inst✝ : Preorder α
x : α
h : {x}.Subsingleton
⊢ Minimal (fun x_1 ↦ x_1 ∈ {x}) x✝ ↔ x✝ ∈ {x}

Tactic:
<;>

Goal state after:
case inl
α : Type u_2
x : α
inst✝ : Preorder α
h : ∅.Subsingleton
⊢ Minimal (fun x ↦ x ∈ ∅) x ↔ x ∈ ∅

case inr
α : Type u_2
x✝ : α
inst✝ : Preorder α
x : α
h : {x}.Subsingleton
⊢ Minimal (fun x_1 ↦ x_1 ∈ {x}) x✝ ↔ x✝ ∈ {x}
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b c : ℕ
⊢ Unique ↥(Iic 0)

Tactic:
rw [← Nat.bot_eq_zero]
  infer_instance

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: n : ℕ
⊢ range (n + 1) = Icc 0 n

Tactic:
range_eq_Icc_zero_sub_one _ (Nat.add_one_ne_zero _),

Goal state after:
n : ℕ
⊢ Icc 0 (n + 1 - 1) = Icc 0 n
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: n : ℕ
⊢ range (n + 1) = Icc 0 n

Tactic:
by
  rw [range_eq_Icc_zero_sub_one _ (Nat.add_one_ne_zero _), Nat.add_sub_cancel_right]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b : ℕ
⊢ ↑(max a b + 1) - ↑(min a b) = ↑((↑b - ↑a).natAbs + 1)

pp: a b : ℕ
⊢ min a b ≤ max a b + 1

Tactic:
<;>

Goal state after:
a b : ℕ
⊢ ↑(max a b + 1) - ↑(min a b) = ↑((↑b - ↑a).natAbs + 1)

a b : ℕ
⊢ min a b ≤ max a b + 1
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
⊢ n + a = l

pp: case succ.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
⊢ k = l

Tactic:
<;>

Goal state after:
case succ.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
hkl : (n + a) % a = l % a
hkn : n + a ≠ n
⊢ n + a = l

case succ.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hl : l ≠ n ∧ (l = n + a ∨ l ∈ Ico n (n + a))
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
⊢ k = l
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
⊢ (x ∈
      match ⊤, b with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ x ∧ x ≤ b

pp: case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, b with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝ ≤ x ∧ x ≤ b

Tactic:
<;>

Goal state after:
case top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
⊢ (x ∈
      match ⊤, b with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ x ∧ x ≤ b

case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, b with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝ ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ.inr.inr.refine_1
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k ∈ ↑(Ico n (n + a))

pp: case succ.inr.inr.refine_2
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ l ∈ ↑(Ico n (n + a))

Tactic:
<;>

Goal state after:
case succ.inr.inr.refine_1
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k ∈ ↑(Ico n (n + a))

case succ.inr.inr.refine_2
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ l ∈ ↑(Ico n (n + a))