awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : WithVal (Rat.padicValuation p)
⊢ Eq (α := ℚ_[p])
    ((withValUniformEquiv : (a : (Rat.padicValuation p).Completion) → ℚ_[p])
        (↑x : Completion (WithVal (Rat.padicValuation p))) :
      ℚ_[p])
    ((↑((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x) : ℚ_[p]) : ℚ_[p])

Tactic:
simpa [Equiv.toUniformEquivOfIsUniformInducing] using
    extension_coe (Padic.isUniformInducing_cast_withVal (p := p)).uniformContinuous _

Premises used: Equiv.toUniformEquivOfIsUniformInducing, UniformSpace.Completion.extension_coe, Padic.isUniformInducing_cast_withVal, IsUniformInducing.uniformContinuous
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
rw : norm (E := ℚ_[p]) (↑x : ℚ_[p]) ≤ 1 ↔ ¬p ∣ x.den
⊢ norm (E := ℚ_[p]) (↑x : ℚ_[p]) ≤ 1 ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
rw [Rat.padicValuation_le_one_iff]

Premises used: Rat.padicValuation_le_one_iff
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
⊢ norm (E := ℚ_[p]) (↑x : ℚ_[p]) ≤ 1 ↔ ¬p ∣ x.den

Tactic:
⟨fun h ↦ ?_, fun h ↦ Padic.norm_rat_le_one h⟩

Premises used: Iff.intro, Padic.norm_rat_le_one
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
refine : ∀ (h : norm (E := ℚ_[p]) (↑x : ℚ_[p]) ≤ 1), ¬p ∣ x.den
⊢ norm (E := ℚ_[p]) (↑x : ℚ_[p]) ≤ 1 ↔ ¬p ∣ x.den

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Padic.norm_rat_le_one h⟩
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h : norm (E := ℚ_[p]) (↑x : ℚ_[p]) ≤ 1
⊢ ¬p ∣ x.den

Tactic:
simpa [Nat.Prime.coprime_iff_not_dvd Fact.out] using isUnit_iff.1 <| isUnit_den _ h

Premises used: PadicInt.isUnit_iff, PadicInt.isUnit_den, Iff.mp, Nat.Prime.coprime_iff_not_dvd, Fact.out
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp :
  IsClosed (X := Completion (WithVal (Rat.padicValuation p)))
    {x : Completion (WithVal (Rat.padicValuation p)) |
      LE.le (α := WithZero (Multiplicative ℤ))
          ((Valued.v : (a : (Rat.padicValuation p).Completion) → WithZero (Multiplicative ℤ)) x :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ)) ↔
        norm (E := ℚ_[p]) ((withValUniformEquiv : (a : (Rat.padicValuation p).Completion) → ℚ_[p]) x : ℚ_[p]) ≤ 1}
⊢ IsClosed (X := Completion (WithVal (Rat.padicValuation p)))
    {a : Completion (WithVal (Rat.padicValuation p)) |
      norm (E := ℚ_[p]) ((withValUniformEquiv : (a : (Rat.padicValuation p).Completion) → ℚ_[p]) a : ℚ_[p]) ≤ 1 ↔
        LE.le (α := WithZero (Multiplicative ℤ))
          ((Valued.v : (a : (Rat.padicValuation p).Completion) → WithZero (Multiplicative ℤ)) a :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ))}

Tactic:
rw [Set.ext fun _ ↦ Iff.comm]

Premises used: Set.ext, Iff.comm
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp :
  IsClosed (X := Completion (WithVal (Rat.padicValuation p)))
    {x : Completion (WithVal (Rat.padicValuation p)) |
      LE.le (α :=
          MonoidWithZeroHom.ValueGroup₀ (F := (Rat.padicValuation p).Completion →*₀ WithZero (Multiplicative ℤ))
            (↑Valued.v : (Rat.padicValuation p).Completion →*₀ WithZero (Multiplicative ℤ)))
          ((Valuation.restrict Valued.v :
                (a : (Rat.padicValuation p).Completion) →
                  MonoidWithZeroHom.ValueGroup₀
                    (↑Valued.v : (Rat.padicValuation p).Completion →*₀ WithZero (Multiplicative ℤ)))
              x :
            MonoidWithZeroHom.ValueGroup₀ (F := (Rat.padicValuation p).Completion →*₀ WithZero (Multiplicative ℤ))
              (↑Valued.v : (Rat.padicValuation p).Completion →*₀ WithZero (Multiplicative ℤ)))
          (1 :
            MonoidWithZeroHom.ValueGroup₀ (F := (Rat.padicValuation p).Completion →*₀ WithZero (Multiplicative ℤ))
              (↑Valued.v : (Rat.padicValuation p).Completion →*₀ WithZero (Multiplicative ℤ))) ↔
        norm (E := ℚ_[p]) ((withValUniformEquiv : (a : (Rat.padicValuation p).Completion) → ℚ_[p]) x : ℚ_[p]) ≤ 1}
⊢ IsClosed (X := Completion (WithVal (Rat.padicValuation p)))
    {x : Completion (WithVal (Rat.padicValuation p)) |
      LE.le (α := WithZero (Multiplicative ℤ))
          ((Valued.v : (a : (Rat.padicValuation p).Completion) → WithZero (Multiplicative ℤ)) x :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ)) ↔
        norm (E := ℚ_[p]) ((withValUniformEquiv : (a : (Rat.padicValuation p).Completion) → ℚ_[p]) x : ℚ_[p]) ≤ 1}

Tactic:
simp_rw [← Valuation.restrict_le_one_iff Valued.v]

Premises used: Valued.v, Valuation.restrict_le_one_iff
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : IsClopen (X := ℚ_[p]) {y : ℚ_[p] | ‖y‖ ≤ 1}
⊢ IsClosed (X := Completion (WithVal (Rat.padicValuation p)))
    {x : Completion (WithVal (Rat.padicValuation p)) |
      LE.le (α :=
          MonoidWithZeroHom.ValueGroup₀ (F := (Rat.padicValuation p).Completion →*₀ WithZero (Multiplicative ℤ))
            (↑Valued.v : (Rat.padicValuation p).Completion →*₀ WithZero (Multiplicative ℤ)))
          ((Valuation.restrict Valued.v :
                (a : (Rat.padicValuation p).Completion) →
                  MonoidWithZeroHom.ValueGroup₀
                    (↑Valued.v : (Rat.padicValuation p).Completion →*₀ WithZero (Multiplicative ℤ)))
              x :
            MonoidWithZeroHom.ValueGroup₀ (F := (Rat.padicValuation p).Completion →*₀ WithZero (Multiplicative ℤ))
              (↑Valued.v : (Rat.padicValuation p).Completion →*₀ WithZero (Multiplicative ℤ)))
          (1 :
            MonoidWithZeroHom.ValueGroup₀ (F := (Rat.padicValuation p).Completion →*₀ WithZero (Multiplicative ℤ))
              (↑Valued.v : (Rat.padicValuation p).Completion →*₀ WithZero (Multiplicative ℤ))) ↔
        norm (E := ℚ_[p]) ((withValUniformEquiv : (a : (Rat.padicValuation p).Completion) → ℚ_[p]) x : ℚ_[p]) ≤ 1}

Tactic:
apply withValUniformEquiv.toHomeomorph.isClosed_setOf_iff (q := fun x ↦ ‖x‖ ≤ 1)
      (Valued.isClopen_closedBall _ one_ne_zero)

Premises used: UniformEquiv.toHomeomorph, Homeomorph.isClosed_setOf_iff, one_ne_zero, Valued.isClopen_closedBall, Padic.withValUniformEquiv
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ IsClopen (X := ℚ_[p]) {y : ℚ_[p] | ‖y‖ ≤ 1}

Tactic:
simpa [Metric.closedBall] using IsUltrametricDist.isClopen_closedBall (0 : ℚ_[p]) one_ne_zero

Premises used: IsUltrametricDist.isClopen_closedBall, Metric.closedBall, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : WithVal (Rat.padicValuation p)
ih :
  norm (E := ℚ_[p]) (↑((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) a) : ℚ_[p]) ≤
      1 ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) a.ofVal : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
⊢ norm (E := ℚ_[p])
        ((withValUniformEquiv : (a : (Rat.padicValuation p).Completion) → ℚ_[p])
            (↑a : Completion (WithVal (Rat.padicValuation p))) :
          ℚ_[p]) ≤
      1 ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      ((Valued.v : (a : (Rat.padicValuation p).Completion) → WithZero (Multiplicative ℤ))
          (↑a : Completion (WithVal (Rat.padicValuation p))) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
rw [Valued.valuedCompletion_apply, ← WithVal.apply_ofVal, withValUniformEquiv_cast_apply]

Premises used: WithVal.apply_ofVal, Valued.valuedCompletion_apply, Padic.withValUniformEquiv_cast_apply
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : WithVal (Rat.padicValuation p)
⊢ norm (E := ℚ_[p]) (↑((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) a) : ℚ_[p]) ≤
      1 ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) a.ofVal : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
(norm_rat_le_one_iff_padicValuation_le_one p)

Premises used: Padic.norm_rat_le_one_iff_padicValuation_le_one
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : WithVal (Rat.padicValuation p)
⊢ norm (E := ℚ_[p]) (↑((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) a) : ℚ_[p]) ≤
      1 ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) a.ofVal : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
exact (norm_rat_le_one_iff_padicValuation_le_one p)

Premises used: Padic.norm_rat_le_one_iff_padicValuation_le_one
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (Rat.padicValuation p).Completion
hp :
  IsClosed (X := Completion (WithVal (Rat.padicValuation p)))
    {a : Completion (WithVal (Rat.padicValuation p)) |
      norm (E := ℚ_[p]) ((withValUniformEquiv : (a : (Rat.padicValuation p).Completion) → ℚ_[p]) a : ℚ_[p]) ≤ 1 ↔
        LE.le (α := WithZero (Multiplicative ℤ))
          ((Valued.v : (a : (Rat.padicValuation p).Completion) → WithZero (Multiplicative ℤ)) a :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ))}
ih :
  ∀ (a : WithVal (Rat.padicValuation p)),
    norm (E := ℚ_[p])
          ((withValUniformEquiv : (a : (Rat.padicValuation p).Completion) → ℚ_[p])
              (↑a : Completion (WithVal (Rat.padicValuation p))) :
            ℚ_[p]) ≤
        1 ↔
      LE.le (α := WithZero (Multiplicative ℤ))
        ((Valued.v : (a : (Rat.padicValuation p).Completion) → WithZero (Multiplicative ℤ))
            (↑a : Completion (WithVal (Rat.padicValuation p))) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
⊢ norm (E := ℚ_[p]) ((withValUniformEquiv : (a : (Rat.padicValuation p).Completion) → ℚ_[p]) x : ℚ_[p]) ≤ 1 ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      ((Valued.v : (a : (Rat.padicValuation p).Completion) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
induction x using UniformSpace.Completion.induction_on with
  | hp =>
    rw [Set.ext fun _ ↦ Iff.comm]
    simp_rw [← Valuation.restrict_le_one_iff Valued.v]
    apply withValUniformEquiv.toHomeomorph.isClosed_setOf_iff (q := fun x ↦ ‖x‖ ≤ 1)
      (Valued.isClopen_closedBall _ one_ne_zero)
    simpa [Metric.closedBall] using IsUltrametricDist.isClopen_closedBall (0 : ℚ_[p]) one_ne_zero
  | ih a =>
    rw [Valued.valuedCompletion_apply, ← WithVal.apply_ofVal, withValUniformEquiv_cast_apply]
    exact (norm_rat_le_one_iff_padicValuation_le_one p)

Premises used: Set.ext, WithVal.apply_ofVal, Valued.v, UniformEquiv.toHomeomorph, Homeomorph.isClosed_setOf_iff, Valued.valuedCompletion_apply, Padic.withValUniformEquiv_cast_apply, Valuation.restrict_le_one_iff, Iff.comm, Padic.norm_rat_le_one_iff_padicValuation_le_one, IsUltrametricDist.isClopen_closedBall, Metric.closedBall, one_ne_zero, OfNat.ofNat, Valued.isClopen_closedBall, Padic.withValUniformEquiv
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : ℤ√d
rw : HPow.hPow (β := ℕ) a.re 2 - d * HPow.hPow (β := ℕ) a.im 2 = 1 ↔ a.norm = 1
rw₁ : HPow.hPow (β := ℕ) a.re 2 - d * HPow.hPow (β := ℕ) a.im 2 = 1 ↔ a.re * a.re - d * a.im * a.im = 1
rw₂ : a.re * a.re - d * HPow.hPow (β := ℕ) a.im 2 = 1 ↔ a.re * a.re - d * a.im * a.im = 1
rw₃ : a.re * a.re - d * (a.im * a.im) = 1 ↔ a.re * a.re - d * a.im * a.im = 1
rw₄ rw₅ : a.re * a.re - d * a.im * a.im = 1 ↔ a.re * a.re - d * a.im * a.im = 1
⊢ HPow.hPow (β := ℕ) a.re 2 - d * HPow.hPow (β := ℕ) a.im 2 = 1 ↔
    Membership.mem (γ := Submonoid (ℤ√d)) (unitary (ℤ√d)) a

Tactic:
rw [← norm_eq_one_iff_mem_unitary, norm_def, sq, sq, ← mul_assoc]

Premises used: Zsqrtd.norm_def, mul_assoc, sq, Zsqrtd.norm_eq_one_iff_mem_unitary
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
⊢ HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2 = 1

Tactic:
is_pell_solution_iff_mem_unitary.mpr a.property

Premises used: Iff.mpr, Pell.is_pell_solution_iff_mem_unitary, Pell.Solution₁.x, Pell.Solution₁.y, Subtype.property
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
rw : HPow.hPow (β := ℕ) a.x 2 = HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2 + d * HPow.hPow (β := ℕ) a.y 2
⊢ HPow.hPow (β := ℕ) a.x 2 = 1 + d * HPow.hPow (β := ℕ) a.y 2

Tactic:
rw [← a.prop]

Premises used: Pell.Solution₁.prop
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
⊢ HPow.hPow (β := ℕ) a.x 2 = HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2 + d * HPow.hPow (β := ℕ) a.y 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
rw : d * HPow.hPow (β := ℕ) a.y 2 = HPow.hPow (β := ℕ) a.x 2 - (HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2)
⊢ d * HPow.hPow (β := ℕ) a.y 2 = HPow.hPow (β := ℕ) a.x 2 - 1

Tactic:
rw [← a.prop]

Premises used: Pell.Solution₁.prop
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
⊢ d * HPow.hPow (β := ℕ) a.y 2 = HPow.hPow (β := ℕ) a.x 2 - (HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
hx : a.x = b.x
hy : a.y = b.y
⊢ a = b

Tactic:
Subtype.ext <| Zsqrtd.ext hx hy

Premises used: Zsqrtd.ext, Pell.Solution₁, Subtype.ext
-- Module: Mathlib.NumberTheory.Pell
Goal:
d x y : ℤ
prop : HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1
⊢ (mk x y prop).x = x

Tactic:
rfl

Premises used: Pell.Solution₁.x, rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d x y : ℤ
prop : HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1
⊢ (mk x y prop).y = y

Tactic:
rfl

Premises used: Pell.Solution₁.y, rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d x y : ℤ
prop : HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1
⊢ (↑(mk x y prop) : ℤ√d) = { re := x, im := y }

Tactic:
Zsqrtd.ext (x_mk x y prop) (y_mk x y prop)

Premises used: Zsqrtd.ext, Pell.Solution₁.y_mk, Pell.Solution₁.x_mk
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
⊢ Solution₁.x (d := d) 1 = 1

Tactic:
rfl

Premises used: Pell.Solution₁.x, rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
⊢ Solution₁.y (d := d) 1 = 0

Tactic:
rfl

Premises used: Pell.Solution₁.y, rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
rw : (a * b).x = a.x * b.x + d * a.y * b.y
⊢ (a * b).x = a.x * b.x + d * (a.y * b.y)

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
⊢ (a * b).x = a.x * b.x + d * a.y * b.y

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
⊢ (a * b).y = a.x * b.y + a.y * b.x

Tactic:
rfl

Premises used: Pell.Solution₁.x, Pell.Solution₁.y, rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
⊢ a⁻¹.x = a.x

Tactic:
rfl

Premises used: Set.Mem, setOf, Pell.Solution₁.x, Pell.Solution₁, Int.neg, rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
⊢ a⁻¹.y = -a.y

Tactic:
rfl

Premises used: Pell.Solution₁.y, rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
⊢ (-a).x = -a.x

Tactic:
rfl

Premises used: Pell.Solution₁.x, rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
⊢ (-a).y = -a.y

Tactic:
rfl

Premises used: Pell.Solution₁.y, rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : d < 0
a : Solution₁ d
⊢ HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2 = 1

Tactic:
have h := a.prop
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2 = 1
contrapose! : ∀ (h : a.x ≠ 0 ∧ a.y ≠ 0), HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2 ≠ 1
⊢ a.x = 0 ∨ a.y = 0

Tactic:
contrapose! h
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : a.x ≠ 0 ∧ a.y ≠ 0
⊢ 0 < HPow.hPow (β := ℕ) a.x 2

Tactic:
have h1 := sq_pos_of_ne_zero h.1
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : a.x ≠ 0 ∧ a.y ≠ 0
h1 : 0 < HPow.hPow (β := ℕ) a.x 2
⊢ 0 < HPow.hPow (β := ℕ) a.y 2

Tactic:
have h2 := sq_pos_of_ne_zero h.2
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : a.x ≠ 0 ∧ a.y ≠ 0
h1 : 0 < HPow.hPow (β := ℕ) a.x 2
h2 : 0 < HPow.hPow (β := ℕ) a.y 2
nlinarith :
  HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2 = 1 →
    -1 + (HAdd.hAdd (α := ℤ) 0 1 - HPow.hPow (β := ℕ) a.x 2) + (HAdd.hAdd (α := ℤ) 0 1 - HPow.hPow (β := ℕ) a.y 2) +
          (HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2 - 1) +
        (0 - (0 - HPow.hPow (β := ℕ) a.y 2) * (d + 1 - 0)) =
      0
⊢ HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2 ≠ 1

Tactic:
nlinarith
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
⊢ 0 ≤ d * HPow.hPow (β := ℕ) a.y 2

Tactic:
have h : 0 ≤ d * a.y ^ 2 := mul_nonneg h₀ (sq_nonneg _)
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
h : 0 ≤ d * HPow.hPow (β := ℕ) a.y 2
⊢ LE.le (α := ℤ) 0 (-1)

Tactic:
rw [a.prop_y, hx, sq, zero_mul, zero_sub] at h

Premises used: MulZeroClass.zero_mul, Pell.Solution₁.prop_y, sq, zero_sub
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
h : LE.le (α := ℤ) 0 (-1)
⊢ False

Tactic:
not_le.mpr (neg_one_lt_zero : (-1 : ℤ) < 0) h

Premises used: not_le, Iff.mpr, neg_one_lt_zero
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
h : LE.le (α := ℤ) 0 (-1)
⊢ False

Tactic:
exact not_le.mpr (neg_one_lt_zero : (-1 : ℤ) < 0) h

Premises used: not_le, Iff.mpr, neg_one_lt_zero
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
hy : a.y = 0
⊢ HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2 = 1

Tactic:
have prop := a.prop
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
hy : a.y = 0
prop : HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2 = 1
⊢ HPow.hPow (β := ℕ) a.x 2 = 1

Tactic:
rw [hy, sq (0 : ℤ), zero_mul, mul_zero, sub_zero] at prop

Premises used: sub_zero, MulZeroClass.zero_mul, sq, MulZeroClass.mul_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
hy : a.y = 0
prop : HPow.hPow (β := ℕ) a.x 2 = 1
⊢ False

Tactic:
lt_irrefl _ (((one_lt_sq_iff₀ <| zero_le_one.trans ha.le).mpr ha).trans_eq prop)

Premises used: Iff.mpr, lt_irrefl, one_lt_sq_iff₀, LT.lt.le, LT.lt.trans_eq, zero_le_one, LE.le.trans
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
hy : a.y = 0
prop : HPow.hPow (β := ℕ) a.x 2 = 1
⊢ False

Tactic:
exact lt_irrefl _ (((one_lt_sq_iff₀ <| zero_le_one.trans ha.le).mpr ha).trans_eq prop)

Premises used: Iff.mpr, lt_irrefl, one_lt_sq_iff₀, LT.lt.le, LT.lt.trans_eq, zero_le_one, LE.le.trans
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ 0 < d

Tactic:
pos_of_mul_pos_left ?_ (sq_nonneg a.y)

Premises used: pos_of_mul_pos_left, Pell.Solution₁.y, sq_nonneg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
refine : 0 < d * HPow.hPow (β := ℕ) a.y 2
⊢ 0 < d

Tactic:
refine pos_of_mul_pos_left ?_ (sq_nonneg a.y)

Premises used: pos_of_mul_pos_left, Pell.Solution₁.y, sq_nonneg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
rw : 1 < HPow.hPow (β := ℕ) a.x 2
⊢ 0 < d * HPow.hPow (β := ℕ) a.y 2

Tactic:
rw [a.prop_y, sub_pos]

Premises used: sub_pos, Pell.Solution₁.prop_y
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ 1 < HPow.hPow (β := ℕ) a.x 2

Tactic:
one_lt_pow₀ ha two_ne_zero

Premises used: two_ne_zero, one_lt_pow₀
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ 1 < HPow.hPow (β := ℕ) a.x 2

Tactic:
exact one_lt_pow₀ ha two_ne_zero

Premises used: two_ne_zero, one_lt_pow₀
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2 = 1

Tactic:
have hp := a.prop
-- Module: Mathlib.NumberTheory.Pell
Goal:
b : ℤ
a : Solution₁ (b * b)
ha : 1 < a.x
hp : HPow.hPow (β := ℕ) a.x 2 - b * b * HPow.hPow (β := ℕ) a.y 2 = 1
⊢ a.x + b * a.y = 1 ∧ a.x - b * a.y = 1 ∨ a.x + b * a.y = -1 ∧ a.x - b * a.y = -1

Tactic:
simp_rw [← sq, ← mul_pow, sq_sub_sq, Int.mul_eq_one_iff_eq_one_or_neg_one] at hp

Premises used: sq, Int.mul_eq_one_iff_eq_one_or_neg_one, mul_pow, sq_sub_sq
-- Module: Mathlib.NumberTheory.Pell
Goal:
b : ℤ
a : Solution₁ (b * b)
ha : 1 < a.x
hp : a.x + b * a.y = 1 ∧ a.x - b * a.y = 1 ∨ a.x + b * a.y = -1 ∧ a.x - b * a.y = -1
⊢ False

Tactic:
lia
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
⊢ d * HPow.hPow (β := ℕ) a.y 2 = HPow.hPow (β := ℕ) a.x 2 - 1

Tactic:
have prop := a.prop_y
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
prop : d * HPow.hPow (β := ℕ) a.y 2 = HPow.hPow (β := ℕ) a.x 2 - 1
⊢ a.y = 0

Tactic:
rw [ha, one_pow, sub_self, mul_eq_zero, or_iff_right h₀, sq_eq_zero_iff] at prop

Premises used: one_pow, sub_self, mul_eq_zero, or_iff_right, sq_eq_zero_iff
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
prop : a.y = 0
⊢ a = 1

Tactic:
ext ha prop

Premises used: Pell.Solution₁.ext
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
prop : a.y = 0
⊢ a = 1

Tactic:
exact ext ha prop

Premises used: Pell.Solution₁.ext
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
H : a = 1 ∨ a = -1
h : a = 1
⊢ a.y = 0

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
H : a = 1 ∨ a = -1
h : a = -1
⊢ a.y = 0

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
refine : ∀ (H : a.y = 0), a = 1 ∨ a = -1
⊢ a = 1 ∨ a = -1 ↔ a.y = 0

Tactic:
refine ⟨fun H => H.elim (fun h => by simp [h]) fun h => by simp [h], fun H => ?_⟩
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
H : a.y = 0
⊢ HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2 = 1

Tactic:
have prop := a.prop
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
H : a.y = 0
prop : HPow.hPow (β := ℕ) a.x 2 - d * HPow.hPow (β := ℕ) a.y 2 = 1
⊢ a.x = 1 ∨ a.x = -1

Tactic:
rw [H, sq (0 : ℤ), mul_zero, mul_zero, sub_zero, sq_eq_one_iff] at prop

Premises used: sq_eq_one_iff, sub_zero, sq, MulZeroClass.mul_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
H : a.y = 0
prop : a.x = 1 ∨ a.x = -1
⊢ a = 1 ∨ a = -1

Tactic:
prop.imp (fun h => ext h H) fun h => ext h H

Premises used: Or.imp, Pell.Solution₁.ext
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
H : a.y = 0
prop : a.x = 1 ∨ a.x = -1
⊢ a = 1 ∨ a = -1

Tactic:
exact prop.imp (fun h => ext h H) fun h => ext h H

Premises used: Or.imp, Pell.Solution₁.ext
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
simp : 0 < a.x * b.x + d * (a.y * b.y)
⊢ 0 < (a * b).x

Tactic:
simp only [x_mul]

Premises used: Pell.Solution₁.x_mul
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ 0 < a.x * b.x + d * (a.y * b.y)

Tactic:
neg_lt_iff_pos_add'.mp (abs_lt.mp ?_).1

Premises used: neg_lt_iff_pos_add', And.left, Iff.mp, abs_lt
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
refine : |d * (a.y * b.y)| < a.x * b.x
⊢ 0 < a.x * b.x + d * (a.y * b.y)

Tactic:
refine neg_lt_iff_pos_add'.mp (abs_lt.mp ?_).1

Premises used: neg_lt_iff_pos_add', And.left, Iff.mp, abs_lt