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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
⊢ m = n

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
hp : (Set.ofPred p).Finite
n : ℕ
⊢ count p n ≤ #hp.toFinset

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = n ↔ ∀ n' < n, p n'

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = 0 ↔ ∀ m < n, ¬p m

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n ≠ 0 ↔ ∃ m < n, p m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ r • ↑a = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a k : ℕ
h : 0 < count (fun k ↦ p (a + k)) (k + 1)
t : ℕ
ht : t < k + 1
hp : p (a + t)
⊢ (a ≤ a + t ∧ a + t < a + k + 1) ∧ p (a + t)

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
h : count p a < count p b
⊢ ∃ x ∈ Set.Ico a b, p x

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝¹ : DecidablePred p
q : ℕ → Prop
inst✝ : DecidablePred q
n : ℕ
hpq : ∀ k < n, p k → q k
⊢ ∀ x ∈ List.range n, decide (p x) = true → decide (q x) = true

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
⊢ f (n % a) = f n

Tactic:
by

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

Goal state before:
pp: n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ (filter p (Ico n (n + a))).card = count p a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (r • a) = (RingHom.id R) r • ExtensionOfMaxAdjoin.extensionToFun i f h a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: a b m n p : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
⊢ (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
⊢ ∀ (n : ℕ), motive n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
m : M
⊢ f m =
    ↑{ domain := supExtensionOfMaxSingleton i f y,
          toFun := { toFun := ExtensionOfMaxAdjoin.extensionToFun i f h, map_add' := ⋯, map_smul' := ⋯ } }
      ⟨i m, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : ↑x = ↑x'
⊢ ↑x' = ↑x + 0 • y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case succ.zero
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime : ∀ (p : ℕ), Prime p → motive p
composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)
n p : ℕ
hp : Prime p
ha : motive (0 + 1)
⊢ motive (p * (0 + 1))

Tactic:
simpa using prime _ hp

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: motive : ℕ → Prop
zero : motive 0
one : motive 1
prime : ∀ (p : ℕ), Prime p → motive p
composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)
n : ℕ
⊢ motive n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : ↑x = ↑x'
⊢ ↑(extensionOfMax i f).toLinearPMap x = ↑(extensionOfMaxAdjoin i f h y).toLinearPMap x'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
⊢ (extensionOfMax i f).domain = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
x y : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨x + y, ⋯⟩ =
    ↑(extensionOfMax f g).toLinearPMap ⟨x, ⋯⟩ + ↑(extensionOfMax f g).toLinearPMap ⟨y, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
r : R
x : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨r • x, ⋯⟩ = (RingHom.id R) r • ↑(extensionOfMax f g).toLinearPMap ⟨x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝² : Ring R
Q : Type v
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
h : Baer R Q
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective ⇑i
f : X →ₗ[R] Q
⊢ ∃ h, ∀ (x : X), h (i x) = f x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv R ↥I
eR : Shrink.{v, u} R ≃ₗ[R] R := Shrink.linearEquiv R R
g' : Shrink.{v, u} R →ₗ[R] Q
hg' : ∀ (x : Shrink.{v, u} ↥I), g' ((↑eR.symm ∘ₗ Submodule.subtype I ∘ₗ ↑eI) x) = (g ∘ₗ ↑eI) x
x : R
mx : x ∈ I
⊢ (g' ∘ₗ ↑eR.symm) x = g ⟨x, mx⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
⊢ Baer R Q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝² : Ring R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R (ULift.{v', v} M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
eX : ULift.{v', v} X ≃ₗ[R] X := ULift.moduleEquiv
⊢ Function.Injective ⇑(↑ULift.moduleEquiv.symm ∘ₗ f ∘ₗ ↑eX)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝² : Ring R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R (ULift.{v', v} M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
eX : ULift.{v', v} X ≃ₗ[R] X := ULift.moduleEquiv
g' : ULift.{v', v} Y →ₗ[R] ULift.{v', v} M
hg' : ∀ (x : ULift.{v', v} X), g' ((↑ULift.moduleEquiv.symm ∘ₗ f ∘ₗ ↑eX) x) = (↑ULift.moduleEquiv.symm ∘ₗ g ∘ₗ ↑eX) x
x : X
⊢ (↑ULift.moduleEquiv ∘ₗ g' ∘ₗ ↑ULift.moduleEquiv.symm) (f x) = g x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R✝ : Type u
inst✝⁷ : Ring R✝
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R✝ Q
R : Type u
inst✝⁴ : Ring R
ι : Type w
M : ι → Type v
inst✝³ : Small.{v, u} R
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Injective R (M i)
X Y : Type (max v w)
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] (i : ι) → M i
⊢ ∃ h, ∀ (x : X), h (f x) = g x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : Small.{v, u} R
S : Type u'
inst✝⁴ : Ring S
M : Type v
N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
I' : Submodule R R := Submodule.map (↑e₁.symm.toSemilinearEquiv) I
e : ↥I' ≃ₛₗ[↑e₁] ↥I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
f : ↥I' →ₗ[R] M := ↑e₂.symm ∘ₛₗ g ∘ₛₗ ↑e
x : R
hx : x ∈ I'
⊢ e₁ x ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun p k ↦ f (p ^ k)

Tactic:
by

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

Goal state before:
pp: n : ℕ
m : ↑{m | m < n ∧ n.Coprime m}
⊢ ↑m ∈ {x ∈ range n | n.Coprime x}

Tactic:
by

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

Goal state before:
pp: n : ℕ
m : ↥({x ∈ range n | n.Coprime x})
⊢ ↑m ∈ {m | m < n ∧ n.Coprime m}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : Small.{v, u} R
S : Type u'
inst✝⁴ : Ring S
M : Type v
N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
I' : Submodule R R := Submodule.map (↑e₁.symm.toSemilinearEquiv) I
e : ↥I' ≃ₛₗ[↑e₁] ↥I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
f : ↥I' →ₗ[R] M := ↑e₂.symm ∘ₛₗ g ∘ₛₗ ↑e
hf : ∀ (x : R) (hx : x ∈ I'), f ⟨x, hx⟩ = e₂.symm (g ⟨e₁ x, ⋯⟩)
f' : R →ₗ[R] M
hf' : ∀ (x : R) (mem : x ∈ I'), f' x = f ⟨x, mem⟩
⊢ ∀ (x : S) (mem : x ∈ I), (↑e₂ ∘ₛₗ f' ∘ₛₗ ↑e₁.toSemilinearEquiv.symm) x = g ⟨x, mem⟩

Tactic:
by

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

Goal state before:
pp: n : ℕ
m : ↑{m | m < n ∧ n.Coprime m}
⊢ (fun m ↦ ⟨↑m, ⋯⟩) ((fun m ↦ ⟨↑m, ⋯⟩) m) = m

Tactic:
by

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

Goal state before:
pp: n : ℕ
m : ↥({x ∈ range n | n.Coprime x})
⊢ (fun m ↦ ⟨↑m, ⋯⟩) ((fun m ↦ ⟨↑m, ⋯⟩) m) = m

Tactic:
simp only

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: n : ℕ
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ f n = n.factorization.prod fun p k ↦ f (p ^ k)

Tactic:
by

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

Goal state before:
pp: n : ℕ
m : ↥({x ∈ range n | n.Coprime x})
⊢ (fun m ↦ ⟨↑m, ⋯⟩) ((fun m ↦ ⟨↑m, ⋯⟩) m) = m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : Small.{v, u} R
S : Type u'
inst✝⁴ : Ring S
M : Type v
N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inj : Injective R M
⊢ Injective S N

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ φ n = Nat.card ↑{m | m < n ∧ n.Coprime m}

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ 0 ∈ range n ∧ ¬n.Coprime 0

Tactic:
by

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

Goal state before:
pp: ⊢ φ 0 = 0 ↔ 0 = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (n + 1).gcd (1 % (n + 1)) = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
this : ∃ x < n + 1, (n + 1).gcd x = 1
⊢ φ (n + 1) = 0 ↔ n + 1 = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ 0 < φ n ↔ 0 < n

Tactic:
by

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

Goal state before:
pp: a n : ℕ
⊢ #({x ∈ Ico n (n + a) | a.Coprime x}) = #({a_1 ∈ range a | a.Coprime a_1})

Tactic:
filter_Ico_card_eq_of_periodic,

Goal state after:
a n : ℕ
⊢ count (fun x ↦ a.Coprime x) a = #({a_1 ∈ range a | a.Coprime a_1})

case pp
a n : ℕ
⊢ Function.Periodic (fun x ↦ a.Coprime x) a
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a n : ℕ
⊢ #({x ∈ Ico n (n + a) | a.Coprime x}) = φ a

Tactic:
by

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

Goal state before:
pp: a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + n % a + a * i + a) | a.Coprime x}) ≤
    #({x ∈ Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x})

Tactic:
by

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

Goal state before:
pp: a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x}) ≤
    #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) + φ a

Tactic:
by

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

Goal state before:
pp: a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) + φ a ≤ φ a * i + φ a + φ a

Tactic:
by

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

Goal state before:
pp: a k n : ℕ
a_ne_zero : a ≠ 0
⊢ #({x ∈ Ico k (k + n) | a.Coprime x}) ≤ φ a * (n / a + 1)

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype (ZMod n)ˣ
⊢ Fintype.card { x // x.val.Coprime n } = φ n

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ Even (φ n)

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 2 < n
⊢ Even (φ n)

Tactic:
by

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

Goal state before:
pp: m n : ℕ
h : m.Coprime n
hmn0 : m * n = 0
⊢ φ (m * n) = φ m * φ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
a✝ : a ∉ s
h1 : ↑s ⊆ S → ⋂₀ ↑s ∈ S
h2 : ↑(insert a s) ⊆ S
this : a ∩ ⋂₀ ↑s ∈ S
⊢ ⋂₀ ↑(insert a s) ∈ S

Tactic:
by

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

Goal state before:
pp: m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
⊢ φ (m * n) = φ m * φ n

Tactic:
by

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

Goal state before:
pp: d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : x.gcd a = 1
⊢ d * a < d * x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ ↑F ⊆ S → ⋂₀ ↑F ∈ S

Tactic:
by

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s✝ : Set α
h✝ : s✝ = A
⊢ s✝ = A ∩ Set.univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s✝ : Set α
h✝ : s✝ ∈ S
⊢ s✝ ∈ S

Tactic:
by

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

Goal state before:
pp: d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
hb2 : (d * x).gcd b = d
⊢ d ∣ b

Tactic:
by

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

Goal state before:
pp: n d : ℕ
hnd : d ∣ n
⊢ φ (n / d) = #({k ∈ range n | n.gcd k = d})

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n > 0
⊢ n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})

Tactic:
by

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
h : T1 ∈ S
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ T1 ∩ (A ∩ R) = A ∩ (T1 ∩ R)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.divisors.sum φ = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T2
Q : Set α
hQ : Q ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ Q)
i : T2 ∈ S
⊢ A ∩ Q ∩ T2 = A ∩ (Q ∩ T2)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ∑ m ∈ range n.succ with m ∣ n, φ m = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ A ∩ Q ∩ (A ∩ R) = A ∩ (Q ∩ R)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
H : P ∈ finiteInterClosure (insert A S)
⊢ P ∈ S ∨ ∃ Q ∈ S, P = A ∩ Q

Tactic:
by

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
⊢ s ∩ t ∈ insert univ S

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
X : Type u_3
s : ι → Set X
⊢ ⋃ i ∈ ∅, s i = ∅

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
a : ℕ
⊢ a ∈ image (fun x ↦ x * p) (range (p ^ n)) → a ∈ range (p ^ (n + 1))

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
p : α → Prop
⊢ (∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in atTop, p x

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ #(range (p ^ (n + 1)) \ image (fun x ↦ x * p) (range (p ^ n))) = p ^ n * (p - 1)

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 β
⊢ atTop ×ˢ atTop = atTop

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
hn : 0 < n
⊢ φ (p ^ n) = p ^ (n - 1) * (p - 1)

Tactic:
by

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, p x
⊢ ∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ φ p = p - 1

Tactic:
by

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 atBot
h_evtl : ∀ᶠ (x : β) in atBot, p x
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
⊢ Tendsto (fun p ↦ p.1 ×ˢ p.2) atTop atTop

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : 0 < p
⊢ φ p = p - 1 ↔ Prime p

Tactic:
by

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

Goal state before:
pp: β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
⊢ ∃ n ≥ N, u k < u n ∧ ∀ m < n, N ≤ m → u m ≤ u k

Tactic:
by

Goal state after:
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 u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∀ (N : ℕ), ∃ n ≥ N, ∀ k < n, u k < u n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fintype (ZMod p)ˣ
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∃ᶠ (n : ℕ) in atTop, ∀ k < n, u k < u n

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after: