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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
val✝ : α
h : argmax f tl = some val✝
h✝ : f hd < f val✝
ham : f val✝ ≤ f hd
⊢ (if hd = val✝ then 0 else idxOf val✝ tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
val✝ : α
h : argmax f tl = some val✝
h✝ : ¬f hd < f val✝
ham : f hd ≤ f hd
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ (if hd = val✝ then 0 else idxOf val✝ tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
· cases not_le_of_gt ‹_› ‹_›

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
val✝ : α
h : argmax f tl = some val✝
h✝ : ¬f hd < f val✝
ham : f hd ≤ f hd
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ (if hd = val✝ then 0 else idxOf val✝ tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_4
β : Type u_5
s₁ s₂ : Finset α
t₁ t₂ : Finset β
⊢ s₁.disjSum t₁ = s₂.disjSum t₂ ↔ s₁ = s₂ ∧ t₁ = t₂

Tactic:
by
  simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s.disjSum t).toLeft = s

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : α
⊢ x ∈ (s.disjSum t).toLeft ↔ x ∈ s
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s.disjSum t).toRight = t

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : β
⊢ x ∈ (s.disjSum t).toRight ↔ x ∈ t
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ (map (Equiv.sumComm α β).toEmbedding u).toLeft = u.toRight

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : β
⊢ x ∈ (map (Equiv.sumComm α β).toEmbedding u).toLeft ↔ x ∈ u.toRight
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ (map (Equiv.sumComm α β).toEmbedding u).toRight = u.toLeft

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : α
⊢ x ∈ (map (Equiv.sumComm α β).toEmbedding u).toRight ↔ x ∈ u.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (image Sum.swap u).toLeft = u.toRight

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (image Sum.swap u).toLeft ↔ x ∈ u.toRight
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (image Sum.swap u).toRight = u.toLeft

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (image Sum.swap u).toRight ↔ x ∈ u.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∩ v).toLeft = u.toLeft ∩ v.toLeft

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u ∩ v).toLeft ↔ x ∈ u.toLeft ∩ v.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∩ v).toRight = u.toRight ∩ v.toRight

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (u ∩ v).toRight ↔ x ∈ u.toRight ∩ v.toRight
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∪ v).toLeft = u.toLeft ∪ v.toLeft

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u ∪ v).toLeft ↔ x ∈ u.toLeft ∪ v.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∪ v).toRight = u.toRight ∪ v.toRight

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (u ∪ v).toRight ↔ x ∈ u.toRight ∪ v.toRight
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u \ v).toLeft = u.toLeft \ v.toLeft

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u \ v).toLeft ↔ x ∈ u.toLeft \ v.toLeft
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u \ v).toRight = u.toRight \ v.toRight

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (u \ v).toRight ↔ x ∈ u.toRight \ v.toRight
Module: Mathlib.Data.List.Zip

Goal state before:
pp: α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) ∈ ([], hd :: tl) :: (map (fun t ↦ hd :: t) tl.inits).zip tl.tails ↔ init ++ tail = hd :: tl

Tactic:
constructor <;> rw [mem_cons, zip_map_left, mem_map, Prod.exists]

Goal state after:
case mp
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ ((init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (init, tail)) →
    init ++ tail = hd :: tl

case mpr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl →
    (init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (init, tail)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
s : List α
h : s = []
⊢ s <+ []

Tactic:
by rw [h]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetAux' l₁ ~ powersetAux' l₂

Tactic:
induction p with
  | nil => simp
  | cons _ _ IH =>
    simp only [powersetAux'_cons]
    exact IH.append (IH.map _)
  | swap a b =>
    simp only [powersetAux'_cons, map_append, List.map_map, append_assoc]
    apply Perm.append_left
    rw [← append_assoc, ← append_assoc,
      (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
    exact perm_append_comm.append_right _
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂

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

Goal state before:
pp: α : Type u
s t : List α
⊢ s ∈ t.sublists ↔ s.reverse ∈ map reverse t.sublists

Tactic:
mem_map_of_injective reverse_injective

Goal state after:
α : Type u
s t : List α
⊢ s ∈ t.sublists ↔ s ∈ t.sublists
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
β : Type v
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = map f (sublistsLen n l) ++ r

Tactic:
rw [sublistsLen, ← sublistsLenAux_append]; rfl

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

Goal state before:
pp: case empty.zero
α : Type u_1
β : Type u_2
f : α → β
⊢ powersetCard 0 (map f 0) = map (map f) (powersetCard 0 0)

Tactic:
simp [powersetCard_zero_left]

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

Goal state before:
pp: case empty.succ
α : Type u_1
β : Type u_2
f : α → β
n✝ : ℕ
⊢ powersetCard (n✝ + 1) (map f 0) = map (map f) (powersetCard (n✝ + 1) 0)

Tactic:
simp [powersetCard_zero_left]

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

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
⊢ (s.erase ⊥).sup id = s.sup id

Tactic:
by
  refine (sup_mono (s.erase_subset _)).antisymm (Finset.sup_le_iff.2 fun a ha => ?_)
  obtain rfl | ha' := eq_or_ne a ⊥
  · exact bot_le
  · exact le_sup (mem_erase.2 ⟨ha', ha⟩)

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

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n ↦ sublistsLen n (h :: tl)) (range ((h :: tl).length + 1)) ~ (h :: tl).sublists'

Tactic:
| cons h tl l_ih =>

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} = image (fun x ↦ x ∪ s) (powersetCard (n - #s) (t \ s))

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
⊢ x ∈ {x ∈ powersetCard n t | s ⊆ x} ↔ x ∈ image (fun x ↦ x ∪ s) (powersetCard (n - #s) (t \ s))
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ s.sup f ↔ ∃ b ∈ s, a ≤ f b

Tactic:
by
  apply Iff.intro
  · induction s using cons_induction with
    | empty => exact (absurd · (not_le_of_gt ha))
    | cons c t hc ih =>
      rw [sup_cons, le_sup_iff]
      exact fun
      | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
      | Or.inr h => let ⟨b, hb, hle⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hle⟩
  · exact fun ⟨b, hb, hle⟩ => le_trans hle (le_sup hb)

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : p
⊢ ⨆ (h : p), f h = f hp

Tactic:
simp [hp]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ⨆ i ∈ s, f i = (image f s).max' h'

Tactic:
rw [iSup, ← h'.csSup_eq_max', coe_image]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ sSup (Set.range fun i ↦ ⨆ (_ : i ∈ s), f i) = sSup (f '' ↑s)
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
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i ↦ ⟨Exists.choose ⋯, ⋯⟩
⊢ {i | (s i).Nonempty}.Finite

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

Goal state after:
α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i ↦ ⟨Exists.choose ⋯, ⋯⟩
u_inj : Injective u
⊢ {i | (s i).Nonempty}.Finite
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
⊢ t = ⋃ i, (fun x ↦ s ↑x ∩ t) i

Tactic:
ext x

Goal state after:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ x ∈ t ↔ x ∈ ⋃ i, (fun x ↦ s ↑x ∩ t) i
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ioc ↑a ↑b ∩ Iio ⊤ = Ioc ↑a ↑b

Tactic:
inter_eq_self_of_subset_left
      (Subset.trans Ioc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ioc ↑a ↑b = Ioc ↑a ↑b
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ioi ↑a = some '' Ioi a ∪ {⊤}

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
x : WithTop α
⊢ x ∈ Ioi ↑a ↔ x ∈ some '' Ioi a ∪ {⊤}
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ici ↑a = some '' Ici a ∪ {⊤}

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
x : WithTop α
⊢ x ∈ Ici ↑a ↔ x ∈ some '' Ici a ∪ {⊤}
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr
α : 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)
hf' : sSup ∅ ≤ ⨆ i, g ↑i
⊢ sSup (g '' f '' s) = sSup ((fun x ↦ g (f x)) '' s)

Tactic:
← Set.image_comp,

Goal state after:
case inr
α : 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)
hf' : sSup ∅ ≤ ⨆ i, g ↑i
⊢ sSup (g ∘ f '' s) = sSup ((fun x ↦ g (f x)) '' s)
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: ι : Type u_5
s : Set ι
⊢ ⋃ s', Subtype.val '' ↑s' = s

Tactic:
ext x

Goal state after:
ι : Type u_5
s : Set ι
x : ι
⊢ x ∈ ⋃ s', Subtype.val '' ↑s' ↔ x ∈ s
Module: Mathlib.Data.Set.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
β : (i : ι) → α i → Type u_7
s : Set ι
t : (i : ι) → Set (α i)
u : (p : (i : ι) × α i) → Set (β p.fst p.snd)
⊢ Sigma.uncurry ⁻¹' (s.sigma t).pi u = s.pi fun i ↦ (t i).pi fun j ↦ u ⟨i, j⟩

Tactic:
ext x

Goal state after:
ι : Type u_1
α : ι → Type u_3
β : (i : ι) → α i → Type u_7
s : Set ι
t : (i : ι) → Set (α i)
u : (p : (i : ι) × α i) → Set (β p.fst p.snd)
x : (x : ι) → (y : α x) → β x y
⊢ x ∈ Sigma.uncurry ⁻¹' (s.sigma t).pi u ↔ x ∈ s.pi fun i ↦ (t i).pi fun j ↦ u ⟨i, j⟩
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
⊢ (t.sigma fun a ↦ s.preimage (Sigma.mk a) ⋯) = {a ∈ s | a.fst ∈ t}

Tactic:
ext x

Goal state after:
α : Type u
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
x : (i : α) × β i
⊢ (x ∈ t.sigma fun a ↦ s.preimage (Sigma.mk a) ⋯) ↔ x ∈ {a ∈ s | a.fst ∈ t}
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
s : Finset (α ⊕ β)
⊢ s.preimage Sum.inl ⋯ = s.toLeft

Tactic:
ext x

Goal state after:
α : Type u
β : Type v
s : Finset (α ⊕ β)
x : α
⊢ x ∈ s.preimage Sum.inl ⋯ ↔ x ∈ s.toLeft
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
s : Finset (α ⊕ β)
⊢ s.preimage Sum.inr ⋯ = s.toRight

Tactic:
ext x

Goal state after:
α : Type u
β : Type v
s : Finset (α ⊕ β)
x : β
⊢ x ∈ s.preimage Sum.inr ⋯ ↔ x ∈ s.toRight
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
h : Set.range ⇑f = Set.range ⇑g
ef : ↑Set.univ ≃o ↑(⇑f '' Set.univ) := StrictMonoOn.orderIso (⇑f) Set.univ ⋯
eg : ↑Set.univ ≃o ↑(⇑g '' Set.univ) := StrictMonoOn.orderIso (⇑g) Set.univ ⋯
i : ↑(⇑f '' Set.univ) ≃o ↑(⇑g '' Set.univ) :=
  let __spread.0 := Equiv.setCongr ⋯;
  { toEquiv := __spread.0, map_rel_iff' := ⋯ }
this : (ef.trans i).trans eg.symm = OrderIso.refl ↑Set.univ
⊢ f = g

Tactic:
ext x

Goal state after:
α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
h : Set.range ⇑f = Set.range ⇑g
ef : ↑Set.univ ≃o ↑(⇑f '' Set.univ) := StrictMonoOn.orderIso (⇑f) Set.univ ⋯
eg : ↑Set.univ ≃o ↑(⇑g '' Set.univ) := StrictMonoOn.orderIso (⇑g) Set.univ ⋯
i : ↑(⇑f '' Set.univ) ≃o ↑(⇑g '' Set.univ) :=
  let __spread.0 := Equiv.setCongr ⋯;
  { toEquiv := __spread.0, map_rel_iff' := ⋯ }
this : (ef.trans i).trans eg.symm = OrderIso.refl ↑Set.univ
x : α
⊢ f x = g x
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a : ℕ
h : 0 < a
⊢ Ico (a - 1) a = {a - 1}

Tactic:
ext x

Goal state after:
a : ℕ
h : 0 < a
x : ℕ
⊢ x ∈ Ico (a - 1) a ↔ x ∈ {a - 1}
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b c : ℕ
h : c ≤ a
⊢ image (fun x ↦ x - c) (Ico a b) = Ico (a - c) (b - c)

Tactic:
ext x

Goal state after:
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ x ∈ image (fun x ↦ x - c) (Ico a b) ↔ x ∈ Ico (a - c) (b - c)
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b c : ℕ
hac : a ≤ c
⊢ image (fun x ↦ c - x) (Ico a b) = Ico (c + 1 - b) (c + 1 - a)

Tactic:
ext x

Goal state after:
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ x ∈ image (fun x ↦ c - x) (Ico a b) ↔ x ∈ Ico (c + 1 - b) (c + 1 - a)
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b : ℕ
⊢ Ico a.succ b = (Ico a b).erase a

Tactic:
ext x

Goal state after:
a b x : ℕ
⊢ x ∈ Ico a.succ b ↔ x ∈ (Ico a b).erase a
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b : ℕ
h : a ≤ b
⊢ Ico a b.succ = insert b (Ico a b)

Tactic:
ext x

Goal state after:
a b : ℕ
h : a ≤ b
x : ℕ
⊢ x ∈ Ico a b.succ ↔ x ∈ insert b (Ico a b)
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: n a : ℕ
⊢ Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))

Tactic:
induction n with
  | zero =>
    simp only [zero_add, Ico_zero_eq_range]
    rintro k hk l hl (hkl : k % a = l % a)
    simp only [Finset.mem_range, Finset.mem_coe] at hk hl
    rwa [mod_eq_of_lt hk, mod_eq_of_lt hl] at hkl
  | succ n ih =>
    rw [Ico_succ_left_eq_erase_Ico, succ_add, succ_eq_add_one,
      Ico_succ_right_eq_insert_Ico (by lia)]
    rintro k hk l hl (hkl : k % a = l % a)
    have ha : 0 < a := Nat.pos_iff_ne_zero.2 <| by rintro rfl; simp at hk
    simp only [Finset.mem_coe, Finset.mem_insert, Finset.mem_erase] at hk hl
    rcases hk with ⟨hkn, rfl | hk⟩ <;> rcases hl with ⟨hln, rfl | hl⟩
    · rfl
    · rw [add_mod_right] at hkl
      refine (hln <| ih hl ?_ hkl.symm).elim
      simpa using Nat.lt_add_of_pos_right (n := n) ha
    · rw [add_mod_right] at hkl
      suffices k = n by contradiction
      refine ih hk ?_ hkl
      simpa using Nat.lt_add_of_pos_right (n := n) ha
    · refine ih ?_ ?_ hkl <;> simp only [Finset.mem_coe, hk, hl]

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

Goal state after:
a b x : ℕ
⊢ x ∈ (range' a b).toFinset ↔ x ∈ Ico a (a + b)
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a : ℕ
⊢ (range' 1 a).toFinset = Icc 1 a

Tactic:
ext x

Goal state after:
a x : ℕ
⊢ x ∈ (range' 1 a).toFinset ↔ x ∈ Icc 1 a
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a : ℕ
⊢ (range a).toFinset = Finset.range a

Tactic:
ext x

Goal state after:
a x : ℕ
⊢ x ∈ (range a).toFinset ↔ x ∈ Finset.range a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ (Ico a b).Nonempty ↔ a < b

Tactic:
by
  rw [← coe_nonempty, coe_Ico, Set.nonempty_Ico]

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

Goal state before:
pp: a b : ℕ
⊢ image (⇑(addLeftEmbedding a)) (Ico 0 b) = Ico a (a + b)

Tactic:
ext x

Goal state after:
a b x : ℕ
⊢ x ∈ image (⇑(addLeftEmbedding a)) (Ico 0 b) ↔ x ∈ Ico a (a + b)
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ P n

Tactic:
apply Nat.decreasing_induction_of_not_bddAbove (P := fun n ↦ ∀ m ≥ n, P m) _ _ n n le_rfl

Goal state after:
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ ∀ (n : ℕ), (∀ m ≥ n + 1, P m) → ∀ m ≥ n, P m

P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ ¬BddAbove {x | ∀ m ≥ x, P m}
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
simp only [mem_Icc, true_and, le_rfl]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inl
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : { x // x ∈ {b | ReflTransGen r b a} }
h' : a = ↑b
⊢ Acc (TransGen r) ↑b

pp: case inr
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : { x // x ∈ {b | ReflTransGen r b a} }
h' : TransGen r (↑b) a
⊢ Acc (TransGen r) ↑b

Tactic:
· rwa [h'] at h

Goal state after:
case inr
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : { x // x ∈ {b | ReflTransGen r b a} }
h' : TransGen r (↑b) a
⊢ Acc (TransGen r) ↑b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : { x // x ∈ {b | ReflTransGen r b a} }
h' : TransGen r (↑b) a
⊢ Acc (TransGen r) ↑b

Tactic:
exact h.inv h'

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
⊢ WellQuasiOrdered r ↔ WellQuasiOrdered s

Tactic:
by
  apply (Equiv.arrowCongr (.refl ℕ) f).forall_congr
  congr! with g a b
  simp [f.map_rel_iff]

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h : a < b
⊢ Iio a ⊂ Iio b

Tactic:
by
  simpa [← coe_ssubset] using Set.Iio_ssubset_Iio h

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:
ext x

Goal state after:
N : Type u_7
inst✝ : CommMonoid N
H K : Submonoid N
x : N
⊢ x ∈ ↑(H ⊔ K) ↔ x ∈ ↑H * ↑K
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
simp [uIcc]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ f, IsBadSeq r s f) → ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
rintro ⟨f0, hf0 : IsBadSeq r s f0⟩

Goal state after:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
⊢ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ Set.univ = ⋃ x, x.orbit

Tactic:
ext x

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : α
⊢ x ∈ Set.univ ↔ x ∈ ⋃ x, x.orbit
Module: Mathlib.Order.WellFoundedSet

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

Tactic:
iff_forall_not_isBadSeq,

Goal state after:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∀ (f : ℕ → α), ¬IsBadSeq r s f) ↔ ¬∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f