awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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₁))
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)
⊢ 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:
constructor
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 : preimage (β := K) (fun (x : K) ↦ x⁻¹) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) ∈ F
⊢ Membership.mem (γ := Filter K) (map (fun (x : K) ↦ x⁻¹) F) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁))

Tactic:
rw [mem_map]

Premises used: Filter.mem_map
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 : M₀ ∩ M₁ ⊆ preimage (β := K) (fun (x : K) ↦ x⁻¹) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁))
⊢ preimage (β := K) (fun (x : K) ↦ x⁻¹) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁)) ∈ F

Tactic:
apply mem_of_superset (Filter.inter_mem M₀_in M₁_in)

Premises used: Filter.inter_mem, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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₀ ∩ M₁ ⊆ preimage (β := K) (fun (x : K) ↦ x⁻¹) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁))

Tactic:
subset_preimage_image _ _

Premises used: Set.subset_preimage_image
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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₀ ∩ M₁ ⊆ preimage (β := K) (fun (x : K) ↦ x⁻¹) ((fun (x : K) ↦ x⁻¹) '' (M₀ ∩ M₁))

Tactic:
exact subset_preimage_image _ _

Premises used: Set.subset_preimage_image
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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₁
h :
  (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y⁻¹ - x⁻¹) <
    (↑γ : MonoidWithZeroHom.ValueGroup₀ v)
⊢ (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀))
      (HSub.hSub (α := K) ((fun (x : K) ↦ x⁻¹) y) ((fun (x : K) ↦ x⁻¹) x)) <
    (↑γ : MonoidWithZeroHom.ValueGroup₀ v)

Tactic:
simp only
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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) <
    (↑(min (γ * γ₀ * γ₀) γ₀) : MonoidWithZeroHom.ValueGroup₀ v)

Tactic:
specialize H₁ x x_in₁ y y_in₁
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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)
⊢ (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤
    (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) x

Tactic:
replace x_in₀ := H₀ x x_in₀
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
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)
⊢ (Valuation.restrict v : (a : K) → MonoidWithZeroHom.ValueGroup₀ (↑v : K →*₀ Γ₀)) (y⁻¹ - x⁻¹) <
    (↑γ : MonoidWithZeroHom.ValueGroup₀ v)

Tactic:
apply Valuation.inversion_estimate

Premises used: Valuation.inversion_estimate
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 →*₀ Γ₀))
⊢ (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤ 0

Tactic:
rw [h] at x_in₀
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 →*₀ Γ₀))
x_in₂ : (↑γ₀ : MonoidWithZeroHom.ValueGroup₀ v) ≤ 0
⊢ 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 →*₀ Γ₀))

Tactic:
rw [h] at x_in₀
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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) ≤ 0
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

Tactic:
simp at x_in₀
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
⊢ 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₀
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
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 →*₀ Γ₀))
⊢ x ≠ 0

Tactic:
(Valuation.ne_zero_iff _).mp this

Premises used: Valuation.ne_zero_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
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 →*₀ Γ₀))
⊢ x ≠ 0

Tactic:
exact (Valuation.ne_zero_iff _).mp this

Premises used: Valuation.ne_zero_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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)

Tactic:
lt_of_lt_of_le H₁ ?_

Premises used: Set.Mem, setOf, lt_of_lt_of_le
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 :
  (↑(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)
⊢ (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:
refine lt_of_lt_of_le H₁ ?_

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ IsClosedMap.{u_1, u_2} (X := K) (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))

Tactic:
IsClosedMap.of_nonempty ?_

Premises used: IsClosedMap.of_nonempty
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
refine :
  ∀ (s : Set K),
    IsClosed[hv.toTopologicalSpace] s →
      s.Nonempty → IsClosed[topologicalSpace] ((⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) '' s)
⊢ IsClosedMap.{u_1, u_2} (X := K) (Y := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))

Tactic:
refine IsClosedMap.of_nonempty ?_

Premises used: IsClosedMap.of_nonempty
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU : IsClosed[hv.toTopologicalSpace] U
hU' : U.Nonempty
⊢ ∀ x ∉ U,
    ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      U ⊆ {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a - x)}

Tactic:
simp only [← isOpen_compl_iff, isOpen_iff_mem_nhds, mem_compl_iff, mem_nhds, subset_compl_comm,
    compl_setOf, not_lt] at hU

Premises used: Set.subset_compl_comm, not_lt, Valued.mem_nhds, isOpen_iff_mem_nhds, isOpen_compl_iff, Set.mem_compl_iff, Set.compl_setOf
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU' : U.Nonempty
hU :
  ∀ x ∉ U,
    ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      U ⊆ {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a - x)}
simp :
  0 ∈ U ∨
    ∃ (γ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)),
      ¬γ = 0 ∧ U ⊆ (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) ⁻¹' Ici γ
⊢ IsClosed[topologicalSpace] ((⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) '' U)

Tactic:
simp only [isClosed_iff, mem_image, map_eq_zero, exists_eq_right, ne_eq, image_subset_iff]

Premises used: Set.mem_image, exists_eq_right, map_eq_zero, WithZeroTopology.isClosed_iff, ne_eq, Set.image_subset_iff
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU' : U.Nonempty
hU :
  ∀ x ∉ U,
    ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      U ⊆ {a : K | (↑γ : ValueGroup₀ v) ≤ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (a - x)}
⊢ 0 ∈ U ∨
    ∃ (γ : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)),
      ¬γ = 0 ∧ U ⊆ (⇑(Valuation.restrict v) : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) ⁻¹' Ici γ

Tactic:
(em _).imp_right fun h ↦ ?_

Premises used: em, Or.imp_right