mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
rw [predAbove_of_castSucc_lt _ _ h, succAbove_pred_of_lt _ _ h]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ card α - #{x | p x}.toFinset = card α - card { x // p x }

pp: case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x

Tactic:
Fintype.card_of_subtype

Goal state after:
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ card α - #{x | p x}.toFinset = card α - #?s

case s
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ Finset α

case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ ?s ↔ p x

case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j

Tactic:
· rw [eq_last_of_not_lt h]
    simp

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ x = l.get (f ⟨0, ⋯⟩) ∧ x = l.get (f ⟨1, ⋯⟩)

Tactic:
rw [← hf, ← hf]

Goal state after:
case mp
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ x = (replicate 2 x).get ⟨0, ⋯⟩ ∧ x = (replicate 2 x).get ⟨1, ⋯⟩
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j : Fin (n + 1)
⊢ i.insertNth a f j.rev = i.rev.insertNth a (f ∘ rev) j

Tactic:
induction j using Fin.succAboveCases

Goal state after:
case i
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ Fin (n + 1)

case x
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ i.insertNth a f (rev ?i) = i.rev.insertNth a (f ∘ rev) ?i

case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j✝ : Fin n
⊢ i.insertNth a f (succAbove ?i j✝).rev = i.rev.insertNth a (f ∘ rev) (succAbove ?i j✝)
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → c <+ tail✝ → c <+ insertionSort r tail✝
l₁✝ : List α
hr✝ : Pairwise r (head✝ :: l₁✝)
h : l₁✝ <+ tail✝
hr : ∀ (a' : α), a' ∈ l₁✝ → r head✝ a'
hp : Pairwise r l₁✝
⊢ head✝ :: l₁✝ <+ insertionSort r (head✝ :: tail✝)

Tactic:
exact cons_sublist_orderedInsert (ih hp h) hr

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ ((r c (f a) ∧ r c b) ∧ ∀ x ∈ s, r c (f x)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)

Tactic:
@and_comm (r c (f a)),

Goal state after:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ ((r c b ∧ r c (f a)) ∧ ∀ x ∈ s, r c (f x)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
s : Multiset α
σ : α → Type u_5
t : (a : α) → Multiset (σ a)
l₁ : List α
f : (a : α) → List (σ a)
hf : ∀ (a : α), ⟦f a⟧ = t a
⊢ Nodup (Quot.mk (⇑(List.isSetoid α)) l₁) →
    (∀ (a : α), (t a).Nodup) → (Multiset.sigma (Quot.mk (⇑(List.isSetoid α)) l₁) t).Nodup

Tactic:
simpa [← funext hf] using List.Nodup.sigma

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

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

Tactic:
by
  obtain ⟨l, rfl⟩ : ∃ l, n = l + 1 := Nat.exists_eq_add_of_le' hn
  rfl

Goal state after:
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:
exact Set.offDiag_inter _ _

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

Goal state before:
pp: case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

pp: case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
· simp only [hm, Nat.zero_mul, Nat.choose_eq_zero_iff]
    exact Nat.pos_of_ne_zero hn

Goal state after:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)
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:
exact Set.infinite_prod

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ⋃ y ∈ range f, f ⁻¹' {y} = univ

Tactic:
by
  rw [biUnion_preimage_singleton, preimage_range]

Goal state after:
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:
rw [insert_eq, closure_union, sup_eq_right, closure_singleton_le_iff_mem]
  apply one_mem

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 : Subgroup N
⊢ ⇑f '' ⇑f ⁻¹' ↑H = ↑(f.range ⊓ H)

Tactic:
Set.image_preimage_eq_inter_range,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ ↑H ∩ Set.range ⇑f = ↑(f.range ⊓ H)
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mp.left
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
x : M
hx : x ∈ ↑s
⊢ (inl M N) x ∈ s.prod t

Tactic:
exact ⟨hx, Submonoid.one_mem _⟩

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

Goal state before:
pp: n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
⊢ (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 < n

Tactic:
by_cases h : n - s * s < s

Goal state after:
case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : n - s * s < s
⊢ (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 < n

case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ (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 < n
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
inst✝ : Encodable α
⊢ ∀ (a : Quotient s), Quotient.mk'' <$> decode (encode a.rep) = some a

Tactic:
by
    rintro ⟨l⟩; dsimp; rw [encodek]; exact congr_arg some ⟦l⟧.rep_spec

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ normalizer ↑(comap f H) ≤ comap f (normalizer ↑H)

Tactic:
← map_le_iff_le_comap

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ map f (normalizer ↑(comap f H)) ≤ normalizer ↑H
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.Symm r
inst✝ : ∀ (i : ι), Std.Symm (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b → Lex r s b a

Tactic:
rintro _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩)
    · exact Lex.left _ _ (symm hij)
    · exact Lex.right _ _ (symm hab)

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ ∀ {a_1 b : M}, a_1 ∈ {1, a} → b ∈ {1, a} → a_1 * b ∈ {1, a}

Tactic:
by
      rintro _ _ (rfl | rfl) (rfl | rfl)
      · rw [one_mul]; exact .inl rfl
      · rw [one_mul]; exact .inr rfl
      · rw [mul_one]; exact .inr rfl
      · rw [ha]; exact .inr rfl

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

Goal state before:
pp: x✝ : ℕ
⊢ x✝ ∈ AddSubmonoid.closure {1} ↔ x✝ ∈ ⊤

Tactic:
simp [AddSubmonoid.mem_closure_singleton]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
⊢ toFunAux (ofNat s (n + 1)) = n + 1

Tactic:
have ih : toFunAux (ofNat s n) = n := right_inverse_aux n
    have h₁ : (ofNat s n : ℕ) ∉ {x ∈ range (ofNat s n) | x ∈ s} := by simp
    have h₂ : {x ∈ range (succ (ofNat s n)) | x ∈ s} =
        insert ↑(ofNat s n) {x ∈ range (ofNat s n) | x ∈ s} := by
      simp only [Finset.ext_iff, mem_insert, mem_range, mem_filter]
      exact fun m =>
        ⟨fun h => by
          simp only [h.2, and_true]
          exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1)),
         fun h =>
          h.elim (fun h => h.symm ▸ ⟨lt_succ_self _, (ofNat s n).prop⟩) fun h =>
            ⟨h.1.trans (lt_succ_self _), h.2⟩⟩
    simp only [toFunAux_eq, ofNat] at ih ⊢
    conv =>
      rhs
      rw [← ih, ← card_insert_of_notMem h₁, ← h₂]

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

Goal state before:
pp: case cons.head
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ foldr max ⊥ (x :: l)

Tactic:
simp only [foldr]

Goal state after:
case cons.head
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ max x (foldr max ⊥ l)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ y :: l
⊢ a ≤ max y (foldr max b l)

Tactic:
obtain rfl | hl := mem_cons.mp hx

Goal state after:
case cons.inl
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ x :: l
⊢ a ≤ max x (foldr max b l)

case cons.inr
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ y :: l
hl : x ∈ l
⊢ a ≤ max y (foldr max b l)
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h₂ : 1 < #s
⊢ s.min' ⋯ < s.max' ⋯

Tactic:
rcases one_lt_card.1 h₂ with ⟨a, ha, b, hb, hab⟩

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h₂ : 1 < #s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
⊢ s.min' ⋯ < s.max' ⋯
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    (Array.foldl (fun r l ↦ r.push (x :: l)) y.toList.toArray y.toList.toArray).toList =
      (Array.foldl (fun r l ↦ r.push (x :: l)) y y).toList

Tactic:
· intros; congr

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

Goal state before:
pp: α : Type u
R : α → α → Prop
l : List α
H : Pairwise R l
⊢ Pairwise (Lex R on reverse) l.sublists

Tactic:
by
  have := (pairwise_reverse.2 H).sublists'
  rwa [sublists'_reverse, pairwise_map] at this

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) l.sublists) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) l.sublists)

Tactic:
induction sublists l

Goal state after:
case nil
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) []) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) [])

case cons
α : Type u
β : Type v
f : α → β
a : α
l head✝ : List α
tail✝ : List (List α)
tail_ih✝ :
  flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) tail✝) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) tail✝)
⊢ flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) (head✝ :: tail✝)) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) (head✝ :: tail✝))
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ (𝒫 s).PairwiseDisjoint fun t ↦ {t, insert a t}

Tactic:
pairwiseDisjoint_iff

Goal state after:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ ∀ ⦃i : Set α⦄, i ∈ 𝒫 s → ∀ ⦃j : Set α⦄, j ∈ 𝒫 s → ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i
⊢ s ⊆ t

Tactic:
by
  rintro i hi
  obtain ⟨a, hai⟩ := h₁ i hi
  obtain ⟨j, hj, haj⟩ := mem_iUnion₂.1 (h <| mem_iUnion₂_of_mem hi hai)
  rwa [h₀.eq (subset_union_left hi) (subset_union_right hj)
      (not_disjoint_iff.2 ⟨a, hai, haj⟩)]

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

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs✝ : s.Nonempty
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs : s✝.Nonempty
ih : a ⊓ s✝.sup' hs f = s✝.sup' hs fun i ↦ a ⊓ f i
⊢ a ⊓ (cons a✝ s✝ h✝).sup' ⋯ f = (cons a✝ s✝ h✝).sup' ⋯ fun i ↦ a ⊓ f i

Tactic:
| cons _ _ _ hs ih =>

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case zero
α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n ↦ Nat.recOn n ⋯.choose fun x a ↦ ⋯.choose
⊢ f 0 ∈ s

Tactic:
exact (h _).choose_spec.1

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case succ
α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n ↦ Nat.recOn n ⋯.choose fun x a ↦ ⋯.choose
n✝ : ℕ
⊢ f (n✝ + 1) ∈ s

Tactic:
exact (h _).choose_spec.1

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 ↦ x1 > x2) ↪r r
k : ℕ
⊢ ¬Acc r (f k)

Tactic:
rw [acc_iff_isEmpty_subtype_mem_range, not_isEmpty_iff]
  exact ⟨⟨f, k, rfl⟩⟩

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inl.succ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m x : ℕ
ih : m < m.succ + x → r (f (g m)) (f (g (m.succ + x)))
mn : m < m.succ + (x + 1)
⊢ r (f (g m)) (f (g (m.succ + (x + 1))))

Tactic:
apply IsTrans.trans _ _ _ _ (hr _)

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m x : ℕ
ih : m < m.succ + x → r (f (g m)) (f (g (m.succ + x)))
mn : m < m.succ + (x + 1)
⊢ r (f (g m)) (f (g (m.succ.add x)))
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
⊢ (range f).WellFoundedOn r ↔ WellFounded (r on f)

Tactic:
let f' : β → range f := fun c => ⟨f c, c, rfl⟩

Goal state after:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c ↦ ⟨f c, ⋯⟩
⊢ (range f).WellFoundedOn r ↔ WellFounded (r on f)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c ↦ ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ ∀ {a : β} {b : ↑(range f)}, Subrel r (fun x ↦ x ∈ range f) b (f' a) → ∃ c, f' c = b

pp: case refine_2
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c ↦ ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ Acc (InvImage (Subrel r fun x ↦ x ∈ range f) f') c

Tactic:
· rintro _ ⟨_, c', rfl⟩ -
    exact ⟨c', rfl⟩

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c ↦ ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ Acc (InvImage (Subrel r fun x ↦ x ∈ range f) f') c
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a < b
⊢ #(Ioo a b) = #(Ico a b) - 1

Tactic:
· rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, Nat.zero_sub]

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ g ∈ ↑(Subgroup.center G)

Tactic:
rw [SetLike.mem_coe, Subgroup.mem_center_iff]

Goal state after:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ ∀ (g_1 : G), g_1 * g = g * g_1
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
b c : A i
⊢ x i * (b * c) = x i * b * c

Tactic:
simpa using h2 (update x i b) (update x i c) i

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
e : ι ↪ κ
⊢ (map e s).prod = fun f ↦ ∏ x ∈ s, f (e x)

Tactic:
by
  funext f
  simp

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

Goal state before:
pp: case convert_3
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ι → M i

Tactic:
intro j
    exact Pi.mulSingle j (x j) i

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
a : ι
⊢ {a}.prod = fun f ↦ f a

Tactic:
by
  funext f
  simp

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case refl
α : Type u
L L₁₂ L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
exact ⟨_, _, eq.symm, by rfl, by rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
x✝ : G
⊢ x✝ ∈ (QuotientGroup.con H).subgroup ↔ x✝ ∈ H

Tactic:
simp [QuotientGroup.con, leftRel_apply]

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ s : R
hs : s ∈ ⊥
h : x✝¹ * ↑⟨s, hs⟩ = x✝ * ↑⟨s, hs⟩
⊢ ↑⟨s, hs⟩ * x✝¹ = ↑⟨s, hs⟩ * x✝

Tactic:
Submonoid.mem_bot

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ s : R
hs✝ : s ∈ ⊥
hs : s = 1
h : x✝¹ * ↑⟨s, hs✝⟩ = x✝ * ↑⟨s, hs✝⟩
⊢ ↑⟨s, hs✝⟩ * x✝¹ = ↑⟨s, hs✝⟩ * x✝
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ s : R
hs : s ∈ ⊥
⊢ ↑⟨s, hs⟩ * x✝ = x✝ * ↑⟨s, hs⟩

Tactic:
Submonoid.mem_bot

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ s : R
hs✝ : s ∈ ⊥
hs : s = 1
⊢ ↑⟨s, hs✝⟩ * x✝ = x✝ * ↑⟨s, hs✝⟩
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
h : ∀ j ∈ {i ∈ I | f i = f n}.erase n, g (f j) = 1
⊢ ∏ j ∈ I with f j = f n, g (f j) = g (f n) * 1

Tactic:
← prod_eq_one h,

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
h : ∀ j ∈ {i ∈ I | f i = f n}.erase n, g (f j) = 1
⊢ ∏ j ∈ I with f j = f n, g (f j) = g (f n) * ∏ x ∈ {i ∈ I | f i = f n}.erase n, g (f x)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun x ↦ f x >>= g

Tactic:
rw [ih]

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f >>= g) = -pure x >>= fun x ↦ f x >>= g

Tactic:
rw [ih]

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= fun x ↦ f x >>= g) = -pure x >>= fun x ↦ f x >>= g
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
s : Multiset M
⊢ IsUnit s.prod ↔ ∀ a ∈ s, IsUnit a

Tactic:
by
  induction s using Multiset.induction with
  | empty => simp
  | cons a s ih => simpa using fun _ ↦ ih

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
⊢ IsMulCommutative (G ⧸ N) ↔ _root_.commutator G ≤ N

Tactic:
refine ⟨fun hcomm ↦ ?_, fun hGN ↦ ⟨⟨fun x' y' ↦ ?_⟩⟩⟩

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
⊢ _root_.commutator G ≤ N

case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x' y' : G ⧸ N
⊢ x' * y' = y' * x'
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
t : R
hst : t * ↑s ∈ S
⊢ s • (t • r, ⟨t * ↑s, hst⟩).fst = ↑s • t • (r, s).fst

Tactic:
Submonoid.smul_def

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
t : R
hst : t * ↑s ∈ S
⊢ ↑s • (t • r, ⟨t * ↑s, hst⟩).fst = ↑s • t • (r, s).fst