mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Finset.Defs

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

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
obtain ⟨m, n, hlt, hle⟩ := h (f ∘ g)
    cases h2 m n hlt hle

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝² a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝², ↑a✝¹ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝² < ↑a✝ ∧ ↑a✝ ≤ ↑a✝¹

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case top.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < ↑a✝ ∧ ↑a✝ < ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
⊢ ∀ {a b : { x // x ∈ s }},
    r ({ toFun := Subtype.val, inj' := ⋯ } a) ({ toFun := Subtype.val, inj' := ⋯ } b) ∧
        { toFun := Subtype.val, inj' := ⋯ } a ∈ s ∧ { toFun := Subtype.val, inj' := ⋯ } b ∈ s ↔
      Subrel r (fun x ↦ x ∈ s) a b

Tactic:
simp

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

Goal state before:
pp: case top.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < ⊤ ∧ ⊤ < ↑a✝

Tactic:
simp

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

Goal state before:
pp: case top.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ⊤, ↑a✝¹ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < ↑a✝ ∧ ↑a✝ < ↑a✝¹

Tactic:
simp

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

Goal state before:
pp: case coe.top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ : α
⊢ (⊤ ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝ < ⊤ ∧ ⊤ < ⊤

Tactic:
simp

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

Goal state before:
pp: case coe.top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝¹, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝¹ < ↑a✝ ∧ ↑a✝ < ⊤

Tactic:
simp

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

Goal state before:
pp: case coe.coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝¹ a✝ : α
⊢ (⊤ ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝¹ < ⊤ ∧ ⊤ < ↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝² a✝¹ a✝ : α
⊢ (↑a✝ ∈
      match ↑a✝², ↑a✝¹ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝² < ↑a✝ ∧ ↑a✝ < ↑a✝¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α), x ∈ map f.symm.toEmbedding (Icc (f a) (f b)) ↔ a ≤ x ∧ x ≤ b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α), x ∈ map f.symm.toEmbedding (Ico (f a) (f b)) ↔ a ≤ x ∧ x < b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α), x ∈ map f.symm.toEmbedding (Ioc (f a) (f b)) ↔ a < x ∧ x ≤ b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α), x ∈ map f.symm.toEmbedding (Ioo (f a) (f b)) ↔ a < x ∧ x < b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrderTop β
f : α ≃o β
⊢ ∀ (a x : α), x ∈ map f.symm.toEmbedding (Ici (f a)) ↔ a ≤ x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrderTop β
f : α ≃o β
⊢ ∀ (a x : α), x ∈ map f.symm.toEmbedding (Ioi (f a)) ↔ a < x

Tactic:
simp

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
x : α
hx : x ∈ Icc ↑a ↑b
⊢ p x

Tactic:
mem_Icc

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

Tactic:
simp

Goal state after:
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
a✝ : α
⊢ a✝ ∈ {j | a < j ∧ j ≤ b} ↔ a✝ ∈ Ioc a b

Tactic:
simp

Goal state after:
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
a✝ : α
⊢ a✝ ∈ {j | a ≤ j ∧ j < b} ↔ a✝ ∈ Ico a b

Tactic:
simp

Goal state after:
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
a✝ : α
⊢ a✝ ∈ {j | a ≤ j ∧ j ≤ b} ↔ a✝ ∈ Icc a b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
⊢ ∀ (x : α), x ∈ univ

Tactic:
simp

Goal state after:
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
⊢ a ∈ Iic a

Tactic:
simp

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
a✝ : α
⊢ a✝ ∈ {x | a < x} ↔ a✝ ∈ Ioi a

Tactic:
simp

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
a✝ : α
⊢ a✝ ∈ {x | a ≤ x} ↔ a✝ ∈ Ici a

Tactic:
simp

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
a✝ : α
⊢ a✝ ∈ {x | x < a} ↔ a✝ ∈ Iio a

Tactic:
simp

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
a✝ : α
⊢ a✝ ∈ {x | x ≤ a} ↔ a✝ ∈ Iic a

Tactic:
simp

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
hi : s.Infinite
⊢ False

Tactic:
obtain ⟨m, n, hmn, h⟩ := hp (hi.natEmbedding _)

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
hi : s.Infinite
m n : ℕ
hmn : m < n
h : Subrel r (fun x ↦ x ∈ s) ((Infinite.natEmbedding s hi) m) ((Infinite.natEmbedding s hi) n)
⊢ False
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
⊢ (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
hf

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)
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:
simp

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

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

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)
a✝ : α
⊢ a✝ ∈ (Icc a b).toFinset ↔ a✝ ∈ Finset.Icc a b

Tactic:
simp

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)
a✝ : α
⊢ a✝ ∈ (Ico a b).toFinset ↔ a✝ ∈ Finset.Ico a b

Tactic:
simp

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

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)
a✝ : α
⊢ a✝ ∈ (Ioo a b).toFinset ↔ a✝ ∈ Finset.Ioo a b

Tactic:
simp

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)
a✝ : α
⊢ a✝ ∈ (Ici a).toFinset ↔ a✝ ∈ Finset.Ici a

Tactic:
simp

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)
a✝ : α
⊢ a✝ ∈ (Ioi a).toFinset ↔ a✝ ∈ Finset.Ioi a

Tactic:
simp

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:
aesop (add safe forward [le_antisymm])

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m ≠ f n
h : n < m
⊢ rᶜ (f m) (f n)

Tactic:
exact mt symm (H _ _ h)

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:
aesop (add safe forward [le_antisymm])

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:
aesop (add safe forward [le_antisymm])

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:
aesop (add safe forward [le_antisymm])

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'
f : ℕ → α × β
⊢ (∀ (n : ℕ), f n ∈ s ×ˢ t) → ∃ m n, m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2

Tactic:
hf

Goal state after:
α : 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'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
⊢ ∃ m n, m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2
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)
f : ℕ → (i : ι) → α i
⊢ (∀ (n : ℕ), f n ∈ univ.pi s) → ∃ g, ∀ (m n : ℕ), m ≤ n → ∀ (i : ι), r i (f (g m) i) (f (g n) i)

Tactic:
hf

Goal state after:
ι : 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)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ), f n ∈ univ.pi s
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → ∀ (i : ι), r i (f (g m) i) (f (g n) i)
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:
simp

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1
ι : 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)
f : ℕ → (i : ι) → α i
⊢ (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ ∅, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)

Tactic:
hf

Goal state after:
case refine_1
ι : 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)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ) (i : ι), f n i ∈ s i
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ ∅, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
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:
rw [smul_mul', ha, hb]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2
ι : 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)
i : ι
t : Finset ι
hi : i ∉ t
ih :
  ∀ (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)
f : ℕ → (i : ι) → α i
⊢ (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
    ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i t hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)

Tactic:
hf

Goal state after:
case refine_2
ι : 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)
i : ι
t : Finset ι
hi : i ∉ t
ih :
  ∀ (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)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ) (i : ι), f n i ∈ s i
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i t hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)
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:
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico' hcb had]

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

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : Disjoint (f '' U) (f '' V)
a : α
a_in_U : a ∈ U
g : G
g_in_V : g • a ∈ V
⊢ (fun m ↦ m • g • a) g⁻¹ = a

Tactic:
simp

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

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

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

Goal state after:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
ha : a₂ ≤ a₁ ∧ a₁ ≤ b₂
hb : a₂ ≤ b₁ ∧ b₁ ≤ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂