mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ (map (id ∘ cons a) (sublistsLen n l) ++ []) =
    sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)

Tactic:
append_nil

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (id ∘ cons a) (sublistsLen n l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
l : List α
⊢ List.map ofList (sublistsLen n l) ++ [] = List.map ofList (sublistsLen n l)

Tactic:
append_nil

Goal state after:
α : Type u_1
n : ℕ
l : List α
⊢ List.map ofList (sublistsLen n l) = List.map ofList (sublistsLen n l)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.nil
α : Type u
l l' l₂ : List α
a : α
s : [] <+ l₂
IH : [] ∈ sublistsLen [].length l₂
⊢ [] ∈ sublistsLen [].length (a :: l₂)

pp: case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (b :: l₁).length (a :: l₂)

Tactic:
· simp

Goal state after:
case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (b :: l₁).length (a :: l₂)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case succ.swap.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++
      (List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b ∘ cons a) (powersetCardAux n✝ l✝)) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      (List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝))

Tactic:
rw [← append_assoc, ← append_assoc,
      (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]

Goal state after:
case succ.swap.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ ∀ (a : List (Fin l.length)), a ∈ (finRange l.length).sublists ↔ a ∈ (finRange l.length).sublists'

pp: α : Type u
l : List α
⊢ (finRange l.length).sublists.Nodup

pp: α : Type u
l : List α
⊢ (finRange l.length).sublists'.Nodup

Tactic:
· simp

Goal state after:
α : Type u
l : List α
⊢ (finRange l.length).sublists.Nodup

α : Type u
l : List α
⊢ (finRange l.length).sublists'.Nodup
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ l.sublists ~ l.sublists'

Tactic:
rw [← map_get_finRange l, sublists_map, sublists'_map]
  apply Perm.map
  apply (perm_ext_iff_of_nodup _ _).mpr
  · simp
  · exact nodup_sublists.mpr (nodup_finRange _)
  · exact (nodup_sublists'.mpr (nodup_finRange _))

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l₁ l₂ : List α
sublist : l₁ <+ l₂
⊢ l₁.sublists' <+ l₂.sublists'

Tactic:
induction sublist with
  | slnil => exact .refl _
  | cons a _ ih =>
    rw [sublists'_cons]
    exact ih.trans (List.sublist_append_left ..)
  | cons_cons a _ ih =>
    rw [sublists'_cons, sublists'_cons]
    exact ih.append (ih.map _)

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

Goal state before:
pp: α : Type u_1
s : Finset α
β : Type u_2
inst✝ : DecidableEq β
f : α → β
H : Set.InjOn f ↑s
this : ∀ {z : Finset α} {a : α}, z ⊆ s → a ∈ s → (a ∈ z ↔ f a ∈ image f z)
x✝⁴ : Finset α
x✝³ : x✝⁴ ∈ ↑s.powerset
x✝² : Finset α
x✝¹ : x✝² ∈ ↑s.powerset
x✝ : (fun x ↦ image f x) x✝⁴ = (fun x ↦ image f x) x✝²
⊢ x✝⁴ = x✝²

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
β : Type u_2
inst✝ : DecidableEq β
f : α → β
t : Finset β
ht : t ∈ ↑(image f s).powerset
⊢ {x ∈ s | f x ∈ t} ∈ ↑s.powerset ∧ (fun x ↦ image f x) ({x ∈ s | f x ∈ t}) = t

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
β : Type u_2
inst✝ : DecidableEq β
f : α → β
a : Finset β
x✝ : a ∈ (image f s).powerset
⊢ {x ∈ s | f x ∈ a} ∈ s.powerset ∧ image f ({x ∈ s | f x ∈ a}) = a

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
β : Type u_2
inst✝ : DecidableEq β
f : α → β
a : Finset β
⊢ a ∈ image (fun x ↦ image f x) s.powerset → a ∈ (image f s).powerset

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
⊢ #({x ∈ powersetCard n t | s ⊆ x}) = (#t - #s).choose (n - #s)

Tactic:
have hinj : Set.InjOn (· ∪ s) ↑((t \ s).powersetCard (n - #s)) := fun a ha b hb hab =>
    (union_sdiff_cancel_right
      (disjoint_of_subset_left (mem_powersetCard.mp ha).1 disjoint_sdiff_self_left)).symm.trans
    ((congrArg (· \ s) hab).trans
      (union_sdiff_cancel_right
        (disjoint_of_subset_left (mem_powersetCard.mp hb).1 disjoint_sdiff_self_left)))

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hinj : Set.InjOn (fun x ↦ x ∪ s) ↑(powersetCard (n - #s) (t \ s))
⊢ #({x ∈ powersetCard n t | s ⊆ x}) = (#t - #s).choose (n - #s)
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset (Option α)
x : α
⊢ x ∈ eraseNone s ↔ some x ∈ s

Tactic:
by
  simp [eraseNone]

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

Goal state before:
pp: case insert
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs : (insert a s).Nonempty
⊢ (insert a s).sup f ∈ f '' ↑(insert a s)

Tactic:
rw [Finset.sup_insert (b := a) (s := s) (f := f)]

Goal state after:
case insert
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs : (insert a s).Nonempty
⊢ max (f a) (s.sup f) ∈ f '' ↑(insert a s)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Sort v
κ : ι → Sort w
inst✝¹ : Order.Frame α
inst✝ : Finite ι
f : (a : ι) → κ a → α
this : ∀ {ι : Type v} {κ : ι → Type w} [Finite ι] (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
by
    simpa [← Equiv.plift.symm.iInf_comp, ← Equiv.plift.symm.iSup_comp,
        ← (Equiv.plift.piCongr fun a => @Equiv.plift (κ a.down)).symm.iSup_comp] using!
      this (κ := fun a => PLift (κ a.down)) fun (a : PLift ι) b => f a.down b.down

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
h✝¹ : Nonempty β
h✝ : Nonempty γ
B : α
hB : ∀ y ∈ range f, y ≤ B
z : β
hy : ⨆ c, f (z, c) ∈ range fun b ↦ ⨆ c, f (b, c)
c : γ
⊢ f (z, c) ≤ B

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
b : β
B : α
hB : ∀ y ∈ range f, y ≤ B
⊢ ∀ y ∈ range fun c ↦ f (b, c), y ≤ B

Tactic:
by grind

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

Goal state before:
pp: α : Type u_5
inst✝¹ : CompleteLinearOrder α
ι : Sort u_6
inst✝ : Finite ι
f : ι → α
a : α
hne : a ≠ ⊥
h : ∀ (x : ι), f x ≠ a
⊢ a ∉ range f

Tactic:
by grind

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)
⊢ ⨆ i ∈ f '' s, g i = ⨆ x ∈ s, g (f x)

Tactic:
by
  rcases s.eq_empty_or_nonempty with (rfl | hs)
  · rw [Set.image_empty, cbiSup_empty, cbiSup_empty]
  have hg : BddAbove (Set.range fun i : f '' s ↦ g i) := by
    simpa [bddAbove_def] using hf
  have hf' : sSup ∅ ≤ ⨆ i : f '' s, g i := by
    refine hg'.trans ?_
    have : Nonempty s := Set.Nonempty.to_subtype hs
    refine ciSup_le ?_
    intro ⟨i, h⟩
    obtain ⟨t, ht⟩ : ∃ t : f '' s, g t = g (f (Subtype.mk i h)) := by
      have : f i ∈ f '' s := Set.mem_image_of_mem _ h
      exact ⟨⟨f i, this⟩, by simp⟩
    rw [← ht]
    refine le_ciSup_set ?_ t.prop
    simpa [bddAbove_def] using hf
  rw [← csSup_image hg hf', ← csSup_image hf hg', ← Set.image_comp, comp_def]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
i : ι
⊢ range (Sigma.mk i) = Sigma.fst ⁻¹' {i}

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b

Tactic:
refine ⟨fun h2 => h.eq_or_eq h2.1 h2.2, ?_⟩; rintro (rfl | rfl)
  exacts [⟨le_rfl, h.le⟩, ⟨h.le, le_rfl⟩]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
i j : ι
h : i ≠ j
s : Set (α j)
⊢ Sigma.mk i ⁻¹' Sigma.mk j '' s = ∅

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
⊢ s.sigma t ⊆ u ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃a : α i⦄, a ∈ t i → ⟨i, a⟩ ∈ u

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
p : (i : ι) × α i → Prop
⊢ (∀ x ∈ s.sigma t, p x) ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃a : α i⦄, a ∈ t i → p ⟨i, a⟩

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
p : (i : ι) × α i → Prop
⊢ (∃ x ∈ s.sigma t, p x) ↔ ∃ i ∈ s, ∃ a ∈ t i, p ⟨i, a⟩

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
⊢ (s.sigma fun i ↦ ∅) = ∅

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
⊢ ∅.sigma t = ∅

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
i : ι
⊢ (univ.sigma fun x ↦ univ) = univ

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
⊢ (s.sigma fun x ↦ univ) = Sigma.fst ⁻¹' s

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ((i : ι) × α i)
⊢ (univ.sigma fun i ↦ Sigma.mk i ⁻¹' s) = s

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
t : (i : ι) → Set (α i)
i : ι
⊢ {i}.sigma t = Sigma.mk i '' t i

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
a : (i : ι) → α i
⊢ (s.sigma fun i ↦ {a i}) = (fun i ↦ ⟨i, a i⟩) '' s

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
i : ι
a : (i : ι) → α i
⊢ ({i}.sigma fun i ↦ {a i}) = {⟨i, a i⟩}

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t : (i : ι) → Set (α i)
⊢ (s₁ ∪ s₂).sigma t = s₁.sigma t ∪ s₂.sigma t

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ (s.sigma fun i ↦ t₁ i ∪ t₂ i) = s.sigma t₁ ∪ s.sigma t₂

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
⊢ (insert i s).sigma t = Sigma.mk i '' t i ∪ s.sigma t

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ (s.sigma fun i ↦ insert (a i) (t i)) = (fun i ↦ ⟨i, a i⟩) '' s ∪ s.sigma t

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hi : i ∈ s
⊢ Sigma.mk i ⁻¹' s.sigma t = t i

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
hi : i ∉ s
⊢ Sigma.mk i ⁻¹' s.sigma t = ∅

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Sigma.mk i ⁻¹' s.sigma t = if i ∈ s then t i else ∅

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
β : Type u_7
inst✝ : DecidablePred fun x ↦ x ∈ s
g : β → α i
⊢ (fun b ↦ ⟨i, g b⟩) ⁻¹' s.sigma t = if i ∈ s then g ⁻¹' t i else ∅

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
x✝ : a ⋖ c ∧ c ⋖ b
hac : a ⋖ c
hcb : c ⋖ b
⊢ {c} ∪ Ico c b = {c}

Tactic:
hcb.Ico_eq,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
x✝ : a ⋖ c ∧ c ⋖ b
hac : a ⋖ c
hcb : c ⋖ b
⊢ {c} ∪ {c} = {c}
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x ↦ x ∈ t ∩ range ⇑f) (f x)
y : α
hy : (fun x ↦ f x ∈ t) y
⊢ f y ≤ f x → f x ≤ f y

Tactic:
exact h.le_of_le ⟨hy, mem_range_self y⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α
finset_mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ x ≤ a ∧ b ≤ x
finset_mem_Ico : ∀ (a b x : α), x ∈ finsetIco a b ↔ x ≤ a ∧ b < x
finset_mem_Ioc : ∀ (a b x : α), x ∈ finsetIoc a b ↔ x < a ∧ b ≤ x
finset_mem_Ioo : ∀ (a b x : α), x ∈ finsetIoo a b ↔ x < a ∧ b < x
⊢ ∀ (a b x : α), x ∈ swap finsetIcc a b ↔ a ≤ x ∧ x ≤ b

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α
finset_mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ x ≤ a ∧ b ≤ x
finset_mem_Ico : ∀ (a b x : α), x ∈ finsetIco a b ↔ x ≤ a ∧ b < x
finset_mem_Ioc : ∀ (a b x : α), x ∈ finsetIoc a b ↔ x < a ∧ b ≤ x
finset_mem_Ioo : ∀ (a b x : α), x ∈ finsetIoo a b ↔ x < a ∧ b < x
⊢ ∀ (a b x : α), x ∈ swap finsetIoc a b ↔ a ≤ x ∧ x < b

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α
finset_mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ x ≤ a ∧ b ≤ x
finset_mem_Ico : ∀ (a b x : α), x ∈ finsetIco a b ↔ x ≤ a ∧ b < x
finset_mem_Ioc : ∀ (a b x : α), x ∈ finsetIoc a b ↔ x < a ∧ b ≤ x
finset_mem_Ioo : ∀ (a b x : α), x ∈ finsetIoo a b ↔ x < a ∧ b < x
⊢ ∀ (a b x : α), x ∈ swap finsetIco a b ↔ a < x ∧ x ≤ b

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
finsetIcc finsetIco finsetIoc finsetIoo : α → α → Finset α
finset_mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ x ≤ a ∧ b ≤ x
finset_mem_Ico : ∀ (a b x : α), x ∈ finsetIco a b ↔ x ≤ a ∧ b < x
finset_mem_Ioc : ∀ (a b x : α), x ∈ finsetIoc a b ↔ x < a ∧ b ≤ x
finset_mem_Ioo : ∀ (a b x : α), x ∈ finsetIoo a b ↔ x < a ∧ b < x
⊢ ∀ (a b x : α), x ∈ swap finsetIoo a b ↔ a < x ∧ x < b

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Icc a b ↔ x ≤ b ∧ a ≤ x

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ico a b ↔ x < b ∧ a ≤ x

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioc a b ↔ x ≤ b ∧ a < x

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioo a b ↔ x < b ∧ a < x

Tactic:
by grind

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

Goal state before:
pp: a : ℕ
⊢ Ico a (a + 1) = {a}

Tactic:
by grind

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

Goal state before:
pp: b : ℕ
⊢ Ioc b (b + 1) = {b + 1}

Tactic:
by grind

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

Goal state before:
pp: n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
classical
  obtain h | ⟨m, hm⟩ := { m | p (m + n) }.eq_empty_or_nonempty
  · rw [h, Nat.sInf_empty, zero_add]
    obtain hnp | hnp := hn.eq_or_lt
    · exact hnp
    suffices hp : p (sInf { m | p m } - n + n) from (h.subset hp).elim
    rw [Nat.sub_add_cancel hn]
    exact csInf_mem (nonempty_of_pos_sInf <| n.zero_le.trans_lt hnp)
  · have hp : ∃ n, n ∈ { m | p m } := ⟨_, hm⟩
    rw [Nat.sInf_def ⟨m, hm⟩, Nat.sInf_def hp]
    rw [Nat.sInf_def hp] at hn
    exact find_add hn

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

Goal state before:
pp: a b : ℕ
⊢ (range' a b).toFinset = Ico a (a + b)

Tactic:
ext x
  rw [List.mem_toFinset, List.mem_range'_1, Finset.mem_Ico]

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) (Ico a b) = Ico ↑a ↑b

Tactic:
rw [subtype_Ico_eq]
  refine Finset.subtype_map_of_mem fun x hx => ?_
  rw [mem_Ico] at hx
  exact hp hx.1 hx.2.le a.prop b.prop

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:
simpa only [coe_Iic] using! (Finset.Iic y).finite_toSet

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_cases h : a ≤ b

Goal state after:
case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ #(Ico a b) = #(Icc a b) - 1

case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a ≤ b
⊢ #(Ico a b) = #(Icc a b) - 1
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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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 grind

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
  simp only [← wellFoundedOn_insert (a := a), insert_sdiff_singleton, mem_insert_iff, true_or,
    insert_eq_of_mem]

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

pp: case refine_2
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'
⊢ (∀ x ∈ U, ∀ (g : G), g • x ∉ V) → Disjoint (f '' U) (f '' V)

Tactic:
· simp

Goal state after:
case refine_2
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'
⊢ (∀ x ∈ U, ∀ (g : G), g • x ∉ V) → Disjoint (f '' U) (f '' V)
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:
rw [mem_uIcc] at h₁ h₂
  exact Icc_subset_Icc (_root_.le_inf h₁.1 h₂.1) (_root_.sup_le h₁.2 h₂.2)

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:
Finset.ext_iff

Goal state after:
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
h : ∀ (a_1 : α), a_1 ∈ (fun b ↦ [[b, a]]) b ↔ a_1 ∈ (fun b ↦ [[b, a]]) c
⊢ b = c
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
⊢ (∀ (i : ι),
      (∀ (a : A i), x i * a = a * x i) ∧
        (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)) →
    (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
      (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
        ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)

Tactic:
by grind

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
⊢ x✝ ∈ center Mˣ

Tactic:
_root_.Semigroup.mem_center_iff

Goal state after:
M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
⊢ ∀ (g : Mˣ), g * x✝ = x✝ * g
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a : M
ha : a ∈ center M
⊢ a⁻¹ ∈ center M

Tactic:
_root_.Semigroup.mem_center_iff

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a : M
ha : a ∈ center M
⊢ ∀ (g : M), g * a⁻¹ = a⁻¹ * g