mathlib-initiative/mathlib-tactics huggingface dataset:
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
ha : 0 ≤ a
⊢ ↑⌈a⌉₊ = ↑↑⌈a⌉₊

Tactic:
Int.cast_natCast

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ ↑⌈a⌉₊ = ↑⌈a⌉₊
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
ha : -1 < a
⊢ ↑⌈a⌉₊ = ↑↑⌈a⌉₊

Tactic:
Int.cast_natCast

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : -1 < a
⊢ ↑⌈a⌉₊ = ↑⌈a⌉₊
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: M : Type u_6
inst✝ : CommMonoid M
u₁ u₂ : Mˣ
⊢ u₁ • u₂ = u₁ * u₂

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
q : ℚ
⊢ q ≤ ↑q

Tactic:
by rw [Rat.cast_id]

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

Goal state before:
pp: α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
⊢ ∀ (s : Multiset α), p s

Tactic:
by
  rintro ⟨l⟩; induction l with | nil => exact empty | cons _ _ ih => exact cons _ _ ih

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ a ∈ l.dedup ↔ a ∈ l

Tactic:
by
  have := not_congr (@forall_mem_pwFilter α (· ≠ ·) _ ?_ a l)
  · simpa only [dedup, forall_mem_ne, not_not] using this
  · intro x y z xz
    exact not_and_or.1 <| mt (fun h ↦ h.1.trans h.2) xz

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

Goal state before:

Tactic:
s.map f = s.pmap (fun x _ => f x) fun _ => id := by rw [pmap_eq_map]
    _ = s.attach.map fun x => f x.1 := by rw [pmap_eq_map_attach]
    _ = t.map g := by rw [this, Multiset.map_map]; exact map_congr rfl fun x _ => h _ _

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = List.insert a (l₁ ∪ l₂.dedup)

Tactic:
← IH,

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = List.insert a (l₁ ++ l₂).dedup
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : ∀ (a : α), count a (M + N) = count a (P + Q)
x : α
⊢ count x M + count x N = count x P + count x Q

Tactic:
simp_all only [Multiset.count_add]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
⊢ count (f x) (map f s) = count x s

Tactic:
rw [count_eq_zero_of_notMem H, count_eq_zero, mem_map]

Goal state after:
case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
⊢ ¬∃ a, a ∈ s ∧ f a = f x
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b ≍ a
st : s ++ r ≍ t
⊢ ∃ l, l ∈ t.inits ∧ a :: l = b :: s

Tactic:
rw [eq_of_heq ba]

Goal state after:
α : Type u_1
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b ≍ a
st : s ++ r ≍ t
⊢ ∃ l, l ∈ t.inits ∧ a :: l = a :: s
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = (a ::ₘ s.val).dedup

Tactic:
rw [dedup_cons, dedup_eq_self]; rfl

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ Subsingleton (Fin n) ↔ n = 1

Tactic:
subsingleton_iff_le_one,

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ n ≤ 1 ↔ n = 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j k : Fin n
⊢ ↑↑j < ↑↑k ↔ j < k

Tactic:
simp only [coe_eq_castSucc, castSucc_lt_castSucc_iff]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
constructor
  · rw [card_eq_succ]
    grind [card_eq_one]
  · grind

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

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

Tactic:
refine Fintype.card_of_subtype _ ?_

Goal state after:
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { a // p a }
inst✝ : DecidablePred p
⊢ ∀ (x : α), x ∈ {x | p x} ↔ p x
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
rcases rev_surjective i with ⟨i, rfl⟩

Goal state after:
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
⊢ append xs ys i.rev.rev = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i.rev)
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case cons
α : Type u_1
l : List α
x : α
l' l₁✝ l₂✝ : List α
y : α
a✝ : l₁✝ <+ l₂✝
IH : x ∈+ l₁✝ → x ∈+ l₂✝
hx : x ∈+ l₁✝
⊢ x ∈+ y :: l₂✝

Tactic:
exact (IH hx).duplicate_cons _

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ card α = 1 ↔ ∃ x, ∀ (y : α), y = x

Tactic:
by
  rw [← card_unit, card_eq]
  exact
    ⟨fun ⟨a⟩ => ⟨a.symm (), fun y => a.injective (Subsingleton.elim _ _)⟩,
     fun ⟨x, hx⟩ =>
      ⟨⟨fun _ => (), fun _ => x, fun _ => (hx _).trans (hx _).symm, fun _ =>
          Subsingleton.elim _ _⟩⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
e : α ↪ α
⊢ e.equivOfFiniteSelfEmbedding.toEmbedding = e

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Refl r
x : α
xs : List α
⊢ (orderedInsert r x xs).erase x = xs

Tactic:
induction xs

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Refl r
x : α
⊢ (orderedInsert r x []).erase x = []

case cons
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Refl r
x head✝ : α
tail✝ : List α
tail_ih✝ : (orderedInsert r x tail✝).erase x = tail✝
⊢ (orderedInsert r x (head✝ :: tail✝)).erase x = head✝ :: tail✝
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
x : α
xs : List α
hx : ¬x ∈ xs
⊢ (orderedInsert r x xs).erase x = xs

Tactic:
induction xs

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
x : α
hx : ¬x ∈ []
⊢ (orderedInsert r x []).erase x = []

case cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
x head✝ : α
tail✝ : List α
tail_ih✝ : ¬x ∈ tail✝ → (orderedInsert r x tail✝).erase x = tail✝
hx : ¬x ∈ head✝ :: tail✝
⊢ (orderedInsert r x (head✝ :: tail✝)).erase x = head✝ :: tail✝
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
x : α
xs : List α
⊢ xs <+ orderedInsert r x xs

Tactic:
induction xs

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
x : α
⊢ [] <+ orderedInsert r x []

case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
x head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ <+ orderedInsert r x tail✝
⊢ head✝ :: tail✝ <+ orderedInsert r x (head✝ :: tail✝)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_3
⊢ (insertNthEquiv α 0).symm = (consEquiv α).symm

Tactic:
ext <;> rfl

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
x : γ
xs : Finset γ
hx : x ∉ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ fold op b f (image g (cons x xs hx)) = fold op b (f ∘ g) (cons x xs hx)

Tactic:
rw [fold_cons, cons_eq_insert, image_insert, fold_insert_idem, ih]

Goal state after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
x : γ
xs : Finset γ
hx : x ∉ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ op (f (g x)) (fold op b (f ∘ g) xs) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Bool
h : (find? p).isSome = true
⊢ find? p = some (Fin.find (fun x ↦ p x = true) ⋯)

Tactic:
simp_rw [find?_eq_dite, exists_eq_true_of_isSome_find? h, dite_true]

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

Goal state before:
pp: α : 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 : β
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)

Tactic:
by
  classical
    induction s using Finset.induction_on with
    | empty => simp
    | insert a s ha IH =>
      rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
      simp

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

Goal state before:
pp: case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (map (map fun x ↦ a + x) l.ranges)

Tactic:
rw [pairwise_map]
      apply Pairwise.imp _ hl
      intro u v
      apply disjoint_map
      exact fun u v => Nat.add_left_cancel

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
⊢ l₁.prod ∣ l₂.prod

Tactic:
hl.prod_eq,

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
⊢ l₁.prod ∣ (l₁ ++ l).prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
⊢ m - (l.length - n % l.length) = (m + n) % l.length

Tactic:
have : n % length l + m - length l < length l := by
        rw [Nat.sub_lt_iff_lt_add hm']
        exact Nat.add_lt_add hlt hml

Goal state after:
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
⊢ m - (l.length - n % l.length) = (m + n) % l.length
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
a : ι
h : a ∈ m
⊢ f a * (map f (m.erase a)).prod = (map f m).prod

Tactic:
by
  rw [← m.coe_toList, coe_erase, map_coe, map_coe, prod_coe, prod_coe,
    List.prod_map_erase f (mem_toList.2 h)]

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

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
n : ℕ
⊢ ((n + 1) • m).prod = m.prod ^ (n + 1)

Tactic:
rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l ~r l' ↔ ∃ a, a < l.length + 1 ∧ l.rotate a = l'

Tactic:
isRotated_iff_mod

Goal state after:
α : Type u
l l' : List α
⊢ (∃ n, n ≤ l.length ∧ l.rotate n = l') ↔ ∃ a, a < l.length + 1 ∧ l.rotate a = l'
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r (List.map f l₁).rotate n

Tactic:
use n

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

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ (a :: l).offDiag ~ map (fun x ↦ (a, x)) l ++ map (fun x ↦ (x, a)) l ++ l.offDiag

Tactic:
by
  simp only [offDiag, zipIdx_cons']
  have : map (fun x ↦ (x.fst, a)) l.zipIdx = map (·, a) l := by
    conv_rhs => rw [← zipIdx_map_fst 0 l, map_map, Function.comp_def]
  simp [append_assoc, perm_append_left_iff, flatMap_map,
    ← (map_append_flatMap_perm _ _ _).congr_left, this]

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

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

pp: case H
n : ℕ
⊢ 0 < 2

Tactic:
Nat.mul_comm 2 n,

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

case H
n : ℕ
⊢ 0 < 2
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (x, y) ∈ l.offDiag ↔ (x, y).fst ∈ l ∧ (x, y).snd ∈ l ∧ (x, y).fst ≠ (x, y).snd

Tactic:
simp_rw [mem_offDiag_iff_getElem, mem_iff_getElem, Ne]

Goal state after:
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y) ↔ (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
x : δ a
h : x ∈ t a
f : (b : α) → a ≠ b → δ b
hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b
⊢ ∃ a_1 ∈ piFinset t, a_1 a = x

Tactic:
exact ⟨fun b ↦ if h : a = b then h ▸ x else f _ h, by aesop, by simp⟩

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

Goal state before:
pp: r n : ℕ
h : r < n / 2
⊢ n.choose r ≤ n.choose (r + 1)

Tactic:
refine Nat.le_of_mul_le_mul_right ?_ (Nat.sub_pos_of_lt (h.trans_le (n.div_le_self 2)))
  rw [← choose_succ_right_eq]
  apply Nat.mul_le_mul_left
  rw [← Nat.lt_iff_add_one_le, Nat.lt_sub_iff_add_lt, ← Nat.mul_two]
  exact lt_of_lt_of_le (Nat.mul_lt_mul_of_pos_right h Nat.zero_lt_two) (n.div_mul_le_self 2)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SMul α β
a : α
S : Set (Set β)
⊢ a • ⋃ i ∈ S, i = ⋃ s ∈ S, a • s

Tactic:
smul_set_iUnion₂

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : SMul α β
a : α
S : Set (Set β)
⊢ ⋃ i ∈ S, a • i = ⋃ s ∈ S, a • s
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' ⋃ i ∈ s, {i} = f ⁻¹' s

Tactic:
biUnion_of_singleton

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = f ⁻¹' s
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
⊢ Pairwise fun i j ↦ ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y)

Tactic:
intro i j hij x y; ext k
  by_cases i = k <;> simp_all

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

Goal state before:
pp: α : Type u_2
inst✝ : CancelMonoid α
s : Set α
hs : s.Nontrivial
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (s ^ (n + 2)).Nontrivial

Tactic:
simpa [pow_succ] using (hs.pow n.succ_ne_zero).mul hs

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

Goal state before:
pp: N : Type u_5
inst✝ : Group N
K : Subgroup N
⊢ comap (MonoidHom.id N) K = K

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
e : G ≃* G'
⊢ H.equivMapOfInjective ↑e ⋯ = e.subgroupMap H

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: case mp.refine_3
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
y₁ : G
hy₁ : y₁ ∈ s
z₁ : G
hz₁ : z₁ ∈ t
hx✝ : y₁ * z₁ ∈ closure (↑s ∪ ↑t)
y₂ : G
hy₂ : y₂ ∈ s
z₂ : G
hz₂ : z₂ ∈ t
hy✝ : y₂ * z₂ ∈ closure (↑s ∪ ↑t)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = y₁ * z₁ * (y₂ * z₂)

Tactic:
exact ⟨y₁ * y₂, s.mul_mem hy₁ hy₂,
            (y₂⁻¹ * z₁ * y₂) * z₂, t.mul_mem (ht.conj_mem' z₁ hz₁ y₂) hz₂, by simp [mul_assoc]⟩

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
S : Submonoid M
e : M ≃* N
⊢ S.equivMapOfInjective ↑e ⋯ = e.submonoidMap S

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: case pos
a b : ℕ
h : a < b
⊢ unpair (b * b + a) = (a, b)

Tactic:
have be : sqrt (b * b + a) = b := sqrt_add_eq _ (le_trans (le_of_lt h) (Nat.le_add_left _ _))

Goal state after:
case pos
a b : ℕ
h : a < b
be : (b * b + a).sqrt = b
⊢ unpair (b * b + a) = (a, b)
Module: Mathlib.Data.Nat.Pairing

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

Tactic:
by
  let s := sqrt n
  simp only [unpair]
  by_cases h : n - s * s < s <;> simp only [h, ↓reduceIte, gt_iff_lt, s]
  · exact lt_of_lt_of_le h (sqrt_le_self _)
  · simp only [not_lt] at h
    have s0 : 0 < s := sqrt_pos.2 n1
    exact lt_of_le_of_lt h (Nat.sub_lt n1 (Nat.mul_pos s0 s0))

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
⊢ r (f a) (f (Directed.sequence f hf (encode a + 1)))

Tactic:
simp only [Directed.sequence, encodek]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
⊢ r (f a) (f (Classical.choose ⋯))
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
xs : List (FreeMonoid α)
⊢ toList xs.prod = (List.map (⇑toList) xs).flatten

Tactic:
induction xs

Goal state after:
case nil
α : Type u_1
⊢ toList [].prod = (List.map ⇑toList []).flatten

case cons
α : Type u_1
head✝ : FreeMonoid α
tail✝ : List (FreeMonoid α)
tail_ih✝ : toList tail✝.prod = (List.map (⇑toList) tail✝).flatten
⊢ toList (head✝ :: tail✝).prod = (List.map (⇑toList) (head✝ :: tail✝)).flatten
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case of_mul
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : ∀ (h : (FreeMonoid.lift Subtype.val) y ∈ closure s), motive ((FreeMonoid.lift Subtype.val) y) h
h : (FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y) ∈ closure s
⊢ motive ((FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y)) h

Tactic:
| of_mul x y ih =>

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
l : FreeMonoid { x // x ∈ s }
h : (FreeMonoid.lift Subtype.val) l ∈ closure s
⊢ motive ((FreeMonoid.lift Subtype.val) l) h

Tactic:
induction l using FreeMonoid.inductionOn' with
  | one => exact one
  | of_mul x y ih =>
    simp only [map_mul, FreeMonoid.lift_eval_of]
    refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)
    simp only [closure_eq_mrange, mem_mrange, exists_apply_eq_apply]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
    (Option.rec (some hd) (fun val ↦ if r hd val then some hd else some val) (foldl (argAux r) o tl) = none ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)

Tactic:
cases foldl (argAux r) o tl

Goal state after:
case none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (none = none ↔ tl = [] ∧ o = none) →
    (Option.rec (some hd) (fun val ↦ if r hd val then some hd else some val) none = none ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)

case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
⊢ (some val✝ = none ↔ tl = [] ∧ o = none) →
    (Option.rec (some hd) (fun val ↦ if r hd val then some hd else some val) (some val✝) = none ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : f hd < f val✝
hm : some val✝ = some m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

Tactic:
injection hm with hm

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : f hd < f val✝
hm : val✝ = m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : ¬f hd < f val✝
hm : some hd = some m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

Tactic:
injection hm with hm

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : ¬f hd < f val✝
hm : hd = m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
hm : some val✝ = some m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
injection hm with hm

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
hm : val✝ = m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
hm : some hd = some m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
injection hm with hm

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
hm : hd = m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ some (ofNat (Sigma γ) n) = some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩

Tactic:
rw [← decode_eq_ofNat, decode_sigma_val]; simp

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑s
⊢ toFunAux x = #({y ∈ range ↑x | y ∈ s})

Tactic:
rw [toFunAux, List.countP_eq_length_filter]

Goal state after:
s : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑s
⊢ (List.filter (fun x ↦ decide (x ∈ s)) (List.range ↑x)).length = #({y ∈ range ↑x | y ∈ s})