mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
x✝ : Int.negSucc n ≠ 0
⊢ 0 ^ Int.negSucc n = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
p : Prop
inst✝ : Decidable p
a : A
⊢ (if p then 1 else 0) • a = if p then a else 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁶ : MonoidWithZero M₀
inst✝⁵ : MonoidWithZero M₀'
inst✝⁴ : Zero A
inst✝³ : MulActionWithZero M₀ A
inst✝² : Zero A'
inst✝¹ : SMul M₀ A'
p : Prop
inst✝ : Decidable p
f : M₀' →*₀ M₀
m : A
⊢ f 1 • m = m

Tactic:
simp

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

Goal state before:
pp: case zero
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
⊢ a ^ (m + 0) = a ^ m * a ^ 0

Tactic:
simp

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

Goal state before:
pp: case inl
G₀ : Type u_2
inst✝ : CommGroupWithZero G₀
b : G₀
⊢ 0 ^ 2 * b / 0 = 0 * b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑(-↑0) = -↑↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑-[n+1] = -↑(n + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(n + 1) = -↑-[n+1]

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: case ofNat
R : Type u_1
inst✝ : AddGroupWithOne R
a✝ : ℕ
⊢ Int.ofNat a✝ • 1 = ↑(Int.ofNat a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: case negSucc
R : Type u_1
inst✝ : AddGroupWithOne R
a✝ : ℕ
⊢ Int.negSucc a✝ • 1 = ↑(Int.negSucc a✝)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ -1 • x = -x

Tactic:
simp

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

Goal state before:
pp: x✝ : ℤ
⊢ x✝ ^ 0 = 1

Tactic:
simp

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

Goal state before:
pp: case inl.zero
α : Type u_1
inst✝ : NonAssocRing α
⊢ ∀ (n : ℤ), ↑(↑0 * n) = ↑↑0 * ↑n

Tactic:
simp

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

Goal state before:
pp: case inr.zero
α : Type u_1
inst✝ : NonAssocRing α
⊢ ∀ (n : ℤ), ↑(-↑0 * n) = ↑(-↑0) * ↑n

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
m : ℤ
⊢ ∀ (n : ℤ), ↑(0 * n) = 0 • ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Equiv.Opposite

Goal state before:
pp: M : Type u_1
α✝ : Type u_2
α : Type ?u.6
β : Type ?u.8
inst✝¹ : Mul α
inst✝ : Mul β
f : αᵐᵒᵖ ≃* βᵐᵒᵖ
x : α
⊢ (unop ∘ ⇑f.symm ∘ MulOpposite.op) ((unop ∘ ⇑f ∘ MulOpposite.op) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Equiv.Opposite

Goal state before:
pp: M : Type u_1
α✝ : Type u_2
α : Type ?u.6
β : Type ?u.8
inst✝¹ : Mul α
inst✝ : Mul β
f : αᵐᵒᵖ ≃* βᵐᵒᵖ
x : β
⊢ (unop ∘ ⇑f ∘ MulOpposite.op) ((unop ∘ ⇑f.symm ∘ MulOpposite.op) x) = x

Tactic:
simp

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

Goal state before:
pp: case neg
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
hlm : ¬l < m
⊢ (ge l ⋯ fun k_1 x ↦ (fun k_2 x ↦ Int.strongRec lt ge k_2) k_1 ⋯) = Int.strongRec lt ge l

Tactic:
ih _ hl

Goal state after:
case neg
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
hlm : ¬l < m
⊢ (ge l ⋯ fun k_1 x ↦ (fun k_2 x ↦ Int.strongRec lt ge k_2) k_1 ⋯) = ge l ?neg✝ fun k x ↦ Int.strongRec lt ge k

case neg
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
hlm : ¬l < m
⊢ m ≤ l
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
⊢ (if P then a else 0) * b = if P then a * b else 0

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
⊢ (a * if P then b else 0) = if P then a * b else 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MulZeroOneClass α
P : Prop
inst✝ : Decidable P
a : α
⊢ (a * if P then 1 else 0) = if P then a else 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MulZeroOneClass α
P : Prop
inst✝ : Decidable P
a : α
⊢ (if P then 1 else 0) * a = if P then a else 0

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
a b : α
⊢ -a * -b = a * b

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
a b : α
⊢ -a * b = a * -b

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ -a = -1 * a

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ a * -1 = -a

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ -1 * a = -a

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (succ 0 + 1).sqrt ≤ succ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: ⊢ 0 = 0 * 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: case succ
i✝ : ℕ
a✝ : IsSquare (↑i✝).sign ↔ 0 ≤ ↑i✝
⊢ IsSquare (↑(i✝ + 1)).sign ↔ 0 ≤ i✝ + 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a c e f : α
⊢ a * e * (c * f) = a * c * (e * f)

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
⊢ a ^ 0 ∣ b ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: a b : Prop
l : List Prop
h : b ∈ l
H : (a :: l).TFAE
⊢ a ∈ a :: l

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
⊢ (map (fun p ↦ ∃ a, p a) l).TFAE

Tactic:
by
  simp only [TFAE, List.forall_mem_map]
  intro p₁ hp₁ p₂ hp₂
  exact exists_congr fun a ↦ H a (p₁ a) (mem_map_of_mem hp₁)
    (p₂ a) (mem_map_of_mem hp₂)

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Instances

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : One M
inst✝ : Monoid N
f : OneHom M N
n : ℕ
⊢ (⇑f ^ n) 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Instances

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f : M →* N
n : ℕ
⊢ (⇑f ^ n) 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Instances

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : One M
inst✝ : Group N
f : OneHom M N
n : ℤ
⊢ (⇑f ^ n) 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Instances

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommGroup N
f : M →* N
n : ℤ
⊢ (⇑f ^ n) 1 = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ x + (b - x) = b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
m : ℕ
⊢ ↑(m ^ 0) = ↑m ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : f 1 = 1
⊢ f 0 = ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: case zero
A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : ZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
⊢ f 0 = g 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: R : Type u_3
F : Type u_5
inst✝² : NonAssocSemiring R
inst✝¹ : FunLike F ℕ R
inst✝ : RingHomClass F ℕ R
f g : F
⊢ f 1 = g 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
x✝ : α
⊢ (g.comp 0) x✝ = 0 x✝

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
g : β →+* γ
f : α →+* β
⊢ g (f 1) = 1

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : MulOneClass R
inst✝ : HasDistribNeg R
a : R
⊢ SemiconjBy a (-1) (-1)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : MulOneClass R
inst✝ : HasDistribNeg R
x : R
⊢ SemiconjBy (-1) x x

Tactic:
simp

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

Goal state before:
pp: case inr.inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ a * b = ↑(ha.unit * hb.unit)

Tactic:
simp

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

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

Tactic:
simp +contextual [not_isUnit_iff_inverse_eq_zero]

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

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

Tactic:
simp +contextual [not_isUnit_iff_inverse_eq_zero]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ (∃ x, x ≠ 0 ∧ x = a) ↔ a ≠ 0

Tactic:
simp

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

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
⊢ 0⁻¹ʳ = 0⁻¹

Tactic:
simp

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ b * (a / b) = a

Tactic:
by
  rw [mul_comm, div_mul_cancel_of_imp h]

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

Goal state before:
pp: α : Type u
β : Type v
R : Type x
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
u : αˣ
⊢ -↑u * -↑u⁻¹ = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
R : Type x
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
u : αˣ
⊢ -↑u⁻¹ * -↑u = 1

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
⊢ (-1) ^ 2 = 1

Tactic:
by simp [neg_sq, one_pow]

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
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 * y) = f (-(x * y))

Tactic:
rw [neg, mul, neg, neg_mul, mul]

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

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

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

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

Goal state before:
pp: case zero
⊢ 2 ∣ 0 * (0 - 1)

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_4
inst✝ : AddMonoidWithOne R
h : 2 = 0
⊢ (Even 0 → ↑0 = 0) ∧ (Odd 0 → ↑0 = 1)

Tactic:
simp

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

Goal state before:
pp: case one
R : Type u_4
inst✝ : AddMonoidWithOne R
h : 2 = 0
⊢ (Even 1 → ↑1 = 0) ∧ (Odd 1 → ↑1 = 1)

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

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

Tactic:
apply le_of_add_le_add_right

Goal state after:
case bc
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ a + ?a ≤ a + c - (b + c) + b + ?a

case a
α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ α
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
← mul_le_mul_iff_left a⁻¹,

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

Goal state before:
pp: case inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a c : α
h : a ≤ a
⊢ a * c ≤ a * c

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂

Tactic:
by
  contrapose!
  exact fun h => mul_lt_mul_of_lt_of_lt h.1 h.2

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

Goal state before:
pp: α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
a : α
inst✝ : Nontrivial α
⊢ ∀ (a : α), ∃ b, a < b

Tactic:
obtain ⟨y, hy⟩ : ∃ a : α, 1 < a := exists_one_lt'
    exact fun a => ⟨a * y, lt_mul_of_one_lt_right' a hy⟩

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ OfNat.ofNat 0 = ↑0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ OfNat.ofNat 1 = ↑1

Tactic:
simp

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:
simp

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a : M₀
n : ℕ
inst✝ : ZeroLEOneClass M₀
ha : 0 ≤ a
hn : n ≠ 0
⊢ a ^ n ≤ 1 ↔ a ≤ 1

Tactic:
by
  refine ⟨fun h ↦ ?_, pow_le_one₀ ha⟩
  contrapose! h
  exact one_lt_pow₀ h hn

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:
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:
simp

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
e : α ≃ β
⊢ e.toEmbedding.trans e.symm.toEmbedding = Embedding.refl α

Tactic:
simp

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
e : α ≃ β
⊢ e.symm.toEmbedding.trans e.toEmbedding = Embedding.refl β

Tactic:
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
⊢ 1 ≤ a⁻¹ * b ↔ a ≤ b

Tactic:
by rw [le_inv_mul_iff₀ ha, mul_one]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : α ↪ γ
x✝ : α
⊢ ((fun f ↦ Embedding.congr h.symm h'.symm f) ((fun f ↦ Embedding.congr h h' f) x)) x✝ = x x✝

Tactic:
simp

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : β ↪ δ
x✝ : β
⊢ ((fun f ↦ Embedding.congr h h' f) ((fun f ↦ Embedding.congr h.symm h'.symm f) x)) x✝ = x x✝

Tactic:
simp

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

Goal state before:
pp: α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ ↪ β₁
g : β₁ ↪ γ₁
x✝ : α₂
⊢ ((ea.embeddingCongr ec) (f.trans g)) x✝ = (((ea.embeddingCongr eb) f).trans ((eb.embeddingCongr ec) g)) x✝

Tactic:
simp

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

Goal state before:
pp: case e'_1.e'_3
R : Type u
inst✝² : Semiring R
inst✝¹ : LinearOrder R
b c : R
inst✝ : PosMulStrictMono R
h : 0 < c
⊢ 0 = c * 0

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

Tactic:
← mul_le_mul_iff_of_pos_right hc,

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 * c⁻¹ * c ↔ 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⁻¹ ≤ a ↔ b ≤ a * c

Tactic:
← mul_le_mul_iff_of_pos_right hc,

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

Goal state before:
pp: case neg
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : a * b < a * c
hbc : b ≤ c
ha : a ≤ 0
⊢ 0 < a

Tactic:
grind [mul_le_mul_of_nonpos_left hbc ha]

Goal state after: