mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ {a ∈ range (p ^ (n + 1)) | (p ^ (n + 1)).Coprime a} =
    {x ∈ range (p ^ (n + 1)) | x ∉ image (fun x ↦ x * p) (range (p ^ n))}

Tactic:
]

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
⊢ {a ∈ range (p ^ (n + 1)) | (p ^ (n + 1)).Coprime a} =
    {x ∈ range (p ^ (n + 1)) | x ∉ image (fun x ↦ x * p) (range (p ^ n))}
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mpr
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p * p ^ n
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False

Tactic:
]

Goal state after:
case mpr
p : ℕ
hp : Prime p
n b : ℕ
ha : p * b < p * p ^ n
h : ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = p * b)
⊢ False
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ n * p

Tactic:
]

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
b : ℕ
h : b < p ^ n
⊢ b * p < p ^ n * p
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ p ^ n * (p - 1) = p ^ n * (p - 1)

Tactic:
]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atTop
h_evtl : ∀ᶠ (x : β) in atTop, ∀ (y : β), x ≤ y → p y
⊢ ∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atTop
h_evtl : ∀ᶠ (x : β) in atTop, ∀ (y : β), x ≤ y → p y
⊢ ∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p ^ (1 - 1) * (p - 1) = p ^ 1 - 1

pp: p : ℕ
hp : Prime p
⊢ 0 < 1

Tactic:
]

Goal state after:
p : ℕ
hp : Prime p
⊢ p ^ (1 - 1) * (p - 1) = p ^ 1 - 1

p : ℕ
hp : Prime p
⊢ 0 < 1
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, ∀ y ≤ x, p y
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, ∀ y ≤ x, p y
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 0 < p

Tactic:
]

Goal state after:
case a
p : ℕ
hp : 0 < p
h : φ p = p - 1
⊢ 0 < p
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: case hf
ι : Type u_1
ι' : Type u_2
⊢ Monotone fun p ↦ p.1 ×ˢ p.2

pp: case h
ι : Type u_1
ι' : Type u_2
⊢ ∀ (b : Finset (ι × ι')), ∃ a, b ⊆ a.1 ×ˢ a.2

Tactic:
· intro p q hpq
    simpa using Finset.product_subset_product hpq.1 hpq.2

Goal state after:
case h
ι : Type u_1
ι' : Type u_2
⊢ ∀ (b : Finset (ι × ι')), ∃ a, b ⊆ a.1 ×ˢ a.2
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case a
hp : 0 < 1
h : 1 = 0
⊢ False

Tactic:
]

Goal state after:
case a
hp : 0 < 1
h : 1 = 0
⊢ False
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
h : #({a ∈ Ico (0 + 1) p | p.Coprime a}) = #(Ico 1 p)
hp : 1 < p
⊢ Prime p

Tactic:
]

Goal state after:
p : ℕ
h : #({a ∈ Ico (0 + 1) p | p.Coprime a}) = #(Ico 1 p)
hp : 1 < p
⊢ Prime p
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α₁ : Type u_6
α₂ : Type u_7
β₁ : Type u_8
β₂ : Type u_9
inst✝¹ : Preorder β₁
inst✝ : Preorder β₂
u₁ : β₁ → α₁
u₂ : β₂ → α₂
⊢ map (fun p ↦ (u₁ p.1, u₂ p.2)) atTop = map (fun p ↦ (u₁ p.1, u₂ p.2)) atTop

Tactic:
]

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

Goal state before:
pp: p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
this : NeZero p
⊢ φ p ≤ p - 1

Tactic:
]

Goal state after:
p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
this : NeZero p
⊢ φ p ≤ p - 1
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atBot (atBot ×ˢ atBot)

Tactic:
]

Goal state after:
α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atBot (atBot ×ˢ atBot)
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atTop (atTop ×ˢ atTop)

Tactic:
]

Goal state after:
α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atTop (atTop ×ˢ atTop)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : NeZero p
⊢ Prime p ↔ Prime p

Tactic:
]

Goal state after:
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 atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atBot ×ˢ atBot)

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atBot ×ˢ atBot)
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 ×ˢ atTop)

Tactic:
]

Goal state after:
α : 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 ×ˢ atTop)
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) atBot

Tactic:
]

Goal state after:
α : 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) atBot
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
⊢ p (n * (b / n) + b % n)

Tactic:
]

Goal state after:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
⊢ p (n * (b / n) + b % n)
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) atTop

Tactic:
]

Goal state after:
α : 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) atTop
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mp
m n : ℕ
⊢ ¬((m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2) → ¬(φ m).Coprime (φ n)

Tactic:
]

Goal state after:
case mp
m n : ℕ
⊢ ¬((m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2) → ¬(φ m).Coprime (φ n)
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 ×ˢ atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop ×ˢ atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
hlt : b % n < n
⊢ n * N (b % n) ≤ b

Tactic:
]

Goal state after:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
hlt : b % n < n
⊢ n * N (b % n) ≤ b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mpr.inl
m n : ℕ
h : φ m = 1
⊢ Coprime 1 (φ n)

Tactic:
]

Goal state after:
case mpr.inl
m n : ℕ
h : φ m = 1
⊢ Coprime 1 (φ n)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mpr.inr
m n : ℕ
h : φ n = 1
⊢ (φ m).Coprime 1

Tactic:
]

Goal state after:
case mpr.inr
m n : ℕ
h : φ n = 1
⊢ (φ m).Coprime 1
Module: Mathlib.Data.Nat.Totient

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

Tactic:
]

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k ↦ φ (p ^ k)) = n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.factorization.support
h : 0 < n.factorization p
⊢ p ^ (n.factorization p - 1) * (p - 1) = p ^ (n.factorization p - 1) * (p - 1)

Tactic:
]

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

Goal state before:
pp: c d : ℕ
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → c ^ b < (b - d)!

Tactic:
]

Goal state after:
c d : ℕ
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → c ^ b < (b - d)!
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
]

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p =
    (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
]

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p =
    (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) * ∏ p ∈ n.primeFactors, (p - 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < n.factorization p
⊢ p ^ (n.factorization p - 1) * (p - 1) * p = p ^ n.factorization p * (p - 1)

Tactic:
]

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < n.factorization p
⊢ p ^ (n.factorization p - 1) * (p - 1) * p = p ^ n.factorization p * (p - 1)
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 + 1) + d') * c ^ d' < (2 * (c ^ 2 + d + 1) + d' - d)!

Tactic:
convert_to! (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

Goal state after:
case e'_3
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d') * c ^ d' = (c ^ 2) ^ (c ^ 2 + d' + d + 1)

case e'_4
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (2 * (c ^ 2 + d + 1) + d' - d)! = (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

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)!
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < n.factorization p
⊢ p ^ n.factorization p * (p - 1) = p ^ n.factorization p * (p - 1)

Tactic:
]

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 ×ˢ atTop).IsCountablyGenerated

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atTop.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atTop.IsCountablyGenerated
⊢ (atTop ×ˢ atTop).IsCountablyGenerated
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 ×ˢ atBot).IsCountablyGenerated

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atBot.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atBot.IsCountablyGenerated
⊢ (atBot ×ˢ atBot).IsCountablyGenerated
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: case e'_3
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ c ^ (2 * (c ^ 2 + d + 1) + d' + d') = c ^ (2 * (c ^ 2 + d' + d + 1))

Tactic:
]

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

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

pp: n : ℕ
⊢ 0 < ∏ p ∈ n.primeFactors, p

Tactic:
]

Goal state after:
n : ℕ
⊢ 0 < ∏ p ∈ n.primeFactors, p
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
⊢ 1 * (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2)! * (c ^ 2 + 1) ^ (c ^ 2 + d' + d + 1)

Tactic:
]

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

Goal state before:
pp: case refine_1
α : 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)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ xs n ≤ c (xs n) (ys n)

Tactic:
]

Goal state after:
case refine_1
α : 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)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ xs n ≤ c (xs n) (ys n)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ 0 < n.factorization.prod fun p x ↦ p

Tactic:
]

Goal state after:
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ 0 < n.factorization.prod fun p x ↦ p
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: case refine_2
α : 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)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ ys n ≤ c (xs n) (ys n)

Tactic:
]

Goal state after:
case refine_2
α : 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)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ ys n ≤ c (xs n) (ys n)
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: a c d n : ℕ
hn : a ^ n * c ^ n < (n - d)!
hn0 : 0 < n
⊢ a * c ^ n < (n - d)!

Tactic:
]

Goal state after:
a c d n : ℕ
hn : a ^ n * c ^ n < (n - d)!
hn0 : 0 < n
⊢ a * c ^ n < (n - d)!
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
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst✝ : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑p - 1 = ↑p - 1

Tactic:
]

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

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

Tactic:
]

Goal state after:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
h : ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
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 : ∃ s ∈ f, ∃ᶠ (x_1 : ι) in l, x x_1 ∉ s
⊢ ∃ s ∈ f, ∃ᶠ (n : ι) in l, x n ∉ s

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst✝ : l.IsCountablyGenerated
hxy : ∃ s ∈ f, ∃ᶠ (x_1 : ι) in l, x x_1 ∉ s
⊢ ∃ s ∈ f, ∃ᶠ (n : ι) in l, x n ∉ s
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b * (a * b) / ((∏ p ∈ (a.gcd b).primeFactors, p) * ∏ p ∈ (a * b).primeFactors, p) *
      ((∏ p ∈ (a.gcd b).primeFactors, (p - 1)) * ∏ p ∈ (a * b).primeFactors, (p - 1)) =
    a * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
        ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b

pp: case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ a.primeFactors, p ∣ a

pp: case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ b.primeFactors, p ∣ b

pp: case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a.gcd b).primeFactors, p ∣ a.gcd b

pp: case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a * b).primeFactors, p ∣ a * b

Tactic:
]

Goal state after:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b * (a * b) / ((∏ p ∈ (a.gcd b).primeFactors, p) * ∏ p ∈ (a * b).primeFactors, p) *
      ((∏ p ∈ (a.gcd b).primeFactors, (p - 1)) * ∏ p ∈ (a * b).primeFactors, (p - 1)) =
    a * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
        ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ a.primeFactors, p ∣ a

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ b.primeFactors, p ∣ b

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a.gcd b).primeFactors, p ∣ a.gcd b

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a * b).primeFactors, p ∣ a * b
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 : (comap u f ⊓ g).NeBot
⊢ ∃ θ, Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_3
g : Filter ι
inst✝¹ : g.IsCountablyGenerated
u : ι → α
f : Filter α
inst✝ : f.IsCountablyGenerated
hx : (comap u f ⊓ g).NeBot
⊢ ∃ θ, Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b * (a * b) / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
      ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) =
    a.gcd b * (a * b) / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
      ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1))

pp: case H
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ (∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p ∣ a * b

Tactic:
]

Goal state after:
case H
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ (∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p ∣ a * b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
hd0 : 0 < d
⊢ φ (a * b) * d ≤ φ (a * b) * d

Tactic:
]

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

Goal state before:
pp: case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
⊢ (a.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) ∣ b.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)

Tactic:
]

Goal state after:
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
⊢ (a.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) ∣ b.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)
Module: Mathlib.Data.Nat.Totient

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

Tactic:
]

Goal state after:
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ p * φ (p * n) = φ p * (φ n * p)
⊢ φ (p * n) = p * φ n
Module: Mathlib.Data.Nat.Totient

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

pp: p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ p.Coprime n

Tactic:
]

Goal state after:
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ p.Coprime n
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ φ n = φ n

Tactic:
]

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

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : b = 0
ha : a = 0
⊢ a = b ∨ 2 * a = b

Tactic:
]

Goal state after:
case pos
a b : ℕ
h : a ∣ b
h' : b = 0
ha : a = 0
⊢ a = b ∨ 2 * a = b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : a = 0
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b

Tactic:
]

Goal state after:
case pos
a b : ℕ
h : a ∣ b
h' : a = 0
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b
Module: Mathlib.Data.Nat.Totient

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

Tactic:
]

Goal state after:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : c = 1 ∨ c = 2
hb : ¬a * c = 0
this : a.Coprime c
⊢ a = a * c ∨ 2 * a = a * c
Module: Mathlib.Data.Nat.Totient

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

Tactic:
]

Goal state after:
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (p * a * d)
hb : ¬a * (p * d) = 0
this : φ a < φ (p * a * d)
⊢ False
Module: Mathlib.Data.Nat.Totient

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

Tactic:
]

Goal state after:
case neg
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ φ a < φ (a * p * d)