mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ ↑n.succ) = f (x ^ ↑n) * f x

Tactic:
zpow_natCast,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ n.succ) = f (x ^ ↑n) * f x
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✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ n.succ) = f (x ^ ↑n) * f x

Tactic:
zpow_natCast,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ n.succ) = f (x ^ n) * f x
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
⊢ IsUnit x ↔ ∃ b, x * b = 1 ∧ b * x = 1

Tactic:
by
  refine ⟨fun ⟨u, hu⟩ => ?_, fun ⟨b, h1b, h2b⟩ => ⟨⟨x, b, h1b, h2b⟩, rfl⟩⟩
  subst x
  exact ⟨u.inv, u.val_inv, u.inv_val⟩

Goal state after:
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✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ (n + 1))⁻¹ = (f (x ^ ↑n.succ))⁻¹

Tactic:
zpow_natCast,

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f (x ^ (n + 1))⁻¹ = (f (x ^ n.succ))⁻¹
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a * d = c / d * b * d ↔ a * d = c * b

Tactic:
mul_right_comm,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a * d = c / d * d * b ↔ a * d = c * b
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ a * b⁻¹ * a⁻¹ = b⁻¹

Tactic:
mul_right_comm,

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ a * a⁻¹ * b⁻¹ = b⁻¹
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ 0 ^ ↑n = 0

Tactic:
zpow_natCast,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ 0 ^ n = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ ↑(n + 1))⁻¹ = (a ^ ↑(n + 1).succ)⁻¹ * a

Tactic:
zpow_natCast,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ (n + 1))⁻¹ = (a ^ ↑(n + 1).succ)⁻¹ * a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ (n + 1))⁻¹ = (a ^ ↑(n + 1).succ)⁻¹ * a

Tactic:
zpow_natCast,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ (n + 1))⁻¹ = (a ^ (n + 1).succ)⁻¹ * a
Module: Mathlib.Algebra.Ring.Defs

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

Tactic:
mul_one_sub,

Goal state after:
α : Type u
inst✝ : NonAssocRing α
a b c : α
⊢ (a - a * b) * c = a * c - a * b * c
Module: Mathlib.Logic.Nontrivial.Basic

Goal state before:
pp: I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
⊢ Nontrivial ((i : I) → f i)

Tactic:
let := Classical.decEq (∀ i : I, f i)
  exact (Function.update_injective (fun i ↦ Classical.choice (inst i)) i').nontrivial

Goal state after:
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⁻¹ʳ

pp: case inr.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⁻¹ʳ

pp: case inr.inr
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]
    simp [Ring.inverse_non_unit, hb, this]

Goal state after:
case inr.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⁻¹ʳ

case inr.inr
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⁻¹ʳ
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x : M₀
a✝ : Nontrivial M₀
⊢ x * x⁻¹ʳ = 1 → IsUnit x

Tactic:
contrapose

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x : M₀
a✝ : Nontrivial M₀
⊢ ¬IsUnit x → ¬x * x⁻¹ʳ = 1
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x : M₀
a✝ : Nontrivial M₀
⊢ x⁻¹ʳ * x = 1 → IsUnit x

Tactic:
contrapose

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x : M₀
a✝ : Nontrivial M₀
⊢ ¬IsUnit x → ¬x⁻¹ʳ * x = 1
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, hbd.right_comm,
    hd.div_mul_cancel]

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * (↑u₂ * ↑u₂⁻¹) * ↑u₁⁻¹ + ↑u₂⁻¹ * ↑u₁⁻¹ * ↑u₁ * b

Tactic:
mul_assoc (↑u₂⁻¹ : α),

Goal state after:
α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * (↑u₂ * ↑u₂⁻¹) * ↑u₁⁻¹ + ↑u₂⁻¹ * (↑u₁⁻¹ * ↑u₁) * b
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NoZeroDivisors R
a b : R
h : Commute a b
⊢ a * a - b * b = 0 ↔ a = b ∨ a = -b

Tactic:
h.mul_self_sub_mul_self_eq,

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

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

Tactic:
mul_right_comm,

Goal state after:
R : Type u
inst✝ : CommRing R
a b : R
⊢ a ^ 2 + b ^ 2 - 2 * b * a = (b - a) ^ 2
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
⊢ IsUnit 2 ↔ ∀ (a : α), Even a

Tactic:
refine ⟨Even.of_isUnit_two, fun h => ?_⟩

Goal state after:
α : Type u_2
inst✝ : Semiring α
h : ∀ (a : α), Even a
⊢ IsUnit 2
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:
rw [tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b c d : α
h₁ : a ≤ b
h₂ : c ≤ d
⊢ a * c ≤ b * d

Tactic:
h₁,

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b c d : α
h₁ : a ≤ b
h₂ : c ≤ d
⊢ b * c ≤ b * d
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
by rw [le_div_iff_mul_le, mul_comm]

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 2

Tactic:
rw [← one_add_one_eq_two]

Goal state after:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 1 + 1
Module: Mathlib.Algebra.Order.Monoid.NatCast

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftStrictMono α
⊢ 1 < 2

Tactic:
rw [← one_add_one_eq_two]

Goal state after:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftStrictMono α
⊢ 1 < 1 + 1
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + c + b * c ≤ b
⊢ 1 + a ≤ (1 + b) * (1 - c)

Tactic:
mul_one_sub,

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + c + b * c ≤ b
⊢ 1 + a ≤ 1 + b - (1 + b) * c
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : c + b * c ≤ a + b
⊢ 1 - a ≤ (1 + b) * (1 - c)

Tactic:
mul_one_sub,

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : c + b * c ≤ a + b
⊢ 1 - a ≤ 1 + b - (1 + b) * c
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u
γ : Sort w
inst✝ : Inhabited γ
⊢ (Embedding.refl α).arrowCongrLeft = Embedding.refl (α → γ)

Tactic:
by
  ext
  simp [coe_refl]

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

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a ≤ b * c⁻¹
hc : 0 < c
⊢ a * c ≤ b

Tactic:
· rwa [le_mul_inv_iff₀ hc] at h

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

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
hb : 0 < b
⊢ a * b⁻¹ ≤ c

Tactic:
mul_inv_le_iff₀ hb

Goal state after:
case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
hb : 0 < b
⊢ a ≤ c * b
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x1 ≤ x2) ↪r fun x1 x2 ↦ x1 ≤ x2
⊢ ∀ {a b : α}, i.toEmbedding b ≤ i.toEmbedding a ↔ b ≤ a

Tactic:
forall_comm

Goal state after:
α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x1 ≤ x2) ↪r fun x1 x2 ↦ x1 ≤ x2
⊢ ∀ (b a : α), i.toEmbedding b ≤ i.toEmbedding a ↔ b ≤ a
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x2 ≤ x1) ↪r fun x1 x2 ↦ x2 ≤ x1
⊢ ∀ {a b : α}, i.toEmbedding a ≤ i.toEmbedding b ↔ a ≤ b

Tactic:
forall_comm

Goal state after:
α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x2 ≤ x1) ↪r fun x1 x2 ↦ x2 ≤ x1
⊢ ∀ (b a : α), i.toEmbedding a ≤ i.toEmbedding b ↔ a ≤ b
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x1 ≤ x2) ≃r fun x1 x2 ↦ x1 ≤ x2
⊢ ∀ {a b : α}, i.toEquiv b ≤ i.toEquiv a ↔ b ≤ a

Tactic:
forall_comm

Goal state after:
α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x1 ≤ x2) ≃r fun x1 x2 ↦ x1 ≤ x2
⊢ ∀ (b a : α), i.toEquiv b ≤ i.toEquiv a ↔ b ≤ a
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x2 ≤ x1) ≃r fun x1 x2 ↦ x2 ≤ x1
⊢ ∀ {a b : α}, i.toEquiv a ≤ i.toEquiv b ↔ a ≤ b

Tactic:
forall_comm

Goal state after:
α : Type u_6
β : Type u_7
inst✝¹ : LE α
inst✝ : LE β
i : (fun x1 x2 ↦ x2 ≤ x1) ≃r fun x1 x2 ↦ x2 ≤ x1
⊢ ∀ (b a : α), i.toEquiv a ≤ i.toEquiv b ↔ a ≤ b
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 β
f : α ↪o β
⊢ ∀ {a b : α}, f.toEmbedding a < f.toEmbedding b ↔ a < b

Tactic:
by simp [lt_iff_le_not_ge, f.map_rel_iff]

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

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
by rw [pow_succ]; exact le_mul_of_one_le_right' ha

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

Goal state before:
pp: 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
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
refine this.mp ⟨fun h ↦ ?_, fun h ↦ by simp only [h.antisymm hb, mabs_of_lt_one ha, mul_one]⟩

Goal state after:
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
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
⊢ 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
hb : 1 ≤ b
⊢ |a|ₘ = b ↔ a = b ∨ a = b⁻¹

Tactic:
by
  refine ⟨eq_or_eq_inv_of_mabs_eq, ?_⟩
  rintro (rfl | rfl) <;> simp only [mabs_inv, mabs_of_one_le hb]

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]

Goal state after:
a : ℤ
⊢ ↑a.natAbs ≤ ↑a.natAbs * ↑a.natAbs
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ ↑n.natAbs = 1 ↔ a ^ n = 1

Tactic:
zpow_natCast,

Goal state after:
G : Type u_1
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ n.natAbs = 1 ↔ a ^ n = 1
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

Goal state after:
case succ.zero
n p : ℕ
dvd : (p + 1).gcd 0 ∣ n
le : (p + 1).pred * pred 0 ≤ n
a : ℕ
eq : n = (p.gcd 0 + 1).gcd 0 * a
⊢ ∃ a b, a * (p + 1) + b * 0 = n
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: 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
⊢ a * ↑p.succ + a_n / ↑q.succ * ↑p.succ * ↑q.succ + b_n * ↑q.succ = ↑n

Tactic:
mul_right_comm,

Goal state after:
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
⊢ a * ↑p.succ + a_n / ↑q.succ * ↑q.succ * ↑p.succ + b_n * ↑q.succ = ↑n
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: p q n : ℕ
dvd : p.gcd q ∣ n
le : p.pred * q.pred ≤ n
⊢ ∃ a b, a * p + b * q = n

Tactic:
obtain _ | p := p
  · have ⟨b, eq⟩ := q.gcd_zero_left ▸ dvd
    exact ⟨0, b, by simpa [mul_comm, eq_comm] using eq⟩
  obtain _ | q := q
  · have ⟨a, eq⟩ := p.gcd_zero_right ▸ dvd
    exact ⟨a, 0, by simpa [mul_comm, eq_comm] using eq⟩
  rw [← Int.gcd_natCast_natCast, Int.gcd_dvd_iff] at dvd
  have ⟨a_n, b_n, eq⟩ := dvd
  let a := a_n % q.succ
  let b := b_n + a_n / q.succ * p.succ
  refine ⟨a.toNat, b.toNat, Nat.cast_injective (R := ℤ) ?_⟩
  have : a * p.succ + b * q.succ = n := by rw [add_mul, ← add_assoc,
    add_right_comm, mul_right_comm, ← add_mul, Int.emod_add_ediv_mul, eq, mul_comm, mul_comm b_n]
  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]
  -- show b ≥ 0 by contradiction
  by_contra hb
  replace hb : b ≤ -1 := by lia
  apply lt_irrefl (n : ℤ)
  have ha := Int.emod_lt a_n (by lia : (q.succ : ℤ) ≠ 0)
  rw [p.pred_succ, q.pred_succ] at le
  calc n = a * p.succ + b * q.succ := this.symm
       _ ≤ q * p.succ + -1 * q.succ := by gcongr <;> lia
       _ = p * q - 1 := by simp_rw [Nat.cast_succ, mul_add, mul_comm]; lia
       _ ≤ n - 1 := by rwa [sub_le_sub_iff_right, ← Nat.cast_mul, Nat.cast_le]
       _ < n := by lia

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

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝ + ↑a✝¹

Tactic:
rw [← WithBot.coe_add, WithBot.coe_le_coe]

Goal state after:
case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ a✝ ≤ a✝ + a✝¹
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝¹ + ↑a✝

Tactic:
rw [← WithBot.coe_add, WithBot.coe_le_coe]

Goal state after:
case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ a✝ ≤ a✝¹ + a✝
Module: Mathlib.Algebra.Order.AddGroupWithTop

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

Tactic:
contrapose

Goal state after:
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a = ⊤ → ¬a + -a = 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✝¹ : 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:
by
    cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]; simpa using lt_of_add_lt_add_right

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
⊢ a - c < b - c ↔ a < b

Tactic:
by rw [hc.lt_tsub_iff_left, add_tsub_cancel_of_le h]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
p : WithBot α → Prop
⊢ (∀ (x : WithBot α), x ≠ ⊥ → p x) ↔ ∀ (x : α), p ↑x

Tactic:
by
  simp [ne_bot_iff_exists]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
p : WithBot α → Prop
⊢ (∃ x, x ≠ ⊥ ∧ p x) ↔ ∃ x, p ↑x

Tactic:
by
  simp [ne_bot_iff_exists]

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✝¹ : 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:
by
    cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]; simpa using lt_of_add_lt_add_right

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedAddCommMonoidWithTop α
⊢ ∀ ⦃a : Multiplicative αᵒᵈ⦄, 0 < a → ∀ ⦃b c : Multiplicative αᵒᵈ⦄, b < c → a * b < a * c

Tactic:
by
    simpa [← ofAdd_add, ← toDual_add]
      using! fun a ha b c hbc ↦ add_right_strictMono_of_ne_top (by simpa using! ha.ne') hbc

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x y : WithBot α
inst✝ : NoBotOrder α
⊢ (∀ (a : α), ↑a ≤ x → ↑a ≤ y) ↔ x ≤ y

Tactic:
obtain _ | a := x

Goal state after:
case none
α : Type u_1
inst✝¹ : Preorder α
y : WithBot α
inst✝ : NoBotOrder α
⊢ (∀ (a : α), ↑a ≤ none → ↑a ≤ y) ↔ none ≤ y

case some
α : Type u_1
inst✝¹ : Preorder α
y : WithBot α
inst✝ : NoBotOrder α
a : α
⊢ (∀ (a_1 : α), ↑a_1 ≤ Option.some a → ↑a_1 ≤ y) ↔ Option.some a ≤ y
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
ι : Sort u_3
r : α → α → Prop
f : ι → α
⊢ DirectedOn r (Set.range f) ↔ Directed r f

Tactic:
Directed,

Goal state after:
α : Type u_1
ι : Sort u_3
r : α → α → Prop
f : ι → α
⊢ DirectedOn r (Set.range f) ↔ ∀ (x y : ι), ∃ z, r (f x) (f z) ∧ r (f y) (f z)
Module: Mathlib.Order.Directed

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
i j : ι
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ z)

Tactic:
rcases hf i j with ⟨k, hi, hj⟩

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
i j k : ι
hi : f i ≤ f k
hj : f j ≤ f k
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ z)
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ↑z < ⊥ → ↑z ≤ ⊥) ↔ ⊥ ≤ ⊥

Tactic:
simp [exists_lt, forall_lt_imp_le_iff_le_of_dense]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑z < ⊥ → ↑z ≤ ↑a✝) ↔ ⊥ ≤ ↑a✝

Tactic:
simp [exists_lt, forall_lt_imp_le_iff_le_of_dense]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝ : α
⊢ (∀ (z : α), ↑z < ↑a✝ → ↑z ≤ ⊥) ↔ ↑a✝ ≤ ⊥

Tactic:
simp [exists_lt, forall_lt_imp_le_iff_le_of_dense]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a✝¹ a✝ : α
⊢ (∀ (z : α), ↑z < ↑a✝¹ → ↑z ≤ ↑a✝) ↔ ↑a✝¹ ≤ ↑a✝

Tactic:
simp [exists_lt, forall_lt_imp_le_iff_le_of_dense]

Goal state after: