mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : a < 0
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
floor_of_nonpos ha.le,

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : a < 0
⊢ 0 < ⌈b⌉₊
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
hna : ↑n ≤ a
⊢ ⌈a - ↑n⌉₊ + n = ⌈a⌉₊

Tactic:
← ceil_add_natCast,

Goal state after:
case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
hna : ↑n ≤ a
⊢ ⌈a - ↑n + ↑n⌉₊ = ⌈a⌉₊

case inr.ha
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
hna : ↑n ≤ a
⊢ 0 ≤ a - ↑n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
a : R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
b : S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : a < 0
⊢ ⌊a⌋₊ = ⌊b⌋₊

Tactic:
floor_of_nonpos ha.le,

Goal state after:
case inl
R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
a : R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
b : S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : a < 0
⊢ 0 = ⌊b⌋₊
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
⊢ FloorSemiring.floor a = FloorSemiring.floor a

Tactic:
rcases lt_or_ge a 0 with h | h

Goal state after:
case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ FloorSemiring.floor a = FloorSemiring.floor a

case inr
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : 0 ≤ a
⊢ FloorSemiring.floor a = FloorSemiring.floor a
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)
⊢ -2 + 1 = -2 + (2 + ⅟b * a + ⅟a * b) ↔ -2 + 1 = ⅟b * a + ⅟a * b

Tactic:
rw [← add_assoc, ← add_assoc, neg_add_cancel, zero_add]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

pp: case neg
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
· have hb := h.mp ha
    obtain ⟨ia⟩ := ha.nonempty_invertible
    obtain ⟨ib⟩ := hb.nonempty_invertible
    simp_rw [inverse_invertible, invOf_add_invOf]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ b - c ↔ a ∣ c

Tactic:
rw [sub_eq_add_neg, dvd_add_right h, dvd_neg]

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ WellFoundedLT (Antisymmetrization α fun x1 x2 ↦ x1 ≤ x2) ↔ WellFoundedLT α

Tactic:
simp_rw [isWellFounded_iff, wellFounded_antisymmetrization_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ Icc a ⊤ = Ici a

Tactic:
simp [← Ici_inter_Iic]

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

Goal state before:
pp: case pos
γ : Type u_3
inst✝ : LinearOrder γ
i j : γ
hj_ub : j ∈ upperBounds (Iio i)
hj_lt_i : j < i
⊢ ∃ j, IsLUB (Iio i) j

Tactic:
exact ⟨j, hj_ub, fun k hk_ub => hk_ub hj_lt_i⟩

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: γ : Type u_1
⊢ LawfulFunctor (Const γ)

Tactic:
by constructor <;> intros <;> rfl

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

Goal state before:
pp: α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 ≤ b
⊢ a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε

Tactic:
refine ⟨fun h _ hε ↦ h.trans <| le_mul_of_one_le_right hb hε.le, fun h ↦ ?_⟩
  obtain rfl | hb := hb.eq_or_lt
  · simp_rw [zero_mul] at h
    exact h 2 one_lt_two
  refine le_of_forall_gt_imp_ge_of_dense fun x hbx => ?_
  convert h (x / b) ((one_lt_div hb).mpr hbx)
  rw [mul_div_cancel₀ _ hb.ne']

Goal state after:
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₂)
h' : Forall₂ R (drop l₁.length l) (drop l₁.length (l₁ ++ l₂))
⊢ Forall₂ R (drop l₁.length l) l₂

Tactic:
rwa [drop_left] at h'

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

Goal state before:
pp: α : Type u
a b c : α
⊢ a ∈ [b, c] ↔ a = b ∨ a = c

Tactic:
mem_cons,

Goal state after:
α : Type u
a b c : α
⊢ a = b ∨ a ∈ [c] ↔ a = b ∨ a = c
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
o₁ o₂ : Option α
p : o₁.toList ~ o₂.toList
⊢ o₁ = o₂

Tactic:
rcases o₁ with - | a

Goal state after:
case none
α : Type u_1
o₂ : Option α
p : none.toList ~ o₂.toList
⊢ none = o₂

case some
α : Type u_1
o₂ : Option α
a : α
p : (some a).toList ~ o₂.toList
⊢ some a = o₂
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
l l' : List α
f : α → β
hf : Function.Injective f
⊢ map f l ~ map f l' ↔ Relation.Comp (fun x1 x2 ↦ x1 = map f x2) (fun x1 x2 ↦ x1 ~ x2) (map f l) l'

Tactic:
eq_map_comp_perm

Goal state after:
α : Type u_1
β : Type u_2
l l' : List α
f : α → β
hf : Function.Injective f
⊢ map f l ~ map f l' ↔ (fun x1 x2 ↦ x1 ~ map f x2) (map f l) l'
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ (map f (a' :: as)).prod = f a ^ count a (a' :: as)

Tactic:
rw [List.map_cons, List.prod_cons, count_cons, h]

Goal state after:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ f a' * f a ^ count a as = f a ^ (count a as + if (a' == a) = true then 1 else 0)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β → β
b : β
hf : ∀ (a : α), f a b = b
a : α
l : List α
⊢ foldr f b (a :: l) = b

Tactic:
foldr_cons,

Goal state after:
α : Type u
β : Type v
f : α → β → β
b : β
hf : ∀ (a : α), f a b = b
a : α
l : List α
⊢ f a (foldr f b l) = b
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case cons.some
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
b : β
ha : f a = some b
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)

Tactic:
· simp +contextual [ha, ih]

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

Goal state before:
pp: m : ℕ
s : Bool
e : ℕ
⊢ 0 ≤ Rat.ofScientific m s e

Tactic:
Rat.ofScientific

Goal state after:
m : ℕ
s : Bool
e : ℕ
⊢ 0 ≤ if s = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)
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 ^ (n + 1)) (y ^ (n + 1))

Tactic:
apply pow_right h

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ n ≤ m → a ^ n ∣ a ^ m

Tactic:
apply pow_dvd_pow

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

Goal state before:
pp: q : ℚ
n : ℤ
⊢ (q - ↑n).den = q.den

Tactic:
rw [sub_eq_add_neg, ← Int.cast_neg, add_intCast_den]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb' : b ≠ 0
e : a * d = n * b
⊢ ↑n * ↑b = ↑a * ↑d

Tactic:
norm_cast
    rw [e]

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

Goal state before:
pp: case pos
n : ℤ
hn : n = 0
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
subst hn

Goal state after:
case pos
⊢ ↑(0 / 0) = ↑0 / ↑0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionRing α
inst✝¹ : DivisionRing β
inst✝ : RingHomClass F α β
f : F
q : ℚ
⊢ ↑q.num / f ↑q.den = ↑q

Tactic:
map_natCast,

Goal state after:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionRing α
inst✝¹ : DivisionRing β
inst✝ : RingHomClass F α β
f : F
q : ℚ
⊢ ↑q.num / ↑q.den = ↑q
Module: Mathlib.Data.Tree.Basic

Goal state before:
pp: α : Type u
t : BinaryTree α
⊢ map id t = t

Tactic:
by
  induction t with
  | nil => rw [map]
  | node v l r hl hr => rw [map, hl, hr, id_eq]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ↑(sSup s) =
    if ⊤ ∈ (fun a ↦ ↑a) '' s then ⊤
    else if BddAbove ((fun a ↦ ↑a) ⁻¹' (fun a ↦ ↑a) '' s) then ↑(sSup ((fun a ↦ ↑a) ⁻¹' (fun a ↦ ↑a) '' s)) else ⊤

Tactic:
rw [if_neg, preimage_image_eq, if_pos hs]

Goal state after:
case h
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ Injective fun a ↦ ↑a

case hnc
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ⊤ ∉ (fun a ↦ ↑a) '' s
Module: Mathlib.Order.Interval.Set.Image

Goal state before:
pp: α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r (↑c) x → p a x
⊢ {x | p a x ∧ q x b} ∩ {y | r (↑c) y} = {y | r (↑c) y ∧ q y b}

Tactic:
by
    ext; simp +contextual [@and_comm (r _ _), h]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝¹ : CompletelyDistribLattice α
inst✝ : CompletelyDistribLattice β
ι✝ : Type (max u v)
κ✝ : ι✝ → Type (max u v)
f : (a : ι✝) → κ✝ a → α × β
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
by ext <;> simp [fst_iSup, fst_iInf, snd_iSup, snd_iInf, iInf_iSup_eq]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ ¬BddAbove univ

Tactic:
contrapose hs

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : BddAbove univ
⊢ BddAbove s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
x : α
hx : x ∈ s
y : α
yt : y ∈ t
hxy : x ≤ y
⊢ x ≤ sSup t

Tactic:
exact hxy.trans (le_csSup Bt yt)

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ sInf ((fun a ↦ ↑a) '' s) = ⨅ a ∈ s, ↑a

Tactic:
sInf_image

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ ⨅ a ∈ s, ↑a = ⨅ a ∈ s, ↑a
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi b ⊆ Ioi a ↔ a ≤ b

Tactic:
by
  refine ⟨fun h => ?_, Ioi_subset_Ioi⟩
  by_contra ba
  exact lt_irrefl _ (h (not_le.mp ba))

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

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
hne : s.Nonempty
⊢ s.Pairwise (r on f) ↔ ∃ z, ∀ (x : α), x ∈ s → r (f x) z

Tactic:
· exact hne.pairwise_iff_exists_forall

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : LE A
inst✝ : IsConcreteLE A B
S T : A
⊢ S ≤ T ↔ ∀ ⦃x : B⦄, x ∈ S → x ∈ T

Tactic:
simp [← coe_subset_coe, Set.subset_def]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
h : (⇑ofDual ⁻¹' s).OrdConnected
⊢ s.OrdConnected

Tactic:
by simpa only [ordConnected_def] using! h.dual

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

Goal state before:
pp: α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
a b : { x // 0 ≤ x }
h : ↑a ≤ ↑b
c : α
hc : ↑b = ↑a + c
⊢ b = a + ⟨c, ?m.49⟩

Tactic:
simp [Subtype.ext_iff, hc]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ ↑p < ↑q

Tactic:
by
  rwa [NNRat.cast_def, NNRat.cast_def, div_lt_div_iff₀, ← Nat.cast_mul, ← Nat.cast_mul,
    Nat.cast_lt (α := K), ← NNRat.lt_def]
  · simp
  · simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a : α
⊢ a⁺ᵐ / a⁻ᵐ = a

Tactic:
by
  rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel,
    sup_comm, oneLePart_def]

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true
h✝ : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h : ↑num✝¹ * ⅟↑da ≤ ⅟↑db * ↑num✝
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
rwa [Int.commute_cast] at h

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h✝ : (fun x ↦ ↑x) (num✝¹ * ↑db) < (fun x ↦ ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ↑num✝¹ * ⅟↑da < ⅟↑db * ↑num✝
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
rwa [Int.commute_cast] at h

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

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

Tactic:
rw [ascFactorial_succ, Nat.pow_succ, Nat.mul_comm, ← Nat.add_assoc, Nat.add_right_comm n 1 k]
    exact Nat.mul_le_mul_right _
      (Nat.le_trans (ascFactorial_le_pow_add _ k) (Nat.pow_le_pow_left (le_succ _) _))

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

Goal state before:
pp: n : ℕ
⊢ n.succ.descFactorial n.succ = n.succ !

Tactic:
by rw [succ_descFactorial_succ, descFactorial_self n, factorial_succ]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ (a + b) ^ 2 * (a ^ (n + 1) + ↑(n + 1) * a ^ n * b) ≤ (a + b) ^ 2 * (a + b) ^ (n + 1)

Tactic:
gcongr
        apply Commute.pow_add_mul_le_add_pow_of_sq_nonneg <;> assumption

Goal state after:
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
x : R
hx : fract x ≠ 0
| -x

Tactic:
← floor_add_fract x

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
| -(↑⌊x⌋ + fract x)
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
s : Set R
x : R
hms : x - ↑⌊x⌋ ∈ s
hm0 : 0 ≤ x - ↑⌊x⌋
hm1 : x - ↑⌊x⌋ < 1
⊢ fract x ∈ s

Tactic:
exact hms

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

Goal state before:
pp: case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m / ↑n - ↑(m % n) / ↑n = ↑(↑m / ↑n)

Tactic:
rw [sub_eq_iff_eq_add', ← mul_right_inj' hn'.ne', mul_div_cancel₀ _ hn'.ne', mul_add,
      mul_div_cancel₀ _ hn'.ne']
    norm_cast
    rw [← Nat.cast_add, Nat.mod_add_div m n]

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : -1 < a
⊢ 0 ≤ ⌈a⌉

Tactic:
by
  rwa [Int.le_ceil_iff, Int.cast_zero, zero_sub]

Goal state after:
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
⊢ fract (↑n * ⅟↑d) = ↑(n % d) * ⅟↑d

Tactic:
simp only [invOf_eq_inv, ← div_eq_mul_inv, fract_div_natCast_eq_div_natCast_mod]

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

Goal state before:
pp: 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)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
⊢ R (f x) (f y)

Tactic:
rcases lt_trichotomy n 0 with hn | rfl | hn

Goal state after:
case inl
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)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : n < 0
⊢ R (f x) (f y)

case inr.inl
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)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
hny : y - 0 • a ∈ Ioc l (l + a)
⊢ R (f x) (f y)

case inr.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)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
⊢ R (f x) (f y)
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
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : 0 < y
q : ℕ
hq : x⁻¹ < y⁻¹ ^ q
⊢ y ^ q < x

Tactic:
rwa [inv_pow, inv_lt_inv₀ hx (pow_pos y_pos _)] at hq

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

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

Tactic:
rcases lt_or_ge a 1 with ha₁ | ha₁
      · refine ⟨0, ?_⟩
        rw [zpow_zero]
        exact ⟨ha₁, hb₁⟩
      · have : b⁻¹ < a⁻¹ * c := by rwa [lt_inv_mul_iff₀' ha, inv_mul_lt_iff₀ hb₀]
        obtain ⟨n, hn₁, hn₂⟩ :=
          exists_pow_btwn_of_lt_mul this (inv_pos_of_pos ha) (inv_le_one_of_one_le₀ ha₁) hc₀ hc₁
        refine ⟨-n, ?_, ?_⟩
        · rwa [lt_inv_comm₀ (pow_pos hc₀ n) ha, ← zpow_natCast, ← zpow_neg] at hn₂
        · rwa [inv_lt_comm₀ hb₀ (pow_pos hc₀ n), ← zpow_natCast, ← zpow_neg] at hn₁

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

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ x -ᵥ y + (x -ᵥ y) = 0 ↔ y = x

Tactic:
← two_nsmul,

Goal state after:
G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ 2 • (x -ᵥ y) = 0 ↔ y = x
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : x₁ -ᵥ x₂ + (x₁ -ᵥ x₂) = 0
⊢ x₁ = x₂

Tactic:
← two_nsmul,

Goal state after:
G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : 2 • (x₁ -ᵥ x₂) = 0
⊢ x₁ = x₂
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
h : l₂.Nodup
⊢ (l₁ ∪ l₂).Nodup

Tactic:
induction l₁ generalizing l₂ with
  | nil => exact h
  | cons a l₁ ih => exact (ih h).insert

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f u = t
this : f a ∈ map f (a ::ₘ u)
⊢ map f ((a ::ₘ u).erase a) = t

Tactic:
Multiset.erase_cons_head,

Goal state after:
case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f u = t
this : f a ∈ map f (a ::ₘ u)
⊢ map f u = t
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.head! :: l.dedup.tail
⊢ l.dedup = a :: l'

Tactic:
mem_cons,

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! ∨ a ∈ l.dedup.tail
⊢ l.dedup = a :: l'
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'
⊢ l.dedup = a :: l'

Tactic:
have := @List.cons_head!_tail α ⟨a⟩ _ (ne_nil_of_mem (mem_dedup.2 h.1))
    have hal : a ∈ l.dedup := mem_dedup.2 h.1
    rw [← this, mem_cons, or_iff_not_imp_right] at hal
    exact this ▸ h.2.2.symm ▸ cons_eq_cons.2 ⟨(hal (h.2.2.symm ▸ h.2.1)).symm, rfl⟩

Goal state after: