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

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 ≤ 0
ha₁ : 0 ≠ 1
⊢ 0 ^ n = 1 ↔ n = 0

pp: case inr
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
ha₀✝ : 0 ≤ a
ha₁ : a ≠ 1
n : ℤ
ha₀ : 0 < a
⊢ a ^ n = 1 ↔ n = 0

Tactic:
· exact zero_zpow_eq_one₀

Goal state after:
case inr
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
ha₀✝ : 0 ≤ a
ha₁ : a ≠ 1
n : ℤ
ha₀ : 0 < a
⊢ a ^ n = 1 ↔ n = 0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ a ^ (n + 2) = a ^ (n + 1) * a

Tactic:
by rw [pow_succ]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) / (a ⊓ b) = |b / a|ₘ

Tactic:
simp_rw [sup_div, div_inf, div_self', sup_comm, sup_sup_sup_comm, sup_idem]
  rw [← inv_div, sup_comm (b := _ / _), ← mabs, sup_eq_left]
  exact one_le_mabs _

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ ≤ |a / b|ₘ

Tactic:
by
  apply le_of_mul_le_of_one_le_left _ (one_le_mabs _); rw [mabs_div_sup_mul_mabs_div_inf]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
⊢ a⁻¹ ≤ b⁻¹

Tactic:
exact inv_le_inv_iff.mpr hab

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: k n : ℕ
hk : n.gcd k < k
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k

Tactic:
have hk' := Int.ofNat_ne_zero.2 (Nat.zero_lt_of_lt hk).ne'

Goal state after:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
⊢ 1 < a * b ↔ 1 < a ∨ 1 < b

Tactic:
by
  simp only [one_lt_iff_ne_one, Ne, mul_eq_one, not_and_or]

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Monoid M
a : M
n : ℕ
hn : a ^ n = 1
m : ℕ
hm : a ^ (m + 1) = 1
⊢ a ^ (m + 1).gcd n = 1

Tactic:
obtain ⟨y, rfl⟩ := IsUnit.of_pow_eq_one hm m.succ_ne_zero

Goal state after:
case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : ↑y ^ n = 1
hm : ↑y ^ (m + 1) = 1
⊢ ↑y ^ (m + 1).gcd n = 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
m n : ℕ
hmn : m.Coprime n
c : α
hab : Commute (c ^ n) (c ^ m)
⊢ (c ^ n) ^ m = (c ^ m) ^ n

Tactic:
← pow_mul,

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
m n : ℕ
hmn : m.Coprime n
c : α
hab : Commute (c ^ n) (c ^ m)
⊢ c ^ (n * m) = (c ^ m) ^ n
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
hb : b ≠ ⊤
a : α
⊢ a + b + -b = a

Tactic:
simp [add_assoc, add_neg_cancel_of_ne_top hb]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
x : β
⊢ e.symm ↑x ≠ 0

Tactic:
simp [e.symm_apply_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
⊢ ∀ (x y : α),
    { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun (x * y) =
      { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun x *
        { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun y

Tactic:
by intro; simp [← coe_inj]

Goal state after:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case pos
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Tactic:
findGreatest_eq h,

Goal state after:
case pos
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : P (n + 1)
⊢ n + 1 ≤ findGreatest Q (n + 1)
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_3
κ : Sort u_4
r r' s : α → α → Prop
inst✝¹ : LE α
inst✝ : IsDirectedOrder α
⊢ IsCodirectedOrder αᵒᵈ

Tactic:
by
  assumption

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Even n
⊢ (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)

Tactic:
obtain ⟨n, rfl⟩ := hn

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ (a + b) ^ (n + n) ≤ 2 ^ (n + n - 1) * (a ^ (n + n) + b ^ (n + n))
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a : K
⊢ a = a⁻¹ ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
by
  rw [eq_comm, inv_eq_self₀]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
ratCast : ∀ (q : ℚ), f ↑q = ↑q
q : ℚ
a : K
⊢ f (q • a) = f (↑q * a)

Tactic:
qsmul,

Goal state after:
K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
ratCast : ∀ (q : ℚ), f ↑q = ↑q
q : ℚ
a : K
⊢ q • f a = f (↑q * a)
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictAnti f
⊢ f a ∈ upperBounds (f '' s) ↔ a ∈ lowerBounds s

Tactic:
simp [upperBounds, lowerBounds, hf.le_iff_ge]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictAnti f
⊢ f a ∈ lowerBounds (f '' s) ↔ a ∈ upperBounds s

Tactic:
simp [upperBounds, lowerBounds, hf.le_iff_ge]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
hbdd : BddAbove (range g)
⊢ BddAbove (range f)

Tactic:
obtain ⟨C, hC⟩ := hbdd
  use C
  rintro - ⟨x, rfl⟩
  exact (h x).trans (hC <| mem_range_self x)

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
x : α
⊢ ¬Acc r x ↔ Nonempty { f // f 0 = x ∧ ∀ (n : ℕ), r (f (n + 1)) (f n) }

Tactic:
rw [nonempty_subtype]

Goal state after:
α : Sort u_1
r : α → α → Prop
x : α
⊢ ¬Acc r x ↔ ∃ a, a 0 = x ∧ ∀ (n : ℕ), r (a (n + 1)) (a n)
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ t.Nonempty

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
    · aesop
    · exact .inl ⟨h, hs⟩

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a ≤ 1 / b ↔ b ≤ 1 / a

Tactic:
simpa using le_inv_of_neg ha hb

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
h1 : a < 0
h2 : -1 < a
this : 1 / a < 1 / -1
⊢ 1 / a < -1

Tactic:
rwa [one_div_neg_one_eq_neg_one] at this

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
h1 : a < 0
h2 : -1 ≤ a
this : 1 / a ≤ 1 / -1
⊢ 1 / a ≤ -1

Tactic:
rwa [one_div_neg_one_eq_neg_one] at this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : α → β → Prop
P : γ → δ → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P (filterMap f (a :: as)) (filterMap g (b :: bs))

Tactic:
by
    rw [filterMap_cons, filterMap_cons]
    exact
      match f a, g b, hfg h₁ with
      | _, _, Option.Rel.none => rel_filterMap (@hfg) h₂
      | _, _, Option.Rel.some h => Forall₂.cons h (rel_filterMap (@hfg) h₂)

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

Goal state before:
pp: case mpr.cons_cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
l₁ : List α
hl1 : Forall₂ R l₁ (a✝¹ :: l₁✝)
⊢ SublistForall₂ R l₁ (a✝¹ :: l₂✝)

Tactic:
obtain - | ⟨hr, hl⟩ := hl1

Goal state after:
case mpr.cons_cons.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝¹ l₂✝ : List β
a✝² : β
a✝¹ : l₁✝¹ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝¹ → SublistForall₂ R l₁ l₂✝
a✝ : α
l₁✝ : List α
hr : R a✝ a✝²
hl : Forall₂ R l₁✝ l₁✝¹
⊢ SublistForall₂ R (a✝ :: l₁✝) (a✝² :: l₂✝)
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inr
α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
this : ∀ {l₁ l₂ : List α}, l₁.length ≤ l₂.length → (l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂)
hle : ¬l₁.length ≤ l₂.length
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
perm_comm,

Goal state after:
case inr
α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
this : ∀ {l₁ l₂ : List α}, l₁.length ≤ l₂.length → (l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂)
hle : ¬l₁.length ≤ l₂.length
⊢ l₂.insertIdx n a ~ l₁.insertIdx n a ↔ l₁ ~ l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mpr
α : Type u
⊢ Subsingleton α → Injective length

Tactic:
· intro hα l1 l2 hl
    induction l1 generalizing l2 <;> cases l2
    · rfl
    · cases hl
    · cases hl
    · next ih _ _ =>
      congr
      · subsingleton
      · apply ih; simpa using hl

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

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
l : List α
h : l ≠ []
h' : l.head! ∈ l.head! :: l.tail
⊢ l.head! ∈ l

Tactic:
rwa [cons_head!_tail h] at h'

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

Goal state before:
pp: case refine_2
α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : idxOf a l₂ < l₁.length
⊢ a ∈ l₁

Tactic:
have := hl.idxOf_le a

Goal state after:
case refine_2
α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : idxOf a l₂ < l₁.length
this : idxOf a l₁ ≤ idxOf a l₂
⊢ a ∈ l₁
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : l₁.eval / (a₂ ::ᵣ l₂).eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval / (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

Tactic:
by
  simp only [eval_cons, ← h, div_eq_mul_inv]
  ac_rfl

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
i : ℕ
hlen : i < l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute l[i] a'
a' : M
a'_mem : a' ∈ take i (l.eraseIdx i)
⊢ a' ∈ take i l

Tactic:
rwa [take_eraseIdx_eq_take_of_le l i i (Nat.le_refl i)] at a'_mem

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

Goal state before:
pp: case cons
ι : Type u_1
α : Type u
β : Type v
γ : Type w
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
head✝ : ι
tail✝ : List ι
tail_ih✝ : ∀ (a : α) (b : β), f (foldl op₁ a tail✝) (foldl op₂ b tail✝) = foldl op₃ (f a b) tail✝
a✝ : α
b✝ : β
⊢ f (foldl op₁ a✝ (head✝ :: tail✝)) (foldl op₂ b✝ (head✝ :: tail✝)) = foldl op₃ (f a✝ b✝) (head✝ :: tail✝)

Tactic:
simp only [*, foldl]

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

Goal state before:
pp: L : List ℕ
⊢ L.tail.sum = L.sum - L.headI

Tactic:
by
  rw [← headI_add_tail_sum L, add_comm, Nat.add_sub_cancel_right]

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

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ ↑(Int.negSucc x✝¹) * x✝ = -(↑↑x✝¹.succ * x✝)

Tactic:
rw [Int.negSucc_eq, Rat.intCast_neg, Rat.neg_mul]

Goal state after:
q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ -(↑(↑x✝¹ + 1) * x✝) = -(↑↑x✝¹.succ * x✝)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q a✝ b c : ℚ
C : ℚ → Sort u_1
a : ℚ
div : (n : ℤ) → (d : ℕ) → d ≠ 0 → n.natAbs.Coprime d → C (↑n / ↑d)
n : ℤ
d : ℕ
nz : d ≠ 0
red : n.natAbs.Coprime d
⊢ C (n /. ↑d)

Tactic:
Rat.divInt_eq_div

Goal state after:
q a✝ b c : ℚ
C : ℚ → Sort u_1
a : ℚ
div : (n : ℤ) → (d : ℕ) → d ≠ 0 → n.natAbs.Coprime d → C (↑n / ↑d)
n : ℤ
d : ℕ
nz : d ≠ 0
red : n.natAbs.Coprime d
⊢ C (↑n / ↑↑d)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: a : ℤ
b : ℕ
hb : b ≠ 0
⊢ mkRat a b < 0 ↔ a < 0

Tactic:
grind [mkRat_nonneg_iff]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
⊢ SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y

Tactic:
simp_rw [SemiconjBy, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul, eq_comm]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑↑a / ↑b

Tactic:
← cast_natCast b,

Goal state after:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑↑a / ↑↑b
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 }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ ↑d ≠ 0

Tactic:
refine fun hd ↦ hb ?_

Goal state after:
α : 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 }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
hd : ↑d = 0
⊢ ↑b = 0
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := ⋯
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.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 ∨
    c = 0

Tactic:
rw [or_iff_not_imp_right]

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
⊢ ¬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.Tactic.NormNum.Inv

Goal state before:
pp: n✝¹ num✝ : ℤ
n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsRat (mkRat ↑n✝¹ ↑n✝) num✝ denom✝

Tactic:
rw [Rat.mkRat_eq_div]

Goal state after:
n✝¹ num✝ : ℤ
n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsRat (↑↑n✝¹ / ↑↑n✝) num✝ denom✝
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ (Int.ofNat a ^ 2) ^ b' = Int.ofNat c

Tactic:
← pow_mul,

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.ofNat a ^ (2 * b') = Int.ofNat c
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ (Int.ofNat a ^ 2) ^ b' * -Int.ofNat a = -Int.ofNat c

Tactic:
← pow_mul,

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ Int.ofNat a ^ (2 * b') * -Int.ofNat a = -Int.ofNat c
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a < b) = (1 / gcd * (bd * a') < 1 / gcd * (ad * b'))

Tactic:
by
  rw [mul_lt_mul_iff_right₀, ← ha, ← hb, ← mul_assoc, ← mul_assoc, mul_comm bd,
    mul_lt_mul_iff_right₀]
  · exact mul_pos had hbd
  · exact one_div_pos.2 hgcd

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

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

Tactic:
by
  subst_vars; simp [add_comm]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLinearOrder α
f : ι → α
⊢ iSup f = ⊤ ↔ ∀ b < ⊤, ∃ i, b < f i

Tactic:
rw [eq_top_iff, le_iSup_iff_forall_lt]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLattice α
a : α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j ≤ a ↔ ∀ (i : ι) (j : κ i), f i j ≤ a

Tactic:
simp_rw [iSup_le_iff]

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

Goal state before:
pp: case mpr
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
⊢ x ∈ ⋃ y, range fun s ↦ ↑(f s y)

Tactic:
obtain ⟨y, hy⟩ := hf ⟨s, hs⟩ ⟨x, hx⟩

Goal state after:
case mpr
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
y : β
hy : f ⟨s, hs⟩ y = ⟨x, hx⟩
⊢ x ∈ ⋃ y, range fun s ↦ ↑(f s y)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLinearOrder α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j = ⊤ ↔ ∀ b < ⊤, ∃ i j, b < f i j

Tactic:
simp_rw [iSup_psigma', iSup_eq_top, PSigma.exists]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
hs : BddAbove ∅
⊢ IsLUB ∅ (sSup ∅)

pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
hne : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
· simp only [csSup_empty, isLUB_empty]

Goal state after:
case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
hne : s.Nonempty
⊢ IsLUB s (sSup s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.some.refine_1.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb✝ : Option.some b ∈ upperBounds s
hb : none ∈ s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty

pp: case pos.some.refine_1.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b✝ : β
hb✝ : Option.some b✝ ∈ upperBounds s
b : β
hb : Option.some b ∈ s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty

Tactic:
· exact absurd hb h₁

Goal state after:
case pos.some.refine_1.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b✝ : β
hb✝ : Option.some b✝ ∈ upperBounds s
b : β
hb : Option.some b ∈ s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
h : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ i = j ∨ Disjoint (f i) (f j)

Tactic:
rw [or_iff_not_imp_right]

Goal state after:
α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
h : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ¬Disjoint (f i) (f j) → i = j
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompletelyDistribLattice β
completeDistribLattice : CompleteDistribLattice α := e.completeDistribLattice
⊢ CompletelyDistribLattice α

Tactic:
apply e.injective.completelyDistribLattice <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Icc x y = Icc (e x) (e y)

Tactic:
rw [← e.preimage_Icc, image_preimage_eq_inter_range, inter_eq_left.2 (he.out ⟨_, rfl⟩ ⟨_, rfl⟩)]

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, b = a + c

Tactic:
rw [← Subtype.coe_le_coe] at h

Goal state after:
α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
a b : { x // 0 ≤ x }
h : ↑a ≤ ↑b
⊢ ∃ c, b = a + c
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
  simp only [Nat.blt_eq] at h₂; simp only [← h, ← hm, Int.cast_id]
  rw [Int.add_mul_ediv_right _ _ (Int.ofNat_ne_zero.2 ((Nat.zero_le ..).trans_lt h₂).ne')]
  rw [Int.ediv_eq_zero_of_lt, zero_add] <;> [simp; simpa using h₂]

Goal state after: