mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
hn✝ : n ≠ 0
hn : Odd n ∧ ¬Even n
⊢ a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n

Tactic:
by simp [hn, (hn.1.strictMono_pow (R := R)).injective.eq_iff]

Goal state after:
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : β
ha : a ∈ upperBounds (Prod.snd '' s)
⊢ p.2 ≤ a

pp: case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ upperBounds s

pp: case refine_4
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ lowerBounds (upperBounds s)

Tactic:
· suffices h : (p.1, a) ∈ upperBounds s from (H.2 h).2
    exact fun q hq => ⟨(H.1 hq).1, ha <| mem_image_of_mem _ hq⟩

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ upperBounds s

case refine_4
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
⊢ p ∈ lowerBounds (upperBounds s)
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a ≤ b
⊢ Icc a b ∪ {a} = Icc a b

Tactic:
union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Icc.2 hab)

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a ≤ b
⊢ Icc a b = Icc a b
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (take l₁.length l) l₁

Tactic:
have h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂)) :=
    forall₂_take (length l₁) h
  rwa [take_left] at h'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ a = a' ∨ a ∈ as ↔ b = b' ∨ b ∈ bs

Tactic:
exact rel_or (rel_eq hr h h₁) (rel_mem hr h h₂)

Goal state after:
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₁[m]? = l₂[n]?
hm : m < l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
rw [getElem?_eq_getElem hm, eq_comm, getElem?_eq_some_iff] at h

Goal state after:
case inl
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
h : ∃ h, l₂[n] = l₁[m]
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: n₁ d₁ n₂ d₂ : ℤ
⊢ n₁ /. d₁ / (n₂ /. d₂) = n₁ * d₂ /. (d₁ * n₂)

Tactic:
by
  rw [div_def, inv_divInt, divInt_mul_divInt]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: q : ℚ
⊢ |q| = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }

Tactic:
refine ext ?_ ?_

Goal state after:
case refine_1
q : ℚ
⊢ |q|.num = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.num

case refine_2
q : ℚ
⊢ |q|.den = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.den
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ≥0
⊢ 0 < q.num ↔ 0 < q

Tactic:
by
  simpa [num, -nonpos_iff_eq_zero] using nonpos_iff_eq_zero _ |>.not.symm

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₁.num * ↑q₂.den + q₂.num * ↑q₁.den

Tactic:
apply Int.dvd_add
    <;> apply dvd_mul_of_dvd_right <;> rw [Int.natCast_dvd_natCast]

Goal state after:
case a
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ q₂.den

case a
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ q₁.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
hqd : ↑q.den ≠ 0
⊢ q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)

Tactic:
have hrd : (r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 r.den_pos

Goal state after:
q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
⊢ q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.num * r.den) / ↑(q.den * r.num) = ↑q.num / ↑q.den / (↑r.num / ↑r.den)

pp: case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.den * r.num) ≠ 0

Tactic:
div_eq_mul_inv (_ / _),

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.num * r.den) / ↑(q.den * r.num) = ↑q.num / ↑q.den * (↑r.num / ↑r.den)⁻¹

case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.den * r.num) ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(p.num * ↑q.den) / ↑(↑p.den * q.num) = ↑p.num / ↑p.den / (↑q.num / ↑q.den)

pp: case b0
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(↑p.den * q.num) ≠ 0

Tactic:
div_eq_mul_inv (_ / _),

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(p.num * ↑q.den) / ↑(↑p.den * q.num) = ↑p.num / ↑p.den * (↑q.num / ↑q.den)⁻¹

case b0
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(↑p.den * q.num) ≠ 0
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₂ b₂ c : R
ea eb e : ℕ
x : R
x✝¹ : ea + eb = e
x✝ : a₂ * b₂ = c
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c

Tactic:
by
  subst_vars; simp [pow_add, mul_mul_mul_comm]

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Defs

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
this : InfSet α := { sInf := fun s ↦ if hs : s.Nonempty then ⋯.min s hs else ⊥ }
s : Set α
x✝ : BddBelow s
hn : s.Nonempty
⊢ IsGLB s (sInf s)

Tactic:
by
      simp only [dif_pos hn]
      exact IsLeast.isGLB ⟨h.wf.min_mem s hn, fun _ hx ↦ h.wf.min_le hx⟩

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ C i) → ∃ i, x ∈ range fun x ↦ ↑(f x i)

Tactic:
rintro ⟨i, hx⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
i : ι
hx : x ∈ C i
⊢ ∃ i, x ∈ range fun x ↦ ↑(f x i)
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi a ∩ Iio b = Ioo a b

Tactic:
Ioi_inter_Iio

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioo a b = Ioo a b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
h : S = ∅
⊢ sSup S ≤ a

Tactic:
change ite _ _ _ ≤ a
      simp [h]

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ [[a, b]] = Icc a b ∪ Icc b a

Tactic:
rw [Icc_union_Icc', max_comm]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ [[a, b]] = Icc (min a b) (max a b)

case h₁
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b ≤ b

case h₂
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a ≤ a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c x : α
⊢ x ∈ [[a, c]] → x ∈ [[a, b]] ∪ [[b, c]]

Tactic:
simp only [mem_uIcc, mem_union]
  rcases le_total x b with h2 | h2 <;> tauto

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝ : a ≤ b
⊢ Ι a b = Ioc a b ∪ Ioc b a

Tactic:
simp [uIoc, *]

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝ : b ≤ a
⊢ Ι a b = Ioc a b ∪ Ioc b a

Tactic:
simp [uIoc, *]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ IsLUB ∅ ⟨a, ⋯⟩

Tactic:
simp only [isLUB_empty_iff, isBot_iff_eq_bot]

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ ⟨a, ⋯⟩ = ⊥
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ ⌊a⌋ < z + 1 ∧ ↑z ≤ a ↔ ↑z ≤ a ∧ a < ↑z + 1

Tactic:
floor_lt,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ a < ↑(z + 1) ∧ ↑z ≤ a ↔ ↑z ≤ a ∧ a < ↑z + 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z - ↑y

Tactic:
← hz,

Goal state after:
case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) = fract a * ↑c - fract (a * ↑c) - ↑y
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:
by
  rw [← Int.floor_toNat, Int.toNat_of_nonneg (Int.floor_nonneg.2 ha)]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
Q : Type u_3
inst✝³ : Group G
inst✝² : Torsor G P
inst✝¹ : SMul G Q
inst✝ : SDiv G Q
f : P → Q
hf : Surjective f
smul : ∀ (c : G) (x : P), f (c • x) = c • f x
sdiv : ∀ (x y : P), x /ₛ y = f x /ₛ f y
⊢ ∀ (p₁ p₂ : Q), (p₁ /ₛ p₂) • p₂ = p₁

Tactic:
by simp [hf.forall, ← smul, ← sdiv]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
Q : Type u_3
inst✝³ : Group G
inst✝² : Torsor G P
inst✝¹ : SMul G Q
inst✝ : SDiv G Q
f : P → Q
hf : Surjective f
smul : ∀ (c : G) (x : P), f (c • x) = c • f x
sdiv : ∀ (x y : P), x /ₛ y = f x /ₛ f y
⊢ ∀ (g : G) (p : Q), g • p /ₛ p = g

Tactic:
by simp [hf.forall, ← smul, ← sdiv]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : a ∈ s
⊢ count a s = 1

Tactic:
exact count_eq_one_of_mem d h

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ (range fun x ↦ l[x]?) = insert none (some '' {x | x ∈ l})

Tactic:
rw [← range_list_get, ← range_comp]
  refine (range_subset_iff.2 fun n => ?_).antisymm (insert_subset_iff.2 ⟨?_, ?_⟩)
  · exact (le_or_gt l.length n).imp getElem?_eq_none_iff.mpr
      (fun hlt => ⟨⟨_, hlt⟩, (getElem?_eq_getElem hlt).symm⟩)
  · exact ⟨_, getElem?_eq_none_iff.mpr le_rfl⟩
  · exact range_subset_iff.2 fun k => ⟨_, getElem?_eq_getElem _⟩

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
s t u : Multiset α
r1 : Rel r s t
r2 : Rel r t u
⊢ Rel r s u

Tactic:
by
  induction t using Multiset.induction_on generalizing s u with
  | empty => rw [rel_zero_right.mp r1, rel_zero_left.mp r2, rel_zero_left]
  | cons x t ih =>
    obtain ⟨a, as, ha1, ha2, rfl⟩ := rel_cons_right.mp r1
    obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp r2
    exact Multiset.Rel.cons (_root_.trans ha1 hb1) (ih ha2 hb2)

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ s.card = 1

Tactic:
← card_map,

Goal state after:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ (map ?f s).card = 1

case f
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ α → ?m.41

α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ Type ?u.34
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

Tactic:
rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
l : Multiset α
d : l.Nodup
⊢ a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l

Tactic:
d.erase_eq_filter b,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : Multiset α
d : l.Nodup
⊢ a ∈ Multiset.filter (fun x ↦ x ≠ b) l ↔ a ≠ b ∧ a ∈ l
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.drop n (List.take l₁.length l₂) <+: List.drop n l₂

Tactic:
drop_take

Goal state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.take (l₁.length - n) (List.drop n l₂) <+: List.drop n l₂
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : a ∈ s
⊢ ndinsert a s ≤ t

Tactic:
simp [h, l]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a✝ : α
a b c : Finset α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ⊆ a ⊔ b ⊓ c

Tactic:
by
      simp +contextual only
        [sup_eq_union, inf_eq_inter, subset_iff, mem_inter, mem_union, and_imp,
        or_imp, true_or, imp_true_iff, true_and, or_true]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
⊢ s ∪ {x} = insert x s

Tactic:
by
  rw [Finset.union_comm, singleton_union]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)

Tactic:
by
  simp_rw [erase_eq, disjoint_sdiff_comm]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
h : ∀ x ∈ s, p x
⊢ ∀ (a : α), a ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ a ∈ s

Tactic:
by simpa [subtype_map] using h

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

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ ↑i.rev.modNat = ↑i.modNat.rev

Tactic:
simp only [val_rev]

Goal state after:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ ↑i.rev.modNat = n - (↑i.modNat + 1)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
⊢ Set.MapsTo f ↑(range n) ↑s

Tactic:
by simpa [Set.MapsTo, mem_range] using hf

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.castPred ⋯).predAbove j.succ = j

Tactic:
predAbove_of_castSucc_lt,

Goal state after:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ j.succ.pred ⋯ = j

case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.castPred ⋯).castSucc < j.succ
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case cons
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Tactic:
by_cases hx : x = y

Goal state after:
case pos
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
i : ℕ
⊢ image (f^[i] ∘ f) s ⊆ image f^[i] s

Tactic:
← image_image

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
i : ℕ
⊢ image f^[i] (image f s) ⊆ image f^[i] s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
motive : ((i : Fin (n + 1)) → α i) → Sort u_2
snoc : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (last n)) → motive (Fin.snoc x x₀)
x : (i : Fin n) → init α i
x₀ : α (last n)
⊢ snocCases snoc (Fin.snoc x x₀) = snoc x x₀

Tactic:
rw [snocCases, cast_eq_iff_heq, Fin.init_snoc, Fin.snoc_last]

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

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

Tactic:
by
    convert h (fun i => v (castAdd n i)) (fun j => v (natAdd m j))
    exact (addCases_castAdd_natAdd v _).symm

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
s : Finset α
n : ℕ
hn : #s ≤ n
⊢ ∃ t, s ⊆ t ∧ #t = n

Tactic:
induction n generalizing s with
  | zero => exact ⟨s, subset_rfl, Nat.eq_zero_of_le_zero hn⟩
  | succ n IH =>
    rcases hn.eq_or_lt with hn' | hn'
    · exact ⟨s, subset_rfl, hn'⟩
    obtain ⟨t, hs, ht⟩ := IH _ (Nat.le_of_lt_succ hn')
    obtain ⟨x, hx⟩ := exists_notMem_finset t
    refine ⟨Finset.cons x t hx, hs.trans (Finset.subset_cons _), ?_⟩
    simp [ht]

Goal state after:
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

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : Std.Antisymm r
l₁ l₂ : List α
hp : l₁ <+~ l₂
hs₁ : Pairwise r l₁
hs₂ : Pairwise r l₂
w✝ : List α
h : w✝ ~ l₁
h' : w✝ <+ l₂
⊢ l₁ <+ l₂
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inr.inr
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑j < ↑x
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Tactic:
simp only [Function.comp_apply, contractNth_apply_of_gt, h]

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

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton s = s
⊢ fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton (insert a s) = insert a s

Tactic:
rw [fold_insert has, ih, insert_eq]

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

Goal state before:
pp: case nil.cons
α : Type u
inst✝ : DecidableEq α
b : α
l₂ : List α
H : [].length ≤ (b :: l₂).length
h : [] ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) [] (b :: l₂)

pp: case cons.nil
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
H : (head✝ :: tail✝).length ≤ [].length
h : head✝ :: tail✝ ≠ []
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) []

pp: case cons.cons
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
b : α
l₂ : List α
H : (head✝ :: tail✝).length ≤ (b :: l₂).length
h : head✝ :: tail✝ ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) (b :: l₂)

Tactic:
· apply nil

Goal state after:
case cons.nil
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
H : (head✝ :: tail✝).length ≤ [].length
h : head✝ :: tail✝ ≠ []
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) []

case cons.cons
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
b : α
l₂ : List α
H : (head✝ :: tail✝).length ≤ (b :: l₂).length
h : head✝ :: tail✝ ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) (b :: l₂)
Module: Mathlib.Data.List.Range

Goal state before:
pp: case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ ∀ (a' : List ℕ), a' ∈ map (map fun x ↦ a + x) l.ranges → (range a).Disjoint a'

Tactic:
intro s hs

Goal state after:
case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s : List ℕ
hs : s ∈ map (map fun x ↦ a + x) l.ranges
⊢ (range a).Disjoint s
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case nil
α : Type u_1
R : α → α → Prop
a : α
⊢ IsChain R [a] ↔ [] = [] ∨ Forall₂ R (a :: [].dropLast) []

Tactic:
simp [isChain_iff_forall₂]

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

Goal state before:
pp: case cons
α : Type u_1
R : α → α → Prop
a head✝ : α
tail✝ : List α
⊢ IsChain R (a :: head✝ :: tail✝) ↔ head✝ :: tail✝ = [] ∨ Forall₂ R (a :: (head✝ :: tail✝).dropLast) (head✝ :: tail✝)

Tactic:
simp [isChain_iff_forall₂]

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

Goal state before:
pp: case cons
M : Type u_8
inst✝ : CommMonoid M
m : M
L : List M
ih : IsUnit L.prod → ∀ (m : M), m ∈ L → IsUnit m
h : IsUnit (m :: L).prod
⊢ ∀ (m_1 : M), m_1 ∈ m :: L → IsUnit m_1

Tactic:
rw [prod_cons, IsUnit.mul_iff] at h
    exact fun m' h' ↦ Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
⊢ iUnion (Fin.snoc f s) = (⋃ i, f i) ∪ s

Tactic:
ext
  simp [Fin.exists_iff_castSucc, or_comm]

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

Goal state before:
pp: case refine_2.inl
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : s.Infinite ∧ t.Nonempty
⊢ (s ×ˢ t).Infinite

pp: case refine_2.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : t.Infinite ∧ s.Nonempty
⊢ (s ×ˢ t).Infinite

Tactic:
· exact h.1.prod_left h.2

Goal state after:
case refine_2.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : t.Infinite ∧ s.Nonempty
⊢ (s ×ˢ t).Infinite
Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice

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

Tactic:
rw [sUnion_eq_biUnion, smul_set_iUnion₂]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s : Set M
S : Subsemigroup M
hn : Nonempty M
h : ⊥ = ⊤
⊢ False

Tactic:
obtain ⟨x⟩ := id hn

Goal state after:
M : Type u_1
N : Type u_2
inst✝ : Mul M
s : Set M
S : Subsemigroup M
hn : Nonempty M
h : ⊥ = ⊤
x : M
⊢ False
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ v i ⊆ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k

Tactic:
intro y y_in

Goal state after:
case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
y : α i
y_in : y ∈ v i
⊢ y ∈ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ f x ∈ iUnion U

Tactic:
hU

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ f x ∈ univ