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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ #(insert a s) = #s

Tactic:
insert_eq_of_mem h

Goal state after:
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ #s = #s
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
⊢ #s = n

Tactic:
classical
  have : s = (range n).attach.image fun i => f i.1 (mem_range.1 i.2) := by
    ext a
    suffices _ : a ∈ s ↔ ∃ (i : _) (hi : i ∈ range n), f i (mem_range.1 hi) = a by
      simpa only [mem_image, mem_attach, true_and, Subtype.exists]
    constructor
    · intro ha; obtain ⟨i, hi, rfl⟩ := hf a ha; use i, mem_range.2 hi
    · rintro ⟨i, hi, rfl⟩; apply hf'
  calc
    #s = #((range n).attach.image fun i => f i.1 (mem_range.1 i.2)) := by rw [this]
    _ = #(range n).attach := ?_
    _ = #(range n) := card_attach
    _ = n := card_range n
  apply card_image_of_injective
  intro ⟨i, hi⟩ ⟨j, hj⟩ eq
  exact Subtype.ext <| f_inj i j (mem_range.1 hi) (mem_range.1 hj) eq

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

Goal state before:
pp: case isTrue
n : ℕ
a b : Fin n
h✝ : b ≤ a
⊢ ↑↑(a - b) = ↑↑a - ↑↑b + ↑0

Tactic:
fin_omega

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

Goal state before:
pp: case isFalse
n : ℕ
a b : Fin n
h✝ : ¬b ≤ a
⊢ ↑↑(a - b) = ↑↑a - ↑↑b + ↑n

Tactic:
fin_omega

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a.castSucc < b.succ ↔ a ≤ b

Tactic:
castSucc_lt_iff_succ_le,

Goal state after:
n : ℕ
a b : Fin n
⊢ a.succ ≤ b.succ ↔ a ≤ b
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
f_inj : Set.InjOn f ↑s
⊢ #s ≤ #t

Tactic:
by
  classical
  calc
    #s = #(s.image f) := (card_image_of_injOn f_inj).symm
    _ ≤ #t := card_le_card <| image_subset_iff.2 hf

Goal state after:
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' : α → β := fun a ↦ ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ ↑s
⊢ ∀ ⦃x₂ : α⦄, x₂ ∈ ↑s → f' a₁ = f' x₂ → a₁ = x₂

Tactic:
a₂

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₂ : α
⊢ a₂ ∈ ↑s → f' a₁ = f' a₂ → a₁ = a₂
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case zero
a b : Fin (0 + 1)
h : a < b
⊢ a + 1 ≤ b

Tactic:
fin_omega

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

Goal state before:
pp: case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
⊢ a + 1 ≤ b

Tactic:
fin_omega

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

Goal state before:
pp: n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
hkb : k < ↑b
⊢ ⟨k, ⋯⟩ + 1 ≤ b

Tactic:
fin_omega

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

Goal state before:
pp: n : ℕ
u v : Fin (n + 2)
h : u < v
⊢ v - (u + 1) < v - u

Tactic:
fin_omega

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s \ t) + #(s ∩ t) = #s

Tactic:
rw [← card_union_of_disjoint (disjoint_sdiff_inter _ _), sdiff_union_inter]

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

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p.succAbove i < p ↔ i.castSucc < p

Tactic:
castSucc_lt_iff_succ_le,

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p.succAbove i < p ↔ i.succ ≤ p
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
⊢ n ≤ k → (∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k

Tactic:
hnk

Goal state after:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
⊢ (∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case cast.last
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i : Fin n
h : x i = x₀
⊢ i.castSucc = last n

Tactic:
← h

Goal state after:
case cast.last
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
i : Fin n
hx₀ : ¬x i ∈ Set.range x
h : x i = x₀
⊢ i.castSucc = last n
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:
rw [← ha] at h; cases h with | step h => cases h;

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

Goal state before:
pp: case mp.cons_cons.refine_2.succ
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝ : ℕ
⊢ (a✝¹ :: l₁✝)[n✝ + 1]? =
    (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix ↦ if ix = 0 then 0 else (f ix.pred).succ) ⋯) (n✝ + 1)]?

Tactic:
· simpa using hf _

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
⊢ m = n

Tactic:
wlog hmlen : m ≤ n generalizing m n

Goal state after:
case inr
α : Type u_4
inst✝ : Infinite α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
this✝ : DecidableEq α := Classical.decEq α
this : ∀ ⦃m n : ℕ⦄, natEmbeddingAux α m = natEmbeddingAux α n → m ≤ n → m = n
hmlen : ¬m ≤ n
⊢ m = n

α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
⊢ m = n
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise R l
ha : a ∈ l.dropLast
⊢ R a (l.getLast ⋯)

Tactic:
rw [← pairwise_reverse] at h
  rw [getLast_eq_head_reverse]
  exact h.rel_head_tail (by rwa [tail_reverse, mem_reverse])

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n : ℕ
⊢ IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ

Tactic:
by
  induction n with
  | zero => simp
  | succ n hn =>
    simp only [range_succ, Nat.add_one_sub_one, Nat.lt_sub_iff_add_lt] at hn ⊢
    cases n with
    | zero => simp
    | succ n =>
      simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append,
        nil_append, isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢
      rw [hn, forall_lt_succ_right]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ l₁.prod = l₂.prod

Tactic:
have : Std.Symm fun x y ↦ ∀ z : M, y * (x * z) = x * (y * z) := { symm x y h z := h z |>.symm }
  refine h.foldr_eq' (Pairwise.forall_of_forall (fun _ _ _ ↦ rfl) <| hc.imp fun {a b} h z ↦ ?_) 1
  rw [← mul_assoc, ← mul_assoc, h]

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

Goal state before:
pp: α : Type u
l : List α
n m : ℕ
hml : m < l.length
⊢ (l.rotate n)[m]? = l[(m + n) % l.length]?

Tactic:
rw [rotate_eq_drop_append_take_mod]

Goal state after:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < l.length - n % l.length
⊢ l[n % l.length + m]? = l[(m + n % l.length) % l.length]?

Tactic:
Nat.lt_sub_iff_add_lt

Goal state after:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m + n % l.length < l.length
⊢ l[n % l.length + m]? = l[(m + n % l.length) % l.length]?
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_3
f : α → α
l : List α
hl : IsChain (fun x y ↦ f x = y) l
i : ℕ
hi : i < l.length
⊢ f^[i] l[0] = l[i]

Tactic:
induction i with
  | zero => rfl
  | succ i h =>
    rw [Function.iterate_succ', Function.comp_apply, h (by lia)]
    rw [List.isChain_iff_getElem] at hl
    apply hl

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

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ k < l.length

Tactic:
exact h.trans_eq (length_rotate _ _)

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

Goal state before:
pp: M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
p : M → Prop
inst✝ : DecidablePred p
⊢ (filter p s).prod * (filter (fun a ↦ ¬p a) s).prod = s.prod

Tactic:
rw [← prod_add, filter_add_not]

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

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

Tactic:
rw [isRotated_comm, isRotated_singleton_iff, eq_comm]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ S.bind f

Tactic:
classical
  refine le_iff_count.2 fun a ↦ ?_
  obtain ⟨m', hm'⟩ := exists_cons_of_mem <| mem_map_of_mem (fun b ↦ count a (f b)) hx
  rw [count_bind, hm', sum_cons]
  exact Nat.le_add_right _ _

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l ~r l' ↔ l' ∈ map l.rotate (range (l.length + 1))

Tactic:
mem_map,

Goal state after:
α : Type u
l l' : List α
⊢ l ~r l' ↔ ∃ a, a ∈ range (l.length + 1) ∧ l.rotate a = l'
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf : { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } g = f
a : α
⊢ f a ∈ t a

Tactic:
← hgf

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf : { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } g = f
a : α
⊢ { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } g a ∈ t a
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
⊢ (∃ a_1, a_1 ∈ t a ∧ f ∈ map (Pi.cons m a a_1) (m.pi t)) ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1

Tactic:
mem_map,

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
⊢ (∃ a_1, a_1 ∈ t a ∧ ∃ a_2, a_2 ∈ m.pi t ∧ Pi.cons m a a_1 a_2 = f) ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
ha : b ∈ conjugatesOf b
⊢ IsConj a b

Tactic:
← h

Goal state after:
α : Type u
inst✝ : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
ha : b ∈ conjugatesOf a
⊢ IsConj a b
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
rw [← closure_singleton_le_iff_mem, le_iSup_iff]

Goal state after:
M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
m : M
⊢ (∀ (b : Subsemigroup M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔
    ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s.Nonempty ∨ n = 0 → (s ^ n).Nonempty

Tactic:
rintro (hs | rfl)

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

case mp.inr
α : Type u_2
inst✝ : Monoid α
s : Set α
⊢ (s ^ 0).Nonempty
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t

Tactic:
← sInter_singleton t,

Goal state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂₀ S ×ˢ ⋂₀ {t} = ⋂ s ∈ S, s ×ˢ ⋂₀ {t}
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
b c : α
h : b * c = 1
⊢ {1} = 1

Tactic:
singleton_one

Goal state after:
case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
b c : α
h : b * c = 1
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s.Nonempty ∨ n = 0 → (s ^ n).Nonempty

Tactic:
rintro (hs | rfl)

Goal state after:
case mp.inl
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

case mp.inr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (s ^ 0).Nonempty
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
rw [← closure_singleton_le_iff_mem, le_iSup_iff]

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ (∀ (b : Submonoid M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
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, hy⟩ = 1

Tactic:
Subsingleton.elim (⟨y, hy⟩ : H) 1,

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
y : G
hy : y ∈ H
⊢ ↑1 = 1
Module: Mathlib.Algebra.Group.Subgroup.Lattice

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

Tactic:
rw [insert_eq, closure_union]

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure {1} ⊔ closure s = closure s
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
K : Subgroup G
f : G →* N
⊢ ∀ (x : N), (∃ x_1, (f.domRestrict K) x_1 = x) ↔ x ∈ map f K

Tactic:
mem_map,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
K : Subgroup G
f : G →* N
⊢ ∀ (x : N), (∃ x_1, (f.domRestrict K) x_1 = x) ↔ ∃ x_1 ∈ K, f x_1 = x
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case hK
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
⊢ DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on fun i ↦ K i.down) {i | True}

Tactic:
simp only [ofPred_true]
    rw [directedOn_onFun_iff, Set.image_univ, directedOn_range]
    -- `Directed.mono_comp` and much of the Set API requires `Type u` instead of `Sort u`
    intro i
    simp only [PLift.exists]
    intro j
    refine (hK i.down j.down).imp ?_
    simp

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

Goal state before:
pp: case neg.hle
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b ≤ a₂ * a₂

Tactic:
exact Nat.mul_self_le_mul_self (not_lt.mp h₂)

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
hp : p ↑x
⊢ False

Tactic:
simpa using h.le_bot x ⟨hp, x.prop⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
⊢ a ∈ u.toLeft ↔ inl a ∈ u

Tactic:
simp [toLeft]

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

Goal state before:
pp: case coe
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
⊢ l.max?.getD d = WithBot.unbotD d ↑y

Tactic:
simp only [WithBot.unbotD_coe]

Goal state after:
case coe
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
⊢ l.max?.getD d = y
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a ∆ b) = f a ∆ f b

Tactic:
by
  rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithTop.map (⇑ofDual) s.min = (image (⇑ofDual) s).max

Tactic:
max_eq_sup_withBot,

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithTop.map (⇑ofDual) s.min = (image (⇑ofDual) s).sup WithBot.some
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithTop.map (⇑toDual) s.min = (image (⇑toDual) s).max

Tactic:
max_eq_sup_withBot,

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithTop.map (⇑toDual) s.min = (image (⇑toDual) s).sup WithBot.some
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) ∨ (init, tail) ∈ map (Prod.map (fun t ↦ hd :: t) id) (tl.inits.zip tl.tails) →
    init ++ tail = hd :: tl

Tactic:
mem_map,

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

Tactic:
Prod.exists

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

Goal state before:
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) ∨ (init, tail) ∈ map (Prod.map (fun t ↦ hd :: t) id) (tl.inits.zip tl.tails)

Tactic:
mem_map,

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, a ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id a = (init, tail)
Module: Mathlib.Data.List.Zip

Goal state before:
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, a ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id a = (init, tail)

Tactic:
Prod.exists

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.Multiset.Powerset

Goal state before:
pp: α : Type u_1
a₁ : Multiset α
⊢ ∀ ⦃a₂ : Multiset α⦄, a₁.powerset = a₂.powerset → a₁ = a₂

Tactic:
a₂

Goal state after:
α : Type u_1
a₁ a₂ : Multiset α
⊢ a₁.powerset = a₂.powerset → a₁ = a₂
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 = l.toFinset.sup id

Tactic:
← Multiset.fold_dedup_idem,

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
⊢ (⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i = ⋃ i ∈ s \ t, f i

Tactic:
by
  refine
    (biUnion_sdiff_biUnion_subset f s t).antisymm
      (iUnion₂_subset fun i hi a ha => (mem_sdiff _).2 ⟨mem_biUnion hi.1 ha, ?_⟩)
  rw [mem_iUnion₂]; rintro ⟨j, hj, haj⟩
  exact (h (Or.inl hi.1) (Or.inr hj) (ne_of_mem_of_not_mem hj hi.2).symm).le_bot ⟨ha, haj⟩

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

Goal state before:
pp: case ex
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∃ x ∈ s, y ∈ f x

pp: case unique
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∀ (y₁ y₂ : ι), y₁ ∈ s ∧ y ∈ f y₁ → y₂ ∈ s ∧ y ∈ f y₂ → y₁ = y₂

Tactic:
· simpa only [mem_iUnion, exists_prop] using hy

Goal state after:
case unique
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∀ (y₁ y₂ : ι), y₁ ∈ s ∧ y ∈ f y₁ → y₂ ∈ s ∧ y ∈ f y₂ → y₁ = y₂
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ g (s.sup' H f) = s.sup' H (g ∘ f)

Tactic:
refine H.cons_induction ?_ ?_ <;> intros

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
a✝ : β
⊢ g ({a✝}.sup' ⋯ f) = {a✝}.sup' ⋯ (g ∘ f)

case refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
a✝¹ : β
s✝ : Finset β
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : g (s✝.sup' hs✝ f) = s✝.sup' hs✝ (g ∘ f)
⊢ g ((cons a✝¹ s✝ h✝).sup' ⋯ f) = (cons a✝¹ s✝ h✝).sup' ⋯ (g ∘ f)
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝² : ConditionallyCompletePartialOrderSup α
inst✝¹ : ConditionallyCompletePartialOrderSup β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hf : BddAbove (range f)
⊢ l (⨆ i, f i) = ⨆ i, l (f i)

Tactic:
by
  rw [iSup, gc.l_csSup_of_directedOn hd.directedOn_range (range_nonempty _) hf, iSup_range']

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
c : α
H : ∀ (x : ι), f x ≤ c
⊢ ∀ b ∈ range f, b ≤ c

Tactic:
forall_mem_range

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
c : α
H : ∀ (x : ι), f x ≤ c
⊢ ∀ (i : ι), f i ≤ c
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Icc a b = Icc ↑a ↑b

Tactic:
rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Icc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]

Goal state after: