mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n = 0 → b = true
ih : motive n
h' : n = 0
⊢ Nat.bit b n = Nat.bit true 0

Tactic:
by
        rw [h', h h']

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

Goal state before:
pp: motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ∀ (e : motive (bit b (bit b n >>> 1)) = motive (bit b n)), e ▸ h b (bit b n >>> 1) = h b n

Tactic:
bit_shiftRight_one

Goal state after:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ∀ (e : motive (bit b n) = motive (bit b n)), e ▸ h b n = h b n
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
⊢ ∀ (e : motive (Nat.bit b (Nat.bit b n >>> 1)) = motive (Nat.bit b n)),
    e ▸ bit b (Nat.bit b n >>> 1) (binaryRec zero bit (Nat.bit b n >>> 1)) = bit b n (binaryRec zero bit n)

Tactic:
bit_shiftRight_one

Goal state after:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
⊢ ∀ (e : motive (Nat.bit b n) = motive (Nat.bit b n)),
    e ▸ bit b n (binaryRec zero bit n) = bit b n (binaryRec zero bit n)
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: case ind
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k' → npowRec' (2 * m_1) m = npowRec' m_1 (m * m)
⊢ npowRec' (2 * k') m = npowRec' k' (m * m)

Tactic:
| ind k' ih =>

Goal state after:
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: case ind
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k' → m_1 ≠ 0 → m * npowRec' m_1 m = npowRec' m_1 m * m
k0 : k' ≠ 0
⊢ m * npowRec' k' m = npowRec' k' m * m

Tactic:
| ind k' ih =>

Goal state after:
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: case ind
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k' → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k' + 1) m = 1 * npowRec' (k' + 1) m

Tactic:
| ind k' ih =>

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
h : ∃! x, ∃! hx, q x hx
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
⊢ y₁ = y₂

Tactic:
by
  simp only [existsUnique_iff_exists] at h
  exact h.unique ⟨hpy₁, hqy₁⟩ ⟨hpy₂, hqy₂⟩

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
r p q : α → Prop
⊢ (∃ x, (p x ∨ q x) ∧ r x) ↔ (∃ x, p x ∧ r x) ∨ ∃ x, q x ∧ r x

Tactic:
exact Iff.trans (exists_congr fun x ↦ or_and_right) exists_or

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
⊢ Injective g

Tactic:
intro s

Goal state after:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
s : Set T
⊢ ∀ ⦃a₂ : Set T⦄, g s = g a₂ → s = a₂
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
motive : {a b : α} → ReflTransGen r a b → Prop
a b : α
refl : ∀ (a : α), motive ⋯
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯
b✝ c✝ : α
hab : ReflTransGen r a b✝
hbc : r b✝ c✝
ih : motive hab
⊢ motive ⋯

Tactic:
| tail hab hbc ih =>

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝¹ : Mul R
inst✝ : IsRightCancelMul R
r₁ r₂ : R
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
by simpa using h r₁

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ FaithfulSMul G α ↔ ∀ (g : G), (∀ (a : α), g • a = a) → g = 1

Tactic:
refine ⟨fun h a ha ↦ h.eq_of_smul_eq_smul ?_, fun h ↦ ⟨fun {a₁ a₂} h' ↦ ?_⟩⟩
  · simpa only [one_smul]
  · rw [← inv_inv a₂, eq_inv_of_mul_eq_one_left (h (a₂⁻¹ * a₁) ?_), inv_inv]
    simpa only [mul_smul, inv_smul_eq_iff] using h'

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝ : LE α
⊢ NoBotOrder α ↔ ∀ (x : α), ¬IsBot x

Tactic:
simp_rw [noBotOrder_iff', IsBot, not_forall]

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

Goal state before:
pp: n m : Nat
h : n ≤ m
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Tactic:
cases Nat.decEq n 0 with
  | isTrue hn => grind [Bool.false_le]
  | isFalse hn => cases Nat.decEq m 0 with grind [Bool.le_true]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x = y ↔ x' = y'

Tactic:
by
  rw [le_antisymm_iff, le_antisymm_iff, le_iff_le_of_cmp_eq_cmp h,
      le_iff_le_of_cmp_eq_cmp (cmp_eq_cmp_symm.1 h)]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictMono (f ∘ ⇑ofDual) ↔ StrictAnti f

Tactic:
strictMono_comp_ofDual_iff

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictAnti f ↔ StrictAnti f
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
p : α → Prop
⊢ (∀ (x : α), x ∈ s ∧ p x ↔ x ∈ ∅) ↔ ∀ (x : α), x ∈ s → ¬p x

Tactic:
mem_empty_iff_false,

Goal state after:
α : Type u
s : Set α
p : α → Prop
⊢ (∀ (x : α), x ∈ s ∧ p x ↔ False) ↔ ∀ (x : α), x ∈ s → ¬p x
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: case refine_2
α : Type u
s : Set α
h : s.Nonempty ∧ s.Subsingleton
⊢ ∃ a, s = {a}

Tactic:
· exact h.2.eq_empty_or_singleton.resolve_left h.1.ne_empty

Goal state after:
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case some.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝
h2 : e (some x) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
rw [removeNoneAux_none _ h2] at h1

Goal state after:
case some.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (e none) = some val✝
h2 : e (some x) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' univ ⊆ s ↔ range f ⊆ s

Tactic:
image_univ

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ range f ⊆ s ↔ range f ⊆ s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' univ \ s = range f \ s

Tactic:
image_univ

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ range f \ s = range f \ s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' (f ⁻¹' s)ᶜ = range f \ s

Tactic:
rw [compl_eq_univ_sdiff, image_sdiff_preimage, image_univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ Surjective (image f)

Tactic:
intro s

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ ∃ a, f '' a = s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Injective (image f)

Tactic:
intro s

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ ∀ ⦃a₂ : Set α⦄, f '' s = f '' a₂ → s = a₂
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ y = z

Tactic:
apply hf (hs ys) (ht zt)

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ f y = f z
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
g : ι → G
n : ℤ
⊢ ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n

Tactic:
by
  ext; simp [map_zpow' f hf]

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

Goal state before:
pp: motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ zero ≍
    match b - b with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] => inductionOn'.neg b zero pred n

Tactic:
by rw [b.sub_self, ← cast_eq_iff_heq]; rfl

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

Goal state before:
pp: a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * (k * d)
⊢ a = k * d

Tactic:
Int.mul_eq_mul_left_iff hb

Goal state after:
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : a = k * d
⊢ a = k * d
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₁
inst✝² : One M₁
inst✝¹ : Pow M₁ ℕ
inst✝ : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ (n + 1)) = f (x ^ n * x)

Tactic:
rw [npow, pow_succ, mul, npow]

Goal state after:
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u = a
⊢ ↑u⁻¹ * ↑u = 1

Tactic:
u.inv_mul

Goal state after:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : ↑u = a
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
⊢ IsUnit a

Tactic:
by
      have : IsUnit (↑u⁻¹ * (↑u * a)) := by exists u⁻¹ * v; rw [← hv, Units.val_mul]
      rwa [← mul_assoc, Units.inv_mul, one_mul] at this

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : α → m β
⊢ f >=> pure = f

Tactic:
by
  simp +unfoldPartialApp only [(· >=> ·), functor_norm]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
f : α → m β
⊢ pure >=> f = f

Tactic:
by
  simp +unfoldPartialApp only [(· >=> ·), functor_norm]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β γ φ : Type u
f : α → m β
g : β → m γ
h : γ → m φ
⊢ (f >=> g) >=> h = f >=> g >=> h

Tactic:
by
  simp +unfoldPartialApp only [(· >=> ·), functor_norm]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
f : α → β
a : m (m α)
⊢ joinM (Functor.map f <$> a) = f <$> joinM a

Tactic:
simp only [joinM, id, ← bind_pure_comp, bind_assoc, pure_bind]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
a : m (m (m α))
⊢ joinM (joinM <$> a) = joinM (joinM a)

Tactic:
simp only [joinM, id, ← bind_pure_comp, bind_assoc, pure_bind]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : FunLike F α β
inst✝¹ : ZeroHomClass F α β
a : α
f : F
hf : Injective ⇑f
inst✝ : NeZero a
⊢ f a ≠ 0

Tactic:
rw [← ZeroHomClass.map_zero f]; exact hf.ne NeZero.out

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝³ : Zero A
inst✝² : SMulZeroClass M A
inst✝¹ : Zero B
inst✝ : SMul M B
f : ZeroHom B A
hf : Injective ⇑f
smul : ∀ (c : M) (x : B), f (c • x) = c • f x
c : M
⊢ f (c • 0) = f 0

Tactic:
by simp only [smul, map_zero, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: case zero
A : Type u_2
F : Type u_4
inst✝² : FunLike F ℕ A
inst✝¹ : AddZeroClass A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
⊢ 0 = g 0

Tactic:
map_zero g

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

Goal state before:
pp: α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∃ a, p₁ a) ↔ ∃ a, p₂ a

Tactic:
exact exists_congr fun a ↦ H a (p₁ a) (mem_map_of_mem hp₁)
    (p₂ a) (mem_map_of_mem hp₂)

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
⊢ ↑y⁻¹ * (↑y * a) * ↑x⁻¹ = ↑y⁻¹ * a

Tactic:
by rw [← h.eq, mul_assoc, Units.mul_inv_cancel_right]

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

Goal state before:
pp: case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
have := mul_ne_zero ha hx

Goal state after:
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : a * x ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
c a b : G₀
hc : c ≠ 0
⊢ c / a / (c / b) = b / a

Tactic:
rw [div_div_div_eq, mul_comm, mul_div_mul_right _ _ hc]

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

Goal state before:
pp: n : ℕ
⊢ ¬Even (2 * n + 1)

Tactic:
by simp [parity_simps]

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

Goal state before:
pp: case succ
k : ℕ
⊢ 2 ∣ (k + 1) * (k + 1 - 1)

Tactic:
simpa [mul_comm (k + 1)] using k.two_dvd_mul_add_one

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

Goal state before:
pp: k : ℕ
⊢ 2 ∣ k * (k - 1)

Tactic:
rcases k with rfl | k; · simp
  simpa [mul_comm (k + 1)] using k.two_dvd_mul_add_one

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - b ≤ c ↔ a - c ≤ b

Tactic:
by rw [tsub_le_iff_left, tsub_le_iff_right]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a * b⁻¹ < c ↔ a < c * b

Tactic:
by
  rw [← mul_lt_mul_iff_right b, inv_mul_cancel_right]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddMonoidWithOne R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : NeZero 1
inst✝ : AddLeftStrictMono R
n : ℕ
⊢ ↑n < ↑(n + 1)

Tactic:
by rw [Nat.cast_succ]; apply lt_add_one

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

Goal state before:
pp: case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hab : a < b
d : R
hd : 0 < d
hcd : c < c + d
⊢ 0 < d

Tactic:
exact hd

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

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
by
  rw [← neg_nonneg, neg_mul_eq_mul_neg, mul_nonneg_iff (R := R), neg_nonneg, neg_nonpos]

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

Goal state before:
pp: case mp
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧ → Acc r a

Tactic:
exact RelHomClass.acc (Quotient.mkRelHom H) a

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
h : Disjoint (f a₁) (f a₂)
x : α
h₁ : x ≤ a₁
h₂ : x ≤ a₂
⊢ x ≤ ⊥

Tactic:
rw [← f.le_iff_le] at h₁ h₂ ⊢

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
h : Disjoint (f a₁) (f a₂)
x : α
h₁ : f x ≤ f a₁
h₂ : f x ≤ f a₂
⊢ f x ≤ f ⊥
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ b = b / a * a

Tactic:
· rw [div_mul_cancel]

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

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
⊢ ∀ {s t s' t' : ℤ}, x.P y (a, s, t) → x.P y (b, s', t') → x.P y (a.xgcdAux s t b s' t')

Tactic:
intro s

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s : ℤ
⊢ ∀ {t s' t' : ℤ}, x.P y (a, s, t) → x.P y (b, s', t') → x.P y (a.xgcdAux s t b s' t')
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case refine_1
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ (n.gcdA k % ↑k).toNat < k

pp: case refine_2
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ↑(n * (n.gcdA k % ↑k).toNat % k) = ↑(↑n * n.gcdA k % ↑k).toNat

Tactic:
· rw [Int.toNat_lt (Int.emod_nonneg _ hk')]
    exact Int.emod_lt _ hk'

Goal state after:
case refine_2
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ↑(n * (n.gcdA k % ↑k).toNat % k) = ↑(↑n * n.gcdA k % ↑k).toNat
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ ↑(a.toNat * (p + 1) + b.toNat * (q + 1)) = ↑n

Tactic:
rw [Nat.cast_add, Nat.cast_mul, Nat.cast_mul, Int.natCast_toNat_eq_self.mpr
    (Int.emod_nonneg _ <| by lia), Int.natCast_toNat_eq_self.mpr, this]

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ 0 ≤ b
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
⊢ IsRightRegular b

Tactic:
refine fun x y xy => ab (?_ : x * (b * a) = y * (b * a))

Goal state after:
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x ↦ x * b) x = (fun x ↦ x * b) y
⊢ x * (b * a) = y * (b * a)
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a b : WithBot α
ha : a ≠ ⊥
hb : b ≠ ⊥
⊢ a.unbot ha = b.unbot hb ↔ a = b

Tactic:
rw [unbot_eq_iff, coe_unbot]

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

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) = (x + y) * (x ^ n + y ^ n)

Tactic:
rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
          add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
β : Type u_2
a✝¹ b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝ : (Antisymmetrization α fun x1 x2 ↦ x1 ≤ x2)ᵒᵈ
a : α
⊢ Quotient.map' id ⋯ (Quotient.map' id ⋯ (Quotient.mk'' a)) = Quotient.mk'' a

Tactic:
by simp_rw [Quotient.map'_mk'', id]

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
β : Type u_2
a✝¹ b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝ : Antisymmetrization αᵒᵈ fun x1 x2 ↦ x1 ≤ x2
a : αᵒᵈ
⊢ Quotient.map' id ⋯ (Quotient.map' id ⋯ (Quotient.mk'' a)) = Quotient.mk'' a

Tactic:
by simp_rw [Quotient.map'_mk'', id]

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

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ IsLeast {w | a ≤ b ⊔ w} (a \ b)

Tactic:
simp [IsLeast, mem_lowerBounds]

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
hb : 0 < b
⊢ 1 / a < b ↔ 1 / b < a

Tactic:
by
  simpa using inv_lt_comm₀ ha hb

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
l : List M
m : M
h : ∀ (x : M), x ∈ l → x = m
⊢ l.prod = m ^ l.length

Tactic:
← prod_replicate,

Goal state after:
M : Type u_2
inst✝ : Monoid M
l : List M
m : M
h : ∀ (x : M), x ∈ l → x = m
⊢ l.prod = (replicate l.length m).prod
Module: Mathlib.Tactic.NormNum.Basic

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

Tactic:
simp only [mul_invOf_cancel_right'] at h₂

Goal state after:
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
Module: Mathlib.Tactic.NormNum.Basic

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

Tactic:
simp only [mul_invOf_cancel_right'] at h₂

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
hr : BiUnique R
a : α
b : β
x✝ : R a b
⊢ (fun x1 x2 ↦ x1 ∈ x2) a [] ↔ (fun x1 x2 ↦ x1 ∈ x2) b []

Tactic:
simp only [not_mem_nil]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
by
  refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_
  obtain ⟨a', ha', hd⟩ := exists_mul_left_lt₀ hd
  obtain ⟨b', hb', hd⟩ := exists_mul_right_lt₀ hd
  exact (h a' ha' b' hb').trans hd.le

Goal state after: