awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
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)
this :
  LiesOver (A := ℤ) (B := 𝓞 K) (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
    (span {(↑p : ℤ)})
⊢ RingHom.comp
      (algebraMap (ZMod p)
        (HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X])
          (span {Polynomial.map (Int.castRingHom (ZMod p)) Q})))
      (Int.quotientSpanNatEquivZMod p).toRingHom =
    (ZModXQuotSpanEquivQuotSpanPair hp hQ).symm.toRingHom.comp
      (algebraMap (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))
        (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K))
          (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))))
have h : ∀ (x : ℤ),
  Eq (α :=
    HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q}))
    ((RingHom.comp
            (RingHom.comp
              (algebraMap (ZMod p)
                (HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X])
                  (span {Polynomial.map (Int.castRingHom (ZMod p)) Q})))
              (Int.quotientSpanNatEquivZMod p).toRingHom)
            (Ideal.Quotient.mk (span {(↑p : ℤ)})) :
          (a : ℤ) → (ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q})
        x :
      HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q}))
    ((RingHom.comp (β := HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))
            ((ZModXQuotSpanEquivQuotSpanPair hp hQ).symm.toRingHom.comp
              (algebraMap (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))
                (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K))
                  (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K)))))))
            (Ideal.Quotient.mk (span {(↑p : ℤ)})) :
          (a : ℤ) → (ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q})
        x :
      HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q}))
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
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)
this :
  LiesOver (A := ℤ) (B := 𝓞 K) (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))
    (span {(↑p : ℤ)})
⊢ Module.finrank.{0, u_1} (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))
      (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K))
        (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K))))) =
    Module.finrank (ZMod p)
      (HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q}))
have refine : HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K))
    (span (insert (↑p : 𝓞 K) (singleton (α := 𝓞 K) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q : 𝓞 K)))) ≃+*
  HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q})
Tactic: refine Algebra.finrank_eq_of_equiv_equiv (Int.quotientSpanNatEquivZMod p) ?_ (by ext; simp)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
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
⊢ inertiaDeg.{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)) =
    Q.natDegree
have obtain : ∀ (S : ℤ[X])
  (hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) (Polynomial.map (Int.castRingHom (ZMod p)) S)),
  inertiaDeg.{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)) =
    natDegree (R := ZMod p) (Polynomial.map (Int.castRingHom (ZMod p)) S)
Tactic: obtain ⟨S, rfl⟩ := (map_surjective _ (ZMod.ringHom_surjective (Int.castRingHom (ZMod p)))) Q
Cleared hypotheses: Q, hQ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
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)
⊢ inertiaDeg.{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)) =
    natDegree (R := ZMod p) (Polynomial.map (Int.castRingHom (ZMod p)) S)
have rw : natDegree (R := ZMod p) (Polynomial.map (Int.castRingHom (ZMod p)) S) =
  natDegree (R := ZMod p) (Polynomial.map (Int.castRingHom (ZMod p)) S)
Tactic: rw [inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
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)
⊢ 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)) Q) hQ)) :
        Ideal (𝓞 K)) =
    multiplicity (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
have rw : multiplicity.{u_1} (α := Ideal (𝓞 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))
    (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})) =
  multiplicity (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
    (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
Tactic: rw [ramificationIdx_eq_multiplicity (map_ne_bot_of_ne_bot (by simp [NeZero.ne p])) inferInstance]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
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)
⊢ multiplicity.{u_1} (α := Ideal (𝓞 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))
      (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})) =
    multiplicity (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
have h : emultiplicity.{u_1} (α := Ideal (𝓞 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))
    (Ideal.map (R := ℤ) (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (span {(↑p : ℤ)})) =
  emultiplicity (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
    (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
Tactic: apply multiplicity_eq_of_emultiplicity_eq
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
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 (γ := 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))
have 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))
Tactic: rw [← mem_primesOver_iff_mem_normalizedFactors _ (by simp [NeZero.ne p])]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
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
⊢ 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 ℤ θ))
have 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 ℤ θ))
Tactic: obtain ⟨S, rfl⟩ := (map_surjective _ (ZMod.ringHom_surjective (Int.castRingHom (ZMod p)))) Q
Cleared hypotheses: Q, hQ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
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)
⊢ 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 ℤ θ))
have 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 ℤ θ))
Tactic: rw [ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (k : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℝ) (↑k : ℝ) (↑k : ℝ)⁻¹) atTop (𝓝 1)
have simp_rw : Tendsto (β := ℝ) (fun (k : ℕ) ↦ HPow.hPow (α := ℝ) (↑k : ℝ) (HDiv.hDiv (α := ℝ) 1 (↑k : ℝ))) atTop (𝓝 1)
Tactic: simp_rw [← one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
R : Type u_1
inst : Semiring R
T : Type u_2
l : List T
y x : R
⊢ 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)
have 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)))
Tactic: simp_rw [← smul_eq_mul, List.smul_sum, List.mapIdx_eq_zipIdx_map]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
R : Type u_1
inst : Semiring R
T : Type u_2
l : List T
y x : R
⊢ 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)))
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
T : Type u_1
F : Type u_2
inst : DivisionRing F
l : List T
y : F
hy : y ≠ 1
⊢ List.sum (List.mapIdx (fun (i : ℕ) (x : T) ↦ y ^ i) l) = (y ^ l.length - 1) / (y - 1)
have 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 : ℕ) sorry with
    | (a, i) => y ^ i)
  (∑ i : Fin l.length, y ^ (↑i : ℕ))
Tactic: rw [← geom_sum_eq hy l.length, List.mapIdx_eq_zipIdx_map, Finset.sum_range,
    ← Fin.sum_univ_fun_getElem]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
T : Type u_1
F : Type u_2
inst : DivisionRing F
l : List T
y : F
hy : y ≠ 1
⊢ 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 : ℕ))
have simp : Eq.{u_2 + 1} (α := F) (∑ x : Fin l.zipIdx.length, y ^ (l.zipIdx.get (⟨(↑x : ℕ), sorry⟩ : Fin l.zipIdx.length)).2)
  (∑ i : Fin l.length, y ^ (↑i : ℕ))
Tactic: simp only
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f g : AbsoluteValue ℚ ℝ
⊢ (∀ (n : ℕ), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)) ↔ f = g
have refine : ∀ (h : ∀ (n : ℕ), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)), f = g
Tactic: refine ⟨fun h ↦ ?_, fun h n ↦ congrFun (congrArg DFunLike.coe h) ↑n⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
⊢ f = g
have a : ∀ (z : ℚ), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) z : ℝ) ((g : (a : ℚ) → ℝ) z : ℝ)
Tactic: ext1 z
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
z : ℚ
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) z : ℝ) ((g : (a : ℚ) → ℝ) z : ℝ)
have a : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑z.num : ℚ) (↑z.den : ℚ)) : ℝ)
  ((g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑z.num : ℚ) (↑z.den : ℚ)) : ℝ)
Tactic: rw [← Rat.num_div_den z, map_div₀, map_div₀, h, eq_on_nat_iff_eq_on_int.mp h]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ)) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) z : ℝ) ((g : (a : ℚ) → ℝ) z : ℝ)
have a₁ : HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑z.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑z.den : ℚ) : ℝ) =
  (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑z.num : ℚ) (↑z.den : ℚ))
Tactic: rw [← Rat.num_div_den z, map_div₀, map_div₀, h, eq_on_nat_iff_eq_on_int.mp h]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ))
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) z : ℝ) ((g : (a : ℚ) → ℝ) z : ℝ)
have a₂ : HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑z.num : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑z.den : ℚ) : ℝ) =
  HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑z.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑z.den : ℚ) : ℝ)
Tactic: rw [← Rat.num_div_den z, map_div₀, map_div₀, h, eq_on_nat_iff_eq_on_int.mp h]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) z : ℝ) ((g : (a : ℚ) → ℝ) z : ℝ)
have a₃ : HDiv.hDiv (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑z.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑z.den : ℚ) : ℝ) =
  HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑z.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑z.den : ℚ) : ℝ)
Tactic: rw [← Rat.num_div_den z, map_div₀, map_div₀, h, eq_on_nat_iff_eq_on_int.mp h]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) z : ℝ) ((g : (a : ℚ) → ℝ) z : ℝ)
have a₄ : HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑z.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑z.den : ℚ) : ℝ) =
  HDiv.hDiv (α := ℝ) (β := ℝ) ((g : (a : ℚ) → ℝ) (↑z.num : ℚ) : ℝ) ((g : (a : ℚ) → ℝ) (↑z.den : ℚ) : ℝ)
Tactic: rw [← Rat.num_div_den z, map_div₀, map_div₀, h, eq_on_nat_iff_eq_on_int.mp h]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f g : AbsoluteValue ℚ ℝ
⊢ (∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (g : (a : ℚ) → ℝ) (↑n : ℚ)) ↔
    f.IsEquiv g
have 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 : ℚ) → ℝ)
Tactic: rw [isEquiv_iff_exists_rpow_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ) → ℝ)
have 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 : ℚ) → ℝ)
Tactic: refine ⟨fun ⟨c, hc, h⟩ ↦ ⟨c, hc, ?_⟩, fun ⟨c, hc, h⟩ ↦ ⟨c, hc, (congrFun h ·)⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ)
⊢ Eq (α := ℚ → ℝ) (fun (x : ℚ) ↦ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c) (⇑g : (a : ℚ) → ℝ)
have h₁ : ∀ (x : ℚ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c = (g : (a : ℚ) → ℝ) x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) x : ℝ) c = (g : (a : ℚ) → ℝ) x
have h₁ : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ)) : ℝ) c =
  (g : (a : ℚ) → ℝ) (HDiv.hDiv (α := ℚ) (↑x.num : ℚ) (↑x.den : ℚ))
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)]