mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t

Tactic:
rw [prl, prr, prt]

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t

Tactic:
rw [prl, prr, prt]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ IsNNRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc

Tactic:
refine ⟨this, ?_⟩

Goal state after:
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
Module: Mathlib.Data.List.Defs

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (ts.length + (t :: is).length, ts.length)
    ((t :: ts).length + is.length, (t :: ts).length)

Tactic:
simp_wf

Goal state after:
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (ts.length + (is.length + 1), ts.length)
    (ts.length + 1 + is.length, ts.length + 1)
Module: Mathlib.Data.List.Defs

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (is.length + [].length, is.length)
    ((t :: ts).length + is.length, (t :: ts).length)

Tactic:
simp_wf

Goal state after:
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (is.length, is.length) (ts.length + 1 + is.length, ts.length + 1)
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ IsRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc

Tactic:
refine ⟨this, ?_⟩

Goal state after:
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: case false
α : Type u
p : α → Bool
a : α
l l₂ : List α
hp : p a = false
⊢ loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))

Tactic:
simp [hp, span.loop, span.loop_eq_take_drop, takeWhile, dropWhile]

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

Goal state before:
pp: case true
α : Type u
p : α → Bool
a : α
l l₂ : List α
hp : p a = true
⊢ loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))

Tactic:
simp [hp, span.loop, span.loop_eq_take_drop, takeWhile, dropWhile]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → α
a : γ
l : List γ
x✝ : List β
⊢ Forall₂ R (map f (a :: l)) x✝ ↔ Forall₂ (fun c b ↦ R (f c) b) (a :: l) x✝

Tactic:
simp only [map, forall₂_cons_left_iff, forall₂_map_left_iff]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ ¬x ∈ {y}

Tactic:
rwa [singleton_eq, mem_singleton]

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₂ ≠ []
⊢ (l₁ ++ l₂).getLast ⋯ = l₂.getLast h

Tactic:
by
  induction l₁ with grind

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
⊢ (L.set n a).prod = L.prod * if hn : n < L.length then L[n]⁻¹ * a else 1

Tactic:
refine (prod_set L n a).trans ?_

Goal state after:
G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
⊢ ((take n L).prod * if n < L.length then a else 1) * (drop (n + 1) L).prod =
    L.prod * if hn : n < L.length then L[n]⁻¹ * a else 1
Module: Mathlib.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ Int.negSucc n) (y ^ Int.negSucc n)

Tactic:
simp only [zpow_negSucc, inv_right_iff]

Goal state after:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ (n + 1)) (y ^ (n + 1))
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ (fun x ↦ a * x) ((fun x ↦ b * x) j) = (fun x ↦ c * x) ((fun x ↦ a * x) j)

Tactic:
by simp only [← mul_assoc, h.eq]

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

Tactic:
rw [he, hdx]

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 * 1
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ q.num ∣ n

Tactic:
qdf

Goal state after:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ (n /. d).num ∣ n
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ q.num ≠ 0

Tactic:
qdf

Goal state after:
case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ (n /. d).num ≠ 0
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a : ℕ
ha0 : 0 < a
⊢ (↑a)⁻¹.den = a

Tactic:
by
  rw [← Int.ofNat_inj, ← Int.cast_natCast a, inv_intCast_den_of_pos]
  rwa [Int.natCast_pos]

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
n e1 t1 k l : α
e2 : ℕ
h1 : n * e1 = t1
h2 : l * n ^ e2 = k
⊢ l * n ^ e2 * e1 ^ e2 = l * t1 ^ e2

Tactic:
← h1,

Goal state after:
α : Type u_1
inst✝ : CommRing α
n e1 t1 k l : α
e2 : ℕ
h1 : n * e1 = t1
h2 : l * n ^ e2 = k
⊢ l * n ^ e2 * e1 ^ e2 = l * (n * e1) ^ e2
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
a : α
inst✝ : Nonempty ι
⊢ sSup (range fun x ↦ a) = a

Tactic:
range_const,

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
a : α
inst✝ : Nonempty ι
⊢ sSup {a} = a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a b x✝ : α
h : sInf {c | a ≤ b ⊔ c} ≤ x✝
⊢ a ≤ b ⊔ sInf {c | a ≤ b ⊔ c}

Tactic:
by simp [minAx.sup_sInf_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : α → Set β
⊢ ⋃ x ∈ ⋃ i, s i, t x = ⋃ i, ⋃ x ∈ s i, t x

Tactic:
simp [@iUnion_comm _ ι]

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

Goal state before:
pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∃ i, f i ≠ ⊥
i : ι
hi : ¬f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'

Tactic:
· exact ⟨⟨i, hi⟩, rfl.le⟩

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst✝ : (i : α) → CompleteLattice (β i)
x✝¹ : Set ((i : α) → β i)
x✝ : α
⊢ IsGLB (eval x✝ '' x✝¹) (sInf x✝¹ x✝)

Tactic:
by rw [sInf_apply_eq_sInf_image]; exact isGLB_sInf _

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

Goal state before:
pp: α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
⊢ x ∈ ⋃ j ∈ J, Es j → i ∈ J

Tactic:
intro x_in_U

Goal state after:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
x_in_U : x ∈ ⋃ j ∈ J, Es j
⊢ i ∈ J
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
inst✝ : CompleteLattice β
t : ι → Set β
⊢ sSup (⋃ i, t i) = ⨆ i, sSup (t i)

Tactic:
by
  simp_rw [sSup_eq_iSup, iSup_iUnion]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
⊢ IsLeast s (sInf s)

Tactic:
by
  rw [sInf_eq_argmin_on hs]
  exact ⟨argminOn_mem _ _ _, fun a ha => argminOn_le id _ ha⟩

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
this : OrderBot α
⊢ sInf s ∈ s ∧ ∀ a ∈ s, sInf s ≤ a

Tactic:
exact ⟨csInf_mem hs, fun _ ↦ csInf_le (OrderBot.bddBelow s)⟩

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ sInf s = n → n ∈ s ∧ ∀ a ∈ s, n ≤ a

pp: case mpr
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ (n ∈ s ∧ ∀ a ∈ s, n ≤ a) → sInf s = n

Tactic:
· intro rfl
    exact ⟨csInf_mem hs, fun _ ↦ csInf_le (OrderBot.bddBelow s)⟩

Goal state after:
case mpr
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ (n ∈ s ∧ ∀ a ∈ s, n ≤ a) → sInf s = n
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
⊢ b' ∈ lowerBounds (f '' Icc a b) → b' ≤ f a

Tactic:
exact fun hb' ↦ hb' ⟨a, by simp [hab]⟩

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

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

Tactic:
cases le_total a b <;> simp [uIoc, *]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a ∈ Ι a b ↔ b < a

Tactic:
simp [mem_uIoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b ∈ Ι a b ↔ a < b

Tactic:
simp [mem_uIoc]

Goal state after:
Module: Mathlib.Algebra.Order.Nonneg.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
⊢ sSup ∅ = ⊥

Tactic:
@subset_sSup_def α (Set.Ici a) _ _ ⟨⟨a, le_rfl⟩⟩

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
⊢ (fun t ↦
        if ht : t.Nonempty ∧ BddAbove t ∧ sSup (Subtype.val '' t) ∈ Ici a then ⟨sSup (Subtype.val '' t), ⋯⟩
        else default)
      ∅ =
    ⊥
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ mulSupport f ≠ ∅ ↔ f ≠ 1

Tactic:
Ne,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ ¬mulSupport f = ∅ ↔ f ≠ 1
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
rw [ascFactorial, Nat.mul_left_comm, succ_ascFactorial n k, ascFactorial, succ_add,
    ← Nat.add_assoc]

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

Goal state before:
pp: n : ℕ
⊢ n ! * (n + 1).ascFactorial 0 = (n + 0)!

Tactic:
by rw [ascFactorial_zero, Nat.add_zero, Nat.mul_one]

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

Goal state before:
pp: k : ℕ
⊢ descFactorial 0 (k + 1) = 0

Tactic:
descFactorial_succ,

Goal state after:
k : ℕ
⊢ (0 - k) * descFactorial 0 k = 0
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
descFactorial_succ,

Goal state after:
n k : ℕ
⊢ (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial k.succ
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
descFactorial_succ,

Goal state after:
n k : ℕ
⊢ (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
descFactorial_succ,

Goal state after:
n k : ℕ
⊢ (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial k.succ = 0 ↔ n < k.succ

Tactic:
descFactorial_succ,

Goal state after:
n k : ℕ
⊢ (n - k) * n.descFactorial k = 0 ↔ n < k.succ
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
descFactorial_succ,

Goal state after:
n k : ℕ
⊢ (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = n.ascFactorial k.succ
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case succ
k m : ℕ
h : k ≤ m
n : ℕ
ih : k.descFactorial n ≤ m.descFactorial n
⊢ k.descFactorial (n + 1) ≤ m.descFactorial (n + 1)

Tactic:
descFactorial_succ,

Goal state after:
case succ
k m : ℕ
h : k ≤ m
n : ℕ
ih : k.descFactorial n ≤ m.descFactorial n
⊢ (k - n) * k.descFactorial n ≤ m.descFactorial (n + 1)
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
descFactorial_succ,

Goal state after:
n k : ℕ
⊢ (n + 1 - (k + 1)) ^ (k + 1) ≤ (n - k) * n.descFactorial k
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) ^ (0 + 2) < n.descFactorial (0 + 2)

Tactic:
descFactorial_succ,

Goal state after:
n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) ^ (0 + 2) < (n - 1) * n.descFactorial 1
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 1 + 2) < n.descFactorial (k + 1 + 2)

Tactic:
descFactorial_succ,

Goal state after:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 1 + 2) < (n - (k + 2)) * n.descFactorial (k + 2)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial (k + 1) ≤ n ^ (k + 1)

Tactic:
descFactorial_succ,

Goal state after:
n k : ℕ
⊢ (n - k) * n.descFactorial k ≤ n ^ (k + 1)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : 2 ≤ k + 2
⊢ n.descFactorial (k + 2) < n ^ (k + 2)

Tactic:
descFactorial_succ,

Goal state after:
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n - (k + 1)) * n.descFactorial (k + 1) < n ^ (k + 2)
Module: Mathlib.Algebra.Order.Round

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

Tactic:
by
  rw [← floor_add_fract x, round, fract_intCast_add, fract_fract, floor_intCast_add, mul_add,
    ← Int.cast_ofNat, ← Int.cast_mul, floor_intCast_add, ceil_intCast_add, add_assoc,
    Int.mul_add_ediv_left _ _ two_ne_zero, Int.cast_ofNat]
  split_ifs with h <;> congr 1
  · rw [Int.floor_eq_zero_iff.mpr, Int.floor_eq_zero_iff.mpr]
    · simp
    · simp [h]
    · suffices fract x < 1 by simpa
      refine lt_of_le_of_lt ?_ h
      apply le_mul_of_one_le_left <;> simp
  · have H : ⌊2 * fract x⌋ = 1 := by simpa [floor_eq_iff, ← two_mul, fract_lt_one] using h
    suffices 0 < fract x by simp [this, H, ceil_eq_iff, (fract_lt_one _).le]
    contrapose! h
    grw [h]
    simp

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

Goal state before:
pp: a b : ℕ+
hab : a < b
⊢ a ≤ b - 1

Tactic:
rw [← coe_le_coe, sub_coe]
  split_ifs with h
  · exact Nat.le_pred_of_lt hab
  · exact hab.le.trans (le_of_not_gt h)

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (↑y + x) = y + round x

Tactic:
by
  rw [add_comm, round_add_intCast, add_comm]

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

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * ↑n + 1
⊢ k * x = k * ↑⌊x⌋ + 1

Tactic:
convert! hn

Goal state after:
R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
n : ℤ
hn : k * x = k * ↑n + 1
⊢ ⌊x⌋ = n
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ (fun x ↦ x ^ n) a ≤ (fun x ↦ x ^ n) b

Tactic:
← one_le_div',

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ 1 ≤ (fun x ↦ x ^ n) b / (fun x ↦ x ^ n) a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ⌈a - ↑n⌉ = ⌈a⌉ - ↑n

Tactic:
by
  convert ceil_sub_intCast a n
  simp

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid G
inst✝³ : LinearOrder G
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
f : G →* M
hf : StrictMono ⇑f
x x✝ : G
h : 1 < x✝
⊢ 1 < ?m.25

Tactic:
by simpa using hf h

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

Goal state before:
pp: case refine_1
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
h : ⌈a⌉ = ⌊a⌋ + 1
ht : a ∈ range Int.cast
h0 : ↑⌊a⌋ = ↑(⌊a⌋ + 1)
⊢ False

Tactic:
cast_add,

Goal state after:
case refine_1
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
h : ⌈a⌉ = ⌊a⌋ + 1
ht : a ∈ range Int.cast
h0 : ↑⌊a⌋ = ↑⌊a⌋ + ↑1
⊢ False
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = ↑⌊a⌋ + ↑1

Tactic:
← Int.cast_add

Goal state after:
case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = ↑(⌊a⌋ + 1)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ ↑(⌊a⌋ + 1) - 1 < a

Tactic:
cast_add,

Goal state after:
case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ ↑⌊a⌋ + ↑1 - 1 < a
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: case inr
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
this : ∀ (x y : G), x < y → x ∈ Ico l (l + a) → R (f x) (f y)
hx : x ∉ Ico l (l + a)
⊢ R (f x) (f y)

Tactic:
rcases existsUnique_sub_zsmul_mem_Ico ha x l with ⟨m, hm, -⟩
    suffices R (f (x - m • a)) (f (y - m • a)) by simpa using hR (m • b) this
    exact this _ _ (by simpa) hm

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

Goal state before:
pp: case e_2
α : Type u_1
β : Type v
γ : Type u_2
C : Multiset α → Sort u_3
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)
m : Multiset α
x✝² x✝¹ : List α
h : x✝² ≈ x✝¹
a✝ : α
l✝ l'✝ : List α
b✝ : C ⟦l✝⟧
b'✝ : C ⟦l'✝⟧
hl : l✝ ~ l'✝
x✝ : b✝ ≍ b'✝
⊢ ⟦l✝⟧ = ⟦l'✝⟧

Tactic:
exact Quot.sound hl

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ Rel r (a ::ₘ as) bs ↔ ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

Tactic:
constructor
  · generalize hm : a ::ₘ as = m
    intro h
    induction h generalizing as with
    | zero => simp at hm
    | @cons a' b as' bs ha'b h ih =>
      rcases cons_eq_cons.1 hm with (⟨rfl, rfl⟩ | ⟨_h, cs, eq₁, eq₂⟩)
      · exact ⟨b, bs, ha'b, h, rfl⟩
      · rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
        exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩
  · exact fun ⟨b, bs', hab, h, Eq⟩ => Eq.symm ▸ Rel.cons hab h

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ t ∧ s = t.erase a → a ::ₘ s = t

Tactic:
rintro ⟨h, rfl⟩

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
h : a ∈ t
⊢ a ::ₘ t.erase a = t
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ 0 < count a (s - t) ↔ count a t < count a s

Tactic:
count_sub,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ 0 < count a s - count a t ↔ count a t < count a s
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (map f (hd :: tl)).Nodup
⊢ ∀ ⦃x : α⦄, x ∈ hd :: tl → ∀ ⦃y : α⦄, y ∈ hd :: tl → f x = f y → x = y

Tactic:
simp only [map, nodup_cons, mem_map, not_exists, not_and, ← Ne.eq_def] at d
    simp only [mem_cons]
    rintro _ (rfl | h₁) _ (rfl | h₂) h₃
    · rfl
    · apply (d.1 _ h₂ h₃.symm).elim
    · apply (d.1 _ h₁ h₃).elim
    · apply ih d.2 h₁ h₂ h₃

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

Goal state before:
pp: case mp
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
a : α
ha : a ∈ s
⊢ map f s = f a ::ₘ map f (s.erase a)

Tactic:
rw [← map_cons, Multiset.cons_erase ha]

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
⊢ map f s = pmap (fun x x_1 ↦ f x) s ⋯

Tactic:
pmap_eq_map

Goal state after:
α : 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
⊢ map f s = map f s