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

Goal state before:
pp: n k : ℕ
⊢ (n - k) ^ k * (n - k) ≤ (n - k) * n.descFactorial k

Tactic:
Nat.mul_comm

Goal state after:
n k : ℕ
⊢ (n - k) * (n - k) ^ k ≤ (n - k) * n.descFactorial k
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) * (n - (0 + 1)) < (n - 1) * n.descFactorial 1

Tactic:
descFactorial_one

Goal state after:
n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) * (n - (0 + 1)) < (n - 1) * n
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 2) * (n - (k + 1 + 1)) < (n - (k + 2)) * n.descFactorial (k + 2)

Tactic:
Nat.mul_comm

Goal state after:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) * (n - (k + 1 + 1)) ^ (k + 2) < (n - (k + 2)) * n.descFactorial (k + 2)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n ! * (n + 1).ascFactorial n ≤ (n + n) ^ n * n !

Tactic:
Nat.mul_comm

Goal state after:
n : ℕ
⊢ (n + 1).ascFactorial n * n ! ≤ (n + n) ^ n * n !
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case pos
m k : ℕ+
h : ↑m % ↑k = 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k

Tactic:
have hm : (m : ℕ) > 0 := m.pos
    rw [← Nat.mod_add_div (m : ℕ) (k : ℕ), h, zero_add] at hm ⊢
    simp
    lia

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(round x)| ≤ 1 / 2

Tactic:
rw [round_eq, abs_sub_le_iff]

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2 ∧ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑n * (↑m / ↑n) = ↑n * (↑(m % n) / ↑n + ↑(↑m / ↑n))

Tactic:
mul_div_cancel₀ _ hn'.ne',

Goal state after:
case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑n * (↑(m % n) / ↑n + ↑(↑m / ↑n))
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
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ m, y ^ m ≤ x
M : ℕ
m : ℤ
hm : y ^ m ≤ x
hM : ↑M < m
⊢ y ^ ↑M ≤ x

Tactic:
exact le_trans (zpow_le_zpow_right₀ hy.le hM.le) hm

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

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this✝ : q⁻¹.num < (⌊q⁻¹⌋ + 1) * ↑q⁻¹.den
this : q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den
⊢ q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den

Tactic:
rwa [← sub_lt_iff_lt_add'] at this

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

Goal state before:
pp: case inl
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
hc₀ : 0 < c
hc₁ : c < 1
ha : a ≤ 0
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hb₀ hc₁
    exact ⟨n, ha.trans_lt (zpow_pos hc₀ _), mod_cast hn⟩

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Add G
inst✝² : Add H
a : G
b : H
K : Type u_3
inst✝¹ : VAdd K H
inst✝ : VAddAssocClass K H H
c : K
f : G →+c[a, b] H
x : G
⊢ (c +ᵥ ⇑f) (x + a) = (c +ᵥ ⇑f) x + b

Tactic:
simp [vadd_add_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
⊢ ∀ (a b c : Multiset α), a.Le b → b.Le c → a.Le c

Tactic:
by rintro ⟨l₁⟩ ⟨l₂⟩ ⟨l₃⟩; exact @Subperm.trans _ _ _ _

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

Goal state before:
pp: α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
⊢ r a x

Tactic:
obtain ⟨b, hb1, hb2⟩ := exists_mem_of_rel_of_mem (rel_flip.2 h) hx
      rwa [eq_of_mem_replicate hb1] at hb2

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

Goal state before:
pp: α : Type u
l : List α
u : α
⊢ (l.concat u).Nodup ↔ ¬u ∈ l ∧ l.Nodup

Tactic:
← nodup_reverse

Goal state after:
α : Type u
l : List α
u : α
⊢ (l.concat u).reverse.Nodup ↔ ¬u ∈ l ∧ l.Nodup
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
f g : α → β
s : Multiset α
h : ∀ (x : α), x ∈ s → f x = g x
⊢ map f s = map g s

Tactic:
induction s using Quot.inductionOn

Goal state after:
case h
α : Type u_1
β : Type v
f g : α → β
a✝ : List α
h : ∀ (x : α), x ∈ Quot.mk (⇑(isSetoid α)) a✝ → f x = g x
⊢ map f (Quot.mk (⇑(isSetoid α)) a✝) = map g (Quot.mk (⇑(isSetoid α)) a✝)
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : List α
h : t ⊆ s
⊢ (↑s).dedup = ↑s.dedup

Tactic:
coe_dedup

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : List α
h : t ⊆ s
⊢ ↑s.dedup = ↑s.dedup
Module: Mathlib.Data.List.Infix

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

Tactic:
rintro ⟨_ | _, bs, h⟩ <;> simp_all

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∉ t₁) s) ⊆ t₂ \ t₁

Tactic:
· intro x
      simp only [coe_filter, Set.mem_ofPred_eq, and_imp]
      intro hx hx₂
      exact ⟨Or.resolve_left (h hx) hx₂, hx₂⟩

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Subsingleton α
⊢ s.Nonempty → s = univ

Tactic:
rintro ⟨x, hx⟩

Goal state after:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
⊢ s = univ
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
h : a ≤ b
⊢ ∃ k, k ≤ b ∧ b = a + k

Tactic:
obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k := Nat.exists_eq_add_of_le h
  have hkb : k ≤ b := by lia
  refine ⟨⟨k, hkb.trans_lt b.is_lt⟩, hkb, ?_⟩
  simp [Fin.ext_iff, Fin.val_add, ← hk, Nat.mod_eq_of_lt b.is_lt]

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

Tactic:
by
  cases n
  · lia
  obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k + 1 := Nat.exists_eq_add_of_lt h
  have hkb : k < b := by lia
  refine ⟨⟨k, hkb.trans b.is_lt⟩, hkb, by fin_omega, ?_⟩
  simp [Fin.ext_iff, Fin.val_add, ← hk, Nat.mod_eq_of_lt b.is_lt]

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

Goal state before:
pp: case zero
inst✝ : NeZero 0
⊢ castPred 1 ⋯ = 1

Tactic:
exact subsingleton_one.elim _ 1

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

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

Tactic:
by rw [lt_succ_castPred_iff, le_def]

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ last n
⊢ a.pred ha < b.castPred hb ↔ a ≤ b

Tactic:
rw [lt_castPred_iff, castSucc_pred_lt_iff ha]

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).castLT ⋯

Tactic:
Fin.ext_iff

Goal state after:
n m : ℕ
a b : Fin m
ha : ↑a < n
h : b ≤ a
⊢ ↑(a.castLT ha - b.castLT ⋯) = ↑((a - b).castLT ⋯)
Module: Mathlib.Data.Finset.Card

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

Tactic:
rw [card_union_of_disjoint sdiff_disjoint, Nat.add_sub_cancel_right]

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

Goal state before:
pp: case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (¬Fin.cons x₀ xs 0 ∈ ofFn fun i ↦ xs i) ∧ (ofFn fun i ↦ xs i).Nodup
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs

Tactic:
Fin.cons_zero,

Goal state after:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (¬x₀ ∈ ofFn fun i ↦ xs i) ∧ (ofFn fun i ↦ xs i).Nodup
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ 0 ∉ map { toFun := succ, inj' := ⋯ } univ

Tactic:
by simp [map_eq_image]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ last n ∉ map castSuccEmb univ

Tactic:
by simp [map_eq_image]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ i.predAbove (last (n + 1)) = last n

Tactic:
predAbove_of_castSucc_lt _ _ (castSucc_lt_last _),

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ (last (n + 1)).pred ⋯ = last n
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Finset α
inst✝ : Nonempty α
⊢ (∃ x, s ⊆ {x}) → #s ≤ 1

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case refine_2
α : Type u_1
s : Finset α
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ #s ≤ 1
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 1 < #s ↔ s.Nontrivial

Tactic:
← not_iff_not,

Goal state after:
α : Type u_1
s : Finset α
⊢ ¬1 < #s ↔ ¬s.Nontrivial
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
⊢ Injective (cons x₀ x) ↔ ¬x₀ ∈ Set.range x ∧ Injective x

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ cons_injective_of_injective h.1 h.2⟩
  · rintro ⟨i, hi⟩
    replace h := @h i.succ 0
    simp [hi] at h
  · simpa [Function.comp] using! h.comp (Fin.succ_injective _)

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

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

Tactic:
by
    rintro rfl
    exact Finset.card_univ

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
h : Fintype ↑Set.univ
⊢ card ↑Set.univ = card α

Tactic:
apply Fintype.card_of_finset'

Goal state after:
α : Type u_1
inst✝ : Fintype α
h : Fintype ↑Set.univ
⊢ ∀ (x : α), x ∈ univ ↔ x ∈ Set.univ
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: case step
α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : (n + 2).le 0
⊢ False

Tactic:
cases h;

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

Goal state before:
pp: m n : ℕ
γ : Fin (m + n) → Sort u_3
P : ((i : Fin (m + n)) → γ i) → Prop
h : ∀ (vₘ : (i : Fin m) → γ (castAdd n i)) (vₙ : (j : Fin n) → γ (natAdd m j)), P fun i ↦ addCases vₘ vₙ i
v : (i : Fin (m + n)) → γ i
x✝ : Fin (m + n)
⊢ v x✝ = addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) x✝

Tactic:
exact (addCases_castAdd_natAdd v _).symm

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

Goal state before:
pp: case mpr.refine_1.succ.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

Tactic:
· simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj
          simp [hi, hj]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : ∀ (x : α), f x ∈ s
⊢ s.Infinite

Tactic:
rw [← range_subset_iff] at hf

Goal state after:
α : Type u
β : Type v
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : range f ⊆ s
⊢ s.Infinite
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
c : α
l₁ l₂ : List α
⊢ IsChain R (l₁ ++ c :: l₂) ↔ IsChain R (l₁ ++ [c]) ∧ IsChain R (c :: l₂)

Tactic:
induction l₁ using twoStepInduction generalizing l₂ with

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

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun x1 x2 ↦ x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as ∨ b :: bs = a' :: as
⊢ b ≤ a'

Tactic:
rcases hmas with hmas | hmas

Goal state after:
case cons.cons.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun x1 x2 ↦ x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as
⊢ b ≤ a'

case cons.cons.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun x1 x2 ↦ x1 > x2) (a' :: as)
hmas : b :: bs = a' :: as
⊢ b ≤ a'
Module: Mathlib.Data.List.Rotate

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

Tactic:
induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · rw [rotate_cons_succ, ← rotate_rotate, hn]
      simp

Goal state after:
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:
induction s using Quot.inductionOn

Goal state after:
case h
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
a✝ : List M
hs : Quot.mk (⇑(List.isSetoid M)) a✝ ≠ 0
⊢ (map (⇑f) (Quot.mk (⇑(List.isSetoid M)) a✝)).prod = f (prod (Quot.mk (⇑(List.isSetoid M)) a✝))
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1) * (n + 1 - 1) / 2 = n * (n - 1 + 2) / 2

pp: case H
n : ℕ
⊢ 0 < 2

Tactic:
Nat.add_sub_cancel,

Goal state after:
n : ℕ
⊢ (n + 1) * n / 2 = n * (n - 1 + 2) / 2

case H
n : ℕ
⊢ 0 < 2
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1) * n / 2 = n * (n - 1 + 2) / 2

pp: case H
n : ℕ
⊢ 0 < 2

Tactic:
Nat.mul_comm

Goal state after:
n : ℕ
⊢ n * (n + 1) / 2 = n * (n - 1 + 2) / 2

case H
n : ℕ
⊢ 0 < 2
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: i j : ℕ
⊢ (i + j)! / (j ! * i !) = (i + j)! / (i ! * j !)

Tactic:
Nat.mul_comm

Goal state after:
i j : ℕ
⊢ (i + j)! / (i ! * j !) = (i + j)! / (i ! * j !)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ n ! / ((n - k)! * k !) = n ! / (k ! * (n - k)!)

Tactic:
Nat.mul_comm

Goal state after:
n k : ℕ
hk : k ≤ n
⊢ n ! / (k ! * (n - k)!) = n ! / (k ! * (n - k)!)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ 0 = 0 * (n + 1 - (k + 1))

Tactic:
Nat.zero_mul

Goal state after:
case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ 0 = 0
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
Nat.mul_comm

Goal state after:
n k : ℕ
⊢ (n + 1).ascFactorial k = (n + k).choose k * k !
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
Nat.mul_comm

Goal state after:
n k : ℕ
⊢ n ! * (n + 1).ascFactorial k = n ! * (n + 1).ascFactorial k
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k = k ! * n.choose k

Tactic:
Nat.mul_comm

Goal state after:
case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k = n.choose k * k !
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k * (n - k)! = (n - k)! * n.descFactorial k

Tactic:
Nat.mul_comm

Goal state after:
case inr
n k : ℕ
h : n ≥ k
⊢ (n - k)! * n.descFactorial k = (n - k)! * n.descFactorial k
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:
by
    convert! DFunLike.congr_fun h using 0

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype ↑s
ht : Fintype ↑t
⊢ Fintype ↑(image2 f s t)

Tactic:
rw [← image_prod]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype ↑s
ht : Fintype ↑t
⊢ Fintype ↑((fun x ↦ f x.1 x.2) '' s ×ˢ t)
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑(image2 f s t)

Tactic:
rw [← image_prod]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑((fun x ↦ f x.1 x.2) '' s ×ˢ t)
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
by
  refine ⟨fun h => ?_, ?_⟩
  · simp_rw [Set.Infinite, @and_comm ¬_, ← Classical.not_imp]
    by_contra!
    exact h ((this.1 h.nonempty.snd).prod <| this.2 h.nonempty.fst)
  · rintro (h | h)
    · exact h.1.prod_left h.2
    · exact h.1.prod_right h.2

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

pp: case refine_2
α : 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
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (image2 f s t).Infinite

Tactic:
· rw [← image_uncurry_prod] at h
    exact h.of_image _

Goal state after:
case refine_2
α : 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
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (image2 f s t).Infinite
Module: Mathlib.Algebra.Group.Submonoid.Defs

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝ : Subsingleton M
x y : Submonoid M
i : M
⊢ i ∈ x ↔ i ∈ y

Tactic:
by simp [← Subsingleton.elim 1 i]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
⊢ f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t

Tactic:
rw [sUnion_eq_biUnion, preimage_iUnion₂]

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
a : α
⊢ {a}⁻¹ = {a⁻¹}

Tactic:
by
  rw [← image_inv_eq_inv, image_singleton]

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
rintro ⟨rfl, hn⟩

Goal state after:
case mpr
α : Type u_2
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ∅ ^ n = ∅
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
rintro ⟨rfl, hn⟩

Goal state after:
case mpr
α : Type u_2
inst✝ : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ ∅ ^ n = ∅
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
⊢ ⨆ i, p i = ⨆ i, closure ↑(p i)

Tactic:
Submonoid.closure_eq

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : H = K ⊔ f.ker
⊢ H = K

Tactic:
sup_of_le_left hK

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : H = K
⊢ H = K
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : y.1 = x.1 ∧ ↑x.2 = ↑y.2
⊢ x = y

Tactic:
←
    Subtype.ext_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : y.1 = x.1 ∧ x.2 = y.2
⊢ x = y
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
this : (bit b n >>> 1 >>> m).bodd = (n >>> m).bodd
⊢ (bit b n).testBit m.succ = n.testBit m

Tactic:
← shiftRight_add,

Goal state after:
m : ℕ
b : Bool
n : ℕ
this : (bit b n >>> (1 + m)).bodd = (n >>> m).bodd
⊢ (bit b n).testBit m.succ = n.testBit m
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ decodeSum n = none

Tactic:
simp only [decodeSum, div2_val]

Goal state after:
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ (match n.bodd, n / 2 with
    | false, m => Option.map Sum.inl (decode m)
    | x, m => Option.map Sum.inr (decode m)) =
    none
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
⊢ ∀ (x y : G₂), g (f_inv (x * y)) = g (f_inv x) * g (f_inv y)

Tactic:
by
    intro x y
    rw [← g.map_mul, ← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker]
    apply hg
    rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one, f.map_mul]
    simp only [hf _]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
⊢ ∃ a, f a = d

Tactic:
rcases fs (FreeMonoid.of d) with ⟨b, hb⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
b : FreeMonoid α
hb : (map f) b = of d
⊢ ∃ a, f a = d
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
⊢ ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N

Tactic:
rintro ⟨x, hx⟩

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
x : G
hx : x ∈ N
⊢ (MulAut.conj c) ↑⟨x, hx⟩ ∈ N
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
⊢ Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)

Tactic:
rintro ⟨x, hx⟩

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ ∃ a, (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h) a = ⟨x, hx⟩
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b → Lex r s b a → a = b

Tactic:
rintro _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩) (⟨_, _, hji⟩ | ⟨_, _, hba⟩)
    · exact (asymm hij hji).elim
    · exact (irrefl _ hij).elim
    · exact (irrefl _ hji).elim
    · exact congr_arg (Sigma.mk _ ·) <| antisymm hab hba

Goal state after: