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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulLeftReflectLT α
a b : α
⊢ a * b < a ↔ a * b < a * 1

Tactic:
by rw [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝² : LE α
inst✝¹ : MulOneClass α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a ≤ a * b ↔ a * 1 ≤ a * b

Tactic:
by rw [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝² : LE α
inst✝¹ : MulOneClass α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a * b ≤ a ↔ a * b ≤ a * 1

Tactic:
by rw [mul_one]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ < b₂

Tactic:
by
  contrapose!
  exact fun h => mul_lt_mul_of_lt_of_le h.1 h.2

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂

Tactic:
refine ⟨lt_or_lt_of_mul_lt_mul, fun h => ?_⟩

Goal state after:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h : a₁ < a₂ ∨ b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
a b : α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : PosMulReflectLE α
a0 : 0 < a
⊢ a ≤ a * b ↔ a * 1 ≤ a * b

Tactic:
by rw [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
a b : α
inst✝² : Preorder α
inst✝¹ : PosMulStrictMono α
inst✝ : PosMulReflectLT α
a0 : 0 < a
⊢ a < a * b ↔ a * 1 < a * b

Tactic:
by rw [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
a b : α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : PosMulReflectLE α
a0 : 0 < a
⊢ a * b ≤ a ↔ a * b ≤ a * 1

Tactic:
by rw [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
a b : α
inst✝² : Preorder α
inst✝¹ : PosMulStrictMono α
inst✝ : PosMulReflectLT α
a0 : 0 < a
⊢ a * b < a ↔ a * b < a * 1

Tactic:
by rw [mul_one]

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

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

Tactic:
mul_inv_cancel_left₀ hc.ne'

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

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

Tactic:
mul_inv_cancel_left₀ hc.ne'

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

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

Tactic:
mul_inv_cancel_left₀ hc.ne'

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

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

Tactic:
mul_inv_cancel_left₀ hc.ne'

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddLeftMono R
inst✝ : NoZeroDivisors R
r : R
⊢ r ^ 2 ≤ 0 ↔ r = 0

Tactic:
trans r ^ 2 = 0

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddLeftMono R
inst✝ : NoZeroDivisors R
r : R
⊢ r ^ 2 ≤ 0 ↔ r ^ 2 = 0

R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddLeftMono R
inst✝ : NoZeroDivisors R
r : R
⊢ r ^ 2 = 0 ↔ r = 0
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ fst.prod snd = id

Tactic:
ext ⟨x, y⟩ : 2

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x : α
y : β
⊢ (fst.prod snd) (x, y) = id (x, y)
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ✝ : Type u_5
inst✝⁷ : LE α✝
inst✝⁶ : LE β✝
inst✝⁵ : LE γ✝
inst✝⁴ : LE δ✝
α : Type ?u.19
β : Type ?u.21
γ : Type ?u.23
δ : Type ?u.25
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : γ →o δ
⊢ ⇑((fun p ↦ (↑g).comp (p.comp ↑f.symm)) ((fun p ↦ (↑g.symm).comp (p.comp ↑f)) p)) = ⇑p

Tactic:
change (g ∘ g.symm) ∘ p ∘ (f ∘ f.symm) = p
    simp only [← OrderIso.coe_trans, Function.id_comp,
               OrderIso.symm_trans_self, OrderIso.coe_refl, Function.comp_id]

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

Goal state before:
pp: a : ℤ
⊢ ↑a.natAbs ≤ a ^ 2

Tactic:
rw [← Int.natAbs_sq a, sq]
  norm_cast
  apply Nat.le_mul_self

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 : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))

Tactic:
sup_assoc,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ (c ⊔ (a ⊔ c))) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
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) ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))

Tactic:
sup_assoc,

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) ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Group α
inst✝⁵ : LinearOrder α
β : Type u_2
F : Type u_3
inst✝⁴ : Group β
inst✝³ : LinearOrder β
inst✝² : FunLike F α β
inst✝¹ : OrderHomClass F α β
inst✝ : MonoidHomClass F α β
f : F
a : α
⊢ f |a|ₘ = |f a|ₘ

Tactic:
rw [mabs, mabs, (OrderHomClass.mono f).map_max, map_inv]

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Group α
inst✝⁵ : LinearOrder α
β : Type u_2
F : Type u_3
inst✝⁴ : Group β
inst✝³ : LinearOrder β
inst✝² : FunLike F α β
inst✝¹ : OrderHomClass F α β
inst✝ : MonoidHomClass F α β
f : F
a : α
⊢ f |a|ₘ = |f a|ₘ

Tactic:
by
  rw [mabs, mabs, (OrderHomClass.mono f).map_max, map_inv]

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 t s' t' p p'
    rw [xgcdAux_rec h]; refine IH ?_ p; dsimp [P] at *
    rw [Int.emod_def]; generalize (b / a : ℤ) = k
    rw [p, p', Int.mul_sub, sub_add_eq_add_sub, Int.mul_sub, Int.add_mul, mul_comm k t,
      mul_comm k s, ← mul_assoc, ← mul_assoc, add_comm (x * s * k), ← add_sub_assoc, sub_sub]

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : a = 0
⊢ a = 0 ^ n ∧ b = 0 ^ m

Tactic:
have := h.symm; simp_all

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : EquivLike F α β
inst✝² : MulZeroClass α
inst✝¹ : MulZeroClass β
inst✝ : MulEquivClass F α β
f : F
⊢ f 0 = f 0 * f (EquivLike.inv f 0)

Tactic:
← map_mul,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : EquivLike F α β
inst✝² : MulZeroClass α
inst✝¹ : MulZeroClass β
inst✝ : MulEquivClass F α β
f : F
⊢ f 0 = f (0 * EquivLike.inv f 0)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
x y z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) x y) (swap (fun x1 x2 ↦ x1 + x2) x z)

Tactic:
cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝¹ + a✝² ≤ a✝ + a✝²
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
x y z : WithTop α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) x y) (swap (fun x1 x2 ↦ x1 + x2) x z) → (fun x1 x2 ↦ x1 < x2) y z

Tactic:
cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝² a✝¹ a✝ : α
⊢ a✝¹ + a✝² < a✝ + a✝² → a✝¹ < a✝
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a✝ b✝ c✝ : α
inst✝ : AddLeftReflectLE α
a b c : α
h : (fun x ↦ a + x) b = (fun x ↦ a + x) c
⊢ b = c

Tactic:
by
      simpa only [add_tsub_cancel_left] using congr_arg (fun x => x - a) h

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
x y z : WithBot α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) x y) (swap (fun x1 x2 ↦ x1 + x2) x z)

Tactic:
cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝¹ + a✝² ≤ a✝ + a✝²
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
x y z : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) x y) (swap (fun x1 x2 ↦ x1 + x2) x z) → (fun x1 x2 ↦ x1 < x2) y z

Tactic:
cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]

Goal state after:
case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝² a✝¹ a✝ : α
⊢ a✝¹ + a✝² < a✝ + a✝² → a✝¹ < a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
b : α
inst✝ : LT α
x : WithBot α
⊢ x < ↑b ↔ ∀ (a : α), x = ↑a → a < b

Tactic:
by simp [lt_iff_exists]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
x y z : WithBot α
⊢ x ≤ y → y ≤ z → x ≤ z

Tactic:
cases x <;> cases y <;> cases z <;> simp [le_def]; simpa using le_trans

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) < toAdd (ofAdd b)
⊢ toAdd (unzero ha) < b

Tactic:
toAdd_ofAdd

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) < b
⊢ toAdd (unzero ha) < b
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) ≤ toAdd (ofAdd b)
⊢ toAdd (unzero ha) ≤ b

Tactic:
toAdd_ofAdd

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) ≤ b
⊢ toAdd (unzero ha) ≤ b
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
x : α
below : ∃ n, ↑n ≤ x
above : ∃ n, x ≤ ↑n
⊢ { n // ↑n ≤ x ∧ ∀ (m : ℤ), ↑m ≤ x → m ≤ n }

Tactic:
let n := Classical.indefiniteDescription _ above

Goal state after:
F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
x : α
below : ∃ n, ↑n ≤ x
above : ∃ n, x ≤ ↑n
n : { x_1 // x ≤ ↑x_1 } := Classical.indefiniteDescription (fun x_1 ↦ x ≤ ↑x_1) above
⊢ { n // ↑n ≤ x ∧ ∀ (m : ℤ), ↑m ≤ x → m ≤ n }
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ ∨ a✝ ≤ a✝¹

Tactic:
simpa using Std.Total.total ..

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
a : α
x✝ : 0 < ↑a
b c : α
hbc : ↑b < ↑c
⊢ ↑a * ↑b < ↑a * ↑c

Tactic:
norm_cast at *; exact mul_lt_mul_right hbc _

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ ∨ a✝ ≤ a✝¹

Tactic:
simpa using Std.Total.total ..

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ a * ⅟c = b ↔ a = b * c

Tactic:
rw [← mul_left_inj_of_invertible (c := c), invOf_mul_cancel_right]

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.univ.pi d
b : (i : ι) → α i
⊢ b ∈ Set.univ.pi d →
    ∃ z ∈ Set.univ.pi d, (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧ (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) b z

Tactic:
hb

Goal state after:
ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.univ.pi d
b : (i : ι) → α i
hb : b ∈ Set.univ.pi d
⊢ ∃ z ∈ Set.univ.pi d, (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧ (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) b z
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : MulOneClass S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ f ⅟r * f r = 1

Tactic:
← map_mul,

Goal state after:
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : MulOneClass S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ f (⅟r * r) = 1
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : MulOneClass S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ f r * f ⅟r = 1

Tactic:
← map_mul,

Goal state after:
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : MulOneClass S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ f (r * ⅟r) = 1
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: case neg
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ f a⁻¹ * f a = 1

Tactic:
← map_mul,

Goal state after:
case neg
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ f (a⁻¹ * a) = 1
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
⊢ b ∈ s → a ≤ b → f₂ a ≤ f₂ b

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a ≤ b → f₂ a ≤ f₂ b
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
⊢ b ∈ s → a < b → f₂ a < f₂ b

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a < b → f₂ a < f₂ b
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
b : α
⊢ b ∈ s → a < b → f a < f b

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
b : α
hb : b ∈ s
⊢ a < b → f a < f b
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
b : α
⊢ b ∈ s → b < a → f b < f a

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
b : α
hb : b ∈ s
⊢ b < a → f b < f a
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
b : α
⊢ b ∈ s → a < b → f b < f a

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
b : α
hb : b ∈ s
⊢ a < b → f b < f a
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
b : α
⊢ b ∈ s → b < a → f a < f b

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
b : α
hb : b ∈ s
⊢ b < a → f a < f b
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Monotone f
⊢ IsCofinalFor (f '' s) (f '' t)

Tactic:
simp only [IsCofinalFor, forall_mem_image, exists_mem_image]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Monotone f
⊢ ∀ ⦃x : α⦄, x ∈ s → ∃ x_1 ∈ t, f x ≤ f x_1
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case inr.inl
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a b : β
IH : ∀ (y : β), y < b → f y = g y
hb : g b = f b
⊢ f b = g b

Tactic:
hb

Goal state after:
case inr.inl
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a b : β
IH : ∀ (y : β), y < b → f y = g y
hb : g b = f b
⊢ f b = f b
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case inr.inr
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : g c = g a
this : c < a
⊢ f a = g a

Tactic:
cases (hg.injective hc).not_lt this

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
contra : ¬c ≤ d
⊢ False

Tactic:
Icc_eq_empty_iff.mpr contra,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = ∅
contra : ¬c ≤ d
⊢ False
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
lt_one_div (@zero_lt_one α _ _ _ _ _) h1,

Goal state after:
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
h1 : 0 < a
h2 : a < 1
⊢ a < 1 / 1
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
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc

Tactic:
simp only [← mul_assoc, (Nat.cast_commute (α := α) da nb).invOf_left.right_comm, 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
⊢ ↑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
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc

Tactic:
simp only [← mul_assoc, (Nat.cast_commute (α := α) da nb).invOf_left.right_comm, 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
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc