mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a ⊓ s.sup f = s.sup fun i ↦ f i ⊓ a

Tactic:
s.sup_inf_distrib_left

Goal state after:
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (s.sup fun i ↦ a ⊓ f i) = s.sup fun i ↦ f i ⊓ a
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ a \ f b) = a \ s✝.inf f
⊢ ((cons a✝ s✝ h✝).sup fun b ↦ a \ f b) = a \ (cons a✝ s✝ h✝).inf f

Tactic:
sup_cons,

Goal state after:
case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ a \ f b) = a \ s✝.inf f
⊢ (a \ f a✝ ⊔ s✝.sup fun b ↦ a \ f b) = a \ (cons a✝ s✝ h✝).inf f
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
⊢ (s.sup fun b ↦ a \ f b) = a \ s.inf f

Tactic:
induction s using Finset.cons_induction with
  | empty => rw [sup_empty, inf_empty, sdiff_top]
  | cons _ _ _ h => rw [sup_cons, inf_cons, h, sdiff_inf]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (s✝.inf fun b ↦ a \ f b) = a \ s✝.sup f
⊢ ((cons a✝ s✝ h✝).inf fun b ↦ a \ f b) = a \ (cons a✝ s✝ h✝).sup f

Tactic:
sup_cons,

Goal state after:
case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (s✝.inf fun b ↦ a \ f b) = a \ s✝.sup f
⊢ ((cons a✝ s✝ h✝).inf fun b ↦ a \ f b) = a \ (f a✝ ⊔ s✝.sup f)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case mp.cons
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : c ∉ t
ih : a ≤ t.sup f → ∃ b ∈ t, a ≤ f b
⊢ a ≤ (cons c t hc).sup f → ∃ b ∈ cons c t hc, a ≤ f b

Tactic:
sup_cons,

Goal state after:
case mp.cons
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
c : ι
t : Finset ι
hc : c ∉ t
ih : a ≤ t.sup f → ∃ b ∈ t, a ≤ f b
⊢ a ≤ max (f c) (t.sup f) → ∃ b ∈ cons c t hc, a ≤ f b
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case mp.cons
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : c ∉ t
ih : a < t.sup f → ∃ b ∈ t, a < f b
⊢ a < (cons c t hc).sup f → ∃ b ∈ cons c t hc, a < f b

Tactic:
sup_cons,

Goal state after:
case mp.cons
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : c ∉ t
ih : a < t.sup f → ∃ b ∈ t, a < f b
⊢ a < max (f c) (t.sup f) → ∃ b ∈ cons c t hc, a < f b
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝² : DecidableEq α
inst✝¹ : Fintype (PLift ι)
f : ι → Set α
inst✝ : (i : ι) → Fintype ↑(f i)
⊢ ∀ (x : α), (x ∈ Finset.univ.biUnion fun i ↦ (f i.down).toFinset) ↔ x ∈ ⋃ i, f i

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
inst✝¹ : DecidableEq α
ι : Type u_1
s : Set ι
inst✝ : Fintype ↑s
t : ι → Set α
H : (i : ι) → i ∈ s → Fintype ↑(t i)
this : (i : ↥s.toFinset) → Fintype ↑(t ↑i)
x : α
⊢ (x ∈ s.toFinset.attach.biUnion fun x ↦ (t ↑x).toFinset) ↔ x ∈ ⋃ x ∈ s, t x

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
ι✝ : Sort w
γ : Type x
inst✝² : DecidableEq α
ι : Type u_1
s : Set ι
inst✝¹ : Fintype ↑s
t : ι → Set α
inst✝ : (i : ι) → Fintype ↑(t i)
⊢ ∀ (x : α), (x ∈ s.toFinset.biUnion fun x ↦ (t x).toFinset) ↔ x ∈ ⋃ x ∈ s, t x

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
⊢ (∀ (i : ι), (s i).Finite) ∧ {i | (s i).Nonempty}.Finite

Tactic:
refine ⟨fun i ↦ h.subset <| subset_iUnion _ _, ?_⟩
    let u (i : {i | (s i).Nonempty}) : ⋃ i, s i := ⟨i.2.choose, mem_iUnion.2 ⟨i.1, i.2.choose_spec⟩⟩
    have u_inj : Function.Injective u := by
      rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
      ext
      refine hs.eq <| not_disjoint_iff.2 ⟨u ⟨i, hi⟩, hi.choose_spec, ?_⟩
      rw [hij]
      exact hj.choose_spec
    have : Finite (⋃ i, s i) := h
    exact .of_injective u u_inj

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

Goal state before:
pp: ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∉ s
⊢ ↑⊥ ≤ ↑(f j)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
⊢ (fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩) ((fun a ↦ untopD ⊤ (map Subtype.val a)) ⊤) = ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a✝ b✝ : WithTop { a // a ≠ ⊤ }
a b : { a // a ≠ ⊤ }
⊢ { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩, left_inv := ⋯,
          right_inv := ⋯ }
        ↑a ≤
      { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ↑b ↔
    ↑a ≤ ↑b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a✝ b a : WithTop { a // a ≠ ⊤ }
⊢ { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩, left_inv := ⋯,
          right_inv := ⋯ }
        a ≤
      { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⊤ ↔
    a ≤ ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Ico a b = Ico ↑a ↑b

Tactic:
by
  rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ico_subset_Iio_self <| Iio_subset_Iio le_top)]

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: case cons
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ↑t ⊆ ⋃ i, f i → ∃ i, ↑t ⊆ f i
hs : ↑(Finset.cons b t hbt) ⊆ ⋃ i, f i
⊢ ∃ i, ↑(Finset.cons b t hbt) ⊆ f i

Tactic:
| cons b t hbt iht =>

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Finset ι
h : s.Nonempty
h' : (image f s).Nonempty
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Finset ι
h : s.Nonempty
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Set ι
h : s.Nonempty
hs : s.Finite
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set ι
a : α
f : ι → α
h : s.Nonempty
hs : s.Finite
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this✝ : Nonempty ↑s
i : ι
h : i ∈ s
this : f i ∈ f '' s
⊢ g ↑⟨f i, this⟩ = g (f ↑⟨i, h⟩)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
b : ι
⊢ b ∈ {b}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: ι : Type u_5
s : Set ι
x : ι
hx : x ∈ s
⊢ ⟨x, ⋯⟩ ∈ {⟨x, hx⟩}

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
a : α
s : α → β
⊢ ⨆ x ∈ {a}, s x = s a

Tactic:
by simp

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

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
j : ι
hj : p j
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅

pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
j : ι
hj : ¬p j
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅

Tactic:
· exact ((ciSup_pos hj).trans_le (le_ciSup bdd ⟨j, hj⟩)).trans gt.le

Goal state after:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
j : ι
hj : ¬p j
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ ↑(∅.preimage f ⋯) = ↑∅

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype β
hf : InjOn f (f ⁻¹' ↑univ)
⊢ ↑(univ.preimage f hf) = ↑univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s t : Finset β
hs : InjOn f (f ⁻¹' ↑s)
ht : InjOn f (f ⁻¹' ↑t)
⊢ ↑((s ∩ t).preimage f ⋯) = ↑(s.preimage f hs ∩ t.preimage f ht)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
s : Finset β
hfc : InjOn f (f ⁻¹' ↑sᶜ)
hf : InjOn f (f ⁻¹' ↑s)
⊢ ↑(sᶜ.preimage f hfc) = ↑(s.preimage f hf)ᶜ

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx : x.snd ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) (⋯ ▸ ⟨x.1, b⟩.snd)
⊢ (Embedding.sigmaMk ⟨x.1, b⟩.fst) x.snd = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
e : α ≃ β
s : Finset β
b : ↥s
⊢ e.symm ↑b ∈ s.preimage ⇑e ⋯

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
e : α ≃ β
s : Finset β
x✝ : ↥(s.preimage ⇑e ⋯)
⊢ (fun b ↦ ⟨e.symm ↑b, ⋯⟩) ((fun a ↦ ⟨e ↑a, ⋯⟩) x✝) = x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
e : α ≃ β
s : Finset β
x✝ : ↥s
⊢ (fun a ↦ ⟨e ↑a, ⋯⟩) ((fun b ↦ ⟨e.symm ↑b, ⋯⟩) x✝) = x✝

Tactic:
by simp

Goal state after:
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 : ι
⊢ MaximalFor (fun x ↦ x ∈ {i}) f i

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ (a ≤ x ∧ x ≤ b) ∧ ¬x ≤ a ↔ a < x ∧ x ≤ b

Tactic:
and_right_comm,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: ι : Sort u_1
h : IsEmpty ι
⊢ ⨅ x, 0 = 0

Tactic:
by simp

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

Goal state before:
pp: ι : Sort u_1
h : Nonempty ι
⊢ (0 ∈ range fun x ↦ 0) ∨ (range fun x ↦ 0) = ∅

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ (a ≤ x ∧ x ≤ b) ∧ a ≠ x ↔ a < x ∧ x ≤ b

Tactic:
and_right_comm,

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ (a ≤ x ∧ a ≠ x) ∧ x ≤ b ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Set.Icc a b)
x✝ : α
⊢ x✝ ∈ Icc a b ↔ x✝ ∈ Set.Icc a b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Set.Ico a b)
x✝ : α
⊢ x✝ ∈ Ico a b ↔ x✝ ∈ Set.Ico a b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Set.Ioo a b)
x✝ : α
⊢ x✝ ∈ Ioo a b ↔ x✝ ∈ Set.Ioo a b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Set.Ici a)
x✝ : α
⊢ x✝ ∈ Ici a ↔ x✝ ∈ Set.Ici a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Set.Ioi a)
x✝ : α
⊢ x✝ ∈ Ioi a ↔ x✝ ∈ Set.Ioi a

Tactic:
by simp

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

Goal state before:
pp: a b : ℕ
⊢ a ∈ Ioc b (b + 1) ↔ a = b + 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x✝ : α
⊢ x✝ ∈ Finset.Icc a b ↔ x✝ ∈ Icc a b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x✝ : α
⊢ x✝ ∈ Finset.Ico a b ↔ x✝ ∈ Ico a b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x✝ : α
⊢ x✝ ∈ Finset.Ioo a b ↔ x✝ ∈ Ioo a b

Tactic:
by 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✝² : Fintype α
inst✝¹ : DecidableLT α
inst✝ : DecidableLE α
a b x : α
⊢ x ∈ (Set.Icc a b).toFinset ↔ a ≤ x ∧ x ≤ b

Tactic:
simp only [Set.mem_toFinset, Set.mem_Icc]

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 ∈ (Ioo (f a) (f b)).preimage ⇑f ⋯ ↔ a < x ∧ x < b

Tactic:
by rw [mem_preimage, mem_Ioo, f.lt_iff_lt, f.lt_iff_lt]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
f : ℕ → α
hf : StrictAnti f
n : ℕ
⊢ n < n + 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
⊢ ⊤ ∉ Finset.map Embedding.coeWithTop s

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

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

Tactic:
obtain hlt | rfl := hle.lt_or_eq

Goal state after:
case inl.inl
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))
m n : ℕ
hle : m ≤ n
hlt : m < n
⊢ r (f (g m)) (f (g n))

case inl.inr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))
m : ℕ
hle : m ≤ m
⊢ r (f (g m)) (f (g m))
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
f : ℕ → α
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
obtain ⟨g, gmon⟩ := h f

Goal state after:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
f : ℕ → α
g : ℕ ↪o ℕ
gmon : ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : seed.succ ≤ x✝
hP✝ : P x✝
⊢ x✝ = 1 * x✝

Tactic:
rw [one_mul]

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

Goal state after:
Module: Mathlib.Order.WellFoundedSet

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

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

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

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 simp

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 : ι
⊢ ∀ (s_1 : Finset ι) (h : i ∉ s_1),
    (∀ (f : ℕ → (i : ι) → α i),
        (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s_1, 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 s_1 h, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)

Tactic:
t

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 ι
⊢ ∀ (h : i ∉ t),
    (∀ (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 h, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)
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 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:
by simp

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 : α
⊢ x ∈ orbitRel.Quotient.orbit (Quotient.mk'' x)

Tactic:
by simp

Goal state after: