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

Goal state before:
pp: case zero
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
f : α → α
⊢ (image f)^[0] s = image f^[0] s

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
s : Finset α
x✝ : α
⊢ x✝ ∈ filterMap some s ⋯ ↔ x✝ ∈ s

Tactic:
simp only [mem_filterMap, Option.some.injEq, exists_eq_right]

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

Goal state before:
pp: α : Type u_1
t : Set α
s : Finset ↑t
⊢ ↑(map (Embedding.subtype fun x ↦ x ∈ t) s) ⊆ t

Tactic:
intro a

Goal state after:
α : Type u_1
t : Set α
s : Finset ↑t
a : α
⊢ a ∈ ↑(map (Embedding.subtype fun x ↦ x ∈ t) s) → a ∈ t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case zero
⊢ range (0 + 1) \ {0} = image Nat.succ (range 0)

Tactic:
| zero =>

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

Goal state before:
pp: n m : ℕ
i : Fin n
h : n = m
⊢ Fin.cast h i.rev = (Fin.cast h i).rev

Tactic:
subst h; simp

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

Goal state before:
pp: case zero
m : ℕ
h : Nonempty (Fin 0 ↪ Fin m)
⊢ 0 ≤ m

Tactic:
| zero =>

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

Goal state before:
pp: n : ℕ
a b : Fin n
huv : ↑a + ↑b < n
⊢ ↑(a + b) = ↑a + ↑b

Tactic:
rw [val_add]
  simp [Nat.mod_eq_of_lt huv]

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

Goal state before:
pp: case zero
k : Fin (Nat.succ 0)
this : NeZero (Nat.succ 0)
hk : k ≠ 0
⊢ 1 ≤ k

Tactic:
| zero =>

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

Goal state before:
pp: n m : ℕ
h : n = m
⊢ finCongr h = Equiv.cast ⋯

Tactic:
subst h; simp

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

Goal state before:
pp: case zero
α : Type u
f : Fin (succ 0) → α
⊢ ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last 0))

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u
n : ℕ
f : Fin (0 * n) → α
⊢ ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten

Tactic:
| zero =>

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

Goal state before:
pp: n m : ℕ
a b : Fin m
ha : ↑a < n
h : b ≤ a
⊢ ↑(a.castLT ha - b.castLT ⋯) = ↑(a - b)

Tactic:
have : b.castLT (lt_of_le_of_lt h ha) ≤ a.castLT ha := by simpa [← val_fin_le] using h
  simp [sub_val_of_le, h, this]

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

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨m * ↑i + ↑j, ⋯⟩).flatten

Tactic:
by simp_rw [m.mul_comm, ofFn_mul, Fin.cast_mk]

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

Tactic:
succAbove_of_lt_succ _ _ h

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ i.succ ≠ p
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ

Tactic:
succAbove_of_castSucc_lt _ _ h,

Goal state after:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ i.succ.succAbove j.succ = j.castSucc.succ
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Tactic:
succAbove_of_castSucc_lt _ _ h,

Goal state after:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ i.castSucc.succAbove j.castSucc = j.castSucc.castSucc
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ (i.pred ⋯).predAbove (i.succAbove j) = j

Tactic:
succAbove_of_castSucc_lt _ _ h,

Goal state after:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ (i.pred ⋯).predAbove j.castSucc = j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ (i.succAbove j).succAbove (j.predAbove i) = i

Tactic:
succAbove_of_castSucc_lt _ _ h,

Goal state after:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc.succAbove (j.predAbove i) = i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
n' : ℕ
h : n' = n
⊢ append (xs ∘ Fin.cast h) ys = append xs ys ∘ Fin.cast ⋯

Tactic:
subst h; simp

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

Goal state before:
pp: α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
m' : ℕ
h : m' = m
⊢ append xs (ys ∘ Fin.cast h) = append xs ys ∘ Fin.cast ⋯

Tactic:
subst h; simp

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

Goal state before:
pp: case pos
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Tactic:
simp [hx, cons_sublist_cons, singleton_sublist]

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

Goal state before:
pp: case zero
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
⊢ cons a (snoc q b) 0 = snoc (cons a q) b 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Infinite α
s : Finset α
hn : #s ≤ 0
⊢ ∃ t, s ⊆ t ∧ #t = 0

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst✝ : Finite ↑s
⊢ Finite ↑{a | a ∈ s ∧ p a}

Tactic:
cases nonempty_fintype s
  classical
  infer_instance

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
inst✝ : Finite ↑s
⊢ Finite ↑(f '' s)

Tactic:
cases nonempty_fintype s
  classical
  infer_instance

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

Goal state before:
pp: α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
⊢ ∀ {a : α} {s_1 : Set α},
    a ∉ s_1 →
      s_1.Finite → (∀ (hts : s_1 ⊆ s), motive s_1 ⋯) → ∀ (hts : Insert.insert a s_1 ⊆ s), motive (Insert.insert a s_1) ⋯

Tactic:
intro a

Goal state after:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
⊢ ∀ {s_1 : Set α},
    a ∉ s_1 →
      s_1.Finite → (∀ (hts : s_1 ⊆ s), motive s_1 ⋯) → ∀ (hts : Insert.insert a s_1 ⊆ s), motive (Insert.insert a s_1) ⋯
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : p x
⊢ op (f x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))

Tactic:
have : x ∉ Finset.filter p s := by simp [hx]

Goal state after:
case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : p x
this : x ∉ filter p s
⊢ op (f x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
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:
intro a

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 : α}, [a, b] <+ l → R a b
Module: Mathlib.Data.List.Range

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

Tactic:
| zero =>

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

Goal state before:
pp: case succ.zero
r : ℕ → ℕ → Prop
hn : IsChain r (range 0) ↔ ∀ (m : ℕ), m + 1 < 0 → r m m.succ
⊢ IsChain r (range 0 ++ [0]) ↔ ∀ (m : ℕ), m < 0 → r m m.succ

Tactic:
| zero =>

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

Goal state before:
pp: case cons
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (a :: l).ranges

Tactic:
| cons a l hl =>

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

Goal state before:
pp: case cons
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ map length (a :: l).ranges = a :: l

Tactic:
| cons a l hl =>

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

Goal state before:
pp: ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Multiset ι
f : ι → M
⊢ (List.map f s.toList).prod = (map f s).prod

Tactic:
← Multiset.prod_coe,

Goal state after:
ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Multiset ι
f : ι → M
⊢ (↑(List.map f s.toList)).prod = (map f s).prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
x✝ : α
n : ℕ
⊢ x✝ ∈ (a :: l).rotate (n + 1) ↔ x✝ ∈ a :: l

Tactic:
by simp [rotate_cons_succ, mem_rotate, or_comm]

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

Goal state before:
pp: case zero
α : Type u
l : List α
⊢ l.rotate' 0 ~ l

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u
l : List α
⊢ l.rotate 0 = [] ↔ l = []

Tactic:
| zero =>

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

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

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case zero
α : Type u_1
a : α
s : Multiset α
h : a ∈ 0 • s
⊢ a ∈ s

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ ∀ (a : α) (s : Multiset α), filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)

Tactic:
intro a

Goal state after:
case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
⊢ ∀ (s : Multiset α), filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case zero
α : Type u
l : List α
⊢ (l.rotate 0).reverse.rotate 0 = l.reverse

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
⊢ Rel r (join 0) (join 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u
β : Type u_1
f : α → β
l : List α
⊢ map f (l.rotate 0) = (map f l).rotate 0

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
⊢ ∀ (a : α), a ∈ m → (if p a then {a} else 0).bind f = if p a then f a else 0

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type v
m : Multiset α
p : α → Prop
f : α → Multiset β
inst✝ : DecidablePred p
a : α
⊢ a ∈ m → (if p a then {a} else 0).bind f = if p a then f a else 0
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
s : Multiset M
hs : s ≠ 0
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
⊢ (map (⇑f) s).prod = f s.prod

Tactic:
by
  induction s using Quot.inductionOn; aesop (add simp List.prod_hom_nonempty)

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
⊢ ∀ (a : α), a ∈ m → ((Option.map singleton (f a)).getD 0).bind g = (Option.map g (f a)).getD 0

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : α
⊢ a ∈ m → ((Option.map singleton (f a)).getD 0).bind g = (Option.map g (f a)).getD 0
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case h₂
M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
⊢ ∀ {a : M} {s : Multiset M},
    a ∈ S → s ⊆ S → (map g1 s).prod ∣ (map g2 s).prod → (map g1 (insert a s)).prod ∣ (map g2 (insert a s)).prod

Tactic:
intro a

Goal state after:
case h₂
M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
a : M
⊢ ∀ {s : Multiset M},
    a ∈ S → s ⊆ S → (map g1 s).prod ∣ (map g2 s).prod → (map g1 (insert a s)).prod ∣ (map g2 (insert a s)).prod
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
x y : α
⊢ (x, y) ∈ l.offDiag ↔ ∃ i x_1 j x_2, i ≠ j ∧ l[i] = (x, y).fst ∧ l[j] = (x, y).snd

Tactic:
simp only [offDiag, exists_mem_zipIdx, mem_eraseIdx_iff_getElem, mem_flatMap, mem_map,
    Nat.zero_add, Prod.ext_iff, ← exists_and_right, exists_and_left, @exists_comm α, and_assoc,
    exists_eq_left', ne_comm]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
h : z = x
⊢ count (x, y) (map (fun x_1 ↦ (x, x_1)) l) = count y l

Tactic:
count_map_of_injective l (x, ·) (by simp [Function.Injective])

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
h : z = x
⊢ count y l = count y l
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case zero
⊢ choose 0 2 = 0 * (0 - 1) / 2

Tactic:
| zero =>

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

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

Tactic:
intro a

Goal state after:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
h : ∀ (a b : α), (List.count a l * List.count b l - if a = b then List.count a l else 0) ≤ 1
a : α
⊢ List.count a l ≤ 1
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
x✝ : ha₁ ≍ ha₂
h₁ : a'' ≠ a
⊢ cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁ ≍ cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂

Tactic:
rcases Decidable.eq_or_ne a'' a' with (rfl | h₂)

Goal state after:
case inl.inl
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
h₁ : a'' ≠ a
b' : δ a''
h : a ≠ a''
ha₁ : a'' ∈ a ::ₘ a'' ::ₘ m
ha₂ : a'' ∈ a'' ::ₘ a ::ₘ m
x✝ : ha₁ ≍ ha₂
⊢ cons (a'' ::ₘ m) a b (cons m a'' b' f) a'' ha₁ ≍ cons (a ::ₘ m) a'' b' (cons m a b f) a'' ha₂

case inl.inr
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
x✝ : ha₁ ≍ ha₂
h₁ : a'' ≠ a
h₂ : a'' ≠ a'
⊢ cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁ ≍ cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
· rw [hk₁]; simp [Nat.mul_comm, choose, Nat.sub_self]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
⊢ ∀ (a_1 : α) (ha : a_1 ∈ a ::ₘ m), r (cons m a b₁ f₁ a_1 ha) (cons m a b₂ f₂ a_1 ha)

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
⊢ ∀ (ha : a ∈ a✝ ::ₘ m), r (cons m a✝ b₁ f₁ a ha) (cons m a✝ b₂ f₂ a ha)
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ (a a' : α) (m : Multiset α) (b : Multiset ((a : α) → a ∈ m → β a)),
    ((t a).bind fun b_1 ↦ map (Pi.cons (a' ::ₘ m) a b_1) ((t a').bind fun b_2 ↦ map (Pi.cons m a' b_2) b)) ≍
      (t a').bind fun b_1 ↦ map (Pi.cons (a ::ₘ m) a' b_1) ((t a).bind fun b_2 ↦ map (Pi.cons m a b_2) b)

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
a : α
⊢ ∀ (a' : α) (m : Multiset α) (b : Multiset ((a : α) → a ∈ m → β a)),
    ((t a).bind fun b_1 ↦ map (Pi.cons (a' ::ₘ m) a b_1) ((t a').bind fun b_2 ↦ map (Pi.cons m a' b_2) b)) ≍
      (t a').bind fun b_1 ↦ map (Pi.cons (a ::ₘ m) a' b_1) ((t a).bind fun b_2 ↦ map (Pi.cons m a b_2) b)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case zero
n : ℕ
⊢ n.choose 0 * (n + 1) = (n + 1).choose 0 * (n + 1 - 0)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ x ∈ Set.univ.pi fun a ↦ ↑(t a)

Tactic:
rw [Set.mem_univ_pi]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ ∀ (i : α), x i ∈ ↑(t i)
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
a : α
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ ∅) = ∅

Tactic:
have : Nonempty α := ⟨a⟩
    simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ (a : α) (s : Multiset α),
    (s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup) →
      (a ::ₘ s).Nodup → (∀ (a_3 : α), a_3 ∈ a ::ₘ s → (t a_3).Nodup) → ((a ::ₘ s).pi t).Nodup

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s : Multiset α
t : (a : α) → Multiset (β a)
a : α
⊢ ∀ (s : Multiset α),
    (s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup) →
      (a ::ₘ s).Nodup → (∀ (a_3 : α), a_3 ∈ a ::ₘ s → (t a_3).Nodup) → ((a ::ₘ s).pi t).Nodup
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case zero
a c : ℕ
⊢ a.choose c ≤ (a + 0).choose c

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ multichoose 1 0 = 1

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ multichoose 2 0 = 0 + 1

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ multichoose 0 1 = 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ DecidablePred fun x ↦ x ∈ s ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: case zero
α : Type u
inst✝ : Group α
a b : α
⊢ (a * b * a⁻¹) ^ 0 = a * b ^ 0 * a⁻¹

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Mul α
inst✝ : IsLeftCancelMul α
s t : Set α
⊢ t.Nontrivial → s.Nonempty → (s * t).Nontrivial

Tactic:
rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩

Goal state after:
α : Type u_2
inst✝¹ : Mul α
inst✝ : IsLeftCancelMul α
s t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
c : α
hc : c ∈ s
⊢ (s * t).Nontrivial
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Mul α
inst✝ : IsRightCancelMul α
s t : Set α
⊢ s.Nontrivial → t.Nonempty → (s * t).Nontrivial

Tactic:
rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩

Goal state after:
α : Type u_2
inst✝¹ : Mul α
inst✝ : IsRightCancelMul α
s t : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ (s * t).Nontrivial
Module: Mathlib.Data.Set.Lattice.Image

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

Tactic:
iUnion_image_left,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = image2 (fun a b ↦ (a, b)) s t
Module: Mathlib.Algebra.Group.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
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
a : α
ha : m a ∈ s
b : α
hb : m b ∈ t
⊢ (fun x1 x2 ↦ x1 / x2) (m a) (m b) ∈ range ⇑m

Tactic:
exact ⟨a / b, map_div ..⟩

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
⊢ ∀ {a b : M}, a ∈ Set.ofPred IsUnit → b ∈ Set.ofPred IsUnit → a * b ∈ Set.ofPred IsUnit

Tactic:
intro a

Goal state after:
M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
a : M
⊢ ∀ {b : M}, a ∈ Set.ofPred IsUnit → b ∈ Set.ofPred IsUnit → a * b ∈ Set.ofPred IsUnit
Module: Mathlib.Algebra.Group.Subgroup.Lattice

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

Tactic:
by
  by_cases h : p <;>
  simp +contextual [h]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : G) (x : ι), a ∈ S x → ∀ (b : G) (x : ι), b ∈ S x → a * b = b * a

Tactic:
intro a

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : G
⊢ ∀ (x : ι), a ∈ S x → ∀ (b : G) (x : ι), b ∈ S x → a * b = b * a
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case zero
m : ℕ
⊢ (m * 0).bodd = (m.bodd && bodd 0)

Tactic:
| zero =>

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

Goal state before:
pp: case succ
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (m.bodd && n.bodd ^^ m.bodd) = (m.bodd && !n.bodd)

Tactic:
cases bodd m

Goal state after:
case succ.false
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && n.bodd ^^ false) = (false && !n.bodd)

case succ.true
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && n.bodd ^^ true) = (true && !n.bodd)
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case zero
⊢ boddDiv2 0 = (bodd 0, div2 0)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Encodable α
e : β ≃ α
n : ℕ
⊢ (decode n).bind (some ∘ ⇑e.symm) = Option.map (⇑e.symm) (decode n)

Tactic:
Option.map_eq_bind

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Encodable α
e : β ≃ α
n : ℕ
⊢ (decode n).bind (some ∘ ⇑e.symm) = (decode n).bind (some ∘ ⇑e.symm)