mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : S → R
hf : Injective f
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
⊢ -f x * f y = -f (x * y)

Tactic:
neg_mul,

Goal state after:
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
f : S → R
hf : Injective f
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
⊢ -(f x * f y) = -f (x * y)
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✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ f (-x * y) = -(f x * f y)

Tactic:
neg_mul,

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✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ f (-(x * y)) = -(f x * f y)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case h
α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
inst✝ : RightDistribClass α
b k : α
⊢ (k + k) * b = k * b + k * b

Tactic:
add_mul

Goal state after:
case h
α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
inst✝ : RightDistribClass α
b k : α
⊢ k * b + k * b = k * b + k * b
Module: Mathlib.Algebra.Ring.Parity

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

Tactic:
rw [mul_add, ← two_mul, add_assoc]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
n : ℕ
inst✝ : IsCancelAdd α
hn : Odd n
hab : a + b = 0
⊢ a ^ n + b ^ n = 0

Tactic:
obtain ⟨k, rfl⟩ := hn

Goal state after:
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
⊢ a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case succ
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) = 0

Tactic:
| succ k ih =>

Goal state after:
case succ
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
⊢ a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) = 0
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
k : ℕ
ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0
this : a ^ 2 = b ^ 2
⊢ (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3) = 0 + b ^ (2 * k + 1) * a ^ 2

Tactic:
rw [ih, zero_mul, zero_add, zero_add, this, ← pow_add]

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

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
⊢ Odd (-1)

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.IsBotOne

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
a : α
⊢ min 1 a = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.IsBotOne

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
a : α
⊢ min a 1 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.IsBotOne

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
a : α
⊢ max 1 a = a

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.IsBotOne

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
a : α
⊢ max a 1 = a

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.MinMax

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ ∀ (x : α), max x x = x

Tactic:
by simp

Goal state after:
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:
grw [tsub_le_iff_left, add_right_comm, ← le_add_tsub]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a ≤ 1 * b ↔ a ≤ b

Tactic:
rw [one_mul]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ b ≤ 1 * a ↔ b ≤ a

Tactic:
rw [one_mul]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ b < 1 * a ↔ b < a

Tactic:
rw [one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulRightMono α
inst✝ : MulRightReflectLE α
a b : α
⊢ a ≤ b * a ↔ 1 * a ≤ b * a

Tactic:
rw [one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulRightMono α
inst✝ : MulRightReflectLE α
a b : α
⊢ a * b ≤ b ↔ a * b ≤ 1 * b

Tactic:
rw [one_mul]

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

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

Tactic:
rw [one_mul]

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

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

Tactic:
rw [one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b

Tactic:
by
  simpa only [zero_mul] using mul_le_mul_of_nonneg_right ha hb

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

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b ≤ 0

Tactic:
by
  simpa only [zero_mul] using mul_le_mul_of_nonneg_right ha hb

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

Goal state before:
pp: α : Type u_1
s : Semiring α
⊢ ∀ (a : α), 0 * a = 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Semiring α
a : α
⊢ a ^ 0 = 1

Tactic:
by simp

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝³ : MulZeroClass α
b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < 0 * b
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

Tactic:
rw [zero_mul] at hab
    exact hab.false.elim

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

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

Tactic:
rw [one_mul]

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

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

Tactic:
rw [one_mul]

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

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

Tactic:
rw [one_mul]

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

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

Tactic:
rw [one_mul]

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a b : M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 0 ≤ a
hab : a ≤ b
⊢ a ^ 0 ≤ b ^ 0

Tactic:
by simp

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

Goal state before:
pp: case inl
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a : M₀
inst✝ : ZeroLEOneClass M₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : a < 1
⊢ Injective fun x ↦ a ^ x

pp: case inr
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a : M₀
inst✝ : ZeroLEOneClass M₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : 1 < a
⊢ Injective fun x ↦ a ^ x

Tactic:
· exact (pow_right_strictAnti₀ ha₀ ha₁).injective

Goal state after:
case inr
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a : M₀
inst✝ : ZeroLEOneClass M₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : 1 < a
⊢ Injective fun x ↦ a ^ x
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:
by
  rw [mul_one_sub, one_add_mul, sub_le_sub_iff, add_assoc, add_comm b]
  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
inst✝ : Nontrivial R
a : R
⊢ a < a + 1

Tactic:
by simp

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
inst✝ : Nontrivial R
a : R
⊢ a - 1 < a

Tactic:
by simp

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 : G₀
ha : 0 < a
⊢ a⁻¹ * b < 1 ↔ b < a

Tactic:
rw [inv_mul_lt_iff₀ ha, mul_one]

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✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ a * a = 0 ∧ b * b = 0 ↔ a = 0 ∧ b = 0

pp: case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ a * a

pp: case hb
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ b * b

Tactic:
mul_self_eq_zero (M₀ := R),

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ a = 0 ∧ b * b = 0 ↔ a = 0 ∧ b = 0

case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ a * a

case hb
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ b * b
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 : G₀
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Tactic:
inv_le_iff_one_le_mul₀' ha,

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ 1 ≤ a * b⁻¹ ↔ b ≤ a
Module: Mathlib.Order.Lex

Goal state before:
pp: α : Type u_1
a b : α
⊢ toLex a = toLex b ↔ a = b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Lex

Goal state before:
pp: α : Type u_1
a b : Lex α
⊢ ofLex a = ofLex b ↔ a = b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Lex

Goal state before:
pp: α : Type u_1
a b : α
⊢ toColex a = toColex b ↔ a = b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Lex

Goal state before:
pp: α : Type u_1
a b : Colex α
⊢ ofColex a = ofColex b ↔ a = b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ ∀ (x : β), (e.symm.trans e) x = (RelIso.refl s) x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ ∀ (x : α), (e.trans e.symm) x = (RelIso.refl r) x

Tactic:
by simp

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
r : α → α → Prop
s : β → β → Prop
inst✝ : IsEmpty β
⊢ ∀ {a b : α ⊕ β}, r ((Equiv.sumEmpty α β) a) ((Equiv.sumEmpty α β) b) ↔ Sum.Lex r s a b

Tactic:
by simp

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
r : α → α → Prop
s : β → β → Prop
inst✝ : IsEmpty α
⊢ ∀ {a b : α ⊕ β}, s ((Equiv.emptySum α β) a) ((Equiv.emptySum α β) b) ↔ Sum.Lex r s a b

Tactic:
by simp

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_6
β : Type u_7
inst✝³ : Unique α
inst✝² : Unique β
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ ∀ {a b : α}, (Equiv.ofUnique α β) a ≤ (Equiv.ofUnique α β) b ↔ a ≤ b

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedMonoid R
inst✝ : MulArchimedean R
a : R
ha : a < 1
b : R
⊢ ∀ (a_1 : ℕ), b⁻¹ < a⁻¹ ^ a_1 → a ^ a_1 < b

Tactic:
by simp

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

Goal state before:
pp: case left
α✝ : Type u_1
inst✝⁴ : Lattice α✝
inst✝³ : CommGroup α✝
α : Type u_2
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ y) * (x ⊔ y)

Tactic:
exact mul_le_mul' (inf_le_inf_left _ inf_le_left) inf_le_left

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
⊢ 1 ≤ a ^ 0

Tactic:
by simp

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✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
x✝ : 1 ≠ 0
⊢ a ^ 1 ≤ b ^ (1 - 1) * a

Tactic:
by simp

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
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
⊢ a ^ 0 ≤ b ^ 0

Tactic:
by simp

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

Goal state before:
pp: G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
H : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ n

Tactic:
apply one_le_pow_of_one_le' H

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

Goal state before:
pp: n : ℤ
⊢ ∃ k, n = 2 * k ∨ n = 2 * k + 1

Tactic:
simpa only [two_mul, exists_or, Odd, Even] using even_or_odd n

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

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
⊢ max a b / min a b = |b / a|ₘ

Tactic:
rw [mabs_div_comm, max_div_min_eq_mabs']

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

Goal state before:
pp: x y : ℕ
⊢ ∀ (n : ℕ) (s t s' t' : ℤ), (xgcdAux 0 s t n s' t').1 = gcd 0 n

Tactic:
by simp

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

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s : ℤ
⊢ ∀ {t s' t' : ℤ}, x.P y (a, s, t) → x.P y (b, s', t') → x.P y (a.xgcdAux s t b s' t')

Tactic:
t

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s t : ℤ
⊢ ∀ {s' t' : ℤ}, x.P y (a, s, t) → x.P y (b, s', t') → x.P y (a.xgcdAux s t b s' t')
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 + b * ↑q.succ = ↑n

Tactic:
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]

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

Goal state before:
pp: α : Type u
inst✝ : Semigroup α
b c : WithOne α
⊢ 1 * b * c = 1 * (b * c)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : Semigroup α
a : α
c : WithOne α
⊢ ↑a * 1 * c = ↑a * (1 * c)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : Semigroup α
a b : α
⊢ ↑a * ↑b * 1 = ↑a * (↑b * 1)

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : AddMonoid α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedAdd α
a : WithBot α
⊢ a < 0 ↔ a = ⊥

Tactic:
induction a <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : MulOneClass α
inst✝ : MulZeroOneClass β
f : α →* β
⊢ recZeroCoe 0 (⇑f) 1 = 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulZeroOneClass β
f : α →* β
hf : Surjective ⇑f
a : α
⊢ (lift' f) ↑a = f a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : ∀ (b : β), ∃ a, f a = b
⊢ (map' f) 0 = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
h : ∀ (x y : R), x * y = 1 → IsRightRegular y
a✝ b✝ : R
eq : a✝ * b✝ = 1
⊢ (fun x ↦ x * b✝) (b✝ * a✝) = (fun x ↦ x * b✝) 1

Tactic:
simp [mul_assoc, eq]

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
h : ∀ (x y : R), x * y = 1 → IsRightRegular y
a✝ b✝ : R
eq : a✝ * b✝ = 1
⊢ (fun x ↦ x * b✝) (b✝ * a✝) = (fun x ↦ x * b✝) 1

Tactic:
by simp [mul_assoc, eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : InvolutiveInv α
a : WithZero α
⊢ Option.map ((fun x ↦ x⁻¹) ∘ fun x ↦ x⁻¹) a = a

Tactic:
by simp

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

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x : M
⊢ exp x = 1 ↔ x = 0

Tactic:
rw [← exp_zero, exp_inj]

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

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
⊢ (0 ^ 0).log = 0 • log 0

Tactic:
by simp

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

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
n : ℕ
⊢ (0 ^ (n + 1)).log = (n + 1) • log 0

Tactic:
by simp

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

Goal state before:
pp: G : Type u_5
inst✝ : AddGroup G
⊢ 0⁻¹.log = -log 0

Tactic:
by simp

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

Goal state before:
pp: G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : ↑x ≠ 0
H : f ↑x = 0
⊢ False

Tactic:
apply one_ne_zero (α := M₀)

Goal state after:
G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : ↑x ≠ 0
H : f ↑x = 0
⊢ 1 = 0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
b : WithTop α
c : α
⊢ ⊤ + b = ↑c ↔ ∃ a' b', ↑a' = ⊤ ∧ ↑b' = b ∧ a' + b' = c

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : Add α
a c : α
⊢ ↑a + ⊤ = ↑c ↔ ∃ a' b', ↑a' = ↑a ∧ ↑b' = ⊤ ∧ a' + b' = c

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : Add α
x : WithTop α
b : α
⊢ x + ↑b = ⊤ ↔ x = ⊤

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : Add α
y : WithTop α
a : α
⊢ ↑a + y = ⊤ ↔ y = ⊤

Tactic:
by 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 c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a - b ≤ a - c ↔ c ≤ b

Tactic:
by
  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.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : AddLeftReflectLE α
h : AddLECancellable ⊤
⊢ ⊤ + ⊤ ≤ ⊤ + ↑(Classical.arbitrary α)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LE α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a b : WithTop α
⊢ ⊤ ≤ ⊤ → ∃ c, ⊤ = ⊤ + c

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : Add α
b : WithBot α
c : α
⊢ ⊥ + b = ↑c ↔ ∃ a' b', ↑a' = ⊥ ∧ ↑b' = b ∧ a' + b' = c

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : Add α
a c : α
⊢ ↑a + ⊥ = ↑c ↔ ∃ a' b', ↑a' = ↑a ∧ ↑b' = ⊥ ∧ a' + b' = c

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : Add α
x : WithBot α
b : α
⊢ x + ↑b = ⊥ ↔ x = ⊥

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝ : Add α
y : WithBot α
a : α
⊢ ↑a + y = ⊥ ↔ y = ⊥

Tactic:
by simp

Goal state after: