mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupNormClass F α β
f : F
x : α
⊢ x = 1 → f x = 0

Tactic:
rintro rfl

Goal state after:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupNormClass F α β
f : F
⊢ f 1 = 0
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case neg
a b : ℕ+
hab : a < b
h : ¬1 < b
⊢ ↑a ≤ 1

Tactic:
· exact hab.le.trans (le_of_not_gt h)

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

Goal state before:
pp: k m : ℕ+
a : ℕ
h : ↑m = ↑k * a
⊢ a ≠ 0

Tactic:
rintro rfl

Goal state after:
k m : ℕ+
h : ↑m = ↑k * 0
⊢ False
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : LinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : FloorRing α
inst✝² : FloorRing β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ round (f a) = round a

Tactic:
by
  simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, map_ofNat]

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n d : ℕ
⊢ ⌊↑n / ↑d⌋ = ↑(n / d)

Tactic:
push_cast

Goal state after:
n d : ℕ
⊢ ⌊↑n / ↑d⌋ = ↑n / ↑d
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
z : ℤ
⊢ -a ≤ ↑z ↔ -↑z ≤ a

Tactic:
neg_le

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
z : ℤ
⊢ -↑z ≤ a ↔ -↑z ≤ a
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℤ
⊢ f (x - ↑n) = f x - n • b

Tactic:
rw [← map_sub_zsmul, zsmul_one]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ (Nat.find this).pred * c < b * c
hn : Nat.find this ≠ 0
⊢ False

Tactic:
mul_lt_mul_iff_left₀ hc₀

Goal state after:
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ (Nat.find this).pred < b
hn : Nat.find this ≠ 0
⊢ False
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : Group G
inst✝ : Torsor G P
p : P
v : G
⊢ (fun x ↦ p /ₛ x) ((fun x ↦ x⁻¹ • p) v) = v

Tactic:
by simp [sdiv_smul_eq_sdiv_div]

Goal state after:
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: case mp
α : Type u_1
l : List α
a : α
⊢ l <+~ [a] → l = [] ∨ l = [a]

Tactic:
rw [subperm_iff]

Goal state after:
case mp
α : Type u_1
l : List α
a : α
⊢ (∃ l_1, l_1 ~ [a] ∧ l <+ l_1) → l = [] ∨ l = [a]
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
⊢ s = 0 → ¬s = {a}

Tactic:
rintro rfl

Goal state after:
α : Type u_1
a : α
⊢ ¬0 = {a}
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2
α : Type u_1
s : Multiset α
a : α
⊢ s = 0 → s ⊂ {a}

Tactic:
rintro rfl

Goal state after:
case refine_2
α : Type u_1
a : α
⊢ 0 ⊂ {a}
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mpr
α : Type u_1
s t : Multiset α
⊢ s = t → Rel (fun x1 x2 ↦ x1 = x2) s t

Tactic:
rintro rfl

Goal state after:
case mpr
α : Type u_1
s : Multiset α
⊢ Rel (fun x1 x2 ↦ x1 = x2) s s
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r p : α → β → Prop
s : Multiset α
t : Multiset β
hst : Rel r s t
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b
⊢ Rel p s t

Tactic:
induction hst with
  | zero => exact Rel.zero
  | @cons a b s t hab _hst ih =>
    apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)
    exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ s ≤ s + t

Tactic:
by
  simpa using Multiset.add_le_add_left (zero_le t)

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
⊢ Rel r as (b ::ₘ bs) ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Tactic:
rw [← rel_flip, rel_cons_left]

Goal state after:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
⊢ (∃ b_1 bs', flip r b b_1 ∧ Rel (flip r) bs bs' ∧ as = b_1 ::ₘ bs') ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ::ₘ s = t → a ∈ t ∧ s = t.erase a

Tactic:
rintro rfl

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ a ∈ a ::ₘ s ∧ s = (a ::ₘ s).erase a
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
⊢ ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ 0 → r a b) → m1.card = card 0 → Rel r m1 0

Tactic:
intro m _h hc
    rw [rel_zero_right, ← card_eq_zero, hc, card_zero]

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

Goal state before:
pp: case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : m.card = t.card + 1
b : α
hb : b ∈ m
⊢ Rel r m (a ::ₘ t)

Tactic:
obtain ⟨m', rfl⟩ := exists_cons_of_mem hb

Goal state after:
case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : (b ::ₘ m').card = t.card + 1
hb : b ∈ b ::ₘ m'
⊢ Rel r (b ::ₘ m') (a ::ₘ t)
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u

Tactic:
rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ s.erase a ≤ t ∩ u.erase a
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ filter (fun x ↦ x = b) ⟦l⟧ = replicate (count b ⟦l⟧) b

Tactic:
by
    simp only [quot_mk_to_coe, filter_coe, coe_count]
    rw [List.filter_eq, coe_replicate]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ s = t → u + s = u ∪ s

Tactic:
rintro rfl

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s u : Multiset α
h : s ≤ s
h0 : u + s = u ∪ s
⊢ u + s = u ∪ s
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s ≤ map f t ↔ s ≤ t

Tactic:
classical
    refine ⟨fun h => le_iff_count.mpr fun a => ?_, map_le_map⟩
    simpa [count_map_eq_count' f _ hf] using le_iff_count.mp h (f a)

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

Goal state before:
pp: case mpr
α : Type u_1
x y : α
⊢ x = y → [x] <:+: [y]

Tactic:
rintro rfl

Goal state after:
case mpr
α : Type u_1
x : α
⊢ [x] <:+: [x]
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case hl
α : Type u_1
l : List α
n : ℕ
⊢ (take n l).inits.length = (take (n + 1) l.inits).length

Tactic:
simp [take_take]

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

Goal state before:
pp: case h
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ) (h₁ : i < (take n l).inits.length) (h₂ : i < (take (n + 1) l.inits).length),
    (take n l).inits[i] = (take (n + 1) l.inits)[i]

Tactic:
simp [take_take]

Goal state after:
case h
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ), i < min n l.length + 1 → min i (min n l.length) = min i l.length
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
hs : s.Nontrivial
⊢ s ≠ {a}

Tactic:
rintro rfl

Goal state after:
α : Type u_1
a : α
hs : {a}.Nontrivial
⊢ False
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
hn : n ≠ 0
⊢ (replicate n a).toFinset = {a}

Tactic:
by
  ext x
  simp [hn, List.mem_replicate]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
⊢ x = a → x ∈ s₂

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x : α
h : x ∈ s₂
⊢ x ∈ s₂
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f (↑s ∪ ↑t)
⊢ ↑(image f (s ∩ t)) = ↑(image f s ∩ image f t)

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f (↑s ∪ ↑t)
⊢ f '' (↑s ∩ ↑t) = f '' ↑s ∩ f '' ↑t
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: m n k : Int
hn : 0 ≤ n
hk : 0 ≤ k
⊢ m / n / k = m.fdiv (n * k)

Tactic:
Int.fdiv_eq_ediv_of_nonneg _ (Int.mul_nonneg hn hk),

Goal state after:
m n k : Int
hn : 0 ≤ n
hk : 0 ≤ k
⊢ m / n / k = m / (n * k)
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = i

Tactic:
induction i using Nat.strong_induction_on with | _ i h
   =>  _ 

Goal state after:
case h
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
k : Fin n
⊢ k = 0 → k ≤ 0

Tactic:
rintro rfl

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ 0 ≤ 0
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
⊢ ↑(-1) = n

Tactic:
by
  cases n
  · simp
  rw [Fin.val_neg', Fin.val_one, Nat.add_one_sub_one, Nat.mod_eq_of_lt]
  constructor

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

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

Tactic:
by
  rw [← card_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]

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

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

Tactic:
by rw [lt_succAbove_iff_le_castSucc, le_castSucc_iff]

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

Goal state before:
pp: case grind
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hst : s ⊆ t
h : #s + 1 = #t
a : α
ha : t \ s = {a}
h✝ : ∀ (a : α), insert a s = t → a ∈ s
⊢ False

Tactic:
have : a ∈ t \ s

Goal state after:
case grind
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hst : s ⊆ t
h : #s + 1 = #t
a : α
ha : t \ s = {a}
h✝ : ∀ (a : α), insert a s = t → a ∈ s
this : a ∈ t \ s
⊢ False
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ image i.succAbove univ = {i}ᶜ

Tactic:
ext m

Goal state after:
n : ℕ
i m : Fin (n + 1)
⊢ m ∈ image i.succAbove univ ↔ m ∈ {i}ᶜ
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: a b : Fin 2
⊢ a = b → (a = 0 ↔ b = 0)

Tactic:
rintro rfl

Goal state after:
a : Fin 2
⊢ a = 0 ↔ a = 0
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card α = card β

Tactic:
← ofEquiv_card f

Goal state after:
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card β = card β
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ s = univ → #s = Fintype.card α

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ #univ = Fintype.card α
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ append u v (natAdd m r) = (v ∘ Fin.cast ⋯) (natAdd m r)

Tactic:
rw [append_right, Function.comp_apply]

Goal state after:
case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ v r = v (Fin.cast ⋯ (natAdd m r))
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ card α = 0 ↔ IsEmpty α

Tactic:
rw [card, Finset.card_eq_zero, univ_eq_empty_iff]

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

Goal state before:
pp: α : Type u
s : Multiset α
⊢ {x | x ∈ s}.Finite

Tactic:
classical simpa only [← Multiset.mem_toFinset] using! s.toFinset.finite_toSet

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

Goal state before:
pp: α : Type u
s : Set α
h : s.Infinite
⊢ s ≠ ∅

Tactic:
rintro rfl

Goal state after:
α : Type u
h : ∅.Infinite
⊢ False
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l.reverse).SortedLE ↔ l.reverse.SortedLE

Tactic:
sortedLE_listMap

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 ∘ map fun x ↦ a + x) l.ranges = map length l.ranges

Tactic:
apply map_congr_left

Goal state after:
case cons
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ ∀ (a_1 : List ℕ), a_1 ∈ l.ranges → (length ∘ map fun x ↦ a + x) a_1 = a_1.length
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∀ {a c : α},
    r a c →
      Relation.ReflTransGen r c b →
        (∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b) → ∃ l, IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b

Tactic:
· intro c d e _ ih
    obtain ⟨l, hl₁, hl₂⟩ := ih
    refine ⟨d :: l, .cons_cons e hl₁, ?_⟩
    rwa [getLast_cons_cons]

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

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

Tactic:
Function.iterate_succ',

Goal state after:
case succ
α : Type u_3
f : α → α
l : List α
hl : IsChain (fun x y ↦ f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ (f ∘ f^[i]) l[0] = l[i + 1]
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_1
α : Type u_1
a : α
s : Multiset α
n : ℕ
ha : a ∈ n • s
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
case refine_1
α : Type u_1
a : α
s : Multiset α
ha : a ∈ 0 • s
⊢ False
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
n : ℕ
a : α
h : r a a
⊢ IsChain r (replicate n a)

Tactic:
induction n using Nat.twoStepInduction

Goal state after:
case zero
α : Type u_1
r : α → α → Prop
a : α
h : r a a
⊢ IsChain r (replicate 0 a)

case one
α : Type u_1
r : α → α → Prop
a : α
h : r a a
⊢ IsChain r (replicate 1 a)

case more
α : Type u_1
r : α → α → Prop
a : α
h : r a a
n✝ : ℕ
a✝¹ : IsChain r (replicate n✝ a)
a✝ : IsChain r (replicate (n✝ + 1) a)
⊢ IsChain r (replicate (n✝ + 2) a)
Module: Mathlib.Data.List.Rotate

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

Tactic:
by
  rw [← Option.some_inj, ← getElem?_eq_getElem, ← getElem?_eq_getElem, getElem?_rotate]
  exact h.trans_eq (length_rotate _ _)

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

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

Tactic:
← length_reverse

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g
a : ↥s
x✝¹ : a ∈ ↑s.attach
b : ↥s
x✝ : b ∈ ↑s.attach
hab : a ≠ b
x : γ
hxa : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) a
hxb : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) b
⊢ False

Tactic:
obtain ⟨xa, hfa, hga⟩ := mem_disjiUnion.mp hxa

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g
a : ↥s
x✝¹ : a ∈ ↑s.attach
b : ↥s
x✝ : b ∈ ↑s.attach
hab : a ≠ b
x : γ
hxa : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) a
hxb : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) b
xa : β
hfa : xa ∈ f ↑a
hga : x ∈ g xa
⊢ False
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g
a : ↥s
x✝¹ : a ∈ ↑s.attach
b : ↥s
x✝ : b ∈ ↑s.attach
hab : a ≠ b
x : γ
hxa : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) a
hxb : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) b
xa : β
hfa : xa ∈ f ↑a
hga : x ∈ g xa
xb : β
hfb : xb ∈ f ↑b
hgb : x ∈ g xb
⊢ xa ≠ xb

Tactic:
rintro rfl

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g
a : ↥s
x✝¹ : a ∈ ↑s.attach
b : ↥s
x✝ : b ∈ ↑s.attach
hab : a ≠ b
x : γ
hxa : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) a
hxb : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) b
xa : β
hfa : xa ∈ f ↑a
hga : x ∈ g xa
hfb : xa ∈ f ↑b
hgb : x ∈ g xa
⊢ False
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ ↑l₁ ×ˢ ↑l₂ = ↑(l₁ ×ˢ l₂)

Tactic:
dsimp only [SProd.sprod]

Goal state after:
α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ (↑l₁).product ↑l₂ = ↑(l₁.product l₂)
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ↑(map { toFun := Prod.swap, inj' := ⋯ } (t ×ˢ s)) = ↑(s ×ˢ t)

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ⇑{ toFun := Prod.swap, inj' := ⋯ } '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ ↑(image Prod.swap (t ×ˢ s)) = ↑(s ×ˢ t)

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ Prod.swap '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ ↑(s ∩ t).offDiag = ↑(s.offDiag ∩ t.offDiag)

Tactic:
push_cast

Goal state after:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (↑s ∩ ↑t).offDiag = (↑s).offDiag ∩ (↑t).offDiag
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ ↑(s ∪ t).offDiag = ↑(s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s)

Tactic:
push_cast

Goal state after:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ (↑s ∪ ↑t).offDiag = (↑s).offDiag ∪ (↑t).offDiag ∪ ↑s ×ˢ ↑t ∪ ↑t ×ˢ ↑s
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
⊢ #u = (#s).choose 2

Tactic:
set v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}

Goal state after:
α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
⊢ #u = (#s).choose 2
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
by
  rw [Nat.mul_comm]
  apply Nat.mul_right_cancel (n + k - k).factorial_pos
  rw [choose_mul_factorial_mul_factorial <| Nat.le_add_left k n, Nat.add_sub_cancel_right,
    ← factorial_mul_ascFactorial, Nat.mul_comm]

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

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

Tactic:
simp [multichoose]

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ (n✝ + 1).multichoose 0 = 1

Tactic:
simp [multichoose]

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

Goal state before:
pp: k : ℕ
⊢ multichoose 0 (k + 1) = 0

Tactic:
simp [multichoose]

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1).multichoose (k + 1) = n.multichoose (k + 1) + (n + 1).multichoose k

Tactic:
simp [multichoose]

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin (n + 1) → Set α
⊢ ⋃ i, f i = iUnion (f ∘ Fin.castSucc) ∪ f (Fin.last n)

Tactic:
cases f using Fin.snocCases

Goal state after:
case snoc
α : Type u_1
n : ℕ
xs✝ : Fin n → Set α
x✝ : Set α
⊢ ⋃ i, Fin.snoc xs✝ x✝ i = iUnion (Fin.snoc xs✝ x✝ ∘ Fin.castSucc) ∪ Fin.snoc xs✝ x✝ (Fin.last n)
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
by
    have : n + (k + 1) < (n + 1) + (k + 1) := Nat.add_lt_add_right (Nat.lt_succ_self _) _
    have : (n + 1) + k < (n + 1) + (k + 1) := Nat.add_lt_add_left (Nat.lt_succ_self _) _
    rw [multichoose_succ_succ, Nat.add_comm, Nat.succ_add_sub_one, ← Nat.add_assoc,
      Nat.choose_succ_succ]
    simp [multichoose_eq n (k + 1), multichoose_eq (n + 1) k]

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

Goal state before:
pp: S : Type u_3
M : Type u_4
inst✝² : SetLike S M
inst✝¹ : Mul M
inst✝ : MulMemClass S M
s : S
⊢ IsMulCommutative ↥s ↔ ∀ (a : M), a ∈ s → ∀ (b : M), b ∈ s → a * b = b * a

Tactic:
simp [isMulCommutative_iff]

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
a : α
s : Set α
⊢ (insert a s)⁻¹ = insert a⁻¹ s⁻¹

Tactic:
insert_eq,

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
a : α
s : Set α
⊢ ({a} ∪ s)⁻¹ = insert a⁻¹ s⁻¹
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ a⁻¹ * x) '' s ∩ t)⁻¹.Nonempty ↔ ((fun x ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
inter_inv

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ (((fun x ↦ a⁻¹ * x) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun x ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ x * a⁻¹) '' s ∩ t)⁻¹.Nonempty ↔ ((fun x ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
inter_inv

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ (((fun x ↦ x * a⁻¹) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun x ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty
Module: Mathlib.Algebra.Group.Submonoid.Basic

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

Tactic:
insert_eq,

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ closure ({1} ∪ s) = closure s