mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (j.predAbove i).predAbove (i.succAbove j) = j

Tactic:
predAbove_of_le_castSucc _ _ h,

Goal state after:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.castPred ⋯).predAbove (i.succAbove j) = j
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
⊢ WellFounded r

Tactic:
by
  classical
  cases nonempty_fintype α
  have (x y) (hxy : r x y) : #{z | r z x} < #{z | r z y} :=
    Finset.card_lt_card <| by
      simp_rw [lt_iff_le_not_ge, Finset.subset_iff, mem_filter_univ]
      exact
        ⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
  exact Subrelation.wf (this _ _) (measure _).wf

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
⊢ ∃ n < #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s

Tactic:
have hg : Antitone g := antitone_nat_of_succ_le <| fun i ↦ by
    simp_rw [g, Function.iterate_succ, ← image_image]
    grw [hs.finsetImage_subset]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
⊢ ∃ n < #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin 1), append x x₀ (natAdd n i) = snoc x (x₀ 0) (natAdd n i)

Tactic:
intro i
    rw [Subsingleton.elim i 0, Fin.append_right]
    exact (@snoc_last _ (fun _ => α) _ _).symm

Goal state after:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : card α ≤ 1
⊢ False

Tactic:
← ha

Goal state after:
α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ False
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
h : Fintype ℕ
⊢ False

Tactic:
exact (Finset.range _).card_le_univ.not_gt ((Nat.lt_succ_self _).trans_eq (card_range _).symm)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c ≥ fold min b f s ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c

Tactic:
apply fold_op_rel_iff_or

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x ≥ min y z ↔ x ≥ y ∨ x ≥ z
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c > fold min b f s ↔ b < c ∨ ∃ x ∈ s, f x < c

Tactic:
apply fold_op_rel_iff_or

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x > min y z ↔ x > y ∨ x > z
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : l.length = 0
⊢ l.rotate n = l.rotate' n

Tactic:
simp_all [length_eq_zero_iff]

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

Goal state before:
pp: α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
⊢ n % l.length + m < l.length + l.length

Tactic:
exact Nat.add_lt_add hlt hml

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

Goal state before:
pp: α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l).bind fun a ↦ ↑(f a)) = ↑(List.flatMap f l)

Tactic:
rw [List.flatMap, ← coe_join, List.map_map]

Goal state after:
α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l).bind fun a ↦ ↑(f a)) = (↑(List.map (ofList ∘ f) l)).join
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l).bind fun a ↦ ↑(f a)) = ↑(List.flatMap f l)

Tactic:
rw [List.flatMap, ← coe_join, List.map_map]
  rfl

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h j h_1, i ≠ j ∧ l[i] = x ∧ l[j] = y) ↔ x ∈ l ∧ y ∈ l ∧ x ≠ y

Tactic:
mem_iff_getElem,

Goal state after:
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h j h_1, i ≠ j ∧ l[i] = x ∧ l[j] = y) ↔ (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ x ≠ y
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1) * n.choose k = (n.choose k + n.choose (k + 1)) * (k + 1)

Tactic:
← choose_succ_succ,

Goal state after:
n k : ℕ
⊢ (n + 1) * n.choose k = n.succ.choose k.succ * (k + 1)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
by_cases hm : m = 0

Goal state after:
case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp.inl
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

Tactic:
exact hs.pow

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
s : Set (α → β)
t : Set α
⊢ f '' s.seq t = ((fun x ↦ f ∘ x) '' s).seq t

Tactic:
simp only [seq, image_image2, image2_image_left, comp_apply]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type u_5
inst✝² : Group N
P : Type u_6
inst✝¹ : Group P
H : Subgroup G
f : G →* G'
inst✝ : IsMulCommutative ↥H
⊢ IsMulCommutative ↥(map f H)

Tactic:
by
  refine .of_setLike_mul_comm ?_
  rintro - ⟨a, ha, rfl⟩ - ⟨b, hb, rfl⟩
  simpa [map_mul] using congr(f $(setLike_mul_comm ha hb))

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_7
inst✝ : Group N
f : G →* N
⊢ ↑f.range = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
coe_range,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_7
inst✝ : Group N
f : G →* N
⊢ Set.range ⇑f = ↑⊤ ↔ Set.range ⇑f = Set.univ
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ ↑H ∩ Set.range ⇑f = ↑f.range ∩ ↑H

Tactic:
coe_range,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ ↑H ∩ Set.range ⇑f = Set.range ⇑f ∩ ↑H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_5
inst✝ : CommGroup G
s : Set G
⊢ normalizer s = ⊤

Tactic:
ext
  simp [mem_set_normalizer_iff]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: M : Type u_5
ι : Type u_6
α : ι → Type u_7
inst✝¹ : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
c : M
hc : IsUnit c
I : Set ι
s : (i : ι) → Set (α i)
⊢ c • I.pi s = I.pi (c • s)

Tactic:
lift c to Mˣ using hc

Goal state after:
M : Type u_5
ι : Type u_6
α : ι → Type u_7
inst✝¹ : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
I : Set ι
s : (i : ι) → Set (α i)
c : Mˣ
⊢ ↑c • I.pi s = I.pi (↑c • s)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G ≃* G'
H : Subgroup G
⊢ (map (↑f) H).Normal ↔ H.Normal

Tactic:
map_equiv_eq_comap_symm,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G ≃* G'
H : Subgroup G
⊢ (comap (↑f.symm) H).Normal ↔ H.Normal
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : CommGroup β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
x : α × β
s : Set α
f : F
⊢ x • graphOn (⇑f) s = graphOn (fun a ↦ x.2 / f x.1 * f a) (x.1 • s)

Tactic:
ext ⟨a, b⟩

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : CommGroup β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
x : α × β
s : Set α
f : F
a : α
b : β
⊢ (a, b) ∈ x • graphOn (⇑f) s ↔ (a, b) ∈ graphOn (fun a ↦ x.2 / f x.1 * f a) (x.1 • s)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
⊢ g ∈ iInf a → ∀ (g_1 : G), g_1 * g * g_1⁻¹ ∈ iInf a

Tactic:
g_in_iInf

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : g ∈ iInf a
⊢ ∀ (g_1 : G), g_1 * g * g_1⁻¹ ∈ iInf a
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case left
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₁.toSubmonoid

Tactic:
suffices x * (y * x⁻¹ * y⁻¹) ∈ H₁ by simpa [mul_assoc]
    exact H₁.mul_mem hx (hH₁.conj_mem _ (H₁.inv_mem hx) _)

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : ∃ i, p i
S : ι → Submonoid M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ x ∈ ⨆ i, ⨆ (_ : p i), S i ↔ ∃ i, p i ∧ x ∈ S i

Tactic:
rw [← nonempty_subtype] at hp

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
ι : Type u_4
p : ι → Prop
hp : Nonempty (Subtype p)
S : ι → Submonoid M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ x ∈ ⨆ i, ⨆ (_ : p i), S i ↔ ∃ i, p i ∧ x ∈ S i
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case append_singleton.none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c ↦ if r a c then some a else some c
hf : foldl (argAux r) o tl = none
⊢ ¬r b m

pp: case append_singleton.some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c ↦ if r a c then some a else some c
c : α
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m

Tactic:
· rw [hf] at ho
    rw [foldl_argAux_eq_none] at hf
    simp_all [hf.1, hf.2, hr₀.irrefl _]

Goal state after:
case append_singleton.some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c ↦ if r a c then some a else some c
c : α
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
x : α ⊕ β
⊢ x ∈ map inl s + map inr t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x

Tactic:
mem_add,

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
x : α ⊕ β
⊢ x ∈ map inl s ∨ x ∈ map inr t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ (s.disjSum t).Nodup

Tactic:
refine ((hs.map inl_injective).add_iff <| ht.map inr_injective).2 ?_

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ Disjoint (Multiset.map inl s) (Multiset.map inr t)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case swap
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ powersetAux' (b :: a :: l✝) ~ powersetAux' (a :: b :: l✝)

Tactic:
| swap a b =>

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

Goal state before:
pp: case nil
α : Type u
⊢ map pure [] <+ [].sublists

Tactic:
simp only [map, map_append, sublists_concat]

Goal state after:
case nil
α : Type u
⊢ [] <+ [].sublists
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case append_singleton
α : Type u
l✝ : List α
a✝¹ : α
a✝ : map pure l✝ <+ l✝.sublists
⊢ map pure (l✝ ++ [a✝¹]) <+ (l✝ ++ [a✝¹]).sublists

Tactic:
simp only [map, map_append, sublists_concat]

Goal state after:
case append_singleton
α : Type u
l✝ : List α
a✝¹ : α
a✝ : map pure l✝ <+ l✝.sublists
⊢ map pure l✝ ++ [pure a✝¹] <+ l✝.sublists ++ map (fun x ↦ x ++ [a✝¹]) l✝.sublists
Module: Mathlib.Data.Multiset.Powerset

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

Tactic:
| swap a b =>

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

Goal state before:
pp: α : Type u
l : List α
⊢ (finRange l.length).sublists ~ (finRange l.length).sublists'

Tactic:
apply (perm_ext_iff_of_nodup _ _).mpr

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

α : 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 α
⊢ (finRange l.length).sublists'.Nodup

Tactic:
exact (nodup_sublists'.mpr (nodup_finRange _))

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

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x ↦ x.sup f, ¬(fun x ↦ x.sup f) t < x
a : α
this : ¬(fun x ↦ x.sup f) t < f a ⊔ t.sup f
⊢ f a ≤ t.sup f

Tactic:
right_lt_sup,

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x ↦ x.sup f, ¬(fun x ↦ x.sup f) t < x
a : α
this : ¬¬f a ≤ (fun x ↦ x.sup f) t
⊢ f a ≤ t.sup f
Module: Mathlib.Data.Finset.Lattice.Fold

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

Tactic:
by
  induction hs using Finset.Nonempty.cons_induction with
  | singleton => simp
  | cons _ _ _ hs ih => simp_rw [sup'_cons hs, inf_sup_left, ih]

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

Goal state before:
pp: case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ (∀ x ∈ s, f x < a) → ⨆ i ∈ s, f i < a

Tactic:
have := hs.ciSup_mem_image _ h

Goal state after:
case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
this : ⨆ i ∈ s, f i ∈ f '' s
⊢ (∀ x ∈ s, f x < a) → ⨆ i ∈ s, f i < a
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: case insert
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : Nonempty α
I : Set β
S : β → Set α
a✝¹ : β
s✝ : Set β
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
hs : BddAbove (⋃ i ∈ s✝, S i) ↔ ∀ i ∈ s✝, BddAbove (S i)
⊢ BddAbove (⋃ i ∈ insert a✝¹ s✝, S i) ↔ ∀ i ∈ insert a✝¹ s✝, BddAbove (S i)

Tactic:
simp only [biUnion_insert, forall_mem_insert, bddAbove_union, hs]

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:
rcases s.eq_empty_or_nonempty with (rfl | hs)

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
⊢ ⨆ i ∈ f '' ∅, g i = ⨆ x ∈ ∅, g (f x)

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
⊢ ⨆ i ∈ f '' s, g i = ⨆ x ∈ s, g (f x)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
· cases isEmpty_or_nonempty ι <;>
      simp [h, iSup_of_empty', ciSup_const]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
x y : α
⊢ y = x ∨ x ⋖ y ↔ ReflGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
reflGen_iff

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case refine_2.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ : β
h : a₁ ⩿ a₂
⊢ (a₁, b₁) ⩿ (a₂, b₁)

pp: case refine_2.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⩿ b₂
⊢ (a₁, b₁) ⩿ (a₁, b₂)

Tactic:
· exact mk_wcovBy_mk_iff_left.2 h

Goal state after:
case refine_2.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⩿ b₂
⊢ (a₁, b₁) ⩿ (a₁, b₂)
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Ioc a a = 0

Tactic:
by rw [Ioc, Finset.Ioc_self, Finset.empty_val]

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

Goal state before:
pp: case inl
m : ℕ
hm : m < sInf ∅
⊢ m ∉ ∅

Tactic:
apply notMem_empty

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

Goal state before:
pp: a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ c - a_1 = x) ↔ c + 1 - b ≤ x ∧ x < c + 1 - a

Tactic:
refine ⟨?_, fun h ↦ ⟨c - x, by lia⟩⟩

Goal state after:
a b c : ℕ
hac : a ≤ c
x : ℕ
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ c - a_1 = x) → c + 1 - b ≤ x ∧ x < c + 1 - a
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
⊢ univ.WellFoundedOn r ↔ WellFounded r

Tactic:
simp [wellFoundedOn_iff]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c ↦ ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ Acc (Subrel r fun x ↦ x ∈ range f) ⟨f c, ⋯⟩

Tactic:
refine Acc.of_downward_closed f' ?_ _ ?_

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c ↦ ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ ∀ {a : β} {b : ↑(range f)}, Subrel r (fun x ↦ x ∈ range f) b (f' a) → ∃ c, f' c = b

case refine_2
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c ↦ ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ Acc (InvImage (Subrel r fun x ↦ x ∈ range f) f') c
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
by
  rw [← coe_eq_singleton, coe_Icc, Set.Icc_eq_singleton_iff]

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

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

Tactic:
by
  simpa only [coe_Iio] using! (Finset.Iio y).finite_toSet

Goal state after:
Module: Mathlib.Order.WellFoundedSet

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

Tactic:
use PartiallyWellOrderedOn.exists_monotone_subseq

Goal state after:
case mpr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
⊢ (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))) → s.PartiallyWellOrderedOn r
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 α
H : Subgroup G
x : α
a b : ↑(orbit G x)
h : a ∈ orbit (↥H) b
⊢ ↑a ∈ orbit ↥H ↑b

Tactic:
rcases h with ⟨g, rfl⟩
    exact MulAction.mem_orbit _ g

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:
rw [Finset.ext_iff] at h

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.GroupTheory.GroupAction.Defs

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
h : a ∈ MulAction.orbit (↥H) b
⊢ ↑a ∈ MulAction.orbit ↥H ↑b

Tactic:
rcases h with ⟨g, rfl⟩
    exact MulAction.mem_orbit _ g

Goal state after:
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:
rw [iff_forall_not_isBadSeq, ← not_exists, not_congr]
  constructor
  · apply exists_min_bad_of_exists_bad
  · rintro ⟨f, hf1, -⟩
    exact ⟨f, hf1⟩

Goal state after: