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

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

Tactic:
simpa using zpow_sub₀ ha n 1

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

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

Goal state after:
Module: Mathlib.Order.MinMax

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
h : a ≤ b
⊢ f (max a b) = max (f a) (f b)

Tactic:
simp only [max_eq_right, max_eq_left, hf ha hb, hf hb ha, h]

Goal state after:
Module: Mathlib.Order.MinMax

Goal state before:
pp: case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
h : b ≤ a
⊢ f (max a b) = max (f a) (f b)

Tactic:
simp only [max_eq_right, max_eq_left, hf ha hb, hf hb ha, h]

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

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a ≤ c * b ↔ a ≤ c * b
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:
inv_mul_cancel_right

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ c * b ≤ a ↔ c * b ≤ a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
inv_mul_cancel_right

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ b ≤ a ↔ b ≤ a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
inv_mul_cancel_right

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a < c * b ↔ a < c * b
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:
inv_mul_cancel_right

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ c * b < a ↔ c * b < a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
inv_mul_cancel_right

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ b < a ↔ b < a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
inv_mul_cancel_right

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
a b c d : α
inst✝ : MulRightMono α
⊢ d * a ≤ c * b ↔ d * a ≤ c * b
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 α
⊢ d * (a * b⁻¹ * b) < c * b ↔ d * a < c * b

Tactic:
inv_mul_cancel_right

Goal state after:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b c d : α
inst✝ : MulRightStrictMono α
⊢ d * a < c * b ↔ d * a < c * b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
inv_mul_cancel_right

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
inv_mul_cancel_right

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a * b ≤ c ↔ a * b ≤ c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
inv_mul_cancel_right

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a ≤ b * c ↔ a ≤ b * c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
inv_mul_cancel_right

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ a < b ↔ a < b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
inv_mul_cancel_right

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a * b < c ↔ a * b < c
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
inv_mul_cancel_right

Goal state after:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a < b * c ↔ a < b * c
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:
simp only [le_antisymm_iff, pow_le_one_iff_of_nonneg ha hn, one_le_pow_iff_of_nonneg ha hn]

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
hb : 0 < b
⊢ 0 < a / b

Tactic:
by
  rw [div_eq_mul_inv]; exact mul_pos ha (inv_pos.2 hb)

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℤ
h : -x < ↑n
⊢ ↑(-n) < x

Tactic:
rw [Int.cast_neg]

Goal state after:
R : Type u_1
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℤ
h : -x < ↑n
⊢ -↑n < x
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a * b * (a ⊓ b)⁻¹ * (a ⊓ b) = a * b

Tactic:
inv_mul_cancel_right

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a * b = a * b
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ |a⁻¹ ^ n|ₘ = a⁻¹ ^ n

Tactic:
mabs_of_one_le

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ a⁻¹ ^ n = a⁻¹ ^ n

case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ 1 ≤ a⁻¹ ^ n
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

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

Tactic:
mabs_of_one_le

Goal state after:
case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ a / b = a / b

case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ 1 ≤ a / b
Module: Mathlib.Algebra.Group.WithOne.Defs

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

Tactic:
simp_rw [← coe_mul, mul_assoc]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ Function.Injective fun x ↦ x - b

Tactic:
by
  simpa [sub_eq_add_neg] using add_left_injective_of_ne_top (-b) (by simpa)

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h1 : c ≤ a
h2 : c ≤ b
⊢ a - c = b - c ↔ a = b

Tactic:
simp_rw [le_antisymm_iff, tsub_le_tsub_iff_right h1, tsub_le_tsub_iff_right h2]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a - b = a - min a b

Tactic:
by
  rcases le_total a b with h | h
  · rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
  · rw [min_eq_right h]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
⊢ a - b < a

Tactic:
refine tsub_le_self.lt_of_ne fun h => ?_
  rw [← h, tsub_pos_iff_lt] at h₁
  exact h₂.not_ge (ha.add_le_iff_nonpos_left.1 <| add_le_of_le_tsub_left_of_le h₁.le h.ge)

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

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑(a✝¹ * a✝) ≤ ↑(a✝¹ * c)

Tactic:
coe_le_coe

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ a✝¹ * a✝ ≤ a✝¹ * c
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.zero.coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ : α
hbc : 0 ≤ ↑a✝
⊢ ↑a✝¹ ≤ ↑(a✝¹ + a✝)

Tactic:
coe_le_coe

Goal state after:
case coe.zero.coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ : α
hbc : 0 ≤ ↑a✝
⊢ a✝¹ ≤ a✝¹ + a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑(a✝¹ + a✝) ≤ ↑(a✝¹ + c)

Tactic:
coe_le_coe

Goal state after:
case coe.coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ a✝¹ + a✝ ≤ a✝¹ + c
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
elt : ℤ
Helt : P elt
⊢ P (- -elt)

Tactic:
rw [neg_neg]

Goal state after:
P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
elt : ℤ
Helt : P elt
⊢ P elt
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
ceil : α → ℤ
gc_ceil_coe : GaloisConnection ceil Int.cast
a : ℤ
z : α
⊢ ↑a ≤ z ↔ a ≤ (fun a ↦ -ceil (-a)) z

Tactic:
by rw [le_neg, gc_ceil_coe, Int.cast_neg, neg_le_neg_iff]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a + 1 / b = (a + b) / (a * b)

Tactic:
rw [(Commute.one_right a).div_add_div hab ha hb, one_mul, mul_one, add_comm]

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ k ≠ 0

Tactic:
simpa using h₀

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
n : ℕ
⊢ a ^ n = -1 ↔ a = -1 ∧ Odd n

Tactic:
simpa using pow_eq_neg_pow_iff (R := R) one_ne_zero

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
β : Type u_4
inst✝ : Preorder β
s : Set (α × β)
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
x : α × β
hx : x ∈ s
y : α × β
hy : y ∈ s
⊢ ∃ b ∈ s, (x.1, y.2) ≤ b

Tactic:
obtain ⟨z, hz, hxz, hyz⟩ := hs _ hx _ hy

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
β : Type u_4
inst✝ : Preorder β
s : Set (α × β)
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
x : α × β
hx : x ∈ s
y : α × β
hy : y ∈ s
z : α × β
hz : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ b ∈ s, (x.1, y.2) ≤ b
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α × Set β
⊢ (fun s ↦ (Sum.inl ⁻¹' s, Sum.inr ⁻¹' s)) ((fun s ↦ Sum.inl '' s.1 ∪ Sum.inr '' s.2) s) = s

Tactic:
by
    simp [preimage_image_eq _ Sum.inl_injective, preimage_image_eq _ Sum.inr_injective]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
s : Set α
⊢ upperBounds (insert a s) = Ici a ∩ upperBounds s

Tactic:
rw [insert_eq, upperBounds_union, upperBounds_singleton]

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
x x' : α
h : x = x'
⊢ x = termg 1 x' 0

Tactic:
by
  simp [termg, h]

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
n : ℤ
⊢ ¬n = 0 → 0 ^ n = 0

Tactic:
intro hn

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
n : ℤ
hn : ¬n = 0
⊢ 0 ^ n = 0
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ zpow' a ↑n = a ^ n

Tactic:
rw [zpow'_of_ne_zero_right]
  · simp
  exact_mod_cast hn

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
⊢ (L.set n a).prod = L.prod * if hn : n < L.length then L[n]⁻¹ * a else 1

Tactic:
by
  refine (prod_set L n a).trans ?_
  split_ifs with hn
  · rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ←
      mul_assoc (take n L).prod, prod_take_mul_prod_drop, mul_comm a, mul_assoc]
  · simp (disch := grind) [take_of_length_le, drop_eq_nil_of_le]

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

Goal state before:
pp: x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x / (d /. x) = n /. d

Tactic:
by
  rw [div_eq_mul_inv, inv_divInt, divInt_mul_divInt_cancel hx]

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Basic

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

Tactic:
inv_mul_cancel_right

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ b = b
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:
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]

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

case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ Nat.rawCast 1 * a = a

Tactic:
by simp [Nat.rawCast]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a * Nat.rawCast 1 = a

Tactic:
by simp [Nat.rawCast]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
⊢ ⨆ i ∈ s, a = a

Tactic:
by
  have : Nonempty s := Set.nonempty_coe_sort.mpr hs
  rw [← iSup_subtype'', iSup_const]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ ⋃ i, ⋃ j, s i j ⊆ t ↔ ∀ (i : ι) (j : κ i), s i j ⊆ t

Tactic:
iUnion_subset_iff

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ Iic (sInf s) = ⋂ a ∈ s, Iic a

Tactic:
by rw [sInf_eq_iInf, Iic_iInf₂]

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

Goal state before:
pp: β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
classical
  constructor
  · change ite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · intro _ _
      exact le_top
    · rintro (⟨⟩ | a) ha
      · contradiction
      apply coe_le_coe.2
      exact le_csSup h₂ ha
    · intro _ _
      exact le_top
  · change ite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · rintro (⟨⟩ | a) ha
      · exact le_rfl
      · exact False.elim (not_top_le_coe a (ha h₁))
    · rintro (⟨⟩ | b) hb
      · exact le_top
      refine coe_le_coe.2 (csSup_le ?_ ?_)
      · rcases hs with ⟨⟨⟩ | b, hb⟩
        · exact absurd hb h₁
        · exact ⟨b, hb⟩
      · intro a ha
        exact coe_le_coe.1 (hb ha)
    · rintro (⟨⟩ | b) hb
      · exact le_rfl
      · exfalso
        apply h₂
        use b
        intro a ha
        exact coe_le_coe.1 (hb ha)

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
a : α
inst✝ : Std.Symm r
ha : ¬a ∈ s
⊢ (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ (b : α), b ∈ s → r a b

Tactic:
simp only [pairwise_insert_of_notMem ha, Std.Symm.iff a, and_self_iff]

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
⊢ (s.PairwiseDisjoint fun a ↦ f a '' t) ↔ InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)

Tactic:
by
  refine ⟨fun hs x hx y hy (h : f _ _ = _) => ?_, fun hs x hx y hy h => ?_⟩
  · suffices x.1 = y.1 by exact Prod.ext this (hf _ hx.1 <| h.trans <| by rw [this])
    refine hs.elim hx.1 hy.1 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.2, ?_⟩)
    rw [h]
    exact mem_image_of_mem _ hy.2
  · refine disjoint_iff_inf_le.mpr ?_
    rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩
    exact h (congr_arg Prod.fst <| hs (mk_mem_prod hx ha) (mk_mem_prod hy hb) hab)

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
ht : t.Nonempty
h_bdd : BddBelow t
⊢ sInf (Subtype.val '' t) ∈ s

Tactic:
by
  obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
  obtain ⟨B, hB⟩ : ∃ B, B ∈ lowerBounds t := h_bdd
  refine hs.out B.2 c.2 ⟨?_, ?_⟩
  · exact (Subtype.mono_coe (· ∈ s)).le_csInf_image ⟨c, hct⟩ hB
  · exact (Subtype.mono_coe (· ∈ s)).csInf_image_le hct ⟨B, hB⟩

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

Goal state before:
pp: case ha
α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible ↑den
⊢ 0 ≤ ↑num

pp: case hb
α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible ↑den
⊢ 0 ≤ ⅟↑den

Tactic:
· exact Nat.cast_nonneg' num

Goal state after:
case hb
α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num den : ℕ
ha1 : Invertible ↑den
⊢ 0 ≤ ⅟↑den
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹.mul db ≤ num✝.mul da) = true
h✝ : ↑(num✝¹.mul db) ≤ ↑(num✝.mul da)
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h : ↑num✝¹ * ⅟↑da ≤ ⅟↑db * ↑num✝
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
rwa [Nat.commute_cast] at h

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * db < num✝ * da) = true
h✝ : ↑(num✝¹ * db) < ↑(num✝ * da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ↑num✝¹ * ⅟↑da < ⅟↑db * ↑num✝
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
rwa [Nat.commute_cast] at h

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : a ≠ 1
x : ι
hx : x ∈ {i}
⊢ mulSingle i a x ≠ 1

Tactic:
hx,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : a ≠ 1
x : ι
hx : x ∈ {i}
⊢ mulSingle i a i ≠ 1
Module: Mathlib.Data.Int.Cast.Field

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
m n : ℤ
n_dvd : n ∣ m
hn : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
rcases n_dvd with ⟨k, rfl⟩

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
hn : ↑n ≠ 0
k : ℤ
⊢ ↑(n * k / n) = ↑(n * k) / ↑n
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case mp
n : ℕ
h : n ! = 1
⊢ ¬1 < 1

Tactic:
apply lt_irrefl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ a⁺ᵐ = if 1 ≤ a then a else 1

Tactic:
rw [oneLePart_def, ← maxDefault, ← sup_eq_maxDefault]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ max a 1 = (fun x1 x2 ↦ max x1 x2) 1 a
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
hi : 3 ≤ n
this : 0 < n
hn : 1 < n.pred
⊢ n < n !

Tactic:
rw [← succ_pred_eq_of_pos ‹0 < n›, factorial_succ]

Goal state after:
n : ℕ
hi : 3 ≤ n
this : 0 < n
hn : 1 < n.pred
⊢ n.pred.succ < (n.pred + 1) * n.pred !
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case succ
k m : ℕ
h : k ≤ m
n : ℕ
ih : k.descFactorial n ≤ m.descFactorial n
⊢ k.descFactorial (n + 1) ≤ m.descFactorial (n + 1)

Tactic:
rw [descFactorial_succ, descFactorial_succ]

Goal state after:
case succ
k m : ℕ
h : k ≤ m
n : ℕ
ih : k.descFactorial n ≤ m.descFactorial n
⊢ (k - n) * k.descFactorial n ≤ (m - n) * m.descFactorial n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a + b⌋ - 1 ≤ a + b - 1

Tactic:
sub_le_sub_iff_right

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a + b⌋ ≤ a + b
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ a - b ≤ a ∧ a < a - b + 1

Tactic:
constructor <;> simpa [sub_eq_add_neg, add_assoc]

Goal state after: