awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
h :
  Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K))
    (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod hp) :
            (a : ↥(monicFactorsMod θ p)) → (↑((span {(↑p : ℤ)}).primesOver (𝓞 K)) : Type u_1))
          (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦ Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) x)
            (Polynomial.map (Int.castRingHom (ZMod p)) Q) hQ)) :
      Ideal (𝓞 K))
⊢ Membership.mem (γ := Multiset (Ideal (𝓞 K)))
    (normalizedFactors (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})))
    (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod hp) :
            (a : ↥(monicFactorsMod θ p)) → (↑((span {(↑p : ℤ)}).primesOver (𝓞 K)) : Type u_1))
          (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦ Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) x)
            (Polynomial.map (Int.castRingHom (ZMod p)) Q) hQ)) :
      Ideal (𝓞 K))

Tactic:
rw [← mem_primesOver_iff_mem_normalizedFactors _ (by simp [NeZero.ne p])]

Premises used: Ideal.mem_primesOver_iff_mem_normalizedFactors
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
⊢ Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K))
    (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod hp) :
            (a : ↥(monicFactorsMod θ p)) → (↑((span {(↑p : ℤ)}).primesOver (𝓞 K)) : Type u_1))
          (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦ Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) x)
            (Polynomial.map (Int.castRingHom (ZMod p)) Q) hQ)) :
      Ideal (𝓞 K))

Tactic:
((primesOverSpanEquivMonicFactorsMod hp).symm ⟨_, hQ⟩).coe_prop

Premises used: Subtype.coe_prop, Set.Mem, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod, Subtype.mk, Equiv.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
⊢ Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K))
    (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod hp) :
            (a : ↥(monicFactorsMod θ p)) → (↑((span {(↑p : ℤ)}).primesOver (𝓞 K)) : Type u_1))
          (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦ Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) x)
            (Polynomial.map (Int.castRingHom (ZMod p)) Q) hQ)) :
      Ideal (𝓞 K))

Tactic:
exact ((primesOverSpanEquivMonicFactorsMod hp).symm ⟨_, hQ⟩).coe_prop

Premises used: Subtype.coe_prop, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod, Subtype.mk, Equiv.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : NumberField K
hp : ¬p ∣ exponent θ
Q : (ZMod p)[X]
hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) Q
obtain :
  ∀ (S : ℤ[X])
    (hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) (Polynomial.map (Int.castRingHom (ZMod p)) S)),
    ramificationIdx.{0, u_1} (R := ℤ) (S := 𝓞 K) (span {(↑p : ℤ)})
        (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod hp) :
                (a : ↥(monicFactorsMod θ p)) → (↑((span {(↑p : ℤ)}).primesOver (𝓞 K)) : Type u_1))
              (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦
                Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) x)
                (Polynomial.map (Int.castRingHom (ZMod p)) S) hQ)) :
          Ideal (𝓞 K)) =
      multiplicity (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) S)
        (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
⊢ ramificationIdx.{0, u_1} (R := ℤ) (S := 𝓞 K) (span {(↑p : ℤ)})
      (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod hp) :
              (a : ↥(monicFactorsMod θ p)) → (↑((span {(↑p : ℤ)}).primesOver (𝓞 K)) : Type u_1))
            (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦ Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) x)
              Q hQ)) :
        Ideal (𝓞 K)) =
    multiplicity Q (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))

Tactic:
obtain ⟨S, rfl⟩ := (map_surjective _ (ZMod.ringHom_surjective (Int.castRingHom (ZMod p)))) Q

Premises used: Polynomial.map_surjective, ZMod, ZMod.ringHom_surjective, Int.castRingHom, rfl
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : NumberField K
hp : ¬p ∣ exponent θ
S : ℤ[X]
hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) (Polynomial.map (Int.castRingHom (ZMod p)) S)
rw rw₁ :
  multiplicity (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) S)
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)) =
    multiplicity (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) S)
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
⊢ ramificationIdx.{0, u_1} (R := ℤ) (S := 𝓞 K) (span {(↑p : ℤ)})
      (↑((Equiv.symm (primesOverSpanEquivMonicFactorsMod hp) :
              (a : ↥(monicFactorsMod θ p)) → (↑((span {(↑p : ℤ)}).primesOver (𝓞 K)) : Type u_1))
            (Subtype.mk (p := fun (x : (ZMod p)[X]) ↦ Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) x)
              (Polynomial.map (Int.castRingHom (ZMod p)) S) hQ)) :
        Ideal (𝓞 K)) =
    multiplicity (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) S)
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))

Tactic:
rw [ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply]

Premises used: NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
C : ℝ
hC : 0 < C
⊢ Tendsto (β := ℝ) (fun (k : ℕ) ↦ HPow.hPow (β := ℝ) C (↑k : ℝ)⁻¹) atTop (𝓝 1)

Tactic:
((continuous_iff_continuousAt.mpr fun _ ↦ continuousAt_const_rpow hC.ne').tendsto'
    0 1 (rpow_zero C)).comp <| tendsto_inv_atTop_zero.comp tendsto_natCast_atTop_atTop

Premises used: Iff.mpr, tendsto_inv_atTop_zero, Real.rpow_zero, LT.lt.ne', tendsto_natCast_atTop_atTop, Real.continuousAt_const_rpow, Continuous.tendsto', Filter.Tendsto.comp, OfNat.ofNat, continuous_iff_continuousAt
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
simp_rw : Tendsto (β := ℝ) (fun (k : ℕ) ↦ HPow.hPow (α := ℝ) (↑k : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ))) atTop (𝓝 1)
⊢ Tendsto (β := ℝ) (fun (k : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℝ) (↑k : ℝ) (↑k : ℝ)⁻¹) atTop (𝓝 1)

Tactic:
simp_rw [← one_div]

Premises used: one_div
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
⊢ Tendsto (β := ℝ) (fun (k : ℕ) ↦ HPow.hPow (α := ℝ) (↑k : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ))) atTop (𝓝 1)

Tactic:
Tendsto.comp tendsto_rpow_div tendsto_natCast_atTop_atTop

Premises used: tendsto_natCast_atTop_atTop, tendsto_rpow_div, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
⊢ Tendsto (β := ℝ) (fun (k : ℕ) ↦ HPow.hPow (α := ℝ) (↑k : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ))) atTop (𝓝 1)

Tactic:
exact Tendsto.comp tendsto_rpow_div tendsto_natCast_atTop_atTop

Premises used: tendsto_natCast_atTop_atTop, tendsto_rpow_div, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
R : Type u_1
inst : Semiring R
T : Type u_2
l : List T
y x : R
simp_rw :
  Eq.{u_1 + 1} (α := R) (List.sum (List.map (fun (x_1 : T × ℕ) ↦ x • y ^ x_1.2) l.zipIdx))
    (List.sum (List.map (fun (x_1 : R) ↦ x • x_1) (List.map (fun (x : T × ℕ) ↦ y ^ x.2) l.zipIdx)))
⊢ List.sum (List.mapIdx (fun (i : ℕ) (x_1 : T) ↦ x * y ^ i) l) =
    x * List.sum (List.mapIdx (fun (i : ℕ) (x : T) ↦ y ^ i) l)

Tactic:
simp_rw [← smul_eq_mul, List.smul_sum, List.mapIdx_eq_zipIdx_map]

Premises used: List.mapIdx_eq_zipIdx_map, smul_eq_mul, List.smul_sum
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
R : Type u_1
inst : Semiring R
T : Type u_2
l : List T
y x : R
e_a :
  Eq.{u_1 + 1} (α := List R) (List.map (fun (x_1 : T × ℕ) ↦ x • y ^ x_1.2) l.zipIdx)
    (List.map (fun (x_1 : R) ↦ x • x_1) (List.map (fun (x : T × ℕ) ↦ y ^ x.2) l.zipIdx))
⊢ Eq.{u_1 + 1} (α := R) (List.sum (List.map (fun (x_1 : T × ℕ) ↦ x • y ^ x_1.2) l.zipIdx))
    (List.sum (List.map (fun (x_1 : R) ↦ x • x_1) (List.map (fun (x : T × ℕ) ↦ y ^ x.2) l.zipIdx)))

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
R : Type u_1
inst : Semiring R
T : Type u_2
l : List T
y x : R
⊢ Eq.{u_1 + 1} (α := List R) (List.map (fun (x_1 : T × ℕ) ↦ x • y ^ x_1.2) l.zipIdx)
    (List.map (fun (x_1 : R) ↦ x • x_1) (List.map (fun (x : T × ℕ) ↦ y ^ x.2) l.zipIdx))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
T : Type u_1
F : Type u_2
inst : DivisionRing F
l : List T
y : F
hy : y ≠ 1
rw :
  Eq.{u_2 + 1} (α := F)
    (∑ i : Fin l.zipIdx.length,
      match (motive := T × ℕ → F)
        getElem (valid := fun (as : List (T × ℕ)) (i : ℕ) ↦ i < as.length) l.zipIdx (↑i : ℕ) ⋯ with
      | (a, i) => y ^ i)
    (∑ i : Fin l.length, y ^ (↑i : ℕ))
⊢ List.sum (List.mapIdx (fun (i : ℕ) (x : T) ↦ y ^ i) l) = (y ^ l.length - 1) / (y - 1)

Tactic:
rw [← geom_sum_eq hy l.length, List.mapIdx_eq_zipIdx_map, Finset.sum_range,
    ← Fin.sum_univ_fun_getElem]

Premises used: geom_sum_eq, Finset.sum_range, List.mapIdx_eq_zipIdx_map, Fin.sum_univ_fun_getElem, List.length
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
T : Type u_1
F : Type u_2
inst : DivisionRing F
l : List T
y : F
hy : y ≠ 1
simp :
  Eq.{u_2 + 1} (α := F) (∑ x : Fin l.zipIdx.length, y ^ (l.zipIdx.get (⟨(↑x : ℕ), ⋯⟩ : Fin l.zipIdx.length)).2)
    (∑ i : Fin l.length, y ^ (↑i : ℕ))
⊢ Eq.{u_2 + 1} (α := F)
    (∑ i : Fin l.zipIdx.length,
      match (motive := T × ℕ → F)
        getElem (valid := fun (as : List (T × ℕ)) (i : ℕ) ↦ i < as.length) l.zipIdx (↑i : ℕ) ⋯ with
      | (a, i) => y ^ i)
    (∑ i : Fin l.length, y ^ (↑i : ℕ))

Tactic:
simp only
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
T : Type u_1
F : Type u_2
inst : DivisionRing F
l : List T
y : F
hy : y ≠ 1
e : Fin l.zipIdx.length ≃ Fin l.length := finCongr ⋯
x : Fin l.zipIdx.length
⊢ y ^ (l.zipIdx.get (⟨(↑x : ℕ), ⋯⟩ : Fin l.zipIdx.length)).2 =
    y ^ (↑((e : (a : Fin l.zipIdx.length) → Fin l.length) x) : ℕ)

Tactic:
simp [e]
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
T : Type u_1
F : Type u_2
inst : DivisionRing F
l : List T
y : F
hy : y ≠ 1
e : Fin l.zipIdx.length ≃ Fin l.length := finCongr ⋯
⊢ Eq.{u_2 + 1} (α := F) (∑ x : Fin l.zipIdx.length, y ^ (l.zipIdx.get (⟨(↑x : ℕ), ⋯⟩ : Fin l.zipIdx.length)).2)
    (∑ i : Fin l.length, y ^ (↑i : ℕ))

Tactic:
exact Fintype.sum_bijective e e.bijective _ _ fun _ ↦ by simp [e]

Premises used: Equiv.bijective, Fintype.sum_bijective, DFunLike.coe
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
⊢ (∀ (n : ℕ), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)) ↔ f = g

Tactic:
⟨fun h ↦ ?_, fun h n ↦ congrFun (congrArg DFunLike.coe h) ↑n⟩

Premises used: Iff.intro
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
refine : ∀ (h : ∀ (n : ℕ), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)), f = g
⊢ (∀ (n : ℕ), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)) ↔ f = g

Tactic:
refine ⟨fun h ↦ ?_, fun h n ↦ congrFun (congrArg DFunLike.coe h) ↑n⟩
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
a : ∀ (z : ℚ), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) z : ℝ) ((g : (a : ℚ) → ℝ) z : ℝ)
⊢ f = g

Tactic:
ext1 z
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
z : ℚ
a :
  Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑z.num : ℚ) (↑z.den : ℚ)) : ℝ)
    ((g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑z.num : ℚ) (↑z.den : ℚ)) : ℝ)
a₁ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑z.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑z.den : ℚ) : ℝ) =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑z.num : ℚ) (↑z.den : ℚ))
a₂ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑z.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑z.den : ℚ) : ℝ) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑z.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑z.den : ℚ) : ℝ)
a₃ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑z.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑z.den : ℚ) : ℝ) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑z.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑z.den : ℚ) : ℝ)
a₄ a₅ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑z.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑z.den : ℚ) : ℝ) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑z.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑z.den : ℚ) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) z : ℝ) ((g : (a : ℚ) → ℝ) z : ℝ)

Tactic:
rw [← Rat.num_div_den z, map_div₀, map_div₀, h, eq_on_nat_iff_eq_on_int.mp h]

Premises used: Rat.num_div_den, AbsoluteValue.eq_on_nat_iff_eq_on_int, map_div₀, Iff.mp
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
rw :
  (∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)) ↔
    ∃ (c : ℝ), 0 < c ∧ Eq (α := ℚ → ℝ) (fun (x : ℚ) ↦ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c) (⇑g : (a : ℚ) → ℝ)
⊢ (∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)) ↔
    f.IsEquiv g

Tactic:
rw [isEquiv_iff_exists_rpow_eq]

Premises used: AbsoluteValue.isEquiv_iff_exists_rpow_eq
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
⊢ (∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)) ↔
    ∃ (c : ℝ), 0 < c ∧ Eq (α := ℚ → ℝ) (fun (x : ℚ) ↦ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c) (⇑g : (a : ℚ) → ℝ)

Tactic:
⟨fun ⟨c, hc, h⟩ ↦ ⟨c, hc, ?_⟩, fun ⟨c, hc, h⟩ ↦ ⟨c, hc, (congrFun h ·)⟩⟩

Premises used: Exists, Nat.cast, And, HPow.hPow, congrFun, And.intro, LT.lt, Iff.intro, Exists.intro, OfNat.ofNat, Eq, DFunLike.coe, _private.0.Rat.AbsoluteValue.exists_nat_rpow_iff_isEquiv.match_1, _private.0.Rat.AbsoluteValue.exists_nat_rpow_iff_isEquiv.match_2
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
refine :
  (∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)) →
    ∀ (c : ℝ) (hc : 0 < c)
      (h : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)),
      Eq (α := ℚ → ℝ) (fun (x : ℚ) ↦ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c) (⇑g : (a : ℚ) → ℝ)
⊢ (∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)) ↔
    ∃ (c : ℝ), 0 < c ∧ Eq (α := ℚ → ℝ) (fun (x : ℚ) ↦ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c) (⇑g : (a : ℚ) → ℝ)

Tactic:
refine ⟨fun ⟨c, hc, h⟩ ↦ ⟨c, hc, ?_⟩, fun ⟨c, hc, h⟩ ↦ ⟨c, hc, (congrFun h ·)⟩⟩
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
h_1 : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
h₁ : ∀ (x : ℚ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c = (g : (a : ℚ) → ℝ) x
⊢ Eq (α := ℚ → ℝ) (fun (x : ℚ) ↦ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c) (⇑g : (a : ℚ) → ℝ)

Tactic:
ext1 x
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
h_1 : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
x : ℚ
⊢ LE.le (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
h_1 : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
x : ℚ
⊢ LE.le (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
h_1 : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)
x : ℚ
h₁ :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ)) : ℝ) c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
h₂ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
    (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
h₃ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) ^ c =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₄ :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) c /
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) c =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₅ :
  HDiv.hDiv (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) c) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₆ :
  HDiv.hDiv (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num.natAbs : ℚ) : ℝ) c)
      ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₇ :
  HDiv.hDiv (β := ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑x.num.natAbs : ℚ) : ℝ) c)
      ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num.natAbs : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
h₈ h₉ :
  HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num.natAbs : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑x.num.natAbs : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑x.den : ℚ) : ℝ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c = (g : (a : ℚ) → ℝ) x

Tactic:
rw [← Rat.num_div_den x, map_div₀, map_div₀, div_rpow (by positivity) (by positivity), h x.den,
    ← apply_natAbs_eq, ← apply_natAbs_eq, h (natAbs x.num)]

Premises used: Rat.num_div_den, Rat.num, Rat.den, Real.div_rpow, map_div₀, Int.natAbs, AbsoluteValue.apply_natAbs_eq
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
p : ℕ
inst : Fact (Nat.Prime p)
⊢ ∀ (x y : ℚ), (↑(padicNorm p (x * y)) : ℝ) = HMul.hMul (α := ℝ) (↑(padicNorm p x) : ℝ) (↑(padicNorm p y) : ℝ)

Tactic:
simp only [padicNorm.mul, Rat.cast_mul, forall_const]

Premises used: Rat.cast_mul, padicNorm.mul, forall_const
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
⊢ (↑(padicNorm p (x + y)) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(padicNorm p x) : ℝ) (↑(padicNorm p y) : ℝ)

Tactic:
exact_mod_cast padicNorm.triangle_ineq x y

Premises used: padicNorm.triangle_ineq
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
r : ℚ
⊢ Eq (α := ℝ) ((padic p : (a : ℚ) → ℝ) r : ℝ) ((↑(padicNorm p r) : ℝ) : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
n : ℤ
⊢ LE.le (α := ℝ) (↑(padicNorm p (↑n : ℚ)) : ℝ) 1

Tactic:
exact_mod_cast padicNorm.of_int n

Premises used: padicNorm.of_int
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
contrapose! :
  ∀ (hf_nontriv : ∀ (n : ℕ) (_ : n ≠ 0), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)), ¬f.IsNontrivial
⊢ ∃ (n : ℕ), n ≠ 0 ∧ Ne (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)

Tactic:
contrapose! hf_nontriv
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
hf_nontriv : ∀ (n : ℕ) (_ : n ≠ 0), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ ¬f.IsNontrivial

Tactic:
(isNontrivial_iff_ne_trivial f).not_left.mpr <| eq_on_nat_iff_eq.mp fun n ↦ ?_

Premises used: Iff.mpr, Iff.not_left, Iff.mp, Rat.AbsoluteValue.eq_on_nat_iff_eq, AbsoluteValue.isNontrivial_iff_ne_trivial
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
hf_nontriv : ∀ (n : ℕ) (_ : n ≠ 0), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
refine : ∀ (n : ℕ), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((AbsoluteValue.trivial : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
⊢ ¬f.IsNontrivial

Tactic:
refine (isNontrivial_iff_ne_trivial f).not_left.mpr <| eq_on_nat_iff_eq.mp fun n ↦ ?_

Premises used: Iff.mpr, Iff.not_left, Iff.mp, Rat.AbsoluteValue.eq_on_nat_iff_eq, AbsoluteValue.isNontrivial_iff_ne_trivial
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
hf_nontriv : ∀ (n : ℕ) (_ : n ≠ 0), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
n : ℕ
inl : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ) ((AbsoluteValue.trivial : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ)
inr : ∀ (hn : n ≠ 0), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((AbsoluteValue.trivial : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((AbsoluteValue.trivial : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
hf_nontriv : ∀ (n : ℕ) (_ : n ≠ 0), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ) ((AbsoluteValue.trivial : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
hf_nontriv : ∀ (n : ℕ) (_ : n ≠ 0), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
n : ℕ
hn : n ≠ 0
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((AbsoluteValue.trivial : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)

Tactic:
simp [hf_nontriv, hn]
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
obtain :
  ∀ (n : ℕ) (hn1 : n ≠ 0) (hn2 : Ne (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)),
    ∃ (p : ℕ),
      (LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧
          LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)) ∧
        ∀ (m : ℕ),
          LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
              LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
            p ≤ m
⊢ ∃ (p : ℕ),
    (LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧
        LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)) ∧
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          p ≤ m

Tactic:
obtain ⟨n, hn1, hn2⟩ : ∃ n : ℕ, n ≠ 0 ∧ f n ≠ 1 := by
    contrapose! hf_nontriv
    refine (isNontrivial_iff_ne_trivial f).not_left.mpr <| eq_on_nat_iff_eq.mp fun n ↦ ?_
    rcases eq_or_ne n 0 with rfl | hn
    · simp
    · simp [hf_nontriv, hn]