awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀) ↔
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
have mp : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀) →
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
mp :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀) →
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀) ↔
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
have mpr : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀) →
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
⊢ ∃ (a : K), (v : (a : K) → Γ₀) a = γ
have mp : ∀ (a : hat K) (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ
Tactic: obtain ⟨a, ha⟩ := h γ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
γ : Γ₀
⊢ ∃ (a : hat K), (v : (a : hat K) → Γ₀) a = γ
have mpr : ∀ (a : K) (ha : (v : (a : K) → Γ₀) a = γ), ∃ (a : hat K), (v : (a : hat K) → Γ₀) a = γ
Tactic: obtain ⟨a, ha⟩ := h γ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
a : hat K
ha : (v : (a : hat K) → Γ₀) a = γ
⊢ ∃ (a : K), (v : (a : K) → Γ₀) a = γ
have mp : IsClosed.{u_1} (X := hat K) {a : hat K | ∀ (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ}
Tactic: induction a using Completion.induction_on
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
a : hat K
ha : (v : (a : hat K) → Γ₀) a = γ
mp :
  IsClosed.{u_1} (X := hat K) {a : hat K | ∀ (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ}
⊢ ∃ (a : K), (v : (a : K) → Γ₀) a = γ
have mp₁ : ∀ (a : K) (ha : (v : (a : hat K) → Γ₀) (↑a : hat K) = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ
Tactic: induction a using Completion.induction_on
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ∀ (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ}
have pos : ∀ (H : ∃ (x : K), (v : (a : K) → Γ₀) x = γ),
  IsClosed.{u_1} (X := hat K) {a : hat K | ∀ (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ}
Tactic: by_cases H : ∃ x : K, (v : K → Γ₀) x = γ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
pos :
  ∀ (H : ∃ (x : K), (v : (a : K) → Γ₀) x = γ),
    IsClosed.{u_1} (X := hat K) {a : hat K | ∀ (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ}
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ∀ (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ}
have neg : ∀ (H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ),
  IsClosed.{u_1} (X := hat K) {a : hat K | ∀ (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ}
Tactic: by_cases H : ∃ x : K, (v : K → Γ₀) x = γ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ∀ (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ}
have neg : IsClosed.{u_1} (X := hat K) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
Tactic: simp only [H, imp_false]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
have neg : ∀ (H : ¬∃ (x : K), Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
  IsClosed.{u_1} (X := hat K) {a : hat K | ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : hat K) → Γ₀) a : Γ₀) (0 : Γ₀)}
Tactic: rcases eq_or_ne γ 0 with rfl | hγ
Cleared hypotheses: γ, H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
neg :
  ∀ (H : ¬∃ (x : K), Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    IsClosed.{u_1} (X := hat K) {a : hat K | ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : hat K) → Γ₀) a : Γ₀) (0 : Γ₀)}
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
have neg₁ : ∀ (hγ : γ ≠ 0), IsClosed.{u_1} (X := hat K) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
Tactic: rcases eq_or_ne γ 0 with rfl | hγ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
hγ : γ ≠ 0
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
have neg : ∀ (r : hat K) (hr : (v : (a : hat K) → Γ₀) r = γ),
  IsClosed.{u_1} (X := hat K) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
Tactic: obtain ⟨r, hr⟩ := h γ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
hγ : γ ≠ 0
r : hat K
hr : (v : (a : hat K) → Γ₀) r = γ
⊢ Ne.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
          (a : hat K) → ValueGroup₀ v)
        r :
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
have erw : ¬γ = 0
Tactic: erw [ne_eq, ← embedding_strictMono.injective.eq_iff, embedding_restrict₀ r, hr,
              map_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (hypothesis)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
hγ : γ ≠ 0
r : hat K
hr : (v : (a : hat K) → Γ₀) r = γ
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
have hr' : Ne.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
  (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
        (a : hat K) → ValueGroup₀ v)
      r :
    ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
  (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
Tactic: have hr' : restrict₀ valuedCompletion.v r ≠ 0 := by
            erw [ne_eq, ← embedding_strictMono.injective.eq_iff, embedding_restrict₀ r, hr,
              map_zero]
            exact hγ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
hγ : γ ≠ 0
r : hat K
hr : (v : (a : hat K) → Γ₀) r = γ
hr' :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
          (a : hat K) → ValueGroup₀ v)
        r :
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
have h₁ : Eq.{u_1 + 1} (α := Set (hat K)) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
  (univ \
    {x : hat K |
      Eq.{u_2 + 1} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
        ((Valuation.restrict v : (a : hat K) → ValueGroup₀ (↑v : hat K →*₀ Γ₀)) x :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
        (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
              (a : hat K) → ValueGroup₀ v)
            r :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)})
Tactic: convert! isClosed_univ.sdiff (isOpen_sphere (hat K) hr') using 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
hγ : γ ≠ 0
r : hat K
hr : (v : (a : hat K) → Γ₀) r = γ
hr' :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
          (a : hat K) → ValueGroup₀ v)
        r :
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
⊢ Eq.{u_1 + 1} (α := Set (hat K)) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
    (univ \
      {x : hat K |
        Eq.{u_2 + 1} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
          ((Valuation.restrict v : (a : hat K) → ValueGroup₀ (↑v : hat K →*₀ Γ₀)) x :
            ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
          (((restrict₀ v :
                  MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
                (a : hat K) → ValueGroup₀ v)
              r :
            ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)})
have h₁ : ∀ (x : hat K),
  Membership.mem (γ := Set (hat K)) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ} x ↔
    Membership.mem (γ := Set (hat K))
      (univ \
        {x : hat K |
          Eq.{u_2 + 1} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
            ((Valuation.restrict v : (a : hat K) → ValueGroup₀ (↑v : hat K →*₀ Γ₀)) x :
              ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
            (((restrict₀ v :
                    MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
                  (a : hat K) → ValueGroup₀ v)
                r :
              ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)})
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
R : Type u_3
inst_2 : CommSemiring R
inst_3 : Algebra R K
inst_4 : UniformContinuousConstSMul R K
inst_5 : FaithfulSMul R K
⊢ FaithfulSMul.{u_3, u_1} R (hat K)
have rw : Function.Injective.{u_3 + 1, u_1 + 1} (α := R) (β := hat K) (⇑(algebraMap R (hat K)) : (a : R) → hat K)
Tactic: rw [faithfulSMul_iff_algebraMap_injective R (hat K)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (hypothesis)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : SMul S R
inst_3 : FaithfulSMul S R
m₁ m₂ : S
h : ∀ (a : WithVal v), m₁ • a = m₂ • a
⊢ m₁ = m₂
have h₁ : ∀ (a : WithVal v), m₁ • a.ofVal = m₂ • a.ofVal
Tactic: simp only [smul_right_def, toVal.injEq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
⊢ Eq (α := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) (valueGroup v)
have simp : Eq.{u_2 + 1} (α := Subgroup Γ₀ˣ)
  (Subgroup.closure (Units.val ⁻¹' Set.range.{u_2, u_3 + 1} (ι := WithVal v) (⇑Valued.v : (a : WithVal v) → Γ₀)))
  (Subgroup.closure (Units.val ⁻¹' Set.range.{u_2, u_3 + 1} (ι := WithVal v) ((⇑v : (a : R) → Γ₀) ∘ ofVal)))
Tactic: simp [valueGroup, valueMonoid, ← (WithVal.ofVal_surjective v).range_comp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
b : WithVal v
⊢ Eq (α := ValueGroup₀ v)
    ((valueGroupOrderIso₀ v : (a : ValueGroup₀ Valued.v) → ValueGroup₀ v)
        ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) b :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_3, u_2} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀)) :
      ValueGroup₀ v)
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) b.ofVal : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
have simp : Eq (α := ValueGroup₀ v)
  ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
        (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
      (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
              Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) sorry) sorry) :
          WithZero ↥(valueGroup Valued.v))) :
    WithZero ↥(valueGroup v))
  (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
    else
      (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
            (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) h) sorry) :
        WithZero ↥(valueGroup v)) :
    ValueGroup₀ v)
Tactic: simp [Valued.v.restrict_def, restrict₀_apply, ← apply_ofVal, v.restrict_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
b : WithVal v
⊢ Eq (α := ValueGroup₀ v)
    ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
          (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) ⋯) ⋯) :
            WithZero ↥(valueGroup Valued.v))) :
      WithZero ↥(valueGroup v))
    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) h) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)
have pos : ∀ (hb : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀)),
  Eq (α := ValueGroup₀ v)
    ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
          (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) sorry) sorry) :
            WithZero ↥(valueGroup Valued.v))) :
      WithZero ↥(valueGroup v))
    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) h) sorry) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)
Tactic: by_cases hb : v b.ofVal = 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
b : WithVal v
pos :
  ∀ (hb : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀)),
    Eq (α := ValueGroup₀ v)
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
          else
            (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                  Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) x)
                  (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) ⋯) ⋯) :
              WithZero ↥(valueGroup Valued.v))) :
        WithZero ↥(valueGroup v))
      (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) h) ⋯) :
            WithZero ↥(valueGroup v)) :
        ValueGroup₀ v)
⊢ Eq (α := ValueGroup₀ v)
    ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
          (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) ⋯) ⋯) :
            WithZero ↥(valueGroup Valued.v))) :
      WithZero ↥(valueGroup v))
    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) h) ⋯) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)
have neg : ∀ (hb : ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀)),
  Eq (α := ValueGroup₀ v)
    ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
          (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
        (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) x)
                (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) sorry) sorry) :
            WithZero ↥(valueGroup Valued.v))) :
      WithZero ↥(valueGroup v))
    (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) b.ofVal) h) sorry) :
          WithZero ↥(valueGroup v)) :
      ValueGroup₀ v)
Tactic: by_cases hb : v b.ofVal = 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.WithVal (goal)
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
b : R
⊢ Eq (α := ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
    (((valueGroupOrderIso₀ v).symm : (a : ValueGroup₀ v) → ValueGroup₀ Valued.v)
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) b : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) :
      ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
    ((Valuation.restrict Valued.v : (a : WithVal v) → ValueGroup₀ (↑Valued.v : WithVal v →*₀ Γ₀)) (toVal v b) :
      ValueGroup₀ (F := MonoidWithZeroHom.{u_3, u_2} (WithVal v) Γ₀) (↑Valued.v : WithVal v →*₀ Γ₀))
have simp : Eq (α := ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
  ((WithZero.map' (↑(valueGroupEquiv v).symm : ↥(valueGroup v) →* ↥(valueGroup Valued.v)) :
        (a : WithZero ↥(valueGroup v)) → WithZero ↥(valueGroup Valued.v))
      (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (0 : Γ₀) then 0
      else
        (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦ Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup v) x)
              (Units.mk0 ((v : (a : R) → Γ₀) b) h) sorry) :
          WithZero ↥(valueGroup v))) :
    WithZero ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v))
  (if h : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) b : Γ₀) (0 : Γ₀) then 0
    else
      (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
            Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) x)
            (Units.mk0 ((v : (a : R) → Γ₀) b) sorry) sorry) :
        WithZero ↥(valueGroup Valued.v)) :
    ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
Tactic: simp [Valued.v.restrict_def, restrict₀_apply, ← apply_ofVal, v.restrict_def]