awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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
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 ℤ))
⊢ 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 ℤ))

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))]

Premises used: Valuation.IsRankOneDiscrete.generator_lt_one, pow_le_pow_iff_right_of_lt_one₀, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, inv_mul_le_one₀, map_div₀, IsDedekindDomain.HeightOneSpectrum.intValuation_def, RatFunc.induction_on, div_inv_eq_mul, Set.pi, div_le_one₀, WithZero.exp_neg
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
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 ℤ))
⊢ ¬Valuation.IsEquiv (R := K⟮X⟯) (valuation K⟮X⟯ p) (inftyValuation K)

Tactic:
simp only [isEquiv_iff_val_le_one]

Premises used: Valuation.isEquiv_iff_val_le_one
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
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 ℤ))
⊢ ¬∀ {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:
push Not

Premises used: Not
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 ℤ))

Tactic:
⟨X, .inl ⟨p.valuation_le_one _, ?_⟩⟩

Premises used: RatFunc.X, And.intro, Exists.intro, Or.inl, IsDedekindDomain.HeightOneSpectrum.valuation_le_one
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
refine :
  LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) X :
      WithZero (Multiplicative ℤ))
⊢ ∃ (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:
refine ⟨X, .inl ⟨p.valuation_le_one _, ?_⟩⟩
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
rw : LT.lt (α := ℤ) 0 1
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) X :
      WithZero (Multiplicative ℤ))

Tactic:
rw [inftyValuation.X, ← log_lt_iff_lt_exp one_ne_zero, log_one]

Premises used: RatFunc.inftyValuation.X, WithZero.log_one, one_ne_zero, WithZero.log_lt_iff_lt_exp
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
⊢ LT.lt (α := ℤ) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
⊢ LT.lt (α := ℤ) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
by_contra : ∀ (h : Eq (α := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) (valuation K⟮X⟯ p) (inftyValuation K)), False
⊢ Ne (α := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) (valuation K⟮X⟯ p) (inftyValuation K)

Tactic:
by_contra h
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
h : Eq (α := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) (valuation K⟮X⟯ p) (inftyValuation K)
⊢ False

Tactic:
absurd Valuation.IsEquiv.refl (h ▸ adicValuation_not_isEquiv_infty_valuation p)

Premises used: absurd, Valuation.IsEquiv.refl
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
h : Eq (α := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) (valuation K⟮X⟯ p) (inftyValuation K)
⊢ False

Tactic:
exact absurd Valuation.IsEquiv.refl (h ▸ adicValuation_not_isEquiv_infty_valuation p)

Premises used: absurd, Valuation.IsEquiv.refl
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
⊢ ∃ (u : HeightOneSpectrum K[X]), v.IsEquiv (valuation K⟮X⟯ u)

Tactic:
⟨_, valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one hle⟩

Premises used: RatFunc.valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one, Exists.intro
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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))
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))
⊢ 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

Premises used: RatFunc.X, lt_or_ge, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 : Γ)
⊢ v.IsEquiv (inftyValuation K)

Tactic:
have hv := valuation_isEquiv_inftyValuation_of_one_lt_valuation_X hlt
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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))

Tactic:
.inl ⟨hv, ?_⟩

Premises used: Xor, And.intro, Or.inl
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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)
inl : ¬∃! 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))

Tactic:
refine .inl ⟨hv, ?_⟩
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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)
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
⊢ ¬∃! u : HeightOneSpectrum K[X], v.IsEquiv (valuation K⟮X⟯ u)

Tactic:
simp only [ExistsUnique, not_exists, not_and, not_forall]

Premises used: not_exists, ExistsUnique, not_and, Classical.not_forall
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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)
pw : HeightOneSpectrum K[X]
hw : v.IsEquiv (valuation K⟮X⟯ pw)
⊢ ∃ (x : HeightOneSpectrum K[X]) (_ : v.IsEquiv (valuation K⟮X⟯ x)), ¬x = pw

Tactic:
absurd (hw.symm.trans hv) (adicValuation_not_isEquiv_infty_valuation pw)

Premises used: RatFunc.adicValuation_not_isEquiv_infty_valuation, Valuation.IsEquiv.trans, absurd, Valuation.IsEquiv.symm
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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)
pw : HeightOneSpectrum K[X]
hw : v.IsEquiv (valuation K⟮X⟯ pw)
⊢ ∃ (x : HeightOneSpectrum K[X]) (_ : v.IsEquiv (valuation K⟮X⟯ x)), ¬x = pw

Tactic:
exact absurd (hw.symm.trans hv) (adicValuation_not_isEquiv_infty_valuation pw)

Premises used: RatFunc.adicValuation_not_isEquiv_infty_valuation, Valuation.IsEquiv.trans, absurd, Valuation.IsEquiv.symm
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 : Γ)
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))
⊢ 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

Premises used: RatFunc.valuation_isEquiv_adic_of_valuation_X_le_one
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 : Γ)
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:
.inr ⟨⟨pw, hw, fun pw' hw' ↦ eq_of_valuation_isEquiv_valuation (hw'.symm.trans hw)⟩,
      fun hv ↦ absurd (hw.symm.trans hv) (adicValuation_not_isEquiv_infty_valuation pw)⟩

Premises used: RatFunc.adicValuation_not_isEquiv_infty_valuation, Xor, Valuation.IsEquiv.trans, absurd, And.intro, Exists.intro, Valuation.IsEquiv.symm, IsDedekindDomain.HeightOneSpectrum.eq_of_valuation_isEquiv_valuation, Or.inr
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 : Γ)
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:
exact .inr ⟨⟨pw, hw, fun pw' hw' ↦ eq_of_valuation_isEquiv_valuation (hw'.symm.trans hw)⟩,
      fun hv ↦ absurd (hw.symm.trans hv) (adicValuation_not_isEquiv_infty_valuation pw)⟩
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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⟯
hni : ¬v.IsEquiv (inftyValuation K)
⊢ ∃! u : HeightOneSpectrum K[X], v.IsEquiv (valuation K⟮X⟯ u)

Tactic:
valuation_isEquiv_infty_or_adic.or.resolve_left hni

Premises used: Or.resolve_left, RatFunc.valuation_isEquiv_infty_or_adic, Xor.or
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
rw :
  ∀ ⦃a : ℤ⦄,
    Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} a → a ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}
⊢ Disjoint (α := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}

Tactic:
rw [Set.disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
this : ∀ (k : ℤ) (h₁ : beattySeq r k = j), j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}
⊢ Membership.mem (γ := Set ℤ) {x : ℤ | ∃ (k : ℤ), beattySeq r k = x} j → j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}

Tactic:
⟨k, h₁⟩
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : beattySeq r k = j
this : ∀ (m : ℤ) (h₂ : beattySeq' s m = j), False
⊢ j ∉ {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}

Tactic:
⟨m, h₂⟩
-- Module: Mathlib.NumberTheory.Rayleigh
Goal:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : beattySeq r k = j
m : ℤ
h₂ : beattySeq' s m = j
rw :
  ∀ (h₁ : (↑j : ℝ) / r ≤ (↑k : ℝ) ∧ (↑k : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) 1 / r) (m : ℤ) (h₂ : beattySeq' s m = j),
    False
⊢ False

Tactic:
rw [beattySeq, Int.floor_eq_iff, ← div_le_iff₀ hrs.pos, ← lt_div_iff₀ hrs.pos] at h₁

Premises used: div_le_iff₀, lt_div_iff₀, Real.HolderTriple.pos, Int.floor_eq_iff, beattySeq
-- Module: Mathlib.NumberTheory.Rayleigh
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
⊢ (↑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₂

Premises used: Int.ceil_eq_iff, Real.HolderConjugate.symm, Real.HolderTriple.pos, Int.cast_add, div_lt_iff₀, sub_eq_iff_eq_add, add_sub_cancel_right, beattySeq', le_div_iff₀, Int.cast_one
-- Module: Mathlib.NumberTheory.Rayleigh
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
⊢ (↑j : ℝ) / r + (↑j : ℝ) / s < HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ)

Tactic:
have h₃ := add_lt_add_of_le_of_lt h₁.1 h₂.1
-- Module: Mathlib.NumberTheory.Rayleigh
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 : ℝ)
⊢ 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
-- Module: Mathlib.NumberTheory.Rayleigh
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
⊢ (↑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₄

Premises used: Real.HolderConjugate.inv_add_inv_eq_one, right_distrib, div_eq_inv_mul, one_mul
-- Module: Mathlib.NumberTheory.Rayleigh
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 : ℝ)
⊢ 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₄

Premises used: Real.HolderConjugate.inv_add_inv_eq_one, right_distrib, div_eq_inv_mul, one_mul
-- Module: Mathlib.NumberTheory.Rayleigh
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
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑j : ℝ) (↑1 : ℝ)

Tactic:
rw [← Int.cast_one] at h₄

Premises used: Int.cast_one
-- Module: Mathlib.NumberTheory.Rayleigh
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 : ℝ)
⊢ j < k + m

Tactic:
simp_rw [← Int.cast_add, Int.cast_lt, Int.lt_add_one_iff] at h₃ h₄

Premises used: Int.cast_add, Int.cast_lt, Int.lt_add_one_iff
-- Module: Mathlib.NumberTheory.Rayleigh
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
⊢ k + m ≤ j

Tactic:
simp_rw [← Int.cast_add, Int.cast_lt, Int.lt_add_one_iff] at h₃ h₄

Premises used: Int.cast_add, Int.cast_lt, Int.lt_add_one_iff