awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.KummerDedekind
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
refine :
  ∀ (a : S)
    (ha :
      Membership.mem (γ := Submodule S S)
        (comap (F := S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
          (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I))
          (span
            (singleton (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
              ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) :
                    (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
                  ((aeval x : (a : R[X]) → S) Q) :
                HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)))))
        a),
    Membership.mem (γ := Submodule S S)
      (span
        ((↑(Ideal.map (F := R →+* S) (algebraMap R S) I) : Set S) ∪
          singleton (α := S) ((aeval x : (a : R[X]) → S) Q : S)))
      a
⊢ Eq (α := Ideal S)
    (comap (F := S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (span
        (singleton (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
          ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) :
                (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
              ((aeval x : (a : R[X]) → S) Q) :
            HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)))))
    (span
      ((↑(Ideal.map (F := R →+* S) (algebraMap R S) I) : Set S) ∪
        singleton (α := S) ((aeval x : (a : R[X]) → S) Q : S)))

Tactic:
refine le_antisymm (fun a ha ↦ ?_) (span_le.mpr <| union_subset_iff.mpr <|
    ⟨le_comap_of_map_le (by simp), by simp⟩)

Premises used: Ideal.span_le, Iff.mpr, Ideal.le_comap_of_map_le, Set.union_subset_iff, le_antisymm, And.intro
-- Module: Mathlib.NumberTheory.KummerDedekind
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
ha :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (span
        (singleton (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
          ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) :
                (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
              ((aeval x : (a : R[X]) → S) Q) :
            HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)))))
    a
⊢ Dvd.dvd.{u_2} (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
        ((aeval x : (a : R[X]) → S) Q) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) a :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))

Tactic:
rw [mem_comap, Ideal.mem_span_singleton] at ha

Premises used: Ideal.mem_span_singleton, Ideal.mem_comap
-- Module: Mathlib.NumberTheory.KummerDedekind
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
ha :
  Dvd.dvd.{u_2} (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
        ((aeval x : (a : R[X]) → S) Q) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) a :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
obtain :
  ∀ (a' : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (ha' :
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) a =
        HMul.hMul (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
          ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) :
                (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
              ((aeval x : (a : R[X]) → S) Q) :
            HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
          a'),
    Membership.mem (γ := Submodule S S)
      (span
        ((↑(Ideal.map (F := R →+* S) (algebraMap R S) I) : Set S) ∪
          singleton (α := S) ((aeval x : (a : R[X]) → S) Q : S)))
      a
⊢ Membership.mem (γ := Submodule S S)
    (span
      ((↑(Ideal.map (F := R →+* S) (algebraMap R S) I) : Set S) ∪
        singleton (α := S) ((aeval x : (a : R[X]) → S) Q : S)))
    a

Tactic:
obtain ⟨a', ha'⟩ := ha
-- Module: Mathlib.NumberTheory.KummerDedekind
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
a' : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
ha' :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) a =
    HMul.hMul (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
          ((aeval x : (a : R[X]) → S) Q) :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      a'
obtain :
  ∀ (b : S)
    (hb :
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) b =
        a'),
    Membership.mem (γ := Submodule S S)
      (span
        ((↑(Ideal.map (F := R →+* S) (algebraMap R S) I) : Set S) ∪
          singleton (α := S) ((aeval x : (a : R[X]) → S) Q : S)))
      a
⊢ Membership.mem (γ := Submodule S S)
    (span
      ((↑(Ideal.map (F := R →+* S) (algebraMap R S) I) : Set S) ∪
        singleton (α := S) ((aeval x : (a : R[X]) → S) Q : S)))
    a

Tactic:
obtain ⟨b, hb⟩ := Ideal.Quotient.mk_surjective a'

Premises used: Ideal.Quotient.mk_surjective
-- Module: Mathlib.NumberTheory.KummerDedekind
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
a' : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
ha' :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) a =
    HMul.hMul (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
          ((aeval x : (a : R[X]) → S) Q) :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      a'
b : S
hb :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) b = a'
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    (a - HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) Q : S) b)

Tactic:
rw [← hb, ← map_mul, Quotient.mk_eq_mk_iff_sub_mem] at ha'

Premises used: map_mul, Ideal.Quotient.mk_eq_mk_iff_sub_mem
-- Module: Mathlib.NumberTheory.KummerDedekind
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
a' : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
ha' :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) a =
    HMul.hMul (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
          ((aeval x : (a : R[X]) → S) Q) :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      a'
b : S
hb :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) b = a'
ha'₁ :
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    (a - HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) Q : S) b)
⊢ (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) b = a'

Tactic:
rw [← hb, ← map_mul, Quotient.mk_eq_mk_iff_sub_mem] at ha'

Premises used: map_mul, Ideal.Quotient.mk_eq_mk_iff_sub_mem
-- Module: Mathlib.NumberTheory.KummerDedekind
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
a' : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
b : S
ha' :
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    (a - HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) Q : S) b)
hb :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) b = a'
rw :
  ∃ (a_1 : S) (b : S),
    Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) b ∧
      HMul.hMul (β := S) a_1 ((aeval x : (a : R[X]) → S) Q : S) + b = a
⊢ Membership.mem (γ := Submodule S S)
    (span
      ((↑(Ideal.map (F := R →+* S) (algebraMap R S) I) : Set S) ∪
        singleton (α := S) ((aeval x : (a : R[X]) → S) Q : S)))
    a

Tactic:
rw [union_comm, span_union, span_eq, mem_span_singleton_sup]

Premises used: Set.union_comm, Ideal.span_eq, Ideal.mem_span_singleton_sup, Ideal.span_union
-- Module: Mathlib.NumberTheory.KummerDedekind
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
a' : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
b : S
ha' :
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    (a - HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) Q : S) b)
hb :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) b = a'
⊢ HMul.hMul (β := S) b ((aeval x : (a : R[X]) → S) Q : S) +
      (a - HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) Q : S) b) =
    a

Tactic:
ring
-- Module: Mathlib.NumberTheory.KummerDedekind
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
a' : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
b : S
ha' :
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    (a - HMul.hMul (α := S) ((aeval x : (a : R[X]) → S) Q : S) b)
hb :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) b = a'
⊢ ∃ (a_1 : S) (b : S),
    Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) b ∧
      HMul.hMul (β := S) a_1 ((aeval x : (a : R[X]) → S) Q : S) + b = a

Tactic:
exact ⟨b, a - Q.aeval x * b, ha', by ring⟩
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
rw : P.g (1 / x) = (P.ε⁻¹ * (↑(x ^ P.k) : ℂ) * (P.ε * (↑((1 / x) ^ P.k) : ℂ))) • P.g (1 / x)
⊢ P.g (1 / x) = (P.ε⁻¹ * (↑(x ^ P.k) : ℂ)) • P.f x

Tactic:
rw [(div_div_cancel₀ (one_ne_zero' ℝ) ▸ P.h_feq (1 / x) (one_div_pos.mpr hx) :), ← mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ P.g (1 / x) = HSMul.hSMul (α := ℂ) 1 (P.g (1 / x))

Tactic:
(one_smul ℂ (P.g (1 / x))).symm

Premises used: WeakFEPair.g, HDiv.hDiv, one_smul, Complex, OfNat.ofNat, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
h : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) * (P.ε * (↑((1 / x) ^ P.k) : ℂ)) = 1
⊢ P.g (1 / x) = (P.ε⁻¹ * (↑(x ^ P.k) : ℂ) * (P.ε * (↑((1 / x) ^ P.k) : ℂ))) • P.g (1 / x)

Tactic:
convert! (one_smul ℂ (P.g (1 / x))).symm using 2

Premises used: WeakFEPair.g, HDiv.hDiv, one_smul, Complex, OfNat.ofNat, Eq.symm
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
h : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) * (P.ε * (↑(x ^ P.k) : ℂ)⁻¹) = 1
⊢ P.ε⁻¹ * (↑(x ^ P.k) : ℂ) * (P.ε * (↑((1 / x) ^ P.k) : ℂ)) = 1

Tactic:
rw [one_div, inv_rpow hx.le, ofReal_inv]

Premises used: Real.inv_rpow, LT.lt.le, one_div, Complex.ofReal_inv
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ P.ε⁻¹ * (↑(x ^ P.k) : ℂ) * (P.ε * (↑(x ^ P.k) : ℂ)⁻¹) = 1

Tactic:
field [P.hε, (rpow_pos_of_pos hx _).ne']

Premises used: Real.rpow_pos_of_pos, LT.lt.ne', WeakFEPair.hε
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r : ℝ
⊢ IsBigO.{0, u_1, 0} (α := ℝ) (E := E) (F := ℝ) (𝓝[>] 0) ((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹)
    ((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹)

Tactic:
have := (P.hg_top (-(r + P.k))).comp_tendsto tendsto_inv_nhdsGT_zero
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r : ℝ
this :
  IsBigO.{0, u_1, 0} (α := ℝ) (E := E) (F := ℝ) (𝓝[>] 0) ((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹)
    ((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹)
simp_rw :
  ∀
    (this :
      ∃ (c : ℝ),
        ∀ᶠ (x : ℝ) in 𝓝 0,
          Membership.mem (γ := Set ℝ) (Ioi 0) x →
            Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
              c * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)),
    ∃ (c : ℝ),
      ∀ᶠ (x : ℝ) in 𝓝 0,
        Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ c * ‖x ^ r‖
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) fun (x : ℝ) ↦
    x ^ r

Tactic:
simp_rw [IsBigO, IsBigOWith, eventually_nhdsWithin_iff] at this ⊢

Premises used: Asymptotics.IsBigOWith, Asymptotics.IsBigO, eventually_nhdsWithin_iff
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r : ℝ
this :
  ∃ (c : ℝ),
    ∀ᶠ (x : ℝ) in 𝓝 0,
      Membership.mem (γ := Set ℝ) (Ioi 0) x →
        Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
          c * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
obtain :
  ∀ (C : ℝ)
    (hC :
      ∀ᶠ (x : ℝ) in 𝓝 0,
        Membership.mem (γ := Set ℝ) (Ioi 0) x →
          Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
            C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)),
    ∃ (c : ℝ),
      ∀ᶠ (x : ℝ) in 𝓝 0,
        Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ c * ‖x ^ r‖
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : ℝ) in 𝓝 0,
      Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ c * ‖x ^ r‖

Tactic:
obtain ⟨C, hC⟩ := this
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
h :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : ℝ) in 𝓝 0,
      Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ c * ‖x ^ r‖

Tactic:
use ‖P.ε‖ * C

Premises used: WeakFEPair.ε
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
x : ℝ
hC' :
  Membership.mem (γ := Set ℝ) (Ioi 0) x →
    Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
      C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
h : ∀ (hx : 0 < x), ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
(hx : 0 < x)
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
h :
  ∀ (x : ℝ)
    (hC' :
      Membership.mem (γ := Set ℝ) (Ioi 0) x →
        Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
          C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x))
    (hx : 0 < x), ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
⊢ ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
filter_upwards [hC] with x hC' (hx : 0 < x)
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
x : ℝ
hC' :
  Membership.mem (γ := Set ℝ) (Ioi 0) x →
    Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
      C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
hx : 0 < x
⊢ (↑(x ^ P.k) : ℂ) ≠ 0

Tactic:
have h_nv2 : ↑(x ^ P.k) ≠ (0 : ℂ) := ofReal_ne_zero.mpr (rpow_pos_of_pos hx _).ne'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
x : ℝ
hC' :
  Membership.mem (γ := Set ℝ) (Ioi 0) x →
    Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
      C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
hx : 0 < x
h_nv2 : (↑(x ^ P.k) : ℂ) ≠ 0
⊢ P.ε⁻¹ * (↑(x ^ P.k) : ℂ) ≠ 0

Tactic:
have h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0 := mul_ne_zero P.symm.hε h_nv2
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
        C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
x : ℝ
hC' :
  Membership.mem (γ := Set ℝ) (Ioi 0) x →
    Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
      C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)
hx : 0 < x
h_nv2 : (↑(x ^ P.k) : ℂ) ≠ 0
h_nv : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) ≠ 0
⊢ Norm.norm.{u_1} (E := E) (((fun (x : ℝ) ↦ P.g x - P.g₀) ∘ fun (x : ℝ) ↦ x⁻¹) x) ≤
    C * Norm.norm (E := ℝ) (((fun (x : ℝ) ↦ x ^ (-(r + P.k))) ∘ fun (x : ℝ) ↦ x⁻¹) x)

Tactic:
specialize hC' hx