mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Ioc x y = Ioc (e x) (e y)

Tactic:
by
  rw [← e.preimage_Ioc, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ioc_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case neg
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬S = ∅
⊢ IsGLB S ⟨sInf (Subtype.val '' S), ⋯⟩

Tactic:
exact .of_image Subtype.coe_le_coe <| isGLB_csInf ((Set.nonempty_iff_ne_empty.mpr hS).image _)
        ((Subtype.mono_coe _).map_bddBelow (OrderBot.bddBelow S))

Goal state after:
Module: Mathlib.Tactic.NormNum.Eq

Goal state before:
pp: α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
n✝¹ n✝ : ℕ
h : n✝¹.beq n✝ = false
⊢ ¬↑n✝¹ = ↑n✝

Tactic:
simpa using Nat.ne_of_beq_eq_false h

Goal state after:
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ a % ↑b' = ↑r

Tactic:
simp only [← h, ← hm, Int.add_mul_emod_self_right]

Goal state after:
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ ↑r % ↑b' = ↑r
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
ha : a < 1
⊢ 1 < a⁻ᵐ

Tactic:
by
  rwa [leOnePart_eq_inv.2 ha.le, one_lt_inv']

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

Goal state before:
pp: m n : ℕ
h : 1 < n ∨ 1 < m
⊢ n ! = m ! ↔ n = m

Tactic:
obtain hn | hm := h
  · exact factorial_inj hn
  · rw [eq_comm, factorial_inj hm, eq_comm]

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

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

Tactic:
rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, Nat.mul_left_comm]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
⊢ round 0 = 0

Tactic:
by simp [round]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
⊢ round 1 = 1

Tactic:
by simp [round]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n : ℕ
⊢ round ↑n = ↑n

Tactic:
by simp [round]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n : ℤ
⊢ round ↑n = n

Tactic:
by simp [round]

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

Goal state before:
pp: case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(↑a - ↑b).toPNat' = 1

Tactic:
rw [tsub_eq_zero_iff_le.mpr (le_of_not_gt h : (a : ℕ) ≤ b)]

Goal state after:
case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' 0) = 1
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
⊢ ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)

Tactic:
rintro ⟨hr, hq⟩

Goal state after:
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m k : ℕ+
⊢ m.div k * ↑k + ↑(m.mod k) = ↑m

Tactic:
rw [mul_comm]
  exact div_add_mod _ _

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

Goal state before:
pp: m k : ℕ+
h : k ∣ m
⊢ ↑k * (m.div k).succ = ↑k * m.div k + ↑(m.mod k)

Tactic:
dvd_iff'.mp h,

Goal state after:
m k : ℕ+
h : k ∣ m
⊢ ↑k * (m.div k).succ = ↑k * m.div k + ↑k
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ round x = ⌊↑2 * (x + 1 / 2)⌋ / 2

Tactic:
round_eq_div

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (⌊2 * x⌋ + 1) / 2 = ⌊↑2 * (x + 1 / 2)⌋ / 2
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : a < 1
⊢ StrictAnti fun n ↦ a ^ n

Tactic:
by
  refine strictAnti_int_of_succ_lt fun n ↦ ?_
  rw [zpow_add_one]
  exact mul_lt_of_lt_one_right' (a ^ n) ha

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
⊢ False

Tactic:
rcases exists_zpow_surjective α with ⟨a, ha⟩

Goal state after:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
⊢ False
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
this : -2 ≤ a - 1
⊢ 1 + ↑n * (a - 1) ≤ a ^ n

Tactic:
simpa only [add_sub_cancel] using one_add_mul_le_pow this n

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
hc : ∃ z, fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑(c + 1) - fract (a * ↑(c + 1)) = ↑z

Tactic:
rcases hc with ⟨z, hz⟩
    rw [Nat.cast_add, mul_add, mul_add, Nat.cast_one, mul_one, mul_one]
    rcases fract_add (a * c) a with ⟨y, hy⟩
    use z - y
    rw [Int.cast_sub, ← hz, ← hy]
    abel

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

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

Tactic:
Rat.floor_def'

Goal state after:
n : ℤ
d : ℕ
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
this : ↑(x + 1 / 2) = ↑x + 1 / 2
⊢ ⌊↑x + 1 / 2⌋ = ⌊x + 1 / 2⌋

Tactic:
← this,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
this : ↑(x + 1 / 2) = ↑x + 1 / 2
⊢ ⌊↑(x + 1 / 2)⌋ = ⌊x + 1 / 2⌋
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⁻¹ = q_inv

Tactic:
rw [q_inv_def, inv_def, divInt_eq_div, Int.cast_natCast]

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

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

Tactic:
by_contra! H

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

Goal state before:
pp: case inr.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 : 0 < a
hb₁ : b ≤ 1
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
obtain ⟨n, hn⟩ := exists_pow_btwn_of_lt_mul h hb₀ hb₁ hc₀ hc₁
      exact ⟨n, mod_cast hn⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
⊢ (isSetoid α) _l₁ _l₂ ↔ ∀ (a : α), List.count a _l₁ = List.count a _l₂

Tactic:
apply perm_iff_count

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
⊢ map f s < map f t

Tactic:
refine (map_le_map h.le).lt_of_not_ge fun H => h.ne <| eq_of_le_of_card_le h.le ?_

Goal state after:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ t.card ≤ s.card
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
hal : a ∈ l.dedup
⊢ l.dedup = a :: l'

Tactic:
← this,

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'
this : l.dedup.head! :: l.dedup.tail = l.dedup
hal : a ∈ l.dedup.head! :: l.dedup.tail
⊢ l.dedup = a :: l'
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
a : α
m : Multiset α
⊢ m.toList = [a] ↔ m = {a}

Tactic:
rw [← perm_singleton, ← coe_eq_coe, coe_toList, coe_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ∪ t + u = s + u ∪ (t + u)

Tactic:
simpa [(· ∪ ·), union, eq_comm, Multiset.add_assoc, Multiset.add_left_inj] using
    show s + u - (t + u) = s - t by
      rw [t.add_comm, Multiset.sub_add_eq_sub_sub, Multiset.add_sub_cancel_right]

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

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

Tactic:
rw [Multiset.ext] at h

Goal state after:
α : 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
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ ↑(insert a s) ⊆ ↑(insert a t) ↔ ↑s ⊆ ↑t

Tactic:
simp [ha]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ insert a (insert a s)ᶜ = sᶜ

Tactic:
by
  simp_rw [compl_insert, insert_erase (mem_compl.2 ha)]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.toFinset.Nonempty ↔ s.Nonempty

Tactic:
← Finset.coe_nonempty,

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ (↑s.toFinset).Nonempty ↔ s.Nonempty
Module: Mathlib.Data.Finset.Image

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

Tactic:
by
    push_cast
    exact Set.image_inter_on fun a ha b hb => hf (Or.inr ha) <| Or.inl hb

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

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ #s ≤ #(filter p s) ↔ ∀ x ∈ s, p x

Tactic:
eq_iff_card_le_of_subset (filter_subset p s),

Goal state after:
α : Type u_1
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p s = s ↔ ∀ x ∈ s, p x
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mpr
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
⊢ (∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a) → a ∈ s

Tactic:
rintro ⟨i, hi, rfl⟩

Goal state after:
case mpr
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
i : ℕ
hi : i ∈ range n
⊢ f i ⋯ ∈ s
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ℕ
⊢ castLE h ↑a = ↑(a % m)

Tactic:
by
  ext
  simp only [val_castLE, val_natCast]
  rw [Nat.mod_eq_of_lt (a := a % m) (lt_of_lt_of_le (Nat.mod_lt _ m.pos_of_neZero) h)]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α i.succ
⊢ consCases cons (Fin.cons x₀ x) = cons x₀ x

Tactic:
by
  rw [consCases, cast_eq]
  congr

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

Goal state before:
pp: case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j

Tactic:
← this,

Goal state after:
case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ (g ∘ cons y q) j'.succ = cons (g y) (g ∘ q) j'.succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ append x₀ x i = (cons (x₀ 0) x ∘ Fin.cast ⋯) i

Tactic:
refine Fin.addCases ?_ ?_ i <;> clear i

Goal state after:
case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ ∀ (i : Fin 1), append x₀ x (castAdd n i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n i)

case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ ∀ (i : Fin n), append x₀ x (natAdd 1 i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (natAdd 1 i)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ append x x₀ i = snoc x (x₀ 0) i

Tactic:
refine Fin.addCases ?_ ?_ i <;> clear i

Goal state after:
case refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin n), append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)

case refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin 1), append x x₀ (natAdd n i) = snoc x (x₀ 0) (natAdd n i)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n m : ℕ
α : Sort u_2
xs : Fin n → α
x : α
ys : Fin m → α
⊢ append xs (append (cons x elim0) ys) ∘ Fin.cast ⋯ = append xs (cons x ys) ∘ Fin.cast ⋯

Tactic:
append_left_eq_cons,

Goal state after:
n m : ℕ
α : Sort u_2
xs : Fin n → α
x : α
ys : Fin m → α
⊢ append xs (cons (cons x elim0 0) ys ∘ Fin.cast ⋯) ∘ Fin.cast ⋯ = append xs (cons x ys) ∘ Fin.cast ⋯
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ False

Tactic:
cases h with | step h => cases h;

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
⊢ hs.toFinset.Nonempty ↔ s.Nonempty

Tactic:
← Finset.coe_nonempty,

Goal state after:
α : Type u
s : Set α
hs : s.Finite
⊢ (↑hs.toFinset).Nonempty ↔ s.Nonempty
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ s_1, p ↑s_1 ∧ ↑s_1 ⊆ f '' s) ↔ ∃ s_1, p (f '' ↑s_1) ∧ ↑s_1 ⊆ s

Tactic:
@and_comm (p _),

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ s_1, ↑s_1 ⊆ f '' s ∧ p ↑s_1) ↔ ∃ s_1, ↑s_1 ⊆ s ∧ p (f '' ↑s_1)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ (range f).Finite ↔ Finite α

Tactic:
simpa [finite_univ_iff] using finite_image_iff (s := univ) hf.injOn

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

Goal state before:
pp: case neg
α : 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
ih : orderedInsert r x (a :: as) <+ orderedInsert r x bs
⊢ x :: a :: as <+ b :: orderedInsert r x bs

Tactic:
simp only [hr, orderedInsert_cons, ite_true] at ih

Goal state after:
case neg
α : 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
ih : x :: a :: as <+ orderedInsert r x bs
⊢ x :: a :: as <+ b :: orderedInsert r x bs
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Antisymm r
l₁ l₂ : List α
hp : l₁ <+~ l₂
hs₁ : Pairwise r l₁
hs₂ : Pairwise r l₂
⊢ l₁ <+ l₂

Tactic:
let ⟨_, h, h'⟩ := hp
  exact Sublist.trans (h.eq_of_pairwise' (hs₂.sublist h') hs₁ ▸ Sublist.refl _) h'

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.SortedLE ↔ Pairwise (fun x1 x2 ↦ x1 ≤ x2) l

Tactic:
simp only [sortedLE_iff_monotone_get, monotone_iff_forall_lt, Fin.forall_iff]

Goal state after:
α : Type u_1
l : List α
inst✝ : Preorder α
⊢ (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      ⟨i, h⟩ < ⟨i_1, h_1⟩ → l.get ⟨i, h⟩ ≤ l.get ⟨i_1, h_1⟩) ↔
    Pairwise (fun x1 x2 ↦ x1 ≤ x2) l
Module: Mathlib.Data.List.Lex

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
l₁ l₂ : List α
h : Lex r (a :: l₁) (a :: l₂)
⊢ Lex r l₁ l₂

Tactic:
obtain - | h | h := h; exacts [(irrefl_of r a h).elim, h]

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

Goal state before:
pp: M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
a : M
inst✝ : DecidableEq M
h : a ∈ s
⊢ a * (s.erase a).prod = s.prod

Tactic:
by
  rw [← s.coe_toList, coe_erase, prod_coe, prod_coe, List.prod_erase (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 • m).prod * m.prod = m.prod ^ n * m.prod

Tactic:
prod_nsmul m n

Goal state after:
M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
n : ℕ
⊢ m.prod ^ n * m.prod = m.prod ^ n * m.prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
⊢ l.cyclicPermutations.head? = some l

Tactic:
head?_eq_some_head (cyclicPermutations_ne_nil l),

Goal state after:
α : Type u
l : List α
⊢ some (l.cyclicPermutations.head ⋯) = some l
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case refine_1.refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ s
⊢ x = a

pp: case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b

Tactic:
· exact (eq_inv_of_mul_eq_one_left <| H hx hb).trans (inv_eq_of_mul_eq_one_left <| H ha hb)

Goal state after:
case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set (β → γ)
t : Set (α → β)
u : Set α
⊢ s.seq (t.seq u) = (((fun x1 x2 ↦ x1 ∘ x2) '' s).seq t).seq u

Tactic:
by
  simp only [seq_eq_image2, image2_image_left]
  exact .symm <| image2_assoc fun _ _ _ ↦ rfl

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

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ ↑n ∈ K

Tactic:
rw [zpow_natCast]
    exact pow_mem hx n

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Nontrivial G
⊢ Nontrivial ↥⊤

Tactic:
by
  rw [nontrivial_iff_ne_bot]
  exact top_ne_bot

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

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
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
K : Subgroup G
f : G →* N
g : N →* G
h : LeftInverse ⇑g ⇑f
⊢ RightInverse (⇑g ∘ ⇑f.range.subtype) ⇑f.rangeRestrict

Tactic:
rintro ⟨x, y, rfl⟩
      solve_by_elim

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid M
⊢ ∀ {a b : N}, a ∈ ⇑f '' ↑S → b ∈ ⇑f '' ↑S → a * b ∈ ⇑f '' ↑S

Tactic:
by
    rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
    exact ⟨x * y, S.mul_mem hx hy, by rw [map_mul]⟩

Goal state after:
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 : u ≤ s.prod t
⊢ map (fst M N) u ≤ s

pp: case mp.right
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 : u ≤ s.prod t
⊢ map (snd M N) u ≤ t

Tactic:
· rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).1

Goal state after:
case mp.right
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 : u ≤ s.prod t
⊢ map (snd M N) u ≤ t
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case h
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
N' : Submonoid N
hf : Surjective ⇑f
y : ↥N'
x : M
hx : f x = ↑y
⊢ (f.submonoidComap N') ⟨x, ⋯⟩ = y

Tactic:
apply Subtype.val_injective

Goal state after:
case h
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
N' : Submonoid N
hf : Surjective ⇑f
y : ↥N'
x : M
hx : f x = ↑y
⊢ ↑((f.submonoidComap N') ⟨x, ⋯⟩) = ↑y
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: a b₁ b₂ : ℕ
h : b₁ < b₂
⊢ pair a b₁ < pair a b₂

Tactic:
by_cases h₁ : a < b₁
  · simpa [pair, h₁, Nat.add_assoc, lt_trans h₁ h, h] using mul_self_lt_mul_self h
  · simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]
    by_cases h₂ : a < b₂; swap; · simp [h₂, h]
    simp only [h₂, ↓reduceIte]
    rw [Nat.add_comm, Nat.add_comm _ a, Nat.add_assoc, Nat.add_lt_add_iff_left]
    rwa [Nat.add_comm, ← sqrt_lt, sqrt_add_eq]
    exact le_trans (not_lt.mp h₁) (Nat.le_add_left _ _)

Goal state after:
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
H K : Subgroup G
k : Set G
N : Type u_5
inst✝² : Group N
P : Type u_6
inst✝¹ : Group P
inst✝ : IsMulTorsionFree G
n : ℕ
hn : ¬n = 0
a b : ↥H
this : ↑a ^ n = ↑b ^ n → ↑a = ↑b
⊢ a ^ n = b ^ n → a = b

Tactic:
norm_cast at this

Goal state after:
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
H✝ K : Subgroup G
ι : Sort u_5
H : ι → Subgroup G
inst✝ : ∀ (i : ι), (H i).Characteristic
⊢ (⨅ i, H i).Characteristic

Tactic:
by
  simp_all [characteristic_iff_comap_eq, comap_iInf]

Goal state after:
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
H K✝ : Subgroup G
inst✝ : H.Characteristic
K : Subgroup ↥H
hK : K.Characteristic
⊢ (map H.subtype K).Characteristic

Tactic:
refine characteristic_iff_map_eq.2 fun φ ↦ ?_

Goal state after:
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
H K✝ : Subgroup G
inst✝ : H.Characteristic
K : Subgroup ↥H
hK : K.Characteristic
φ : G ≃* G
⊢ map φ.toMonoidHom (map H.subtype K) = map H.subtype K