mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x✝ : α
l₁✝ l₂✝ : List α
h✝ : l₁✝ ~ l₂✝
r : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
b : β
⊢ foldr f b (x✝ :: l₁✝) = foldr f b (x✝ :: l₂✝)

Tactic:
simp [r b]

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

Goal state before:
pp: α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l).flatten.getLast? = l.getLast?

Tactic:
rw [← List.head?_reverse, ← List.head?_reverse, List.reverse_flatten, List.map_replicate,
  List.reverse_replicate, head?_flatten_replicate h]

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case e'_4
M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
p : ℤ × M
⊢ ((fun x ↦ zpow' x.2 x.1) ∘ fun x ↦ (-x.1, x.2)) p = ((fun x ↦ x⁻¹) ∘ fun x ↦ zpow' x.2 x.1) p

Tactic:
simp [zpow'_neg]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Semiring α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : AddLeftMono α
inst✝ : PosMulMono α
⊢ MonoidWithZero { x // 0 ≤ x }

Tactic:
infer_instance

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

Goal state before:
pp: case cons
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
head✝ : α
tail✝ : List α
l_ih :
  ∀ (mb : m β),
    (do
        let b ← mb
        foldlM f b tail✝) =
      foldl
        (fun mb a ↦ do
          let b ← mb
          f b a)
        mb tail✝
⊢ ∀ (mb : m β),
    (do
        let b ← mb
        foldlM f b (head✝ :: tail✝)) =
      foldl
        (fun mb a ↦ do
          let b ← mb
          f b a)
        mb (head✝ :: tail✝)

Tactic:
intro

Goal state after:
case cons
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
head✝ : α
tail✝ : List α
l_ih :
  ∀ (mb : m β),
    (do
        let b ← mb
        foldlM f b tail✝) =
      foldl
        (fun mb a ↦ do
          let b ← mb
          f b a)
        mb tail✝
mb✝ : m β
⊢ (do
      let b ← mb✝
      foldlM f b (head✝ :: tail✝)) =
    foldl
      (fun mb a ↦ do
        let b ← mb
        f b a)
      mb✝ (head✝ :: tail✝)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q✝ a b c : ℚ
n : ℕ
q : ℚ
⊢ ↑(↑n + 1) * q = n • q + q

Tactic:
rw [Rat.intCast_add, Rat.add_mul, Rat.intCast_one, Rat.one_mul]

Goal state after:
q✝ a b c : ℚ
n : ℕ
q : ℚ
⊢ ↑↑n * q + q = n • q + q
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q a b c : ℚ
⊢ AddGroup ℚ

Tactic:
infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ AddCommMonoid ℚ

Tactic:
infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ AddMonoid ℚ

Tactic:
infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ AddLeftCancelSemigroup ℚ

Tactic:
infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ AddRightCancelSemigroup ℚ

Tactic:
infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ AddCommSemigroup ℚ

Tactic:
infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ AddSemigroup ℚ

Tactic:
infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ Monoid ℚ

Tactic:
infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ CommSemigroup ℚ

Tactic:
infer_instance

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

Goal state before:
pp: q a b c : ℚ
⊢ Semigroup ℚ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ CommSemiring ℚ

Tactic:
infer_instance

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

Goal state before:
pp: ⊢ Semiring ℚ

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ ↑u * b ↔ a ∣ b

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ b * ↑u ↔ a ∣ b
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ ↑u * a ∣ b ↔ a ∣ b

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a * ↑u ∣ b ↔ a ∣ b
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x : α
x✝ : x ∣ 1
y : α
h : 1 = x * y
⊢ y * x = x * y

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
x : α
x✝ : x ∣ 1
y : α
h : 1 = x * y
⊢ x * y = x * y
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hx : IsPrimal x
⊢ x * y ∣ z

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hx : IsPrimal x
⊢ y * x ∣ z
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 : ℚ
⊢ q.num * q.num / ↑((q.num.natAbs * q.num.natAbs).gcd (q.den * q.den)) = q.num * q.num

Tactic:
Nat.Coprime.gcd_eq_one,

Goal state after:
q : ℚ
⊢ q.num * q.num / ↑1 = q.num * q.num

q : ℚ
⊢ (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
⊢ q.den * q.den / (q.num.natAbs * q.num.natAbs).gcd (q.den * q.den) = q.den * q.den

Tactic:
Nat.Coprime.gcd_eq_one,

Goal state after:
q : ℚ
⊢ q.den * q.den / 1 = q.den * q.den

q : ℚ
⊢ (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ (q * r).num * (↑q.den * ↑r.den) = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den

Tactic:
mul_comm

Goal state after:
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ ↑q.den * ↑r.den * (q * r).num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ ¬c = 0 →
    ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
      (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den

Tactic:
intro

Goal state after:
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
⊢ ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
    (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ (q + r).num * (↑q.den * ↑r.den) = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den

Tactic:
mul_comm

Goal state after:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ ↑q.den * ↑r.den * (q + r).num = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ ¬c = 0 →
    ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
      (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den

Tactic:
intro

Goal state after:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q + r = s
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * s.num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑s.den

Tactic:
mul_comm

Goal state after:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q + r = s
⊢ s.num * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑s.den
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
n e e' : α
h : n * e = e'
h2 : n ≠ 0
⊢ e * n = e'

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝ : Field α
n e e' : α
h : e * n = e'
h2 : n ≠ 0
⊢ e * n = e'
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n e1 e2 t1 t2 : α
h1 : n * e1 = t1
h2 : n * e2 = t2
⊢ n * (e1 + e2) = t1 + t2

Tactic:
by simp [left_distrib, *]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' + b' = c
⊢ a + b = c

Tactic:
by
  subst_vars; rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' * b' = c
⊢ a * b = c

Tactic:
by
  subst_vars; rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b b' c : R
a a' : ℕ
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' • b' = c
⊢ a • b = c

Tactic:
by
  subst_vars; rfl

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
b b' c : R
a a' : ℤ
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' • b' = c
⊢ a • b = c

Tactic:
by
  subst_vars; rfl

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

Goal state before:
pp: β : Type u_2
ι : Sort u_5
s : ι → Set β
⊢ ⋃ i, s i = (⋂ i, (s i)ᶜ)ᶜ

Tactic:
by
  simp only [compl_iInter, compl_compl]

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✝ : α
⊢ IsLUB (eval x✝ '' x✝¹) (sSup x✝¹ x✝)

Tactic:
by rw [sSup_apply_eq_sSup_image]; exact isLUB_sSup _

Goal state after:
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:
ext; simp +contextual [@and_comm (r _ _), h]

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

Goal state before:
pp: case inr
α : 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 : α
hb : b ∈ upperBounds t
x : α
hx : x ∈ s
⊢ x ≤ b

Tactic:
rcases hs x hx with ⟨y, hy, hxy⟩

Goal state after:
case inr
α : 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 : α
hb : b ∈ upperBounds t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : x ≤ y
⊢ x ≤ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α : 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
Bs : BddAbove s
b : α
hb : b ∈ upperBounds s
y : α
hy : y ∈ t
x : α
hx : x ∈ s
hyx : y ≤ x
⊢ y ≤ b

Tactic:
exact hyx.trans (hb hx)

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

Goal state before:
pp: case neg.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
hb : b ∈ (fun a ↦ ↑a) ⁻¹' s
⊢ a ≤ b

Tactic:
← coe_le_coe

Goal state after:
case neg.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
hb : b ∈ (fun a ↦ ↑a) ⁻¹' s
⊢ ↑a ≤ ↑b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ Option.some a ≤ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))

Tactic:
refine coe_le_coe.2 (le_csInf ?_ ?_)
        · classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim
        · intro b hb
          rw [← coe_le_coe]
          exact ha hb

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

Goal state before:
pp: ι : Type u_4
s : Set ι
⊢ s.PairwiseDisjoint singleton

Tactic:
intro

Goal state after:
ι : Type u_4
s : Set ι
x✝ : ι
⊢ x✝ ∈ s → ∀ ⦃y : ι⦄, y ∈ s → x✝ ≠ y → (Disjoint on singleton) x✝ y
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ uIoo a b ⊆ [[a, b]]

Tactic:
simp [uIoo, uIcc, Ioo_subset_Icc_self]

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✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
S T : A
⊢ ↑S ⊂ ↑T ↔ S < T

Tactic:
ssubset_iff_subset_ne,

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
S T : A
⊢ ↑S ⊆ ↑T ∧ ↑S ≠ ↑T ↔ S < T
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
ht : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun x ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun x ↦ x ∈ s) b
⊢ {x | Maximal (fun x ↦ x ∈ s) x} = t

Tactic:
by
  refine Set.ext fun x ↦ ⟨h _, fun hx ↦ ?_⟩
  obtain ⟨y, hyx, hy⟩ := hs x hx
  rwa [← ht.eq (h y hy) hx hyx]

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

Goal state before:
pp: a b q m a' : ℤ
b' r : ℕ
ha : IsInt a a'
hb : IsNat b b'
hm : q * ↑b' = m
h : ↑r + m = a'
h₂ : r.blt b' = true
⊢ a / b = ↑q

Tactic:
obtain ⟨⟨rfl⟩, ⟨rfl⟩⟩ := ha, hb

Goal state after:
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ a / ↑b' = ↑q
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a b q m a' : ℤ
b' r : ℕ
ha : IsInt a a'
hb : IsNat b b'
hm : q * ↑b' = m
h : ↑r + m = a'
h₂ : r.blt b' = true
⊢ a % b = ↑r

Tactic:
obtain ⟨⟨rfl⟩, ⟨rfl⟩⟩ := ha, hb

Goal state after:
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ a % ↑b' = ↑r
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: case neg
ι : 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_apply' _ _ _ hf]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
⊢ Injective fun a ↦ (a⁺ᵐ, a⁻ᵐ)

Tactic:
by
  simp only [Injective, Prod.mk.injEq, and_imp]
  rintro a b hpos hneg
  rw [← oneLePart_div_leOnePart a, ← oneLePart_div_leOnePart b, hpos, hneg]

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

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LE «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» «$nb» : ℕ
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»

Tactic:
infer_instance

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

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LT «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» «$nb» : ℕ
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»

Tactic:
infer_instance

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

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

Tactic:
intro

Goal state after:
n : ℕ
a✝ : 2 ≤ 1
⊢ (n + 1) ^ 1 < (n + 1).ascFactorial 1
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
intro

Goal state after:
n : ℕ
a✝ : 2 ≤ 1
⊢ (n + 1).ascFactorial 1 < (n + 1) ^ 1
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
intro

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 2 ≤ 1 → n.descFactorial 1 < n ^ 1

Tactic:
intro

Goal state after:
n : ℕ
hn : n ≠ 0
a✝ : 2 ≤ 1
⊢ n.descFactorial 1 < n ^ 1
Module: Mathlib.Algebra.Order.Round

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

Tactic:
rw [round_add_intCast, sub_eq_add_neg]

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

Goal state before:
pp: m k : ℕ+
⊢ ↑(m.mod k) + m.div k * ↑k = ↑m

Tactic:
mul_comm

Goal state after:
m k : ℕ+
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m k : ℕ+
⊢ m.div k * ↑k + ↑(m.mod k) = ↑m

Tactic:
mul_comm

Goal state after:
m k : ℕ+
⊢ ↑k * m.div k + ↑(m.mod k) = ↑m
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 b : R
⊢ ↑(⌊a⌋ + ⌊b⌋) ≤ a + b

Tactic:
Int.cast_add

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a⌋ + ↑⌊b⌋ ≤ a + b
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℤ
hn✝ : 0 ≤ n
a : k
hn : 0 < n
⊢ ⌊a / ↑n⌋ = ⌊a / ↑n * ↑n⌋ / n

Tactic:
rw [mul_cast_floor_div_cancel_of_pos hn]

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
a b : R
z : ℤ
hz : a - b = ↑z
⊢ b + ↑z - fract b = ↑(z + ⌊b⌋)

Tactic:
Int.cast_add

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
z : ℤ
hz : a - b = ↑z
⊢ b + ↑z - fract b = ↑z + ↑⌊b⌋
Module: Mathlib.Algebra.Order.Ring.Pow

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

Tactic:
by
  simpa using (Commute.one_left a).pow_add_mul_le_add_pow_of_sq_nonneg zero_le_one Hsq Hsq'
    (by simpa using H) 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
inst✝ : IsOrderedRing R
a b : R
⊢ a + b ≤ ↑(⌈a⌉ + ⌈b⌉)

Tactic:
Int.cast_add

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a + b ≤ ↑⌈a⌉ + ↑⌈b⌉
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✝
⊢ ∃ n, x ≤ x✝ ^ n

Tactic:
refine (MulArchimedean.arch (f x) (by simpa using hf h)).imp ?_
    simp [← map_pow, hf.le_iff_le]

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

Tactic:
by
  simpa using (AddConstMapClass.semiconj f).iterate_right n x

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

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

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
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉

Tactic:
· exact Or.inl ha

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
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ a
⊢ ↑⌈a⌉ ≤ b * a

Tactic:
by
  obtain rfl | hba := hba.eq_or_lt
  · rw [ceil_div_ceil_inv_sub_one hb.le, mul_div_cancel₀]
    positivity
  · exact (ceil_lt_mul hb hba).le

Goal state after:
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_inv_num_denom_ineq : ↑q.den - ⌊q_inv⌋ * q.num < q.num
this : q_inv.num = ↑q.den ∧ q_inv.den = q.num.natAbs
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num

Tactic:
mul_comm

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_inv_num_denom_ineq : ↑q.den - q.num * ⌊q_inv⌋ < q.num
this : q_inv.num = ↑q.den ∧ q_inv.den = q.num.natAbs
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ ↑⌈a⌉₊ = ↑⌈a⌉

Tactic:
← Int.natCast_ceil_eq_ceil ha,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ ↑⌈a⌉₊ = ↑↑⌈a⌉₊