mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
⊢ ⇑f.toMonoidWithZeroHom = ⇑f

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x✝ : β
⊢ ↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) x✝ = f x✝

Tactic:
rfl

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
⊢ IsUnit a ∧ ¬IsUnit b ∨ ¬IsUnit a ∧ IsUnit b ∨ IsUnit a ∧ IsUnit b

Tactic:
grind

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

Goal state before:
pp: M₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ ¬IsUnit x ↔ x⁻¹ʳ = 0

Tactic:
grind

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
h : 1 ≠ 0
⊢ ↑(mk0 1 h) = ↑1

Tactic:
rfl

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
x y : G₀
hxy : x * y ≠ 0
⊢ ↑(mk0 (x * y) hxy) = ↑(mk0 x ⋯ * mk0 y ⋯)

Tactic:
rfl

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

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

Tactic:
natCast

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
inst✝ : AddMonoidWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
n : ℕ
⊢ ↑n + 1 = ↑n + 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✝ : 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
n : ℕ
⊢ f ↑n + 1 = ↑n + 1

Tactic:
natCast

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✝ : 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
n : ℕ
⊢ ↑n + 1 = ↑n + 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 : ℕ
⊢ f ↑n = ↑n

Tactic:
natCast

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 : ℕ
⊢ ↑n = ↑n
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Covariant N N (fun b a ↦ mu a b) r ↔ Covariant N N mu r

Tactic:
simp_rw [h.comm]

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

Goal state before:
pp: N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Contravariant N N (fun b a ↦ mu a b) r ↔ Contravariant N N mu r

Tactic:
simp_rw [h.comm]

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 : ℕ
⊢ -f ↑(n + 1) = -↑(n + 1)

Tactic:
natCast

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 : ℕ
⊢ -↑(n + 1) = -↑(n + 1)
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) + 1) + b ^ (2 * k + 1) * a ^ 2 + b ^ (2 * (k + 1) + 1) =
    a ^ (2 * k + 1 + 2) + b ^ (2 * k + 1) * a ^ 2 + b ^ (2 * k + 3)

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.OpClass

Goal state before:
pp: α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f a (f b c) = f b (f a c)

Tactic:
rw [← ha.assoc, hc.comm a, ha.assoc]

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

Goal state before:
pp: n : ℕ
⊢ ¬Odd n ↔ n % 2 = 0

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ ¬Odd n ↔ Even n

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ ¬Even n ↔ Odd n

Tactic:
grind

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

Goal state before:
pp: ⊢ ¬Odd 0

Tactic:
grind

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

Goal state before:
pp: n : ℕ
h : Odd n
⊢ ¬2 ∣ n

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ Xor (Even n) (Odd n)

Tactic:
grind

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

Goal state before:
pp: case h
k : ℕ
⊢ Xor (k + k = 2 * k) (k + k = 2 * k + 1)

Tactic:
grind

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

Goal state before:
pp: case h
k : ℕ
⊢ Xor (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ Odd (n + 1) ↔ ¬Odd n

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
hn : Odd n
⊢ m % 2 + (m + n) % 2 = 1

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
⊢ Even (m + n) ↔ (Odd m ↔ Odd n)

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ ¬Even (2 * n + 1)

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ (Odd m ↔ Odd n)

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
hm : Odd m
hn : Odd n
⊢ Even (m - n)

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
⊢ Odd (m * n) ↔ Odd m ∧ Odd n

Tactic:
grind

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

Goal state before:
pp: n e : ℕ
he : e ≠ 0
⊢ Odd (n ^ e) ↔ Odd n

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
⊢ Odd (m + n) ↔ (Odd m ↔ Even n)

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
⊢ Odd (m + n) ↔ (Odd n ↔ Even m)

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
h : Odd (m + n)
⊢ m ≠ n

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
h : n ≤ m
⊢ Odd (m - n) ↔ (Odd m ↔ Even n)

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
h : n ≤ m
hm : Odd m
hn : Even n
⊢ Odd (m - n)

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
h : n ≤ m
⊢ Odd (m - n) ↔ (Odd n ↔ Even m)

Tactic:
grind

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

Goal state before:
pp: m n : ℕ
h : n ≤ m
hm : Even m
hn : Odd n
⊢ Odd (m - n)

Tactic:
grind

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

Goal state before:
pp: n : ℕ
h : Odd n
⊢ 2 * (n / 2) + 1 = n

Tactic:
grind

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

Goal state before:
pp: n : ℕ
h : Odd n
⊢ n / 2 * 2 + 1 = n

Tactic:
grind

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

Goal state before:
pp: n : ℕ
h : Odd n
⊢ 1 + n / 2 * 2 = n

Tactic:
grind

Goal state after:
Module: Mathlib.Order.MinMax

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a b : α
⊢ min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a

Tactic:
grind

Goal state after:
Module: Mathlib.Order.MinMax

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min a b = c ↔ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a

Tactic:
grind

Goal state after:
Module: Mathlib.Order.MinMax

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min a c < min b c ↔ a < b ∧ a < c

Tactic:
grind

Goal state after:
Module: Mathlib.Order.MinMax

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min a b < min a c ↔ b < c ∧ b < a

Tactic:
grind

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

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

Tactic:
by
  rw [← mul_lt_mul_iff_right a, inv_mul_cancel, 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 : α
⊢ 1 < a⁻¹ ↔ a < 1

Tactic:
by
  rw [← mul_lt_mul_iff_right a, inv_mul_cancel, one_mul]

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ c⁻¹ * a < b ↔ a < b * c

Tactic:
by rw [inv_mul_lt_iff_lt_mul, mul_comm]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ b₁ : α
this✝ : MulLeftMono α
this : MulRightMono α
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁ * b₁ ≤ a₁ * b₁

Tactic:
rfl

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

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hac : a < c
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
grind

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

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
b c a : α
⊢ a / b < a / c ↔ c < b

Tactic:
by
  rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_lt_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_lt_inv_iff]

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

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hbd : b < d
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommSemigroup β
f : α → β
a b : α
⊢ f (min a b) * f (max a b) = f a * f b

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommSemigroup β
f : α → β
a b : α
⊢ f (max a b) * f (min a b) = f a * f b

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Semiring α
⊢ ↑2 = 2

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n✝ n : ℕ
⊢ OfNat.ofNat (n + 2) = ↑(n + 2)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a c : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
a0 : 0 < a
hab : a ≤ a
hcd : c ≤ c
d0 : 0 < c
⊢ a * c = a * c

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a c : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
c0 : 0 < c
hab : a ≤ a
b0 : 0 < a
hcd : c ≤ c
⊢ a * c = a * c

Tactic:
rfl

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✝ : PosMulMono α
ha : 0 ≤ a
h : b ≤ 1
⊢ a * b ≤ a

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonneg_left h ha

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✝ : PosMulMono α
ha : 0 ≤ a
h : 1 ≤ b
⊢ a ≤ a * b

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonneg_left h ha

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✝ : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
⊢ a ^ (n + 1) ≤ a ^ n

Tactic:
have : ZeroLEOneClass M₀ := ⟨ha₀.trans ha₁⟩
    rw [← mul_one (a ^ n), pow_succ]
    gcongr
    exact pow_nonneg ha₀ n

Goal state after:
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₀
inst✝ : ZeroLEOneClass M₀
ha : 0 < a
⊢ 0 < a ^ 0

Tactic:
by nontriviality; rw [pow_zero]; exact zero_lt_one

Goal state after:
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort ?u.9
β : Type ?u.24
x✝¹ : α ≃ β
x✝ : α
⊢ ((fun f ↦ (↑f).equivOfSurjective ⋯) ((fun f ↦ ⟨f.toEmbedding, ⋯⟩) x✝¹)) x✝ = x✝¹ x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (f a' = b)
x y : α
h :
  (fun a' ↦ if a' = a then b else if f a' = b then f a else f a') x =
    (fun a' ↦ if a' = a then b else if f a' = b then f a else f a') y
⊢ x = y

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: β : Sort u_1
b : β
a✝ : (fun x ↦ b) PUnit.unit = (fun x ↦ b) PUnit.unit
⊢ PUnit.unit = PUnit.unit

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst✝ : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
f : α₁ → γ
a : α₃
⊢ extend (⇑e₂₃) (extend (⇑e₁₂) f fun a ↦ default) (fun a ↦ default) a =
    extend (⇑e₂₃) (extend (⇑e₁₂) f ((fun a ↦ default) ∘ ⇑e₂₃)) (fun a ↦ default) a

Tactic:
Function.comp_def

Goal state after:
α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst✝ : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
f : α₁ → γ
a : α₃
⊢ extend (⇑e₂₃) (extend (⇑e₁₂) f fun a ↦ default) (fun a ↦ default) a =
    extend (⇑e₂₃) (extend (⇑e₁₂) f fun x ↦ default) (fun a ↦ default) a
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 + 1) ≤ a ^ n

Tactic:
rw [zpow_add_one₀ ha₀.ne']

Goal state after:
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
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 + 1) < a ^ n

Tactic:
rw [zpow_add_one₀ ha₀.ne']

Goal state after:
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
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₀
inst✝ : MulPosMono G₀
n : ℤ
hn : 0 ≤ n
ha : 0 ≤ a
h : a ≤ b
⊢ b ∈ {a | 0 ≤ a}

Tactic:
grind

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₀
inst✝ : MulPosMono G₀
n : ℤ
hn : 0 < n
ha : 0 ≤ a
h : a < b
⊢ b ∈ {a | 0 ≤ a}

Tactic:
grind

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₀
hc : 0 < c
⊢ a * c ≤ b * c⁻¹ * c ↔ a * c ≤ b

Tactic:
inv_mul_cancel_right₀ hc.ne'

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a * c ≤ b ↔ a * c ≤ b
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₀
hc : 0 < c
⊢ b * c⁻¹ * c ≤ a * c ↔ b ≤ a * c

Tactic:
inv_mul_cancel_right₀ hc.ne'

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b ≤ a * c ↔ b ≤ a * c
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₀
hc : 0 < c
⊢ a * c < b * c⁻¹ * c ↔ a * c < b

Tactic:
inv_mul_cancel_right₀ hc.ne'

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a * c < b ↔ a * c < b
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₀
hc : 0 < c
⊢ b * c⁻¹ * c < a * c ↔ b < a * c

Tactic:
inv_mul_cancel_right₀ hc.ne'

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b < a * c ↔ b < a * c
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✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
⊢ 0 ≤ a * -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
mul_nonneg_iff (R := R),

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
⊢ 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Module: Mathlib.Algebra.Order.Group.OrderIso

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a x : α
⊢ (mulRight a).symm x = (mulRight a⁻¹) x

Tactic:
rfl

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a x : α
⊢ (mulLeft a).symm x = (mulLeft a⁻¹) x

Tactic:
rfl

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
α : Type u
r : α → α → Prop
a b : α
s : α → α → Prop
h₂ : r ≍ s
⊢ s ((Equiv.cast ⋯) a) ((Equiv.cast ⋯) b) ↔ s a b

Tactic:
rfl

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

Goal state before:
pp: α γ : Type u
r : α → α → Prop
t : γ → γ → Prop
x : α
s : α → α → Prop
h₁' : α = γ
h₂ : r ≍ s
h₂' : s ≍ t
⊢ ((RelIso.cast ⋯ h₂).trans (RelIso.cast h₁' h₂')) x = (RelIso.cast ⋯ ⋯) x

Tactic:
rfl

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
x✝¹ : r ≃r s
x✝ : α
⊢ ((fun f ↦ ofSurjective ↑f ⋯) ((fun f ↦ ⟨f.toRelEmbedding, ⋯⟩) x✝¹)) x✝ = x✝¹ x✝

Tactic:
rfl

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
f : α ↪ β
⊢ ∀ {a b : α}, r (f a) (f b) ↔ (r on ⇑f) a b

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
x✝ : α
⊢ (f.comp id) x✝ = f x✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
x✝ : α
⊢ (id.comp f) x✝ = f x✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x : α
y : β
⊢ (fst.prod snd) (x, y) = id (x, y)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
f : α ↪o β
x✝ : α
⊢ ((id α).comp f) x✝ = f x✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
f : α ↪o β
x✝ : α
⊢ (f.comp (id β)) x✝ = f x✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
x : α
⊢ ((refl α).trans e) x = e x

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
x : α
⊢ (e.trans (refl β)) x = e x

Tactic:
rfl

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✝³ : LE α
inst✝² : LE β
inst✝¹ : LE γ
inst✝ : LE δ
x✝¹ : α ≃o β
x✝ : α
⊢ ((fun f ↦ ofSurjective ↑f ⋯) ((fun f ↦ ⟨RelIso.toRelEmbedding f, ⋯⟩) x✝¹)) x✝ = x✝¹ x✝

Tactic:
rfl

Goal state after: