mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (image2 f s t)

Tactic:
exact ⟨f a b, mem_upperBounds_image2 h₀ h₁ ha hb⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoTopOrder α
⊢ ¬BddAbove univ

Tactic:
simp [BddAbove]

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

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a : α
⊢ IsGreatest {w | Disjoint w a} aᶜ

Tactic:
simpa only [himp_bot, disjoint_iff_inf_le] using isGreatest_himp a ⊥

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

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

Tactic:
div_le_iff₀ hb,

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

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ 0
hs : IsLUB ∅ b
⊢ IsLUB ((fun a ↦ 0) '' ∅) 0

Tactic:
simp only [Set.image_empty, isLUB_empty_iff] at hs ⊢
      have hb := hs (b + b)
      rw [le_add_iff_nonneg_right] at hb
      exact hs.mono hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) ∈ zipWith Prod.mk (a✝ :: l₁✝) (b✝ :: l₂✝)
⊢ R x y

Tactic:
zipWith,

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) ∈ (a✝, b✝) :: zipWith Prod.mk l₁✝ l₂✝
⊢ R x y
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
⊢ (c :: (l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?

Tactic:
← cons_append,

Goal state after:
α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
⊢ (c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
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 ^ count a as = f a ^ (count a as + 0)

Tactic:
add_zero

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 ^ count a as = f a ^ count a as
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
l : List α
⊢ (map (fun a ↦ if p a then f a else g a) l).prod =
    (map f (filter (fun b ↦ decide (p b)) l)).prod * (map g (filter (fun a ↦ decide ¬p a) l)).prod

Tactic:
by
  induction l with
  | nil => simp
  | cons x xs ih =>
    simp only [map_cons, filter_cons, prod_cons] at ih ⊢
    rw [ih]
    clear ih
    by_cases hx : p x
    · simp only [hx, ↓reduceIte, decide_not, decide_true, map_cons, prod_cons, not_true_eq_false,
        decide_false, Bool.false_eq_true, mul_assoc]
    · simp only [hx, ↓reduceIte, decide_not, decide_false, Bool.false_eq_true, not_false_eq_true,
      decide_true, map_cons, prod_cons, mul_left_comm]

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

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ a = 0 ∨ b = 0 ↔ a = 0

Tactic:
or_iff_left b0

Goal state after:
a b : ℤ
b0 : b ≠ 0
⊢ a = 0 ↔ a = 0
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
p : { a // a ∈ l } → Bool
inst✝ : DecidableEq α
⊢ filter p l.attach = map (Subtype.map id ⋯) (filter (fun x ↦ decide (∃ h, p ⟨x, h⟩ = true)) l).attach

Tactic:
classical
  refine map_injective_iff.2 Subtype.coe_injective ?_
  simp [comp_def, map_filter _ Subtype.coe_injective]

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

Goal state before:
pp: α : Type u
l : List α
p : { a // a ∈ l } → Bool
inst✝ : DecidableEq α
⊢ filter p l.attach = map (Subtype.map id ⋯) (filter (fun x ↦ decide (∃ h, p ⟨x, h⟩ = true)) l).attach

Tactic:
by
  classical
  refine map_injective_iff.2 Subtype.coe_injective ?_
  simp [comp_def, map_filter _ Subtype.coe_injective]

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

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ ↑x✝¹.succ • x✝ = ↑x✝¹ • x✝ + x✝

Tactic:
by simp_rw [HSMul.hSMul, SMul.smul]; simp [Rat.add_mul]

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

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num

Tactic:
simpa using q.coprime_num_den.symm

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

Goal state before:
pp: case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ∃ x, ¬IsUnit x ∧ a * c = a * x

Tactic:
refine ⟨c, ?_, rfl⟩

Goal state after:
case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ¬IsUnit c
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime x z
H2 : IsRelPrime y z
x✝ : α
h : x✝ ∣ x * y
hz : x✝ ∣ z
⊢ IsUnit x✝

Tactic:
obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul h

Goal state after:
α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime x z
H2 : IsRelPrime y z
a b : α
ha : a ∣ x
hb : b ∣ y
h : a * b ∣ x * y
hz : a * b ∣ z
⊢ IsUnit (a * b)
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
⊢ q.den * q.den / 1 = q.den * q.den

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

Tactic:
Nat.div_one

Goal state after:
q : ℚ
⊢ q.den * q.den = q.den * q.den

q : ℚ
⊢ (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ p = q

Tactic:
rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]

Goal state after:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑p.num * ↑q.den = ↑q.num * ↑p.den

case hb
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑p.den ≠ 0

case hd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑q.den ≠ 0
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
q : ℚ≥0
⊢ ↑q = 0 ↔ q = 0

Tactic:
← cast_zero,

Goal state after:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
q : ℚ≥0
⊢ ↑q = ↑0 ↔ q = 0
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(Int.negOfNat n.succ) * ⅟↑d)⁻¹ (Int.negOfNat d) n.succ

Tactic:
simp only [Int.negOfNat_eq]

Goal state after:
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(-Int.ofNat n.succ) * ⅟↑d)⁻¹ (-Int.ofNat d) n.succ
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * a - b * b = a * a + a * b - a * b - b * b

Tactic:
add_tsub_cancel_right

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * a - b * b = a * a - b * b
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * a - b * b = (a + b) * (a - b)

Tactic:
rw [mul_tsub, add_mul, add_mul, tsub_add_eq_tsub_tsub, mul_comm b a, add_tsub_cancel_right]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
c k : ℕ
⊢ a ^ (c * k) = (a ^ c) ^ k

Tactic:
simp [pow_mul]

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

Goal state before:
pp: case e'_4.succ
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ f (n + 1) (rec (f 0 x) (f ∘ succ) n) = f (n + 1) (f n (rec x f n))

Tactic:
ihn

Goal state after:
case e'_4.succ
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ f (n + 1) (f n (rec x f n)) = f (n + 1) (f n (rec x f n))
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋃ i, ⋃ j, s i j)ᶜ = ⋂ i, ⋂ j, (s i j)ᶜ

Tactic:
by
  simp_rw [compl_iUnion]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ x ∈ ∅, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ ∅, y ≤ x
⊢ sSup ∅ = sSup t

Tactic:
have : t = ∅ := eq_empty_of_forall_notMem (fun y yt ↦ by simpa using ht y yt)
    rw [this]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
⊢ (Disjoint on fun a ↦ f a '' t) x y

Tactic:
refine disjoint_iff_inf_le.mpr ?_

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
⊢ (fun a ↦ f a '' t) x ⊓ (fun a ↦ f a '' t) y ⊆ ⊥
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (Disjoint on fun b ↦ (fun a ↦ f a b) '' s) x y

Tactic:
refine disjoint_iff_inf_le.mpr ?_

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (fun b ↦ (fun a ↦ f a b) '' s) x ⊓ (fun b ↦ (fun a ↦ f a b) '' s) y ⊆ ⊥
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
⊢ CompleteAtomicBooleanAlgebra α

Tactic:
apply e.injective.completeAtomicBooleanAlgebra <;> intros <;>
  first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := ⋯
x : β
xt : x ∈ t
y : β
yt : y ∈ t
yx : y ≤ x
ys : f y ∈ s
z : β
zt : z ∈ t
xz : x ≤ z
zs : f z ∈ s
⊢ f x ∈ Icc (f y) (f z)

Tactic:
exact ⟨hf yt xt yx, hf xt zt xz⟩

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

Goal state before:
pp: a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
⊢ a / b = ↑q'

Tactic:
by rw [Int.cast_id, ← hq, ← @Int.cast_id q, ← h.out, ← Int.ediv_neg, Int.neg_neg]

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
⊢ Injective fun a ↦ (a⁺ᵐ, a⁻ᵐ)

Tactic:
simp only [Injective, Prod.mk.injEq, and_imp]

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
⊢ ∀ ⦃a₁ a₂ : α⦄, a₁⁺ᵐ = a₂⁺ᵐ → a₁⁻ᵐ = a₂⁻ᵐ → a₁ = a₂
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ * a = a⁺ᵐ * ?c * (a⁺ᵐ / ?c)

pp: case c
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ α

Tactic:
oneLePart_mul_leOnePart,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ * a = |a|ₘ * (a⁺ᵐ / a⁻ᵐ)
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ * a = a⁺ᵐ ^ 2

Tactic:
mabs_mul_eq_oneLePart_sq

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ a⁺ᵐ ^ 2 = a⁺ᵐ ^ 2
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ / a = ?a * a⁻ᵐ / (?a / a⁻ᵐ)

pp: case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ α

Tactic:
oneLePart_mul_leOnePart,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ / a = |a|ₘ / (a⁺ᵐ / a⁻ᵐ)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
hn : 0 < n
⊢ n ! < m ! ↔ n < m

Tactic:
refine ⟨fun h => not_le.mp fun hmn => Nat.not_le_of_gt h (factorial_le hmn), fun h => ?_⟩
  have : ∀ {n}, 0 < n → n ! < (n + 1)! := by
    intro k hk
    rw [factorial_succ, succ_mul, Nat.lt_add_left_iff_pos]
    exact Nat.mul_pos hk k.factorial_pos
  induction h generalizing hn with
  | refl => exact this hn
  | step hnk ih => exact lt_trans (ih hn) <| this <| lt_trans hn <| lt_of_succ_le hnk

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Group α
a b : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
⊢ a⁻¹ < b ∧ 1 < b ↔ b⁻¹ < a ∧ 1 < b

Tactic:
rw [inv_lt']

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

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

Tactic:
· rw [descFactorial_eq_zero_iff_lt.mpr (show n < k by lia), Nat.mul_zero]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ ⌊x⌋ + ⌊fract x⌋ = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2

Tactic:
congr 1

Goal state after:
case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ ⌊fract x⌋ = (⌊2 * fract x⌋ + 1) / 2
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case neg
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : ¬2 * fract x < 1
⊢ ⌊x⌋ + ⌈fract x⌉ = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2

Tactic:
congr 1

Goal state after:
case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : ¬2 * fract x < 1
⊢ ⌈fract x⌉ = (⌊2 * fract x⌋ + 1) / 2
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case pos
m k : ℕ+
h : ↑m % ↑k = 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k

pp: case neg
m k : ℕ+
h : ¬↑m % ↑k = 0
⊢ ↑m % ↑k ≤ ↑m ∧ ↑m % ↑k ≤ ↑k

Tactic:
· have hm : (m : ℕ) > 0 := m.pos
    rw [← Nat.mod_add_div (m : ℕ) (k : ℕ), h, zero_add] at hm ⊢
    simp
    lia

Goal state after:
case neg
m k : ℕ+
h : ¬↑m % ↑k = 0
⊢ ↑m % ↑k ≤ ↑m ∧ ↑m % ↑k ≤ ↑k
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
⊢ ⌊0⌋ = 0

Tactic:
← cast_zero,

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

Goal state before:
pp: case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑n * (↑(m % n) / ↑n) + ↑n * ↑(↑m / ↑n)

Tactic:
mul_div_cancel₀ _ hn'.ne'

Goal state after:
case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑(m % n) + ↑n * ↑(↑m / ↑n)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ ↑l₀
⊢ fract (↑l₀ / ↑n) = ↑(l₀ % n) / ↑n

Tactic:
fract_div_natCast_eq_div_natCast_mod

Goal state after:
case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ ↑l₀
⊢ ↑(l₀ % n) / ↑n = ↑(l₀ % n) / ↑n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
⊢ ⌈0⌉ = 0

Tactic:
← cast_zero,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
⊢ ⌈↑0⌉ = 0
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
y x : R
hy : 0 < y
this : 0 ≤ 1 + y
n : ℕ
h : x ≤ n • y
⊢ (1 + y) ^ n = (y + 1) ^ n

Tactic:
by rw [add_comm]

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

Goal state before:
pp: n d : ℕ
n_coprime_d : n.Coprime d
this✝ : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
this : d.Coprime n
⊢ (↑n % ↑d).natAbs.Coprime d

Tactic:
rwa [Nat.Coprime, Nat.gcd_rec] at this

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

Goal state before:
pp: case inl
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 : a ≤ 0
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

pp: case 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
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
· obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hb₀ hc₁
    exact ⟨n, ha.trans_lt (zpow_pos hc₀ _), mod_cast hn⟩

Goal state after:
case 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
⊢ ∃ n, a < c ^ n ∧ c ^ n < b
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ g • ↑m * g⁻¹ • ↑m⁻¹ = 1

Tactic:
by rw [smul_mul_smul_comm, Units.mul_inv, mul_inv_cancel, one_smul]

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

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
by
  have ⟨δ, δ_pos, cont⟩ := uniform_continuous_npow_on_bounded (max 1 y)
    (sub_pos.mpr <| max_lt_iff.mpr ⟨h, hy⟩) n
  have ex : ∃ m : ℕ, y ≤ (m * δ) ^ n := by
    have ⟨m, hm⟩ := exists_nat_ge (y / δ + 1 / δ)
    refine ⟨m, le_trans ?_ (le_self_pow₀ ?_ hn)⟩ <;> rw [← div_le_iff₀ δ_pos]
    · exact (lt_add_of_pos_right _ <| by positivity).le.trans hm
    · exact (le_add_of_nonneg_left <| by positivity).trans hm
  let m := Nat.find ex
  have m_pos : 0 < m := (Nat.find_pos _).mpr <| by simpa [zero_pow hn] using hy
  let q := m.pred * δ
  have qny : q ^ n < y := lt_of_not_ge (Nat.find_min ex <| Nat.pred_lt m_pos.ne')
  have q1y : |q| < max 1 y := (abs_eq_self.mpr <| by positivity).trans_lt <| lt_max_iff.mpr
    (or_iff_not_imp_left.mpr fun q1 ↦ (le_self_pow₀ (le_of_not_gt q1) hn).trans_lt qny)
  have xqn : max x 0 < q ^ n :=
    calc _ = y - (y - max x 0) := by rw [sub_sub_cancel]
      _ ≤ (m * δ) ^ n - (y - max x 0) := sub_le_sub_right (Nat.find_spec ex) _
      _ < (m * δ) ^ n - ((m * δ) ^ n - q ^ n) := by
        refine sub_lt_sub_left ((le_abs_self _).trans_lt <| cont _ _ q1y.le ?_) _
        rw [← Nat.succ_pred_eq_of_pos m_pos, Nat.cast_succ, ← sub_mul,
          add_sub_cancel_left, one_mul, abs_eq_self.mpr (by positivity)]
      _ = q ^ n := sub_sub_cancel ..
  exact ⟨q, lt_of_le_of_ne (by positivity) fun q0 ↦
    (le_sup_right.trans_lt xqn).ne <| q0 ▸ (zero_pow hn).symm, le_sup_left.trans_lt xqn, qny⟩

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

Goal state before:
pp: case coe
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
x : WithZero M
y : M
hxy : 1 < ↑y
⊢ ∃ n, x ≤ ↑y ^ n

Tactic:
cases x with
    | zero => refine ⟨0, zero_le⟩
    | coe x => simpa [← WithZero.coe_pow] using (MulArchimedean.arch x (by simpa using hxy))

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
s t : Set P
⊢ 1 ∈ s /ₛ t ↔ ¬Disjoint s t

Tactic:
simp [not_disjoint_iff_nonempty_inter, mem_sdiv, Set.Nonempty]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
C : Multiset α → Sort u_3
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)
m : Multiset α
x✝² x✝¹ : List α
h : x✝² ≈ x✝¹
a✝ : α
l✝ l'✝ : List α
b✝ : C ⟦l✝⟧
b'✝ : C ⟦l'✝⟧
hl : l✝ ~ l'✝
x✝ : b✝ ≍ b'✝
⊢ C_cons a✝ ⟦l✝⟧ b✝ ≍ C_cons a✝ ⟦l'✝⟧ b'✝

Tactic:
congr 1

Goal state after:
case e_2
α : Type u_1
β : Type v
γ : Type u_2
C : Multiset α → Sort u_3
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)
m : Multiset α
x✝² x✝¹ : List α
h : x✝² ≈ x✝¹
a✝ : α
l✝ l'✝ : List α
b✝ : C ⟦l✝⟧
b'✝ : C ⟦l'✝⟧
hl : l✝ ~ l'✝
x✝ : b✝ ≍ b'✝
⊢ ⟦l✝⟧ = ⟦l'✝⟧
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ s + a ::ₘ t = a ::ₘ (s + t)

Tactic:
by
  rw [Multiset.add_comm, cons_add, Multiset.add_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = count a ⟦l⟧ - 1

Tactic:
convert! List.count_erase_self (a := a) (l := l) <;> rw [← coe_count] <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
a✝ : α
⊢ count a✝ (s - {a}) = count a✝ (s.erase a)

Tactic:
simp only [count_sub, count_singleton]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
a✝ : α
⊢ (count a✝ s - if a✝ = a then 1 else 0) = count a✝ (s.erase a)