mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
⊢ c < b

Tactic:
by
  conv_lhs at h => rw [← tsub_add_cancel_of_le hca]
  exact lt_of_add_lt_add_left (hb.lt_add_of_tsub_lt_right h)

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a c : α
inst✝ : AddLeftReflectLE α
d : α
h : c ≤ c + d
⊢ a - d = c + a - (c + d)

Tactic:
add_tsub_add_eq_tsub_left

Goal state after:
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a c : α
inst✝ : AddLeftReflectLE α
d : α
h : c ≤ c + d
⊢ a - d = a - d
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b✝ : α
n : ℕ
a b : α
hab✝ : a ≤ b
c : α
hc : c ≠ 0
hab : a < b
⊢ a * c ≤ b * c

Tactic:
· exact (mul_lt_mul_of_pos_right hab hc.pos).le

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrderedCommMonoidWithZero α
a : α
n : ℕ
inst✝ : IsReduced α
hn : n ≠ 0
⊢ a ^ n ≠ 0 ↔ a ≠ 0

Tactic:
pow_ne_zero_iff hn

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
p : WithBot α → Prop
⊢ (∃ x, ↑a < x ∧ p x) ↔ ∃ b, a < b ∧ p ↑b

Tactic:
simp [WithBot.exists]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
p : WithBot α → Prop
⊢ (∃ x, ↑a ≤ x ∧ p x) ↔ ∃ b, a ≤ b ∧ p ↑b

Tactic:
simp [WithBot.exists]

Goal state after:
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ 1 = 1 + 1 + ⅟b * a + ⅟a * b ↔ -2 + 1 = -2 + (2 + ⅟b * a + ⅟a * b)

Tactic:
one_add_one_eq_two,

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ 1 = 2 + ⅟b * a + ⅟a * b ↔ -2 + 1 = -2 + (2 + ⅟b * a + ⅟a * b)
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
⊢ MonotoneOn f (insert a s) ↔
    (∀ (b : α), b ∈ s → b ≤ a → f b ≤ f a) ∧ (∀ (b : α), b ∈ s → a ≤ b → f a ≤ f b) ∧ MonotoneOn f s

Tactic:
simp [MonotoneOn, forall_and]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
b : β
⊢ image2 f s (insert b t) = (fun a ↦ f a b) '' s ∪ image2 f s t

Tactic:
rw [insert_eq, image2_union_right, image2_singleton_right]

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

Goal state before:
pp: m n : ℕ
hn : Odd n
hm : m ∣ n
⊢ m ≠ 2

Tactic:
by
  rintro rfl
  exact absurd (hn.of_dvd_nat hm) (by decide)

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : Icc a b = Ioo a b
⊢ ¬a ≤ b

Tactic:
simpa using Set.ext_iff.mp h b

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : Ioo a b = Ioc a b
⊢ ¬a < b

Tactic:
simpa using Set.ext_iff.mp h b

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

Tactic:
refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_

Goal state after:
case pos.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Ioc a b

case pos.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ Ioc a b ⊆ s
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y : α
z : ↑(Icc x y)
⊢ x ≤ ↑z ∧ ↑z ≤ y

Tactic:
exact z.property

Goal state after:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y : α
z : ↑(Icc (e x) (e y))
⊢ e x ≤ ↑z ∧ ↑z ≤ e y

Tactic:
exact z.property

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
⊢ ↑(Int.negOfNat n) = -↑n

Tactic:
by simp [Int.negOfNat_eq, Int.cast_neg]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a

Tactic:
rcases lt_trichotomy b 0 with (hb | rfl | hb)
  · simp [hb, hb.not_gt, hb.ne, div_lt_one_of_neg]
  · simp [zero_lt_one]
  · simp [hb, hb.not_gt, div_lt_one, hb.ne.symm]

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
hn : n ≠ l.length
a : α
⊢ (l.eraseIdx n).insertIdx n a = l.set n a

Tactic:
induction n generalizing l <;> cases l <;> simp_all

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

Goal state before:
pp: α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ → l₁ ⊆ l₂

Tactic:
intro h2 x hx

Goal state after:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
⊢ x ∈ l₂
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
by_cases hm : m = 0

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
hm : m = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
hm : ¬m = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Injective f ∧ Surjective (map f) ↔ Injective f ∧ Surjective f

Tactic:
map_surjective_iff

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

Goal state before:
pp: α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x → Forall p l → q x ∧ Forall q l

Tactic:
← and_imp

Goal state after:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x ∧ Forall p l → q x ∧ Forall q l
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * 1 = x * (d * e)

Tactic:
lhs
            rw [he, hdx]
            simp [mul_assoc]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * (d * e)
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: m k : ℕ+
⊢ ↑(k.modDivAux (↑m % ↑k) (↑m / ↑k)).fst = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k

Tactic:
cases (m : ℕ) % (k : ℕ) with
  | zero =>
    rw [if_pos rfl]
    rfl
  | succ n =>
    rw [if_neg n.succ_ne_zero]
    rfl

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

Goal state before:
pp: m k : ℕ+
⊢ (k.modDivAux (↑m % ↑k) (↑m / ↑k)).snd = if ↑m % ↑k = 0 then ↑m / ↑k - 1 else ↑m / ↑k

Tactic:
cases (m : ℕ) % (k : ℕ) with
  | zero =>
    rw [if_pos rfl]
    rfl
  | succ n =>
    rw [if_neg n.succ_ne_zero]
    rfl

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

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ n.natAbs ∣ a.natAbs * d

Tactic:
have := congr_arg Int.natAbs e

Goal state after:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
this : (a * ↑d).natAbs = (n * b).natAbs
⊢ n.natAbs ∣ a.natAbs * d
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
this : (a * ↑d).natAbs = (n * b).natAbs
⊢ n.natAbs ∣ a.natAbs * d

Tactic:
simp only [Int.natAbs_mul, Int.natAbs_natCast] at this

Goal state after:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
this : a.natAbs * d = n.natAbs * b.natAbs
⊢ n.natAbs ∣ a.natAbs * d
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b₁ b₃ : R
a₁ a₃ a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₃ = b₃
⊢ ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃

Tactic:
by
  subst_vars; simp

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b₁ b₂ : R
a₁ a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂

Tactic:
by
  subst_vars; simp

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
b₁ b₃ : R
a₁ a₃ : ℤ
a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₃ = b₃
⊢ ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃

Tactic:
by
  subst_vars; simp

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
b₁ b₂ : R
a₁ a₂ : ℤ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂

Tactic:
by
  subst_vars; simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b₁ b₂ : R
a₁ a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂

Tactic:
by
  subst_vars; simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
x✝ : ι
⊢ f x✝ = g (h x✝)

Tactic:
exact (h2 _).symm

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ ⋃ i, ⋃ j, s i j ⊆ t ↔ ∀ (i : ι) (j : κ i), s i j ⊆ t

Tactic:
by simp_rw [iUnion_subset_iff]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋂ i, ⋂ j, s i j)ᶜ = ⋃ i, ⋃ j, (s i j)ᶜ

Tactic:
by
  simp_rw [compl_iInter]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
⊢ ⨅ a, ⨆ b, g a b = ⨆ g_1, ⨅ a, g a (g_1 a)

Tactic:
suffices lhs ≤ rhs from le_antisymm this le_iInf_iSup

Goal state after:
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
⊢ lhs ≤ rhs
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs)

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
⊢ sSup (∅ ∪ t) ≤ max (sSup ∅) (sSup t)

case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
⊢ False

Tactic:
obtain ⟨c, bc, ca⟩ : ∃ c, b < c ∧ c < a := exists_between (not_le.mp ba)

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
c : α
bc : b < c
ca : c < a
⊢ False
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a✝ b c✝ a c : α
h : b ∈ Icc a c
hac : a ≤ c
⊢ Ioc a b ∪ Ioc b c = Ioc a c

Tactic:
Ioc_union_Ioc_eq_Ioc h.1 h.2

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a✝ b c✝ a c : α
h : b ∈ Icc a c
hac : a ≤ c
⊢ Ioc a c = Ioc a c
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : One M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
f : ι → M
x : ι
y : M
⊢ mulSupport (update f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)

Tactic:
rcases eq_or_ne y 1 with rfl | hy

Goal state after:
case inl
ι : Type u_1
M : Type u_3
inst✝² : One M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
f : ι → M
x : ι
⊢ mulSupport (update f x 1) = if 1 = 1 then mulSupport f \ {x} else insert x (mulSupport f)

case inr
ι : Type u_1
M : Type u_3
inst✝² : One M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
f : ι → M
x : ι
y : M
hy : y ≠ 1
⊢ mulSupport (update f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
ha : 1 < max a 1
⊢ a⁺ᵐ = a

Tactic:
right_lt_sup,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
ha : ¬a ≤ 1
⊢ a⁺ᵐ = a
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: case inr.e_a
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑q⁻¹ = (↑q)⁻¹

Tactic:
cast_inv_of_ne_zero hq

Goal state after:
case inr.e_a
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ (↑q)⁻¹ = (↑q)⁻¹
Module: Mathlib.Tactic.NormNum.OfScientific

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a✝ n✝ : ℕ
⊢ OfScientific.ofScientific (↑a✝) false ↑n✝ = ↑(a✝ * 10 ^ n✝)

Tactic:
rw [NNRatCast.ofScientific_eq_ite, if_neg Bool.false_ne_true]

Goal state after:
α : Type u_1
inst✝ : DivisionSemiring α
a✝ n✝ : ℕ
⊢ ↑↑(↑a✝ * 10 ^ ↑n✝) = ↑(a✝ * 10 ^ n✝)
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m n : ℕ+
⊢ m ∣ n → m ≤ n

Tactic:
rw [dvd_iff']

Goal state after:
m n : ℕ+
⊢ n.mod m = m → m ≤ n
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑n / ↑d⌋ = ↑n / ↑d

Tactic:
← floor_natCast_div_natCast n d,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑n / ↑d⌋ = ⌊↑n / ↑d⌋
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌈↑(negOfNat n) / ↑d⌉ = -(↑n / ↑d)

Tactic:
← floor_natCast_div_natCast n d,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌈↑(negOfNat n) / ↑d⌉ = -⌊↑n / ↑d⌋
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num

Tactic:
suffices (q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num by
    -- use that `q.num` and `q.den` are coprime to show that the numerator stays unreduced
    have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ := by
      suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs from
        mod_cast Rat.num_div_eq_of_coprime q_num_pos this
      have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
      simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using! tmp
    rwa [this]

Goal state after:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ m ≤ replicate n x → ∃ a, a ::ₘ m ≤ replicate (n + 1) x

Tactic:
· intro h
    rw [replicate_succ]
    exact ⟨x, cons_le_cons _ h⟩

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

Goal state before:
pp: α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
x : α × β
h₁ : x ∈ (fun a ↦ map (Prod.mk a) l₂) a₁
h₂ : x ∈ (fun a ↦ map (Prod.mk a) l₂) a₂
⊢ False

Tactic:
rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩

Goal state after:
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : β
left✝ : b₁ ∈ l₂
h₁ : (a₁, b₁) ∈ (fun a ↦ map (Prod.mk a) l₂) a₁
h₂ : (a₁, b₁) ∈ (fun a ↦ map (Prod.mk a) l₂) a₂
⊢ False
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
x : (a : α) × σ a
h₁ : x ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₁
h₂ : x ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₂
⊢ False

Tactic:
rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩

Goal state after:
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : σ a₁
left✝ : b₁ ∈ l₂ a₁
h₁ : ⟨a₁, b₁⟩ ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₁
h₂ : ⟨a₁, b₁⟩ ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₂
⊢ False
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset γ
f : γ → α
⊢ ∀ (a : γ) (s : Multiset γ),
    (∀ {t : Multiset β}, Rel r (map f s) t ↔ Rel (fun a b ↦ r (f a) b) s t) →
      ∀ {t : Multiset β}, Rel r (map f (a ::ₘ s)) t ↔ Rel (fun a b ↦ r (f a) b) (a ::ₘ s) t

Tactic:
by simp +contextual [rel_cons_left]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ pmap (fun x x_1 ↦ f x) s ⋯ = map (fun x ↦ f ↑x) s.attach

Tactic:
rw [pmap_eq_map_attach]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h : a ∈ l₁ ∩ l₂
⊢ a ∈ l₂

Tactic:
simpa using of_mem_filter h

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.toList.Nodup

Tactic:
rw [toList, ← Multiset.coe_nodup, Multiset.coe_toList]
  exact s.nodup

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
⊢ replicate n x ∩ s = replicate (min n (count x s)) x

Tactic:
ext y
  rw [count_inter, count_replicate, count_replicate]
  by_cases h : x = y
  · simp only [h, if_true]
  · simp only [h, if_false, Nat.zero_min]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∉ s ∧ Disjoint t s ↔ a ∉ s ∧ Disjoint s t

Tactic:
_root_.disjoint_comm

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∉ s ∧ Disjoint s t ↔ a ∉ s ∧ Disjoint s t
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a : α
⊢ (replicate n a).toFinset = if n = 0 then ∅ else {a}

Tactic:
by
  ext x
  simp only [mem_toFinset, mem_replicate]
  split_ifs with hn <;> simp [hn]

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
⊢ x ∈ s ∪ t ↔ Xor (x ∈ s) (x ∈ t)

Tactic:
Finset.mem_union,

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
⊢ x ∈ s ∨ x ∈ t ↔ Xor (x ∈ s) (x ∈ t)
Module: Mathlib.Data.Fin.Rev

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

Tactic:
predAbove_of_le_castSucc _ _ h,

Goal state after:
case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ p.rev.predAbove i = (i.rev.castPred ⋯).rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ p.predAbove i.rev = (p.rev.predAbove i).rev

Tactic:
predAbove_rev_left,

Goal state after:
n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ p.predAbove i.rev = (p.predAbove i.rev).rev.rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ (p.predAbove i).rev = p.rev.predAbove i.rev

Tactic:
predAbove_rev_left,

Goal state after:
n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ (p.predAbove i).rev = (p.predAbove i.rev.rev).rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
j : Fin (n + 1)
⊢ ↑j.rev + ↑j = n

Tactic:
by
  rw [Nat.add_comm, j.add_rev_cast]

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

Goal state before:
pp: case succ
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m
⊢ n + 1 ≤ m

Tactic:
rcases exists_eq_succ_of_ne_zero (pos_iff_nonempty.2 (Nonempty.map e inferInstance)).ne'
      with ⟨m, rfl⟩

Goal state after:
case succ
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
⊢ n + 1 ≤ m.succ
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case calc_2.mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
h : b ∈ image (fun a ↦ i ↑a ⋯) s.attach
⊢ b ∈ t

Tactic:
obtain ⟨_, _, rfl⟩ := mem_image.1 h; apply hi

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

Goal state before:
pp: case calc_2
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ #(image (fun a ↦ i ↑a ⋯) s.attach) = #t

Tactic:
congr 1
    ext b
    constructor <;> intro h
    · obtain ⟨_, _, rfl⟩ := mem_image.1 h; apply hi
    · obtain ⟨a, ha, rfl⟩ := i_surj b h; exact mem_image.2 ⟨⟨a, ha⟩, by simp⟩

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.succ ≤ p ∨ p ≤ i.castSucc

Tactic:
by
  rw [le_castSucc_iff, ← castSucc_lt_iff_succ_le]
  exact p.castSucc_lt_or_lt_succ i

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

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten

Tactic:
by
  induction m with
  | zero => simp [ofFn_zero, Nat.zero_mul, ofFn_zero]
  | succ m IH =>
    simp_rw [ofFn_succ', succ_mul]
    simp [ofFn_add, IH]
    rfl

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ y ∈ {x}

Tactic:
card_le_one.1 H y hy x hx,

Goal state after:
α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ x ∈ {x}
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
predAbove_of_le_castSucc _ _ h,

Goal state after:
case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b ≤ a.castSucc
⊢ a.castSucc.predAbove b.castSucc = (b.castPred ⋯).castSucc