mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ (n.choose k + n.choose k.succ) * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

Tactic:
Nat.add_mul,

Goal state after:
case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ (n.choose k * k.succ ! + n.choose k.succ * k.succ !) * (n + 1 - k.succ)! = (n + 1)!
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ (n.choose k * k.succ ! + n.choose k.succ * k.succ !) * (n + 1 - k.succ)! = (n + 1)!

Tactic:
Nat.add_mul,

Goal state after:
case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ n.choose k * k.succ ! * (n + 1 - k.succ)! + n.choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : (List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1
⊢ List.count a l ≤ 1

Tactic:
contrapose h

Goal state after:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : ¬List.count a l ≤ 1
⊢ ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ (k + 1) * n ! + (n - k) * n ! = (n + 1)!

Tactic:
Nat.add_mul,

Goal state after:
case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ k * n ! + 1 * n ! + (n - k) * n ! = (n + 1)!
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a' : α
f : (a'_1 : α) → a'_1 ∈ a' ::ₘ m → δ a'_1
h' : a' ∈ a' ::ₘ m
⊢ cons m a' (f a' ⋯) (fun a'_1 ha' ↦ f a'_1 ⋯) a' h' = f a' h'

Tactic:
rw [Pi.cons_same]

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

Goal state before:
pp: case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ n.choose (k + 1) * (n + 1) = (n.choose k + n.choose k.succ) * (n + 1 - (k + 1))

Tactic:
Nat.add_mul,

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

Goal state before:
pp: case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
⊢ ((p + 1) * n).choose n = (p + 1) * ((p + 1) * n - 1).choose (n - 1)

Tactic:
Nat.add_mul,

Goal state after:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
⊢ (p * n + 1 * n).choose n = (p + 1) * (p * n + 1 * n - 1).choose (n - 1)
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case cons.mpr
α : 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 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1) →
    ∃ a_2, a_2 ∈ t a ∧ ∃ a_3, (∀ (a : α) (h : a ∈ m), a_3 a h ∈ t a) ∧ Pi.cons m a a_2 a_3 = f

Tactic:
intro hf

Goal state after:
case cons.mpr
α : 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
hf : ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
⊢ ∃ a_1, a_1 ∈ t a ∧ ∃ a_2, (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons m a a_1 a_2 = f
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
e₁ e₂ : α ≃ β
h : e₁.toEmbedding = e₂.toEmbedding
⊢ ∀ (x : α), e₁ x = e₂ x

Tactic:
convert! DFunLike.congr_fun h using 0

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (image2 f s t).Infinite
⊢ (s ×ˢ t).Infinite

Tactic:
← image_uncurry_prod

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (uncurry f '' s ×ˢ t).Infinite
⊢ (s ×ˢ t).Infinite
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case refine_1
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ S ^ n * {a} ⊆ S ^ (n + 1)

Tactic:
exact mul_subset_mul Set.Subset.rfl (Set.singleton_subset_iff.mpr ha)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
f : α → β
⊢ f '' ⋂ i ∈ S, i ⊆ ⋂ s ∈ S, f '' s

Tactic:
apply image_iInter₂_subset

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

Goal state before:
pp: case mul
M : Type u_1
inst✝ : Mul M
p : M → Prop
s : Set M
closure : Subsemigroup.closure s = ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x x✝ y✝ : M
hx✝ : x✝ ∈ Subsemigroup.closure s
hy✝ : y✝ ∈ Subsemigroup.closure s
h₁ : p x✝
h₂ : p y✝
⊢ p (x✝ * y✝)

Tactic:
exact mul _ _ h₁ h₂

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

Goal state before:
pp: case mul
M : Type u_1
N : Type u_2
inst✝ : Mul M
s✝ : Set M
S : Subsemigroup M
p : M → Prop
s : Set M
closure : Subsemigroup.closure s = ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x✝ y✝ : M
h₁ : p x✝
h₂ : p y✝
⊢ p (x✝ * y✝)

Tactic:
exact mul _ _ h₁ h₂

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set α
⊢ f '' ⋃ i, s i = ⋃ i, f '' s i

Tactic:
ext1 x

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set α
x : β
⊢ x ∈ f '' ⋃ i, s i ↔ x ∈ ⋃ i, f '' s i
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case mul
M : Type u_1
inst✝ : MulOneClass M
motive : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x x✝ y✝ : M
hx✝ : x✝ ∈ Submonoid.closure s
hy✝ : y✝ ∈ Submonoid.closure s
h₁ : motive x✝
h₂ : motive y✝
⊢ motive (x✝ * y✝)

Tactic:
exact mul _ _ h₁ h₂

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

Goal state before:
pp: case mul
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
x✝ y✝ : M
h₁ : p x✝
h₂ : p y✝
⊢ p (x✝ * y✝)

Tactic:
exact mul _ _ h₁ h₂

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
H K L : S
⊢ ↑H ⊆ ↑K ∪ ↑L ↔ H ≤ K ∨ H ≤ L

Tactic:
refine ⟨fun h ↦ ?_, fun h x xH ↦ h.imp (mem_of_le_of_mem · xH) (mem_of_le_of_mem · xH)⟩
  rw [or_iff_not_imp_left, SetLike.not_le_iff_exists, ← SetLike.coe_subset_coe]
  exact fun ⟨x, xH, xK⟩ y yH ↦ (h <| mul_mem xH yH).elim
    ((h yH).resolve_left fun yK ↦ xK <| (mul_mem_cancel_right yK).mp ·)
    (mul_mem_cancel_left <| (h xH).resolve_left xK).mp

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

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

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

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

Tactic:
· exact ⟨1, s.one_mem, 1, t.one_mem, by simp⟩

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

case mp.refine_4
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ closure (↑s ∪ ↑t), (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B

Tactic:
by
  refine
    map_injective_of_ker_le B.subtype (ker_le_comap _ _)
      (le_trans (ker_le_comap B.subtype _) le_sup_left) ?_
  simp only [subgroupOf, map_comap_eq, map_sup, range_subtype]
  rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]

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

Goal state before:
pp: case bit
b : Bool
n : ℕ
⊢ bit b n % 2 = (bit b n).bodd.toNat

Tactic:
cases b <;> simp

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

Goal state before:
pp: n a b : ℕ
H : unpair n = (a, b)
⊢ pair a b = n

Tactic:
simpa [H] using pair_unpair n

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

Goal state before:
pp: m n : ℕ
a b : Bool
h : m < n
⊢ bit a m < 2 * n

Tactic:
cases a

Goal state after:
case false
m n : ℕ
b : Bool
h : m < n
⊢ bit false m < 2 * n

case true
m n : ℕ
b : Bool
h : m < n
⊢ bit true m < 2 * n
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ decode n = none

Tactic:
suffices decodeSum n = none by
    change (decodeSum n).bind _ = none
    rw [this]
    rfl
  have : 1 ≤ n / 2 := by
    rw [Nat.le_div_iff_mul_le]
    exacts [h, by decide]
  obtain ⟨m, e⟩ := exists_eq_succ_of_ne_zero (_root_.ne_of_gt this)
  simp only [decodeSum, div2_val]; cases bodd n <;> simp [e]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
P : α → Prop
encA : Encodable α
decP : DecidablePred P
a : Subtype P
⊢ encode a = encode ↑a

Tactic:
cases a

Goal state after:
case mk
α : Type u_1
P : α → Prop
encA : Encodable α
decP : DecidablePred P
val✝ : α
property✝ : P val✝
⊢ encode ⟨val✝, property✝⟩ = encode ↑⟨val✝, property✝⟩
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → (x • s ∩ t).Nonempty

Tactic:
rintro ⟨a, b, ⟨ha, hb⟩, rfl⟩

Goal state after:
case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
ha : a ∈ t
hb : b ∈ s
⊢ ((a * b⁻¹) • s ∩ t).Nonempty
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → (x • s ∩ t).Nonempty

Tactic:
rintro ⟨a, b, ⟨ha, hb⟩, rfl⟩
    exact ⟨a, mem_inter (mem_smul_set.mpr ⟨b, hb, by simp⟩) ha⟩

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

Goal state before:
pp: case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : List α
ih : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpl : ∀ (a_1 : α), a_1 ∈ a :: s → p a_1
⊢ f (a :: s).prod ≤ (map f (a :: s)).prod

Tactic:
have hpla : ∀ x, x ∈ s → p x := fun x hx => hpl x (mem_cons_of_mem _ hx)
    have hp_prod : p s.prod := prod_induction p hp_mul hp_one hpla
    grw [prod_cons, map_cons, prod_cons, h_mul a s.prod (hpl _ mem_cons_self) hp_prod, ih hpla]

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

Goal state before:
pp: case nil
M : Type u_3
N : Type u_4
inst✝² : AddZeroClass M
inst✝¹ : Zero N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
⊢ f [].sum ≤ foldr max 0 (map f [])

Tactic:
simpa using h0

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

Goal state before:
pp: M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
a b : M
l : List M
hl₁ : ∀ (x : M), x ∈ a :: b :: l → 1 < x
x✝ : a :: b :: l ≠ []
⊢ 1 < (a :: b :: l).prod

Tactic:
by
    simp only [forall_eq_or_imp, List.mem_cons] at hl₁
    rw [List.prod_cons]
    apply one_lt_mul_of_lt_of_le' hl₁.1
    apply le_of_lt ((b :: l).one_lt_prod_of_one_lt _ (l.cons_ne_nil b))
    grind

Goal state after:
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ toLex x ≤ toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 ≤ y.2)

Tactic:
simp only [toLex_le_toLex, lt_iff_le_not_ge, le_antisymm_iff]
  tauto

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S T : Submonoid M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
by
  rw [← SetLike.le_def]
  exact le_sup_right

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

Goal state before:
pp: case nil
α : Type u
init tail : List α
⊢ (init, tail) ∈ [].inits.zip [[]] ↔ init ++ tail = []

Tactic:
inits,

Goal state after:
case nil
α : Type u
init tail : List α
⊢ (init, tail) ∈ [[]].zip [[]] ↔ init ++ tail = []
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {init tail : List α}, (init, tail) ∈ tail✝.inits.zip tail✝.tails ↔ init ++ tail = tail✝
init tail : List α
⊢ (init, tail) ∈ (head✝ :: tail✝).inits.zip ((head✝ :: tail✝) :: tail✝.tails) ↔ init ++ tail = head✝ :: tail✝

Tactic:
inits,

Goal state after:
case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {init tail : List α}, (init, tail) ∈ tail✝.inits.zip tail✝.tails ↔ init ++ tail = tail✝
init tail : List α
⊢ (init, tail) ∈ ([] :: map (fun t ↦ head✝ :: t) tail✝.inits).zip ((head✝ :: tail✝) :: tail✝.tails) ↔
    init ++ tail = head✝ :: tail✝
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case succ.cons
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : powersetCardAux (n + 1) l₁✝ ~ powersetCardAux (n + 1) l₂✝
⊢ powersetCardAux (n + 1) l₁✝ ++ List.map (cons x✝) (powersetCardAux n l₁✝) ~
    powersetCardAux (n + 1) l₂✝ ++ List.map (cons x✝) (powersetCardAux n l₂✝)

Tactic:
exact IH.append ((IHn p).map _)

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

Goal state before:
pp: case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
⊢ j ∈ ⋃ n, f n → i ≠ j → r i j

Tactic:
hj

Goal state after:
case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
⊢ i ≠ j → r i j
Module: Mathlib.Data.Set.Finite.Range

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
hsu : u ⊆ f '' s
⊢ ∃ t ⊆ s, ∃ (_ : t.Finite), f '' t = u

Tactic:
by
  have : Finite u := Finite.to_subtype hu
  choose g hg hg' using hsu
  let g' (x : u) : α := g x.property
  exact ⟨range g', fun a ha ↦ by aesop, finite_range _, by aesop⟩

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
⊢ (s ×ˢ t).PairwiseDisjoint f

Tactic:
by
  rintro ⟨i, i'⟩ hi ⟨j, j'⟩ hj h
  rw [mem_prod] at hi hj
  obtain rfl | hij := eq_or_ne i j
  · refine (ht hi.2 hj.2 <| (Prod.mk_right_injective _).ne_iff.1 h).mono ?_ ?_
    · convert! le_iSup₂ (α := α) i hi.1; rfl
    · convert! le_iSup₂ (α := α) i hj.1; rfl
  · refine (hs hi.1 hj.1 hij).mono ?_ ?_
    · convert! le_iSup₂ (α := α) i' hi.2; rfl
    · convert! le_iSup₂ (α := α) j' hj.2; rfl

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

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ (↑(powersetCard n ∅)).Subsingleton

Tactic:
simp [Set.Subsingleton, subset_empty]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset α
⊢ eraseNone (image some s) = s

Tactic:
simpa only [map_eq_image] using! eraseNone_map_some s

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ (powersetCard n.succ u).sup id = u

Tactic:
by
  apply le_antisymm
  · simp_rw [Finset.sup_le_iff, mem_powersetCard]
    rintro x ⟨h, -⟩
    exact h
  · rw [sup_eq_biUnion, subset_iff]
    intro x hx
    simp only [mem_biUnion, id]
    obtain ⟨t, ht⟩ : ∃ t, t ∈ powersetCard n (u.erase x) := powersetCard_nonempty.2
      (le_trans (Nat.le_sub_one_of_lt hn) pred_card_le_card_erase)
    refine ⟨insert x t, ?_, mem_insert_self _ _⟩
    rw [← insert_erase hx, powersetCard_succ_insert (notMem_erase _ _)]
    exact mem_union_right _ (mem_image_of_mem _ ht)

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Trunc (P α)

Tactic:
by
  suffices ∀ n : ℕ, Trunc (P (ULift <| Fin n)) by
    apply Trunc.bind (this (Fintype.card α))
    intro h
    apply Trunc.map _ (Fintype.truncEquivFin α)
    intro e
    exact of_equiv (Equiv.ulift.trans e.symm) h
  intro n
  induction n with
  | zero =>
    have : card PEmpty = card (ULift (Fin 0)) := by
      simp only [card_fin, card_pempty, card_ulift]
    apply Trunc.bind (truncEquivOfCardEq this)
    intro e
    apply Trunc.mk
    exact of_equiv e h_empty
  | succ n ih =>
    have : card (Option (ULift (Fin n))) = card (ULift (Fin n.succ)) := by
      simp only [card_fin, card_option, card_ulift]
    apply Trunc.bind (truncEquivOfCardEq this)
    intro e
    apply Trunc.map _ ih
    intro ih
    exact of_equiv e (h_option ih)

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f ({x ∈ s | f x ∈ t}) = t
⊢ {x ∈ s | f x ∈ t} ⊆ s ∧ #({x ∈ s | f x ∈ t}) = n

Tactic:
← card_map f,

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
h : t ⊆ map f s ∧ #t = n
this : map f ({x ∈ s | f x ∈ t}) = t
⊢ {x ∈ s | f x ∈ t} ⊆ s ∧ #(map f ({x ∈ s | f x ∈ t})) = n
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α ↪ β
s a : Finset α
has : a ⊆ s
⊢ (mapEmbedding f).toEmbedding a ⊆ map f s ∧ #((mapEmbedding f).toEmbedding a) = #a

Tactic:
simp [has]

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
⊢ ∃ i ∈ s, s.sup' H f = f i

Tactic:
induction H using Finset.Nonempty.cons_induction with
  | singleton c => exact ⟨c, mem_singleton_self c, rfl⟩
  | cons c s hcs hs ih =>
    rcases ih with ⟨b, hb, h'⟩
    rw [sup'_cons hs, h']
    cases le_total (f b) (f c) with
    | inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
    | inr h => exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩

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

Goal state before:
pp: case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ BddBelow (range fun i ↦ ⨅ (_ : i ∈ s), f i)

pp: case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i ↦ ⨅ (_ : i ∈ s), f i

Tactic:
· classical
      refine (((hs.image f).union (finite_singleton (sInf ∅))).subset ?_).bddBelow
      intro
      simp only [ciInf_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
      grind

Goal state after:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i ↦ ⨅ (_ : i ∈ s), f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case inr
α : Type u_5
inst✝ : CompleteLinearOrder α
s : Set α
hfin : s.Finite
a : α
hne : a ≠ ⊥
hmem : a ∉ s
hnonempty : s.Nonempty
⊢ sSup s ≠ a

Tactic:
exact (hmem <| · ▸ hnonempty.csSup_mem hfin)

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this : Nonempty ↑s
⊢ ⨆ i, g (f ↑i) ≤ ⨆ i, g ↑i

Tactic:
refine ciSup_le ?_

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this : Nonempty ↑s
⊢ ∀ (x : ↑s), g (f ↑x) ≤ ⨆ i, g ↑i
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b - Ico a c = Ico (max a c) b

Tactic:
rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_sdiff_Ico_left]

Goal state after: