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

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

Tactic:
mul_assoc,

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
⊢ ↑y⁻¹ * (a * ↑x * ↑x⁻¹) = ↑y⁻¹ * a
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
by_cases ha : a = 0
  · simp only [ha, zero_left]
  by_cases hx : x = 0
  · subst x
    simp only [SemiconjBy, mul_zero, @eq_comm _ _ (y * a), mul_eq_zero] at h
    simp [h.resolve_right ha]
  · have := mul_ne_zero ha hx
    rw [h.eq, mul_ne_zero_iff] at this
    exact @units_inv_right _ _ _ (Units.mk0 x hx) (Units.mk0 y this.1) h

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
a : M₀
h : a * ↑u = 0
⊢ a = 0

Tactic:
by simpa using mul_eq_zero_of_left h ↑u⁻¹

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

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

Tactic:
mul_assoc,

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

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

Tactic:
mul_assoc,

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ y * (x⁻¹ʳ * x) = y
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:
mul_assoc,

Goal state after:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u) a ↔ ↑u⁻¹ * (a * ↑u) = a
Module: Mathlib.Algebra.Ring.Units

Goal state before:
pp: α : Type u
inst✝ : Semiring α
a b : α
u : αˣ
⊢ a /ₚ u + b /ₚ u = (a + b) /ₚ u

Tactic:
simp only [divp, add_mul]

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ b = b * ↑u * ↑u⁻¹

Tactic:
mul_assoc,

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective 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
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
⊢ ↑0 = 0

Tactic:
by rw [← natCast, Nat.cast_zero, zero]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective 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✝ : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
← intCast,

Goal state after:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective 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✝ : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ f ↑↑n = ↑n
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a : α
⊢ Odd (a + 1 + a)

Tactic:
simp [add_comm _ a]

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

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * a * (2 * b) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1

Tactic:
mul_assoc,

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ 2 * (a * (2 * b)) + 2 * b + 2 * a + 1 = 2 * (2 * a * b + b + a) + 1
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective 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✝ : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ ↑(Int.negSucc n) = -↑(n + 1)

Tactic:
← intCast,

Goal state after:
R : Type u_1
S : Type u_2
f : R → S
hf : Surjective 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✝ : AddGroupWithOne R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : R), f (x + y) = f x + f y
neg : ∀ (x : R), f (-x) = -f x
sub : ∀ (x y : R), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ f ↑(Int.negSucc n) = -↑(n + 1)
Module: Mathlib.Algebra.Order.Sub.Defs

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

Tactic:
refine add_tsub_add_le_tsub_right.antisymm (tsub_le_iff_right.2 <| ?_)

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

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

Tactic:
mul_assoc,

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

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

Tactic:
mul_assoc,

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b c d : α
inst✝ : MulRightStrictMono α
⊢ d * (a * b⁻¹ * b) < c * b ↔ d * a < c * b
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:
mul_assoc,

Goal state after:
α : 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
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 < x2
a : { x // 0 ≤ x }
b c : α
h : (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ ↑x * y) a b) ((fun x y ↦ ↑x * y) a c)
ha : 0 = ↑a
⊢ b < c

Tactic:
simp [← ha] at h

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 < x2
a : { x // 0 ≤ x }
b c : α
h : (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ y * ↑x) a b) ((fun x y ↦ y * ↑x) a c)
ha : 0 = ↑a
⊢ b < c

Tactic:
simp [← ha] at h

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * c
⊢ a = b ∧ c = d

Tactic:
refine ⟨le_antisymm hab ?_, le_antisymm hcd ?_⟩
  · grw [hcd] at h
    · exact le_of_mul_le_mul_of_pos_right h <| hc.trans_le hcd
    · exact ha.le
  · grw [hab] at h
    · exact le_of_mul_le_mul_of_pos_left h <| ha.trans_le hab
    · exact hc.le

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a ^ (n + 1)

Tactic:
by rw [pow_succ']; exact one_lt_mul_of_lt_of_le ha (one_le_pow₀ ha.le)

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hba : b < a
hdc : d < c
⊢ a * d + b * c < a * c + b * d

Tactic:
rw [add_comm (a * d), add_comm (a * c)]
  exact mul_add_mul_lt_mul_add_mul hba hdc

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ 4 * a * b = 2 * a * b + 2 * a * b

Tactic:
mul_assoc,

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ 4 * (a * b) = 2 * a * b + 2 * a * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : MulPosMono G₀
n : ℕ
x✝ : Int.negSucc n ≠ 0
⊢ Set.InjOn (fun a ↦ a ^ Int.negSucc n) {a | 0 ≤ a}

Tactic:
simpa using! inv_injective.comp_injOn (pow_left_strictMonoOn₀ n.succ_ne_zero).injOn

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

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

Tactic:
refine fun wf => ⟨fun q => ?_⟩
    obtain ⟨a, rfl⟩ := q.exists_rep
    exact acc_lift₂_iff.2 (wf.apply a)

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ a ^ 2 ⊓ (a ⊓ (a ⊓ 1)) = a ⊓ 1

Tactic:
inf_left_idem,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
ha : 1 ≤ a ^ 2
⊢ a ^ 2 ⊓ (a ⊓ 1) = a ⊓ 1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ n * a * a = b ^ n * a ^ 2

Tactic:
mul_assoc,

Goal state after:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ n * (a * a) = b ^ n * a ^ 2
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:
mul_assoc,

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:
mul_assoc,

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: this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / -↑n| ≤ |a|

Tactic:
by rw [Int.ediv_neg, abs_neg]; apply this

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 ⊔ a) * c * (c⁻¹ * (b ⊓ a)⁻¹) = (b ⊔ a) / (b ⊓ a)

Tactic:
mul_assoc,

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

Goal state before:
pp: case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, a * a.gcdA b * ↑(n / a.gcd b) + b * a.gcdB b * ↑(n / a.gcd b) = a * x + b * y

Tactic:
mul_assoc,

Goal state after:
case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, a * (a.gcdA b * ↑(n / a.gcd b)) + b * a.gcdB b * ↑(n / a.gcd b) = a * x + b * y
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Group α
x✝ : (WithZero α)ˣ
⊢ ↑((fun a ↦ Units.mk0 ↑a ⋯) ((fun a ↦ unzero ⋯) x✝)) = ↑x✝

Tactic:
simp only [coe_unzero, Units.mk0_val]

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

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y z : WithTop α
inst✝ : IsLeftCancelAdd α
hx : x ≠ ⊤
⊢ x + y = x + z ↔ y = z

Tactic:
lift x to α using hx

Goal state after:
α : Type u
inst✝¹ : Add α
y z : WithTop α
inst✝ : IsLeftCancelAdd α
x : α
⊢ ↑x + y = ↑x + z ↔ y = z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
hx : x ≠ ⊤
⊢ x + y ≤ x + z → y ≤ z

Tactic:
lift x to α using hx

Goal state after:
α : Type u
inst✝² : Add α
y z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + y ≤ ↑x + z → y ≤ z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithTop α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
hx : x ≠ ⊤
⊢ y < z → x + y < x + z

Tactic:
lift x to α using hx

Goal state after:
α : Type u
inst✝² : Add α
y z : WithTop α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ y < z → ↑x + y < ↑x + z
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:
refine ⟨?_, fun h => tsub_le_tsub_left h a⟩
  rw [tsub_le_iff_left, ← hc.add_tsub_assoc_of_le h, hc.le_tsub_iff_right (h.trans le_add_self),
    add_comm b]
  apply ha

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

Goal state before:
pp: case h
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ min a b ≤ a

Tactic:
apply min_le_left

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

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y z : WithBot α
inst✝ : IsLeftCancelAdd α
hx : x ≠ ⊥
⊢ x + y = x + z ↔ y = z

Tactic:
lift x to α using hx

Goal state after:
α : Type u
inst✝¹ : Add α
y z : WithBot α
inst✝ : IsLeftCancelAdd α
x : α
⊢ ↑x + y = ↑x + z ↔ y = z
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n * x + ↑n * ↑n

Tactic:
rw [← mul_add, mul_nonneg_iff]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
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

Goal state after:
α : Type u_1
a : α
inst✝ : LE α
x : α
hx : ↑x ≠ ⊥
⊢ a ≤ (↑x).unbot hx ↔ ↑a ≤ ↑x
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

Goal state after:
α : Type u_1
a : α
inst✝ : LE α
x : α
hx : ↑x ≠ ⊥
⊢ (↑x).unbot hx ≤ a ↔ ↑x ≤ ↑a
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

Goal state after:
α : Type u_1
a b : α
inst✝ : LE α
x : α
⊢ b ≤ unbotD a ↑x ↔ ↑b ≤ ↑x
Module: Mathlib.Order.WithBot

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

Tactic:
lift x to α using hx

Goal state after:
α : Type u_1
a : α
inst✝ : LE α
y : WithBot α
x : α
h : ↑x ≤ y
⊢ unbotD a ↑x ≤ unbotD a y
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

Goal state after:
α : Type u_1
a : α
inst✝¹ : LE α
inst✝ : Nonempty α
x : α
⊢ (↑x).unbotA ≤ a ↔ ↑x ≤ ↑a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithBot α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
hx : x ≠ ⊥
⊢ x + y ≤ x + z → y ≤ z

Tactic:
lift x to α using hx

Goal state after:
α : Type u
inst✝² : Add α
y z : WithBot α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + y ≤ ↑x + z → y ≤ z
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

Goal state after:
α : Type u_1
a : α
inst✝ : LT α
x : α
hx : ↑x ≠ ⊥
⊢ a < (↑x).unbot hx ↔ ↑a < ↑x
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

Goal state after:
α : Type u_1
b : α
inst✝ : LT α
x : α
hx : ↑x ≠ ⊥
⊢ (↑x).unbot hx < b ↔ ↑x < ↑b
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

Goal state after:
α : Type u_1
a b : α
inst✝ : LT α
x : α
⊢ b < unbotD a ↑x ↔ ↑b < ↑x
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

Goal state after:
α : Type u_1
a : α
inst✝¹ : LT α
inst✝ : Nonempty α
x : α
⊢ (↑x).unbotA < a ↔ ↑x < ↑a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithBot α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
hx : x ≠ ⊥
⊢ y < z → x + y < x + z

Tactic:
lift x to α using hx

Goal state after:
α : Type u
inst✝² : Add α
y z : WithBot α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ y < z → ↑x + y < ↑x + z
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: case succ
α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
hn : ↑n = ↑n.succ
k : ℕ
k_ih : ↑(n + k) = ↑n
⊢ ↑(n + (k + 1)) = ↑n

Tactic:
| succ k k_ih =>

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

Goal state after:
α : Type u_1
inst✝ : LE α
a b x : α
⊢ b ≤ unzeroD a ↑x ↔ ↑b ≤ ↑x
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
lift x to α using hx

Goal state after:
α : Type u_1
inst✝ : LE α
y : WithZero α
a x : α
h : ↑x ≤ y
⊢ unzeroD a ↑x ≤ unzeroD a y
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

Goal state after:
α : Type u_1
inst✝ : LT α
a b x : α
⊢ b < unzeroD a ↑x ↔ ↑b < ↑x
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a ≤ b
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

Tactic:
obtain ha | ha := le_total a 0
  · rw [floor_of_nonpos ha]
    exact Nat.zero_le _
  · exact le_floor ((floor_le ha).trans h)

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
⊢ ⌈a⌉₊ = 0 ↔ a ≤ 0

Tactic:
rw [← Nat.le_zero, ceil_le, Nat.cast_zero]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
⊢ ⌈1⌉₊ = 1

Tactic:
by rw [← Nat.cast_one, ceil_natCast]

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

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible (a * b)
⊢ ⅟(a * b) * a * b = 1

Tactic:
mul_assoc,

Goal state after:
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible (a * b)
⊢ ⅟(a * b) * (a * b) = 1
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible (a * b)
inst✝ : Invertible b
⊢ b * ⅟(a * b) * a * b = 1 * b

Tactic:
mul_assoc,

Goal state after:
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible (a * b)
inst✝ : Invertible b
⊢ b * ⅟(a * b) * (a * b) = 1 * b
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible (a * b)
inst✝ : Invertible b
⊢ b * ⅟(a * b) * (a * b) = 1 * b

Tactic:
mul_assoc,

Goal state after:
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible (a * b)
inst✝ : Invertible b
⊢ b * (⅟(a * b) * (a * b)) = 1 * b
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟a + ⅟b = ⅟b + ⅟a * b * ⅟b

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝² : Semiring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟a + ⅟b = ⅟b + ⅟a * (b * ⅟b)
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 * ⅟b - ⅟b

Tactic:
mul_assoc,

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) =
    2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))

Tactic:
mul_assoc,

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * ((a ^ (n + 1) + b ^ (n + 1)) * (a + b)) =
    2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a))