awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : I = O ∙ x
⊢ ∃ (x : Γ₀),
    IsGreatest
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O))
      x
have mp : Membership.mem (γ := Set Γ₀)
  (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
  (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) x)
Tactic: refine ⟨(v ∘ algebraMap O F) x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : I = O ∙ x
mp :
  Membership.mem (γ := Set Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) x)
⊢ ∃ (x : Γ₀),
    IsGreatest
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O))
      x
have mp₁ : Membership.mem (γ := Set Γ₀)
  (upperBounds
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
      (↑I : Set O)))
  (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) x)
Tactic: refine ⟨(v ∘ algebraMap O F) x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : I = O ∙ x
⊢ Membership.mem (γ := Set Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) x)
have mp : x ∈ (↑I : Set O)
Tactic: refine Set.mem_image_of_mem _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (hypothesis)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : I = O ∙ x
y : Γ₀
hy :
  Membership.mem (γ := Set Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    y
⊢ y ≤ Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) x
have hy₁ : ∃ (x_1 : O), x ∣ x_1 ∧ (v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x_1 : F) = y
Tactic: simp only [Function.comp_apply, hx, Ideal.submodule_span_eq, Set.mem_image,
        SetLike.mem_coe, Ideal.mem_span_singleton] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx : I = O ∙ x
y : Γ₀
hy : ∃ (x_1 : O), x ∣ x_1 ∧ (v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x_1 : F) = y
⊢ y ≤ Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) x
have mp : ∀ (y : O) (hy : x ∣ y),
  LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) x : Γ₀)
Tactic: obtain ⟨y, hy, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
x : Γ₀
hx :
  IsGreatest
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    x
⊢ Submodule.IsPrincipal I
have mpr : ∀ (a : O) (ha : a ∈ I)
  (hx :
    IsGreatest.{v} (α := Γ₀)
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O))
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)),
  Submodule.IsPrincipal I
Tactic: obtain ⟨a, ha, rfl⟩ : ∃ a ∈ I, (v ∘ algebraMap O F) a = x := by simpa using hx.left
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx :
  IsGreatest.{v} (α := Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)
⊢ Submodule.IsPrincipal I
have mpr : I = O ∙ a
Tactic: refine ⟨a, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx :
  IsGreatest.{v} (α := Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)
⊢ I = O ∙ a
have mpr : ∀ (b : O), b ∈ I ↔ Membership.mem (γ := Ideal O) (O ∙ a) b
Tactic: ext b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx :
  IsGreatest.{v} (α := Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)
b : O
⊢ b ∈ I ↔ Membership.mem (γ := Ideal O) (O ∙ a) b
have mpr : b ∈ I ↔ a ∣ b
Tactic: simp only [Ideal.submodule_span_eq, Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
⊢ Submodule.IsPrincipal I ↔
    ∃ (x : O),
      (↑I : Set O) =
        {y : O |
          LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
            ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
have rw : (∃ (x : Γ₀),
    IsGreatest
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O))
      x) ↔
  ∃ (x : O),
    (↑I : Set O) =
      {y : O |
        LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
          ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
Tactic: rw [isPrincipal_iff_exists_isGreatest hv]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
⊢ (∃ (x : Γ₀),
      IsGreatest
        (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
          (↑I : Set O))
        x) ↔
    ∃ (x : O),
      (↑I : Set O) =
        {y : O |
          LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
            ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
have mp : (∃ (x : Γ₀),
    IsGreatest
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O))
      x) →
  ∃ (x : O),
    (↑I : Set O) =
      {y : O |
        LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
          ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
mp :
  (∃ (x : Γ₀),
      IsGreatest
        (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
          (↑I : Set O))
        x) →
    ∃ (x : O),
      (↑I : Set O) =
        {y : O |
          LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
            ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
⊢ (∃ (x : Γ₀),
      IsGreatest
        (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
          (↑I : Set O))
        x) ↔
    ∃ (x : O),
      (↑I : Set O) =
        {y : O |
          LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
            ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
have mpr : (∃ (x : O),
    (↑I : Set O) =
      {y : O |
        LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
          ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}) →
  ∃ (x : Γ₀),
    IsGreatest
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O))
      x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
x : Γ₀
hx :
  IsGreatest
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    x
⊢ ∃ (x : O),
    (↑I : Set O) =
      {y : O |
        LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
          ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
have mp : ∀ (a : O) (ha : a ∈ I)
  (hx :
    IsGreatest.{v} (α := Γ₀)
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O))
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)),
  ∃ (x : O),
    (↑I : Set O) =
      {y : O |
        LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
          ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
Tactic: obtain ⟨a, ha, rfl⟩ : ∃ a ∈ I, (v ∘ algebraMap O F) a = x := by simpa using hx.left
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx :
  IsGreatest.{v} (α := Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)
⊢ ∃ (x : O),
    (↑I : Set O) =
      {y : O |
        LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
          ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
have mp : (↑I : Set O) =
  {y : O |
    LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) a : F) : Γ₀)}
Tactic: refine ⟨a, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx :
  IsGreatest.{v} (α := Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)
⊢ (↑I : Set O) =
    {y : O |
      LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) a : F) : Γ₀)}
have mp : ∀ (b : O),
  b ∈ (↑I : Set O) ↔
    Membership.mem (γ := Set O)
      {y : O |
        LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
          ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) a : F) : Γ₀)}
      b
Tactic: ext b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx :
  IsGreatest.{v} (α := Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)
b : O
⊢ b ∈ (↑I : Set O) ↔
    Membership.mem (γ := Set O)
      {y : O |
        LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
          ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) a : F) : Γ₀)}
      b
have mp : b ∈ I ↔
  LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) b : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) a : F) : Γ₀)
Tactic: simp only [SetLike.mem_coe, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx :
  IsGreatest.{v} (α := Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)
b : O
⊢ b ∈ I ↔
    LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) b : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) a : F) : Γ₀)
have mp : b ∈ I →
  LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) b : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) a : F) : Γ₀)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx :
  IsGreatest.{v} (α := Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)
b : O
mp :
  b ∈ I →
    LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) b : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) a : F) : Γ₀)
⊢ b ∈ I ↔
    LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) b : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) a : F) : Γ₀)
have mp₁ : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) b : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) a : F) : Γ₀) →
  b ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (hypothesis)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
a : O
ha : a ∈ I
hx :
  IsGreatest.{v} (α := Γ₀)
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) '' (↑I : Set O))
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a)
b : O
h :
  LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) b : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) a : F) : Γ₀)
⊢ b ∈ I
have h₁ : a ∣ b
Tactic: rw [le_iff_dvd hv] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx :
  (↑I : Set O) =
    {y : O |
      LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
⊢ ∃ (x : Γ₀),
    IsGreatest
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O))
      x
have mpr : x ∈ (↑I : Set O)
Tactic: refine ⟨v (algebraMap O F x), Set.mem_image_of_mem _ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
x : O
hx :
  (↑I : Set O) =
    {y : O |
      LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
mpr : x ∈ (↑I : Set O)
⊢ ∃ (x : Γ₀),
    IsGreatest
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O))
      x
have mpr₁ : Membership.mem.{v, v} (α := Γ₀) (γ := Set Γ₀)
  (upperBounds
    (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
      (↑I : Set O)))
  ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
Tactic: refine ⟨v (algebraMap O F x), Set.mem_image_of_mem _ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
inst_4 : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered.{v} (↑(range.{v, u + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type v)
c x : O
⊢ Membership.mem (γ := Set O)
      (preimage.{w, v} (β := Γ₀)
        (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)) (Iio 1))
      x →
    Membership.mem (γ := Set O)
      (preimage.{w, v} (β := Γ₀)
        (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)) (Iio 1))
      (c • x)
have simp : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (1 : Γ₀) →
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) c : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) <
    1
Tactic: simp only [mem_preimage, Function.comp_apply, mem_Iio, smul_eq_mul, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
inst_4 : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered.{v} (↑(range.{v, u + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type v)
I : Ideal O :=
  {
    carrier :=
      preimage.{w, v} (β := Γ₀)
        (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)) (Iio 1),
    add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ False
have obtain : ∀ (x : O) (hx₁ : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (1 : Γ₀))
  (hx :
    Membership.mem.{v, v} (α := Γ₀) (γ := Set Γ₀)
      (upperBounds
        (Iio 1 ∩
          range.{v, w + 1} (ι := O)
            (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))))
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)),
  False
Tactic: obtain ⟨x, hx₁, hx⟩ :
    ∃ x, v (algebraMap O F x) < 1 ∧
      v (algebraMap O F x) ∈ upperBounds (Iio 1 ∩ range (v ∘ algebraMap O F)) := by
    simpa [I, IsGreatest, hv.isPrincipal_iff_exists_isGreatest, ← image_preimage_eq_inter_range]
      using IsPrincipalIdealRing.principal I
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
inst_4 : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered.{v} (↑(range.{v, u + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type v)
I : Ideal O :=
  {
    carrier :=
      preimage.{w, v} (β := Γ₀)
        (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)) (Iio 1),
    add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
x : O
hx₁ : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (1 : Γ₀)
hx :
  Membership.mem.{v, v} (α := Γ₀) (γ := Set Γ₀)
    (upperBounds
      (Iio 1 ∩
        range.{v, w + 1} (ι := O)
          (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))))
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
⊢ False
have obtain : ∀ (y : F)
  (hy :
    LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) ((v : (a : F) → Γ₀) y : Γ₀))
  (hy₁ : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) y : Γ₀) (1 : Γ₀)), False
Tactic: obtain ⟨y, hy, hy₁⟩ : ∃ y, v (algebraMap O F x) < v y ∧ v y < 1 := by
    simpa only [Subtype.exists, Subtype.mk_lt_mk, exists_range_iff, exists_prop]
      using H.dense ⟨v (algebraMap O F x), mem_range_self _⟩ ⟨1, 1, v.map_one⟩ hx₁