awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
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
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
have :
  Membership.mem (α := (R ⧸ I)[X]) (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
    ((normalize : (a : (R ⧸ I)[X]) → (R ⧸ I)[X]) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) : (R ⧸ I)[X])
⊢ Irreducible.{u_2} (M := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
have have₁ : ∀
  (mem_norm_factors :
    Membership.mem (α := (R ⧸ I)[X]) (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
      ((normalize : (a : (R ⧸ I)[X]) → (R ⧸ I)[X]) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) : (R ⧸ I)[X])),
  Irreducible.{u_2} (M := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
Tactic: classical
  have mem_norm_factors : normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
      normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) := by
    simp [normalizedFactors_irreducible hf]
  suffices ∃ y, normalizedFactors (I.map (algebraMap R S)) = {y} by
    obtain ⟨y, hy⟩ := this
    have h := prod_normalizedFactors (show I.map (algebraMap R S) ≠ 0 by
          rwa [← bot_eq_zero, Ne,
            map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)])
    rw [associated_iff_eq, hy, Multiset.prod_singleton] at h
    rw [← h]
    exact
      irreducible_of_normalized_factor y
        (show y ∈ normalizedFactors (I.map (algebraMap R S)) by simp [hy])
  rw [normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map hI hI' hx hx']
  use ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm
        ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩ :
      Ideal S)
  rw [Multiset.map_eq_singleton]
  use ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩
  refine ⟨?_, rfl⟩
  apply Multiset.map_injective Subtype.coe_injective
  rw [Multiset.attach_map_val, Multiset.map_singleton, Subtype.coe_mk]
  exact normalizedFactors_irreducible hf
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
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
⊢ 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))
      (Ideal.map (R :=
        HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
          (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
        (F :=
        RingHom.{u_1, u_2}
          (HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
            (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)))
        (↑(quotMapEquivQuotQuotMap hx hx').symm :
          (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)} →+* S ⧸ Ideal.map (algebraMap R S) I)
        (Ideal.map (R := (R ⧸ I)[X]) (F :=
          (R ⧸ I)[X] →+*
            HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
              (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          (span {Polynomial.map (Ideal.Quotient.mk I) Q}))))
    (span
      ((↑(Ideal.map (F := R →+* S) (algebraMap R S) I) : Set S) ∪
        singleton (α := S) ((aeval x : (a : R[X]) → S) Q : S)))
have simp : 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: simp only [map_span, image_singleton, coe_coe, quotMapEquivQuotQuotMap_symm_apply hx hx' Q]
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
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
⊢ 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)))
have 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
Tactic: refine le_antisymm (fun a ha ↦ ?_) (span_le.mpr <| union_subset_iff.mpr <|
    ⟨le_comap_of_map_le (by simp), by simp⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (hypothesis)
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
⊢ 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
have 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))
Tactic: rw [mem_comap, Ideal.mem_span_singleton] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
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))
⊢ 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
have 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
Tactic: obtain ⟨a', ha'⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
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'
⊢ 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
have 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
Tactic: obtain ⟨b, hb⟩ := Ideal.Quotient.mk_surjective a'
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (hypothesis)
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 (γ := 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
have 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)
Tactic: rw [← hb, ← map_mul, Quotient.mk_eq_mk_iff_sub_mem] at ha'
Cleared hypotheses: ha', hb
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
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'
⊢ 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
have 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
Tactic: rw [union_comm, span_union, span_eq, mem_span_singleton_sup]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ P.g (1 / x) = (P.ε⁻¹ * (↑(x ^ P.k) : ℂ)) • P.f x
have rw : P.g (1 / x) = (P.ε⁻¹ * (↑(x ^ P.k) : ℂ) * (P.ε * (↑((1 / x) ^ P.k) : ℂ))) • P.g (1 / x)
Tactic: rw [(div_div_cancel₀ (one_ne_zero' ℝ) ▸ P.h_feq (1 / x) (one_div_pos.mpr hx) :), ← mul_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ P.g (1 / x) = (P.ε⁻¹ * (↑(x ^ P.k) : ℂ) * (P.ε * (↑((1 / x) ^ P.k) : ℂ))) • P.g (1 / x)
have h : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) * (P.ε * (↑((1 / x) ^ P.k) : ℂ)) = 1
Tactic: convert! (one_smul ℂ (P.g (1 / x))).symm using 2
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ P.ε⁻¹ * (↑(x ^ P.k) : ℂ) * (P.ε * (↑((1 / x) ^ P.k) : ℂ)) = 1
have h : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) * (P.ε * (↑(x ^ P.k) : ℂ)⁻¹) = 1
Tactic: rw [one_div, inv_rpow hx.le, ofReal_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
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.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) fun (x : ℝ) ↦
    x ^ r
have 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⁻¹)
Tactic: have := (P.hg_top (-(r + P.k))).comp_tendsto tendsto_inv_nhdsGT_zero
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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⁻¹)
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) fun (x : ℝ) ↦
    x ^ r
have 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‖
Tactic: simp_rw [IsBigO, IsBigOWith, eventually_nhdsWithin_iff] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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)
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : ℝ) in 𝓝 0,
      Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ c * ‖x ^ r‖
have 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‖
Tactic: obtain ⟨C, hC⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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)
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : ℝ) in 𝓝 0,
      Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ c * ‖x ^ r‖
have h : ∀ᶠ (x : ℝ) in 𝓝 0,
  Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
Tactic: use ‖P.ε‖ * C
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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)
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
have h : ∀ (hx : 0 < x), ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
Tactic: (hx : 0 < x)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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 : ℝ) in 𝓝 0,
    Membership.mem (γ := Set ℝ) (Ioi 0) x → ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
have 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‖
Tactic: filter_upwards [hC] with x hC' (hx : 0 < x)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
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
⊢ ‖P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
have h_nv2 : (↑(x ^ P.k) : ℂ) ≠ 0
Tactic: have h_nv2 : ↑(x ^ P.k) ≠ (0 : ℂ) := ofReal_ne_zero.mpr (rpow_pos_of_pos hx _).ne'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
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.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
have h_nv : P.ε⁻¹ * (↑(x ^ P.k) : ℂ) ≠ 0
Tactic: have h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0 := mul_ne_zero P.symm.hε h_nv2