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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0, ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0,
      ∀ {a : R}, a ≠ 0 → IsRegular a].TFAE

Tactic:
isRegular_iff_eq_zero_of_mul

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0, ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0,
      ∀ {a : R}, a ≠ 0 → (∀ (x : R), a * x = 0 → x = 0) ∧ ∀ (x : R), x * a = 0 → x = 0].TFAE
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -a / -b = a / b

Tactic:
div_neg_eq_neg_div,

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -(-a / b) = a / b
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ m * a ^ (-n) = a ^ m / a ^ n

Tactic:
zpow_neg,

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ m * (a ^ n)⁻¹ = a ^ m / a ^ n
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : M
⊢ 0 • a = 0

Tactic:
simp_rw [HSMul.hSMul, SMul.smul, Int.cast_zero]; exact zero_smul R a

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 + b - c ≤ a - c + b

Tactic:
rw [add_comm, add_comm _ b]

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ b + a - c ≤ b + (a - c)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
hb : AddLECancellable b
⊢ a ≤ b + a - b

Tactic:
exact hb.le_add_tsub_swap

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 : α
hb : AddLECancellable b
⊢ a ≤ a + b - b

Tactic:
rw [add_comm]
  exact hb.le_add_tsub_swap

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

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

Tactic:
rw [inv_mul_cancel_right]

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

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

Tactic:
rw [inv_mul_cancel_right]

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

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

Tactic:
rw [inv_mul_cancel_right]

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 d : α
inst✝ : MulRightStrictMono α
⊢ a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b

Tactic:
rw [← mul_lt_mul_iff_left d, ← mul_lt_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
    inv_mul_cancel_right]

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
mul_le_mul_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
toIsOrderedMonoid : IsOrderedMonoid α := { mul_le_mul_left := mul_le_mul_left }
le_of_mul_le_mul_left : ∀ (a b c : α), a * b ≤ a * c → b ≤ c
a b c : α
h : a * b ≤ c * a
⊢ b ≤ c

Tactic:
mul_comm _ a

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
mul_le_mul_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
toIsOrderedMonoid : IsOrderedMonoid α := { mul_le_mul_left := mul_le_mul_left }
le_of_mul_le_mul_left : ∀ (a b c : α), a * b ≤ a * c → b ≤ c
a b c : α
h : a * b ≤ a * c
⊢ b ≤ c
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a * a ≤ 1 ↔ a ≤ 1

Tactic:
contrapose!; exact one_lt_mul_self_iff

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₀
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ^ (n + 1) < 1

Tactic:
by
    rw [pow_succ']; exact mul_lt_one_of_nonneg_of_lt_one_left h₀ h₁ (pow_le_one₀ h₀ h₁.le)

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

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : ZeroLEOneClass R
inst✝ : Nontrivial R
mul_pos : ∀ (a b : R), 0 < a → 0 < b → 0 < a * b
a : R
ha : 0 < a
b c : R
hbc : b < c
⊢ b * a < c * a

Tactic:
simpa only [sub_mul, sub_pos] using mul_pos _ _ (sub_pos.2 hbc) 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✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (-↑(n + 1))

Tactic:
zpow_neg,

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ (a ^ ↑(n + 1))⁻¹
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
n : ℕ
⊢ 0 < a ^ (-↑(n + 1))

Tactic:
zpow_neg,

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 < a
n : ℕ
⊢ 0 < (a ^ ↑(n + 1))⁻¹
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
or_a : 0 ≤ a ∨ a ≤ 0
or_b : 0 ≤ b ∨ b ≤ 0
or_c : 0 ≤ c ∨ c ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0

Tactic:
aesop

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

Goal state before:
pp: case mpr.inl
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
h✝ : a ≠ 0
h : a < 0
⊢ 0 < a * a

pp: case mpr.inr
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
h✝ : a ≠ 0
h : 0 < a
⊢ 0 < a * a

Tactic:
exacts [mul_pos_of_neg_of_neg h h, mul_pos h h]

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 β
inst✝² : Preorder γ
inst✝¹ : Preorder δ
ι : Type u_6
π : ι → Type u_7
inst✝ : (i : ι) → Preorder (π i)
p q : α → Prop
h : ∀ (a : α), p a → q a
⊢ ∀ {a b : { x // p x }}, (Subtype.impEmbedding p q h) a ≤ (Subtype.impEmbedding p q h) b ↔ a ≤ b

Tactic:
aesop

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 b c : G
⊢ b ≤ a * c ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c

Tactic:
div_le_iff_le_mul',

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ b ≤ a * c ∧ a ≤ b * c ↔ a ≤ b * c ∧ b / a ≤ c
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ 1 ≤ |b / a|ₘ

Tactic:
exact one_le_mabs _

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ ((b ⊔ a) ⊓ c) * (b ⊔ a ⊔ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)

Tactic:
inf_mul_sup,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ a) * c / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a⁻¹ < b ∧ a < b ↔ b⁻¹ < a ∧ a < b

Tactic:
inv_lt'

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ b⁻¹ < a ∧ a < b ↔ b⁻¹ < a ∧ a < b
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: x y : ℕ
⊢ x.P y (x, 1, 0)

Tactic:
simp [P]

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

Goal state before:
pp: x y : ℕ
⊢ x.P y (y, 0, 1)

Tactic:
simp [P]

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ Commute a b

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ Commute b b

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : CommGroupWithZero α
m n : ℕ
hmn : m.Coprime n
a : α
⊢ (∃ c, a = c ^ n) ↔ ∃ y, y ^ n = a

Tactic:
aesop

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

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

Tactic:
by
  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:
by
  simp [unoneD_eq_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ (if n + 1 = 0 then 0 else ↑↑(n + 1)) = (if n = 0 then 0 else ↑↑n) + 1

Tactic:
by cases n <;> 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 : α
⊢ a - b = 0 ↔ a ≤ b

Tactic:
by
  rw [← nonpos_iff_eq_zero, tsub_le_iff_left, add_zero]

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

Goal state before:
pp: case refine_2
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
m : ℕ
hm : m < Nat.find hₙ - n
hpm : p (m + n)
⊢ Nat.find hₙ - n ≤ m

Tactic:
rw [Nat.sub_le_iff_le_add]

Goal state after:
case refine_2
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
m : ℕ
hm : m < Nat.find hₙ - n
hpm : p (m + n)
⊢ Nat.find hₙ ≤ m + n
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
x y z : WithTop α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
by
    cases x <;> cases y <;> cases z <;> simp [← WithTop.coe_inf, ← WithTop.coe_sup]
    simpa [← coe_inf, ← coe_sup] using le_sup_inf

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
⊢ ⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊

Tactic:
by
  rw [ceil_le, Nat.cast_add]
  gcongr <;> apply le_ceil

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ y * ↑x + y * x.neg = 0

Tactic:
simp [← mul_add]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ y * x.neg + y * ↑x = 0

Tactic:
simp [← mul_add]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ ↑x * ↑(-y) + ↑(x.mulRight ↑y) = 0

Tactic:
simp [← mul_add]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithTop αᵒᵈ
y : WithBot α
⊢ x ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual x

Tactic:
by cases x <;> cases y <;> simp [le_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x : WithTop α
y : WithBot αᵒᵈ
⊢ x ≤ WithBot.ofDual y ↔ y ≤ WithTop.toDual x

Tactic:
by cases x <;> cases y <;> simp [le_toDual]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
have hb := h.not.mp ha
    simp [inverse_non_unit, ha, hb]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ

Tactic:
have hb := h.not.mp ha
    simp [inverse_non_unit, ha, hb]

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

Goal state before:
pp: case inl
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
this : f (t * 0) = f t * f 0
⊢ f t = 1

Tactic:
rw [← one_mul (f (t * 0)), mul_zero] at this

Goal state after:
case inl
M : Type u_1
G₀ : Type u_3
F : Type u_6
inst✝³ : Monoid M
inst✝² : GroupWithZero G₀
inst✝¹ : FunLike F G₀ M
inst✝ : MonoidHomClass F G₀ M
f : F
h : IsUnit (f 0)
t : G₀
ht : f t ≠ 1
this : 1 * f 0 = f t * f 0
⊢ f t = 1
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a : K
h : a ≠ 0
⊢ a / -a = -1

Tactic:
div_neg_eq_neg_div,

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
a : K
h : a ≠ 0
⊢ -(a / a) = -1
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|

Tactic:
rw [← mabs_inv, ← zpow_neg, ← abs_neg, h, zpow_natCast, Nat.abs_cast, zpow_natCast]

Goal state after:
case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ |a ^ m|ₘ = |a|ₘ ^ m
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
hn✝ : n ≠ 0
hn : Odd n ∧ ¬Even n
⊢ a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n

Tactic:
simp [hn, (hn.1.strictMono_pow (R := R)).injective.eq_iff]

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst✝³ : EquivLike E { x // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ (if h_1 : True then if e ⟨i, ⋯⟩ = j then x else v (e ⟨i, ⋯⟩) else w i) =
    if i = ↑(EquivLike.inv e j) then x else if h_1 : True then v (e ⟨i, ⋯⟩) else w i

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b x : α
⊢ x ∈ Icc a b \ {a} ↔ x ∈ Ioc a b

Tactic:
by simp [lt_iff_le_and_ne, eq_comm, and_right_comm]

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ Icc a b \ ({a} ∪ {b}) = Ioo a b

Tactic:
← sdiff_sdiff,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ (Icc a b \ {a}) \ {b} = Ioo a b
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : Preorder α
t : Set α
hn : (∅ ∪ t).Nonempty
h✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (∅ ∪ t)
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ∅
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ∅ ∧ ∅.Nonempty ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ t.Nonempty

Tactic:
aesop

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
t : Set γ
hf : MapsTo f s.1 t
hg : MapsTo g s.2 t
a : α
⊢ Sum.inl a ∈ sumEquiv.symm s → Sum.elim f g (Sum.inl a) ∈ t

Tactic:
aesop

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
t : Set γ
hf : MapsTo f s.1 t
hg : MapsTo g s.2 t
b : β
⊢ Sum.inr b ∈ sumEquiv.symm s → Sum.elim f g (Sum.inr b) ∈ t

Tactic:
aesop

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Preorder α
s : Set α
hn : (s ∪ ∅).Nonempty
h✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ ∅)
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ∅
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ∅ ∧ ∅.Nonempty

Tactic:
aesop

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

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
a₁ : α
h₁ : Sum.inl a₁ ∈ sumEquiv.symm s
a₂ : α
h₂ : Sum.inl a₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inl a₁) = Sum.elim f g (Sum.inl a₂)
⊢ Sum.inl a₁ = Sum.inl a₂

Tactic:
aesop

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

Goal state before:
pp: case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
a₁ : α
h₁ : Sum.inl a₁ ∈ sumEquiv.symm s
b₂ : β
h₂ : Sum.inr b₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inl a₁) = Sum.elim f g (Sum.inr b₂)
⊢ Sum.inl a₁ = Sum.inr b₂

Tactic:
aesop

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
b₁ : β
h₁ : Sum.inr b₁ ∈ sumEquiv.symm s
a₂ : α
h₂ : Sum.inl a₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inr b₁) = Sum.elim f g (Sum.inl a₂)
⊢ Sum.inr b₁ = Sum.inl a₂

Tactic:
aesop

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
b₁ : β
h₁ : Sum.inr b₁ ∈ sumEquiv.symm s
b₂ : β
h₂ : Sum.inr b₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inr b₁) = Sum.elim f g (Sum.inr b₂)
⊢ Sum.inr b₁ = Sum.inr b₂

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: ⊢ Iic False = {False}

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: ⊢ Iic True = univ

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: ⊢ Ici False = univ

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: ⊢ Ici True = {True}

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: ⊢ Iio False = ∅

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: ⊢ Ioi True = ∅

Tactic:
aesop

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : a ≤ b
⊢ 1 / b ≤ 1 / a

Tactic:
simpa using inv_anti₀ ha h

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: n✝¹ n✝ : ℕ
⊢ ↑n✝¹ % ↑n✝ = ↑(n✝¹.mod n✝)

Tactic:
aesop

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: n✝¹ n✝ : ℕ
⊢ ↑n✝¹ / ↑n✝ = ↑(n✝¹.div n✝)

Tactic:
aesop

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

Goal state before:
pp: case nil
α : Type u
h : [] ≠ []
⊢ drop ([].length - 1) [] = [[].getLast h]

Tactic:
aesop

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ |1 / a| = 1 / |a|

Tactic:
rw [abs_div, abs_one]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
⊢ |q - r| * ↑n * max |q| |r| ^ (n - 1) < ε

Tactic:
obtain h | h := (abs_nonneg (q - r)).eq_or_lt

Goal state after:
case inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 = |q - r|
⊢ |q - r| * ↑n * max |q| |r| ^ (n - 1) < ε

case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q - r| * ↑n * max |q| |r| ^ (n - 1) < ε
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
o₁ o₂ : Option α
⊢ o₁.toList ~ o₂.toList ↔ o₁ = o₂

Tactic:
refine ⟨fun p => ?_, fun e => e ▸ Perm.refl _⟩
  rcases o₁ with - | a <;> rcases o₂ with - | b; · rfl
  · cases p.length_eq
  · cases p.length_eq
  · exact Option.mem_toList.1 (p.symm.subset <| by simp)

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

Goal state before:
pp: α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l).flatten.head? = l.head?

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
  induction l <;> simp [replicate]

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

Goal state before:
pp: case mp.cons
α : Type u
l : List α
a : α
a✝ : l <+ []
⊢ l = [] ∨ l = [a]

Tactic:
aesop

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

Goal state before:
pp: case mp.cons_cons
α : Type u
a : α
l₁✝ : List α
a✝ : l₁✝ <+ []
⊢ a :: l₁✝ = [] ∨ a :: l₁✝ = [a]

Tactic:
aesop

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

Goal state before:
pp: case mpr.inl
α : Type u
l : List α
a : α
h✝ : l = []
⊢ l <+ [a]

Tactic:
aesop

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

Goal state before:
pp: case mpr.inr
α : Type u
l : List α
a : α
h✝ : l = [a]
⊢ l <+ [a]

Tactic:
aesop

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
r : ℤ
hr : r = 0
x : M
hx : x ≠ 0
l : NF M
⊢ ((r, x) ::ᵣ l).eval = l.eval

Tactic:
simp [hr, zpow'_zero_of_ne_zero hx]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β → β
b : β
x : α
xs : List α
⊢ foldr f b (xs ++ [x]) = foldr f (f x b) xs

Tactic:
by
  simp only [List.foldr_append, List.foldr]

Goal state after:
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
n : ℕ
⊢ q ^ n = mkRat (q.num ^ n) (q.den ^ n)

Tactic:
rw [pow_def, mk_eq_mkRat]

Goal state after: