mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
a : α
f : ι → α
h : BddAbove (range f)
⊢ a < iSup f ↔ ∃ i, a < f i

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
a : α
f : ι → α
h : BddAbove (range f)
⊢ a < iSup f ↔ ∃ i, a < f i
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
x : α
s : Set α
⊢ s ⩿ insert x s

Tactic:
by
  refine wcovBy_of_eq_or_eq (subset_insert x s) fun t hst h2t => ?_
  by_cases h : x ∈ t
  · exact Or.inr (subset_antisymm h2t <| insert_subset_iff.mpr ⟨h, hst⟩)
  · refine Or.inl (subset_antisymm ?_ hst)
    rwa [← sdiff_singleton_eq_self h, sdiff_singleton_subset_iff]

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

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

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h✝ : Nonempty ι
hf : ¬BddAbove (range f)
⊢ ∀ (x : α), ∃ x_1, x < f x_1
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 : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
⊢ Function.update a i ci ≤ b

Tactic:
simpa using

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
⊢ ∀ (j : ι), ¬j = i → a j ≤ b j
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
i : ι
hi : a.untop ⋯ < f i
⊢ a < ↑(f i)

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
i : ι
hi : a.untop ⋯ < f i
⊢ a < ↑(f i)
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update a i (b i)
⊢ c ≤ b

Tactic:
simpa using

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update 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 : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update a i (b i)
h₁ : c ≤ b
h₂ : ¬c j < b j
⊢ (fun x1 x2 ↦ x1 ≤ x2) (b j) (a j)

Tactic:
simpa using

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update a i (b i)
h₁ : c ≤ b
h₂ : ¬c j < b j
⊢ b j ≤ a 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 : ι
hi : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ b = Function.update a i (b i)

Tactic:
simpa using

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
hi : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ ∀ (x : ι), ¬i = x → a x = b x
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 : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ b = Function.update a i (b i)

Tactic:
simpa using

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ ∀ (x : ι), ¬i = x → a x = b x
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ (↑s).PairwiseDisjoint fun i ↦ map (Embedding.sigmaMk i) (t i)

Tactic:
intro i _ j _ hij
  rw [Function.onFun, disjoint_left]
  simp_rw [mem_map, Function.Embedding.sigmaMk_apply]
  rintro _ ⟨y, _, rfl⟩ ⟨z, _, hz'⟩
  exact hij (congr_arg Sigma.fst hz'.symm)

Goal state after:
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 : ι
hi : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ a = Function.update b i (a i)

Tactic:
simpa using

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
hi : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ ∀ (x : ι), ¬i = x → a x = b x
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 : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ a = Function.update b i (a i)

Tactic:
simpa using

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ ∀ (x : ι), ¬i = x → a x = b x
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
hf : BijOn f (f ⁻¹' ↑s) ↑s
⊢ ↑(image f (s.preimage f ⋯)) = ↑s

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
hf : BijOn f (f ⁻¹' ↑s) ↑s
⊢ f '' f ⁻¹' ↑s = ↑s
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
x : α
hx : x ∈ ↑t
⊢ x ∈ Subtype.val '' Subtype.val ⁻¹' ↑t

Tactic:
simpa using

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) := Subtype.orderBot Pbot
x : α
hx : x ∈ ↑t
⊢ x ∈ t ∧ P x
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun x ↦ x ∈ s) f j
hji : ¬f j ≤ f i
⊢ ∀ ⦃j_1 : ι⦄, (fun x ↦ x ∈ cons i s hi) j_1 → f j ≤ f j_1 → f j_1 ≤ f j

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun x ↦ x ∈ s) f j
hji : ¬f j ≤ f i
⊢ ∀ a ∈ s, f j ≤ f a → f a ≤ f j
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a : α
s : Finset α
ha : a ∈ s
⊢ ∃ b ∈ s, a ≤ b ∧ ?m.24 b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Preorder α
a : α
s : Finset α
ha : a ∈ s
⊢ ∃ b ∈ s, a ≤ b ∧ ?m.24 b
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s : Set ι
h : s.Finite
hs : s.Nonempty
⊢ ∃ i, MaximalFor (fun x ↦ x ∈ s) f i

Tactic:
by
  lift s to Finset ι using h; exact s.exists_maximalFor f hs

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → t ⊆ s → P s
hs : P s
h : ¬Minimal P s
⊢ ∃ x, x ∈ s ∧ P (s \ {x})

Tactic:
simpa using

Goal state after:
α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → t ⊆ s → P s
hs : P s
h : ¬Minimal P s
⊢ ∃ x, x ∈ s ∧ P (s \ {x})
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
hs : P s
h : ¬Maximal P s
⊢ ∃ x, ¬x ∈ s ∧ P (insert x s)

Tactic:
simpa using

Goal state after:
α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
hs : P s
h : ¬Maximal P s
⊢ ∃ x, ¬x ∈ s ∧ P (insert x s)
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
inst✝¹ : LinearOrder α
inst✝ : Finite α
f : α →o α
hf : Function.Injective ⇑f
⊢ Set.range ⇑f = Set.range ⇑id

Tactic:
simpa using

Goal state after:
α : Type u_4
inst✝¹ : LinearOrder α
inst✝ : Finite α
f : α →o α
hf : Function.Injective ⇑f
⊢ Function.Surjective ⇑f
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ x ≤ a
hab : a < b
⊢ filter (fun x ↦ x ≤ a) (Ico a b) = {a}

Tactic:
by
  rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_left hab]
  rfl

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

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

Tactic:
simpa using

Goal state after:
case succ.inl.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : n % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ 0 < a
Module: Mathlib.Order.Interval.Finset.Nat

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

Tactic:
simpa using

Goal state after:
case succ.inr.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
⊢ 0 < a
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr.inl.refine_1
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a ≤ i + a

Tactic:
simpa using

Goal state after:
case inr.mpr.inl.refine_1
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a ≤ i + a
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
⊢ Finite α

Tactic:
apply Finite.of_not_infinite

Goal state after:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
⊢ ¬Infinite α
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr.inr
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
    · lia
    · lia
    · rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂

Tactic:
simpa using

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂

Tactic:
simpa using

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Set.Ico a₁ b₁ ⊆ Set.Ico a₂ b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂

Tactic:
simpa using

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Set.Ioc a₁ b₁ ⊆ Set.Ioc a₂ b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ioo a₁ b₁ ⊆ Ioo a₂ b₂

Tactic:
simpa using

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Set.Ioo a₁ b₁ ⊆ Set.Ioo a₂ b₂
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 : (Subtype.val ⁻¹' t).Nonempty
m : α
ms : m ∈ s
mt : ⟨m, ms⟩ ∈ Subtype.val ⁻¹' t
hm : ∀ x ∈ Subtype.val ⁻¹' t, ¬Subrel r (fun x ↦ x ∈ s) x ⟨m, ms⟩
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
exact ⟨m, mt, fun x xt ⟨xm, xs, _⟩ => hm ⟨x, xs⟩ xt xm⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
h : WellQuasiOrdered r
f : r →r s
hf : Function.Surjective ⇑f
seq : ℕ → β
w✝¹ w✝ : ℕ
hle : w✝¹ < w✝
hr : r ((Function.surjInv hf ∘ seq) w✝¹) ((Function.surjInv hf ∘ seq) w✝)
⊢ s (seq w✝¹) (seq w✝)

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
h : WellQuasiOrdered r
f : r →r s
hf : Function.Surjective ⇑f
seq : ℕ → β
w✝¹ w✝ : ℕ
hle : w✝¹ < w✝
hr : r ((Function.surjInv hf ∘ seq) w✝¹) ((Function.surjInv hf ∘ seq) w✝)
⊢ s (seq w✝¹) (seq w✝)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : LE α
inst✝ : LE β
f : α ≃o β
⊢ WellQuasiOrderedLE α ↔ WellQuasiOrderedLE β

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : LE α
inst✝ : LE β
f : α ≃o β
⊢ (WellQuasiOrdered fun x1 x2 ↦ x1 ≤ x2) ↔ WellQuasiOrdered fun x1 x2 ↦ x1 ≤ x2
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mp
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
H : ∀ (n : ℕ), f n ∈ s
⊢ ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b

Tactic:
simpa using

Goal state after:
case mp
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b
H : ∀ (n : ℕ), f n ∈ s
⊢ ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mpr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b
hfs : ∀ (n : ℕ), f n ∈ s
⊢ ∀ {a b : ℕ}, r (f a) (f b) ∧ f a ∈ s ∧ f b ∈ s ↔ a > b

Tactic:
simpa using

Goal state after:
case mpr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b
hfs : ∀ (n : ℕ), f n ∈ s
⊢ ∀ {a b : ℕ}, r (f a) (f b) ↔ a > b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
h : a ≤ b
⊢ Ioi b ⊆ Ioi a

Tactic:
simpa using

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
h : a ≤ b
⊢ Set.Ioi b ⊆ Set.Ioi a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
h : a < b
⊢ Ioi b ⊂ Ioi a

Tactic:
simpa using

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
h : a < b
⊢ Set.Ioi b ⊂ Set.Ioi a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Icc a b ⊆ Ici a

Tactic:
simpa using

Goal state after:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Set.Icc a b ⊆ Set.Ici a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b ⊆ Ici a

Tactic:
simpa using

Goal state after:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ico a b ⊆ Set.Ici a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Ioi a

Tactic:
simpa using

Goal state after:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioc a b ⊆ Set.Ioi a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ioi a

Tactic:
simpa using

Goal state after:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ Set.Ioi a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h : a ≤ b
⊢ Iio a ⊆ Iio b

Tactic:
simpa using

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h : a ≤ b
⊢ Set.Iio a ⊆ Set.Iio b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h : a < b
⊢ Iio a ⊂ Iio b

Tactic:
simpa using

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h : a < b
⊢ Set.Iio a ⊂ Set.Iio b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
β : Type u_3
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : α → β
hf : Monotone f
x✝ : α
h : x✝ ∈ Iic a
⊢ x✝ ≤ a

Tactic:
simpa using

Goal state after:
α : Type u_2
a : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
β : Type u_3
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : α → β
hf : Monotone f
x✝ : α
h : x✝ ∈ Iic a
⊢ x✝ ≤ a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Icc a b ⊆ Iic b

Tactic:
simpa using

Goal state after:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Set.Icc a b ⊆ Set.Iic b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Iic b

Tactic:
simpa using

Goal state after:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioc a b ⊆ Set.Iic b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b ⊆ Iio b

Tactic:
simpa using

Goal state after:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ico a b ⊆ Set.Iio b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b ⊆ Iio b

Tactic:
by
  simpa [← coe_subset] using Set.Ico_subset_Iio_self

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Iio b

Tactic:
simpa using

Goal state after:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ Set.Iio b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ioi a ⊆ Ici a

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Set.Ioi a ⊆ Set.Ici a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ Iio a ⊆ Iic a

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ Set.Iio a ⊆ Set.Iic a
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : Preorder α
p : α → Prop
inst✝⁵ : DecidablePred p
y : α
F : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : Preorder M
inst✝³ : Preorder N
inst✝² : EquivLike F M N
inst✝¹ : OrderIsoClass F M N
f : F
inst✝ : LocallyFiniteOrder N
⊢ ∀ (a b x : M), x ∈ map { toFun := EquivLike.inv f, inj' := ⋯ } (finsetIoc (f a) (f b)) ↔ a < x ∧ x ≤ b

Tactic:
by
    simp [finset_mem_Ioc, EquivLike.inv_apply_eq, map_lt_map_iff]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x y : Quotient G α
h : (orbitRel G α) (Quotient.out x) (Quotient.out y)
⊢ x = y

Tactic:
simpa using

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x y : Quotient G α
h : (orbitRel G α) (Quotient.out x) (Quotient.out y)
⊢ x = y
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Injective (uIcc a)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Injective (uIcc a)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⩿ b → f a ≤ f b
a b : α
hab : a ≤ b
⊢ f a ≤ f b

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⩿ b → f a ≤ f b
a b : α
hab : a ≤ b
⊢ f a ≤ f b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a ≤ f b
a b : α
hab : a ≤ b
⊢ f a ≤ f b

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a ≤ f b
a b : α
hab : a ≤ b
⊢ f a ≤ f b
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a✝ : α
b : β
h : Injective fun x ↦ x • b
a : G
ha : a ∈ stabilizer G (a✝ • b)
⊢ a ∈ stabilizer G a✝

Tactic:
simpa using

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a✝ : α
b : β
h : Injective fun x ↦ x • b
a : G
ha : a ∈ stabilizer G (a✝ • b)
⊢ a • a✝ = a✝