-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
left :
  ∀ (i : ℕ),
    ∃ (j :
      (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
          Valued.v)ˣ),
      ∀ (x y : WithVal (Rat.padicValuation p)),
        (Valuation.restrict Valued.v :
                (a : WithVal (Rat.padicValuation p)) →
                  MonoidWithZeroHom.ValueGroup₀
                    (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
              (y - x) <
            (↑j : MonoidWithZeroHom.ValueGroup₀ Valued.v) →
          (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) :
              ℝ) ≤
            (HPow.hPow (α := ℝ) (↑p : ℝ) i)⁻¹
⊢ (∀ (i : ℕ),
      ∃ (j :
        (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
            Valued.v)ˣ),
        ∀ (x y : WithVal (Rat.padicValuation p)),
          (Valuation.restrict Valued.v :
                  (a : WithVal (Rat.padicValuation p)) →
                    MonoidWithZeroHom.ValueGroup₀
                      (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
                (y - x) <
              (↑j : MonoidWithZeroHom.ValueGroup₀ Valued.v) →
            (↑(padicNorm p
                    ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) :
                ℝ) ≤
              (HPow.hPow (α := ℝ) (↑p : ℝ) i)⁻¹) ∧
    ∀
      (j :
        (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
            Valued.v)ˣ),
      ∃ (i : ℕ),
        ∀ (x y : WithVal (Rat.padicValuation p)),
          (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) :
                ℝ) ≤
              (HPow.hPow (α := ℝ) (↑p : ℝ) i)⁻¹ →
            (Valuation.restrict Valued.v :
                  (a : WithVal (Rat.padicValuation p)) →
                    MonoidWithZeroHom.ValueGroup₀
                      (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
                (y - x) <
              (↑j : MonoidWithZeroHom.ValueGroup₀ Valued.v)
have right : ∀
  (j :
    (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
        Valued.v)ˣ),
  ∃ (i : ℕ),
    ∀ (x y : WithVal (Rat.padicValuation p)),
      (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
          (HPow.hPow (α := ℝ) (↑p : ℝ) i)⁻¹ →
        (Valuation.restrict Valued.v :
              (a : WithVal (Rat.padicValuation p)) →
                MonoidWithZeroHom.ValueGroup₀
                  (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
            (y - x) <
          (↑j : MonoidWithZeroHom.ValueGroup₀ Valued.v)
Tactic: constructor