mathlib-initiative/mathlib-tactics huggingface dataset:
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:
mabs_of_one_lt ab,

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 * b = a⁻¹ * b
ab : 1 < a * b
⊢ b ≤ 1
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 n : G
one_le_a : 1 ≤ a
a_le_n : a ≤ n
one_le_b : 1 ≤ b
b_le_n : b ≤ n
⊢ a / b ≤ n ∧ b / a ≤ n

Tactic:
div_le_iff_le_mul,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_le_n : a ≤ n
one_le_b : 1 ≤ b
b_le_n : b ≤ n
⊢ a ≤ n * b ∧ b / a ≤ n
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

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

Tactic:
← pow_two

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) ^ 2 = (a ⊓ b) ^ 2
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))

Tactic:
by
        rw [← sup_inf_right, ← inf_sup_right, sup_assoc, sup_comm c (a ⊔ c), sup_right_idem,
          sup_assoc, inf_assoc, inf_comm c (a ⊓ c), inf_right_idem, inf_assoc]

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 : α
h : b ≤ c
h2 : a ≤ c - b
⊢ a + b ≤ c

Tactic:
grw [h2, tsub_add_cancel_of_le h]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x y : WithBot α
⊢ x ≤ y ↔ ∀ (a : α), x = ↑a → ∃ b, y = ↑b ∧ a ≤ b

Tactic:
by
  cases x <;> cases y <;> simp [le_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst✝ : DenselyOrdered α
⊢ Nontrivial αˣ

Tactic:
have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
  tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst✝ : DenselyOrdered α
⊢ DenselyOrdered αˣ

Tactic:
have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
  tauto

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : Nontrivial αˣ
⊢ DenselyOrdered αˣ ↔ DenselyOrdered α

Tactic:
have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
  tauto

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

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

Tactic:
induction k generalizing m with

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

Goal state before:
pp: case step
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
⊢ findGreatest P m ≤ findGreatest P m✝.succ

Tactic:
rw [findGreatest_succ]
    split_ifs
    · exact le_trans ih <| le_trans (findGreatest_le _) (le_succ _)
    · exact ih

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
⊢ (∀ x ∈ s, ∀ y ∈ s, ∃ z ∈ s, r x z ∧ r y z) ↔ ∀ a ∈ s, ∀ a_1 ∈ s, ∃ a_2, r a a_2 ∧ a_2 ∈ s ∧ r a_1 a_2

Tactic:
exact forall₂_congr fun x _ => by simp [And.comm, and_assoc]

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
⊢ DirectedOn (r on f) s ↔ DirectedOn r (f '' s)

Tactic:
by
  refine ⟨DirectedOn.mono_comp (by simp), fun h x hx y hy ↦ ?_⟩
  obtain ⟨_, ⟨z, hz, rfl⟩, hz'⟩ := h (f x) (Set.mem_image_of_mem f hx) (f y)
    (Set.mem_image_of_mem f hy)
  grind

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

Goal state before:
pp: u : ℤ
⊢ IsUnit u ↔ u.natAbs = 1

Tactic:
by simp [natAbs_eq_iff, isUnit_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| = |b| ↔ a * a = b * b

Tactic:
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
  exact (mul_self_inj (abs_nonneg a) (abs_nonneg b)).symm

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s

Tactic:
intro x hx y hy
  obtain ⟨z, hz, hxz, hyz⟩ := hd x (hst hx) y (hst hy)
  obtain ⟨w, hw, hzw⟩ := hc hz
  exact ⟨w, hw, hxz.trans hzw, hyz.trans hzw⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a ≤ b
⊢ Ioc a b ∪ {a} = Icc a b

Tactic:
by
  rw [← Icc_sdiff_left, sdiff_union_self,
    union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Icc.2 hab)]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

Tactic:
refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_

Goal state after:
case neg.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ico a b

case neg.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ Ico a b ⊆ s
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 - 2⁻¹ = 2⁻¹

Tactic:
rw [sub_eq_iff_eq_add, ← two_mul, mul_inv_cancel₀ two_ne_zero]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))

Tactic:
have : q b := by rwa [← hpq h₁]
      simp only [filter_cons_of_pos h, filter_cons_of_pos this, forall₂_cons, h₁, true_and,
        rel_filter hpq h₂]

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

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

Tactic:
cases h with
    | intro hn hnm =>
      rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
        rel_congr_right (getElem_cons_eraseIdx_perm ..)]

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

Goal state before:
pp: α : Type u
a b : α
l : List α
⊢ b :: l = replicate (b :: l).length a ↔ ∀ (b_1 : α), b_1 ∈ b :: l → b_1 = a

Tactic:
simp [eq_replicate_length, replicate_succ]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
⊢ 1 / l.eval = l⁻¹.eval

Tactic:
simp [eval_inv]

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

Goal state before:
pp: α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
⊢ l.Disjoint l₁ ↔ l.Disjoint l₂

Tactic:
by
  simp_rw [List.disjoint_right, p.mem_iff]

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

Goal state before:
pp: q : ℚ
⊢ |q|.num = |q.num|

Tactic:
by
  rw [abs_def']

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

Goal state before:
pp: q : ℚ
⊢ |q|.den = q.den

Tactic:
by
  rw [abs_def']

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ ↑u * b ↔ a ∣ b

Tactic:
rw [mul_comm]
  apply dvd_mul_right

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

Goal state before:
pp: n : ℤ
hn : 0 < n
⊢ ↑↑n.natAbs.toPNat' = n

Tactic:
rw [Nat.toPNat'_coe, if_pos (Int.natAbs_pos.2 hn.ne'),
        Int.natAbs_of_nonneg hn.le]

Goal state after:
Module: Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm

Goal state before:
pp: matType : Nat → Nat → Type
inst✝ : UsableInSimplexAlgorithm matType
exitIdx enterIdx : Nat
s : Tableau matType
mat✝² : matType s.basic.size s.free.size := s.mat
intersectCoef : Rat := mat✝²[(exitIdx, enterIdx)]!
__s✝ : matType s.basic.size s.free.size
mat✝¹ : matType s.basic.size s.free.size := __s✝
mat✝ : matType s.basic.size s.free.size := setElem mat✝¹ exitIdx enterIdx (-1)
mat : matType s.basic.size s.free.size := divideRow mat✝ exitIdx (-intersectCoef)
newBasic : Array Nat := s.basic.set! exitIdx s.free[enterIdx]!
newFree : Array Nat := s.free.set! enterIdx s.basic[exitIdx]!
⊢ newBasic.size = s.basic.size

Tactic:
apply Array.size_setIfInBounds

Goal state after:
Module: Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm

Goal state before:
pp: matType : Nat → Nat → Type
inst✝ : UsableInSimplexAlgorithm matType
exitIdx enterIdx : Nat
s : Tableau matType
mat✝² : matType s.basic.size s.free.size := s.mat
intersectCoef : Rat := mat✝²[(exitIdx, enterIdx)]!
__s✝ : matType s.basic.size s.free.size
mat✝¹ : matType s.basic.size s.free.size := __s✝
mat✝ : matType s.basic.size s.free.size := setElem mat✝¹ exitIdx enterIdx (-1)
mat : matType s.basic.size s.free.size := divideRow mat✝ exitIdx (-intersectCoef)
newBasic : Array Nat := s.basic.set! exitIdx s.free[enterIdx]!
newFree : Array Nat := s.free.set! enterIdx s.basic[exitIdx]!
hb : newBasic.size = s.basic.size
⊢ newFree.size = s.free.size

Tactic:
apply Array.size_setIfInBounds

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

Goal state before:
pp: case node
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
v : α
l r : BinaryTree α
hl : traverse pure l = pure l
hr : traverse pure r = pure r
⊢ traverse pure (node v l r) = pure (node v l r)

Tactic:
rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]

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

Goal state before:
pp: α : Type u
x : BinaryTree α
⊢ 0 < x.numLeaves

Tactic:
rw [numLeaves_eq_numNodes_succ]

Goal state after:
α : Type u
x : BinaryTree α
⊢ 0 < x.numNodes + 1
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:
by
  rw [iSup_split_single _ i]
  -- Squeezed for a ~10x speedup, though it's still reasonably fast unsqueezed.
  simp only [ge_iff_le, le_refl, iSup_pos, ne_comm, iSup_and', gt_iff_lt, lt_iff_le_and_ne,
    and_comm]

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:
sInf_eq_iInf,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ Iic (⨅ a ∈ s, a) = ⋂ a ∈ s, Iic a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds (upperBounds s)

Tactic:
rintro (⟨⟩ | b) hb

Goal state after:
case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ≤ none

case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ≤ Option.some b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ lowerBounds (upperBounds s)

Tactic:
rintro (⟨⟩ | b) hb

Goal state after:
case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ ⊤ ≤ none

case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ⊤ ≤ Option.some b
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z ∈ Icc x x
⊢ z ∈ s

Tactic:
Icc_self,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z ∈ {x}
⊢ z ∈ s
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a b q m a' : ℤ
b' r : ℕ
ha : IsInt a a'
hb : IsNat b b'
hm : q * ↑b' = m
h : ↑r + m = a'
h₂ : r.blt b' = true
⊢ a / b = ↑q

Tactic:
by
  obtain ⟨⟨rfl⟩, ⟨rfl⟩⟩ := ha, hb
  simp only [Nat.blt_eq] at h₂; simp only [← h, ← hm, Int.cast_id]
  rw [Int.add_mul_ediv_right _ _ (Int.ofNat_ne_zero.2 ((Nat.zero_le ..).trans_lt h₂).ne')]
  rw [Int.ediv_eq_zero_of_lt, zero_add] <;> [simp; simpa using h₂]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : One M
f : ι → M
s : Set κ
g : κ → ι
⊢ g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g))

Tactic:
by
  rw [mulSupport_comp_eq_preimage f g, image_inter_preimage]

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

Goal state before:
pp: m n : ℕ
hn : 0 < n
h : n < m
this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
⊢ n ! < m !

Tactic:
induction h generalizing hn with

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

Goal state before:
pp: case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x < 1 - fract x
⊢ |fract x| = fract x

Tactic:
abs_fract

Goal state after:
case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x < 1 - fract x
⊢ fract x = fract x
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m n : ℕ+
⊢ m ∣ n → m ≤ n

Tactic:
rw [dvd_iff']
  intro h
  rw [← h]
  apply (mod_le n m).left

Goal state after:
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
⊢ (∃ z, a - b = ↑z) → fract a = fract b

Tactic:
by
    rintro ⟨z, hz⟩
    refine fract_eq_iff.2 ⟨fract_nonneg _, fract_lt_one _, z + ⌊b⌋, ?_⟩
    rw [eq_add_of_sub_eq hz, add_comm, Int.cast_add]
    exact add_sub_sub_cancel _ _ _

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = negOfNat ⌈↑n / ↑d⌉.toNat

Tactic:
rw [@negOfNat_eq (toNat _), ofNat_eq_natCast,
    natCast_toNat_eq_self.mpr (ceil_nonneg (div_nonneg n.cast_nonneg d.cast_nonneg)),
    ← Int.cast_natCast n, ceil_intCast_div_natCast n d, neg_neg, ← ofNat_eq_natCast, ← negOfNat_eq,
    ← floor_intCast_div_natCast (.negOfNat n) d, ← floor_cast (α := α), Rat.cast_div,
    cast_intCast, cast_natCast]

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

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
inst✝ : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)

Tactic:
have h : ∃ n : ℕ, x < y ^ n := pow_unbounded_of_one_lt _ hy
  exact
      let n := Nat.find h
      have hn : x < y ^ n := Nat.find_spec h
      have hnp : 0 < n :=
        pos_iff_ne_zero.2 fun hn0 => by rw [hn0, pow_zero] at hn; exact not_le_of_gt hn hx
      have hnsp : Nat.pred n + 1 = n := Nat.succ_pred_eq_of_pos hnp
      have hltn : Nat.pred n < n := Nat.pred_lt (ne_of_gt hnp)
      ⟨Nat.pred n, le_of_not_gt (Nat.find_min h hltn), by rwa [hnsp]⟩

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

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ m, y ^ m ≤ x
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b := by
    obtain ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
    refine ⟨M, fun m hm ↦ ?_⟩
    contrapose! hM
    rw [← zpow_natCast]
    exact le_trans (zpow_le_zpow_right₀ hy.le hM.le) hm

Goal state after:
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ m, y ^ m ≤ x
hb : ∃ b, ∀ (m : ℤ), y ^ m ≤ x → m ≤ b
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case inr.inr.inr
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
obtain ⟨n, hn₁, hn₂⟩ :=
          exists_pow_btwn_of_lt_mul this (inv_pos_of_pos ha) (inv_le_one_of_one_le₀ ha₁) hc₀ hc₁

Goal state after:
case inr.inr.inr
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
⊢ ∃ n, a < c ^ n ∧ c ^ n < b
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ ∀ (a_1 : List α), p a → countP p (a ::ₘ Quot.mk (⇑(isSetoid α)) a_1) = countP p (Quot.mk (⇑(isSetoid α)) a_1) + 1

Tactic:
simpa using fun _ => List.countP_cons_of_pos (p := (p ·))

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

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ y = (x -ᵥ y) +ᵥ x ↔ y = x

Tactic:
eq_vadd_iff_vsub_eq,

Goal state after:
G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ y -ᵥ x = x -ᵥ y ↔ y = x
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
β : Type v
r : α → β → Prop
hr : Relator.BiUnique r
⊢ (fun x1 x2 ↦ x1 ↔ x2) [].Nodup [].Nodup

Tactic:
simp only [nodup_nil]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
f : α → β
a : β
l : List α
ihl : map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f} → map f l ∈ range (map f)
hl : a :: map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ a :: map f l ∈ range (map f)

Tactic:
rcases hl a mem_cons_self with ⟨a, rfl⟩

Goal state after:
case cons
α : Type u_1
β : Type u_2
f : α → β
l : List α
ihl : map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f} → map f l ∈ range (map f)
a : α
hl : f a :: map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ f a :: map f l ∈ range (map f)
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l t₁ t₂ : List α
p : t₁ ~ t₂
⊢ l.bagInter t₁ = l.bagInter t₂

Tactic:
by
  induction l generalizing t₁ t₂ p with | nil => simp | cons a l IH => ?_
  by_cases h : a ∈ t₁
  · simp [h, p.subset h, IH (p.erase _)]
  · simp [h, mt p.mem_iff.2 h, IH p]

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ s + filter (fun a ↦ p a ∧ ¬p a) s = s

pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → p a ∨ ¬p a

Tactic:
filter_eq_nil.2

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ s + 0 = s

α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → ¬(p a ∧ ¬p a)

α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → p a ∨ ¬p a
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t = 0 ↔ _root_.Disjoint s t

Tactic:
rw [← subset_zero]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t ⊆ 0 ↔ _root_.Disjoint s t
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.ndinter t = 0 ↔ _root_.Disjoint s t

Tactic:
rw [← subset_zero]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.ndinter t ⊆ 0 ↔ _root_.Disjoint s t
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <:+ List.insert a l

Tactic:
simp only [insert_of_not_mem h, suffix_cons]

Goal state after:
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : Unique α
s : Finset α
⊢ s.Nonempty ↔ s = {default}

Tactic:
simp [eq_singleton_iff_nonempty_unique_mem, eq_iff_true_of_subsingleton]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
hst : Disjoint s (t.erase a)
⊢ Disjoint s t

Tactic:
by
  rw [← erase_insert ha, disjoint_erase_comm, disjoint_insert_left]
  exact ⟨notMem_erase _ _, hst⟩

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

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ ({ toFun := fun f ↦ (fun i ↦ f (Sum.inl i), fun i' ↦ f (Sum.inr i')), invFun := fun g t_1 ↦ Sum.rec g.1 g.2 t_1,
              left_inv := ⋯, right_inv := ⋯ }.symm.trans
        { toFun := fun f x ↦ f ((Finset.union s t h).symm.symm x),
            invFun := fun f x ↦ ⋯ ▸ f ((Finset.union s t h).symm x), left_inv := ⋯, right_inv := ⋯ }.symm)
      (f, g) ⟨i, hi'⟩ =
    f ⟨i, hi⟩

Tactic:
trans_apply,

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ { toFun := fun f x ↦ f ((Finset.union s t h).symm.symm x), invFun := fun f x ↦ ⋯ ▸ f ((Finset.union s t h).symm x),
          left_inv := ⋯, right_inv := ⋯ }.symm
      ({ toFun := fun f ↦ (fun i ↦ f (Sum.inl i), fun i' ↦ f (Sum.inr i')), invFun := fun g t_1 ↦ Sum.rec g.1 g.2 t_1,
            left_inv := ⋯, right_inv := ⋯ }.symm
        (f, g))
      ⟨i, hi'⟩ =
    f ⟨i, hi⟩