awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
inst_4 : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) ≠
    0
hp0 : p ≠ 0
pi : K[X] := πᵥ
hpi_def : pi = πᵥ
⊢ LE.le.{u_2} (α := Γ)
      ((v : (a : K⟮X⟯) → Γ)
          (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)) :
        Γ)
      (1 : Γ) ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K⟮X⟯ Pᵥ : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
          (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
have hpi : v.IsUniformizer (↑pi : K⟮X⟯)
Tactic: have hpi : v.IsUniformizer (pi : RatFunc K) := uniformizingPolynomial_isUniformizer hle
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
inst_4 : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) ≠
    0
hp0 : p ≠ 0
pi : K[X] := πᵥ
hpi_def : pi = πᵥ
hpi : v.IsUniformizer (↑pi : K⟮X⟯)
⊢ LE.le.{u_2} (α := Γ)
      ((v : (a : K⟮X⟯) → Γ)
          (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)) :
        Γ)
      (1 : Γ) ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K⟮X⟯ Pᵥ : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
          (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
have inr : HDiv.hDiv (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) : Γ)
      ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : Γ) ≤
    1 ↔
  HMul.hMul (α := WithZero (Multiplicative ℤ))
      (exp (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) : ℤ))⁻¹
      (exp (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {q})))) : ℤ)) ≤
    1
Tactic: simp only [map_div₀, valuation_of_algebraMap, intValuation_def, exp_neg, if_neg hp0,
        if_neg hq0, div_inv_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
inst_4 : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) ≠
    0
hp0 : p ≠ 0
pi : K[X] := πᵥ
hpi_def : pi = πᵥ
hpi : v.IsUniformizer (↑pi : K⟮X⟯)
⊢ HDiv.hDiv (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) : Γ)
        ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : Γ) ≤
      1 ↔
    HMul.hMul (α := WithZero (Multiplicative ℤ))
        (exp
            (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) :
              ℤ))⁻¹
        (exp
          (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {q})))) : ℤ)) ≤
      1
have inr : HDiv.hDiv (α := Γ) (β := Γ)
      ((v : (a : K⟮X⟯) → Γ)
          ((↑πᵥ : K⟮X⟯) ^
            Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) :
        Γ)
      ((v : (a : K⟮X⟯) → Γ)
          ((↑πᵥ : K⟮X⟯) ^
            Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {q})))) :
        Γ) ≤
    1 ↔
  HMul.hMul (α := WithZero (Multiplicative ℤ))
      (exp (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) : ℤ))⁻¹
      (exp (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {q})))) : ℤ)) ≤
    1
Tactic: rw [valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hp0,
        valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hq0]
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
inst_4 : v.IsRankOneDiscrete
f : K⟮X⟯
hf0 : f ≠ 0
⊢ LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) f : Γ) (1 : Γ) ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K⟮X⟯ Pᵥ : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
          f :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
have inr : ∀ (p q : K[X]) (hq0 : q ≠ 0)
  (hf0 :
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) ≠
      0),
  LE.le.{u_2} (α := Γ)
      ((v : (a : K⟮X⟯) → Γ)
          (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)) :
        Γ)
      (1 : Γ) ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K⟮X⟯ Pᵥ : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
          (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
Tactic: induction f using RatFunc.induction_on with
    | f p q hq0 =>
      have hp0 : p ≠ 0 := by simp_all
      set pi := πᵥ with hpi_def
      have hpi : v.IsUniformizer (pi : RatFunc K) := uniformizingPolynomial_isUniformizer hle
      simp only [map_div₀, valuation_of_algebraMap, intValuation_def, exp_neg, if_neg hp0,
        if_neg hq0, div_inv_eq_mul]
      rw [valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hp0,
        valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hq0]
      simp_all [div_le_one₀, inv_mul_le_one₀,
        (pow_le_pow_iff_right_of_lt_one₀ (by simp_all) (IsRankOneDiscrete.generator_lt_one v))]
Cleared hypotheses: f, hf0
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
⊢ ¬Valuation.IsEquiv (R := K⟮X⟯) (valuation K⟮X⟯ p) (inftyValuation K)
have simp : ¬∀ {x : K⟮X⟯},
    LE.le (α := WithZero (Multiplicative ℤ))
        (((valuation K⟮X⟯ p : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
            x :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) ↔
      LE.le (α := WithZero (Multiplicative ℤ))
        (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
            x :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
Tactic: simp only [isEquiv_iff_val_le_one]
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
⊢ ¬∀ {x : K⟮X⟯},
      LE.le (α := WithZero (Multiplicative ℤ))
          (((valuation K⟮X⟯ p : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
                (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
              x :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ)) ↔
        LE.le (α := WithZero (Multiplicative ℤ))
          (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
                (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
              x :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ))
have push : ∃ (x : K⟮X⟯),
  LE.le (α := WithZero (Multiplicative ℤ))
        (((valuation K⟮X⟯ p : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
            x :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) ∧
      LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
        (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
            x :
          WithZero (Multiplicative ℤ)) ∨
    LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
        (((valuation K⟮X⟯ p : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
            x :
          WithZero (Multiplicative ℤ)) ∧
      LE.le (α := WithZero (Multiplicative ℤ))
        (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
            x :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
Tactic: push Not
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
⊢ ∃ (x : K⟮X⟯),
    LE.le (α := WithZero (Multiplicative ℤ))
          (((valuation K⟮X⟯ p : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
                (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
              x :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ)) ∧
        LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
          (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
                (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
              x :
            WithZero (Multiplicative ℤ)) ∨
      LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
          (((valuation K⟮X⟯ p : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
                (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
              x :
            WithZero (Multiplicative ℤ)) ∧
        LE.le (α := WithZero (Multiplicative ℤ))
          (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
                (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
              x :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ))
have refine : LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
  (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) X :
    WithZero (Multiplicative ℤ))
Tactic: refine ⟨X, .inl ⟨p.valuation_le_one _, ?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) X :
      WithZero (Multiplicative ℤ))
have rw : LT.lt (α := ℤ) 0 1
Tactic: rw [inftyValuation.X, ← log_lt_iff_lt_exp one_ne_zero, log_one]
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsRankOneDiscrete
inst_3 : IsTrivialOn K v
inst_4 : DecidableEq K⟮X⟯
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u : HeightOneSpectrum K[X], v.IsEquiv (valuation K⟮X⟯ u))
have inl : ∀ (hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)),
  Xor (v.IsEquiv (inftyValuation K)) (∃! u : HeightOneSpectrum K[X], v.IsEquiv (valuation K⟮X⟯ u))
Tactic: rcases lt_or_ge 1 (v X) with hlt | hge
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsRankOneDiscrete
inst_3 : IsTrivialOn K v
inst_4 : DecidableEq K⟮X⟯
inl :
  ∀ (hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)),
    Xor (v.IsEquiv (inftyValuation K)) (∃! u : HeightOneSpectrum K[X], v.IsEquiv (valuation K⟮X⟯ u))
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u : HeightOneSpectrum K[X], v.IsEquiv (valuation K⟮X⟯ u))
have inr : ∀ (hge : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)),
  Xor (v.IsEquiv (inftyValuation K)) (∃! u : HeightOneSpectrum K[X], v.IsEquiv (valuation K⟮X⟯ u))
Tactic: rcases lt_or_ge 1 (v X) with hlt | hge
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsRankOneDiscrete
inst_3 : IsTrivialOn K v
inst_4 : DecidableEq K⟮X⟯
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u : HeightOneSpectrum K[X], v.IsEquiv (valuation K⟮X⟯ u))
have hv : v.IsEquiv (inftyValuation K)
Tactic: have hv := valuation_isEquiv_inftyValuation_of_one_lt_valuation_X hlt
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsRankOneDiscrete
inst_3 : IsTrivialOn K v
inst_4 : DecidableEq K⟮X⟯
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
hv : v.IsEquiv (inftyValuation K)
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u : HeightOneSpectrum K[X], v.IsEquiv (valuation K⟮X⟯ u))
have inl : ¬∃! u : HeightOneSpectrum K[X], v.IsEquiv (valuation K⟮X⟯ u)
Tactic: refine .inl ⟨hv, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsRankOneDiscrete
inst_3 : IsTrivialOn K v
inst_4 : DecidableEq K⟮X⟯
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
hv : v.IsEquiv (inftyValuation K)
⊢ ¬∃! u : HeightOneSpectrum K[X], v.IsEquiv (valuation K⟮X⟯ u)
have inl : ∀ (x : HeightOneSpectrum K[X]),
  v.IsEquiv (valuation K⟮X⟯ x) → ∃ (x_1 : HeightOneSpectrum K[X]) (_ : v.IsEquiv (valuation K⟮X⟯ x_1)), ¬x_1 = x
Tactic: simp only [ExistsUnique, not_exists, not_and, not_forall]
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsRankOneDiscrete
inst_3 : IsTrivialOn K v
inst_4 : DecidableEq K⟮X⟯
hge : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u : HeightOneSpectrum K[X], v.IsEquiv (valuation K⟮X⟯ u))
have inr : ∀ (pw : HeightOneSpectrum K[X]) (hw : v.IsEquiv (valuation K⟮X⟯ pw)),
  Xor (v.IsEquiv (inftyValuation K)) (∃! u : HeightOneSpectrum K[X], v.IsEquiv (valuation K⟮X⟯ u))
Tactic: obtain ⟨pw, hw⟩ := valuation_isEquiv_adic_of_valuation_X_le_one hge
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
⊢ Disjoint (α := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}
have rw : ∀ ⦃a : ℤ⦄,
  Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} a → a ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}
Tactic: rw [Set.disjoint_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j → j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}
have this : ∀ (k : ℤ) (h₁ : beattySeq r k = j), j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}
Tactic: ⟨k, h₁⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : beattySeq r k = j
⊢ j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}
have this : ∀ (m : ℤ) (h₂ : beattySeq' s m = j), False
Tactic: ⟨m, h₂⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (goal)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : beattySeq r k = j
m : ℤ
h₂ : beattySeq' s m = j
⊢ False
have rw : ∀ (h₁ : (↑j : ℝ) / r ≤ (↑k : ℝ) ∧ (↑k : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r) (m : ℤ) (h₂ : beattySeq' s m = j), False
Tactic: rw [beattySeq, Int.floor_eq_iff, ← div_le_iff₀ hrs.pos, ← lt_div_iff₀ hrs.pos] at h₁
Cleared hypotheses: h₁, m, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : (↑j : ℝ) / r ≤ (↑k : ℝ) ∧ (↑k : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r
m : ℤ
h₂ : beattySeq' s m = j
⊢ False
have h₃ : (↑j : ℝ) / s < (↑m : ℝ) ∧ (↑m : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s
Tactic: rw [beattySeq', sub_eq_iff_eq_add, Int.ceil_eq_iff, Int.cast_add, Int.cast_one,
    add_sub_cancel_right, ← div_lt_iff₀ hrs.symm.pos, ← le_div_iff₀ hrs.symm.pos] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : (↑j : ℝ) / r ≤ (↑k : ℝ) ∧ (↑k : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r
m : ℤ
h₂ : (↑j : ℝ) / s < (↑m : ℝ) ∧ (↑m : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s
⊢ False
have h₃ : (↑j : ℝ) / r + (↑j : ℝ) / s < HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ)
Tactic: have h₃ := add_lt_add_of_le_of_lt h₁.1 h₂.1
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : (↑j : ℝ) / r ≤ (↑k : ℝ) ∧ (↑k : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r
m : ℤ
h₂ : (↑j : ℝ) / s < (↑m : ℝ) ∧ (↑m : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s
h₃ : (↑j : ℝ) / r + (↑j : ℝ) / s < HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ)
⊢ False
have h₄ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r + HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s
Tactic: have h₄ := add_lt_add_of_lt_of_le h₁.2 h₂.2
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : (↑j : ℝ) / r ≤ (↑k : ℝ) ∧ (↑k : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r
m : ℤ
h₂ : (↑j : ℝ) / s < (↑m : ℝ) ∧ (↑m : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s
h₃ : (↑j : ℝ) / r + (↑j : ℝ) / s < HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ)
h₄ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r + HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s
⊢ False
have h₅ : (↑j : ℝ) < HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ)
Tactic: simp_rw [div_eq_inv_mul, ← right_distrib, hrs.inv_add_inv_eq_one, one_mul] at h₃ h₄
Cleared hypotheses: h₃, h₄
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : (↑j : ℝ) / r ≤ (↑k : ℝ) ∧ (↑k : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r
m : ℤ
h₂ : (↑j : ℝ) / s < (↑m : ℝ) ∧ (↑m : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s
h₃ : (↑j : ℝ) / r + (↑j : ℝ) / s < HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ)
h₄ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r + HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s
h₅ : (↑j : ℝ) < HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ)
⊢ False
have h₆ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1
Tactic: simp_rw [div_eq_inv_mul, ← right_distrib, hrs.inv_add_inv_eq_one, one_mul] at h₃ h₄
Cleared hypotheses: h₃, h₄
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : (↑j : ℝ) / r ≤ (↑k : ℝ) ∧ (↑k : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r
m : ℤ
h₂ : (↑j : ℝ) / s < (↑m : ℝ) ∧ (↑m : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s
h₃ : (↑j : ℝ) < HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ)
h₄ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1
⊢ False
have h₅ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) (↑1 : ℝ)
Tactic: rw [← Int.cast_one] at h₄
Cleared hypotheses: h₄
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : (↑j : ℝ) / r ≤ (↑k : ℝ) ∧ (↑k : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r
m : ℤ
h₂ : (↑j : ℝ) / s < (↑m : ℝ) ∧ (↑m : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s
h₃ : (↑j : ℝ) < HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ)
h₄ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) (↑1 : ℝ)
⊢ False
have h₅ : j < k + m
Tactic: simp_rw [← Int.cast_add, Int.cast_lt, Int.lt_add_one_iff] at h₃ h₄
Cleared hypotheses: h₃, h₄
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : (↑j : ℝ) / r ≤ (↑k : ℝ) ∧ (↑k : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r
m : ℤ
h₂ : (↑j : ℝ) / s < (↑m : ℝ) ∧ (↑m : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s
h₃ : (↑j : ℝ) < HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ)
h₄ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) (↑1 : ℝ)
h₅ : j < k + m
⊢ False
have h₆ : k + m ≤ j
Tactic: simp_rw [← Int.cast_add, Int.cast_lt, Int.lt_add_one_iff] at h₃ h₄
Cleared hypotheses: h₃, h₄
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s
h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ False
have h₃ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < (↑j : ℝ) / r + (↑j : ℝ) / s
Tactic: have h₃ := add_lt_add_of_lt_of_le h₁₁ h₂₁
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s
h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
h₃ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < (↑j : ℝ) / r + (↑j : ℝ) / s
⊢ False
have h₄ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r + HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s <
  HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
Tactic: have h₄ := add_lt_add_of_le_of_lt h₁₂ h₂₂
-- Lean 4 proof step from Mathlib.NumberTheory.Rayleigh (hypothesis)
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : (↑k : ℝ) < (↑j : ℝ) / r
h₁₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
h₂₁ : (↑m : ℝ) ≤ (↑j : ℝ) / s
h₂₂ : HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
h₃ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < (↑j : ℝ) / r + (↑j : ℝ) / s
h₄ :
  HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r + HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / s <
    HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 + HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ False
have h₅ : HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < (↑j : ℝ)
Tactic: simp_rw [div_eq_inv_mul, ← right_distrib, hrs.inv_add_inv_eq_one, one_mul] at h₃ h₄
Cleared hypotheses: h₃, h₄