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

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

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

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:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
a✝ a₁ a₂ b✝ b₁ b₂ c x : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
a : α
b : ↑(Set.Iic a)
⊢ ↑b ∈ Iic a

Tactic:
by

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

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

Tactic:
by

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

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

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

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

Tactic:
by

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

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

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

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : BoundedOrder α
inst✝ : Fintype α
⊢ Icc ⊥ ⊤ = univ

Tactic:
by

Goal state after:
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
⊢ map (Embedding.subtype p) (Ioo a b) = Ioo ↑a ↑b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Icc a a = {a}

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Icc a b = {c} ↔ a = c ∧ b = c

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x : α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : OrderBot α
⊢ Unique ↥(Iic ⊥)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Icc a b).erase a = Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
⊢ (s ∪ t).PartiallyWellOrderedOn r

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Icc a b).erase b = Ico a b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Ico a b).erase a = Ioo a b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Ioc a b).erase b = Ioo a b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ Icc a b \ {a, b} = Ioo a b

Tactic:
by

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

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert b (Ico a b) = Icc a b

Tactic:
rw [← coe_inj, coe_insert, coe_Icc, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ico_union_right h]

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert b (Ico a b) = Icc a b

Tactic:
by

Goal state after:
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) (Ioi a) = Ioi ↑a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert a (Ioc a b) = Icc a b

Tactic:
by

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

Goal state before:
pp: α : Type u_3
s : Set α
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
⊢ s.Finite ↔ BddBelow s ∧ BddAbove s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : DecidableLE α
inst✝ : LocallyFiniteOrder α
a : { x // x ≤ y }
⊢ y ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : s.PartiallyWellOrderedOn r
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
⊢ (f '' s).PartiallyWellOrderedOn r'

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert a (Ioo a b) = Ico a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
⊢ s.Finite

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : DecidableLE α
inst✝ : LocallyFiniteOrder α
a b : { x // x ≤ y }
⊢ b ∈ Icc a ⟨y, ⋯⟩ ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : DecidableLE α
inst✝ : LocallyFiniteOrder α
a b : { x // x ≤ y }
⊢ b ∈ Ioc a ⟨y, ⋯⟩ ↔ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ WellQuasiOrderedLE α ↔ WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ WellQuasiOrderedLE α ↔ WellFoundedLT α

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert b (Ioo a b) = Ioc a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : DecidableLT α
inst✝ : LocallyFiniteOrder α
a b : { x // x < y }
⊢ b ∈ Finset.subtype (fun x ↦ x < y) (Ico (↑a) y) ↔ a ≤ b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : DecidableLT α
inst✝ : LocallyFiniteOrder α
a b : { x // x < y }
⊢ b ∈ Finset.subtype (fun x ↦ x < y) (Ioo (↑a) y) ↔ a < b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
y : α
inst✝ : LocallyFiniteOrderBot α
⊢ Finite { x // x ≤ y }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
S : Type u_6
inst✝² : Monoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
H : S
⊢ ↑H * ↑H = ↑H

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
S : Type u_6
inst✝² : Monoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
x✝ : 1 ≠ 0
H : S
⊢ ↑H ^ 1 = ↑H

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
S : Type u_6
inst✝² : Monoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
n : ℕ
x✝ : n + 2 ≠ 0
H : S
⊢ ↑H ^ (n + 2) = ↑H

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : Set M
S : Submonoid M
n : ℕ
hs : s ⊆ ↑S
⊢ s ^ n ⊆ ↑S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : Submonoid M
⊢ ↑s * ↑s = ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : Set M
n : ℕ
⊢ closure (s ^ n) ≤ closure s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : Set M
m n : ℕ
hmn : m ∣ n
⊢ closure (s ^ n) ≤ closure (s ^ m)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : Set M
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ closure s ≤ closure (s ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
H K : Submonoid M
⊢ closure ↑H ⊔ closure ↑K ≤ H ⊔ K

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
y : α
inst✝ : LocallyFiniteOrderBot α
⊢ Finite { x // x < y }

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Icc a b \ Ioo a b = {a, b}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: N : Type u_7
inst✝ : CommMonoid N
H K : Submonoid N
⊢ ↑(H ⊔ K) = ↑H * ↑K

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ Ico a b \ Ioo a b = {a}

Tactic:
by

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

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

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ Ioc a b \ Ioo a b = {b}

Tactic:
by

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:
by

Goal state after:
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 : N
⊢ r ^ 0 • 1 ∈ closure (r • s)

Tactic:
by

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

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons b (Ico a b) ⋯

Tactic:
by

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

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons a (Ioc a b) ⋯

Tactic:
by

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

Goal state after:
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' := ⋯ } (finsetIcc (f a) (f b)) ↔ a ≤ x ∧ x ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ioc a b = cons b (Ioo a b) ⋯

Tactic:
by

Goal state after:
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' := ⋯ } (finsetIco (f a) (f b)) ↔ a ≤ x ∧ x < b

Tactic:
by

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

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ico a b = cons a (Ioo a b) ⋯

Tactic:
by

Goal state after:
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' := ⋯ } (finsetIoo (f a) (f b)) ↔ a < x ∧ x < b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ x ≤ a
hab : a < b
⊢ {x ∈ Ico a b | x ≤ a} = {a}

Tactic:
by

Goal state after:
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 : N
hx : x ∈ closure s
⊢ ∃ n, r ^ n • x ∈ closure (r • s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
a✝ b✝ : G
ha : a✝ ∈ (↑S)⁻¹
hb : b✝ ∈ (↑S)⁻¹
⊢ a✝ * b✝ ∈ (↑S)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
⊢ 1⁻¹ ∈ ↑S

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ #(Ico a b) = #(Icc a b) - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ = (closure s)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
x : G
⊢ x ∈ closure s⁻¹ ↔ x⁻¹ ∈ closure s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝³ : Monoid M
inst✝² : AddMonoid A
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α M
S : Submonoid M
⊢ 1 • S = S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
⊢ (↑(Submonoid.closure s)).IsPWO

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ #(Ioo a b) = #(Ico a b) - 1

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ #(Ioo a b) = #(Icc a b) - 2

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) [[a, b]] = [[(a, c), (b, 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✝³ : PartialOrder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) (Icc a b) = Icc (a, c) (b, c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
⊢ s.PartiallyWellOrderedOn r ↔ ∀ t ⊆ s, IsAntichain r t → t.Finite

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : Preorder α
inst✝³ : PartialOrder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) (Ioc a b) = Ioc (a, c) (b, 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✝³ : PartialOrder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) (Ico a b) = Ico (a, c) (b, 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✝³ : PartialOrder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) (Ioo a b) = Ioo (a, c) (b, c)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) [[a, b]] = [[(c, a), (c, b)]]

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) (Icc a b) = Icc (c, a) (c, b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
⊢ s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) (Ioc a b) = Ioc (c, a) (c, b)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) (Ico a b) = Ico (c, a) (c, b)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) (Ioo a b) = Ioo (c, a) (c, b)

Tactic:
by

Goal state after: