mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atTop

Tactic:
by

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

Goal state before:
pp: ⊢ φ 2 = 1 ↔ 2 = 1 ∨ 2 = 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
this : 3 ≤ n + 3
⊢ n + 3 = 2 → φ (n + 3) = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) atBot atBot

Tactic:
by

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

Goal state before:
pp: a : ℕ
han : 0 < a
ha : φ a ≤ 1
⊢ a ∣ 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Odd (φ n) ↔ φ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) atTop atTop

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsCodirectedOrder α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ a, ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsCodirectedOrder α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ a, ∀ k ≤ a, ∀ l ≤ a, p (k, l)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atTop, p x) ↔ ∃ a, ∀ k ≥ a, ∀ l ≥ a, p (k, l)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ k < n, ∀ᶠ (a : ℕ) in atTop, p (n * a + k)
⊢ ∀ᶠ (a : ℕ) in atTop, p a

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ (φ m).Coprime (φ n) ↔ (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ φ n = n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
⊢ ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atTop.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atTop.IsCountablyGenerated
⊢ atTop.IsCountablyGenerated

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atBot.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atBot.IsCountablyGenerated
⊢ atBot.IsCountablyGenerated

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : f.NeBot
⊢ ∃ x, Tendsto x atTop f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirectedOrder α
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n ↦ List.foldl (fun x n ↦ c x (ys n)) (ys 0) (List.range n)
n : ℕ
⊢ xs (n + 1) = c (xs n) (ys n)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: case inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

Tactic:
refine (lt_of_lt_of_le ?_ Nat.factorial_mul_pow_le_factorial).trans_le <|
    (factorial_le (Nat.le_succ _))

Goal state after:
case inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2)! * (c ^ 2 + 1) ^ (c ^ 2 + d' + d + 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
⊢ φ n = (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : ¬n = 0
⊢ ↑n ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ∏ p ∈ n.primeFactors, ↑p ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: c d : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop, c ^ n < (n - d)!

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirectedOrder α
inst✝ : atTop.IsCountablyGenerated
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
⊢ Tendsto f k l ↔ ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l

Tactic:
refine ⟨fun h x hx => h.comp hx, fun H s hs => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
H : ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l
s : Set β
hs : s ∈ l
⊢ s ∈ map f k
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: a c d : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop, a * c ^ n < (n - d)!

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
⊢ (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
⊢ Tendsto f k l ↔ ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)

Tactic:
by

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

Goal state before:
pp: a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2)

Tactic:
by

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

Goal state before:
pp: a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * (a2 / b2) * (c1 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)

Tactic:
by

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

Goal state before:
pp: a b : ℕ
⊢ ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∃ᶠ (n : ι) in l, p n) ↔ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Curry

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
p : α × β → Prop
⊢ (∃ᶠ (x : α × β) in l.curry m, p x) ↔ ∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, p (x, y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Curry

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
s : Set α
t : Set β
⊢ (∃ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ (∃ᶠ (x : α) in l, x ∈ s) ∧ ∃ᶠ (y : β) in m, y ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
h : ∃ᶠ (n : ι) in l, p n
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.Curry

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
s : Set α
t : Set β
inst✝¹ : l.NeBot
inst✝ : m.NeBot
⊢ (∀ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst✝ : l.IsCountablyGenerated
hxy : ¬Tendsto x l f
⊢ ∃ s ∈ f, ∃ᶠ (n : ι) in l, x n ∉ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst✝ : l.IsCountablyGenerated
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n ↦ x (ns (ms n))) atTop f
⊢ Tendsto x l f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι : Type u_3
g : Filter ι
inst✝¹ : g.IsCountablyGenerated
u : ι → α
f : Filter α
inst✝ : f.IsCountablyGenerated
hx : (f ⊓ map u g).NeBot
⊢ ∃ θ, Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
u : ℕ → α
hx : (f ⊓ map u atTop).NeBot
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Tactic:
by

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

Goal state before:
pp: a b : ℕ
⊢ φ (a.gcd b) * φ (a * b) = φ a * φ b * a.gcd b

Tactic:
by

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

Goal state before:
pp: a b : ℕ
⊢ φ a * φ b ≤ φ (a * b)

Tactic:
by

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

Goal state before:
pp: a b : ℕ
h : a ∣ b
⊢ φ a ∣ φ b

Tactic:
by

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

Goal state before:
pp: p n : ℕ
hp : Prime p
h : p ∣ n
⊢ φ (p * n) = p * φ n

Tactic:
by

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

Goal state before:
pp: p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ φ (p * n) = (p - 1) * φ n

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ φ (2 * n) = φ n

Tactic:
by

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

Goal state before:
pp: a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
this : a.Coprime c
⊢ a = a * c ∨ 2 * a = a * c

Tactic:
by

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

Goal state before:
pp: a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
this : φ a < φ (p * a * d)
⊢ False

Tactic:
by

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

Goal state before:
pp: a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ a * p * d ≠ 0

Tactic:
by

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

Goal state before:
pp: a b : ℕ
h : a ∣ b
h' : φ a = φ b
⊢ a = b ∨ 2 * a = b

Tactic:
by

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

Goal state before:
pp: a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
⊢ a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
b : α
⊢ toIcoMod hp 0 b ∈ Set.Ico 0 p

Tactic:
by

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

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
⊢ p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b • p - b = -toIcoMod hp a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b • p - b = -toIocMod hp a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b - b = -toIcoDiv hp a b • p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b - b = -toIocDiv hp a b • p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIcoMod hp a b = toIcoDiv hp a b • p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIocMod hp a b = toIocDiv hp a b • p

Tactic:
by

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

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
⊢ (p ^ k) ^ φ (p ^ k) / ∏ q ∈ (p ^ k).primeFactors, q ^ (φ (p ^ k) / (q - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b + toIcoDiv hp a b • p = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b + toIocDiv hp a b • p = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b • p + toIcoMod hp a b = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b • p + toIocMod hp a b = b

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) ∣ n ^ φ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoMod hp a b = c ↔ c ∈ Set.Ico a (a + p) ∧ ∃ z, b = c + z • p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocMod hp a b = c ↔ c ∈ Set.Ioc a (a + p) ∧ ∃ z, b = c + z • p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a - 0 • p ∈ Set.Ico a (a + p)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a - -1 • p ∈ Set.Ioc a (a + p)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a = a + 0 • p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ toIcoMod hp a a = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a = a + p + -1 • p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ toIocMod hp a a = a + p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a + p - 1 • p ∈ Set.Ico a (a + p)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a + p - 0 • p ∈ Set.Ioc a (a + p)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a + p = a + 1 • p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ toIcoMod hp a (a + p) = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a + p = a + p + 0 • p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ toIocMod hp a (a + p) = a + p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b + m • p - (toIcoDiv hp a b + m) • p ∈ Set.Ico a (a + p)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp (a + m • p) b = toIcoDiv hp a b - m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b + m • p - (toIocDiv hp a b + m) • p ∈ Set.Ioc a (a + p)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp (a + m • p) b = toIocDiv hp a b - m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp a (m • p + b) = m + toIcoDiv hp a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp a (m • p + b) = m + toIocDiv hp a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp (a - m • p) b = toIcoDiv hp a b + m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp a (b - m • p) = toIocDiv hp a b - m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp (a - m • p) b = toIocDiv hp a b + m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a (b + p) = toIcoDiv hp a b + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp (a + p) b = toIcoDiv hp a b - 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a (b + p) = toIocDiv hp a b + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp (a + p) b = toIocDiv hp a b - 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a (p + b) = toIcoDiv hp a b + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp (p + a) b = toIcoDiv hp a b - 1

Tactic:
by

Goal state after: