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

Goal state before:
pp: case inl
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
h✝ : a ≤ b
⊢ a * b + b * a ≤ a * a + b * b

Tactic:
exact mul_add_mul_le_mul_add_mul ‹_› ‹_›

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ |a ^ n| = 1 ↔ |a| = 1

Tactic:
convert! pow_left_inj₀ (abs_nonneg a) zero_le_one h

Goal state after:
case e'_2
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ |a ^ n| = |a| ^ n

case e'_3
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ 1 = 1 ^ n
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
t : Set β
⊢ image2 f {a} t = t

Tactic:
by
  rw [image2_singleton_left, show f a = id from funext h, image_id]

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

Goal state before:
pp: γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderTop γ
⊢ upperBounds univ = {⊤}

Tactic:
by rw [isGreatest_univ.upperBounds_eq, Ici_top]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ upperBounds ∅ = univ

Tactic:
by
  simp only [upperBounds, eq_univ_iff_forall, mem_ofPred_eq, forall_mem_empty, forall_true_iff]

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : a < b
⊢ a / b < 1

Tactic:
div_lt_one (ha.trans h)

Goal state after:
α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : a < b
⊢ a < b
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
s : Set α
ha : 0 ≤ a
hs : IsGLB s b
⊢ IsGLB ((fun b ↦ b * a) '' s) (b * a)

Tactic:
by simpa [mul_comm] using hs.mul_left ha

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
s : Set α
ha : 0 ≤ a
hs : IsLUB s b
⊢ IsLUB ((fun b ↦ b * a) '' s) (b * a)

Tactic:
by simpa [mul_comm] using hs.mul_left ha

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

Goal state before:
pp: α : Type u
i j : ℕ
xs : List α
⊢ (dropSlice i j xs).length = xs.length - min j (xs.length - i)

Tactic:
induction xs generalizing i j with cases i with grind [dropSlice]

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
n : ℕ
l : List α
ha : a ∈ l
⊢ a ∈ take n l ↔ idxOf a l < n

Tactic:
rw [l.take_prefix n |>.mem_iff_idxOf_lt_length]
  grind

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

Goal state before:
pp: case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod

Tactic:
by_cases hx : p x

Goal state after:
case pos
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod

case neg
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : ¬p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod
Module: Mathlib.Algebra.Order.Nonneg.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : SemilatticeSup α
a : α
h : 0 ≤ a
⊢ toNonneg a = ⟨a, h⟩

Tactic:
by simp [toNonneg, h]

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

Goal state before:
pp: f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
x : ℚ
hc : c /. d = x
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } x = f₁ a b c d /. f₂ a b c d

Tactic:
obtain ⟨n₂, d₂, h₂, c₂⟩ := x

Goal state after:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ }
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
    f₁ a b c d /. f₂ a b c d
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: l : List ℕ
n : ℕ
⊢ l.sum % n = (map (fun x ↦ x % n) l).sum % n

Tactic:
induction l with
  | nil => simp only [map_nil]
  | cons a l ih =>
    simpa only [map_cons, sum_cons, Nat.mod_add_mod, Nat.add_mod_mod] using congr((a + $ih) % n)

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

Goal state before:
pp: case nil
n : ℤ
⊢ [].prod % n = (map (fun x ↦ x % n) []).prod % n

Tactic:
simp [Int.mul_emod, *]

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

Goal state before:
pp: case cons
n head✝ : ℤ
tail✝ : List ℤ
tail_ih✝ : tail✝.prod % n = (map (fun x ↦ x % n) tail✝).prod % n
⊢ (head✝ :: tail✝).prod % n = (map (fun x ↦ x % n) (head✝ :: tail✝)).prod % n

Tactic:
simp [Int.mul_emod, *]

Goal state after:
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ a⁻¹

Tactic:
rw [inv_def]

Goal state after:
a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ ↑a.den /. a.num
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n : ℕ
⊢ ↑(↑n).toNNRat = ↑↑n

Tactic:
simp only [Nat.cast_nonneg', Rat.coe_toNNRat]

Goal state after:
n : ℕ
⊢ ↑n = ↑↑n
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ¬IsUnit c

Tactic:
rintro ⟨u, rfl⟩

Goal state after:
case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
u : αˣ
hnd : ¬a * ↑u ∣ a
⊢ False
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

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.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
n : ℤ
⊢ ↑n / ↑1 = ↑n

Tactic:
rw [Nat.cast_one, div_one]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ ∀ (b : γ), True

Tactic:
forall_true_iff

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 α
⊢ sSup ∅ = ⊥

Tactic:
by simp [sSup, bot_unique (WellFounded.min_le _ (mem_univ _))]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
⊢ ⨆ i, ⨆ j, ⨆ (_ : i ∈ s ∧ j ∈ t), f (i, j) = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)

Tactic:
iSup_and

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
⊢ ⨆ i, ⨆ j, ⨆ (_ : i ∈ s), ⨆ (_ : j ∈ t), f (i, j) = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : (fun a ↦ ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a ↦ ↑a) '' s)
⊢ ↑(sInf s) = ⊤

Tactic:
rcases h with h1 | h2

Goal state after:
case pos.inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h1 : (fun a ↦ ↑a) '' s ⊆ {⊤}
⊢ ↑(sInf s) = ⊤

case pos.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h2 : ¬BddBelow ((fun a ↦ ↑a) '' s)
⊢ ↑(sInf s) = ⊤
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case ht
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ y ∈ range fun i ↦ f i, ∃ x ∈ ⋃ i, Iic (f i), y ≤ x

Tactic:
rintro x ⟨i, rfl⟩

Goal state after:
case ht
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
i : ι
⊢ ∃ x ∈ ⋃ i, Iic (f i), (fun i ↦ f i) i ≤ x
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
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 ⟨hn, hle⟩

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

Goal state before:
pp: α✝ : 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
⊢ sSup S ≤ a

Tactic:
rcases S.eq_empty_or_nonempty with h | h

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

case inr
α✝ : 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.Nonempty
⊢ sSup S ≤ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
⊢ (if S ⊆ {⊤} ∨ ¬BddBelow S then ⊤ else ↑(sInf ((fun a ↦ ↑a) ⁻¹' S))) ≤ a

Tactic:
simp only [OrderBot.bddBelow, not_true_eq_false, or_false]

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
⊢ (if S ⊆ {⊤} then ⊤ else ↑(sInf ((fun a ↦ ↑a) ⁻¹' S))) ≤ a
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
change ¬ ∀ i, i ∈ s → ∀ j, j ∈ s → i ≠ j → ∀ t, t ≤ f i → t ≤ f j → t ≤ ⊥ at h
  simp only [not_forall] at h
  obtain ⟨i, hi, j, hj, h_ne, t, hfi, hfj, ht⟩ := h
  replace ht : t.Nonempty := by
    rwa [le_bot_iff, bot_eq_empty, ← Ne, ← nonempty_iff_ne_empty] at ht
  obtain ⟨x, hx⟩ := ht
  exact ⟨i, hi, j, hj, h_ne, x, hfi hx, hfj hx⟩

Goal state after:
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 = Ι a c

Tactic:
uIoc_of_le hac,

Goal state after:
α : 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
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : Nontrivial α
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : AddLeftMono α
a : α
ha : a ≠ 0
lt : a < 0
⊢ Nontrivial { x // 0 ≤ x }

pp: case inr
α : Type u_1
inst✝³ : Nontrivial α
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : AddLeftMono α
a : α
ha : a ≠ 0
lt : 0 < a
⊢ Nontrivial { x // 0 ≤ x }

Tactic:
· exact ⟨0, ⟨-a, neg_nonneg.mpr lt.le⟩, Subtype.coe_ne_coe.mp (neg_ne_zero.mpr ha).symm⟩

Goal state after:
case inr
α : Type u_1
inst✝³ : Nontrivial α
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : AddLeftMono α
a : α
ha : a ≠ 0
lt : 0 < a
⊢ Nontrivial { x // 0 ≤ x }
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
by
  rw [← cast_le (K := K), cast_natCast]

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℕ
n : ℚ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
by
  rw [← cast_le (K := K), cast_natCast]

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
m : ℚ≥0
n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
by
  rw [← cast_le (K := K), cast_natCast]

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
m : ℕ
n : ℚ≥0
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
by
  rw [← cast_le (K := K), cast_natCast]

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: case pos
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ∃ a, f a = x
⊢ extend f g 1 x = 1

Tactic:
rw [extend, dif_pos hf, ← notMem_mulSupport]
      rw [← Classical.choose_spec hf] at hfg
      exact fun hg ↦ hfg ⟨_, hg, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a ⊔ a⁻¹ ⊔ 1 = |a|ₘ

Tactic:
exact sup_eq_left.2 <| one_le_mabs a

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

Goal state before:
pp: case refl
m n : ℕ
⊢ m ! ∣ m !

Tactic:
exact Nat.dvd_refl _

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

Goal state before:
pp: m n : ℕ
⊢ m ! * (m + 1) ^ (n + 1) ≤ (m + (n + 1))!

Tactic:
rw [← Nat.add_assoc, factorial_succ, Nat.mul_comm (_ + 1), Nat.pow_succ, ← Nat.mul_assoc]

Goal state after:
m n : ℕ
⊢ m ! * (m + 1) ^ n * (m + 1) ≤ (m + n)! * (m + n + 1)
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x ∈ Ico 0 1

Tactic:
suffices fract x < 1 by simpa

Goal state after:
case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x < 1
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: n : ℕ+
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
⊢ p n

Tactic:
by
  rcases n with ⟨n, h⟩
  induction n with
  | zero => exact absurd h (by decide)
  | succ n IH =>
    rcases n with - | n
    · exact one
    · exact succ _ (IH n.succ_pos)

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

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

Tactic:
rw [← coe_le_coe, sub_coe]
  split_ifs with h
  · exact Nat.sub_le a b
  · exact a.2

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

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

Tactic:
refine strictMono_int_of_lt_succ fun n ↦ ?_

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ (n + 1)
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:
by
  rw [← one_lt_div', ← div_zpow]; exact one_lt_zpow (one_lt_div'.2 hab) hn

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

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

Tactic:
by
  rw [← Int.ofNat_inj, Int.natCast_floor_eq_floor (by positivity)]
  push_cast
  exact floor_intCast_div_natCast n d

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✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
| f (x - n • a + n • a) - n • b

Tactic:
map_add_nsmul,

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
| f (x - n • a) + n • b - n • b
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k✝ : ℕ
hk✝ : g⁻¹ ≤ a ^ k✝
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
hm'' : g < a ^ (m + 1)
n : ℤ
hn : (fun k ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) n
⊢ a ^ m < a ^ (n + 1)

Tactic:
exact lt_of_le_of_lt hm hn.2

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

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

Tactic:
exact Nat.find_min this (Nat.sub_one_lt hn) H

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

Goal state before:
pp: K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
⊢ (∀ (x : K), ∃ n, x < ↑n) → Archimedean K

Tactic:
archimedean_iff_nat_lt

Goal state after:
K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
⊢ (∀ (x : K), ∃ n, x < ↑n) → ∀ (x : K), ∃ n, x < ↑n
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₃ /ₛ p₂) / (p₃ /ₛ p₁) = p₁ /ₛ p₂

Tactic:
by
  rw [div_eq_mul_inv, inv_sdiv_eq_sdiv_rev, mul_comm, sdiv_mul_sdiv_cancel]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p (l₁.diff l₂) = countP p l₁ - countP p l₂

Tactic:
by
  refine (Nat.sub_eq_of_eq_add ?_).symm
  rw [← countP_append]
  exact ((subperm_append_diff_self_of_count_le <| subperm_ext_iff.1 hl).symm.trans
    perm_append_comm).countP_eq _

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

Goal state before:
pp: case mp.zero
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs : Multiset β
m as : Multiset α
hm : a ::ₘ as = 0
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ 0 = b ::ₘ bs'

Tactic:
simp at hm

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

Goal state before:
pp: case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ tl.Nodup
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)

Tactic:
simp only [mem_cons, map, ihl hl.2]

Goal state after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ tl.Nodup
⊢ (update f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ b :: take n l = List.filter (fun a ↦ elem a (b :: take n l)) (b :: l)

Tactic:
Nodup.take_eq_filter_mem (Nodup.of_cons hl),

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ b :: List.filter (fun a ↦ elem a (take n l)) l =
    List.filter (fun a ↦ elem a (b :: List.filter (fun a ↦ elem a (take n l)) l)) (b :: l)
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ t : List α
h : l₁ ~ l₂
⊢ l₁.bagInter t ~ l₂.bagInter t

Tactic:
induction h generalizing t with

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ s - filter p s = filter (fun a ↦ ¬p a) s

Tactic:
by ext a; by_cases h : p a <;> simp [h]

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

Goal state before:
pp: case cons.cons
α : Type u_1
head✝¹ : α
tail✝¹ : List α
ih : ∀ {l₁ : List α}, l₁ <+: tail✝¹ → tail✝¹ = l₁ ++ drop l₁.length tail✝¹
head✝ : α
tail✝ : List α
h : head✝ :: tail✝ <+: head✝¹ :: tail✝¹
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝ ++ drop (head✝ :: tail✝).length (head✝¹ :: tail✝¹)

Tactic:
obtain ⟨rfl, h'⟩ := List.cons_prefix_cons.mp h
      simpa using ih h'

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.reverse.inits = (map reverse l.tails).reverse

Tactic:
tails_eq_inits l

Goal state after:
α : Type u_1
l : List α
⊢ l.reverse.inits = (map reverse (map reverse l.reverse.inits).reverse).reverse
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ map reverse l.tails = l.reverse.inits.reverse

Tactic:
tails_eq_inits l

Goal state after:
α : Type u_1
l : List α
⊢ map reverse (map reverse l.reverse.inits).reverse = l.reverse.inits.reverse
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
f : α → β
⊢ (Multiset.map f univ.val).Nodup ↔ Injective f

Tactic:
nodup_map_iff_injOn,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
f : α → β
⊢ Set.InjOn f ↑univ ↔ Injective f