mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
⊢ (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
a✝ : WithTop (WithBot α)
⊢ (f.comp g).withTopWithBot a✝ = (f.withTopWithBot.comp g.withTopWithBot) a✝
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ range some = Iio ⊤

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : Preorder α
x✝ : WithTop α
⊢ x✝ ∈ range some ↔ x✝ ∈ Iio ⊤
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

Tactic:
by_cases hp : p

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.CompleteLattice.Finset

Goal state before:
pp: ι : Type u_5
s : Set ι
⊢ ⋃ s', Subtype.val '' ↑s' = s

Tactic:
ext x
  simp only [Set.mem_iUnion, Set.mem_image, SetLike.mem_coe, Subtype.exists,
    exists_and_right, exists_eq_right]
  exact ⟨fun ⟨_, hx, _⟩ ↦ hx, fun hx ↦ ⟨{⟨x, hx⟩}, hx, by simp⟩⟩

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

Tactic:
by
  rcases le_or_gt (sSup ∅) (iSup f) with le | gt
  · rw [max_eq_left le]
    by_cases bdd : BddAbove (range f)
    · rw [← ciSup_subtype bdd le]
    · rw [ciSup_of_not_bddAbove bdd, cbiSup_of_not_bddAbove bdd]
  have ⟨i, hi⟩ := not_forall.mp hp
  have : Nonempty ι := ⟨i⟩
  have bdd : BddAbove (range f) := not_not.mp fun h ↦ gt.ne (ciSup_of_not_bddAbove h)
  rw [max_eq_right gt.le]
  refine ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j ↦ ?_) ?_
  · by_cases hj : p j
    · exact ((ciSup_pos hj).trans_le (le_ciSup bdd ⟨j, hj⟩)).trans gt.le
    · exact (ciSup_neg hj).le
  · exact fun w hw ↦ ⟨i, hw.trans_eq (ciSup_neg hi).symm⟩

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
this : OrderBot α
⊢ ⨅ i, f i = n ↔ (∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
this : OrderBot α
⊢ ⨅ i, f i = n → (∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i

case mpr
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
this : OrderBot α
⊢ ((∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i) → ⨅ i, f i = n
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

Tactic:
by_cases hp : p

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.Cover

Goal state before:
pp: case e'_4
α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ s = insert a (s \ {a})

Tactic:
ext

Goal state after:
case e'_4
α : Type u_1
s : Set α
a : α
ha : a ∈ s
x✝ : α
⊢ x✝ ∈ s ↔ x✝ ∈ insert a (s \ {a})
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
⊢ (a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂

Tactic:
by
  refine ⟨WCovBy.fst, (And.imp mk_le_mk_iff_left.2) fun h c h₁ h₂ => ?_⟩
  have : c.2 = b := h₂.le.2.antisymm h₁.le.2
  rw [← @Prod.mk.eta _ _ c, this, mk_lt_mk_iff_left] at h₁ h₂
  exact h h₁ h₂

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
inst✝ : Nonempty ι
⊢ a ⩿ b ↔ ∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
constructor

Goal state after:
case mp
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
⊢ a ⩿ b → ∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
⊢ (∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)) → a ⩿ b
Module: Mathlib.Order.Cover

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

Tactic:
constructor

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

case mpr
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)) → a ⋖ b
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔ ∃ i x, a i ⩿ x ∧ b = Function.update a i x

Tactic:
constructor

Goal state after:
case mp
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) → ∃ i x, a i ⩿ x ∧ b = Function.update a i x

case mpr
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i x, a i ⩿ x ∧ b = Function.update a i x) → ∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔ ∃ i x, a i ⋖ x ∧ b = Function.update a i x

Tactic:
constructor

Goal state after:
case mp
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) → ∃ i x, a i ⋖ x ∧ b = Function.update a i x

case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i x, a i ⋖ x ∧ b = Function.update a i x) → ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔ ∃ i x, x ⩿ b i ∧ a = Function.update b i x

Tactic:
constructor

Goal state after:
case mp
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) → ∃ i x, x ⩿ b i ∧ a = Function.update b i x

case mpr
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i x, x ⩿ b i ∧ a = Function.update b i x) → ∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨i, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨i, b⟩.snd)

Tactic:
constructor

Goal state after:
case inl.mp
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ →
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨i, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨i, b⟩.snd)

case inl.mpr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ (∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨i, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨i, b⟩.snd)) →
    x ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔ ∃ i x, x ⋖ b i ∧ a = Function.update b i x

Tactic:
constructor

Goal state after:
case mp
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) → ∃ i x, x ⋖ b i ∧ a = Function.update b i x

case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i x, x ⋖ b i ∧ a = Function.update b i x) → ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot Pbot
⊢ (t.preimage Subtype.val ⋯).sup id = ⟨t.sup id, ⋯⟩

Tactic:
ext

Goal state after:
α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := ⋯
⊢ ↑((t.preimage Subtype.val ⋯).sup id) = ↑⟨t.sup id, ⋯⟩
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hca : c ≤ a
⊢ filter (fun x ↦ x < c) (Ico a b) = ∅

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_left hca]
  rfl

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Tactic:
constructor

Goal state after:
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 → k + 1 ∈ s ∧ k ∉ s

case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ k + 1 ∈ s ∧ k ∉ s → sInf s = k + 1
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : LocallyFiniteOrderTop α
inst✝² : One α
inst✝¹ : IsBotOneClass α
inst✝ : Fintype α
⊢ Ici 1 = univ

Tactic:
ext

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : LocallyFiniteOrderTop α
inst✝² : One α
inst✝¹ : IsBotOneClass α
inst✝ : Fintype α
a✝ : α
⊢ a✝ ∈ Ici 1 ↔ a✝ ∈ univ
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ k + 1 ∈ s ∧ k ∉ s → sInf s = k + 1

Tactic:
rintro ⟨H, H'⟩
    rw [sInf_def (⟨_, H⟩ : s.Nonempty), find_eq_iff]
    exact ⟨H, fun n hnk hns ↦ H' <| hs n k (Nat.lt_succ_iff.mp hnk) hns⟩

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

Goal state before:
pp: case inr
n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ i < a

Tactic:
constructor

Goal state after:
case inr.mp
n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → i < a

case inr.mpr
n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ i < a → ∃ a_2, (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
⊢ ∃ a, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
choose next hnext using exists_covBy_of_wellFoundedLT (α := α)

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
⊢ ∃ a, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b x : ℕ
⊢ (∃ a_1 < b, a + a_1 = x) ↔ a ≤ x ∧ x < a + b

Tactic:
constructor

Goal state after:
case mp
a b x : ℕ
⊢ (∃ a_1 < b, a + a_1 = x) → a ≤ x ∧ x < a + b

case mpr
a b x : ℕ
⊢ a ≤ x ∧ x < a + b → ∃ a_2 < b, a + a_2 = x
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
⊢ WellQuasiOrdered r ↔ ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
⊢ WellQuasiOrdered r → ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
⊢ (∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))) → WellQuasiOrdered r
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case pos
α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : (s ∩ t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
rw [← Subtype.preimage_coe_nonempty] at hst
    rcases h.has_min (Subtype.val ⁻¹' t) hst with ⟨⟨m, ms⟩, mt, hm⟩
    exact ⟨m, mt, fun x xt ⟨xm, xs, _⟩ => hm ⟨x, xs⟩ xt xm⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ Nonempty ((fun x1 x2 ↦ x1 > x2) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s) ↔ ∃ x, ∀ (n : ℕ), x n ∈ s

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ Nonempty ((fun x1 x2 ↦ x1 > x2) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s) → ∃ x, ∀ (n : ℕ), x n ∈ s

case mpr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ (∃ x, ∀ (n : ℕ), x n ∈ s) → Nonempty ((fun x1 x2 ↦ x1 > x2) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a < j ∧ j < b
⊢ {j | a < j ∧ j < b} = Ioo a b

Tactic:
ext

Goal state after:
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a < j ∧ j < b
a✝ : α
⊢ a✝ ∈ {j | a < j ∧ j < b} ↔ a✝ ∈ Ioo a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a < j ∧ j ≤ b
⊢ {j | a < j ∧ j ≤ b} = Ioc a b

Tactic:
ext

Goal state after:
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a < j ∧ j ≤ b
a✝ : α
⊢ a✝ ∈ {j | a < j ∧ j ≤ b} ↔ a✝ ∈ Ioc a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a ≤ j ∧ j < b
⊢ {j | a ≤ j ∧ j < b} = Ico a b

Tactic:
ext

Goal state after:
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a ≤ j ∧ j < b
a✝ : α
⊢ a✝ ∈ {j | a ≤ j ∧ j < b} ↔ a✝ ∈ Ico a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a ≤ j ∧ j ≤ b
⊢ {j | a ≤ j ∧ j ≤ b} = Icc a b

Tactic:
ext

Goal state after:
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a ≤ j ∧ j ≤ b
a✝ : α
⊢ a✝ ∈ {j | a ≤ j ∧ j ≤ b} ↔ a✝ ∈ Icc a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ a < x
⊢ {x | a < x} = Ioi a

Tactic:
ext

Goal state after:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ a < x
a✝ : α
⊢ a✝ ∈ {x | a < x} ↔ a✝ ∈ Ioi a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ a ≤ x
⊢ {x | a ≤ x} = Ici a

Tactic:
ext

Goal state after:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ a ≤ x
a✝ : α
⊢ a✝ ∈ {x | a ≤ x} ↔ a✝ ∈ Ici a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ x < a
⊢ {x | x < a} = Iio a

Tactic:
ext

Goal state after:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ x < a
a✝ : α
⊢ a✝ ∈ {x | x < a} ↔ a✝ ∈ Iio a
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ioo ↑a ↑b
⊢ p x

Tactic:
rw [mem_Ioo] at hx

Goal state after:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a < x ∧ x < ↑b
⊢ p x
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ x ≤ a
⊢ {x | x ≤ a} = Iic a

Tactic:
ext

Goal state after:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ x ≤ a
a✝ : α
⊢ a✝ ∈ {x | x ≤ a} ↔ a✝ ∈ Iic a
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Ici a) = Ici ↑a

Tactic:
subtype_Ici_eq

Goal state after:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ici ↑a)) = Ici ↑a
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Ici a) = Ici ↑a

Tactic:
rw [subtype_Ici_eq]

Goal state after:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ici ↑a)) = Ici ↑a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Set.Ico a b ∪ {b} = Set.Icc a b

Tactic:
Set.Ico_union_right h

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Set.Icc a b = Set.Icc a b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Icc a b)
⊢ (Icc a b).toFinset = Finset.Icc a b

Tactic:
ext

Goal state after:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Icc a b)
a✝ : α
⊢ a✝ ∈ (Icc a b).toFinset ↔ a✝ ∈ Finset.Icc a b
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ x : N
hx : x ∈ s
⊢ (fun x ↦ r • x) x = r ^ 1 • x

Tactic:
rw [pow_one]

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

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ico a b)
⊢ (Ico a b).toFinset = Finset.Ico a b

Tactic:
ext

Goal state after:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ico a b)
a✝ : α
⊢ a✝ ∈ (Ico a b).toFinset ↔ a✝ ∈ Finset.Ico a b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ioo a b)
⊢ (Ioo a b).toFinset = Finset.Ioo a b

Tactic:
ext

Goal state after:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ioo a b)
a✝ : α
⊢ a✝ ∈ (Ioo a b).toFinset ↔ a✝ ∈ Finset.Ioo a b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Ici a)
⊢ (Ici a).toFinset = Finset.Ici a

Tactic:
ext

Goal state after:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Ici a)
a✝ : α
⊢ a✝ ∈ (Ici a).toFinset ↔ a✝ ∈ Finset.Ici a
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Ioi a)
⊢ (Ioi a).toFinset = Finset.Ioi a

Tactic:
ext

Goal state after:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Ioi a)
a✝ : α
⊢ a✝ ∈ (Ioi a).toFinset ↔ a✝ ∈ Finset.Ioi a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a : α
⊢ (Ici a).erase a = Ioi a

Tactic:
ext

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ (Ici a).erase a ↔ a✝ ∈ Ioi a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a : α
⊢ insert a (Ioi a) = Ici a

Tactic:
ext

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ insert a (Ioi a) ↔ a✝ ∈ Ici a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b : α
⊢ (Iic b).erase b = Iio b

Tactic:
ext

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ (Iic b).erase b ↔ a✝ ∈ Iio b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b : α
⊢ insert b (Iio b) = Iic b

Tactic:
ext

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ insert b (Iio b) ↔ a✝ ∈ Iic b
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: M : Type u_1
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
S : Submonoid M
a : α
g : ↥S
⊢ (fun m ↦ m • a) g ∈ orbit M a

Tactic:
exact mem_orbit _ _

Goal state after: