mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.Abs

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

Tactic:
rw [mabs_of_one_le ha, mabs_of_one_le (one_le_pow_of_one_le' ha n)]

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

Goal state before:
pp: case inr.inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : a * b = a⁻¹ * b
ab : 1 < a * b
⊢ b ≤ 1

Tactic:
mul_left_inj

Goal state after:
case inr.inl.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : a = a⁻¹
ab : 1 < a * b
⊢ b ≤ 1
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
a : α
k : ℤ
⊢ (-a) ^ (2 * k + 1) = -a ^ (2 * k + 1)

Tactic:
cases k with
  | ofNat k =>
    rw [Int.ofNat_eq_natCast]
    norm_cast
    simp [pow_add]
  | negSucc k =>
    simp_rw [Int.negSucc_eq, show 2 * -(↑k + 1) + (1 : ℤ) = - (1 + k*2) by grind, _root_.zpow_neg]
    norm_cast
    simp [pow_add]

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

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
⊢ ∀ (a_1 : α), b = a * a_1 ∧ a ≠ b ↔ a_1 > 1 ∧ b = a * a_1

Tactic:
intro c

Goal state after:
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
c : α
⊢ b = a * c ∧ a ≠ b ↔ c > 1 ∧ b = a * c
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: α : Type u_1
inst✝² : AddMonoid α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedAdd α
a : WithBot α
⊢ a < 0 ↔ a = ⊥

Tactic:
induction a

Goal state after:
case bot
α : Type u_1
inst✝² : AddMonoid α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedAdd α
⊢ ⊥ < 0 ↔ ⊥ = ⊥

case coe
α : Type u_1
inst✝² : AddMonoid α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedAdd α
a✝ : α
⊢ ↑a✝ < 0 ↔ ↑a✝ = ⊥
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ ((∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a) ↔ ∀ (b : β), ∃ a, f a = b

Tactic:
refine ⟨fun h b ↦ ?_, fun h ↦ ⟨⟨0, by simp⟩, fun b ↦ ?_⟩⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
⊢ ∃ a, f a = b

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : ∀ (b : β), ∃ a, f a = b
b : β
⊢ ∃ a, (map' f) a = ↑b
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: G : Type u_5
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
n : ℤ
⊢ (x ^ n).log = n • x.log

Tactic:
by cases n <;> simp [log_pow, log_inv]

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 c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a - b ≤ a - c ↔ c ≤ b

Tactic:
refine ⟨?_, fun h => tsub_le_tsub_left h a⟩

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a - b ≤ a - c → c ≤ b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : WithTop α
⊢ map (⇑f) (a + b) = map (⇑f) a + map (⇑f) b

Tactic:
induction a

Goal state after:
case top
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
⊢ map (⇑f) (⊤ + b) = map ⇑f ⊤ + map (⇑f) b

case coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
a✝ : α
⊢ map (⇑f) (↑a✝ + b) = map ⇑f ↑a✝ + map (⇑f) b
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : WithBot α
b : α
h : a ≠ ⊥
⊢ a.unbot h = b ↔ a = ↑b

Tactic:
induction a

Goal state after:
case bot
α : Type u_1
b : α
h : ⊥ ≠ ⊥
⊢ ⊥.unbot h = b ↔ ⊥ = ↑b

case coe
α : Type u_1
b a✝ : α
h : ↑a✝ ≠ ⊥
⊢ (↑a✝).unbot h = b ↔ ↑a✝ = ↑b
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
b : α
h : ⊥ ≠ ⊥
⊢ ⊥.unbot h = b ↔ ⊥ = ↑b

Tactic:
simpa using h rfl

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
a : α
h : ⊥ ≠ ⊥
⊢ a = ⊥.unbot h ↔ ↑a = ⊥

Tactic:
simpa using h rfl

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ ((StrictMono fun a ↦ map f ↑a) ∧ ∀ (x : α), map f ⊥ < map f ↑x) ↔ StrictMono f

Tactic:
by simp [StrictMono, bot_lt_coe]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
⊢ a + c ≤ b + c ↔ a ≤ b

Tactic:
induction a

Goal state after:
case bot
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
⊢ ⊥ + c ≤ b + c ↔ ⊥ ≤ b

case coe
α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a✝ : WithTop α
⊢ ↑a✝ + c ≤ b + c ↔ ↑a✝ ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
induction a

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b✝ : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
b c : WithZero α
hbc : b ≤ c
⊢ 0 * b ≤ 0 * c

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a b c : WithZero α
hbc : b ≤ c
⊢ a + b ≤ a + c

Tactic:
induction a

Goal state after:
case zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
⊢ 0 + b ≤ 0 + c

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a✝ b✝ : α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a b : WithZero α
⊢ a ≤ b → ∃ c, b = a + c

Tactic:
induction a

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b✝ : α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
b : WithZero α
⊢ 0 ≤ b → ∃ c, b = 0 + c

case coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b✝ : α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
b : WithZero α
a✝ : α
⊢ ↑a✝ ≤ b → ∃ c, b = ↑a✝ + c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : WithBot α
⊢ map (⇑f) (a + b) = map (⇑f) a + map (⇑f) b

Tactic:
induction a

Goal state after:
case bot
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithBot α
⊢ map (⇑f) (⊥ + b) = map ⇑f ⊥ + map (⇑f) b

case coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithBot α
a✝ : α
⊢ map (⇑f) (↑a✝ + b) = map ⇑f ↑a✝ + map (⇑f) b
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
a b c : WithZero α
h : a * b < a * c
this : a * c ≠ 0
⊢ b < c

Tactic:
induction a

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
b c : WithZero α
h : 0 * b < 0 * c
this : 0 * c ≠ 0
⊢ b < c

case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
b c : WithZero α
a✝ : α
h : ↑a✝ * b < ↑a✝ * c
this : ↑a✝ * c ≠ 0
⊢ b < c
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ (fun a ↦ ⌈a⌉.toNat) a ≤ n ↔ a ≤ ↑n

Tactic:
Int.toNat_le,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ ⌈a⌉ ≤ ↑n ↔ a ≤ ↑n
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
zero_le : ∀ (a : α), 0 ≤ a
this : AddLeftMono (WithZero α)
⊢ ∀ (a b : WithZero α), a ≤ b → ∀ (c : WithZero α), c + a ≤ c + b

Tactic:
by simpa [add_comm] using fun _ _ ↦ add_le_add_left

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 : 1 * f (t * 0) = f t * f 0
⊢ f t = 1

Tactic:
mul_zero

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.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
f : F
inst✝ : DecompositionMonoid β
a b c : α
h : f a ∣ f (b * c)
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
map_mul

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
f : F
inst✝ : DecompositionMonoid β
a b c : α
h : f a ∣ f b * f c
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Add α
inst✝¹ : Semigroup α
inst✝ : LeftDistribClass α
a b c : α
h₁ : a ∣ b
h₂ : a ∣ c
d : α
hd : b = a * d
e : α
he : c = a * e
⊢ a * (d + e) = b + c

Tactic:
simp [left_distrib, hd, he]

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ (WellFounded fun x1 x2 ↦ x1 < x2) ↔ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
wellFounded_antisymmetrization_iff

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : PartialOrder α
a b c : α
⊢ a = c ∧ b = c → Icc a b = {c}

Tactic:
rintro ⟨rfl, rfl⟩
    exact Icc_self _

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
⊢ IsGLB s a ↔ IsGLB s b

Tactic:
by
  simp [isGLB_iff_le_iff, h.le_congr_right]

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

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝² : Semiring A
inst✝¹ : PartialOrder A
inst✝ : IsOrderedRing A
h : NormNum.IsNat e n
⊢ 0 ≤ e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]
  exact Nat.cast_nonneg n

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 * db + nb * da = k * nc
h₂ : da * db = k * dc
this : Invertible ↑(da * db)
⊢ IsNNRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc

Tactic:
have := invertibleOfMul' (α := α) h₂

Goal state after:
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * db + nb * da = k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ IsNNRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this : Invertible ↑(da * db)
⊢ IsRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc

Tactic:
have := invertibleOfMul' (α := α) h₂

Goal state after:
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ IsRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc
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)
⊢ IsNNRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc

Tactic:
have := invertibleOfMul' (α := α) 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
⊢ IsNNRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
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)
⊢ IsRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc

Tactic:
have := invertibleOfMul' (α := α) h₂

Goal state after:
α : Type u_1
inst✝ : Ring α
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
⊢ IsRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a / c ≤ b / c ↔ b ≤ a

Tactic:
rw [div_le_iff_of_neg hc, div_mul_cancel₀ _ hc.ne]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
h₁ : l₁.length = l₂.length
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ l₁.zip l₂
⊢ (a✝, b✝) ∈ zipWith Prod.mk l₁ l₂

Tactic:
simpa [zip] using h

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

Goal state before:
pp: case trans
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : ∀ {v : List β}, Forall₂ r l₂✝ v → (Forall₂ r ∘r Perm) l₁✝ v
ih₂ : ∀ {v : List β}, Forall₂ r l₃✝ v → (Forall₂ r ∘r Perm) l₂✝ v
v : List β
huv : Forall₂ r l₃✝ v
lb₂ : List β
hab₂ : Forall₂ r l₂✝ lb₂
h₂₃ : lb₂ ~ v
lb₁ : List β
hab₁ : Forall₂ r l₁✝ lb₁
h₁₂ : lb₁ ~ lb₂
⊢ (Forall₂ r ∘r Perm) l₁✝ v

Tactic:
exact ⟨lb₁, hab₁, Perm.trans h₁₂ h₂₃⟩

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

Goal state before:
pp: case e_tail
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ tail✝¹.length = tail✝.length

Tactic:
simpa using hl

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

Goal state before:
pp: α : Type u
a b : α
l : List α
c : α
hc : c ∈ (b :: l).getLast?
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l

Tactic:
rw [dropLast_cons_cons, cons_append, dropLast_append_getLast? _ hc]

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

Goal state before:
pp: case mpr
α : Type u
l₁ l₂ : List α
h₁ : l₁.length = l₂.length
h₂ : ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩
⊢ l₁ = l₂

Tactic:
exact ext_get h₁ h₂

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

Goal state before:
pp: G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
l : List A
f g : A → G
a : A
⊢ (map (fun x ↦ if x = a then f x else g x) l).prod = (f a / g a) ^ count a l * (map g l).prod

Tactic:
by
  induction l with
  | nil => simp
  | cons x xs ih =>
    simp only [map_cons, prod_cons, count_cons] at ih ⊢
    rw [ih]
    clear ih
    by_cases hx : x = a
    · simp only [hx, ite_true, pow_add, pow_one, div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm,
      mul_inv_cancel_left, beq_self_eq_true]
    · simp only [hx, ite_false, add_zero, mul_assoc, mul_comm (g x) _, beq_iff_eq]

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

Goal state before:
pp: q : ℚ
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ (n₁ * n₂).natAbs.Coprime (d₁ * d₂)

Tactic:
by
      rw [Int.natAbs_mul]; exact (hnd₁.mul_left h₂₁).mul_right (h₁₂.mul_left hnd₂)

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

Goal state before:
pp: case inr
a : ℤ
ha : a ≤ 0
b : ℕ
hb : b ≠ 0
⊢ mkRat a b ≤ 0

Tactic:
exact (mkRat_nonpos_iff a hb).mpr ha

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

Goal state before:
pp: case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ 0 = p.toNNRat * 0

Tactic:
mul_zero

Goal state after:
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ 0 = 0
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q : ℚ≥0
⊢ p ≤ q ↔ p.num * q.den ≤ q.num * p.den

Tactic:
by
  rw [← NNRat.coe_le_coe, Rat.le_iff]; norm_cast

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

Goal state before:
pp: n₁ n₂ : ℤ
d : ℕ
h : d ≠ 0
⊢ mkRat n₁ d + mkRat n₂ d = mkRat (n₁ + n₂) d

Tactic:
mkRat_add_mkRat _ _ h h,

Goal state after:
n₁ n₂ : ℤ
d : ℕ
h : d ≠ 0
⊢ mkRat (n₁ * ↑d + n₂ * ↑d) (d * d) = mkRat (n₁ + n₂) d
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ (Int.negOfNat a).pow b = Int.negOfNat c

Tactic:
rw [← hb, Int.negOfNat_eq, Int.negOfNat_eq, Int.pow_eq, pow_succ, pow_mul, neg_pow_two, ← pow_mul,
    two_mul, pow_add, ← hc, ← h1]
  simp [mul_comm, mul_left_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
f : α → ℕ → α
a : α
an cn ad b b' cd : ℕ
⊢ f = HPow.hPow → IsNNRat a an ad → IsNat b b' → an.pow b' = cn → ad.pow b' = cd → IsNNRat (f a b) cn cd

Tactic:
rintro rfl ⟨_, rfl⟩ ⟨rfl⟩ (rfl : an ^ b = _) (rfl : ad ^ b = _)
  have := invertiblePow (ad:α) b
  rw [← Nat.cast_pow] at this
  use this; simp [invOf_pow, Commute.mul_pow, Nat.cast_commute]

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

Goal state before:
pp: case inl
R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b d : R
hab : a < b
this : MulPosStrictMono R
hcd : 0 < d
⊢ a * 0 < b * d

Tactic:
mul_zero

Goal state after:
case inl
R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b d : R
hab : a < b
this : MulPosStrictMono R
hcd : 0 < d
⊢ 0 < b * d
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α ≃o β
s : Set α
⊢ f (sSup s) = ⨆ a ∈ s, f a

Tactic:
by
  simp only [sSup_eq_iSup, OrderIso.map_iSup]

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

Goal state before:
pp: case mpr
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ x ∈ ⋃₀ C → x ∈ ⋃ y, range fun s ↦ ↑(f s y)

Tactic:
rintro ⟨s, hs, hx⟩
    obtain ⟨y, hy⟩ := hf ⟨s, hs⟩ ⟨x, hx⟩
    refine ⟨_, ⟨y, rfl⟩, ⟨s, hs⟩, ?_⟩
    exact congr_arg Subtype.val hy

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
⊢ ⨅ a, ⨆ b, g a b = ⨆ g_1, ⨅ a, g a (g_1 a)

Tactic:
let rhs := ⨆ h : ∀ a, β a, ⨅ a, g a (h a)

Goal state after:
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
⊢ ⨅ a, ⨆ b, g a b = ⨆ g_1, ⨅ a, g a (g_1 a)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ s ⊆ {⊤}

Tactic:
intro c

Goal state after:
case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
⊢ c ∈ s → c ∈ {⊤}
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case h
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
⊢ b ∈ lowerBounds ((fun a ↦ ↑a) ⁻¹' s)

Tactic:
intro c

Goal state after:
case h
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
c : β
⊢ c ∈ (fun a ↦ ↑a) ⁻¹' s → b ≤ c
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.refine_1.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a : β
ha✝ : Option.some a ∈ lowerBounds s
h : (fun a ↦ ↑a) ⁻¹' s = ∅
ha : none ∈ s
⊢ none ∈ {⊤}

pp: case neg.some.refine_1.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a✝ : β
ha✝ : Option.some a✝ ∈ lowerBounds s
h : (fun a ↦ ↑a) ⁻¹' s = ∅
a : β
ha : Option.some a ∈ s
⊢ Option.some a ∈ {⊤}

Tactic:
· exact mem_singleton ⊤

Goal state after:
case neg.some.refine_1.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a✝ : β
ha✝ : Option.some a✝ ∈ lowerBounds s
h : (fun a ↦ ↑a) ⁻¹' s = ∅
a : β
ha : Option.some a ∈ s
⊢ Option.some a ∈ {⊤}
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
⊢ sSup S ≤ a

Tactic:
by
    rcases S.eq_empty_or_nonempty with h | h
    · change ite _ _ _ ≤ a
      simp [h]
    · exact (WithTop.isLUB_sSup' h).2 ha

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: case inr
α : Type u_1
s : Set α
inst✝ : Preorder α
hs : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x < y
h' : y ≤ x
⊢ y ≤ x

Tactic:
| inr h' =>

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: case inl
α : Type u_1
s : Set α
inst✝ : Preorder α
hs : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x < y
h' : x ≤ y
⊢ y ≤ x

Tactic:
simpa [lt_iff_le_not_ge, h'] using h

Goal state after: