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
⊢ a * d = c / d * d * b ↔ a * d = c * b

Tactic:
hd.div_mul_cancel

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ a * d = c * b ↔ a * d = c * b
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
⊢ (a ^ m)⁻¹ * (a ^ n)⁻¹⁻¹ = (a ^ m)⁻¹ * a ^ n

Tactic:
inv_inv

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
⊢ (a ^ m)⁻¹ * a ^ n = (a ^ m)⁻¹ * a ^ n
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ (a ^ m)⁻¹ * (a ^ n)⁻¹⁻¹ = (a ^ m)⁻¹ * a ^ n

Tactic:
inv_inv

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ (a ^ m)⁻¹ * a ^ n = (a ^ m)⁻¹ * a ^ n
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
⊢ (-1) ^ n = if Even n then 1 else -1

Tactic:
cases even_or_odd n with
  | inl h => rw [h.neg_one_pow, if_pos h]
  | inr h => rw [h.neg_one_pow, if_neg (by simpa using h)]

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ 0 ≤ f a

Tactic:
← zero,

Goal state after:
α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ f 0 ≤ f a
Module: Mathlib.Algebra.Order.GroupWithZero.Defs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ 0 ≤ f a

Tactic:
← zero,

Goal state after:
α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ f 0 ≤ f a
Module: Mathlib.Algebra.Order.GroupWithZero.Defs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ 0 < f a

Tactic:
← zero,

Goal state after:
α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ f 0 < f a
Module: Mathlib.Algebra.Order.GroupWithZero.Defs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ 0 < f a

Tactic:
← zero,

Goal state after:
α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ f 0 < f a
Module: Mathlib.Algebra.Order.GroupWithZero.Defs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ b * a < c * a

Tactic:
by
    rw [← lt, mul, mul]; exact mul_lt_mul_of_pos_right (lt.2 hbc) (by rwa [← zero, lt])

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

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

Tactic:
inv_inv

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

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

Tactic:
inv_inv

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

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

Tactic:
simpa only [div_eq_mul_inv] using mul_le_mul_iff_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 : b * a ≤ c * a
⊢ b ≤ c

Tactic:
by
    rw [mul_comm _ a, mul_comm _ a] at h; exact le_of_mul_le_mul_left a b c h

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ b * c
⊢ d ≤ c

Tactic:
exact le_of_mul_le_mul_of_pos_left h <| ha.trans_le hab

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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hba : b < a
hdc : d < c
⊢ b * c + a * d < b * d + a * c

Tactic:
exact mul_add_mul_lt_mul_add_mul hba hdc

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

Tactic:
rw [← inv_mul_lt_iff₀ ha, mul_one]

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₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b⁻¹ ≤ a⁻¹⁻¹ ↔ b⁻¹ ≤ a

Tactic:
inv_inv

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b⁻¹ ≤ a ↔ b⁻¹ ≤ a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b⁻¹ < a⁻¹⁻¹ ↔ b⁻¹ < a

Tactic:
inv_inv

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b⁻¹ < a ↔ b⁻¹ < a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b⁻¹⁻¹ ≤ a⁻¹ ↔ b ≤ a⁻¹

Tactic:
inv_inv

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b ≤ a⁻¹ ↔ b ≤ a⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b⁻¹⁻¹ < a⁻¹ ↔ b < a⁻¹

Tactic:
inv_inv

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b < a⁻¹ ↔ b < a⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b / c ≤ a ↔ b ≤ c * a

Tactic:
rw [div_le_iff₀ hc, mul_comm]

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

Goal state before:
pp: case mpr.intro
α : Type u_1
x✝¹ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) ⟦y⟧
⊢ Acc (Quotient.lift₂ r H) ⟦x✝⟧

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

Goal state after:
case mpr.intro
α : Type u_1
x✝¹ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) ⟦y⟧
q : Quotient x✝¹
h : Quotient.lift₂ r H q ⟦x✝⟧
⊢ Acc (Quotient.lift₂ r H) q
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 : 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 : b ≤ 1
⊢ |a * b|ₘ = a⁻¹ * b

Tactic:
simp only [h.antisymm hb, mabs_of_lt_one ha, mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ |a|ₘ

Tactic:
apply pow_two_semiclosed _

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ |a|ₘ ^ 2
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
⊢ a = b ∨ a = b⁻¹ → |a|ₘ = |b|ₘ

Tactic:
by rintro (h | h) <;> simp [h]

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

Goal state before:
pp: α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
⊢ ∃ c x, a * c = b

Tactic:
obtain ⟨c, hc⟩ := le_iff_exists_mul.1 h.le

Goal state after:
α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
c : α
hc : b = a * c
⊢ ∃ c x, a * c = b
Module: Mathlib.Data.Int.GCD

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

Tactic:
simp [← pow_gcd_eq_one, hmn]

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

Goal state before:
pp: case refine_3.inr
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
y x : αˣ
h : ↑x < ↑y
hx : 0 < ↑x
z : αˣ
hz : x < z
hz' : z < y
⊢ ∃ a, ↑x < a ∧ a < ↑y

Tactic:
exact ⟨z, by simp [hz, hz']⟩

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

Goal state before:
pp: case succ
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
by_cases hk : P (k + 1)

Goal state after:
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

case neg
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
⊢ findGreatest P n ≤ findGreatest Q n

Tactic:
induction n with
  | zero => rfl
  | succ n hn =>
    by_cases h : P (n + 1)
    · rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]
    · rw [findGreatest_of_not h]
      exact le_trans hn (Nat.findGreatest_mono_right _ <| le_succ _)

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

Goal state before:
pp: P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z

Tactic:
by
  classical
  let ⟨b, Hb⟩ := Hbdd
  let ⟨lb, H⟩ := leastOfBdd b Hb Hinh
  exact ⟨lb, H⟩

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

Goal state before:
pp: case h
F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
bounded : ∀ (x : α), ∃ n, x ≤ ↑n
x : α
n : ℕ
hn : -x ≤ ↑n
⊢ ↑(-↑n) ≤ x

Tactic:
simpa [neg_le]

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
ha : 0 ≤ 0
⊢ ⌊0⌋₊ = 0

Tactic:
exact floor_zero

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
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < ↑(n + 1)

Tactic:
← floor_lt' (Nat.add_one_ne_zero n),

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ ⌊a⌋₊ < n + 1
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ ⊥) ≤ ⊥ ⊔ ⊥ ⊓ ⊥

Tactic:
simp [← coe_inf, ← coe_sup]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ ↑a✝) ≤ ⊥ ⊔ ⊥ ⊓ ↑a✝

Tactic:
simp [← coe_inf, ← coe_sup]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (⊥ ⊔ ↑a✝) ⊓ (⊥ ⊔ ⊥) ≤ ⊥ ⊔ ↑a✝ ⊓ ⊥

Tactic:
simp [← coe_inf, ← coe_sup]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (⊥ ⊔ ↑a✝¹) ⊓ (⊥ ⊔ ↑a✝) ≤ ⊥ ⊔ ↑a✝¹ ⊓ ↑a✝

Tactic:
simp [← coe_inf, ← coe_sup]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (↑a✝ ⊔ ⊥) ⊓ (↑a✝ ⊔ ⊥) ≤ ↑a✝ ⊔ ⊥ ⊓ ⊥

Tactic:
simp [← coe_inf, ← coe_sup]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ⊥) ⊓ (↑a✝¹ ⊔ ↑a✝) ≤ ↑a✝¹ ⊔ ⊥ ⊓ ↑a✝

Tactic:
simp [← coe_inf, ← coe_sup]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ ⊥) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ ⊥

Tactic:
simp [← coe_inf, ← coe_sup]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝² a✝¹ a✝ : α
⊢ (↑a✝² ⊔ ↑a✝¹) ⊓ (↑a✝² ⊔ ↑a✝) ≤ ↑a✝² ⊔ ↑a✝¹ ⊓ ↑a✝

Tactic:
simp [← coe_inf, ← coe_sup]

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝² a✝¹ a✝ : α
⊢ (a✝² ⊔ a✝¹) ⊓ (a✝² ⊔ a✝) ≤ a✝² ⊔ a✝¹ ⊓ a✝
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
h : a = b
⊢ ⅟a = ⅟b

Tactic:
apply invOf_eq_right_inv
  rw [h, mul_invOf_self]

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

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
x : R
h : IsSquare x
⊢ 0 ≤ x

Tactic:
rcases h with ⟨y, rfl⟩

Goal state after:
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
y : R
⊢ 0 ≤ y * y
Module: Mathlib.Data.Set.NAry

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

Tactic:
simp_rw [← image_uncurry_prod, inter_prod, image_inter hf.uncurry]

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

Goal state before:
pp: case refine_1
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval a '' s)
⊢ update f a b ∈ upperBounds s

Tactic:
exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩

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

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

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Goal state after:
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

case inl.inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : s.Nonempty
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ t.Nonempty
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
inst✝ : IsStrictOrderedRing α
h : a / b ≤ c / d
he : 0 ≤ e
⊢ a / (b * e) ≤ c / (d * e)

Tactic:
rw [div_mul_eq_div_mul_one_div, div_mul_eq_div_mul_one_div]
  gcongr
  exact one_div_nonneg.2 he

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: case map_const
γ : Type u_1
⊢ ∀ {α β : Type u_2}, mapConst = map ∘ Function.const β

Tactic:
intros

Goal state after:
case map_const
γ : Type u_1
α✝ β✝ : Type u_2
⊢ mapConst = map ∘ Function.const β✝
Module: Mathlib.Control.Functor

Goal state before:
pp: case id_map
γ : Type u_1
⊢ ∀ {α : Type u_2} (x : Const γ α), id <$> x = x

Tactic:
intros

Goal state after:
case id_map
γ : Type u_1
α✝ : Type u_2
x✝ : Const γ α✝
⊢ id <$> x✝ = x✝
Module: Mathlib.Control.Functor

Goal state before:
pp: case comp_map
γ : Type u_1
⊢ ∀ {α β γ_1 : Type u_2} (g : α → β) (h : β → γ_1) (x : Const γ α), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
intros

Goal state after:
case comp_map
γ : Type u_1
α✝ β✝ γ✝ : Type u_2
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Const γ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
⊢ f = HMul.hMul → IsRat a na da → IsRat b nb db → na.mul nb = (↑k).mul nc → da.mul db = k.mul dc → IsRat (f a b) nc dc

Tactic:
by
  rintro rfl ⟨_, rfl⟩ ⟨_, rfl⟩ (h₁ : na * nb = k * nc) (h₂ : da * db = k * dc)
  have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da:α) db
  have := invertibleOfMul' (α := α) h₂
  refine ⟨this, ?_⟩
  have H := (Nat.cast_commute (α := α) da db).invOf_left.invOf_right.right_comm
  have h₁ := congr_arg (Int.cast (R := α)) h₁
  simp only [Int.cast_mul, Int.cast_natCast] at h₁
  simp only [← mul_assoc, (Nat.cast_commute (α := α) da nb).invOf_left.right_comm, h₁]
  have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
  simp only [Nat.cast_mul, ← mul_assoc] at h₂; rw [H] at h₂
  simp only [mul_invOf_cancel_right'] at h₂; rw [h₂, Nat.cast_commute]
  simp only [mul_invOf_cancel_right,
    (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
    (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]

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

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

Tactic:
inv_inv

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ b⁻¹ ≤ a ↔ b⁻¹ ≤ a
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
inv_inv

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ b ≤ a⁻¹ ↔ b ≤ a⁻¹
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a / 0 < 1 ↔ 0 < 0 ∧ a < 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 < a

Tactic:
simp [zero_lt_one]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
hr : BiUnique R
a : α
b : β
x✝ : R a b
⊢ (fun x1 x2 ↦ x1 ∈ x2) a [] ↔ (fun x1 x2 ↦ x1 ∈ x2) b []

Tactic:
by simp only [not_mem_nil]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ SublistForall₂ R l₁ (map f l₂) ↔ SublistForall₂ (fun a c ↦ R a (f c)) l₁ l₂

Tactic:
simp only [sublistForall₂_iff]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂) ↔ ∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : 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
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝

Tactic:
congr
      · subsingleton
      · apply ih; simpa using hl

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
inst✝³ : Monoid M
inst✝² : Monoid N
L : List ι
f : ι → M
G : Type u_8
inst✝¹ : FunLike G M N
inst✝ : MonoidHomClass G M N
g : G
⊢ (map (⇑g ∘ f) L).prod = g (map f L).prod

Tactic:
by rw [← prod_hom, map_map]

Goal state after: