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

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : LE α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddRightMono α
⊢ 0 + 1 ≤ 1 + 1

Tactic:
gcongr

Goal state after:
case bc
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : LE α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddRightMono α
⊢ 0 ≤ 1
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝² : LE R
inst✝¹ : NonAssocSemiring R
inst✝ : AddLeftMono R
a : R
a1 : 1 ≤ a
⊢ a + 1 ≤ a + a

Tactic:
gcongr

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : Preorder R
a b : R
inst✝² : ZeroLEOneClass R
inst✝¹ : MulPosMono R
inst✝ : AddLeftMono R
a2 : 2 ≤ a
b0 : 0 ≤ b
⊢ a + (2 + b) ≤ a + (a + a * b)

Tactic:
gcongr

Goal state after:
case h₂
R : Type u
inst✝⁴ : Semiring R
inst✝³ : Preorder R
a b : R
inst✝² : ZeroLEOneClass R
inst✝¹ : MulPosMono R
inst✝ : AddLeftMono R
a2 : 2 ≤ a
b0 : 0 ≤ b
⊢ b ≤ a * b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ d * b ≤ d * a

Tactic:
gcongr

Goal state after:
case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ 0 ≤ d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a : M₀
inst✝ : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
this : ZeroLEOneClass M₀
⊢ a ^ n * a ≤ a ^ n * 1

Tactic:
gcongr

Goal state after:
case ha
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a : M₀
inst✝ : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
this : ZeroLEOneClass M₀
⊢ 0 ≤ a ^ n
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ b * d + (a * c + a * d) = b * d

Tactic:
← mul_add,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ b * d + a * (c + d) = b * d
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ b * d ≤ a * d

Tactic:
gcongr

Goal state after:
case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ 0 ≤ d
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * d = b * c + b * d + a * d

Tactic:
← mul_add,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * d = b * (c + d) + a * d
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Preorder R
a b c d : R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosMono R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
hca : c ≤ a
hbd : b ≤ d
hc : 0 ≤ c
hb : b ≤ 0
⊢ c * b ≤ c * d

Tactic:
gcongr

Goal state after:
case ha
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Preorder R
a b c d : R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosMono R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
hca : c ≤ a
hbd : b ≤ d
hc : 0 ≤ c
hb : b ≤ 0
⊢ 0 ≤ c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a : M₀
inst✝ : PosMulStrictMono M₀
h₀ : 0 < a
h₁ : a < 1
n : ℕ
⊢ a ^ (n + 1) < a ^ n

Tactic:
by
    have : ZeroLEOneClass M₀ := ⟨(h₀.trans h₁).le⟩
    simpa only [pow_succ, mul_one] using mul_lt_mul_of_pos_left h₁ (pow_pos h₀ n)

Goal state after:
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 + b + b * c ≤ c
⊢ 1 + (a + b + b * c) ≤ 1 + c

Tactic:
gcongr

Goal state after:
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 + c + b * c) ≤ 1 + b

Tactic:
gcongr

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 : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ b * d + (a * c + a * d) = b * d

Tactic:
← mul_add,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ b * d + a * (c + d) = b * d
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ a * d = b * c + b * d + a * d

Tactic:
← mul_add,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ a * d = b * (c + d) + a * d
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 : b + b * c ≤ a + c
⊢ 1 + (b + b * c) ≤ 1 + (a + c)

Tactic:
gcongr

Goal state after:
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 + (c + b * c) ≤ 1 + (a + b)

Tactic:
gcongr

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 : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hab : a ≤ b
d : R
hd : 0 ≤ d
hcd : c ≤ c + d
⊢ a * c + b * c + a * d ≤ a * c + b * c + b * d

Tactic:
gcongr

Goal state after:
case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hab : a ≤ b
d : R
hd : 0 ≤ d
hcd : c ≤ c + d
⊢ 0 ≤ d
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

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

Tactic:
gcongr

Goal state after:
case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hab : a < b
d : R
hd : 0 < d
hcd : c < c + d
⊢ 0 < d
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : ZeroLEOneClass R
inst✝² : NeZero 1
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftMono R
a2 : 2 ≤ a
ab : a ≤ b
this : 0 < b
⊢ a + b ≤ b + b

Tactic:
gcongr

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : ZeroLEOneClass R
inst✝² : NeZero 1
inst✝¹ : AddLeftMono R
inst✝ : PosMulStrictMono R
b2 : 2 ≤ b
ba : b ≤ a
this : 0 < a
⊢ a + b ≤ a + a

Tactic:
gcongr

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 : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n

Tactic:
exact mul_lt_of_lt_one_right (zpow_pos ha₀ _) ha₁

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

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

Tactic:
gcongr

Goal state after:
case ha
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ 0 ≤ c⁻¹
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
a d : R
inst✝¹ : PosMulMono R
inst✝ : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ b * a ≤ max d b * max c a

Tactic:
gcongr

Goal state after:
case c0
R : Type u
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
a d : R
inst✝¹ : PosMulMono R
inst✝ : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ 0 ≤ a

case b0
R : Type u
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
a d : R
inst✝¹ : PosMulMono R
inst✝ : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ 0 ≤ max d b

case h₁
R : Type u
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
a d : R
inst✝¹ : PosMulMono R
inst✝ : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ b ≤ max d b

case h₂
R : Type u
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
a d : R
inst✝¹ : PosMulMono R
inst✝ : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ a ≤ max c a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

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

Tactic:
exact mul_lt_mul_of_pos_right h (Right.inv_pos.2 hc)

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₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a * b⁻¹ ≤ a * c⁻¹

Tactic:
gcongr

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

case hb
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ 0 < c
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
⊢ 2 * a * b + 2 * a * b ≤ a ^ 2 + b ^ 2 + 2 * a * b

Tactic:
gcongr

Goal state after:
case h₁
R : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ 2 * a * b ≤ a ^ 2 + b ^ 2
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

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

Tactic:
gcongr

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

case b0
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ 0 ≤ c

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

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

Tactic:
gcongr

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

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

Tactic:
lt_div_iff₀ hc,

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

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ 0 < x - a ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x

Tactic:
sub_pos,

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ a < x ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ a < x ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x

Tactic:
sub_pos,

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ a < x ∧ b < x ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ 0 < x - a ∧ x - b < 0 ∨ x - a < 0 ∧ 0 < x - b ↔ a < x ∧ x < b

Tactic:
sub_pos,

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ a < x ∧ x - b < 0 ∨ x - a < 0 ∧ 0 < x - b ↔ a < x ∧ x < b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ a < x ∧ x - b < 0 ∨ x - a < 0 ∧ 0 < x - b ↔ a < x ∧ x < b

Tactic:
sub_pos,

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ a < x ∧ x - b < 0 ∨ x - a < 0 ∧ b < x ↔ a < x ∧ x < 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:
rw [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:
rw [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:
rw [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:
rw [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.Algebra.Order.Group.Abs

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

Tactic:
rw [div_eq_mul_inv, ← mabs_inv b]
  exact mabs_mul_le a _

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

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

Tactic:
mabs_one

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ 1 ≤ 1
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 * q ≤ 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
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ a * ↑p.succ + b * ↑q.succ ≤ ↑q * ↑p.succ + -1 * ↑q.succ

Tactic:
gcongr

Goal state after:
case ha
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := ⋯
b : ℤ := ⋯
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ 0 ≤ ↑p.succ

case hbc
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := ⋯
b : ℤ := ⋯
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ a ≤ ↑q

case ha
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := ⋯
b : ℤ := ⋯
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ 0 ≤ ↑q.succ
Module: Mathlib.Algebra.Group.WithOne.Defs

Goal state before:
pp: α : Type u
d : α
x : WithOne α
⊢ unoneD d x = d ↔ x = ↑d ∨ x = 1

Tactic:
simp [unoneD_eq_iff]

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

Goal state before:
pp: α : Type u
d : α
x : WithOne α
hx : x ≠ 1
⊢ unoneD d x = unone hx

Tactic:
simp [unoneD_eq_iff]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRegular (a * b)
ba : IsRegular (b * a)
⊢ IsRegular a ∧ IsRegular b

Tactic:
exact
      ⟨⟨IsLeftRegular.of_mul ba.left, IsRightRegular.of_mul ab.right⟩,
        ⟨IsLeftRegular.of_mul ab.left, IsRightRegular.of_mul ba.right⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝ : WithZero α ≃* WithZero β
x : WithZero α
⊢ ((fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
        ((fun e ↦
            { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
          x✝))
      x =
    x✝ x

Tactic:
cases x <;> simp

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:
cases x <;> simp

Goal state after:
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✝ : AddLeftMono α
a✝² a✝¹ a✝ : α
x✝ : a✝¹ ≤ a✝
⊢ a✝² + a✝¹ ≤ a✝² + a✝

Tactic:
gcongr

Goal state after:
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 α
a✝² a✝¹ a✝ : α
x✝ : a✝¹ ≤ a✝
⊢ a✝¹ + a✝² ≤ a✝ + a✝²

Tactic:
gcongr

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

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝¹ a✝ : α
x✝ : a✝¹ < a✝
⊢ x + a✝¹ < x + a✝

Tactic:
gcongr

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

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝¹ a✝ : α
x✝ : a✝¹ < a✝
⊢ a✝¹ + z < a✝ + z

Tactic:
gcongr

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

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

Tactic:
gcongr

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

Goal state before:
pp: α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
hz : z ≠ ⊤
x✝ : x ≤ y
⊢ x + z ≤ y + z

Tactic:
gcongr

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

Goal state before:
pp: α : Type u
inst✝³ : Add α
w x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightMono α
hw : w ≠ ⊤
hwy : w ≤ y
hxz : x < z
⊢ w + z ≤ y + z

Tactic:
gcongr

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

Goal state before:
pp: α : Type u
inst✝³ : Add α
w x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftMono α
inst✝ : AddRightStrictMono α
hx : x ≠ ⊤
hwy : w < y
hxz : x ≤ z
⊢ y + x ≤ y + z

Tactic:
gcongr

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

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 * (x + ↑n)
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✝ : AddLeftMono α
a✝² a✝¹ a✝ : α
x✝ : a✝¹ ≤ a✝
⊢ a✝² + a✝¹ ≤ a✝² + a✝

Tactic:
gcongr

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.symm) (WithBot.map (⇑e) x) = x

Tactic:
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:
cases x <;> simp

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 α
a✝² a✝¹ a✝ : α
x✝ : a✝¹ ≤ a✝
⊢ a✝¹ + a✝² ≤ a✝ + a✝²

Tactic:
gcongr

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
x : WithBot α
⊢ ↑a ≤ x → x ≤ ↑a

Tactic:
cases x <;> simp

Goal state after:
case coe
α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
a✝ : α
⊢ a ≤ a✝ → a✝ ≤ a