awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
j : ℕ
hj : p ^ j = p ^ i * n
neg : ∀ (v : ℕ) (hmn : (p ^ i).Coprime (p ^ v)) (hj : p ^ j = p ^ i * p ^ v), ∃ (j : ℕ), p ^ j = p ^ v
⊢ ∃ (j : ℕ), p ^ j = n

Tactic:
obtain ⟨v, -, rfl⟩ := (Nat.dvd_prime_pow hp).mp (Dvd.intro_left _ hj.symm)

Premises used: Dvd.intro_left, Iff.mp, Eq.symm, rfl, Nat.dvd_prime_pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i j v : ℕ
hmn : (p ^ i).Coprime (p ^ v)
hj : p ^ j = p ^ i * p ^ v
⊢ ∃ (j : ℕ), p ^ j = p ^ v

Tactic:
⟨v, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i j v : ℕ
hmn : (p ^ i).Coprime (p ^ v)
hj : p ^ j = p ^ i * p ^ v
⊢ ∃ (j : ℕ), p ^ j = p ^ v

Tactic:
exact ⟨v, rfl⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hm : ¬∃ (i : ℕ), p ^ i = m
neg :
  Function.extend (fun (x : ℕ) ↦ p ^ x)
      (fun (x : ℕ) ↦
        (PowerSeries.coeff x : (a : PowerSeries R) → R)
          (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
      0 (m * n) =
    HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ p ^ x)
        (fun (x : ℕ) ↦
          (PowerSeries.coeff x : (a : PowerSeries R) → R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
        0 m)
      (Function.extend (fun (x : ℕ) ↦ p ^ x)
        (fun (x : ℕ) ↦
          (PowerSeries.coeff x : (a : PowerSeries R) → R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
        0 n)
⊢ (((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
          ArithmeticFunction R) :
        (a : ℕ) → R)
      (m * n) =
    HMul.hMul (α := R) (β := R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          m :
        R)
      ((((ofPowerSeries p : (a : PowerSeries R) → ArithmeticFunction R)
                (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f) :
              ArithmeticFunction R) :
            (a : ℕ) → R)
          n :
        R)

Tactic:
simp_rw [ofPowerSeries_apply hp.one_lt]

Premises used: Nat.Prime.one_lt, ArithmeticFunction.ofPowerSeries_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hm : ¬∃ (i : ℕ), p ^ i = m
neg : ¬∃ (a : ℕ), p ^ a = m * n
⊢ Function.extend (fun (x : ℕ) ↦ p ^ x)
      (fun (x : ℕ) ↦
        (PowerSeries.coeff x : (a : PowerSeries R) → R)
          (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
      0 (m * n) =
    HMul.hMul (α := R)
      (Function.extend (fun (x : ℕ) ↦ p ^ x)
        (fun (x : ℕ) ↦
          (PowerSeries.coeff x : (a : PowerSeries R) → R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
        0 m)
      (Function.extend (fun (x : ℕ) ↦ p ^ x)
        (fun (x : ℕ) ↦
          (PowerSeries.coeff x : (a : PowerSeries R) → R)
            (PowerSeries.subst (HPow.hPow (α := PowerSeries R) PowerSeries.X k) f))
        0 n)

Tactic:
rw [Function.extend_apply', Function.extend_apply' _ _ _ hm,
      Pi.zero_apply, Pi.zero_apply, zero_mul]

Premises used: MulZeroClass.zero_mul, Pi.zero_apply, Function.extend_apply'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hm : ¬∃ (i : ℕ), p ^ i = m
neg : ∀ (hm : ∃ (a : ℕ), p ^ a = m * n), ∃ (i : ℕ), p ^ i = m
⊢ ¬∃ (a : ℕ), p ^ a = m * n

Tactic:
contrapose! hm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hm : ∃ (a : ℕ), p ^ a = m * n
neg : ∀ (i : ℕ) (hi : p ^ i = m * n), ∃ (i : ℕ), p ^ i = m
⊢ ∃ (i : ℕ), p ^ i = m

Tactic:
obtain ⟨i, hi⟩ := hm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hi : p ^ i = m * n
neg : ∀ (j : ℕ) (hmn : (p ^ j).Coprime n) (hi : p ^ i = p ^ j * n), ∃ (i : ℕ), p ^ i = p ^ j
⊢ ∃ (i : ℕ), p ^ i = m

Tactic:
obtain ⟨j, -, rfl⟩ := (Nat.dvd_prime_pow hp).mp ⟨n, hi⟩

Premises used: Exists.intro, Iff.mp, rfl, Nat.dvd_prime_pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i j : ℕ
hmn : (p ^ j).Coprime n
hi : p ^ i = p ^ j * n
⊢ ∃ (i : ℕ), p ^ i = p ^ j

Tactic:
⟨j, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
R : Type u_1
inst : CommRing R
f : PowerSeries R
hf : Eq (α := R) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) (1 : R)
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i j : ℕ
hmn : (p ^ j).Coprime n
hi : p ^ i = p ^ j * n
⊢ ∃ (i : ℕ), p ^ i = p ^ j

Tactic:
exact ⟨j, rfl⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
F : Filter ι
g : ArithmeticFunction R
this : UniformSpace R := ⊥
⊢ Topology.IsInducing.{u_2, u_2} (X := ArithmeticFunction R) (Y := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))

Tactic:
have : Topology.IsInducing ((↑) : ArithmeticFunction R → (ℕ → R)) := ⟨rfl⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
F : Filter ι
g : ArithmeticFunction R
this_1 : UniformSpace R := ⊥
this :
  Topology.IsInducing.{u_2, u_2} (X := ArithmeticFunction R) (Y := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
⊢ Tendsto f F (nhds g) ↔ ∀ (n : ℕ), ∀ᶠ (i : ι) in F, Eq (α := R) ((f i : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)

Tactic:
simp [this.tendsto_nhds_iff, tendsto_pi_nhds]

Premises used: tendsto_pi_nhds, Topology.IsInducing.tendsto_nhds_iff
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
this : UniformSpace R := ⊥
apply :
  IsComplete.{u_2} (α := (a : ℕ) → R) (Set.range (ι := ArithmeticFunction R) (DFunLike.coe (β := fun (x : ℕ) ↦ R)))
⊢ CompleteSpace.{u_2} (ArithmeticFunction R)

Tactic:
apply IsUniformInducing.completeSpace ⟨rfl⟩

Premises used: IsUniformInducing.completeSpace, IsUniformInducing.mk
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
this : UniformSpace R := ⊥
h : IsClosed.{u_2} (X := (a : ℕ) → R) (Set.range (ι := ArithmeticFunction R) (DFunLike.coe (β := fun (x : ℕ) ↦ R)))
⊢ IsComplete.{u_2} (α := (a : ℕ) → R) (Set.range (ι := ArithmeticFunction R) (DFunLike.coe (β := fun (x : ℕ) ↦ R)))

Tactic:
apply IsClosed.isComplete

Premises used: IsClosed.isComplete
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
this : UniformSpace R := ⊥
h :
  ∀ (f : (a : ℕ) → R),
    Membership.mem (γ := Set ((a : ℕ) → R))
        (Set.range (ι := ArithmeticFunction R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))) f ↔
      Membership.mem (γ := Set ((a : ℕ) → R)) {f : (a : ℕ) → R | f 0 = 0} f
⊢ Eq.{u_2 + 1} (α := Set ((a : ℕ) → R)) (Set.range (ι := ArithmeticFunction R) (DFunLike.coe (β := fun (x : ℕ) ↦ R)))
    {f : (a : ℕ) → R | f 0 = 0}

Tactic:
ext f
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
this : UniformSpace R := ⊥
f : ArithmeticFunction R
⊢ Membership.mem (γ := Set ((a : ℕ) → R)) {f : (a : ℕ) → R | f 0 = 0} (⇑f : (a : ℕ) → R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
this : UniformSpace R := ⊥
f : (a : ℕ) → R
⊢ Membership.mem (γ := Set ((a : ℕ) → R)) (Set.range (ι := ArithmeticFunction R) (DFunLike.coe (β := fun (x : ℕ) ↦ R)))
      f ↔
    Membership.mem (γ := Set ((a : ℕ) → R)) {f : (a : ℕ) → R | f 0 = 0} f

Tactic:
exact ⟨by rintro ⟨f, rfl⟩; simp, fun hf ↦ ⟨⟨f, hf⟩, rfl⟩⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
this : UniformSpace R := ⊥
⊢ Eq.{u_2 + 1} (α := Set ((a : ℕ) → R)) (Set.range (ι := ArithmeticFunction R) (DFunLike.coe (β := fun (x : ℕ) ↦ R)))
    {f : (a : ℕ) → R | f 0 = 0}

Tactic:
have : Set.range ((↑) : ArithmeticFunction R → (ℕ → R)) = {f | f 0 = 0} := by
    ext f
    exact ⟨by rintro ⟨f, rfl⟩; simp, fun hf ↦ ⟨⟨f, hf⟩, rfl⟩⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
this_1 : UniformSpace R := ⊥
this :
  Eq.{u_2 + 1} (α := Set ((a : ℕ) → R)) (Set.range (ι := ArithmeticFunction R) (DFunLike.coe (β := fun (x : ℕ) ↦ R)))
    {f : (a : ℕ) → R | f 0 = 0}
h : IsClosed.{u_2} (X := (a : ℕ) → R) {f : (a : ℕ) → R | f 0 = 0}
⊢ IsClosed.{u_2} (X := (a : ℕ) → R) (Set.range (ι := ArithmeticFunction R) (DFunLike.coe (β := fun (x : ℕ) ↦ R)))

Tactic:
rw [ArithmeticFunction.range_coe]

Premises used: ArithmeticFunction.range_coe
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
this_1 : UniformSpace R := ⊥
this :
  Eq.{u_2 + 1} (α := Set ((a : ℕ) → R)) (Set.range (ι := ArithmeticFunction R) (DFunLike.coe (β := fun (x : ℕ) ↦ R)))
    {f : (a : ℕ) → R | f 0 = 0}
⊢ IsClosed.{u_2} (X := (a : ℕ) → R) {f : (a : ℕ) → R | f 0 = 0}

Tactic:
apply isClosed_setOf_map_zero

Premises used: isClosed_setOf_map_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, Eq (α := R) ((f i : (a : ℕ) → R) n : R) ((1 : (a : ℕ) → R) n : R)
this : UniformSpace R := ⊥
⊢ IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))

Tactic:
have : IsUniformInducing ((↑) : ArithmeticFunction R → (ℕ → R)) := ⟨rfl⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, Eq (α := R) ((f i : (a : ℕ) → R) n : R) ((1 : (a : ℕ) → R) n : R)
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
suffices : Multipliable f
⊢ ∀ (n : ℕ),
    ∀ᶠ (s : Finset ι) in atTop, Eq (α := R) ((∏ i ∈ s, f i : (a : ℕ) → R) n : R) ((eulerProduct f : (a : ℕ) → R) n : R)

Tactic:
suffices Multipliable f from tendsto_iff.mp this.hasProd
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, Eq (α := R) ((f i : (a : ℕ) → R) n : R) ((1 : (a : ℕ) → R) n : R)
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
simp_rw :
  ∀ (i : ℕ),
    ∃ (a : Finset ι),
      ∀ (k l : Finset ι),
        a ≤ k → a ≤ l → Eq.{u_2 + 1} (α := R) ((∏ b ∈ k, f b : (a : ℕ) → R) i : R) ((∏ b ∈ l, f b : (a : ℕ) → R) i : R)
⊢ Multipliable f

Tactic:
simp_rw [multipliable_iff_cauchySeq_finset, CauchySeq, ← this.cauchy_map_iff,
    Filter.map_map, cauchy_map_iff', Pi.uniformity, DiscreteUniformity.eq_principal_setRelId,
    tendsto_iInf, tendsto_comap_iff, tendsto_principal, Function.comp_apply, prod_atTop_atTop_eq,
    eventually_atTop_prod_self, SetRel.mem_id]

Premises used: CauchySeq, Filter.map_map, Filter.tendsto_comap_iff, Filter.tendsto_principal, multipliable_iff_cauchySeq_finset, DiscreteUniformity.eq_principal_setRelId, SetRel.mem_id, cauchy_map_iff', Filter.tendsto_iInf, Filter.prod_atTop_atTop_eq, Function.comp_apply, Filter.eventually_atTop_prod_self, IsUniformInducing.cauchy_map_iff, Pi.uniformity
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, Eq (α := R) ((f i : (a : ℕ) → R) n : R) ((1 : (a : ℕ) → R) n : R)
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
n : ℕ
⊢ ∀ k ∈ Set.Iic n, ∀ᶠ (x : ι) in cofinite, Eq (α := R) ((f x : (a : ℕ) → R) k : R) ((1 : (a : ℕ) → R) k : R)

Tactic:
replace hf : ∀ k ∈ Set.Iic n, ∀ᶠ (x : ι) in cofinite, (f x) k = (1 : ArithmeticFunction R) k :=
    fun k hk ↦ hf k
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
n : ℕ
hf : ∀ k ∈ Set.Iic n, ∀ᶠ (x : ι) in cofinite, Eq (α := R) ((f x : (a : ℕ) → R) k : R) ((1 : (a : ℕ) → R) k : R)
⊢ ∃ (v : Set ι),
    Membership.mem (γ := Filter ι) cofinite v ∧
      ∀ y ∈ v, ∀ i ∈ Set.Iic n, Eq (α := R) ((f y : (a : ℕ) → R) i : R) ((1 : (a : ℕ) → R) i : R)

Tactic:
rw [← eventually_all_finite (Set.finite_Iic n), eventually_iff_exists_mem] at hf

Premises used: Set.finite_Iic, Filter.eventually_all_finite, Filter.eventually_iff_exists_mem
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
n : ℕ
hf :
  ∃ (v : Set ι),
    Membership.mem (γ := Filter ι) cofinite v ∧
      ∀ y ∈ v, ∀ i ∈ Set.Iic n, Eq (α := R) ((f y : (a : ℕ) → R) i : R) ((1 : (a : ℕ) → R) i : R)
obtain :
  ∀ (s : Set ι) (hs : Membership.mem (γ := Filter ι) cofinite s)
    (hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, Eq (α := R) ((f y : (a : ℕ) → R) i : R) ((1 : (a : ℕ) → R) i : R)),
    ∃ (a : Finset ι),
      ∀ (k l : Finset ι),
        a ≤ k → a ≤ l → Eq.{u_2 + 1} (α := R) ((∏ b ∈ k, f b : (a : ℕ) → R) n : R) ((∏ b ∈ l, f b : (a : ℕ) → R) n : R)
⊢ ∃ (a : Finset ι),
    ∀ (k l : Finset ι),
      a ≤ k → a ≤ l → Eq.{u_2 + 1} (α := R) ((∏ b ∈ k, f b : (a : ℕ) → R) n : R) ((∏ b ∈ l, f b : (a : ℕ) → R) n : R)

Tactic:
obtain ⟨s, hs, hs'⟩ := hf
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
n : ℕ
s : Set ι
hs : Membership.mem (γ := Filter ι) cofinite s
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, Eq (α := R) ((f y : (a : ℕ) → R) i : R) ((1 : (a : ℕ) → R) i : R)
t : Finset ι := ⋯.toFinset (s := sᶜ)
⊢ ∃ (a : Finset ι),
    ∀ (k l : Finset ι),
      a ≤ k → a ≤ l → Eq.{u_2 + 1} (α := R) ((∏ b ∈ k, f b : (a : ℕ) → R) n : R) ((∏ b ∈ l, f b : (a : ℕ) → R) n : R)

Tactic:
⟨t, fun u v hu hv ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
n : ℕ
s : Set ι
hs : Membership.mem (γ := Filter ι) cofinite s
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, Eq (α := R) ((f y : (a : ℕ) → R) i : R) ((1 : (a : ℕ) → R) i : R)
t : Finset ι := ⋯.toFinset (s := sᶜ)
refine :
  ∀ (u v : Finset ι) (hu : t ≤ u) (hv : t ≤ v),
    Eq.{u_2 + 1} (α := R) ((∏ b ∈ u, f b : (a : ℕ) → R) n : R) ((∏ b ∈ v, f b : (a : ℕ) → R) n : R)
⊢ ∃ (a : Finset ι),
    ∀ (k l : Finset ι),
      a ≤ k → a ≤ l → Eq.{u_2 + 1} (α := R) ((∏ b ∈ k, f b : (a : ℕ) → R) n : R) ((∏ b ∈ l, f b : (a : ℕ) → R) n : R)

Tactic:
refine ⟨t, fun u v hu hv ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
n : ℕ
s : Set ι
hs : Membership.mem (γ := Filter ι) cofinite s
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, Eq (α := R) ((f y : (a : ℕ) → R) i : R) ((1 : (a : ℕ) → R) i : R)
t : Finset ι := ⋯.toFinset (s := sᶜ)
u v : Finset ι
hu : t ≤ u
hv : t ≤ v
rw :
  Eq (α := R) ((HMul.hMul (α := ArithmeticFunction R) (∏ x ∈ u \ t, f x) (∏ x ∈ t, f x) : (a : ℕ) → R) n : R)
    ((HMul.hMul (α := ArithmeticFunction R) (∏ x ∈ v \ t, f x) (∏ x ∈ t, f x) : (a : ℕ) → R) n : R)
⊢ Eq.{u_2 + 1} (α := R) ((∏ b ∈ u, f b : (a : ℕ) → R) n : R) ((∏ b ∈ v, f b : (a : ℕ) → R) n : R)

Tactic:
rw [← Finset.prod_sdiff hu, ← Finset.prod_sdiff hv]

Premises used: Finset.prod_sdiff
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
n : ℕ
s : Set ι
hs : Membership.mem (γ := Filter ι) cofinite s
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, Eq (α := R) ((f y : (a : ℕ) → R) i : R) ((1 : (a : ℕ) → R) i : R)
t : Finset ι := ⋯.toFinset (s := sᶜ)
u v : Finset ι
hu : t ≤ u
hv : t ≤ v
i : ι
hi : i ∈ u \ t
⊢ i ∈ u ∧ i ∈ s

Tactic:
rw [Finset.mem_sdiff, Set.Finite.mem_toFinset, Set.notMem_compl_iff] at hi

Premises used: Set.Finite.mem_toFinset, Finset.mem_sdiff, Set.notMem_compl_iff
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
n : ℕ
s : Set ι
hs : Membership.mem (γ := Filter ι) cofinite s
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, Eq (α := R) ((f y : (a : ℕ) → R) i : R) ((1 : (a : ℕ) → R) i : R)
t : Finset ι := ⋯.toFinset (s := sᶜ)
u v : Finset ι
hu : t ≤ u
hv : t ≤ v
i : ι
hi : i ∈ u ∧ i ∈ s
⊢ i ∈ s

Tactic:
hi.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
n : ℕ
s : Set ι
hs : Membership.mem (γ := Filter ι) cofinite s
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, Eq (α := R) ((f y : (a : ℕ) → R) i : R) ((1 : (a : ℕ) → R) i : R)
t : Finset ι := ⋯.toFinset (s := sᶜ)
u v : Finset ι
hu : t ≤ u
hv : t ≤ v
i : ι
hi : i ∈ u ∧ i ∈ s
⊢ i ∈ s

Tactic:
exact hi.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
n : ℕ
s : Set ι
hs : Membership.mem (γ := Filter ι) cofinite s
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, Eq (α := R) ((f y : (a : ℕ) → R) i : R) ((1 : (a : ℕ) → R) i : R)
t : Finset ι := ⋯.toFinset (s := sᶜ)
u v : Finset ι
hu : t ≤ u
hv : t ≤ v
⊢ ∀ i ∈ u \ t, i ∈ s

Tactic:
replace hu : ∀ i ∈ u \ t, i ∈ s := by
    intro i hi
    rw [Finset.mem_sdiff, Set.Finite.mem_toFinset, Set.notMem_compl_iff] at hi
    exact hi.2
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
n : ℕ
s : Set ι
hs : Membership.mem (γ := Filter ι) cofinite s
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, Eq (α := R) ((f y : (a : ℕ) → R) i : R) ((1 : (a : ℕ) → R) i : R)
t : Finset ι := ⋯.toFinset (s := sᶜ)
u v : Finset ι
hv : t ≤ v
hu : ∀ i ∈ u \ t, i ∈ s
i : ι
hi : i ∈ v \ t
⊢ i ∈ v ∧ i ∈ s

Tactic:
rw [Finset.mem_sdiff, Set.Finite.mem_toFinset, Set.notMem_compl_iff] at hi

Premises used: Set.Finite.mem_toFinset, Finset.mem_sdiff, Set.notMem_compl_iff
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
n : ℕ
s : Set ι
hs : Membership.mem (γ := Filter ι) cofinite s
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, Eq (α := R) ((f y : (a : ℕ) → R) i : R) ((1 : (a : ℕ) → R) i : R)
t : Finset ι := ⋯.toFinset (s := sᶜ)
u v : Finset ι
hv : t ≤ v
hu : ∀ i ∈ u \ t, i ∈ s
i : ι
hi : i ∈ v ∧ i ∈ s
⊢ i ∈ s

Tactic:
hi.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
n : ℕ
s : Set ι
hs : Membership.mem (γ := Filter ι) cofinite s
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, Eq (α := R) ((f y : (a : ℕ) → R) i : R) ((1 : (a : ℕ) → R) i : R)
t : Finset ι := ⋯.toFinset (s := sᶜ)
u v : Finset ι
hv : t ≤ v
hu : ∀ i ∈ u \ t, i ∈ s
i : ι
hi : i ∈ v ∧ i ∈ s
⊢ i ∈ s

Tactic:
exact hi.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
f : ι → ArithmeticFunction R
this_1 : UniformSpace R := ⊥
this : IsUniformInducing.{u_2, u_2} (α := ArithmeticFunction R) (β := (a : ℕ) → R) (DFunLike.coe (β := fun (x : ℕ) ↦ R))
n : ℕ
s : Set ι
hs : Membership.mem (γ := Filter ι) cofinite s
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, Eq (α := R) ((f y : (a : ℕ) → R) i : R) ((1 : (a : ℕ) → R) i : R)
t : Finset ι := ⋯.toFinset (s := sᶜ)
u v : Finset ι
hv : t ≤ v
hu : ∀ i ∈ u \ t, i ∈ s
⊢ ∀ i ∈ v \ t, i ∈ s

Tactic:
replace hv : ∀ i ∈ v \ t, i ∈ s := by
    intro i hi
    rw [Finset.mem_sdiff, Set.Finite.mem_toFinset, Set.notMem_compl_iff] at hi
    exact hi.2