awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Integers
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
inst_4 : Subsingleton.{v + 1} (↥(MonoidHom.mrange v))ˣ
refine : ∀ (x : F), LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Function.Bijective.{w + 1, u + 1} (α := O) (β := F) (⇑(algebraMap O F) : (a : O) → F)

Tactic:
refine ⟨hv.hom_inj, fun x ↦ hv.exists_of_le_one ?_⟩
-- Module: Mathlib.RingTheory.Valuation.Integers
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
inst_4 : Subsingleton.{v + 1} (↥(MonoidHom.mrange v))ˣ
x : F
inl : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) 0 : Γ₀) (1 : Γ₀)
inr : ∀ (hx : x ≠ 0), LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Valuation.Integers
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
inst_4 : Subsingleton.{v + 1} (↥(MonoidHom.mrange v))ˣ
⊢ LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) 0 : Γ₀) (1 : Γ₀)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Integers
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
inst_4 : Subsingleton.{v + 1} (↥(MonoidHom.mrange v))ˣ
x : F
hx : x ≠ 0
⊢ LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
(congr_arg Units.val (Subsingleton.elim (α := (MonoidHom.mrange v)ˣ)
      ((isUnit_iff_ne_zero.mpr hx).unit.map v.toMonoidHom.mrangeRestrict) 1)).le

Premises used: Iff.mpr, Units.val, Eq.le, isUnit_iff_ne_zero, congr_arg, Valuation.toMonoidWithZeroHom, MonoidWithZeroHom.toMonoidHom, MonoidHom.mrangeRestrict, IsUnit.unit, Subsingleton.elim, OfNat.ofNat, DFunLike.coe, Units.map
-- Module: Mathlib.RingTheory.Valuation.Integers
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
inst_4 : Subsingleton.{v + 1} (↥(MonoidHom.mrange v))ˣ
x : F
hx : x ≠ 0
⊢ LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
exact (congr_arg Units.val (Subsingleton.elim (α := (MonoidHom.mrange v)ˣ)
      ((isUnit_iff_ne_zero.mpr hx).unit.map v.toMonoidHom.mrangeRestrict) 1)).le

Premises used: Iff.mpr, Units.val, Eq.le, isUnit_iff_ne_zero, congr_arg, Valuation.toMonoidWithZeroHom, MonoidWithZeroHom.toMonoidHom, MonoidHom.mrangeRestrict, IsUnit.unit, Subsingleton.elim, OfNat.ofNat, DFunLike.coe, Units.map
-- Module: Mathlib.RingTheory.Valuation.Integers
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 :
  Submodule.IsPrincipal I →
    ∃ (x : Γ₀),
      IsGreatest
        (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
          (↑I : Set O))
        x
mpr :
  (∃ (x : Γ₀),
      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
⊢ Submodule.IsPrincipal I ↔
    ∃ (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
-- Module: Mathlib.RingTheory.Valuation.Integers
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

Tactic:
⟨(v ∘ algebraMap O F) x, ?_, ?_⟩

Premises used: Algebra.algebraMap, Function.comp, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Integers
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)
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)
⊢ ∃ (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:
refine ⟨(v ∘ algebraMap O F) x, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Valuation.Integers
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)

Tactic:
Set.mem_image_of_mem _ ?_

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.RingTheory.Valuation.Integers
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 : x ∈ (↑I : Set O)
⊢ 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 Set.mem_image_of_mem _ ?_

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.RingTheory.Valuation.Integers
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 ∈ (↑I : Set O)

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.Valuation.Integers
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
⊢ ∃ (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

Premises used: Ideal.submodule_span_eq, Set.mem_image, SetLike.mem_coe, Function.comp_apply, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Valuation.Integers
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
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 : Γ₀)
⊢ y ≤ 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

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Integers
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 : 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:
le_of_dvd hv hy

Premises used: Valuation.Integers.le_of_dvd
-- Module: Mathlib.RingTheory.Valuation.Integers
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 : 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:
exact le_of_dvd hv hy

Premises used: Valuation.Integers.le_of_dvd
-- Module: Mathlib.RingTheory.Valuation.Integers
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
⊢ ∃ a ∈ I, Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) a = x

Tactic:
simpa using hx.left

Premises used: And.left
-- Module: Mathlib.RingTheory.Valuation.Integers
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
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
⊢ Submodule.IsPrincipal I

Tactic:
obtain ⟨a, ha, rfl⟩ : ∃ a ∈ I, (v ∘ algebraMap O F) a = x := by simpa using hx.left

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Integers
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

Tactic:
⟨a, ?_⟩

Premises used: Submodule.IsPrincipal.mk, Exists.intro
-- Module: Mathlib.RingTheory.Valuation.Integers
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)
mpr : I = O ∙ a
⊢ Submodule.IsPrincipal I

Tactic:
refine ⟨a, ?_⟩
-- Module: Mathlib.RingTheory.Valuation.Integers
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)
mpr : ∀ (b : O), b ∈ I ↔ Membership.mem (γ := Ideal O) (O ∙ a) b
⊢ I = O ∙ a

Tactic:
ext b
-- Module: Mathlib.RingTheory.Valuation.Integers
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
mpr : b ∈ I ↔ a ∣ b
⊢ b ∈ I ↔ Membership.mem (γ := Ideal O) (O ∙ a) b

Tactic:
simp only [Ideal.submodule_span_eq, Ideal.mem_span_singleton]

Premises used: Ideal.submodule_span_eq, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Valuation.Integers
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 ↔ a ∣ b

Tactic:
⟨fun hb ↦ dvd_of_le hv (hx.2 <| mem_image_of_mem _ hb), fun hb ↦ I.mem_of_dvd hb ha⟩

Premises used: Algebra.algebraMap, Valuation.Integers.dvd_of_le, Function.comp, Ideal.mem_of_dvd, And.right, Set.mem_image_of_mem, Iff.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Integers
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 ↔ a ∣ b

Tactic:
exact ⟨fun hb ↦ dvd_of_le hv (hx.2 <| mem_image_of_mem _ hb), fun hb ↦ I.mem_of_dvd hb ha⟩
-- Module: Mathlib.RingTheory.Valuation.Integers
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
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) : Γ₀)}
⊢ 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) : Γ₀)}

Tactic:
rw [isPrincipal_iff_exists_isGreatest hv]

Premises used: Valuation.Integers.isPrincipal_iff_exists_isGreatest
-- Module: Mathlib.RingTheory.Valuation.Integers
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) : Γ₀)}
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
⊢ (∃ (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
-- Module: Mathlib.RingTheory.Valuation.Integers
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
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) : Γ₀)}
⊢ ∃ (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

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Integers
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) : Γ₀)}

Tactic:
⟨a, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Valuation.Integers
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)
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) : Γ₀)}
⊢ ∃ (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:
refine ⟨a, ?_⟩
-- Module: Mathlib.RingTheory.Valuation.Integers
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)
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
⊢ (↑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:
ext b
-- Module: Mathlib.RingTheory.Valuation.Integers
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 : 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:
simp only [SetLike.mem_coe, mem_setOf_eq]

Premises used: Set.mem_setOf_eq, SetLike.mem_coe
-- Module: Mathlib.RingTheory.Valuation.Integers
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) : Γ₀)
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
⊢ 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
-- Module: Mathlib.RingTheory.Valuation.Integers
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 : 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:
hx.right (Set.mem_image_of_mem _ h)

Premises used: And.right, Set.mem_image_of_mem