mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c

Tactic:
rw [← (hd.mul hb).mul_right_inj, ← mul_assoc, mul_assoc d, hb.mul_inv_cancel, mul_one,
    ← mul_assoc, mul_assoc d, hbd.symm.left_comm, hd.mul_inv_cancel, mul_one]

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

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

Tactic:
div_mul_cancel_left₀ h,

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : a ≠ 0
⊢ b⁻¹ = 1 / b
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : -↑(a✝ + 1) = 0
⊢ -[a✝+1] = 0

Tactic:
neg_eq_zero,

Goal state after:
case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑(a✝ + 1) = 0
⊢ -[a✝+1] = 0
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:
zero_smul

Goal state after:
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 = 0
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case zero
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
⊢ 0 = 0 • b

Tactic:
zero_smul

Goal state after:
case zero
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
⊢ 0 = 0
Module: Mathlib.Algebra.Ring.Parity

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

Tactic:
induction k with | zero => simpa | 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✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n✝ : ℤ
n : ℕ
h✝ : n✝ = ↑n ∨ n✝ = -↑n
⊢ (-1) ^ n✝ = if Even n✝ then 1 else -1

Tactic:
aesop (add safe (by rw [neg_one_pow_eq_ite]))

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

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a - c < b
⊢ a < b + c

Tactic:
rw [lt_iff_le_and_ne, ← tsub_le_iff_right]

Goal state after:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a - c < b
⊢ a - c ≤ b ∧ a ≠ b + c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a : M₀
m : ℕ
inst✝¹ : PosMulStrictMono M₀
inst✝ : ZeroLEOneClass M₀
h : 1 < a
hm : 1 < m
⊢ a < a ^ m

Tactic:
by
  simpa only [pow_one] using pow_lt_pow_right₀ h hm

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

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ a * b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
by
  rw [← neg_nonneg, ← neg_mul, mul_nonneg_iff_pos_imp_nonneg (R := R)]
  simp only [neg_pos, neg_nonneg]

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

Goal state before:
pp: case refine_1
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
a b : X
⊢ f a ≤ f b ↔ b ≤ a

Tactic:
rw [hf.le_iff_ge]

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

Goal state before:

Tactic:
|(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ =
        (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ := by
        rw [sup_div_inf_eq_mabs_div]
    _ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) := by
        rw [sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)]
    _ = (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) := by
        rw [← sup_inf_right, ← inf_sup_right, sup_assoc, sup_comm c (a ⊔ c), sup_right_idem,
          sup_assoc, inf_assoc, inf_comm c (a ⊓ c), inf_right_idem, inf_assoc]
    _ = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) := by rw [div_mul_div_comm]
    _ = (b ⊔ a) * c / ((b ⊓ a) * c) := by
        rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
    _ = (b ⊔ a) / (b ⊓ a) := by
        rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
    _ = |a / b|ₘ := by rw [sup_div_inf_eq_mabs_div]

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

Goal state before:
pp: R : Type u_2
S : Type u_3
F : Type u_4
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : FunLike F R S
n : ℕ
inst✝¹ : NeZero ↑n
inst✝ : RingHomClass F R S
f : F
hf : Function.Injective ⇑f
h : ↑n = 0
⊢ f ↑n = f 0

Tactic:
simpa only [map_natCast, map_zero f]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ a ^ m = 1 ∧ a ^ n = 1

Tactic:
by
    constructor
    · rw [← Nat.mul_div_cancel' (m.gcd_dvd_left n), pow_mul, hmn, one_pow]
    · rw [← Nat.mul_div_cancel' (m.gcd_dvd_right n), pow_mul, hmn, one_pow]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤

Tactic:
by simp [lt_top_iff_ne_top]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ -(a + b) + (a + b) = 0

Tactic:
by simp [neg_add_cancel_of_ne_top, *]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
h : a + b = 0
ha : a ≠ ⊤
⊢ -a + a = 0

Tactic:
by simp [neg_add_cancel_of_ne_top, *]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ 0 < -a ↔ a < 0 ∨ a = ⊤

Tactic:
simpa using sub_pos (a := 0) (b := a)

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h✝ : b ≤ a
h : b ≤ b + ⋯.choose
this : a = b + ⋯.choose
⊢ ⋯.choose ≤ c ↔ a ≤ c + b

Tactic:
conv_rhs => rw [this, add_comm]

Goal state after:
case pos
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h✝ : b ≤ a
h : b ≤ b + ⋯.choose
this : a = b + ⋯.choose
⊢ ⋯.choose ≤ c ↔ ⋯.choose + b ≤ c + b
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ 0 ≤ ⌈a⌉

Tactic:
rw [← FloorRing.intCast_strictMono.le_iff_le (β := α), Int.cast_zero]

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ 0 ≤ ↑⌈a⌉
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : a ≤ 0
⊢ ⌊a⌋ ≤ 0

Tactic:
rw [← FloorRing.intCast_strictMono.le_iff_le (β := α), Int.cast_zero]

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
ha : a ≤ 0
⊢ ↑⌊a⌋ ≤ 0
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

Tactic:
by
  obtain ha | ha := le_total a 0
  · rw [floor_of_nonpos ha]
    exact
      iff_of_false (Nat.pos_of_ne_zero hn).not_ge
        (not_le_of_gt <| ha.trans_lt <| cast_pos.2 <| Nat.pos_of_ne_zero hn)
  · exact le_floor_iff ha

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.univ.pi d
b : (i : ι) → α i
hb : b ∈ Set.univ.pi d
⊢ ∃ z ∈ Set.univ.pi d, (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧ (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) b z

Tactic:
choose f hfd haf hbf using fun i => hd i (a i) (ha i trivial) (b i) (hb i trivial)

Goal state after:
ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.univ.pi d
b : (i : ι) → α i
hb : b ∈ Set.univ.pi d
f : (i : ι) → α i
hfd : ∀ (i : ι), f i ∈ d i
haf : ∀ (i : ι), r i (a i) (f i)
hbf : ∀ (i : ι), r i (b i) (f i)
⊢ ∃ z ∈ Set.univ.pi d, (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧ (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) b z
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
x y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), x < ↑z → y ≤ ↑z) ↔ y ≤ x

Tactic:
by
  cases x <;> cases y <;> simp [exists_lt, forall_gt_imp_ge_iff_le_of_dense]

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

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

Tactic:
← AddUnits.ext_iff,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ (-y).mulLeft ↑(-x) = y.mulLeft ↑x
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: a b c d : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hd : IsUnit d
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c

Tactic:
by
  rw [isUnit_iff] at ha hb hc hd
  lia

Goal state after:
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
⊢ image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t'

Tactic:
rw [← image2_swap, image2_union_left, image2_swap f, image2_swap f]

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ WellFoundedGT (Antisymmetrization α fun x1 x2 ↦ x1 ≤ x2) ↔ WellFoundedGT α

Tactic:
simp_rw [isWellFounded_iff]

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ (WellFounded fun x1 x2 ↦ x2 < x1) ↔ WellFounded fun x1 x2 ↦ x2 < x1
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a ≤ b
⊢ Icc a b = Ioc a b

Tactic:
by rw [Icc_eq_empty h, Ioc_eq_empty (mt le_of_lt h)]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
⊢ c ≤ d

Tactic:
by_contra contra

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
contra : ¬c ≤ d
⊢ False
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case neg
γ : Type u_3
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ∀ j ∈ upperBounds (Iio i), i ≤ j
⊢ ∃ j, IsLUB (Iio i) j

Tactic:
refine ⟨i, fun j hj => le_of_lt hj, ?_⟩

Goal state after:
case neg
γ : Type u_3
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ∀ j ∈ upperBounds (Iio i), i ≤ j
⊢ i ∈ lowerBounds (upperBounds (Iio i))
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
⊢ a < (a + b) / 2 ↔ a < b

Tactic:
by simp [lt_div_iff₀, mul_two]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc

Tactic:
have h₁ := congr_arg (Nat.cast (R := α)) h₁

Goal state after:
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑(na * nb) = ↑(k * nc)
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
h : l₁ ~ l₂.insertIdx n a
⊢ False

Tactic:
h.length_eq

Goal state after:
case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : (l₂.insertIdx n a).length < n
hn₂ : l₂.length ≥ n
h : l₁ ~ l₂.insertIdx n a
⊢ False
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl.intro
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
hn : n < l₂.length
hnm : l₂[n] = l₁[m]
⊢ l₁ ~ l₁[m] :: l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
← hnm,

Goal state after:
case inl.intro
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m < l₁.length
hn : n < l₂.length
hnm : l₂[n] = l₁[m]
⊢ l₁ ~ l₂[n] :: l₂.eraseIdx n ↔ l₁ ~ l₂
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case swap.cons
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
a₁ a₂ : α
h₂₃ : List α
b✝ : β
l₂✝ : List β
h₁ : r a₁ b✝
hr₂₃ : Forall₂ r (a₂ :: h₂₃) l₂✝
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) (b✝ :: l₂✝)

Tactic:
obtain - | ⟨h₂, h₁₂⟩ := hr₂₃

Goal state after:
case swap.cons.cons
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
a₁ a₂ : α
h₂₃ : List α
b✝¹ : β
h₁ : r a₁ b✝¹
b✝ : β
l₂✝ : List β
h₂ : r a₂ b✝
h₁₂ : Forall₂ r h₂₃ l₂✝
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) (b✝¹ :: b✝ :: l₂✝)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hl✝ : l ≠ []
x : M
xs : List M
hl : x :: xs ≠ []
⊢ (map (⇑f) (x :: xs)).prod = f (x :: xs).prod

Tactic:
induction xs generalizing x <;> simp_all

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl✝ : l ≠ []
x : ι
xs : List ι
hl : x :: xs ≠ []
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) (x :: xs)).prod = f (map f₁ (x :: xs)).prod (map f₂ (x :: xs)).prod

Tactic:
induction xs generalizing x <;> simp_all

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℕ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ l.eval ^ r = zpow' l.eval ↑r

Tactic:
zpow'_ofNat _ hr

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℕ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ l.eval ^ r = l.eval ^ r
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mp
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ → x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Tactic:
simp only [append_eq_append_iff, cons_eq_append_iff, cons_eq_cons]

Goal state after:
case mp
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ ((∃ as, x₂ = x₁ ++ as ∧ (as = [] ∧ a₂ = a₁ ∧ z₂ = z₁ ∨ ∃ as', as = a₁ :: as' ∧ z₁ = as' ++ a₂ :: z₂)) ∨
      ∃ bs, x₁ = x₂ ++ bs ∧ (bs = [] ∧ a₁ = a₂ ∧ z₁ = z₂ ∨ ∃ as', bs = a₂ :: as' ∧ z₂ = as' ++ a₁ :: z₁)) →
    x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂
Module: Mathlib.Data.NNRat.Defs

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

Tactic:
by simp [num, Int.natAbs_pow]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ DvdNotUnit a b

Tactic:
by
  constructor
  · rintro rfl
    exact hnd (dvd_zero _)
  · rcases hd with ⟨c, rfl⟩
    refine ⟨c, ?_, rfl⟩
    rintro ⟨u, rfl⟩
    simp at hnd

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x (y * z)
⊢ IsRelPrime x y

Tactic:
isRelPrime_comm

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime (y * z) x
⊢ IsRelPrime y x
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a⁻¹ * b * a = b

Tactic:
h.inv_left.eq,

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ b * a⁻¹ * a = b
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime z y ↔ IsRelPrime y z

Tactic:
isRelPrime_comm

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y z ↔ IsRelPrime y z
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime x y
H2 : IsRelPrime x z
⊢ IsRelPrime x (y * z)

Tactic:
isRelPrime_comm

Goal state after:
α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime y x
H2 : IsRelPrime z x
⊢ IsRelPrime (y * z) x
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q + r) = ↑q + ↑r

Tactic:
by
  rw [add_def', cast_mkRat_of_ne_zero, cast_def, cast_def, mul_comm r.num,
    (Nat.cast_commute _ _).div_add_div (Nat.commute_cast _ _) hq hr]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hq hr

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

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionSemiring α
inst✝¹ : DivisionSemiring β
inst✝ : RingHomClass F α β
f : F
q : ℚ≥0
⊢ f ↑q = ↑q

Tactic:
by simp_rw [NNRat.cast_def, map_div₀, map_natCast]

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
n k e : α
h2 : e ≠ 0
h3 : n * e = k
⊢ k * e⁻¹ = n

Tactic:
by rw [← div_eq_mul_inv, ← h3, mul_div_cancel_right₀ _ h2]

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < ad * bd

pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd

Tactic:
· exact mul_pos had hbd

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
⊢ ⨅ i, ⨅ (_ : i > 0), f i = ⨅ i, f (i + 1)

Tactic:
rw [← iInf_range, Nat.range_succ]
  simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift ι → α
⊢ sSup (range fun i ↦ f i) = sSup (range fun i ↦ f { down := i })

Tactic:
congr with x

Goal state after:
α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift ι → α
x : α
⊢ (x ∈ range fun i ↦ f i) ↔ x ∈ range fun i ↦ f { down := i }
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : SupSet α
p : Prop
f₁ f₂ : p → α
pq : p ↔ p
f : ∀ (x : p), f₁ ⋯ = f₂ x
⊢ iSup f₁ = iSup f₂

Tactic:
congr with x

Goal state after:
α : Type u_1
inst✝ : SupSet α
p : Prop
f₁ f₂ : p → α
pq : p ↔ p
f : ∀ (x : p), f₁ ⋯ = f₂ x
x : p
⊢ f₁ x = f₂ x
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
c : α
⊢ ⨆ x, f x ≤ c ↔ ⨆ i, ⨆ j, f (i, j) ≤ c

Tactic:
simp only [iSup_le_iff, Prod.forall]

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

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∃ i, f i ≠ ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'

Tactic:
rw [hi]

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∃ i, f i ≠ ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', ⊥ ≤ f ↑i'
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst✝ : (i : α) → CompleteLattice (β i)
x✝¹ : Set ((i : α) → β i)
x✝ : α
⊢ IsLUB (eval x✝ '' x✝¹) (sSup x✝¹ x✝)

Tactic:
sSup_apply_eq_sSup_image

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst✝ : (i : α) → CompleteLattice (β i)
x✝¹ : Set ((i : α) → β i)
x✝ : α
⊢ IsLUB (eval x✝ '' x✝¹) (sSup (eval x✝ '' x✝¹))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → ConditionallyCompleteLattice (α i)
x✝¹ : Set ((i : ι) → α i)
hn : x✝¹.Nonempty
hb : BddAbove x✝¹
x✝ : ι
⊢ IsLUB (eval x✝ '' x✝¹) (sSup x✝¹ x✝)

Tactic:
sSup_apply_eq_sSup_image

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → ConditionallyCompleteLattice (α i)
x✝¹ : Set ((i : ι) → α i)
hn : x✝¹.Nonempty
hb : BddAbove x✝¹
x✝ : ι
⊢ IsLUB (eval x✝ '' x✝¹) (sSup (eval x✝ '' x✝¹))
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inl.inl.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

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

Goal state before:
pp: case inl.inr.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

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

Goal state before:
pp: case inr.inl.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

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

Goal state before:
pp: case inr.inr.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

Goal state after: