mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ l[idxOf a l]? = some a

Tactic:
rw [getElem?_eq_getElem (idxOf_lt_length_iff.2 h), getElem_idxOf]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → Option β
g : α → β
l : List α
h : ∀ (x : α), x ∈ l → f x = some (g x)
⊢ ∀ (x : α), x ∈ l → f x = (some ∘ g) x

Tactic:
simpa

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

Goal state before:
pp: case cons
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ L.length + 1 ≤ j + L.sum

Tactic:
add_comm

Goal state after:
case cons
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ 1 + L.length ≤ j + L.sum
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case cons
ι : Type u_1
inst✝¹ : BEq ι
inst✝ : LawfulBEq ι
a : ι
l : List ι
IH : ∀ {i : ℕ} (hi : i < l.length), l.erase l[i] ~ l.eraseIdx i
i : ℕ
hi : i < (a :: l).length
⊢ (a :: l).erase (a :: l)[i] ~ (a :: l).eraseIdx i

Tactic:
cases i with grind

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (x * y) (x * z) ↔ IsRelPrime y z

Tactic:
by
  rw [isRelPrime_mul_unit_left_left hu, isRelPrime_mul_unit_left_right hu]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (x * y) z ↔ IsRelPrime y z

Tactic:
isRelPrime_mul_unit_left_left hu

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y z ↔ IsRelPrime y z
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : ↑(n₁ /. ↑d₁) = ↑(n₂ /. ↑d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ ↑↑d₁ ≠ 0

Tactic:
simpa

Goal state after:
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : ↑n₁ / ↑↑d₁ = ↑(n₂ /. ↑d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ ↑↑d₂ ≠ 0

Tactic:
simpa

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(divNat (q.num * r.den + r.num * q.den) (q.den * r.den)) = ↑q + ↑r

Tactic:
cast_divNat_of_ne_zero,

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * r.den + r.num * q.den) / ↑(q.den * r.den) = ↑q + ↑r

case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(divNat (q.num * r.num) (q.den * r.den)) = ↑q * ↑r

Tactic:
cast_divNat_of_ne_zero,

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * r.num) / ↑(q.den * r.den) = ↑q * ↑r

case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(divNat (q.num * r.den) (q.den * r.num)) = ↑q / ↑r

Tactic:
cast_divNat_of_ne_zero,

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.num * r.den) / ↑(q.den * r.num) = ↑q / ↑r

case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.den * r.num) ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n
⊢ ∀ {n : ℕ},
    0 < n →
      ((MonoidWithZeroHom.ofClass f).comp (MonoidWithZeroHom.ofClass (Nat.castRingHom ℚ≥0))) n =
        ((MonoidWithZeroHom.ofClass g).comp (MonoidWithZeroHom.ofClass (Nat.castRingHom ℚ≥0))) n

Tactic:
simpa

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

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
same_on_neg_one : f (-1) = g (-1)
same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n
⊢ ((MonoidWithZeroHom.ofClass f).comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ))) (-1) =
    ((MonoidWithZeroHom.ofClass g).comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ))) (-1)

Tactic:
simpa

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

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
same_on_neg_one : f (-1) = g (-1)
same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n
⊢ ∀ (n : ℕ),
    0 < n →
      ((MonoidWithZeroHom.ofClass f).comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ))) ↑n =
        ((MonoidWithZeroHom.ofClass g).comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ))) ↑n

Tactic:
simpa

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

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : 0 < b
this : -b * a > 0
⊢ 0 < -(b * a)

Tactic:
simpa

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

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a ≤ 0
hb : 0 < b
this : -b * a ≥ 0
⊢ b * a ≤ 0

Tactic:
simpa

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

Goal state before:
pp: α β : Type u_2
inst : CSLift α β
a b : α
a' b' : β
h1 : CSLiftVal a a'
h2 : CSLiftVal b b'
h : a' = b'
⊢ CSLift.lift a = CSLift.lift b

Tactic:
by rwa [← h1.1, ← h2.1]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a b c d : R
x✝¹ : -b = c
x✝ : a + c = d
⊢ a - b = d

Tactic:
subst_vars; simp [sub_eq_add_neg]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone fun n ↦ ⨅ i, ⨅ (_ : i ≥ n), f i
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n + k), f i

Tactic:
iInf_ge_eq_iInf_nat_add,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone fun n ↦ ⨅ i, ⨅ (_ : i ≥ n), f i
⊢ ⨆ n, ⨅ i, f (i + n + k) = ⨆ n, ⨅ i, f (i + (n + k))
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (x ∈ ⋃ y, range fun x ↦ ↑(f x y)) ↔ x ∈ ⋃ x, C x

Tactic:
mem_iUnion,

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ range fun x ↦ ↑(f x i)) ↔ x ∈ ⋃ x, C x
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : Preorder α
inst✝ : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), Monotone (f i)
⊢ ∀ f_1 ∈ range fun i ↦ f i, Monotone f_1

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : Preorder α
inst✝ : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), Antitone (f i)
⊢ ∀ f_1 ∈ range fun i ↦ f i, Antitone f_1

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : CompleteLattice β
s : ι → Set α
f : α → β
⊢ ⨆ a ∈ ⋃ i, s i, f a = ⨆ j, ⨆ i, ⨆ (_ : j ∈ s i), f j

Tactic:
mem_iUnion,

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : CompleteLattice β
s : ι → Set α
f : α → β
⊢ ⨆ a, ⨆ (_ : ∃ i, a ∈ s i), f a = ⨆ j, ⨆ i, ⨆ (_ : j ∈ s i), f j
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
⊢ (sSup s)ᶜ = ⨅ i ∈ s, iᶜ

Tactic:
simp only [sSup_eq_iSup, compl_iSup]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Ioi b ⊂ Ioi a
left✝ : Ioi b ⊆ Ioi a
c : α
ac : c ∈ Ioi a
cb : ¬c ∈ Ioi b
⊢ a < b

Tactic:
exact ac.trans_le (le_of_not_gt cb)

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ⊆ f i
hfj : t ⊆ f j
ht : ¬t = ∅
⊢ t.Nonempty

Tactic:
← Ne,

Goal state after:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ⊆ f i
hfj : t ⊆ f j
ht : t ≠ ∅
⊢ t.Nonempty
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: case inl
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx hy : x ∈ s
hxy : x ≤ x
⊢ Icc x x ⊆ s

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : s.OrdConnected
x y : ↑s
⊢ (range ⇑(OrderEmbedding.subtype fun x ↦ x ∈ s)).OrdConnected

Tactic:
simpa

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

Goal state before:
pp: α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b : β
ab : a ≤ b
c : β
⊢ f (a * c) ≤ f (b * c)

Tactic:
rw [mul, mul]; grw [le.2 ab]

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 = a / - -b

Tactic:
Int.neg_neg

Goal state after:
a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
⊢ a / b = a / b
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
← cast_le (K := K),

Goal state after:
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℕ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ ↑↑n
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℕ
n : ℚ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
← cast_le (K := K),

Goal state after:
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℕ
n : ℚ
⊢ ↑m ≤ ↑n ↔ ↑↑m ≤ ↑n
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℤ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
← cast_le (K := K),

Goal state after:
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℤ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ ↑↑n
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℤ
n : ℚ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
← cast_le (K := K),

Goal state after:
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℤ
n : ℚ
⊢ ↑m ≤ ↑n ↔ ↑↑m ≤ ↑n
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ≥0
n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
← cast_le (K := K),

Goal state after:
K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ≥0
n : ℕ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ ↑↑n
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℕ
n : ℚ≥0
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
← cast_le (K := K),

Goal state after:
K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℕ
n : ℚ≥0
⊢ ↑m ≤ ↑n ↔ ↑↑m ≤ ↑n
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
⊢ a⁺ᵐ / a⁻ᵐ = b

Tactic:
← oneLePart_div_leOnePart b,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
⊢ a⁺ᵐ / a⁻ᵐ = b⁺ᵐ / b⁻ᵐ
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
ha : 1 < a⁺ᵐ
⊢ a⁺ᵐ = a

Tactic:
by
  rw [oneLePart_def, right_lt_sup, not_le] at ha; exact oneLePart_eq_self.2 ha.le

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

Goal state before:
pp: n k : ℕ
⊢ (n - k) ^ k ≤ n.descFactorial k

Tactic:
exact (le_trans (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) k)
      (pow_sub_le_descFactorial n k))

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
q : ℚ
h : 0 ≤ q
⊢ 0 ≤ q.num

Tactic:
simpa

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
this : fract x < 1
⊢ fract x ∈ Ico 0 1

Tactic:
simpa

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

Goal state before:
pp: k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * q = ↑k * q + ↑k

Tactic:
add_comm

Goal state after:
k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k * q + ↑k = ↑k * q + ↑k
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round x + y = y + round x

Tactic:
add_comm

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ y + round x = y + round x
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℕ
⊢ round x + ↑y = ↑y + round x

Tactic:
add_comm

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℕ
⊢ ↑y + round x = ↑y + round x
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
x k : R
hk : 1 < k
⊢ k * fract x = 1 ↔ ∃ n, k * x = k * ↑n + 1

Tactic:
rw [fract, mul_sub, sub_eq_iff_eq_add']
  refine ⟨fun hx ↦ ⟨⌊x⌋, hx⟩, ?_⟩
  rintro ⟨n, hn⟩
  convert! hn
  have hk0 : 0 < (k : R) := zero_le_one.trans_lt hk
  rw [floor_eq_iff, ← mul_le_mul_iff_right₀ hk0, ← mul_lt_mul_iff_right₀ hk0, hn]
  simp [mul_add, hk]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
⊢ ¬IsCyclic α

Tactic:
intro h
  rcases exists_zpow_surjective α with ⟨a, ha⟩
  rcases lt_trichotomy a 1 with hlt | rfl | hlt
  · rcases exists_between hlt with ⟨b, hab, hb⟩
    rcases ha b with ⟨k, rfl⟩
    suffices 0 < k ∧ k < 1 by lia
    rw [← one_lt_inv'] at hlt
    simp_rw [← zpow_lt_zpow_iff_right hlt]
    simp_all
  · rcases exists_ne (1 : α) with ⟨b, hb⟩
    simpa [hb.symm] using ha b
  · rcases exists_between hlt with ⟨b, hb, hba⟩
    rcases ha b with ⟨k, rfl⟩
    suffices 0 < k ∧ k < 1 by lia
    simp_rw [← zpow_lt_zpow_iff_right hlt]
    simp_all

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

Goal state before:
pp: case mpr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
x : R
⊢ (∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1) → ∃ x_1 ∈ s, fract x_1 = x

Tactic:
· rintro ⟨m, ⟨y, hys, rfl⟩, h0, h1⟩
    obtain rfl : ⌊y⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 h0, sub_lt_iff_lt_add'.1 h1⟩
    exact ⟨y, hys, rfl⟩

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

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
b a : k
hb : 0 < b
⊢ a / b < 1 + ↑⌊a / b⌋

Tactic:
add_comm

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
b a : k
hb : 0 < b
⊢ a / b < ↑⌊a / b⌋ + 1
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
z : ℤ
a : R
⊢ ⌈a⌉ + z = z + ⌈a⌉

Tactic:
add_comm

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
z : ℤ
a : R
⊢ z + ⌈a⌉ = z + ⌈a⌉
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
r : α
n d : ℕ
⊢ IsRat r (negOfNat n) d → IsRat (fract r) (-↑n % ↑d) d

Tactic:
by
  rintro ⟨inv, rfl⟩
  refine ⟨inv, ?_⟩
  simp only [invOf_eq_inv, ← div_eq_mul_inv, fract_div_intCast_eq_div_intCast_mod,
    negOfNat_eq, ofNat_eq_natCast]

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

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! x, b * a ^ (Equiv.addRight 1) x ∈ Ioc c (c * a)

Tactic:
by
    simpa only [zpow_add_one, div_lt_iff_lt_mul', le_div_iff_mul_le', ← mul_assoc, and_comm,
      mem_Ioc, Equiv.coe_addRight, mul_le_mul_iff_right] using
      existsUnique_zpow_near_of_one_lt ha (c / b)

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

Goal state after:
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
⊢ (y + 1) ^ n = (y + 1) ^ n
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
inst✝ : ExistsAddOfLE R
x z : R
hz : 0 < z
hy1 : 1 < 1 + z
⊢ ∃ n, x < (1 + z) ^ n

Tactic:
add_comm

Goal state after:
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
inst✝ : ExistsAddOfLE R
x z : R
hz : 0 < z
hy1 : 1 < 1 + z
⊢ ∃ n, x < (z + 1) ^ n
Module: Mathlib.Data.Rat.Floor

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

Tactic:
← this

Goal state after:
n d : ℕ
n_coprime_d : n.Coprime d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ (↑n % ↑d).natAbs.Coprime d
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
this : ∀ (x y : G), x < y → x ∈ Ico l (l + a) → R (f x) (f y)
hx : x ∉ Ico l (l + a)
m : ℤ
hm : x - m • a ∈ Ico l (l + a)
⊢ x - m • a < y - m • a

Tactic:
simpa

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

Goal state before:
pp: q : ℚ
this : 0 < (1 - fract q) * ↑q.den
⊢ ↑q.num - ↑q.num < (1 - fract q) * ↑q.den

Tactic:
simpa

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

Goal state before:

Tactic:
⌈a⌉ ≤ (⌈(b - 1)⁻¹⌉ : k) := by gcongr
      _ < b * a := by rwa [← div_lt_iff₀']; positivity

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

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : q.den.Coprime q.num.natAbs
this : (↑q.den).natAbs = q.den
⊢ q_inv.num = ↑q.den ∧ q_inv.den = q.num.natAbs

Tactic:
← this

Goal state after:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : (↑q.den).natAbs.Coprime q.num.natAbs
this : (↑q.den).natAbs = q.den
⊢ q_inv.num = ↑q.den ∧ q_inv.den = q.num.natAbs
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
⊢ l ∈ Icc l (l + a)

Tactic:
simpa

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

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : ↑q.den - ⌊q_inv⌋ * ↑q.num.natAbs < ↑q.num.natAbs
this : q_inv.num = ↑q.den ∧ q_inv.den = q.num.natAbs
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num

Tactic:
q_num_abs_eq_q_num,

Goal state after:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : ↑q.den - ⌊q_inv⌋ * q.num < q.num
this : q_inv.num = ↑q.den ∧ q_inv.den = q.num.natAbs
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: case refine_1
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
k : ℤ
⊢ l ∈ Icc l (l + a)

Tactic:
simpa

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

Goal state before:
pp: case refine_2
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
k : ℤ
⊢ l + a ∈ Icc l (l + a)

Tactic:
simpa

Goal state after: