awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : UniformSpace K
inst_3 : IsUniformAddGroup K
inst_4 : IsNonarchimedeanLocalField K
⊢ CompleteSpace K

Tactic:
letI : (Valued.v (R := K)).RankOne :=
  { hom' := IsRankLeOne.nonempty.some.emb (R := K).comp MonoidWithZeroHom.ValueGroup₀.embedding
    strictMono' := IsRankLeOne.nonempty.some.strictMono.comp
        MonoidWithZeroHom.ValueGroup₀.embedding_strictMono }
  open scoped Valued in
  have : ProperSpace K := .of_nontriviallyNormedField_of_weaklyLocallyCompactSpace K
  (properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField.mp
    inferInstance).1

Premises used: inferInstance, ProperSpace.of_nontriviallyNormedField_of_weaklyLocallyCompactSpace, Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField, And.left, Iff.mp
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : UniformSpace K
inst_3 : IsUniformAddGroup K
inst_4 : IsNonarchimedeanLocalField K
⊢ CompleteSpace.{u_1} ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))

Tactic:
letI : (Valued.v (R := K)).RankOne :=
  { hom' := IsRankLeOne.nonempty.some.emb (R := K).comp MonoidWithZeroHom.ValueGroup₀.embedding
    strictMono' := IsRankLeOne.nonempty.some.strictMono.comp
        MonoidWithZeroHom.ValueGroup₀.embedding_strictMono }
  (compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField.mp
    (inferInstanceAs (CompactSpace 𝒪[K]))).1

Premises used: Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, Set.Mem, Valuation.RankOne.mk, setOf, And.left, Iff.mp
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : UniformSpace K
inst_3 : IsUniformAddGroup K
inst_4 : IsNonarchimedeanLocalField K
f : ℕ → ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      f m ≡ f n [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) m)
          ⊤]
S : (n : ℕ) → Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)) :=
  fun (n : ℕ) ↦
    f n +ᵥ
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K])
n : ℕ
apply :
  f (n + 1) +ᵥ
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K]) ⊆
    S n
⊢ S (n + 1) ⊆ S n

Tactic:
apply (Set.vadd_set_subset_vadd_set_iff.mpr (Ideal.pow_le_pow_right n.le_succ)).trans

Premises used: Iff.mpr, HasSubset.Subset.trans, Set.vadd_set_subset_vadd_set_iff, Nat.le_succ, Ideal.pow_le_pow_right
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : UniformSpace K
inst_3 : IsUniformAddGroup K
inst_4 : IsNonarchimedeanLocalField K
f : ℕ → ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      f m ≡ f n [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) m)
          ⊤]
S : (n : ℕ) → Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)) :=
  fun (n : ℕ) ↦
    f n +ᵥ
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K])
n : ℕ
⊢ f (n + 1) +ᵥ
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K]) ⊆
    S n

Tactic:
simpa [S] using (hf n.le_succ).symm

Premises used: SModEq.symm, Nat.le_succ
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : UniformSpace K
inst_3 : IsUniformAddGroup K
inst_4 : IsNonarchimedeanLocalField K
f : ℕ → ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      f m ≡ f n [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) m)
          ⊤]
S : (n : ℕ) → Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)) :=
  fun (n : ℕ) ↦
    f n +ᵥ
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K])
⊢ ∀ (n : ℕ), S (n + 1) ⊆ S n

Tactic:
have hS n : S (n + 1) ⊆ S n := by
      apply (Set.vadd_set_subset_vadd_set_iff.mpr (Ideal.pow_le_pow_right n.le_succ)).trans
      simpa [S] using (hf n.le_succ).symm
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : UniformSpace K
inst_3 : IsUniformAddGroup K
inst_4 : IsNonarchimedeanLocalField K
f : ℕ → ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      f m ≡ f n [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) m)
          ⊤]
S : (n : ℕ) → Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)) :=
  fun (n : ℕ) ↦
    f n +ᵥ
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K])
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
⊢ ∀ (n : ℕ), IsClosed (S n)

Tactic:
have h n : IsClosed (S n) := (IsNoetherianRing.isClosed_ideal (𝓂[K] ^ n)).vadd (f n)
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : UniformSpace K
inst_3 : IsUniformAddGroup K
inst_4 : IsNonarchimedeanLocalField K
f : ℕ → ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      f m ≡ f n [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) m)
          ⊤]
S : (n : ℕ) → Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)) :=
  fun (n : ℕ) ↦
    f n +ᵥ
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K])
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
h : ∀ (n : ℕ), IsClosed (S n)
⊢ ∀ (i : ℕ), (S i).Nonempty

Tactic:
simp [S]
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : UniformSpace K
inst_3 : IsUniformAddGroup K
inst_4 : IsNonarchimedeanLocalField K
f : ℕ → ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      f m ≡ f n [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) m)
          ⊤]
S : (n : ℕ) → Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)) :=
  fun (n : ℕ) ↦
    f n +ᵥ
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K])
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
h : ∀ (n : ℕ), IsClosed (S n)
obtain :
  ∀ (L : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
    (hL : Membership.mem (γ := Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) (⋂ (i : ℕ), S i) L),
    ∃ (L : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))),
      ∀ (n : ℕ),
        f n ≡ L [SMOD
          HSMul.hSMul (β :=
            Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
              ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
              (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n)
            ⊤]
⊢ ∃ (L : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))),
    ∀ (n : ℕ),
      f n ≡ L [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n)
          ⊤]

Tactic:
obtain ⟨L, hL⟩ := (h 0).isCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed S hS
      (by simp [S]) h

Premises used: IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed, IsClosed.isCompact, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : UniformSpace K
inst_3 : IsUniformAddGroup K
inst_4 : IsNonarchimedeanLocalField K
f : ℕ → ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      f m ≡ f n [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) m)
          ⊤]
S : (n : ℕ) → Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)) :=
  fun (n : ℕ) ↦
    f n +ᵥ
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K])
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
h : ∀ (n : ℕ), IsClosed (S n)
L : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hL : Membership.mem (γ := Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) (⋂ (i : ℕ), S i) L
⊢ ∃ (L : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))),
    ∀ (n : ℕ),
      f n ≡ L [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n)
          ⊤]

Tactic:
⟨L, fun n ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : UniformSpace K
inst_3 : IsUniformAddGroup K
inst_4 : IsNonarchimedeanLocalField K
f : ℕ → ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      f m ≡ f n [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) m)
          ⊤]
S : (n : ℕ) → Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)) :=
  fun (n : ℕ) ↦
    f n +ᵥ
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K])
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
h : ∀ (n : ℕ), IsClosed (S n)
L : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hL : Membership.mem (γ := Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) (⋂ (i : ℕ), S i) L
refine :
  ∀ (n : ℕ),
    f n ≡ L [SMOD
      HSMul.hSMul (β :=
        Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
          ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
        (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n)
        ⊤]
⊢ ∃ (L : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))),
    ∀ (n : ℕ),
      f n ≡ L [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n)
          ⊤]

Tactic:
refine ⟨L, fun n ↦ ?_⟩
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : UniformSpace K
inst_3 : IsUniformAddGroup K
inst_4 : IsNonarchimedeanLocalField K
f : ℕ → ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      f m ≡ f n [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) m)
          ⊤]
S : (n : ℕ) → Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)) :=
  fun (n : ℕ) ↦
    f n +ᵥ
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K])
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
h : ∀ (n : ℕ), IsClosed (S n)
L : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hL : Membership.mem (γ := Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) (⋂ (i : ℕ), S i) L
n : ℕ
obtain :
  ∀ (y : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
    (hy :
      y ∈
        (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
              (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
          Set ↥𝒪[K]))
    (hL :
      Membership.mem (γ := Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) (⋂ (i : ℕ), S i)
        ((fun (x : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) ↦ f n +ᵥ x) y)),
    f n ≡ (fun (x : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) ↦ f n +ᵥ x) y [SMOD
      HSMul.hSMul (β :=
        Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
          ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
        (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n)
        ⊤]
⊢ f n ≡ L [SMOD
    HSMul.hSMul (β :=
      Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
        ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
      (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
        (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n)
      ⊤]

Tactic:
obtain ⟨y, hy, rfl⟩ := Set.mem_iInter.mp hL n

Premises used: Set.mem_iInter, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.LocalField.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : ValuativeRel K
inst_2 : UniformSpace K
inst_3 : IsUniformAddGroup K
inst_4 : IsNonarchimedeanLocalField K
f : ℕ → ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hf :
  ∀ {m n : ℕ},
    m ≤ n →
      f m ≡ f n [SMOD
        HSMul.hSMul (β :=
          Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
            ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) m)
          ⊤]
S : (n : ℕ) → Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)) :=
  fun (n : ℕ) ↦
    f n +ᵥ
      (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
            (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
        Set ↥𝒪[K])
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
h : ∀ (n : ℕ), IsClosed (S n)
n : ℕ
y : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
hy :
  y ∈
    (↑(HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
          (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n) :
      Set ↥𝒪[K])
hL :
  Membership.mem (γ := Set ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) (⋂ (i : ℕ), S i)
    ((fun (x : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) ↦ f n +ᵥ x) y)
⊢ f n ≡ (fun (x : ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) ↦ f n +ᵥ x) y [SMOD
    HSMul.hSMul (β :=
      Submodule ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))
        ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
      (HPow.hPow (α := Ideal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K)))
        (IsLocalRing.maximalIdeal ↥(Valuation.integer (Γ₀ := ValueGroupWithZero K) (valuation K))) n)
      ⊤]

Tactic:
simpa [SModEq.sub_mem] using hy

Premises used: SModEq.sub_mem
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
m n : ℕ
h : m < n
h₁ : LT.lt (α := ℕ) 1 2
⊢ HPow.hPow (α := ℕ) 2 m < HPow.hPow (α := ℕ) 2 n

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
m n : ℕ
h : m < n
⊢ LT.lt (α := ℕ) 1 2

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p q : ℕ
⊢ mersenne p < mersenne q ↔ p < q

Tactic:
strictMono_mersenne.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, strictMono_mersenne
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p q : ℕ
⊢ mersenne p ≤ mersenne q ↔ p ≤ q

Tactic:
strictMono_mersenne.le_iff_le

Premises used: strictMono_mersenne, StrictMono.le_iff_le
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
⊢ mersenne 0 = 0

Tactic:
rfl

Premises used: mersenne, rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
⊢ Odd (mersenne 0) ↔ Ne (α := ℕ) 0 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
⊢ Odd (mersenne (p + 1)) ↔ p + 1 ≠ 0

Tactic:
simpa using Nat.Even.sub_odd (one_le_pow₀ one_le_two)
      (even_two.pow_of_ne_zero p.succ_ne_zero) odd_one

Premises used: Even.pow_of_ne_zero, one_le_pow₀, Nat.Even.sub_odd, Nat.succ_ne_zero, odd_one
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
⊢ 0 < mersenne p ↔ 0 < p

Tactic:
mersenne_lt_mersenne (p := 0)

Premises used: mersenne, mersenne_lt_mersenne
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
n : ℕ
⊢ 1 ≤ HPow.hPow (α := ℕ) 2 n

Tactic:
have := Nat.one_le_pow n 2 two_pos
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
n : ℕ
this : 1 ≤ HPow.hPow (α := ℕ) 2 n
⊢ HPow.hPow (α := ℕ) 2 (n + 1) - 1 = 2 * (HPow.hPow (α := ℕ) 2 n - 1) + 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
h : Prime (mersenne p)
apply : p ≠ 1
⊢ Prime p

Tactic:
apply Nat.prime_of_pow_sub_one_prime _ h |>.2

Premises used: And.right, Nat.prime_of_pow_sub_one_prime
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
h : Prime (mersenne 1)
⊢ False

Tactic:
apply Nat.not_prime_one h

Premises used: Nat.not_prime_one
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
p : ℕ
⊢ 1 < mersenne p ↔ 1 < p

Tactic:
mersenne_lt_mersenne (p := 1)

Premises used: mersenne, mersenne_lt_mersenne
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k : ℕ
rw : 1 ≤ HPow.hPow (α := ℕ) 2 k
⊢ mersenne k + 1 = HPow.hPow (α := ℕ) 2 k

Tactic:
rw [mersenne, tsub_add_cancel_of_le]

Premises used: tsub_add_cancel_of_le, mersenne
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k : ℕ
⊢ LE.le (α := ℕ) 1 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k : ℕ
⊢ 1 ≤ HPow.hPow (α := ℕ) 2 k

Tactic:
exact one_le_pow₀ (by simp)

Premises used: one_le_pow₀
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
n : ℕ
⊢ mersenne 2 % 4 = 3

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
n n_1 : ℕ
hmn : 2 ≤ n_1
h : mersenne n_1 % 4 = 3
succ : (2 * mersenne n_1 + 1) % 4 = 3
⊢ mersenne (n_1 + 1) % 4 = 3

Tactic:
rw [mersenne_succ]

Premises used: mersenne_succ
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
n n_1 : ℕ
hmn : 2 ≤ n_1
h : mersenne n_1 % 4 = 3
⊢ (2 * mersenne n_1 + 1) % 4 = 3

Tactic:
lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
n : ℕ
h : 2 ≤ n
base : mersenne 2 % 4 = 3
succ : ∀ (n : ℕ), 2 ≤ n → mersenne n % 4 = 3 → mersenne (n + 1) % 4 = 3
⊢ mersenne n % 4 = 3

Tactic:
induction n, h using Nat.le_induction with
  | base => rfl
  | succ _ _ _ => rw [mersenne_succ]; lia

Premises used: mersenne_succ
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
n : ℕ
odd : Odd n
h : 3 ≤ n
obtain : ∀ (k : ℕ) (h : 3 ≤ 2 * k + 1), mersenne (2 * k + 1) % 3 = 1
⊢ mersenne n % 3 = 1

Tactic:
obtain ⟨k, rfl⟩ := odd

Premises used: rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k : ℕ
h : 3 ≤ 2 * k + 1
⊢ 1 ≤ k

Tactic:
lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k : ℕ
h : 3 ≤ 2 * k + 1
⊢ 1 ≤ k

Tactic:
replace h : 1 ≤ k := by lia
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k : ℕ
⊢ mersenne (HMul.hMul (α := ℕ) 2 1 + 1) % 3 = 1

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LucasLehmer
Goal:
k j : ℕ
hmn : 1 ≤ j
h : mersenne (2 * j + 1) % 3 = 1
⊢ 2 * (j + 1) = 2 * j + 1 + 1

Tactic:
lia