awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
rw : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R])ᶜ Set.univ ↔ FormallyUnramified R A
rw₁ : Eq (α := Set (PrimeSpectrum A)) Set.univᶜ (Module.support A Ω[A⁄R]) ↔ FormallyUnramified R A
rw₂ : Eq (α := Set (PrimeSpectrum A)) ∅ (Module.support A Ω[A⁄R]) ↔ FormallyUnramified R A
⊢ Eq (α := Set (PrimeSpectrum A)) (unramifiedLocus R A) Set.univ ↔ FormallyUnramified R A
have rw₃ : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R]) ∅ ↔ FormallyUnramified R A
Tactic: rw [unramifiedLocus_eq_compl_support, compl_eq_comm, Set.compl_univ, eq_comm,
    Module.support_eq_empty_iff, Algebra.formallyUnramified_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
rw : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R])ᶜ Set.univ ↔ FormallyUnramified R A
rw₁ : Eq (α := Set (PrimeSpectrum A)) Set.univᶜ (Module.support A Ω[A⁄R]) ↔ FormallyUnramified R A
rw₂ : Eq (α := Set (PrimeSpectrum A)) ∅ (Module.support A Ω[A⁄R]) ↔ FormallyUnramified R A
rw₃ : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R]) ∅ ↔ FormallyUnramified R A
⊢ Eq (α := Set (PrimeSpectrum A)) (unramifiedLocus R A) Set.univ ↔ FormallyUnramified R A
have rw₄ : Subsingleton.{u_2 + 1} Ω[A⁄R] ↔ FormallyUnramified R A
Tactic: rw [unramifiedLocus_eq_compl_support, compl_eq_comm, Set.compl_univ, eq_comm,
    Module.support_eq_empty_iff, Algebra.formallyUnramified_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
rw : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R])ᶜ Set.univ ↔ FormallyUnramified R A
rw₁ : Eq (α := Set (PrimeSpectrum A)) Set.univᶜ (Module.support A Ω[A⁄R]) ↔ FormallyUnramified R A
rw₂ : Eq (α := Set (PrimeSpectrum A)) ∅ (Module.support A Ω[A⁄R]) ↔ FormallyUnramified R A
rw₃ : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R]) ∅ ↔ FormallyUnramified R A
rw₄ : Subsingleton.{u_2 + 1} Ω[A⁄R] ↔ FormallyUnramified R A
⊢ Eq (α := Set (PrimeSpectrum A)) (unramifiedLocus R A) Set.univ ↔ FormallyUnramified R A
have rw₅ : Subsingleton.{u_2 + 1} Ω[A⁄R] ↔ Subsingleton.{u_2 + 1} Ω[A⁄R]
Tactic: rw [unramifiedLocus_eq_compl_support, compl_eq_comm, Set.compl_univ, eq_comm,
    Module.support_eq_empty_iff, Algebra.formallyUnramified_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
⊢ IsOpen (X := PrimeSpectrum A) (unramifiedLocus R A)
have rw : IsOpen (X := PrimeSpectrum A) (PrimeSpectrum.zeroLocus (↑(Module.annihilator A Ω[A⁄R]) : Set A))ᶜ
Tactic: rw [unramifiedLocus_eq_compl_support, Module.support_eq_zeroLocus]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : Ideal A
inst_4 : p.IsPrime
inst_5 : IsUnramifiedAt R p
⊢ ∃ f ∉ p, FormallyUnramified.{u_2, u_1} R (Localization.Away f)
have obtain : ∀ (r : A)
  (hpr : { asIdeal := p, isPrime := inst_4 : PrimeSpectrum A } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum A)))
  (hr : (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum A)) ⊆ unramifiedLocus R A),
  ∃ f ∉ p, FormallyUnramified.{u_2, u_1} R (Localization.Away f)
Tactic: obtain ⟨_, ⟨_, ⟨r, rfl⟩, rfl⟩, hpr, hr⟩ :=
    PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open
      (show ⟨p, ‹_›⟩ ∈ unramifiedLocus R A from ‹_›) isOpen_unramifiedLocus
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FiniteType R A
p : Ideal A
inst_4 : p.IsPrime
inst_5 : IsUnramifiedAt R p
⊢ ∃ f ∉ p, Unramified.{u_1, u_2} R (Localization.Away f)
have obtain : ∀ (f : A) (hfp : f ∉ p) (H : FormallyUnramified.{u_2, u_1} R (Localization.Away f)),
  ∃ f ∉ p, Unramified.{u_1, u_2} R (Localization.Away f)
Tactic: obtain ⟨f, hfp, H⟩ := exists_formallyUnramified_of_isUnramifiedAt (R := R) p
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (goal)
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v_1 : Valuation F Γ₀
v : F →*₀ Γ₀
⊢ ∀ ⦃a : ↥(MonoidHom.mrange v)⦄ (ha : 0 < a) ⦃b c : ↥(MonoidHom.mrange v)⦄ (hbc : b < c), a * b < a * c
have simp : ∀ (a : F) (ha : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : F) → Γ₀) a : Γ₀)) (a_1 a_2 : F)
  (hbc : LT.lt.{u_2} (α := Γ₀) ((v : (a : F) → Γ₀) a_1 : Γ₀) ((v : (a : F) → Γ₀) a_2 : Γ₀)),
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) a : Γ₀) ((v : (a : F) → Γ₀) a_1 : Γ₀) <
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) a : Γ₀) ((v : (a : F) → Γ₀) a_2 : Γ₀)
Tactic: simp only [← Subtype.coe_lt_coe, val_mrange_zero, Submonoid.coe_mul, Subtype.forall,
      MonoidHom.mem_mrange, forall_exists_index, forall_apply_eq_imp_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (goal)
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
hv : v.Integers O
⊢ WfDvdMonoid O ↔
    WellFounded.{u_3 + 1} (α := O)
      ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
        Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))
have refine_1 : WfDvdMonoid O →
  ∀ (a b : O),
    ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
          Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))
        a b →
      DvdNotUnit a b
Tactic: refine ⟨fun _ ↦ wellFounded_dvdNotUnit.mono ?_, fun h ↦ ⟨h.mono ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (goal)
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
hv : v.Integers O
refine_1 :
  WfDvdMonoid O →
    ∀ (a b : O),
      ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
            Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))
          a b →
        DvdNotUnit a b
⊢ WfDvdMonoid O ↔
    WellFounded.{u_3 + 1} (α := O)
      ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
        Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))
have refine_2 : ∀
  (h :
    WellFounded.{u_3 + 1} (α := O)
      ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
        Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
  (a b : O),
  DvdNotUnit a b →
    ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
        Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F))
      a b
Tactic: refine ⟨fun _ ↦ wellFounded_dvdNotUnit.mono ?_, fun h ↦ ⟨h.mono ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (goal)
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
⊢ WellFounded.{u_3 + 1} (α := O)
      ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
        Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)) ↔
    Nonempty.{max 1 (u_2 + 1)} (↥(MonoidHom.mrange v) ≃*o WithZero (Multiplicative ℤ))
have rw : (Set.WellFoundedOn
    (Set.range.{u_2, u_3 + 1} (ι := O)
      (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
    fun (x1 x2 : Γ₀) ↦ x1 > x2) ↔
  Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2
Tactic: rw [← LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero
    one_ne_zero, ← Set.wellFoundedOn_range]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (goal)
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
⊢ (Set.WellFoundedOn
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      fun (x1 x2 : Γ₀) ↦ x1 > x2) ↔
    Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2
have refine_1 : ∀
  (h :
    Set.WellFoundedOn
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      fun (x1 x2 : Γ₀) ↦ x1 > x2),
  Set.MapsTo.{u_2, u_2} (α := ↥(MonoidHom.mrange v))
    (Subtype.val (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x))
    {x : ↥(MonoidHom.mrange v) | x ≤ 1}
    (Set.range.{u_2, u_3 + 1} (ι := O)
      (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
Tactic: refine ⟨fun h ↦ (h.mapsTo Subtype.val ?_).mono' (by simp), fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (goal)
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
refine_1 :
  ∀
    (h :
      Set.WellFoundedOn
        (Set.range.{u_2, u_3 + 1} (ι := O)
          (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
        fun (x1 x2 : Γ₀) ↦ x1 > x2),
    Set.MapsTo.{u_2, u_2} (α := ↥(MonoidHom.mrange v))
      (Subtype.val (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x))
      {x : ↥(MonoidHom.mrange v) | x ≤ 1}
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
⊢ (Set.WellFoundedOn
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      fun (x1 x2 : Γ₀) ↦ x1 > x2) ↔
    Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2
have refine_2 : (h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2) →
  Γ₀ → ↥(MonoidHom.mrange v)
Tactic: refine ⟨fun h ↦ (h.mapsTo Subtype.val ?_).mono' (by simp), fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (goal)
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
refine_1 :
  ∀
    (h :
      Set.WellFoundedOn
        (Set.range.{u_2, u_3 + 1} (ι := O)
          (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
        fun (x1 x2 : Γ₀) ↦ x1 > x2),
    Set.MapsTo.{u_2, u_2} (α := ↥(MonoidHom.mrange v))
      (Subtype.val (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x))
      {x : ↥(MonoidHom.mrange v) | x ≤ 1}
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
refine_2 :
  (h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2) →
    Γ₀ → ↥(MonoidHom.mrange v)
⊢ (Set.WellFoundedOn
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      fun (x1 x2 : Γ₀) ↦ x1 > x2) ↔
    Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2
have refine_3 : ∀ (h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2),
  Set.MapsTo (β := ↥(MonoidHom.mrange v))
    (fun (x : Γ₀) ↦
      if hx : Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x then
        Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) x hx
      else 1)
    (Set.range.{u_2, u_3 + 1} (ι := O)
      (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
    {x : ↥(MonoidHom.mrange v) | x ≤ 1}
Tactic: refine ⟨fun h ↦ (h.mapsTo Subtype.val ?_).mono' (by simp), fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (goal)
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
refine_1 :
  ∀
    (h :
      Set.WellFoundedOn
        (Set.range.{u_2, u_3 + 1} (ι := O)
          (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
        fun (x1 x2 : Γ₀) ↦ x1 > x2),
    Set.MapsTo.{u_2, u_2} (α := ↥(MonoidHom.mrange v))
      (Subtype.val (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x))
      {x : ↥(MonoidHom.mrange v) | x ≤ 1}
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
refine_2 :
  (h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2) →
    Γ₀ → ↥(MonoidHom.mrange v)
refine_3 :
  ∀ (h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2),
    Set.MapsTo (β := ↥(MonoidHom.mrange v))
      (fun (x : Γ₀) ↦
        if hx : Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x then
          Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) x hx
        else 1)
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      {x : ↥(MonoidHom.mrange v) | x ≤ 1}
⊢ (Set.WellFoundedOn
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      fun (x1 x2 : Γ₀) ↦ x1 > x2) ↔
    Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2
have refine_4 : ∀ (h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2) (a : Γ₀),
  Membership.mem (γ := Set Γ₀)
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      a →
    ∀ (b : Γ₀),
      Membership.mem (γ := Set Γ₀)
          (Set.range.{u_2, u_3 + 1} (ι := O)
            (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
          b →
        a > b →
          ((fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2) on fun (x : Γ₀) ↦
              if hx : Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x then
                Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) x hx
              else 1)
            a b
Tactic: refine ⟨fun h ↦ (h.mapsTo Subtype.val ?_).mono' (by simp), fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (goal)
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h :
  Set.WellFoundedOn
    (Set.range.{u_2, u_3 + 1} (ι := O)
      (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
    fun (x1 x2 : Γ₀) ↦ x1 > x2
x : F
⊢ Membership.mem.{u_2, u_2} (α := ↥(MonoidHom.mrange v)) (γ := Set ↥(MonoidHom.mrange v))
      {x : ↥(MonoidHom.mrange v) | x ≤ 1}
      (Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) ((v : (a : F) → Γ₀) x)
          ⋯ :
        ↥(MonoidHom.mrange v)) →
    Membership.mem.{u_2, u_2} (α := Γ₀) (γ := Set Γ₀)
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      ((↑(Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x)
              ((v : (a : F) → Γ₀) x) ⋯) :
          Γ₀) :
        Γ₀)
have refine_1 : LE.le.{u_2} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀) →
  ∃ (y : O),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀) ((v : (a : F) → Γ₀) x : Γ₀)
Tactic: simp only [← Subtype.coe_le_coe, OneMemClass.coe_one, Set.mem_setOf_eq, Set.mem_range,
      Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (goal)
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h :
  Set.WellFoundedOn
    (Set.range.{u_2, u_3 + 1} (ι := O)
      (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
    fun (x1 x2 : Γ₀) ↦ x1 > x2
x : F
hx : LE.le.{u_2} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (y : O),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀) ((v : (a : F) → Γ₀) x : Γ₀)
have refine_1 : ∀ (y : O) (hx : LE.le.{u_2} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀) (1 : Γ₀)),
  ∃ (y_1 : O),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y_1 : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
Tactic: obtain ⟨y, rfl⟩ := hv.exists_of_le_one hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (goal)
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2
x : Γ₀
⊢ Membership.mem (γ := Set Γ₀)
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      x →
    Membership.mem (γ := Set ↥(MonoidHom.mrange v)) {x : ↥(MonoidHom.mrange v) | x ≤ 1}
      ((fun (x : Γ₀) ↦
          (if hx : Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x then
              Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) x hx
            else 1 :
            ↥(MonoidHom.mrange v)))
        x)
have refine_3 : ∀ (x_1 : O) (h : (v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x_1 : F) = x),
  LE.le.{u_2} (α := ↥(MonoidHom.mrange v))
    (if h : ∃ (x_2 : F), (v : (a : F) → Γ₀) x_2 = x then
      Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) x sorry
    else 1)
    1
Tactic: simp only [Set.mem_range, Function.comp_apply, MonoidHom.mem_mrange, Set.mem_setOf_eq,
      forall_exists_index]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (goal)
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
⊢ (Set.WellFoundedOn
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      fun (x1 x2 : Γ₀) ↦ x1 > x2) ↔
    Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2
have refine_1 : ∀
  (h :
    Set.WellFoundedOn
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      fun (x1 x2 : Γ₀) ↦ x1 > x2),
  Set.MapsTo.{u_2, u_2} (α := ↥(MonoidHom.mrange v))
    (Subtype.val (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x))
    {x : ↥(MonoidHom.mrange v) | x ≤ 1}
    (Set.range.{u_2, u_3 + 1} (ι := O)
      (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
Tactic: classical
  refine ⟨fun h ↦ (h.mapsTo Subtype.val ?_).mono' (by simp), fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
  · rintro ⟨_, x, rfl⟩
    simp only [← Subtype.coe_le_coe, OneMemClass.coe_one, Set.mem_setOf_eq, Set.mem_range,
      Function.comp_apply]
    intro hx
    obtain ⟨y, rfl⟩ := hv.exists_of_le_one hx
    exact ⟨y, by simp⟩
  · exact fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1
  · intro
    simp only [Set.mem_range, Function.comp_apply, MonoidHom.mem_mrange, Set.mem_setOf_eq,
      forall_exists_index]
    rintro x rfl
    simp [← Subtype.coe_le_coe, hv.map_le_one]
  · simp [Function.onFun]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (goal)
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
refine_1 :
  ∀
    (h :
      Set.WellFoundedOn
        (Set.range.{u_2, u_3 + 1} (ι := O)
          (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
        fun (x1 x2 : Γ₀) ↦ x1 > x2),
    Set.MapsTo.{u_2, u_2} (α := ↥(MonoidHom.mrange v))
      (Subtype.val (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x))
      {x : ↥(MonoidHom.mrange v) | x ≤ 1}
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
⊢ (Set.WellFoundedOn
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      fun (x1 x2 : Γ₀) ↦ x1 > x2) ↔
    Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2
have refine_2 : (h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2) →
  Γ₀ → ↥(MonoidHom.mrange v)
Tactic: classical
  refine ⟨fun h ↦ (h.mapsTo Subtype.val ?_).mono' (by simp), fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
  · rintro ⟨_, x, rfl⟩
    simp only [← Subtype.coe_le_coe, OneMemClass.coe_one, Set.mem_setOf_eq, Set.mem_range,
      Function.comp_apply]
    intro hx
    obtain ⟨y, rfl⟩ := hv.exists_of_le_one hx
    exact ⟨y, by simp⟩
  · exact fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1
  · intro
    simp only [Set.mem_range, Function.comp_apply, MonoidHom.mem_mrange, Set.mem_setOf_eq,
      forall_exists_index]
    rintro x rfl
    simp [← Subtype.coe_le_coe, hv.map_le_one]
  · simp [Function.onFun]