mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst✝ : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
⊢ (s ×ˢ t).PartiallyWellOrderedOn fun x y ↦ r x.1 y.1 ∧ r' x.2 y.2

Tactic:
by

Goal state after:
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:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ #(Ioi a) = #(Ici a) - 1

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ #(Iio a) = #(Iic a) - 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
f : ι → α
s : Finset ι
⊢ image f s ⊆ Iic (s.sup f)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ico a b ∪ Ico b c = Ico a c

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Ioc a b ∪ Ioc b c = Ioc a c

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝¹ : Fintype ι
this✝ : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
this :
  ∀ (t : Finset ι) (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ (univ.pi s).PartiallyWellOrderedOn fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a c ⊆ Ico a b ∪ Ico b c

Tactic:
by

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

Goal state before:
pp: M : Type u_1
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
a₁ a₂ : α
m : M
h : a₂ ∈ orbit M a₁
⊢ m • a₂ ∈ orbit M a₁

Tactic:
by

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

Goal state before:
pp: M : Type u_1
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : α
⊢ (fun m ↦ m • a) 1 = a

Tactic:
by

Goal state after:
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 : α
⊢ orbit (↥S) a ⊆ orbit M a

Tactic:
by

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

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
a✝ b✝ : α
ha : a✝ ∈ MulAction.fixedPoints M α
hb : b✝ ∈ MulAction.fixedPoints M α
x✝ : M
⊢ x✝ • (a✝ * b✝) = a✝ * b✝

Tactic:
by

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

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
g : M
x : ↥(FixedPoints.submonoid M α)
y : α
⊢ g • x • y = x • g • y

Tactic:
by

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

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Group α
inst✝ : MulDistribMulAction M α
x✝¹ : α
ha : x✝¹ ∈ (submonoid M α).carrier
x✝ : M
⊢ x✝ • x✝¹⁻¹ = x✝¹⁻¹

Tactic:
by

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 α
g : G
a : α
⊢ orbit G a = orbit G (g⁻¹ • g • a)

Tactic:
by

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 α
g : G
a : α
⊢ a ∈ orbit G (g • a)

Tactic:
by

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 α
g h : G
a : α
⊢ g • a ∈ orbit G (h • a)

Tactic:
by

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 α
a₁ a₂ : α
⊢ a₁ ∈ orbit G a₂ ↔ a₂ ∈ orbit G a₁

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Tactic:
by

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 α
H : Subgroup G
x : α
a b : ↑(orbit G x)
⊢ a ∈ orbit (↥H) b ↔ ↑a ∈ orbit ↥H ↑b

Tactic:
by

Goal state after:
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 β
⊢ ∀ {x y z : α}, x ∈ orbit G y → y ∈ orbit G z → x ∈ orbit G z

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Ioc a b ∩ Ioc c d = Ioc (max a c) (min b d)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ {x ∈ Ico a b | x < c} = Ico a (min b c)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ {x ∈ Ico a b | c ≤ x} = Ico (max a c) b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ {x ∈ Ioo a b | x < c} = Ioo a (min b c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
⊢ (univ.pi s).PartiallyWellOrderedOn fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrderBot α
a b : α
⊢ {x ∈ Iio a | x < b} = Iio (min a b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
h : s.IsPWO
⊢ s.IsWF

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b \ Ico a c = Ico (max a c) b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
⊢ (insert a s).IsPWO ↔ s.IsPWO

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b \ Ico c b = Ico a (min b c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
⊢ (insert a s).IsWF ↔ s.IsWF

Tactic:
by

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 α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x ↦ g • x) u = a
⊢ f (g⁻¹ • a) = f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsPWO
ha : a ∈ s
⊢ ∃ b ≤ a, Minimal (fun x ↦ x ∈ s) b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
h : s.IsPWO
hs : s.Nonempty
⊢ ∃ a, Minimal (fun x ↦ x ∈ s) a

Tactic:
by

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 α
U : Set α
⊢ Quotient.mk' ⁻¹' Quotient.mk' '' U = ⋃ g, (fun x ↦ g • x) '' U

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
⊢ Iic b \ Ioc a b = Iic (min a b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Preorder α
f : ι → α
s : Set ι
h : (f '' s).IsPWO
hs : s.Nonempty
⊢ ∃ i, MinimalFor (fun x ↦ x ∈ s) f i

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
hab : a ≤ b
⊢ Iic b \ Ioc a b = Iic a

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
a : α
⊢ (insert a s).WellFoundedOn r ↔ s.WellFoundedOn r

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
a : α
⊢ (s \ {a}).WellFoundedOn r ↔ s.WellFoundedOn r

Tactic:
by

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
h : a ≤ b
⊢ Iic a ∪ Ioc a b = Iic b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_6
β : Type u_7
r : α → α → Prop
f : β → α
s : Set α
t : Set β
h : MapsTo f t s
hw : s.WellFoundedOn r
⊢ t.WellFoundedOn (r on f)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ (Ioi a).disjUnion (Iio a) ⋯ = {a}ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Set α
⊢ s.IsPWO ↔ s.IsWF

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Finset ι
f : ι → Set α
⊢ (∅.sup f).WellFoundedOn r ↔ ∀ i ∈ ∅, (f i).WellFoundedOn r

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ [[a, b]] = Icc a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s✝ : Finset ι
f : ι → Set α
a : ι
s : Finset ι
ha : a ∉ s
hs : (s.sup f).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r
⊢ ((cons a s ha).sup f).WellFoundedOn r ↔ ∀ i ∈ cons a s ha, (f i).WellFoundedOn r

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
r : α → α → Prop
s : Finset ι
f : ι → Set α
⊢ (∅.sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ ∅, (f i).PartiallyWellOrderedOn r

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : b ≤ a
⊢ [[a, b]] = Icc b a

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
r : α → α → Prop
s✝ : Finset ι
f : ι → Set α
a : ι
s : Finset ι
ha : a ∉ s
hs : (s.sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r
⊢ ((cons a s ha).sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ cons a s ha, (f i).PartiallyWellOrderedOn r

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Finset ι
f : ι → Set α
⊢ (⋃ i ∈ s, f i).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r

Tactic:
by

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 α
U V : Set α
⊢ Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
r : α → α → Prop
s : Finset ι
f : ι → Set α
⊢ (⋃ i ∈ s, f i).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ [[a, b]] = [[b, a]]

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsWF
ha : a ∈ s
hlt : ∀ b ∈ s, b ≠ a → a < b
⊢ hs.min ⋯ = a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a : α
⊢ [[a, a]] = {a}

Tactic:
by

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 α
a : α
x : Quotient G α
⊢ a ∈ x.orbit ↔ Quotient.mk'' a = x

Tactic:
by

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 : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
⊢ x.orbit = MulAction.orbit G (φ x)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ ∈ [[a₂, b₂]]
h₂ : b₁ ∈ [[a₂, b₂]]
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
⊢ ⋯.min ⋯ = Min.min (hs.min hsn) (ht.min htn)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
ha : a₁ ∈ Icc a₂ b₂
hb : b₁ ∈ Icc a₂ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂

Tactic:
by

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 α
⊢ Injective orbit

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
s : Set α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ BddBelow s → s.WellFoundedOn fun x1 x2 ↦ x1 < x2

Tactic:
by

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 α
H : Subgroup G
a b : α
h : ⟦a⟧ = ⟦b⟧
⊢ ⟦a⟧ = ⟦b⟧

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a ∈ [[b, c]] → b ∈ [[a, c]] → a = b

Tactic:
by

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 : Quotient G α
⊢ x.orbit.Nonempty

Tactic:
by

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 α
g : G
x : Quotient G α
⊢ Set.MapsTo (fun x ↦ g • x) x.orbit x.orbit

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
h : (fun b ↦ [[b, a]]) b = (fun b ↦ [[b, a]]) c
⊢ b = c

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ ↑[[a, b]] = ↑(Icc a b ∪ Icc b a)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ c < a → c < b → c ∉ [[a, b]]

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
⊢ BddAbove (f ⁻¹' s)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a < c → b < c → c ∉ [[a, b]]

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑[[a, c]] ⊆ ↑([[a, b]] ∪ [[b, c]])

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
⊢ ∃ k, ∀ (m : ℕ), k < m → f m ∉ s

Tactic:
by

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 α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
⊢ ↑a ∈ MulAction.orbit ↥H ↑b ↔ a ∈ MulAction.orbit (↥H) b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
f : ℕ → α
⊢ ((∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)) ↔ ¬IsBadSeq r s f

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
⊢ s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), ¬IsBadSeq r s f

Tactic:
by

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 α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
⊢ ⟦a⟧ = ⟦b⟧ ↔ ⟦↑a⟧ = ⟦↑b⟧

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ k g, (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 : ∀ m < n, f m = Classical.choose ⋯ m
h2 : IsBadSeq r s (Classical.choose ⋯)
h3 : rk (Classical.choose ⋯ n) = Nat.find h
⊢ IsBadSeq r s (Classical.choose ⋯)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
⊢ x ≤ y ↔ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
x y : α
⊢ x ≤ y ↔ ReflTransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
⊢ { g // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }

Tactic:
by

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 α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ orbit ⟦a⟧
⊢ ↑b ∈ MulAction.orbit ↥H ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
⊢ (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
⊢ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
⊢ x < y ↔ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
by

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 α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
⊢ ↑a ∈ MulAction.orbit (↥H) c ↔ ↑b ∈ MulAction.orbit (↥H) c

Tactic:
by

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

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

Tactic:
by

Goal state after: