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

Goal state before:
pp: case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := ⋯
⊢ Set.InjOn f' ↑s

Tactic:
intro a₁ ha₁ a₂ ha₂ haa

Goal state after:
case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a ↦ ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ ↑s
a₂ : α
ha₂ : a₂ ∈ ↑s
haa : f' a₁ = f' a₂
⊢ a₁ = a₂
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
⊢ #s ≤ #t

Tactic:
let f' : α → β := fun a => f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩)
    apply card_le_card_of_injOn f'
    · aesop (add safe unfold Set.MapsTo)
    · intro a₁ ha₁ a₂ ha₂ haa
      rw [mem_coe] at ha₁ ha₂
      simp only [f', ha₁, ha₂, ← Subtype.ext_iff] at haa
      exact Subtype.ext_iff.mp (hf haa)

Goal state after:
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
hkb : k < ↑b
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

Tactic:
refine ⟨⟨k, hkb.trans b.is_lt⟩, hkb, by fin_omega, ?_⟩

Goal state after:
case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
hkb : k < ↑b
⊢ b = a + ⟨k, ⋯⟩ + 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
x✝ : Fin n
⊢ ↑((last n).succAbove x✝) = ↑x✝.castSucc

Tactic:
simp only [succAbove_of_castSucc_lt, castSucc_lt_last]

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

Goal state before:
pp: a b : Fin 2
⊢ a = b → (a = 0 ↔ b = 0)

Tactic:
rintro rfl; rfl

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p i : Fin n
h : p ≤ i
⊢ p.predAbove (p.castSucc.succAbove i) = i

Tactic:
rw [succAbove_castSucc_of_le _ _ h, predAbove_succ_of_le _ _ h]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #s + #sᶜ = Fintype.card α

Tactic:
Finset.card_compl,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #s + (Fintype.card α - #s) = Fintype.card α
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mpr
α : Type u_1
s : Finset α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ ∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}

Tactic:
exact ⟨a, b, c, {a, b, c}, by simp_all [insert_subset_iff]⟩

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ t ⊆ s, #t = 4) ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
card_eq_four,

Goal state after:
α : Type u_1
s : Finset α
⊢ (∃ t ⊆ s, ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ t = {x, y, z, w}) ↔
    ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ #{x | p x}.toFinsetᶜ = card α - card { x // p x }

pp: case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x

Tactic:
Finset.card_compl,

Goal state after:
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ card α - #{x | p x}.toFinset = card α - card { x // p x }

case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ univ = {x}

Tactic:
by
  symm
  apply eq_of_subset_of_card_le (subset_univ {x})
  simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b : α
⊢ a = b

Tactic:
by
      let ⟨x, hx⟩ := card_eq_one_iff.1 ha.symm
      rw [hx a, hx b]

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

Goal state before:
pp: case cons.hl₁
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ insertionSort r xs → (r a x ↔ s (f a) (f x))

Tactic:
simpa only [mem_insertionSort] using hl.2.1

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
⊢ Pairwise r (List.orderedInsert r a (b :: l))

Tactic:
(«tacticBy_cases_:_»
 "by_cases"
 [`h' ":"]
 (choice
  (_private.Mathlib.Data.List.Sort.0.List.«term_≼__1» `a "≼" `b)
  (_private.Mathlib.Data.List.Sort.0.List.«term_≼_» `a "≼" `b)))

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : r a b
⊢ Pairwise r (List.orderedInsert r a (b :: l))

case neg
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
⊢ Pairwise r (List.orderedInsert r a (b :: l))
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: ι : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Multiset ι
r : M → N → Prop
f : ι → M
g : ι → N
h₁ : r 1 1
h₂ : ∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a * b) (g a * c)
l : List ι
⊢ r (map f ⟦l⟧).prod (map g ⟦l⟧).prod

Tactic:
by
    simp only [l.prod_hom_rel h₁ h₂, quot_mk_to_coe, map_coe, prod_coe]

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

Goal state before:
pp: α : Type u
l : List α
⊢ [] ~r l ↔ [] = l

Tactic:
by
  rw [isRotated_comm, isRotated_nil_iff, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ (↑l₁).product ↑l₂ = ↑(l₁.product l₂)

Tactic:
product,

Goal state after:
α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ ((↑l₁).bind fun a ↦ map (Prod.mk a) ↑l₂) = ↑(l₁.product l₂)
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty

Tactic:
simp only [Finset.Nonempty, mem_biUnion]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (∃ x, ∃ a ∈ s, x ∈ t a) ↔ ∃ x ∈ s, ∃ x_1, x_1 ∈ t x
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
h : 0 < (n - k)! * (k - s)! * s !
⊢ n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) =
    n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !)

Tactic:
by
      grind

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
by rw [choose_succ_succ, choose_succ_self_right n, choose_self]

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
⊢ iUnion (Fin.cons s f) = s ∪ ⋃ i, f i

Tactic:
by
  ext
  simp [Fin.exists_iff_succ]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 2 (k + 1) = k + 1 + 1

Tactic:
rw [multichoose, IH]

Goal state after:
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (k + 1) = k + 1 + 1
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ f ∈ (a ::ₘ m).pi t ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1

Tactic:
pi_cons,

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (f ∈ (t a).bind fun b ↦ map (Pi.cons m a b) (m.pi t)) ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ f x ∈ iUnion U

Tactic:
rw [hU]

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ f x ∈ univ
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ x ∈ iUnion U

Tactic:
rw [hU]

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ x ∈ univ
Module: Mathlib.Algebra.Group.Submonoid.Defs

Goal state before:
pp: M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ x ^ 0 ∈ S

Tactic:
by
    rw [pow_zero]
    exact OneMemClass.one_mem S

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = image2 (fun f a ↦ f a) (Prod.mk '' s) t

Tactic:
image2_image_left,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = image2 (fun a b ↦ (a, b)) s t
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ closure (insert 1 s) = closure s

Tactic:
rw [insert_eq, closure_union, sup_eq_right, closure_singleton_le_iff_mem]

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ 1 ∈ closure s
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
M : Type u_7
inst✝ : MulOneClass M
f : G →* G'
g : G' →* M
⊢ g.comp f = 1 → f.range ≤ g.ker

Tactic:
rintro h _ ⟨y, rfl⟩; exact DFunLike.congr_fun h y

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ map f H = ⊥ ↔ H = ⊥

Tactic:
by rw [map_eq_bot_iff, f.ker_eq_bot hf, le_bot_iff]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
Hs : Set (Subgroup G)
h : ∀ H ∈ Hs, H.Characteristic
⊢ (sSup Hs).Characteristic

Tactic:
simp [sSup_eq_iSup', characteristic_iSup, h]

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

Goal state before:
pp: case refine_3
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
s : Set G
n : G
h : n ∈ normalClosure s
g x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * (x * y) * g⁻¹ ∈ normalClosure s

Tactic:
← conj_mul

Goal state after:
case refine_3
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
s : Set G
n : G
h : n ∈ normalClosure s
g x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * x * g⁻¹ * (g * y * g⁻¹) ∈ normalClosure s
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s t : Set α
⊢ image2 (fun x1 x2 ↦ x1 • x2) (op '' s) t = image2 (fun x1 x2 ↦ x1 * x2) t s

Tactic:
image2_image_left,

Goal state after:
α : Type u_2
inst✝ : Mul α
s t : Set α
⊢ image2 (fun a b ↦ op a • b) s t = image2 (fun x1 x2 ↦ x1 * x2) t s
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : Std.Irrefl r
inst✝ : ∀ (i : ι), Std.Irrefl (s i)
i✝ : ι
a : α i✝
ha : s i✝ a a
⊢ False

Tactic:
exact irrefl _ ha

Goal state after:
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: S : Set ℕ
⊢ S = Set.univ → 0 ∈ S ∧ ∀ (k : ℕ), k ∈ S → k + 1 ∈ S

Tactic:
by rintro rfl; simp

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

Goal state before:
pp: case bot
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
l : List α
a : α
ha : a ∈ l
h : l.maximum = ⊥
⊢ ¬⊥ < ↑a

Tactic:
simp_all [not_maximum_lt_of_mem ha]

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

Goal state before:
pp: case coe
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
l : List α
a : α
ha : a ∈ l
a✝ : α
h : l.maximum = ↑a✝
⊢ ¬↑a✝ < ↑a

Tactic:
simp_all [not_maximum_lt_of_mem ha]

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

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (powersetAux' l).zip (powersetAux' l).reverse
⊢ x.1 + x.2 = ↑l

Tactic:
powersetAux',

Goal state after:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (List.map ofList l.sublists').zip (List.map ofList l.sublists').reverse
⊢ x.1 + x.2 = ↑l
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (↑l).dedup = (Multiset.map id (↑l).dedup).sup

Tactic:
Multiset.map_id

Goal state after:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (↑l).dedup = (↑l).dedup.sup
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ powersetCard n s = ∅ ↔ #s < n

Tactic:
by
  refine ⟨?_, fun h ↦ card_eq_zero.1 <| by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]⟩
  contrapose!
  exact fun h ↦ (exists_subset_card_eq h).imp <| by simp

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

Goal state before:
pp: case empty
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ι → α
a : α
⊢ a ⊓ ⊥ = ⊥

Tactic:
inf_bot_eq

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

Goal state before:
pp: α : Type u_1
a b : Finset α
r : ℕ
hab : #a = #b
hr₀ : r ≠ 0
hra : r ≤ #a
h : powersetCard r a = powersetCard r b
⊢ a = b

Tactic:
by
  classical
  simpa [powersetCard_biUnion hr₀, ← hab, hra] using congr(($h).biUnion id)

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

Goal state before:
pp: case empty
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
hs : ∅.Nonempty
⊢ ∅.sup f ∈ f '' ↑∅

Tactic:
simp only [Finset.not_nonempty_empty] at hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Preorder β
f : β → α
a : β
hf : Monotone f
⊢ ⨆ x, f ↑x = f a

Tactic:
by
  have hd : Directed (· ≤ ·) (fun x : Iic a ↦ f x) := fun x y ↦ ⟨⟨a, le_refl a⟩, ⟨hf x.2, hf y.2⟩⟩
  have H : BddAbove (range fun x : Iic a ↦ f x) := ⟨f a, fun _ ↦ by aesop⟩
  apply (hd.le_ciSup H (⟨a, le_refl a⟩ : Iic a)).antisymm'
  rw [hd.ciSup_le_iff H]
  rintro ⟨a, h⟩
  exact hf h

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Finite ι
f : ι → Set α
inst✝ : ∀ (i : ι), Finite ↑(f i)
⊢ Finite ↑(⋃ i, f i)

Tactic:
by
  have : Fintype (PLift ι) := Fintype.ofFinite _
  have : ∀ i, Fintype (f i) := fun i => Fintype.ofFinite _
  classical apply (fintypeiUnion _).finite

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

Goal state before:
pp: α : Type u
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ i ∈ s, Finite ↑(t i)
⊢ Finite ↑(⋃ x ∈ s, t x)

Tactic:
rw [biUnion_eq_iUnion]

Goal state after:
α : Type u
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ i ∈ s, Finite ↑(t i)
⊢ Finite ↑(⋃ x, t ↑x)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
this : Finite ↑s
⊢ (⋃ i, ⋃ (h : i ∈ s), t i h).Finite

Tactic:
rw [biUnion_eq_iUnion]

Goal state after:
α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
this : Finite ↑s
⊢ (⋃ x, t ↑x ⋯).Finite
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ i ∈ a, s i).Infinite

Tactic:
rw [biUnion_eq_iUnion]

Goal state after:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ x, s ↑x).Infinite
Module: Mathlib.Order.Cover

Goal state before:
pp: case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t ⊆ s

Tactic:
← sdiff_singleton_eq_self h,

Goal state after:
case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t \ {x} ⊆ s
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
⊢ (t.preimage Subtype.val ⋯).sup id = ⟨t.sup id, ⋯⟩

Tactic:
let : OrderBot (Subtype P) := Subtype.orderBot Pbot

Goal state after:
α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot Pbot
⊢ (t.preimage Subtype.val ⋯).sup id = ⟨t.sup id, ⋯⟩
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s : Set ι
h : s.Finite
hs : s.Nonempty
⊢ ∃ i, MaximalFor (fun x ↦ x ∈ s) f i

Tactic:
lift s to Finset ι using h; exact s.exists_maximalFor f hs

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_1
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal P x
⊢ Q x

Tactic:
obtain ⟨y, hyx, hy⟩ := h h'.prop

Goal state after:
case refine_1
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal P x
y : α
hyx : y ≤ x
hy : Q y
⊢ Q x
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
⊢ f = g → Set.range ⇑f = Set.range ⇑g

Tactic:
rintro rfl; rfl

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α →o β
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ f = g → Set.range ⇑f = Set.range ⇑g

Tactic:
rintro rfl; rfl

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

Goal state before:
pp: case inl
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
hm : n ≥ n
⊢ P n

pp: case inr
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
hm✝ : m ≥ n
hm : n < m
⊢ P m

Tactic:
· exact step n ih

Goal state after:
case inr
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
hm✝ : m ≥ n
hm : n < m
⊢ P m
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r r' : α → α → Prop
s t : Set α
h : t.WellFoundedOn r'
hle : r ≤ r'
hst : s ⊆ t
⊢ s.WellFoundedOn r

Tactic:
rw [wellFoundedOn_iff] at *

Goal state after:
α : Type u_2
r r' : α → α → Prop
s t : Set α
h : WellFounded fun a b ↦ r' a b ∧ a ∈ t ∧ b ∈ t
hle : r ≤ r'
hst : s ⊆ t
⊢ WellFounded fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
rw [← coe_subset, coe_Icc, coe_Icc, Set.Icc_subset_Icc_iff h₁]

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ insert a (Ioi a) ↔ a✝ ∈ Ici a

Tactic:
Finset.mem_insert,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ = a ∨ a✝ ∈ Ioi a ↔ a✝ ∈ Ici a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ insert b (Iio b) ↔ a✝ ∈ Iic b

Tactic:
Finset.mem_insert,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ = b ∨ a✝ ∈ Iio b ↔ a✝ ∈ Iic b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz✝ : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : x < z
⊢ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
exact .tail (transGen_covBy_of_lt hxz) hzy

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:
← not_exists,

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

Goal state before:
pp: case inr
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
⊢ {l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)

Tactic:
iff_not_exists_isMinBadSeq List.length

Goal state after:
case inr
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
⊢ ¬∃ f,
      IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f ∧
        ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
S : Set G
x✝¹ : G
hx✝ : x✝¹ ∈ (closure S).toSubmonoid
x : G
x✝ : x ∈ closure S
hx : x ∈ Submonoid.closure (S ∪ S⁻¹)
⊢ x⁻¹ ∈ Submonoid.closure (S ∪ S⁻¹)

Tactic:
rwa [← Submonoid.mem_closure_inv, Set.union_inv, inv_inv, Set.union_comm]

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

Goal state before:
pp: case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (x✝ ∈ ↑A ∧ ∃ x ∈ ↑B, ∃ y ∈ ↑C, x * y = x✝) → ∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y ∈ ↑C, x * y = x✝

Tactic:
rintro ⟨hyz, y, hy, z, hz, rfl⟩

Goal state after:
case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ ↑B
z : G
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ ∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y_1 ∈ ↑C, x * y_1 = y * z
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Finset M
⊢ s.val.prod = (Multiset.map id s.val).prod

Tactic:
Multiset.map_id

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
s : Finset M
⊢ s.val.prod = s.val.prod