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 Γ₀
F : Filter K
hF :
  F.NeBot ∧
    ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M,
          ∀ y ∈ M,
            (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
              (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
⊢ NeBot (α := K) (map (fun (x : K) ↦ x⁻¹) F) ∧
    ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      ∃ (M : Set K),
        Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) M ∧
          ∀ x ∈ M,
            ∀ y ∈ M,
              (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
                (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
have refine : ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
  ∃ (M : Set K),
    Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) M ∧
      ∀ x ∈ M,
        ∀ y ∈ M,
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
            (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
Tactic: refine ⟨hF.1.map _, ?_⟩
-- 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 Γ₀
F : Filter K
hF :
  F.NeBot ∧
    ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M,
          ∀ y ∈ M,
            (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
              (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
⊢ ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    ∃ (M : Set K),
      Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) M ∧
        ∀ x ∈ M,
          ∀ y ∈ M,
            (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
              (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
have hF₁ : ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
  ∃ M ∈ F,
    ∀ x ∈ M,
      ∀ y ∈ M,
        (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
          (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
Tactic: replace hF := hF.2
Cleared hypotheses: hF
-- 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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
hF :
  ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        ∀ y ∈ M,
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
            (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
⊢ ∃ (M : Set K),
    Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) M ∧
      ∀ x ∈ M,
        ∀ y ∈ M,
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
            (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
have rcases : ∀ (M₁ : Set K) (M₁_in : M₁ ∈ F)
  (H₁ :
    ∀ x ∈ M₁,
      ∀ y ∈ M₁,
        (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
          (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)),
  ∃ (M : Set K),
    Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) M ∧
      ∀ x ∈ M,
        ∀ y ∈ M,
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
            (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
Tactic: rcases hF (min (γ * γ₀ * γ₀) γ₀) with ⟨M₁, M₁_in, 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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ :
  ∀ x ∈ M₁,
    ∀ y ∈ M₁,
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
        (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
⊢ ∃ (M : Set K),
    Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) M ∧
      ∀ x ∈ M,
        ∀ y ∈ M,
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
            (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
have h : Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) ∧
  ∀ (x : K),
    Membership.mem (γ := Set K) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) x →
      ∀ (y : K),
        Membership.mem (γ := Set K) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) y →
          (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
            (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
Tactic: use (fun x : K => x⁻¹) '' (M₀ ∩ M₁)
-- 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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ :
  ∀ x ∈ M₁,
    ∀ y ∈ M₁,
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
        (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
⊢ Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) ∧
    ∀ (x : K),
      Membership.mem (γ := Set K) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) x →
        ∀ (y : K),
          Membership.mem (γ := Set K) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) y →
            (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
              (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
have h : Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁))
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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ :
  ∀ x ∈ M₁,
    ∀ y ∈ M₁,
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
        (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
h : Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁))
⊢ Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) ∧
    ∀ (x : K),
      Membership.mem (γ := Set K) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) x →
        ∀ (y : K),
          Membership.mem (γ := Set K) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) y →
            (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
              (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
have h₁ : ∀ (x : K),
  Membership.mem (γ := Set K) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) x →
    ∀ (y : K),
      Membership.mem (γ := Set K) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) y →
        (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
          (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ :
  ∀ x ∈ M₁,
    ∀ y ∈ M₁,
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
        (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
⊢ Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁))
have h : preimage (β := K) (fun (x : K) ↦ x⁻¹) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) ∈ F
Tactic: rw [mem_map]
-- 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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ :
  ∀ x ∈ M₁,
    ∀ y ∈ M₁,
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
        (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
⊢ preimage (β := K) (fun (x : K) ↦ x⁻¹) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) ∈ F
have h : M₀ ∩ M₁ ⊆ preimage (β := K) (fun (x : K) ↦ x⁻¹) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁))
Tactic: apply mem_of_superset (Filter.inter_mem M₀_in M₁_in)
-- 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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
H₁ :
  ∀ x ∈ M₁,
    ∀ y ∈ M₁,
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
        (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
x : K
x_in₀ : x ∈ M₀
x_in₁ : x ∈ M₁
y : K
left : y ∈ M₀
y_in₁ : y ∈ M₁
⊢ (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y⁻¹ - x⁻¹) <
    (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
have H₂ : (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
  (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
Tactic: specialize H₁ x x_in₁ y y_in₁
Cleared hypotheses: H₁
-- 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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
H₀ :
  ∀ x ∈ M₀,
    (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
      (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₀ : x ∈ M₀
x_in₁ : x ∈ M₁
y : K
left : y ∈ M₀
y_in₁ : y ∈ M₁
H₁ :
  (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
    (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
⊢ (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y⁻¹ - x⁻¹) <
    (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
have x_in₂ : (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
  (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
Tactic: replace x_in₀ := H₀ x x_in₀
Cleared hypotheses: x_in₀
-- 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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
left : y ∈ M₀
y_in₁ : y ∈ M₁
H₁ :
  (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
    (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
x_in₀ :
  (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
    (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
⊢ (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y⁻¹ - x⁻¹) <
    (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
have h : x ≠ 0
Tactic: apply Valuation.inversion_estimate
-- 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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
left : y ∈ M₀
y_in₁ : y ∈ M₁
H₁ :
  (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
    (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
x_in₀ :
  (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
    (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
h : x ≠ 0
⊢ (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y⁻¹ - x⁻¹) <
    (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
have h₁ : (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
  min
    ((↑γ : MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) *
      HMul.hMul (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β :=
        MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)))
    ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x)
Tactic: apply Valuation.inversion_estimate
-- 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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
left : y ∈ M₀
y_in₁ : y ∈ M₁
H₁ :
  (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
    (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
x_in₀ :
  (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
    (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
h :
  Eq.{u_2 + 1} (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
      MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (0 : MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ False
have x_in₂ : (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤ 0
Tactic: rw [h] at x_in₀
Cleared hypotheses: x_in₀, h
-- 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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
left : y ∈ M₀
y_in₁ : y ∈ M₁
H₁ :
  (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
    (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
x_in₀ :
  (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
    (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
⊢ x ≠ 0
have this : Ne.{u_2 + 1} (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
  ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
    MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
  (0 : MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
Tactic: have : (v.restrict x) ≠ 0 := by
            intro h
            rw [h] at x_in₀
            simp at x_in₀
-- 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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
left : y ∈ M₀
y_in₁ : y ∈ M₁
H₁ :
  (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
    (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
x_in₀ :
  (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
    (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
⊢ (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
    min
      ((↑γ : MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) *
        HMul.hMul (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β :=
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)))
      ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x)
have h : (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v) ≤
  min
    ((↑γ : MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) *
      HMul.hMul (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β :=
        MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)))
    ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x)
Tactic: refine lt_of_lt_of_le 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 Γ₀
F : Filter K
h0 : 𝓝 0 ⊓ F = ⊥
γ₀ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₀ : Set K
M₀_in : M₀ ∈ F
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
M₁ : Set K
M₁_in : M₁ ∈ F
x : K
x_in₁ : x ∈ M₁
y : K
left : y ∈ M₀
y_in₁ : y ∈ M₁
H₁ :
  (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
    (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)
x_in₀ :
  (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
    (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x
⊢ (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v) ≤
    min
      ((↑γ : MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) *
        HMul.hMul (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β :=
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
          ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
            MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)))
      ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x)
have h : min (↑(γ * γ₀ * γ₀) : MonoidWithZeroHom.ValueGroup₀ v) (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
  min
    ((↑γ : MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) *
      HMul.hMul (α := MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β :=
        MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
        ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
          MonoidWithZeroHom.ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)))
    ((Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x)
Tactic: grw [Units.min_val, mul_assoc, Units.val_mul, Units.val_mul, x_in₀]