mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑n + ↑d < a + ↑n ↔ d + n < ⌈a⌉₊ + n

Tactic:
add_comm (n : R),

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑d + ↑n < a + ↑n ↔ d + n < ⌈a⌉₊ + n
Module: Mathlib.Order.Directed

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
b : β
i : ι
hb : ¬∃ i, e i = b
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

Tactic:
use e i

Goal state after:
case h
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
b : β
i : ι
hb : ¬∃ i, e i = b
⊢ (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ (e i)) ∧
    (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ (e i))
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Invertible 2
⊢ ⅟2 + ⅟2 = 1

Tactic:
by rw [← two_mul, 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✝¹ : IsStrictOrderedRing R
a : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ a ^ n ≤ 0 ↔ a ≤ 0

Tactic:
by
  rw [le_iff_lt_or_eq, le_iff_lt_or_eq, hn.pow_neg_iff, pow_eq_zero_iff]
  rintro rfl; simp at hn

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Units

Goal state before:
pp: u v : ℤˣ
⊢ u ≠ v ↔ u = -v

Tactic:
by
  simpa only [Ne, Units.ext_iff] using! isUnit_ne_iff_eq_neg u.isUnit v.isUnit

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
q : ℚ≥0
⊢ ↑q.num / ↑q.den = f (↑q.num / ↑q.den)

Tactic:
div,

Goal state after:
K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
q : ℚ≥0
⊢ ↑q.num / ↑q.den = f ↑q.num / f ↑q.den
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
ratCast : ∀ (q : ℚ), f ↑q = ↑q
q : ℚ
⊢ ↑q = f (↑q.num / ↑q.den)

Tactic:
div,

Goal state after:
K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
ratCast : ∀ (q : ℚ), f ↑q = ↑q
q : ℚ
⊢ ↑q = f ↑q.num / f ↑q.den
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:
by
  simp_rw [← image_uncurry_prod, inter_prod, image_inter hf.uncurry]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
s : Set α
t : Set β
hs : s.Subsingleton
ht : t.Subsingleton
f : α → β → γ
⊢ (Set.image2 f s t).Subsingleton

Tactic:
rw [← image_prod]

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
s : Set α
t : Set β
hs : s.Subsingleton
ht : t.Subsingleton
f : α → β → γ
⊢ ((fun x ↦ f x.1 x.2) '' s ×ˢ t).Subsingleton
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |a ^ (n + 1) - b ^ (n + 1)| ≤ |a - b| * ↑(n + 1) * max |a| |b| ^ (n + 1 - 1)

Tactic:
Nat.add_sub_cancel,

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |a ^ (n + 1) - b ^ (n + 1)| ≤ |a - b| * ↑(n + 1) * max |a| |b| ^ n
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Monotone f
⊢ IsCofinalFor (f '' s) (f '' t)

Tactic:
by
  simp only [IsCofinalFor, forall_mem_image, exists_mem_image]
  rintro a ha
  obtain ⟨b, hb, hab⟩ := hst ha
  exact ⟨b, hb, hf hab⟩

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.12
a : α
x✝ : ↑{a}
x : α
h : x ∈ {a}
⊢ (fun x ↦ ⟨a, ⋯⟩) ((fun x ↦ PUnit.unit) ⟨x, h⟩) = ⟨x, h⟩

Tactic:
subst x
    rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a < b
⊢ Ico a b \ (Ico a b \ {a}) = {a}

Tactic:
sdiff_sdiff_cancel_left (singleton_subset_iff.2 <| left_mem_Ico.2 h)

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a < b
⊢ {a} = {a}
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
ho : Iio a ⊆ s
hc : s ⊆ Iic a
h : a ∈ s
⊢ Iic a ⊆ s

Tactic:
rw [← Iio_union_right, union_subset_iff]

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
ho : Iio a ⊆ s
hc : s ⊆ Iic a
h : a ∈ s
⊢ Iio a ⊆ s ∧ {a} ⊆ s
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
s : Set α
a : α
⊢ BddAbove (insert a s) ↔ BddAbove s

Tactic:
simp only [insert_eq, bddAbove_union, bddAbove_singleton, true_and]

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
inst✝ : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < ↑n

Tactic:
apply Nat.cast_pos.2

Goal state after:
A : Type u_1
e : A
n : ℕ
inst✝³ : Semiring A
inst✝² : PartialOrder A
inst✝¹ : IsOrderedRing A
inst✝ : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < n
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
simpa using inv_le_comm₀ ha hb

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ { map := m, mapConst := mc } = { map := m', mapConst := mc' }

Tactic:
cases show @m = @m' by funext α β f x; apply H

Goal state after:
case refl
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ { map := m, mapConst := mc } = { map := m, mapConst := mc' }
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
x y : List α
n : ℕ
⊢ take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length

Tactic:
apply take_eq_left_iff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
x✝² : List α
x✝¹ : List β
x✝ : Forall₂ R x✝² x✝¹
⊢ Forall₂ R (take 0 x✝²) (take 0 x✝¹)

Tactic:
by simp only [Forall₂.nil, take]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
n✝ : ℕ
⊢ Forall₂ R (take (n✝ + 1) []) (take (n✝ + 1) [])

Tactic:
by simp only [Forall₂.nil, take]

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

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

Tactic:
rcases lt_trichotomy b 0 with (hb | rfl | hb)
  · simp [hb, hb.not_gt, hb.ne, div_le_one_of_neg]
  · simp [zero_le_one]
  · simp [hb, hb.not_gt, div_le_one, hb.ne.symm]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
h : ∀ ε > 0, b - ε ≤ a
⊢ b ≤ a

Tactic:
by
  contrapose! h
  simpa only [@and_comm ((0 : α) < _), lt_sub_iff_add_lt, gt_iff_lt] using
    exists_add_lt_and_pos_of_lt h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ Forall₂ r ∘r Perm = Perm ∘r Forall₂ r

Tactic:
funext l₁ l₃

Goal state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ = (Perm ∘r Forall₂ r) l₁ l₃
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
P : α → Prop
inst✝ : DecidablePred P
l : List α
a : α
⊢ countP (fun x ↦ x == a) l =
    countP (fun x ↦ x == a) (filter (fun b ↦ decide (P b)) l) + countP (fun x ↦ x == a) (filter (fun x ↦ decide ¬P x) l)

Tactic:
convert countP_eq_countP_filter_add l _ P

Goal state after:
case e'_3
α : Type u_1
inst✝¹ : DecidableEq α
P : α → Prop
inst✝ : DecidablePred P
l : List α
a x✝ : α
⊢ (decide ¬P x✝) = !decide (P x✝)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : Inhabited M
l : List M
h : l ≠ []
⊢ l.headI * l.tail.prod = l.prod

Tactic:
by cases l <;> [contradiction; simp]

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

Goal state before:
pp: case some
α : Type u
l : List α
h : ∀ (x : α), x ∈ l
x : α
⊢ ∃ a, (fun n ↦ l[n]?) a = some x

Tactic:
| some x =>

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

Goal state before:
pp: case pos
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
ha' : a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 1)

pp: case neg
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
ha' : ¬a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 0)

Tactic:
· rw [ha', _root_.pow_succ']

Goal state after:
case neg
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
ha' : ¬a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 0)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
⊢ L = L'

Tactic:
refine ext_get h fun i h₁ h₂ => ?_
  have : (L.take (i + 1)).prod = (L'.take (i + 1)).prod := h' _ (Nat.succ_le_of_lt h₁)
  rw [prod_take_succ L i h₁, prod_take_succ L' i h₂, h' i (Nat.le_of_lt h₁)] at this
  convert! mul_left_cancel this

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

Goal state before:
pp: case cons.some
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
b : β
ha : f a = some b
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)

Tactic:
simp +contextual [ha, ih]

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

Goal state before:
pp: a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ a /. b ≤ c /. d ↔ a * d ≤ c * b

Tactic:
Rat.le_iff_sub_nonneg,

Goal state after:
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ 0 ≤ c /. d - a /. b ↔ a * d ≤ c * b
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ * q₂).num = q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))

Tactic:
by
  rw [mul_def, normalize_eq]

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)

Tactic:
by
  rw [mul_def, normalize_eq]

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

Goal state before:
pp: q : ℚ
⊢ (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)

Tactic:
exact (q.reduced.mul_right q.reduced).mul_left (q.reduced.mul_right q.reduced)

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

Goal state before:
pp: z : ℤ
⊢ IsSquare ↑z ↔ IsSquare z

Tactic:
by
  simp_rw [isSquare_iff, num_intCast, den_intCast, IsSquare.one, and_true]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ n1 * n2 * (e1 * e2) = t1 * t2

Tactic:
mul_comm n1,

Goal state after:
α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ n2 * n1 * (e1 * e2) = t1 * t2
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ c
⊢ a * b ≤ a * c

Tactic:
rcases exists_add_of_le h with ⟨c, rfl⟩

Goal state after:
R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ a * b ≤ a * (b + c)
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ c
⊢ b * a ≤ c * a

Tactic:
rcases exists_add_of_le h with ⟨c, rfl⟩

Goal state after:
R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ b * a ≤ (b + c) * a
Module: Mathlib.Data.Bool.Set

Goal state before:
pp: α : Type u_1
f : Bool → α
⊢ range f = {f false, f true}

Tactic:
grind [cases Bool]

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

Goal state before:
pp: b : Bool
⊢ {b}ᶜ = {!b}

Tactic:
grind [cases Bool]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ ⨆ j, ⨆ (_ : j ≤ i), f j = (⨆ j, ⨆ (_ : j < i), f j) ⊔ f i

Tactic:
rw [iSup_split_single _ i]

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ (⨆ (_ : i ≤ i), f i) ⊔ ⨆ i_1, ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≤ i), f i_1 = (⨆ j, ⨆ (_ : j < i), f j) ⊔ f i
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ ⨆ j, ⨆ (_ : j ≥ i), f j = f i ⊔ ⨆ j, ⨆ (_ : j > i), f j

Tactic:
rw [iSup_split_single _ i]

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ (⨆ (_ : i ≥ i), f i) ⊔ ⨆ i_1, ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≥ i), f i_1 = f i ⊔ ⨆ j, ⨆ (_ : j > i), f j
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ⋃ x, {f x} = range f

Tactic:
by
  ext x
  simp [@eq_comm _ x]

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ AntitoneOn f s ↔ Antitone fun a ↦ f ↑a

Tactic:
simp [Antitone, AntitoneOn]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
⊢ min a b = if a ≤ b then a else b

Tactic:
· rcases ConditionallyCompleteLinearOrder.le_total a b with (h₁ | h₂)
      · simp [h₁]
      · simp [show ¬(a ≤ b) from fun h => hab (le_antisymm h h₂), h₂]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
⊢ max a b = if a ≤ b then b else a

Tactic:
· rcases ConditionallyCompleteLinearOrder.le_total a b with (h₁ | h₂)
      · simp [h₁]
      · simp [show ¬(a ≤ b) from fun h => hab (le_antisymm h h₂), h₂]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup s ∆ sSup t ≤ sSup (image2 (fun x1 x2 ↦ x1 ∆ x2) s t)

Tactic:
rw [sSup_image2]
  calc
  _ ≤ ⨆ a ∈ s, a ∆ sSup t := by simpa [sSup_image] using sSup_symmDiff_le hs
  _ ≤ _ := iSup_mono fun a ↦ iSup_mono fun _ ↦ by simpa [sSup_image] using symmDiff_sSup_le ht

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

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

Tactic:
refine coe_le_coe.2 (le_csInf ?_ ?_)

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

case neg.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ ∀ b ∈ (fun a ↦ ↑a) ⁻¹' s, a ≤ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.coe
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a✝ : WithBot α
haS : ↑a✝ ∈ S
⊢ sInf ((fun a ↦ ↑a) ⁻¹' S) ≤ a✝

Tactic:
refine csInf_le ?_ haS

Goal state after:
case neg.coe
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a✝ : WithBot α
haS : ↑a✝ ∈ S
⊢ BddBelow ((fun a ↦ ↑a) ⁻¹' S)
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
a : α
ha : ¬a ∈ s
b : α
hb : b ∈ s
⊢ a ≠ b → r a b ∧ r b a ↔ r a b ∧ r b a

Tactic:
by simp [(ne_of_mem_of_not_mem hb ha).symm]

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
h : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ¬Disjoint (f i) (f j) → i = j

Tactic:
exact h.elim hi hj

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : ¬IsMaxChain r s
⊢ SuperChain r s (SuccChain r s)

Tactic:
simp only [IsMaxChain, _root_.not_and, not_forall, exists_prop] at hs₂
  obtain ⟨t, ht, hst⟩ := hs₂ hs₁
  exact succChain_spec ⟨t, hs₁, ht, ssubset_iff_subset_ne.2 hst⟩

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : SupSet α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
⊢ sSup t = default

Tactic:
simp [sSup, ht]

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 : BddAbove t
⊢ sSup (Subtype.val '' t) ∈ s

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

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: ⊢ 0 * 1 = 0

Tactic:
Nat.zero_mul

Goal state after:
⊢ 0 = 0
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1) ^ (k + 1) * (n + 1) < (n + 1 + (k + 1)) * (n + 1).ascFactorial (k + 1)

Tactic:
Nat.mul_comm

Goal state after:
n k : ℕ
⊢ (n + 1) * (n + 1) ^ (k + 1) < (n + 1 + (k + 1)) * (n + 1).ascFactorial (k + 1)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: k : ℕ
⊢ 0 * descFactorial 0 k = 0

Tactic:
Nat.zero_mul

Goal state after:
k : ℕ
⊢ 0 = 0
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case pos
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : k ≤ n
⊢ 0 * n.descFactorial k = 0

Tactic:
Nat.zero_mul

Goal state after:
case pos
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : k ≤ n
⊢ 0 = 0
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommMonoid β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
a : α
⊢ 0 ≤ 2 • f a

Tactic:
by
        rw [two_nsmul, ← map_one_eq_zero f, ← div_self' a]
        exact map_div_le_add _ _ _

Goal state after: