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

Goal state before:
pp: α : Type u
n : ℕ
f g : Fin n → α
h : ofFn f = ofFn g
⊢ f ≍ g

Tactic:
ofFn_inj'

Goal state after:
α : Type u
n : ℕ
f g : Fin n → α
h : ⟨n, f⟩ = ⟨n, g⟩
⊢ f ≍ g
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
hs : 1 < #s
a : α
⊢ ∃ b ∈ s, b ≠ a

Tactic:
have : Nonempty α := ⟨a⟩
  by_contra!
  exact hs.not_ge (card_le_one_iff_subset_singleton.2 ⟨a, subset_singleton_iff'.2 this⟩)

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
x✝ : ∃ a t, ∃ (h : a ∉ t), cons a t h = s ∧ #t = n
a : α
t : Finset α
w✝ : a ∉ t
hs : cons a t w✝ = s
right✝ : #t = n
⊢ #s = n + 1

Tactic:
by simpa [← hs]

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

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 2 → ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
rw [card_eq_succ]
    grind [card_eq_one]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑sᶜ
⊢ card ↑sᶜ = card α - card ↑s

Tactic:
← Set.toFinset_card,

Goal state after:
α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑sᶜ
⊢ #sᶜ.toFinset = card α - card ↑s
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑sᶜ
⊢ #sᶜ.toFinset = card α - card ↑s

Tactic:
← Set.toFinset_card,

Goal state after:
α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑sᶜ
⊢ #sᶜ.toFinset = card α - #s.toFinset
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ ((fun a ↦ p a) x ∧ ∀ (y : α), (fun a ↦ p a) y → y = x) ↔ {x | p x} = {x}

Tactic:
simp only [Subset.antisymm_iff, subset_singleton_iff', singleton_subset_iff, and_comm,
    mem_filter_univ]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ Fintype.card ↑s = Fintype.card α ↔ s = Set.univ

Tactic:
← Set.toFinset_card,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ #s.toFinset = Fintype.card α ↔ s = Set.univ
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ l
h : l <+ l'
⊢ x ∈+ l'

Tactic:
by
  induction h with
  | slnil => exact hx
  | cons y _ IH => exact (IH hx).duplicate_cons _
  | cons_cons y h IH =>
    rw [duplicate_cons_iff] at hx ⊢
    rcases hx with (⟨rfl, hx⟩ | hx)
    · simp [h.subset hx]
    · simp [IH hx]

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

Goal state before:
pp: m n : ℕ
α : Fin (n + 1) → Sort u_1
x✝ : α (last n)
q : (i : Fin (n + 1)) → α i
p✝ : (i : Fin n) → α i.castSucc
i✝ : Fin n
y : α i✝.castSucc
z : α (last n)
p : (i : Fin n) → α i.castSucc
x : α (last n)
i : Fin (n + 1)
h : ↑i < n
⊢ α (i.castLT h).castSucc = α i

Tactic:
rw [Fin.castSucc_castLT i h]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
⊢ snoc (update p i y) x j = update (snoc p x) i.castSucc y j

Tactic:
cases j using lastCases with
  | cast j => rcases eq_or_ne j i with rfl | hne <;> simp [*]
  | last => simp [Ne.symm]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hs : s ⊆ range f
⊢ s.Finite

Tactic:
← image_preimage_eq_of_subset hs

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hs : s ⊆ range f
⊢ (f '' f ⁻¹' s).Finite
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
⊢ IsChain R (a :: l) ↔ l = [] ∨ Forall₂ R (a :: l.dropLast) l

Tactic:
cases l <;> simp [isChain_iff_forall₂]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l l₁ : List α
h : IsChain R l
h' : l₁ <:+: l
⊢ IsChain R l₁

Tactic:
rcases h' with ⟨l₂, l₃, rfl⟩

Goal state after:
α : Type u_1
R : α → α → Prop
l₁ l₂ l₃ : List α
h : IsChain R (l₂ ++ l₁ ++ l₃)
⊢ IsChain R l₁
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Tactic:
rcases l.length.zero_le.eq_or_lt with hl | hl
  · simp [eq_nil_of_length_eq_zero hl.symm]
  rw [← rotate_eq_drop_append_take (n.mod_lt hl).le, rotate_mod]

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

Goal state before:
pp: α : Type u
l : List α
⊢ some (l.cyclicPermutations.head ⋯) = some l

Tactic:
head_cyclicPermutations

Goal state after:
α : Type u
l : List α
⊢ some l = some l
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
inst✝ : DecidableEq β
f : α → Finset β
⊢ (s.attach.biUnion fun x ↦ f ↑x) = s.biUnion f

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : ↥s → Finset β
⊢ s.attach.biUnion f = s.biUnion fun a ↦ if h : a ∈ s then f ⟨a, h⟩ else ∅

Tactic:
by aesop

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

Goal state before:
pp: n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ (n + 1).choose (k + 1) = 0

Tactic:
rw [choose_succ_succ, choose_eq_zero_of_lt hnk, choose_eq_zero_of_lt hnk1]

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

Goal state before:
pp: m : ℕ
⊢ 1 + 2 * m = 1 + (m + m)

Tactic:
Nat.two_mul m

Goal state after:
m : ℕ
⊢ 1 + (m + m) = 1 + (m + m)
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
x : δ a
h : x ∈ t a
f : (b : α) → a ≠ b → δ b
hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b
⊢ (fun b ↦ if h : a = b then h ▸ x else f b h) ∈ piFinset t

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : DecidableEq (ι → α)
s : Finset α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ {f ∈ Fintype.piFinset fun x ↦ s | ∃ a ∈ s, const ι a = f} = s.piDiag ι

Tactic:
by aesop

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

Goal state before:
pp: case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
⊢ ∀ (i_1 : ι), update z i y i_1 ∈ v i_1

Tactic:
@forall_update_iff ι α _ z i y fun i t => t ∈ v i

Goal state after:
case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
⊢ y ∈ v i ∧ ∀ (x : ι), x ≠ i → z x ∈ v x
Module: Mathlib.Algebra.Group.Submonoid.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
s : Set M
inst✝ : MulOneClass N
f g : M →* N
⊢ 1 ∈ {x | f x = g x}

Tactic:
rw [Set.mem_ofPred_eq, f.map_one, g.map_one]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s / t) = s / t

Tactic:
image_preimage_eq_iff.2 (div_subset_range m hs ht)

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ s / t = s / t
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
y : G
hy : y ∈ H
⊢ y = 1

Tactic:
← Subgroup.coe_mk H y hy,

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
y : G
hy : y ∈ H
⊢ ↑⟨y, hy⟩ = 1
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
N : Type u_7
inst✝ : Group N
f : G →* N
H : Subgroup N
a : G
ha : a ∈ ⇑f ⁻¹' ↑H
⊢ f a⁻¹ ∈ H

Tactic:
f.map_inv

Goal state after:
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
N : Type u_7
inst✝ : Group N
f : G →* N
H : Subgroup N
a : G
ha : a ∈ ⇑f ⁻¹' ↑H
⊢ (f a)⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
x : N
⊢ x ∈ range 1 ↔ x ∈ ⊥

Tactic:
by simpa using @comm _ (· = ·) _ 1 x

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

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
H : (↑e).comp (powMonoidHom n) = (powMonoidHom n).comp ↑e
⊢ Subgroup.map (↑e) (powMonoidHom n).range = (powMonoidHom n).range

Tactic:
map_range,

Goal state after:
M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
H : (↑e).comp (powMonoidHom n) = (powMonoidHom n).comp ↑e
⊢ ((↑e).comp (powMonoidHom n)).range = (powMonoidHom n).range
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ pair a₁ b < pair a₂ b

Tactic:
simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]

Goal state after:
case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ pair a₁ b < pair a₂ b

Tactic:
simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]

Goal state after:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ pair a b₁ < pair a b₂

Tactic:
simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]

Goal state after:
case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
⊢ r (f (Directed.sequence f hf n)) (f (Directed.sequence f hf (n + 1)))

Tactic:
by
  dsimp [Directed.sequence]
  generalize hf.sequence f n = p
  rcases (decode n : Option α) with - | a
  · exact (Classical.choose_spec (hf p p)).1
  · exact (Classical.choose_spec (hf p a)).1

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H ≤ H

Tactic:
by
  simp_rw [map_equiv_eq_comap_symm']
  exact characteristic_iff_comap_le.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

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

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
inst✝¹ : H.Characteristic
inst✝ : K.Characteristic
⊢ (H ⊓ K).Characteristic

Tactic:
simp_all [characteristic_iff_comap_eq, comap_inf]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ a ∈ H

Tactic:
rw [← mul_one a, ← inv_one, ← one_mul a]
  exact h 1

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
g : G
⊢ H.normalCore ≤ map (↑(MulAut.conj g)) H

pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H.normalCore

Tactic:
· grw [← Normal.map_conj_eq H.normalCore g, normalCore_le]

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H.normalCore
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
⊢ ∃ n, ¬p n ∧ p (n + 1)

Tactic:
suffices 0 < k from
    ⟨k - 1, Nat.find_min H <| Nat.pred_lt this.ne', by rwa [Nat.sub_add_cancel this]⟩

Goal state after:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
⊢ 0 < k
Module: Mathlib.Data.List.Zip

Goal state before:
pp: 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

pp: 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)

Tactic:
· rintro (⟨rfl, rfl⟩ | ⟨_, _, h, rfl, rfl⟩)
      · simp
      · simp [ih.mp h]

Goal state after:
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
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun l ↦ [l, a :: l]) r
⊢ sublistsAux a (r ++ [l]) = flatMap (fun l ↦ [l, a :: l]) (r ++ [l])

Tactic:
rw [flatMap_append, ← ih, flatMap_singleton, sublistsAux, foldl_append]

Goal state after:
α : Type u
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun l ↦ [l, a :: l]) r
⊢ foldl (fun r l ↦ r ++ [l, a :: l]) (foldl (fun r l ↦ r ++ [l, a :: l]) [] r) [l] = sublistsAux a r ++ [l, a :: l]
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
h✝ : l.Nodup
l₁ l₂ : List α
h : ((Lex fun x1 x2 ↦ x1 ≠ x2) on reverse) l₁ l₂
⊢ l₁ ≠ l₂

Tactic:
by simpa using h.to_ne

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

Goal state before:
pp: α : Type u
n : ℕ
l : List α
h : l.Nodup
⊢ (sublistsLen n l).Nodup

Tactic:
have : Pairwise (· ≠ ·) l.sublists' := Pairwise.imp
    (fun h => Lex.to_ne (by convert! h using 3; simp [eq_comm])) h.sublists'
  exact this.sublist (sublistsLen_sublist_sublists' _ _)

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x ↦ [x, f a :: x]) (map f l).sublists = map (map f) (a :: l).sublists

Tactic:
sublists_map f l,

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x ↦ [x, f a :: x]) (map (map f) l.sublists) = map (map f) (a :: l).sublists
Module: Mathlib.Data.Set.Finite.Range

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
this : Finite ↑u
g : ⦃a : β⦄ → a ∈ u → α
hg : ∀ ⦃a : β⦄ (a_1 : a ∈ u), g a_1 ∈ s
hg' : ∀ ⦃a : β⦄ (a_1 : a ∈ u), f (g a_1) = a
g' : ↑u → α := fun x ↦ g ⋯
a : α
ha : a ∈ range g'
⊢ a ∈ s

Tactic:
by aesop

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
this : Finite ↑u
g : ⦃a : β⦄ → a ∈ u → α
hg : ∀ ⦃a : β⦄ (a_1 : a ∈ u), g a_1 ∈ s
hg' : ∀ ⦃a : β⦄ (a_1 : a ∈ u), f (g a_1) = a
g' : ↑u → α := fun x ↦ g ⋯
⊢ f '' range g' = u

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset α
f : α → β
⊢ s.sup f = sSup (f '' ↑s)

Tactic:
classical rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ powersetCard n.succ (insert x s) = powersetCard n.succ s ∪ image (insert x) (powersetCard n s)

Tactic:
rw [powersetCard_eq_filter, powerset_insert, filter_union, ← powersetCard_eq_filter]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ powersetCard n.succ s ∪ {x ∈ image (insert x) s.powerset | #x = n.succ} =
    powersetCard n.succ s ∪ image (insert x) (powersetCard n s)
Module: Mathlib.Data.Finset.Lattice.Fold

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

Tactic:
rw [sup_cons, sup_cons, inf_sup_left, h]

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
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ f ↑x
x✝ : α
⊢ (x✝ ∈ range fun x ↦ f ↑x) → x✝ ≤ f a

Tactic:
by aesop

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
himage : (f '' s).Finite
hfibers : ∀ x ∈ f '' s, (s ∩ f ⁻¹' {x}).Finite
x : α
⊢ x ∈ s → x ∈ ⋃ i ∈ f '' s, s ∩ f ⁻¹' {i}

Tactic:
by aesop

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

Goal state before:
pp: α : Type u
ι : Type v
κ : ι → Sort w
inst✝¹ : Nonempty ((a : ι) → κ a)
inst✝ : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
⊢ ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)

Tactic:
by
  classical
  suffices h : ∀ {κ : ι → Type w} [Nonempty (Π a, κ a)] (f : Π a, κ a → α),
      ⨅ a ∈ s, ⨆ b, f a b = ⨆ g : (Π a, κ a), ⨅ a ∈ s, f a (g a) by
    have : Nonempty (Π a, PLift (κ a)) := (Equiv.piCongrRight fun _ => Equiv.plift).nonempty
    simpa [← Equiv.plift.symm.iSup_comp, ← (Equiv.piCongrRight fun _ => Equiv.plift).symm.iSup_comp]
      using h (κ := fun a => PLift (κ a)) fun a b => f a b.down
  intro κ _ f
  have := hs.to_subtype
  have : Nonempty (Π a : { a // a ∉ s }, κ ↑a) := ‹Nonempty (Π a, κ a)›.map fun f a ↦ f a
  simp [← iInf_subtype'', iInf_iSup_eq_of_finite (ι := s),
    ← Equiv.piEquivPiSubtypeProd (· ∈ s) _ |>.symm.iSup_comp, iSup_prod, iSup_const]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

Tactic:
by_cases! hf : ¬BddAbove (range f)

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : ¬BddAbove (range f)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ∀ (x : α), a < x ↔ x = b
⊢ IsTop b ∧ a ⋖ b

Tactic:
have hb : a < b := (h b).mpr rfl

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ∀ (x : α), a < x ↔ x = b
hb : a < b
⊢ IsTop b ∧ a ⋖ b
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
s : Finset β
f : α → β
hf : InjOn f (f ⁻¹' ↑s)
inst✝ : DecidablePred fun x ↦ x ∈ Set.range f
b : β
hb : b ∈ ↑({x ∈ s | x ∈ Set.range f})
⊢ b ∈ f '' ↑(s.preimage f hf)

Tactic:
by aesop

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

Goal state before:
pp: a x : ℕ
⊢ x ∈ range a ↔ x ∈ Finset.range a

Tactic:
List.mem_range,

Goal state after:
a x : ℕ
⊢ x < a ↔ x ∈ Finset.range a
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: 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

Tactic:
exact h.apply _

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    (∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
      ∀ (f : ℕ → (i : ι) → α i),
        ∃ g, ∀ ⦃a_2 b : ℕ⦄, a_2 ≤ b → ∀ i ∈ Finset.cons a s h, r i ((f ∘ ⇑g) a_2 i) ((f ∘ ⇑g) b i)

Tactic:
· intro i s hi ih f
    obtain ⟨g, hg⟩ := (hr i).exists_monotone_subseq (f · i)
    obtain ⟨g', hg'⟩ := ih (f ∘ g)
    refine ⟨g'.trans g, fun a b hab => (Finset.forall_mem_cons _ _).2 ?_⟩
    exact ⟨hg _ _ (OrderHomClass.mono g' hab), hg' hab⟩

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
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Icc ↑a ↑b) ↔ a ≤ x ∧ x ≤ b

Tactic:
Finset.mem_subtype,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ ↑x ∈ Icc ↑a ↑b ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Ico ↑a ↑b) ↔ a ≤ x ∧ x < b

Tactic:
Finset.mem_subtype,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ ↑x ∈ Ico ↑a ↑b ↔ a ≤ x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Ioc ↑a ↑b) ↔ a < x ∧ x ≤ b

Tactic:
Finset.mem_subtype,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ ↑x ∈ Ioc ↑a ↑b ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Ioo ↑a ↑b) ↔ a < x ∧ x < b

Tactic:
Finset.mem_subtype,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ ↑x ∈ Ioo ↑a ↑b ↔ a < x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a x : Subtype p
⊢ x ∈ Finset.subtype p (Ici ↑a) ↔ a ≤ x

Tactic:
Finset.mem_subtype,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a x : Subtype p
⊢ ↑x ∈ Ici ↑a ↔ a ≤ x
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a x : Subtype p
⊢ x ∈ Finset.subtype p (Ioi ↑a) ↔ a < x

Tactic:
Finset.mem_subtype,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a x : Subtype p
⊢ ↑x ∈ Ioi ↑a ↔ a < x