mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x y : β
⊢ g • (x * y⁻¹) = g • x / g • y

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x y : β
⊢ g • (x * y⁻¹) = g • x * (g • y)⁻¹
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ a * (b - 1) = a * b - a

Tactic:
mul_sub,

Goal state after:
α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ a * b - a * 1 = a * b - a
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ a * (1 - b) = a - a * b

Tactic:
mul_sub,

Goal state after:
α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ a * 1 - a * b = a - a * b
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
c : α
⊢ a * c ∣ b * c

Tactic:
by
  gcongr

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

Goal state before:
pp: α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c

Tactic:
refine ⟨b - x, ?_, by simp, by rw [this]⟩

Goal state after:
α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ (b - x) * (b - x) - b * (b - x) + c = 0
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : ∀ (x : R), r * x = 0 → x = 0
r₁ r₂ : R
eq : (fun x ↦ r * x) r₁ = (fun x ↦ r * x) r₂
⊢ r * (r₁ - r₂) = 0

Tactic:
mul_sub,

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : ∀ (x : R), r * x = 0 → x = 0
r₁ r₂ : R
eq : (fun x ↦ r * x) r₁ = (fun x ↦ r * x) r₂
⊢ r * r₁ - r * r₂ = 0
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : f 1 = 1
n : ℕ
⊢ f n + 1 = ↑(n + 1)

Tactic:
eq_natCast' f h1 n,

Goal state after:
A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : f 1 = 1
n : ℕ
⊢ ↑n + 1 = ↑(n + 1)
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x / x') (y / y')

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x'⁻¹) (y / y')
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x = y * z⁻¹ʳ
⊢ y * z⁻¹ʳ * z = y

Tactic:
inverse_mul_cancel_right _ _ h

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x = y * z⁻¹ʳ
⊢ y = y
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

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

Tactic:
by
  rw [div_div_eq_mul_div, div_mul_cancel₀ _ hc]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a = c / d * b ↔ a = b / d * c

Tactic:
rw [mul_comm _ c, div_mul_eq_mul_div, mul_div_assoc]

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = a * (a - b) + b * (a - b)

Tactic:
mul_sub,

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = a * a - a * b + b * (a - b)
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = a * a - a * b + b * (a - b)

Tactic:
mul_sub,

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocRing R
a b : R
h : Commute a b
⊢ a * a - b * b = a * a - a * b + (b * a - b * b)
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ b ≤ a / b * b ↔ b ≤ a

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ b ≤ a * b⁻¹ * b ↔ b ≤ a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a / b * b ≤ b ↔ a ≤ b

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a * b⁻¹ * b ≤ b ↔ a ≤ b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a * b ≤ c / b * b ↔ a * b ≤ c

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a * b ≤ c * b⁻¹ * b ↔ a * b ≤ c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a / c * c ≤ b * c ↔ a ≤ b * c

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a * c⁻¹ * c ≤ b * c ↔ a ≤ b * c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
b c a : α
⊢ a / b ≤ a / c ↔ c ≤ b

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
b c a : α
⊢ a * b⁻¹ ≤ a / c ↔ c ≤ b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
b c a : α
⊢ a * b⁻¹ ≤ a / c ↔ c ≤ b

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
b c a : α
⊢ a * b⁻¹ ≤ a * c⁻¹ ↔ c ≤ b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a / d ≤ b / c

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a * d⁻¹ ≤ b / c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a * d⁻¹ ≤ b / c

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a * d⁻¹ ≤ b * c⁻¹
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ b < a * b⁻¹ * b ↔ b < a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ a * b⁻¹ * b < b ↔ a < b
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 / b * b ↔ a * b < c

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a * b < c * b⁻¹ * b ↔ a * b < c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a * c⁻¹ * c < b * c ↔ a < b * c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
b c a : α
⊢ a * b⁻¹ < a / c ↔ c < b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
b c a : α
⊢ a * b⁻¹ < a * c⁻¹ ↔ c < b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a⁻¹ < b * c⁻¹ ↔ c < a * b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a / d < b / c

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a * d⁻¹ < b / c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a * d⁻¹ < b / c

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a * d⁻¹ < b * c⁻¹
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
h : a * b ≤ c * d
⊢ min a b ≤ max c d

Tactic:
by
  simp_rw [min_le_iff, le_max_iff]; contrapose! h; exact mul_lt_mul_of_le_of_lt h.1.1.le h.2.2

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

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a / b ≤ a⁻¹ * b ↔ a ≤ b

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a * b⁻¹ ≤ a⁻¹ * b ↔ a ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
⊢ a * c = b * d ↔ a = b ∧ c = d

Tactic:
by
  refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  simp only [eq_iff_le_not_lt, hab, hcd, true_and]
  refine ⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩
  · exact (mul_lt_mul_of_pos_right hab c0).trans_le (mul_le_mul_of_nonneg_left hcd b0.le)
  · exact (mul_le_mul_of_nonneg_right hab c0.le).trans_lt (mul_lt_mul_of_pos_left hcd b0)

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b / c ↔ a * c ≤ b

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b * c⁻¹ ↔ a * c ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b / c ≤ a ↔ b ≤ a * c

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b * c⁻¹ ≤ a ↔ b ≤ a * c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b / c ↔ a * c < b

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b * c⁻¹ ↔ a * c < b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b / c < a ↔ b < a * c

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b * c⁻¹ < a ↔ b < a * c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a / b ≤ a / c

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a * b⁻¹ ≤ a / c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ a / b ≤ c / d

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ a * b⁻¹ ≤ c / d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ a / b < c / d

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ a * b⁻¹ < c / d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a ≤ c
hdb : d < b
hc : 0 < c
hd : 0 < d
⊢ a / b < c / d

Tactic:
div_eq_mul_inv,

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a ≤ c
hdb : d < b
hc : 0 < c
hd : 0 < d
⊢ a * b⁻¹ < c / d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: 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 : ℤ
⊢ a ^ n = 1 ↔ n = 0

Tactic:
by
  obtain rfl | ha₀ := ha₀.eq_or_lt
  · exact zero_zpow_eq_one₀
  simpa using zpow_right_inj₀ ha₀ ha₁ (n := 0)

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
obtain ha | ha := le_or_gt 1 a <;> obtain hb | hb := le_or_gt 1 b

Goal state after:
case inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

case inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

case inr.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

case inr.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : b < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
⊢ |a / b|ₘ ≤ |a|ₘ * |b|ₘ

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
⊢ |a * b⁻¹|ₘ ≤ |a|ₘ * |b|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

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

Tactic:
div_eq_mul_inv,

Goal state after:
case right
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (|a|ₘ * |b|ₘ⁻¹)⁻¹ ≤ |a / b|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

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

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) ^ 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
⊢ a.sign * a = |a|

Tactic:
by
  rw [abs_eq_natAbs, sign_mul_self_eq_natAbs]

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) ^ 2 = (a ⊓ b) * (a ⊔ b) / ((a ⊔ b) / (a ⊓ b))

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) ^ 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))⁻¹
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

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

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) ^ 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)⁻¹
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) * c / ((b ⊓ a) * c) = (b ⊔ a) / (b ⊓ a)

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) * c * ((b ⊓ a) * c)⁻¹ = (b ⊔ a) / (b ⊓ a)
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.zero
n p : ℕ
dvd : (p + 1).gcd 0 ∣ n
le : (p + 1).pred * pred 0 ≤ n
⊢ ∃ a b, a * (p + 1) + b * 0 = n

Tactic:
have ⟨a, eq⟩ := p.gcd_zero_right ▸ dvd
    exact ⟨a, 0, by simpa [mul_comm, eq_comm] using eq⟩

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

Goal state before:
pp: M : Type u_4
a : M
⊢ exp a ≠ 0

Tactic:
simp [exp]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hc : AddLECancellable c
h : c ≤ b
a : α
⊢ a + b - c = a + (b - c)

Tactic:
conv_lhs => rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hc : AddLECancellable c
h : c ≤ b
a : α
⊢ a + b - c = a + (b - c)

Tactic:
by
  conv_lhs => rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < b + c

Tactic:
refine ⟨hb.lt_add_of_tsub_lt_left, ?_⟩
  intro h; refine (tsub_le_iff_left.mpr h.le).lt_of_ne ?_
  rintro rfl; exact h.ne' (add_tsub_cancel_of_le hba)

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

Goal state before:
pp: case refine_2
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
⊢ Nat.find hₙ - n ≤ Nat.find hₘ

Tactic:
refine (le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_

Goal state after:
case refine_2
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
m : ℕ
hm : m < Nat.find hₙ - n
hpm : p (m + n)
⊢ Nat.find hₙ - n ≤ m
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝ : Preorder G
a b : G
⊢ exp a ≤ exp b ↔ a ≤ b

Tactic:
simp [exp]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝ : Preorder G
a b : G
⊢ exp a < exp b ↔ a < b

Tactic:
simp [exp]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝ : Preorder G
a : G
⊢ 0 < exp a

Tactic:
simp [exp]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Invertible 2
⊢ 2 * (1 - ⅟2) = 2 * ⅟2

Tactic:
mul_sub,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Invertible 2
⊢ 2 * 1 - 2 * ⅟2 = 2 * ⅟2
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟a - ⅟b = ⅟a * (b - a) * ⅟b

Tactic:
mul_sub,

Goal state after:
R : Type u_1
inst✝² : Ring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟a - ⅟b = (⅟a * b - ⅟a * a) * ⅟b
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
⊢ (a + b) / c = a / c + b / c

Tactic:
div_eq_mul_inv,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
⊢ (a + b) * c⁻¹ = a * c⁻¹ + b * c⁻¹
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
n : ℕ
hn : Even n
a : α
⊢ |a| ^ n = a ^ n

Tactic:
by
  rw [← abs_pow, abs_eq_self]; exact hn.pow_nonneg _

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
a b c : α
inst✝ : Preorder α
h₁ : SymmGen (fun x1 x2 ↦ x1 ≤ x2) a b
h₂ : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) b c
⊢ SymmGen (fun x1 x2 ↦ x1 ≤ x2) a c

Tactic:
obtain (h | h) := h₁

Goal state after:
case inl
α : Type u_1
a b c : α
inst✝ : Preorder α
h₂ : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) b c
h : a ≤ b
⊢ SymmGen (fun x1 x2 ↦ x1 ≤ x2) a c

case inr
α : Type u_1
a b c : α
inst✝ : Preorder α
h₂ : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) b c
h : b ≤ a
⊢ SymmGen (fun x1 x2 ↦ x1 ≤ x2) a c
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddAbove s → BddBelow t → BddAbove (image2 f s t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩
  exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb⟩

Goal state after: