awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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: 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 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
⊢ IsPrincipalIdealRing O ↔ ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
have refine : ∀ (H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)),
  IsPrincipalIdealRing O
Tactic: refine ⟨fun _ ↦ not_denselyOrdered_of_isPrincipalIdealRing hv, fun H ↦ ?_⟩
-- 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 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
⊢ IsPrincipalIdealRing O
have inl : ∀ (hs : Subsingleton.{u_2 + 1} (↥(MonoidHom.mrange v))ˣ), IsPrincipalIdealRing O
Tactic: rcases subsingleton_or_nontrivial (MonoidHom.mrange v)ˣ with hs | _
-- 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 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
inl : ∀ (hs : Subsingleton.{u_2 + 1} (↥(MonoidHom.mrange v))ˣ), IsPrincipalIdealRing O
⊢ IsPrincipalIdealRing O
have inr : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ → IsPrincipalIdealRing O
Tactic: rcases subsingleton_or_nontrivial (MonoidHom.mrange v)ˣ with hs | _
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (hypothesis)
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 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
hs : Subsingleton.{u_2 + 1} (↥(MonoidHom.mrange v))ˣ
⊢ IsPrincipalIdealRing O
have this : Function.Bijective.{u_3 + 1, u_1 + 1} (α := O) (β := F) (⇑(algebraMap O F) : (a : O) → F)
Tactic: have := bijective_algebraMap_of_subsingleton_units_mrange hv
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (hypothesis)
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 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
h : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
⊢ IsPrincipalIdealRing O
have this : IsDomain O
Tactic: have : IsDomain O := hv.hom_inj.isDomain
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (hypothesis)
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 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
h : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
this : IsDomain O
⊢ IsPrincipalIdealRing O
have this₁ : ValuationRing O
Tactic: have : ValuationRing O := ValuationRing.of_integers v hv
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Archimedean (hypothesis)
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 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
h : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
this_1 : IsDomain O
this : ValuationRing O
⊢ IsPrincipalIdealRing O
have this₁ : IsPrincipalIdealRing O ↔ WfDvdMonoid O
Tactic: have := ((IsBezout.TFAE (R := O)).out 1 3)
-- 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 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
h : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
this_1 : IsDomain O
this_2 : ValuationRing O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
⊢ IsPrincipalIdealRing O
have inr : ¬DenselyOrdered.{u_2} ↥(MonoidHom.mrange v)
Tactic: rw [this, hv.wfDvdMonoid_iff_wellFounded_gt_on_v, hv.wellFounded_gt_on_v_iff_discrete_mrange,
    LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
f g : Valuation R Γ₀
h :
  Eq (α := (a : R) → Γ₀) ((fun (f : Valuation R Γ₀) ↦ (↑f.toMonoidWithZeroHom : ZeroHom R Γ₀).toFun) f)
    ((fun (f : Valuation R Γ₀) ↦ (↑f.toMonoidWithZeroHom : ZeroHom R Γ₀).toFun) g)
⊢ f = g
have obtain : ∀ (toFun : R → Γ₀) (map_zero' : toFun 0 = 0)
  (map_one' : { toFun := toFun, map_zero' := map_zero' : ZeroHom R Γ₀ }.toFun 1 = 1)
  (map_mul' :
    ∀ (x y : R),
      { toFun := toFun, map_zero' := map_zero' : ZeroHom R Γ₀ }.toFun (x * y) =
        { toFun := toFun, map_zero' := map_zero' : ZeroHom R Γ₀ }.toFun x *
          { toFun := toFun, map_zero' := map_zero' : ZeroHom R Γ₀ }.toFun y)
  (map_add_le_max' :
    ∀ (x y : R),
      (↑{ toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : R →*₀ Γ₀ } :
              ZeroHom R Γ₀).toFun
          (x + y) ≤
        max
          ((↑{ toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : R →*₀ Γ₀ } :
                ZeroHom R Γ₀).toFun
            x)
          ((↑{ toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : R →*₀ Γ₀ } :
                ZeroHom R Γ₀).toFun
            y))
  (h :
    Eq (α := (a : R) → Γ₀)
      ((fun (f : Valuation R Γ₀) ↦ (↑f.toMonoidWithZeroHom : ZeroHom R Γ₀).toFun)
        { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul',
          map_add_le_max' := map_add_le_max' })
      ((fun (f : Valuation R Γ₀) ↦ (↑f.toMonoidWithZeroHom : ZeroHom R Γ₀).toFun) g)),
  { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul',
      map_add_le_max' := map_add_le_max' : Valuation R Γ₀ } =
    g
Tactic: obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ∨
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
have rw : LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
Tactic: rw [← le_max_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hf : ∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g
have s₁ : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g)
  (hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) ≤ g), (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) ≤ g
Tactic: refine
    Finset.induction_on s (fun _ => v.map_zero ▸ zero_le')
      (fun a s has ih hf => ?_) hf
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s_1 : Finset ι
f : ι → R
g : Γ₀
hf_1 : ∀ i ∈ s_1, (v : (a : R) → Γ₀) (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g
hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) ≤ g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) ≤ g
have hf₁ : (v : (a : R) → Γ₀) (f a) ≤ g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) ≤ g
Tactic: rw [Finset.forall_mem_insert] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s_1 : Finset ι
f : ι → R
g : Γ₀
hf_1 : ∀ i ∈ s_1, (v : (a : R) → Γ₀) (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g
hf : (v : (a : R) → Γ₀) (f a) ≤ g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) ≤ g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) ≤ g
have rw : (v : (a : R) → Γ₀) (f a + ∑ x ∈ s, f x) ≤ g
Tactic: rw [Finset.sum_insert has]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hf : ∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g
have s₁ : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g)
  (hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) ≤ g), (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) ≤ g
Tactic: classical
  refine
    Finset.induction_on s (fun _ => v.map_zero ▸ zero_le')
      (fun a s has ih hf => ?_) hf
  rw [Finset.forall_mem_insert] at hf; rw [Finset.sum_insert has]
  exact v.map_add_le hf.1 (ih hf.2)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hf : ∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g
s₁ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g)
    (hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) ≤ g), (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) ≤ g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g
have s₂ : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g)
  (hf : (v : (a : R) → Γ₀) (f a) ≤ g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) ≤ g),
  (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) ≤ g
Tactic: classical
  refine
    Finset.induction_on s (fun _ => v.map_zero ▸ zero_le')
      (fun a s has ih hf => ?_) hf
  rw [Finset.forall_mem_insert] at hf; rw [Finset.sum_insert has]
  exact v.map_add_le hf.1 (ih hf.2)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hf : ∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g
s₁ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g)
    (hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) ≤ g), (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) ≤ g
s₂ s₃ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g)
    (hf : (v : (a : R) → Γ₀) (f a) ≤ g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) ≤ g),
    (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) ≤ g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g
have s₄ : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g)
  (hf : (v : (a : R) → Γ₀) (f a) ≤ g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) ≤ g),
  (v : (a : R) → Γ₀) (f a + ∑ x ∈ s, f x) ≤ g
Tactic: classical
  refine
    Finset.induction_on s (fun _ => v.map_zero ▸ zero_le')
      (fun a s has ih hf => ?_) hf
  rw [Finset.forall_mem_insert] at hf; rw [Finset.sum_insert has]
  exact v.map_add_le hf.1 (ih hf.2)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf : ∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g
have s₁ : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g)
  (hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) < g), (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) < g
Tactic: refine
    Finset.induction_on s (fun _ => v.map_zero ▸ (zero_lt_iff.2 hg))
      (fun a s has ih hf => ?_) hf
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s_1 : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf_1 : ∀ i ∈ s_1, (v : (a : R) → Γ₀) (f i) < g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g
hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) < g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) < g
have hf₁ : (v : (a : R) → Γ₀) (f a) < g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) < g
Tactic: rw [Finset.forall_mem_insert] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s_1 : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf_1 : ∀ i ∈ s_1, (v : (a : R) → Γ₀) (f i) < g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g
hf : (v : (a : R) → Γ₀) (f a) < g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) < g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) < g
have rw : (v : (a : R) → Γ₀) (f a + ∑ x ∈ s, f x) < g
Tactic: rw [Finset.sum_insert has]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf : ∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g
have s₁ : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g)
  (hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) < g), (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) < g
Tactic: classical
  refine
    Finset.induction_on s (fun _ => v.map_zero ▸ (zero_lt_iff.2 hg))
      (fun a s has ih hf => ?_) hf
  rw [Finset.forall_mem_insert] at hf; rw [Finset.sum_insert has]
  exact v.map_add_lt hf.1 (ih hf.2)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf : ∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g
s₁ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g)
    (hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) < g), (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) < g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g
have s₂ : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g)
  (hf : (v : (a : R) → Γ₀) (f a) < g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) < g),
  (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) < g
Tactic: classical
  refine
    Finset.induction_on s (fun _ => v.map_zero ▸ (zero_lt_iff.2 hg))
      (fun a s has ih hf => ?_) hf
  rw [Finset.forall_mem_insert] at hf; rw [Finset.sum_insert has]
  exact v.map_add_lt hf.1 (ih hf.2)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf : ∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g
s₁ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g)
    (hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) < g), (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) < g
s₂ s₃ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g)
    (hf : (v : (a : R) → Γ₀) (f a) < g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) < g),
    (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) < g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g
have s₄ : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g)
  (hf : (v : (a : R) → Γ₀) (f a) < g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) < g),
  (v : (a : R) → Γ₀) (f a + ∑ x ∈ s, f x) < g
Tactic: classical
  refine
    Finset.induction_on s (fun _ => v.map_zero ▸ (zero_lt_iff.2 hg))
      (fun a s has ih hf => ?_) hf
  rw [Finset.forall_mem_insert] at hf; rw [Finset.sum_insert has]
  exact v.map_add_lt hf.1 (ih hf.2)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial Γ₀
v : Valuation K Γ₀
x : K
⊢ LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ↔ x ≠ 0
have rw : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) ↔ x ≠ 0
Tactic: rw [zero_lt_iff, ne_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial Γ₀
v : Valuation K Γ₀
x : K
rw : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) ↔ x ≠ 0
⊢ LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ↔ x ≠ 0
have rw₁ : x ≠ 0 ↔ x ≠ 0
Tactic: rw [zero_lt_iff, ne_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) (x + -y) : Γ₀)
have rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + -y) : Γ₀) ((v : (a : R) → Γ₀) (x + -y) : Γ₀)
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ Eq.{u_4 + 1} (α := Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) (-y)) : Γ₀)
    (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
have rw : Eq.{u_4 + 1} (α := Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
  (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
Tactic: rw [map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
g : Γ₀
hx : (v : (a : R) → Γ₀) x ≤ g
hy : (v : (a : R) → Γ₀) y ≤ g
⊢ (v : (a : R) → Γ₀) (x - y) ≤ g
have rw : (v : (a : R) → Γ₀) (x + -y) ≤ g
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
g : Γ₀
hx : (v : (a : R) → Γ₀) x < g
hy : (v : (a : R) → Γ₀) y < g
⊢ (v : (a : R) → Γ₀) (x - y) < g
have rw : (v : (a : R) → Γ₀) (x + -y) < g
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Subsingleton R
v : Valuation R Γ₀
x : R
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have rw : LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) (1 : Γ₀)
Tactic: rw [Subsingleton.elim x 1, Valuation.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Subsingleton R
v : Valuation R Γ₀
x : R
rw : LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have rw₁ : LE.le.{u_4} (α := Γ₀) 1 1
Tactic: rw [Subsingleton.elim x 1, Valuation.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
have suffices : ¬LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
Tactic: suffices ¬v (x + y) < max (v x) (v y) from
    or_iff_not_imp_right.1 (le_iff_eq_or_lt.1 (v.map_add x y)) this