mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
a c : α
b d : αˣ
⊢ a * ↑b⁻¹ = c * ↑d⁻¹ ↔ a * ↑d = c * ↑b

Tactic:
by
  rw [mul_comm c, Units.mul_inv_eq_iff_eq_mul, mul_assoc, Units.eq_inv_mul_iff_mul_eq, mul_comm]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit a
⊢ a * b = a * 1 ↔ b = 1

Tactic:
by rw [h.mul_right_inj]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ a / (a / b) = b

Tactic:
rw [div_div_eq_mul_div, h.mul_div_cancel_left]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
α : Type u_6
inst✝ : Monoid α
⊢ (↑1, op ↑1⁻¹) = 1

Tactic:
simp only [inv_one, Units.val_one, op_one, Prod.mk_eq_one, and_self_iff]

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

Goal state before:
pp: M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
⊢ 1 x = 0 ↔ x = 0

Tactic:
rcases eq_or_ne x 0 with rfl | hx <;> simp_all [one_apply_of_ne_zero]

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

Goal state before:
pp: M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
⊢ 1 x = 1 ↔ x ≠ 0

Tactic:
rcases eq_or_ne x 0 with rfl | hx <;> simp_all [one_apply_of_ne_zero]

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

Goal state before:
pp: α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ -a * b + a * b = 0

Tactic:
← right_distrib,

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

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

Tactic:
simpa only [sub_eq_add_neg, neg_mul_eq_mul_neg] using mul_add a b (-c)

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: ⊢ ¬Even 1

Tactic:
by simp [even_iff]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
n : ℕ
⊢ r⁻¹ʳ * r⁻¹ʳ ^ n = (r ^ n * r)⁻¹ʳ

Tactic:
Ring.mul_inverse_rev' ((Commute.refl r).pow_left n),

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
n : ℕ
⊢ r⁻¹ʳ * r⁻¹ʳ ^ n = r⁻¹ʳ * (r ^ n)⁻¹ʳ
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case inl
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : IsUnit a
hb : ¬IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
have : ¬ IsUnit (a * b) := by simpa [ha.mul_left_iff]

Goal state after:
case inl
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : IsUnit a
hb : ¬IsUnit b
this : ¬IsUnit (a * b)
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u) a ↔ ↑u * (a * ↑u⁻¹) = a

Tactic:
by
  rw [u.commute_iff_mul_inv_cancel, mul_assoc]

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

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

Tactic:
simp [sq, add_mul, mul_add, two_mul, h.eq, add_assoc]

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

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

Tactic:
by
  rw [sq, sq, h.mul_self_sub_mul_self_eq]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective f✝
inst✝¹¹ : Add S
inst✝¹⁰ : Mul S
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Neg S
inst✝⁶ : Sub S
inst✝⁵ : SMul ℕ S
inst✝⁴ : SMul ℤ S
inst✝³ : Pow S ℕ
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ f ↑(n + 1) = f (↑n + 1)

Tactic:
by rw [natCast, Nat.cast_succ, add, one, natCast]

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ ↑m = ↑n

Tactic:
← nsmul_one,

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ m • 1 = ↑n
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ m • 1 = ↑n

Tactic:
← nsmul_one,

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ m • 1 = n • 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Even b
⊢ Odd (a - b)

Tactic:
rw [sub_eq_add_neg]

Goal state after:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Even b
⊢ Odd (a + -b)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a b : α
ha : Even a
hb : Odd b
⊢ Odd (a - b)

Tactic:
rw [sub_eq_add_neg]

Goal state after:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Even a
hb : Odd b
⊢ Odd (a + -b)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Odd b
⊢ Even (a - b)

Tactic:
rw [sub_eq_add_neg]

Goal state after:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Odd b
⊢ Even (a + -b)
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:
tsub_le_iff_left,

Goal state after:
α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a ≤ b + c ↔ a - c ≤ b
Module: Mathlib.Algebra.Order.Sub.Defs

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

Tactic:
tsub_le_iff_left,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b : α
inst✝ : AddLeftMono α
h : a ≤ b
c : α
⊢ c ≤ b + (c - a)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b - c ≤ a + (b - c)

Tactic:
tsub_le_iff_left,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ c + (a + (b - c))
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a - c ≤ a - b + (b - c)

Tactic:
tsub_le_iff_left,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a ≤ c + (a - b + (b - c))
Module: Mathlib.Algebra.Order.Sub.Defs

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

Tactic:
tsub_le_iff_left,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ c - a ≤ c - b + (b - a)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ c - a ≤ c - b + (b - a)

Tactic:
tsub_le_iff_left,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ c ≤ a + (c - b + (b - a))
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + b - (d + c) ≤ a - c + (b - d)

Tactic:
tsub_le_iff_left,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + b ≤ d + c + (a - c + (b - d))
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b - (a + c) ≤ b - c

Tactic:
tsub_le_iff_left,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a + c + (b - c)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + c - (b + c) ≤ a - b

Tactic:
tsub_le_iff_left,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + c ≤ b + c + (a - b)
Module: Mathlib.Algebra.Order.Sub.Defs

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

Tactic:
tsub_le_iff_left,

Goal state after:
α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a ≤ b + 0 ↔ a ≤ b
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - a - c ≤ b - (a + c)

Tactic:
tsub_le_iff_left,

Goal state after:
case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - a ≤ c + (b - (a + c))
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - a ≤ c + (b - (a + c))

Tactic:
tsub_le_iff_left,

Goal state after:
case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b ≤ a + (c + (b - (a + c)))
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - (a + c) ≤ b - a - c

Tactic:
tsub_le_iff_left,

Goal state after:
case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b ≤ a + c + (b - a - c)
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a b c d : α
⊢ a / d < b / c → a < b ∨ c < d

Tactic:
by
  contrapose!; exact fun h ↦ div_le_div'' h.1 h.2

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

Goal state before:
pp: α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : MulLeftMono α
a b : α
h : MulLECancellable (a * b)
c d : α
hcd : b * c ≤ b * d
⊢ a * b * c ≤ a * b * d

Tactic:
rw [mul_assoc, mul_assoc]; exact mul_le_mul_right hcd _

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
add_le_add_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
toIsOrderedAddMonoid : IsOrderedAddMonoid α := { add_le_add_left := add_le_add_left }
le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
a b c : α
h : a + b ≤ a + c
⊢ b ≤ c

Tactic:
exact le_of_add_le_add_left a b c h

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a b : M₀
inst✝ : MulPosMono M₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ 2 = b ^ 2 ↔ a = b

Tactic:
by
  simp [ha, hb]

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
⊢ a < c⁻¹ * b ↔ c * a < b

Tactic:
rw [← mul_lt_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

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⁻¹ * b < a ↔ b < c * a

Tactic:
rw [← mul_lt_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a✝ b✝ : β
h : s a✝ b✝
⊢ r (surjInv hf a✝) (surjInv hf b✝)

Tactic:
simpa only [o, surjInv_eq hf] using h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
⊢ r ↪r s

Tactic:
haveI := @Std.Asymm.irrefl β s _

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
⊢ r ↪r s
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
a b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (f a) (f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (g a) (g b) ↔ r₂ a b
⊢ Sum.Lex s₁ s₂ (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) a)
      (({ toEquiv := f, map_rel_iff' := hf }.sumCongr { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ a b

Tactic:
cases a <;> cases b <;> simp [hf, hg]

Goal state after:
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✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a b : α
⊢ cmp ({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a)
      ({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b) =
    cmp a b

Tactic:
convert! (h a (f b)).symm

Goal state after:
case e'_3
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a b : α
⊢ b = g (f b)
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: case mpr
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝³ : Preorder X
inst✝² : Preorder Y
inst✝¹ : EquivLike F X Y
inst✝ : OrderIsoClass F X Y
f : F
⊢ DenselyOrdered Y → DenselyOrdered X

Tactic:
intro H
    refine ⟨fun a b h ↦ ?_⟩
    obtain ⟨c, hc⟩ := exists_between ((map_lt_map_iff f).mpr h)
    exact ⟨EquivLike.inv f c, by simpa using hc⟩

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

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
h✝ : 1 ≤ a
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

Tactic:
simp [*, le_of_lt]

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

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
h✝ : a < 1
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

Tactic:
simp [*, le_of_lt]

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

Goal state before:
pp: case mp
n : ℕ
x : ℤ
h : ↑n = x * x
⊢ IsSquare n

Tactic:
exact ⟨x.natAbs, (natAbs_mul_natAbs_eq h.symm).symm⟩

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

Goal state after:
α : 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
this : b ^ n = a ^ m
⊢ a = 0 ^ n ∧ b = 0 ^ m
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
la : IsLeftRegular 0
x y : R
xy : x ≠ y
⊢ False

Tactic:
refine xy (la ?_)

Goal state after:
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
la : IsLeftRegular 0
x y : R
xy : x ≠ y
⊢ (fun x ↦ 0 * x) x = (fun x ↦ 0 * x) y
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: β : Type u_2
inst✝ : MulOneClass β
x : WithZero β
⊢ ↑(map' (MonoidHom.id β)) x = (MonoidHom.id (WithZero β)) x

Tactic:
induction x <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
f : α →* β
g : β →* γ
x : WithZero α
⊢ (map' g) ((map' f) x) = (map' (g.comp f)) x

Tactic:
induction x <;> rfl

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : One α
a : α
inst✝¹ : LE α
inst✝ : IsBotOneClass α
x : WithTop α
⊢ 1 ≤ x

Tactic:
by cases x <;> simp

Goal state after:
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 : α
⊢ a - b ≤ 0 ↔ a ≤ b

Tactic:
tsub_le_iff_left,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a ≤ b + 0 ↔ a ≤ b
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 : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a - b ≤ a - c → c ≤ b

Tactic:
tsub_le_iff_left,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a ≤ b + (a - c) → c ≤ b
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
x : WithBot α
⊢ WithBot.map (⇑e.symm) (WithBot.map (⇑e) x) = x

Tactic:
by cases x <;> simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
x : WithBot β
⊢ WithBot.map (⇑e) (WithBot.map (⇑e.symm) x) = x

Tactic:
by cases x <;> simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LE α
x : WithBot α
hx : x ≠ ⊥
⊢ a ≤ x.unbot hx ↔ ↑a ≤ x

Tactic:
lift x to α using hx; simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LE α
x : WithBot α
hx : x ≠ ⊥
⊢ x.unbot hx ≤ a ↔ x ≤ ↑a

Tactic:
lift x to α using hx; simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : LE α
x : WithBot α
hx : x ≠ ⊥
⊢ b ≤ unbotD a x ↔ ↑b ≤ x

Tactic:
lift x to α using hx; simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : LE α
x : WithBot α
inst✝ : Nonempty α
hx : x ≠ ⊥
⊢ x.unbotA ≤ a ↔ x ≤ ↑a

Tactic:
lift x to α using hx; simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithBot α
⊢ ⊥ < x ↔ x ≠ ⊥

Tactic:
by cases x <;> simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LT α
x : WithBot α
hx : x ≠ ⊥
⊢ a < x.unbot hx ↔ ↑a < x

Tactic:
lift x to α using hx; simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
b : α
inst✝ : LT α
x : WithBot α
hx : x ≠ ⊥
⊢ x.unbot hx < b ↔ x < ↑b

Tactic:
lift x to α using hx; simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : LT α
x : WithBot α
hx : x ≠ ⊥
⊢ b < unbotD a x ↔ ↑b < x

Tactic:
lift x to α using hx; simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : LT α
x : WithBot α
inst✝ : Nonempty α
hx : x ≠ ⊥
⊢ x.unbotA < a ↔ x < ↑a

Tactic:
lift x to α using hx; simp

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : a⁻¹ ≤ c⁻¹
ha : a ≠ 0
⊢ b < d

Tactic:
simpa [inv_mul_cancel_left₀ ha, inv_mul_cancel_left₀ hc.ne']
    using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos hh h zero_le (inv_pos.2 hc)

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : WithBot α
b : α
⊢ x ≤ ↑(unbotD b x)

Tactic:
by cases x <;> simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : OrderBot α
⊢ x < ↑⊥ ↔ x = ⊥

Tactic:
by cases x <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
hf : Monotone ⇑f
⊢ Monotone ⇑(map' f)

Tactic:
simpa [Monotone, WithZero.forall]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
a b : ℤ
⊢ ↑a ≤ b ↔ a ≤ id b

Tactic:
by
    rw [Int.cast_id, id_def]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
a b : ℤ
⊢ id a ≤ b ↔ a ≤ ↑b

Tactic:
by
    rw [Int.cast_id, id_def]

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ x.log < y.log ↔ x < y

Tactic:
log_lt_iff_lt_exp hx,

Goal state after:
G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ x < exp y.log ↔ x < y
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithZero α
a b : α
hx : x ≠ 0
⊢ b ≤ unzeroD a x ↔ ↑b ≤ x

Tactic:
lift x to α using hx; simp

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

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithZero α
a b : α
hx : x ≠ 0
⊢ b < unzeroD a x ↔ ↑b < x

Tactic:
lift x to α using hx; simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : WithZero α
b : α
⊢ x ≤ ↑(unzeroD b x)

Tactic:
by cases x <;> simp

Goal state after: