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

Goal state before:
pp: case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ f 0 :: (ofFn fun i ↦ f i.castSucc.succ).concat (f (Fin.last n).succ) =
    f 0 :: (ofFn fun i ↦ f i.succ.castSucc).concat (f (Fin.last (n + 1)))

Tactic:
Fin.succ_last

Goal state after:
case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ f 0 :: (ofFn fun i ↦ f i.castSucc.succ).concat (f (Fin.last n.succ)) =
    f 0 :: (ofFn fun i ↦ f i.succ.castSucc).concat (f (Fin.last (n + 1)))
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ a < a.succ.castPred ha

Tactic:
lt_castPred_succ_iff,

Goal state after:
n : ℕ
a : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ a ≤ a
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
x✝¹ x✝ : Fin (n + 1)
h : x✝¹.succAbove = x✝.succAbove
⊢ x✝¹ = x✝

Tactic:
by
  simpa [range_succAbove] using congr_arg (fun f : Fin n → Fin (n + 1) => (Set.range f)ᶜ) h

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ (j : Fin n), j < i → ¬p (f j) = true
⊢ (ofFn f)[↑i] = b

Tactic:
simpa using! hfb

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

Goal state before:
pp: case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
isLt : n + m < n + (m + 1)
lt_n : ¬n + m < n
sub_lt : n + m - n < m
nlt_add : ¬n + m < n + m
⊢ bs ⟨n + m - n, ⋯⟩ = b

Tactic:
simp [Nat.add_comm n m] at sub_lt

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
op : (j : Fin (n + 1)) → α j → α j → α j
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (i.succAbove j)
⊢ op i x y = op i (i.insertNth x p i) (i.insertNth y q i) ∧
    (fun j ↦ op (i.succAbove j) (p j) (q j)) = i.removeNth fun j ↦ op j (i.insertNth x p j) (i.insertNth y q j)

Tactic:
unfold removeNth; simp

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))

Tactic:
by rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm a,
      ha.assoc]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
i : Fin n
x : α (p.succAbove i)
f : (j : Fin (n + 1)) → α j
j : Fin n
⊢ p.removeNth (update f (p.succAbove i) x) j = update (p.removeNth f) i x j

Tactic:
rcases eq_or_ne j i with rfl | hne <;> simp [removeNth, *]

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

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
⊢ Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1

Tactic:
have := Classical.decEq α

Goal state after:
α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
this : DecidableEq α
⊢ Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
f : Fin n → α
⊢ (ofFn f).SortedLE ↔ Monotone f

Tactic:
simp only [sortedLE_iff_monotone_get, Monotone, Fin.forall_iff,
    length_ofFn, get_ofFn, Fin.cast_mk, Fin.mk_le_mk]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
⊢ [a, b] <+ l → R a b

Tactic:
hab

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
⊢ R a b
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case inr.inl
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ l₂ l₃ : List α
h : Lex r l₁ l₃
⊢ Lex r (a :: l₁) (a :: l₂) ∨ Lex r (a :: l₂) (a :: l₃)

Tactic:
exact (aux _ l₂ _ h).imp cons cons

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: case pos
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : s = ∅
⊢ p (a * s.prod)

Tactic:
simp [hs_empty, p_s a]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: l s : List ℕ
hs : s ∈ l.ranges
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) l.ranges.flatten

Tactic:
rw [ranges_flatten]; exact nodup_range

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:
rw [Nat.sub_lt_iff_lt_add hm']

Goal state after:
α : 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
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ l.reverse.alternatingProd * [a].alternatingProd ^ (-1) ^ l.reverse.length =
    (a :: l).alternatingProd ^ (-1) ^ ((a :: l).length + 1)

Tactic:
alternatingProd_reverse,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ l.alternatingProd ^ (-1) ^ (l.length + 1) * [a].alternatingProd ^ (-1) ^ l.reverse.length =
    (a :: l).alternatingProd ^ (-1) ^ ((a :: l).length + 1)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
l : List α
h : l.rotate 1 = l
n✝ n : ℕ
hn : l.rotate n = l
⊢ l.rotate n.succ = l

Tactic:
by rwa [Nat.succ_eq_add_one, ← l.rotate_rotate, hn]

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

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

Tactic:
Nat.mul_comm,

Goal state after:
n k : ℕ
e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
⊢ n.choose k * (n + 1) - n.choose k * (k + 1) = n.choose k * (n - k)
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝ : CommMonoid α
⊢ ∀ (x : ConjClasses α), ConjClasses.mk (Quotient.lift id ⋯ x) = x

Tactic:
forall_isConj

Goal state after:
α : Type u
β : Type v
inst✝ : CommMonoid α
⊢ ∀ (a : α), ConjClasses.mk (Quotient.lift id ⋯ (ConjClasses.mk a)) = ConjClasses.mk a
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
⊢ ∀ {b : ConjClasses α}, a ∈ b.carrier ↔ ConjClasses.mk a = b

Tactic:
forall_isConj

Goal state after:
α : Type u
inst✝ : Monoid α
a : α
⊢ ∀ (a_1 : α), a ∈ (ConjClasses.mk a_1).carrier ↔ ConjClasses.mk a = ConjClasses.mk a_1
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = ⋃ b ∈ t, (fun a ↦ (a, b)) '' s

Tactic:
rw [iUnion_image_right, image2_mk_eq_prod]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (Prod.mk '' s).seq t = ((fun b a ↦ (a, b)) '' t).seq s

Tactic:
rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ ((fun x ↦ Prod.swap ∘ x) ∘ Prod.mk '' t).seq s = ((fun b a ↦ (a, b)) '' t).seq s
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
⊢ 1 ∈ t⁻¹ * s ↔ ¬Disjoint s t

Tactic:
by
  aesop (add simp [not_disjoint_iff_nonempty_inter, mem_mul, mul_eq_one_iff_eq_inv, Set.Nonempty])

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : H.Normal
n : G
hn : n ∈ H
g : G
⊢ g⁻¹ * n * g ∈ H

Tactic:
by
  convert! nH.conj_mem n hn g⁻¹
  rw [inv_inv]

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

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
p : Prop
K : p → Subgroup G
x : G
h : p
⊢ x ∈ ⨆ (h : p), K h ↔ x = 1 ∨ ∃ (h : p), x ∈ K h

Tactic:
simp +contextual [h]

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

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
p : Prop
K : p → Subgroup G
x : G
h : ¬p
⊢ x ∈ ⨆ (h : p), K h ↔ x = 1 ∨ ∃ (h : p), x ∈ K h

Tactic:
simp +contextual [h]

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

Goal state before:
pp: case mp.refine_1
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ ↑s ∪ ↑t, ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
rintro x (hx | hx)
      · exact ⟨x, hx, 1, t.one_mem, by simp⟩
      · exact ⟨1, s.one_mem, x, hx, by simp⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
hxy : x * y = 1
hx1 : x = 1 := h hx (Subgroup.inv_mem H₂ hy) (eq_inv_iff_mul_eq_one.mpr hxy)
⊢ y = 1

Tactic:
by simpa [hx1] using hxy

Goal state after:
Module: Mathlib.Data.Nat.Bits

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

Tactic:
Nat.mul_comm,

Goal state after:
m n : ℕ
⊢ m * 2 ^ n * 2 = 2 ^ (n + 1) * m
Module: Mathlib.Data.Nat.Pairing

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

Tactic:
· simp [pair, h]

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_eq.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

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

Goal state before:
pp: case pos
M : Type u_1
inst✝ : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
h : p
⊢ x ∈ ⨆ (h : p), S h ↔ x = 1 ∨ ∃ (h : p), x ∈ S h

Tactic:
simp +contextual [h]

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

Goal state before:
pp: case neg
M : Type u_1
inst✝ : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
h : ¬p
⊢ x ∈ ⨆ (h : p), S h ↔ x = 1 ∨ ∃ (h : p), x ∈ S h

Tactic:
simp +contextual [h]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Fintype ↥⊥
⊢ card ↥⊥ = 1

Tactic:
exact card_bot

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

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

Tactic:
have hk : p k := Nat.find_spec H

Goal state after:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
⊢ ∃ n, ¬p n ∧ p (n + 1)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a
⊢ argmax f (a :: hd ++ [tl]) =
    Option.casesOn (argmax f (hd ++ [tl])) (some a) fun c ↦ if f a < f c then some c else some a

Tactic:
argmax_concat,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a
⊢ (Option.casesOn (argmax f (a :: hd)) (some tl) fun c ↦ if f c < f tl then some tl else some c) =
    Option.casesOn (argmax f (hd ++ [tl])) (some a) fun c ↦ if f a < f c then some c else some a
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
a : α
left✝ : a ∈ s
ha : inl a = inr b
⊢ False

Tactic:
exact inl_ne_inr ha

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
h : Forall₂ (fun a b ↦ f a b = g a b) la lb
⊢ zipWith f la lb = zipWith g la lb

Tactic:
induction h with
  | nil => rfl
  | cons hfg _ ih => exact congr_arg₂ _ hfg ih

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

Goal state before:
pp: case cons.mpr.cons_cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
l₁✝ : List α
h : l₁✝ <+ t
⊢ a :: l₁✝ <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: l₁✝

Tactic:
exact Or.inr ⟨_, h, rfl⟩

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.sublists = map reverse l.reverse.sublists'

Tactic:
rw [← sublists_reverse, reverse_reverse]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ (powersetAux l).revzip ~ (powersetAux' l).revzip

Tactic:
have := Classical.decEq α

Goal state after:
α : Type u_1
l : List α
this : DecidableEq α
⊢ (powersetAux l).revzip ~ (powersetAux' l).revzip
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ (powersetAux l₁).revzip ~ (powersetAux l₂).revzip

Tactic:
have := Classical.decEq α

Goal state after:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ (powersetAux l₁).revzip ~ (powersetAux l₂).revzip
Module: Mathlib.Data.Multiset.Powerset

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

Tactic:
simp [Perm.swap]

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

Goal state before:
pp: case right
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ (insert a r).sup id ≤ z

Tactic:
rw [sup_insert, id, sup_le_iff]

Goal state after:
case right
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ a ≤ z ∧ r.sup id ≤ z
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : IsEmpty α
⊢ ∃ t, ∀ (a : α), f a ≤ t.sup f

Tactic:
exact ⟨⊥, isEmptyElim⟩

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
⊢ i ∈ t

Tactic:
obtain ⟨j, hj, haj⟩ := mem_iUnion₂.1 (h <| mem_iUnion₂_of_mem hi hai)

Goal state after:
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ i ∈ t
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
r : ℕ
hr : r ≠ 0
hrs : r ≤ #s
⊢ (powersetCard r s).biUnion id = s

Tactic:
obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hr
  rw [← sup_eq_biUnion]
  exact powersetCard_sup _ _ hrs

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

Goal state before:
pp: case cons.inl
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s✝ : Finset ι
H : s✝.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
b : ι
hb : b ∈ s
h' : s.sup' hs f = f b
h : f b ≤ f c
⊢ ∃ i ∈ cons c s hcs, max (f c) (f b) = f i

Tactic:
exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ ∃ i, x ∈ t (f i)

Tactic:
exact ⟨⟨x, hx⟩, hf _⟩

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

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

Tactic:
rw [bddAbove_def] at hf ⊢

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : ∃ x, ∀ y ∈ range f, y ≤ x
h✝¹ : Nonempty β
h✝ : Nonempty γ
⊢ ∃ x, ∀ y ∈ range fun b ↦ ⨆ c, f (b, c), y ≤ x
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

Tactic:
rw [bddAbove_def] at hf ⊢

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : ∃ x, ∀ y ∈ range f, y ≤ x
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
b : β
⊢ ∃ x, ∀ y ∈ range fun c ↦ f (b, c), y ≤ x
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i.down

Tactic:
rw [← iSup_eq_iSup_finset, ← Equiv.plift.surjective.iSup_comp]; rfl

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ⩿ b
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
rw [wcovBy_iff_covBy_or_le_and_le] at h

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ⋖ b ∨ a ≤ b ∧ b ≤ a
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
⊢ a ⋖ b → ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
intro h
    obtain ⟨j, hj⟩ := (Pi.lt_def.1 h.1).2
    have : Nonempty ι := ⟨j⟩
    obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h.wcovBy
    obtain rfl : i = j := by_contra fun this ↦ (hi j (Ne.symm this)).2.not_gt hj
    exact ⟨i, covBy_iff_wcovBy_and_lt.2 ⟨h.wcovBy.eval i, hj⟩, hi⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Nonempty α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' ↑s) ↑s
⊢ (s.preimage f ⋯).sup f = s.sup id

Tactic:
by
  classical
  have hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' ↑s)) x = id x := hf.invOn_invFunOn.2
  rw [← sup_congr (Eq.refl s) hfinvs, ← sup_image]
  congr
  exact (image_eq_preimage_of_leftInvOn_injOn hf.invOn_invFunOn.2 hf.2.1).symm

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ ⇑f '' s
⊢ x ∈ s ∧ Minimal (fun x ↦ x ∈ t) (f x) ↔ Minimal (fun x ↦ x ∈ s ∧ x ∈ ⇑f ⁻¹' t) x

Tactic:
mem_preimage,

Goal state after:
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ ⇑f '' s
⊢ x ∈ s ∧ Minimal (fun x ↦ x ∈ t) (f x) ↔ Minimal (fun x ↦ x ∈ s ∧ f x ∈ t) x
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
⊢ ⇑f '' {x | Minimal P x} = {x | Minimal (fun x ↦ P (f.symm x)) x}

Tactic:
convert! _root_.image_monotone_setOfPred_minimal (f := f) (by simp [f.le_iff_le])

Goal state after:
case e'_3
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
x✝¹ x✝ : β
⊢ P (f.symm x✝) ↔ ∃ x₀, P x₀ ∧ f x₀ = x✝
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ x ∈ (Icc (f a) (f b)).preimage ⇑f ⋯ ↔ a ≤ x ∧ x ≤ b

Tactic:
mem_preimage,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ f x ∈ Icc (f a) (f b) ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ x ∈ (Ico (f a) (f b)).preimage ⇑f ⋯ ↔ a ≤ x ∧ x < b

Tactic:
mem_preimage,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ f x ∈ Ico (f a) (f b) ↔ a ≤ x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ x ∈ (Ioc (f a) (f b)).preimage ⇑f ⋯ ↔ a < x ∧ x ≤ b

Tactic:
mem_preimage,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ f x ∈ Ioc (f a) (f b) ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ x ∈ (Ioo (f a) (f b)).preimage ⇑f ⋯ ↔ a < x ∧ x < b

Tactic:
mem_preimage,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ f x ∈ Ioo (f a) (f b) ↔ a < x ∧ x < b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
a : α
inst✝ : Std.Refl r
⊢ (insert a s).PartiallyWellOrderedOn r ↔ s.PartiallyWellOrderedOn r

Tactic:
simp only [← singleton_union, partiallyWellOrderedOn_union,
    partiallyWellOrderedOn_singleton, true_and]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
this : TransGen CovBy a b ≤ (TransGen LT.lt on f) a b
⊢ f a < f b

Tactic:
rw [← lt_iff_transGen_covBy, transGen_eq_self] at this

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
this : (a < b) ≤ (LT.lt on f) a b
⊢ f a < f b
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ ∃ c, c * g * c⁻¹ = h * g * h⁻¹

Tactic:
exact ⟨h, rfl⟩

Goal state after: