mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ ↑q.num < (q - fract q + 1) * ↑q.den

Tactic:
have : (q - fract q + 1) * q.den = q.num + (1 - fract q) * q.den := by
      calc
        (q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
        _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
        _ = q.num + (1 - fract q) * q.den := by simp

Goal state after:
q : ℚ
this✝ : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
this : (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den
⊢ ↑q.num < (q - fract q + 1) * ↑q.den
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.den - q.num * ⌊q_inv⌋ < q.num
⊢ (↑q.den - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs

Tactic:
have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm

Goal state after:
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.den - q.num * ⌊q_inv⌋ < q.num
tmp : (↑q.den - ↑q.num.natAbs * ⌊↑q.den / ↑q.num.natAbs⌋).natAbs.Coprime q.num.natAbs
⊢ (↑q.den - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G✝ : Type u_1
M : Type u_2
A✝ : Type u_3
B✝ : Type u_4
α : Type u_5
β : Type u_6
G : Type u_7
A : Type u_8
B : Type u_9
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
x y : G
f : A → B
⊢ (fun a ↦ f ((x * y)⁻¹ • a)) = fun a ↦ f (y⁻¹ • x⁻¹ • a)

Tactic:
simp only [mul_smul, mul_inv_rev]

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

Goal state before:
pp: case refine_2
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ 1 / δ ≤ ↑m

Tactic:
· exact (le_add_of_nonneg_left <| by positivity).trans hm

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]
    rintro ⟨s, hla, h⟩
    rwa [perm_singleton.mp hla, sublist_singleton] at h

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

Goal state before:
pp: α : Type u_1
s : Multiset α
n : ℕ
⊢ s.card = n + 1 ↔ ∃ a t, a ::ₘ t = s ∧ t.card = n

Tactic:
by
  refine ⟨?_, by aesop⟩
  induction s using Multiset.induction generalizing n with aesop

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

Goal state before:
pp: case refine_3
α : Type u_1
l : List α
⊢ range (some ∘ l.get) ⊆ range fun x ↦ l[x]?

Tactic:
· exact range_subset_iff.2 fun k => ⟨_, getElem?_eq_getElem _⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
h : s ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t

Tactic:
rw [← cons_erase m] at h; exact (cons_le_cons_iff _).1 h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
ih : 0 - s = 0
⊢ 0 - a ::ₘ s = 0

Tactic:
by simp [ih]

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

Goal state before:
pp: α : Type u
β : Type v
l₁ : List α
f : α → List β
⊢ (flatMap f l₁).Nodup ↔ (∀ (x : α), x ∈ l₁ → (f x).Nodup) ∧ Pairwise (Disjoint on f) l₁

Tactic:
simp only [List.flatMap, nodup_flatten, pairwise_map, and_comm, mem_map,
    exists_imp, and_imp]
  rw [show (∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔ ∀ x : α, x ∈ l₁ → Nodup (f x)
      from forall_comm.trans <| forall_congr' fun _ => forall_eq']

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

Tactic:
by
    by_cases h : b ∈ l₂
    · simp [h]
    · simpa [h] using bagInter_nil_iff_inter_nil l₁ l₂

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ l <:+ List.insert a l

Tactic:
by_cases h : a ∈ l
  · simp only [insert_of_mem h, suffix_refl]
  · simp only [insert_of_not_mem h, suffix_cons]

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

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ ({ toFun := fun f ↦ (fun i ↦ f (Sum.inl i), fun i' ↦ f (Sum.inr i')), invFun := fun g t_1 ↦ Sum.rec g.1 g.2 t_1,
              left_inv := ⋯, right_inv := ⋯ }.symm.trans
        (piCongrLeft' (fun i ↦ α ↑i) (Finset.union s t h).symm).symm)
      (f, g) ⟨i, hi'⟩ =
    f ⟨i, hi⟩

Tactic:
piCongrLeft',

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ ({ toFun := fun f ↦ (fun i ↦ f (Sum.inl i), fun i' ↦ f (Sum.inr i')), invFun := fun g t_1 ↦ Sum.rec g.1 g.2 t_1,
              left_inv := ⋯, right_inv := ⋯ }.symm.trans
        { toFun := fun f x ↦ f ((Finset.union s t h).symm.symm x),
            invFun := fun f x ↦ ⋯ ▸ f ((Finset.union s t h).symm x), left_inv := ⋯, right_inv := ⋯ }.symm)
      (f, g) ⟨i, hi'⟩ =
    f ⟨i, hi⟩
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ ({ toFun := fun f ↦ (fun i ↦ f (Sum.inl i), fun i' ↦ f (Sum.inr i')), invFun := fun g t_1 ↦ Sum.rec g.1 g.2 t_1,
              left_inv := ⋯, right_inv := ⋯ }.symm.trans
        (piCongrLeft' (fun i ↦ α ↑i) (Finset.union s t h).symm).symm)
      (f, g) ⟨i, hi'⟩ =
    g ⟨i, hi⟩

Tactic:
piCongrLeft',

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ ({ toFun := fun f ↦ (fun i ↦ f (Sum.inl i), fun i' ↦ f (Sum.inr i')), invFun := fun g t_1 ↦ Sum.rec g.1 g.2 t_1,
              left_inv := ⋯, right_inv := ⋯ }.symm.trans
        { toFun := fun f x ↦ f ((Finset.union s t h).symm.symm x),
            invFun := fun f x ↦ ⋯ ▸ f ((Finset.union s t h).symm x), left_inv := ⋯, right_inv := ⋯ }.symm)
      (f, g) ⟨i, hi'⟩ =
    g ⟨i, hi⟩
Module: Mathlib.Data.Fin.Basic

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

Tactic:
Int.emod_eq_add_self_emod,

Goal state after:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑u - ↑↑v + ↑n = (↑↑u - ↑↑v + ↑n) % ↑n
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
by
  rw [castSucc_lt_iff_succ_le, succ_le_succ_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun a ↦ f ↑a ⋯
x : β
hx : x ∈ ↑t
⊢ x ∈ f' '' ↑s.attach

Tactic:
by simpa [f'] using hsurj x hx

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
simp only [exists_and_left]

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (f n)

Tactic:
conv_rhs => rw [hf]

Goal state after:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (seqOfForallFinsetExistsAux P r h' n)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
⊢ g ∘ cons y q = cons (g y) (g ∘ q)

Tactic:
by
  ext j
  by_cases h : j = 0
  · rw [h]
    rfl
  · let j' := pred j h
    have : j'.succ = j := succ_pred j h
    rw [← this, cons_succ, comp_apply, comp_apply, cons_succ]

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

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

Tactic:
| inr h =>

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

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

Tactic:
| inr h =>

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

Goal state before:
pp: case mpr
α : Type u_1
s : Finset α
⊢ (∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) →
    ∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}

Tactic:
· rintro ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩
      exact ⟨a, b, c, {a, b, c}, by simp_all [insert_subset_iff]⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card ↥s
f : α ↪ ↥s
⊢ Set.range ⇑(f.trans (subtype fun x ↦ x ∈ s)) ⊆ ↑s

Tactic:
by simp [Set.range_subset_iff]

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
⊢ ↥hs.toFinset = ↑s

Tactic:
rw [← Finset.coe_sort_coe _, hs.coe_toFinset]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ p j ≍ snoc (fun j ↦ cast ⋯ (p j)) x j.castSucc

pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ snoc (fun j ↦ cast ⋯ (p j)) x j.castSucc ≍ (last n).removeNth (snoc (fun j ↦ cast ⋯ (p j)) x) j

Tactic:
· rw [snoc_castSucc]
    exact (cast_heq _ _).symm

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ snoc (fun j ↦ cast ⋯ (p j)) x j.castSucc ≍ (last n).removeNth (snoc (fun j ↦ cast ⋯ (p j)) x) j
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
⊢ InjOn f s ↔ BijOn f s s

Tactic:
refine ⟨fun h ↦ ⟨hm, h, ?_⟩, BijOn.injOn⟩
  have : Finite s := finite_coe_iff.mpr hs
  exact hm.restrict_surjective_iff.mp (Finite.injective_iff_surjective.mp <| hm.restrict_inj.mpr h)

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

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : r x b
⊢ a :: orderedInsert r x as <+ x :: b :: bs

Tactic:
have hba := pairwise_cons.mp hb |>.left _ (mem_of_cons_sublist ‹a :: as <+ bs›)
        exact absurd (trans_of _ ‹r x b› hba) hr

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
x : α
l : List α
h : IsChain R (x :: l)
y : α
hy : y ∈ l.head?
⊢ R x y

Tactic:
by
  rw [← cons_head?_tail hy] at h
  exact h.rel

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
hl : List.IsChain (flip r) []
acc : ∀ (a : α), a ∈ (↑⟨[], hl⟩).head? → Acc r a
⊢ Acc (List.lex_chains r) ⟨[], hl⟩

Tactic:
apply Acc.intro

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
hl : List.IsChain (flip r) []
acc : ∀ (a : α), a ∈ (↑⟨[], hl⟩).head? → Acc r a
⊢ ∀ (y : List.chains r), List.lex_chains r y ⟨[], hl⟩ → Acc (List.lex_chains r) y
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
hl : List.IsChain (flip r) [a]
hl' : List.IsChain (flip r) []
l' : List.chains r := ⟨[], hl'⟩
⊢ Acc (List.lex_chains r) l'

Tactic:
apply Acc.intro

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
hl : List.IsChain (flip r) [a]
hl' : List.IsChain (flip r) []
l' : List.chains r := ⋯
⊢ ∀ (y : List.chains r), List.lex_chains r y l' → Acc (List.lex_chains r) y
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons.intro.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l✝ : List α
hl' : List.IsChain (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l → ∀ (hl : List.IsChain (flip r) (a :: ↑y)), Acc (List.lex_chains r) ⟨a :: ↑y, hl⟩
hl : List.IsChain (flip r) (a :: ↑l)
⊢ Acc (List.lex_chains r) ⟨a :: ↑l, hl⟩

Tactic:
apply Acc.intro

Goal state after:
case cons.intro.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l✝ : List α
hl' : List.IsChain (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l → ∀ (hl : List.IsChain (flip r) (a :: ↑y)), Acc (List.lex_chains r) ⟨a :: ↑y, hl⟩
hl : List.IsChain (flip r) (a :: ↑l)
⊢ ∀ (y : List.chains r), List.lex_chains r y ⟨a :: ↑l, hl⟩ → Acc (List.lex_chains r) y
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons.intro.intro.nil.nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l✝ : List α
hl' : List.IsChain (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l → ∀ (hl : List.IsChain (flip r) (a :: ↑y)), Acc (List.lex_chains r) ⟨a :: ↑y, hl⟩
hl : List.IsChain (flip r) (a :: ↑l)
hm : List.IsChain (flip r) []
⊢ Acc (List.lex_chains r) ⟨[], hm⟩

Tactic:
apply Acc.intro

Goal state after:
case cons.intro.intro.nil.nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l✝ : List α
hl' : List.IsChain (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l → ∀ (hl : List.IsChain (flip r) (a :: ↑y)), Acc (List.lex_chains r) ⟨a :: ↑y, hl⟩
hl : List.IsChain (flip r) (a :: ↑l)
hm : List.IsChain (flip r) []
⊢ ∀ (y : List.chains r), List.lex_chains r y ⟨[], hm⟩ → Acc (List.lex_chains r) y
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f g : α → Multiset β
⊢ (s.bind fun a ↦ f a + g a) = s.bind f + s.bind g

Tactic:
simp [bind, join]

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

Goal state before:
pp: ι : Type u_2
κ : Type u_3
M : Type u_5
inst✝ : CommMonoid M
m✝ : Multiset ι
n : Multiset κ
f : ι → κ → M
a : ι
m : Multiset ι
ih : (map (fun a ↦ (map (fun b ↦ f a b) n).prod) m).prod = (map (fun b ↦ (map (fun a ↦ f a b) m).prod) n).prod
⊢ (map (fun a ↦ (map (fun b ↦ f a b) n).prod) (a ::ₘ m)).prod =
    (map (fun b ↦ (map (fun a ↦ f a b) (a ::ₘ m)).prod) n).prod

Tactic:
by simp [ih]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (Rel p) (map f s) (map g t)

Tactic:
rw [rel_map]

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (fun a b ↦ Rel p (f a) (g b)) s t
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
have e : (n + 1) * choose n k = choose n (k + 1) * (k + 1) + choose n k * (k + 1) := by
    rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, add_one_mul_choose_eq]
  rw [← Nat.sub_eq_of_eq_add e, Nat.mul_comm, ← Nat.mul_sub_left_distrib, Nat.add_sub_add_right]

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

Goal state before:
pp: case intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
val✝ : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ (univ.pi fun i ↦ ↑(t i)).Finite

Tactic:
classical
    rw [← Fintype.coe_piFinset]
    apply Finset.finite_toSet

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : MulOneClass M
s : Set M
S : Submonoid M
a✝ b✝ : M
ha : a✝ ∈ {1}
hb : b✝ ∈ {1}
⊢ a✝ * b✝ ∈ {1}

Tactic:
push _ ∈ _ at *
        rw [ha, hb, mul_one]

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

Goal state before:
pp: 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 : M
⊢ p x

Tactic:
induction closure.symm ▸ mem_top x using closure_induction with
  | mem _ h => exact mem _ h
  | mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
p₁ p₂ : Submonoid M
⊢ Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1

Tactic:
by
  simp_rw [disjoint_iff_inf_le, SetLike.le_def, mem_inf, and_imp, mem_bot]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 1

Tactic:
rw [Subtype.nontrivial_iff_exists_ne (fun x => x ∈ H) (1 : H)]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ y, ∃ (_ : y ∈ H), y ≠ ↑1) ↔ ∃ x ∈ H, x ≠ 1
Module: Mathlib.Algebra.Group.Subgroup.Lattice

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

Tactic:
closure_union

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
K L : Subgroup N
⊢ comap f K = comap f L → K = L

Tactic:
simp only [le_antisymm_iff, comap_le_comap_of_surjective h, imp_self]

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

Goal state before:
pp: n : ℕ
⊢ pair
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt)
        else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).2 =
    n

Tactic:
let s := sqrt n

Goal state after:
n : ℕ
s : ℕ := n.sqrt
⊢ pair
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt)
        else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).2 =
    n
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n : ℕ
n1 : 1 ≤ n
⊢ (unpair n).1 < n

Tactic:
let s := sqrt n

Goal state after:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
⊢ (unpair n).1 < n
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: A : Type u_2
inst✝ : AddGroup A
x : A
⊢ ⇑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x) = ↑(Subgroup.zpowers (Multiplicative.ofAdd x))

Tactic:
by
  symm
  rw [Equiv.eq_image_iff_symm_image_eq]
  exact ofMul_image_zpowers_eq_zmultiples_ofMul

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

Goal state before:
pp: G : Type u_5
inst✝ : Group G
s t : Set G
⊢ closure (conjugatesOfSet s ∪ conjugatesOfSet t) = closure (conjugatesOfSet s) ⊔ closure (conjugatesOfSet t)

Tactic:
closure_union

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Set β
⊢ (fun x2 ↦ 1 • x2) '' s = s

Tactic:
simp_rw [one_smul, image_id']

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid α
inst✝ : MulAction α β
x✝² x✝¹ : α
x✝ : Set β
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by simp only [← image_smul, image_image, ← mul_smul]

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_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 : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ f (a :: l).prod ≤ (map f (a :: l)).prod

Tactic:
rw [prod_cons, map_cons, prod_cons]
    by_cases hl_empty : l = []
    · simp [hl_empty]
    have hla_restrict : ∀ x, x ∈ l → p x := fun x hx => hl x (mem_cons_of_mem _ hx)
    have hp_sup : p l.prod := prod_induction_nonempty p hp_mul hl_empty hla_restrict
    have hp_a : p a := hl a mem_cons_self
    grw [h_mul a _ hp_a hp_sup, ← ih hl_empty hla_restrict]

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

Goal state before:
pp: case inr.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
i : ι
a b : α i
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

Tactic:
obtain hab | hba := total_of (s i) a b
      · exact Or.inl (Lex.right _ _ hab)
      · exact Or.inr (Lex.right _ _ hba)

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

Goal state before:
pp: case inr.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ ⟨i, a⟩ = ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

Tactic:
obtain hab | rfl | hba := trichotomous_of (s i) a b
      · exact Or.inl (Lex.right _ _ hab)
      · exact Or.inr (Or.inl rfl)
      · exact Or.inr (Or.inr <| Lex.right _ _ hba)

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
⊢ ∀ {a m : α} {o : Option α}, a ∈ l → m ∈ foldl (argAux r) o l → ¬r a m

Tactic:
by
  induction l using List.reverseRecOn with
  | nil => simp
  | append_singleton tl a ih => ?_
  intro b m o hb ho
  rw [foldl_append, foldl_cons, foldl_nil, argAux] at ho
  rcases hf : foldl (argAux r) o tl with - | c
  · rw [hf] at ho
    rw [foldl_argAux_eq_none] at hf
    simp_all [hf.1, hf.2, hr₀.irrefl _]
  rw [hf, Option.mem_def] at ho
  grind +splitIndPred

Goal state after: