awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
linarith :
  log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a) = 0 →
    log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a) - 0 +
        (HMul.hMul (α := ℝ) 1 0 - 1 * (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a))) =
      0
⊢ log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a) ≠ 0

Tactic:
linarith [h.log_div_log_pos ha₀ ha₁]

Premises used: AbsoluteValue.IsEquiv.log_div_log_pos
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
⊢ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) 0 : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) 0

Tactic:
simp [zero_rpow (by linarith [h.log_div_log_pos ha₀ ha₁])]

Premises used: Real.zero_rpow
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
pos :
  ∀ (hb₁ : Eq (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (1 : ℝ)),
    HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
      (w : (a : F) → ℝ) b
pos₁ :
  ∀ (hb₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (1 : ℝ)),
    HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
      (w : (a : F) → ℝ) b
⊢ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b

Tactic:
rcases eq_or_ne (w b) 1 with hb₁ | hb₁

Premises used: eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
hb₁ : Eq (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (1 : ℝ)
⊢ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b

Tactic:
simp [hb₁, h.eq_one_iff.2 hb₁]

Premises used: Iff.mpr, AbsoluteValue.IsEquiv.eq_one_iff
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : w.IsNontrivial
a : F
ha₀ : a ≠ 0
ha₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) a : ℝ) (1 : ℝ)
b : F
hb₀ : b ≠ 0
hb₁ : Ne (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) (1 : ℝ)
pos :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) b) / log ((v : (a : F) → ℝ) b)) =
    (w : (a : F) → ℝ) b
pos₁ :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) ((log ((v : (a : F) → ℝ) b))⁻¹ * log ((w : (a : F) → ℝ) b)) =
    (w : (a : F) → ℝ) b
pos₂ :
  HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((v : (a : F) → ℝ) b))⁻¹ ^ log ((w : (a : F) → ℝ) b) =
    (w : (a : F) → ℝ) b
pos₃ : rexp 1 ^ log ((w : (a : F) → ℝ) b) = (w : (a : F) → ℝ) b
pos₄ : rexp (log ((w : (a : F) → ℝ) b)) = (w : (a : F) → ℝ) b
pos₅ pos₆ : Eq (α := ℝ) ((w : (a : F) → ℝ) b : ℝ) ((w : (a : F) → ℝ) b : ℝ)
⊢ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) b : ℝ) (log ((w : (a : F) → ℝ) a) / log ((v : (a : F) → ℝ) a)) =
    (w : (a : F) → ℝ) b

Tactic:
rw [← h.symm.log_div_log_eq_log_div_log ha₀ ha₁ hb₀ hb₁, div_eq_inv_mul, rpow_mul (v.nonneg _),
      rpow_inv_log (v.pos hb₀) (h.eq_one_iff.not.2 hb₁), exp_one_rpow, exp_log (w.pos hb₀)]

Premises used: Iff.mpr, Real.rpow_inv_log, Real.exp_one_rpow, Iff.not, AbsoluteValue.pos, AbsoluteValue.nonneg, Real.exp_log, AbsoluteValue.IsEquiv.eq_one_iff, AbsoluteValue.IsEquiv.symm, div_eq_inv_mul, Real.rpow_mul, AbsoluteValue.IsEquiv.log_div_log_eq_log_div_log
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : ¬w.IsNontrivial
x : F
inl : HPow.hPow (α := ℝ) (β := ℝ) ((v : (a : F) → ℝ) 0 : ℝ) 1 = (w : (a : F) → ℝ) 0
inr : ∀ (h₀ : x ≠ 0), HPow.hPow (α := ℝ) (β := ℝ) ((v : (a : F) → ℝ) x : ℝ) 1 = (w : (a : F) → ℝ) x
⊢ HPow.hPow (α := ℝ) (β := ℝ) ((v : (a : F) → ℝ) x : ℝ) 1 = (w : (a : F) → ℝ) x

Tactic:
rcases eq_or_ne x 0 with rfl | h₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : ¬w.IsNontrivial
⊢ HPow.hPow (α := ℝ) (β := ℝ) ((v : (a : F) → ℝ) 0 : ℝ) 1 = (w : (a : F) → ℝ) 0

Tactic:
aesop (add simp [h.isNontrivial_congr])

Premises used: AbsoluteValue.IsEquiv.isNontrivial_congr
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : ¬w.IsNontrivial
x : F
h₀ : x ≠ 0
⊢ HPow.hPow (α := ℝ) (β := ℝ) ((v : (a : F) → ℝ) x : ℝ) 1 = (w : (a : F) → ℝ) x

Tactic:
aesop (add simp [h.isNontrivial_congr])

Premises used: AbsoluteValue.IsEquiv.isNontrivial_congr
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : ¬w.IsNontrivial
⊢ ∃ (c : ℝ), 0 < c ∧ Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)

Tactic:
exact ⟨1, zero_lt_one,
      funext fun x ↦ by
        rcases eq_or_ne x 0 with rfl | h₀ <;>
        aesop (add simp [h.isNontrivial_congr])⟩
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : Membership.mem (γ := Filter (WithAbs v)) (𝓝 0) U
rw :
  ∀ (hU : ∃ ε > 0, Metric.ball 0 ε ⊆ U),
    ∃ ε > 0,
      Subset (α := Set (WithAbs w)) (Metric.ball 0 ε)
        ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
⊢ Membership.mem (γ := Filter (WithAbs w)) (𝓝 0)
    ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)

Tactic:
rw [Metric.mem_nhds_iff] at hU ⊢

Premises used: Metric.mem_nhds_iff
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : ∃ ε > 0, Metric.ball 0 ε ⊆ U
obtain :
  ∀ (ε : ℝ) (hε : ε > 0) (hU : Metric.ball 0 ε ⊆ U),
    ∃ ε > 0,
      Subset (α := Set (WithAbs w)) (Metric.ball 0 ε)
        ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
⊢ ∃ ε > 0,
    Subset (α := Set (WithAbs w)) (Metric.ball 0 ε)
      ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)

Tactic:
obtain ⟨ε, hε, hU⟩ := hU
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
obtain :
  ∀ (c : ℝ) (hc : 0 < c)
    (hvw : Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)),
    ∃ ε > 0,
      Subset (α := Set (WithAbs w)) (Metric.ball 0 ε)
        ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
⊢ ∃ ε > 0,
    Subset (α := Set (WithAbs w)) (Metric.ball 0 ε)
      ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)

Tactic:
obtain ⟨c, hc, hvw⟩ := isEquiv_iff_exists_rpow_eq.1 h

Premises used: Iff.mp, AbsoluteValue.isEquiv_iff_exists_rpow_eq
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
c : ℝ
hc : 0 < c
hvw : Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
⊢ ∃ ε > 0,
    Subset (α := Set (WithAbs w)) (Metric.ball 0 ε)
      ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)

Tactic:
⟨ε ^ c, rpow_pos_of_pos hε _, fun x hx ↦ ?_⟩

Premises used: Real.rpow_pos_of_pos, HPow.hPow, And.intro, Exists.intro
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
c : ℝ
hc : 0 < c
hvw : Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
refine :
  ∀ (x : WithAbs w) (hx : Membership.mem (γ := Set (WithAbs w)) (Metric.ball 0 (ε ^ c)) x),
    Membership.mem (γ := Set (WithAbs w)) ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
      x
⊢ ∃ ε > 0,
    Subset (α := Set (WithAbs w)) (Metric.ball 0 ε)
      ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)

Tactic:
refine ⟨ε ^ c, rpow_pos_of_pos hε _, fun x hx ↦ ?_⟩
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
c : ℝ
hc : 0 < c
hvw : Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
x : WithAbs w
hx : Membership.mem (γ := Set (WithAbs w)) (Metric.ball 0 (ε ^ c)) x
rw :
  Membership.mem (α := WithAbs w) (γ := Set (WithAbs w))
    ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
    ((WithAbs.congr v w (RingEquiv.refl F) : (a : WithAbs v) → WithAbs w)
        (((WithAbs.congr v w (RingEquiv.refl F)).symm : (a : WithAbs w) → WithAbs v) x) :
      WithAbs w)
⊢ Membership.mem (γ := Set (WithAbs w)) ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U) x

Tactic:
rw [← RingEquiv.apply_symm_apply (WithAbs.congr v w (.refl F)) x]

Premises used: RingEquiv.apply_symm_apply, RingEquiv.refl, WithAbs.congr
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
c : ℝ
hc : 0 < c
hvw : Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
x : WithAbs w
hx : Membership.mem (γ := Set (WithAbs w)) (Metric.ball 0 (ε ^ c)) x
⊢ Membership.mem (α := WithAbs w) (γ := Set (WithAbs w))
    ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
    ((WithAbs.congr v w (RingEquiv.refl F) : (a : WithAbs v) → WithAbs w)
        (((WithAbs.congr v w (RingEquiv.refl F)).symm : (a : WithAbs w) → WithAbs v) x) :
      WithAbs w)

Tactic:
Set.mem_image_of_mem _ (hU ?_)

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
c : ℝ
hc : 0 < c
hvw : Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
x : WithAbs w
hx : Membership.mem (γ := Set (WithAbs w)) (Metric.ball 0 (ε ^ c)) x
refine :
  Membership.mem (α := WithAbs v) (γ := Set (WithAbs v)) (Metric.ball 0 ε)
    (((WithAbs.congr v w (RingEquiv.refl F)).symm : (a : WithAbs w) → WithAbs v) x : WithAbs v)
⊢ Membership.mem (α := WithAbs w) (γ := Set (WithAbs w))
    ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U)
    ((WithAbs.congr v w (RingEquiv.refl F) : (a : WithAbs v) → WithAbs w)
        (((WithAbs.congr v w (RingEquiv.refl F)).symm : (a : WithAbs w) → WithAbs v) x) :
      WithAbs w)

Tactic:
refine Set.mem_image_of_mem _ (hU ?_)

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
c : ℝ
hc : 0 < c
hvw : Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
x : WithAbs w
hx : Membership.mem (γ := Set (WithAbs w)) (Metric.ball 0 (ε ^ c)) x
⊢ (v : (a : F) → ℝ) x.ofAbs < ε

Tactic:
rw [Metric.mem_ball, dist_zero_right, WithAbs.norm_eq_apply_ofAbs, ← funext_iff.1 hvw,
    rpow_lt_rpow_iff (v.nonneg _) hε.le hc] at hx

Premises used: funext_iff, LT.lt.le, AbsoluteValue.nonneg, Metric.mem_ball, Iff.mp, WithAbs.norm_eq_apply_ofAbs, Real.rpow_lt_rpow_iff, dist_zero_right
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
c : ℝ
hc : 0 < c
hvw : Eq (α := F → ℝ) (fun (x : F) ↦ HPow.hPow (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) c) (⇑w : (a : F) → ℝ)
x : WithAbs w
hx : (v : (a : F) → ℝ) x.ofAbs < ε
⊢ Membership.mem (α := WithAbs v) (γ := Set (WithAbs v)) (Metric.ball 0 ε)
    (((WithAbs.congr v w (RingEquiv.refl F)).symm : (a : WithAbs w) → WithAbs v) x : WithAbs v)

Tactic:
simpa [WithAbs.norm_eq_apply_ofAbs]

Premises used: WithAbs.norm_eq_apply_ofAbs
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
⊢ IsEmbedding (X := WithAbs v) (Y := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)

Tactic:
IsInducing.isEmbedding <| isInducing_iff_nhds_zero.2 <| Filter.ext fun U ↦
    ⟨fun hU ↦ ?_, fun hU ↦ ?_⟩

Premises used: Iff.mpr, IsTopologicalAddGroup.isInducing_iff_nhds_zero, Filter.ext, Topology.IsInducing.isEmbedding, Iff.intro
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
refine_1 :
  ∀ (U : Set (WithAbs v)) (hU : Membership.mem (γ := Filter (WithAbs v)) (𝓝 0) U),
    Membership.mem (γ := Filter (WithAbs v))
      (Filter.comap (β := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) (𝓝 0)) U
refine_2 :
  ∀ (U : Set (WithAbs v))
    (hU :
      Membership.mem (γ := Filter (WithAbs v))
        (Filter.comap (β := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) (𝓝 0))
        U),
    Membership.mem (γ := Filter (WithAbs v)) (𝓝 0) U
⊢ IsEmbedding (X := WithAbs v) (Y := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)

Tactic:
refine IsInducing.isEmbedding <| isInducing_iff_nhds_zero.2 <| Filter.ext fun U ↦
    ⟨fun hU ↦ ?_, fun hU ↦ ?_⟩

Premises used: Iff.mpr, IsTopologicalAddGroup.isInducing_iff_nhds_zero, Filter.ext, Topology.IsInducing.isEmbedding, Iff.intro
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : Membership.mem (γ := Filter (WithAbs v)) (𝓝 0) U
rw :
  (fun (x : WithAbs v) ↦
        ((WithAbs.congr v w (RingEquiv.refl F)).symm : (a : WithAbs w) → WithAbs v)
          ((WithAbs.congr v w (RingEquiv.refl F) : (a : WithAbs v) → WithAbs w) x)) ⁻¹'
      U ⊆
    U
⊢ Set.preimage (β := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
      ((⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) '' U) ⊆
    U

Tactic:
rw [RingEquiv.image_eq_preimage_symm, Set.preimage_preimage]

Premises used: Set.preimage_preimage, RingEquiv.image_eq_preimage_symm
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : Membership.mem (γ := Filter (WithAbs v)) (𝓝 0) U
⊢ (fun (x : WithAbs v) ↦
        ((WithAbs.congr v w (RingEquiv.refl F)).symm : (a : WithAbs w) → WithAbs v)
          ((WithAbs.congr v w (RingEquiv.refl F) : (a : WithAbs v) → WithAbs w) x)) ⁻¹'
      U ⊆
    U

Tactic:
simp
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : Membership.mem (γ := Filter (WithAbs v)) (𝓝 0) U
⊢ Membership.mem (γ := Filter (WithAbs v))
    (Filter.comap (β := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) (𝓝 0)) U

Tactic:
exact ⟨WithAbs.congr v w (.refl F)'' U, h.equivWithAbs_image_mem_nhds_zero hU,
      by
        #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
        (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
        goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in
        the new canonicalizer; a minimization would help. The original proof was:
        `grind [RingEquiv.image_eq_preimage_symm, Set.preimage_preimage]` -/
        rw [RingEquiv.image_eq_preimage_symm, Set.preimage_preimage]; simp⟩
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU :
  Membership.mem (γ := Filter (WithAbs v))
    (Filter.comap (β := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) (𝓝 0)) U
⊢ Membership.mem (γ := Filter (WithAbs v))
    (Filter.map (α := WithAbs w)
      (⇑(↑(WithAbs.congr v w (RingEquiv.refl F)) : WithAbs v ≃ WithAbs w).symm : (a : WithAbs w) → WithAbs v) (𝓝 0))
    U

Tactic:
rw [← RingEquiv.coe_toEquiv, ← Filter.map_equiv_symm] at hU

Premises used: RingEquiv.coe_toEquiv, Filter.map_equiv_symm
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU :
  Membership.mem (γ := Filter (WithAbs v))
    (Filter.map (α := WithAbs w)
      (⇑(↑(WithAbs.congr v w (RingEquiv.refl F)) : WithAbs v ≃ WithAbs w).symm : (a : WithAbs w) → WithAbs v) (𝓝 0))
    U
refine_2 :
  ∀ (s : Set (WithAbs w)) (hs : Membership.mem (γ := Filter (WithAbs w)) (𝓝 0) s)
    (hss :
      (⇑(↑(WithAbs.congr v w (RingEquiv.refl F)) : WithAbs v ≃ WithAbs w).symm : (a : WithAbs w) → WithAbs v) '' s ⊆ U),
    Membership.mem (γ := Filter (WithAbs v)) (𝓝 0) U
⊢ Membership.mem (γ := Filter (WithAbs v)) (𝓝 0) U

Tactic:
obtain ⟨s, hs, hss⟩ := Filter.mem_map_iff_exists_image.1 hU

Premises used: Iff.mp, Filter.mem_map_iff_exists_image
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU :
  Membership.mem (γ := Filter (WithAbs v))
    (Filter.map (α := WithAbs w)
      (⇑(↑(WithAbs.congr v w (RingEquiv.refl F)) : WithAbs v ≃ WithAbs w).symm : (a : WithAbs w) → WithAbs v) (𝓝 0))
    U
s : Set (WithAbs w)
hs : Membership.mem (γ := Filter (WithAbs w)) (𝓝 0) s
hss : (⇑(↑(WithAbs.congr v w (RingEquiv.refl F)) : WithAbs v ≃ WithAbs w).symm : (a : WithAbs w) → WithAbs v) '' s ⊆ U
⊢ (⇑(↑(WithAbs.congr w v (RingEquiv.symm (RingEquiv.refl F))) : WithAbs w ≃ WithAbs v) : (a : WithAbs w) → WithAbs v) ''
      s ⊆
    U

Tactic:
rw [← RingEquiv.coe_toEquiv_symm, WithAbs.congr_symm] at hss

Premises used: RingEquiv.coe_toEquiv_symm, WithAbs.congr_symm
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU :
  Membership.mem (γ := Filter (WithAbs v))
    (Filter.map (α := WithAbs w)
      (⇑(↑(WithAbs.congr v w (RingEquiv.refl F)) : WithAbs v ≃ WithAbs w).symm : (a : WithAbs w) → WithAbs v) (𝓝 0))
    U
s : Set (WithAbs w)
hs : Membership.mem (γ := Filter (WithAbs w)) (𝓝 0) s
hss :
  (⇑(↑(WithAbs.congr w v (RingEquiv.symm (RingEquiv.refl F))) : WithAbs w ≃ WithAbs v) : (a : WithAbs w) → WithAbs v) ''
      s ⊆
    U
⊢ Membership.mem (γ := Filter (WithAbs v)) (𝓝 0) U

Tactic:
Filter.mem_of_superset (h.symm.equivWithAbs_image_mem_nhds_zero hs) hss

Premises used: AbsoluteValue.IsEquiv.equivWithAbs_image_mem_nhds_zero, AbsoluteValue.IsEquiv.symm, Filter.mem_of_superset
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU :
  Membership.mem (γ := Filter (WithAbs v))
    (Filter.map (α := WithAbs w)
      (⇑(↑(WithAbs.congr v w (RingEquiv.refl F)) : WithAbs v ≃ WithAbs w).symm : (a : WithAbs w) → WithAbs v) (𝓝 0))
    U
s : Set (WithAbs w)
hs : Membership.mem (γ := Filter (WithAbs w)) (𝓝 0) s
hss :
  (⇑(↑(WithAbs.congr w v (RingEquiv.symm (RingEquiv.refl F))) : WithAbs w ≃ WithAbs v) : (a : WithAbs w) → WithAbs v) ''
      s ⊆
    U
⊢ Membership.mem (γ := Filter (WithAbs v)) (𝓝 0) U

Tactic:
exact Filter.mem_of_superset (h.symm.equivWithAbs_image_mem_nhds_zero hs) hss

Premises used: AbsoluteValue.IsEquiv.equivWithAbs_image_mem_nhds_zero, AbsoluteValue.IsEquiv.symm, Filter.mem_of_superset
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
rw :
  v.IsEquiv w ↔
    IsEmbedding (X := WithAbs v) (Y := WithAbs w)
        (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) ∧
      Function.Surjective (α := WithAbs v) (β := WithAbs w)
        (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
⊢ v.IsEquiv w ↔
    IsHomeomorph (X := WithAbs v) (Y := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)

Tactic:
rw [isHomeomorph_iff_isEmbedding_surjective]

Premises used: isHomeomorph_iff_isEmbedding_surjective
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
⊢ v.IsEquiv w ↔
    IsEmbedding (X := WithAbs v) (Y := WithAbs w)
        (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) ∧
      Function.Surjective (α := WithAbs v) (β := WithAbs w)
        (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)

Tactic:
⟨fun h ↦ ⟨h.isEmbedding_equivWithAbs, RingEquiv.surjective _⟩, fun ⟨hi, _⟩ ↦ ?_⟩

Premises used: AbsoluteValue.IsEquiv.isEmbedding_equivWithAbs, RingEquiv.surjective, RingEquiv.refl, _private.0.AbsoluteValue.isEquiv_iff_isHomeomorph.match_1, And.intro, Iff.intro, WithAbs.congr, AbsoluteValue.IsEquiv
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
refine :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w)
        (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) ∧
      Function.Surjective (α := WithAbs v) (β := WithAbs w)
        (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) →
    ∀
      (hi :
        IsEmbedding (X := WithAbs v) (Y := WithAbs w)
          (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)),
      Function.Surjective (α := WithAbs v) (β := WithAbs w)
          (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) →
        v.IsEquiv w
⊢ v.IsEquiv w ↔
    IsEmbedding (X := WithAbs v) (Y := WithAbs w)
        (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) ∧
      Function.Surjective (α := WithAbs v) (β := WithAbs w)
        (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)

Tactic:
refine ⟨fun h ↦ ⟨h.isEmbedding_equivWithAbs, RingEquiv.surjective _⟩, fun ⟨hi, _⟩ ↦ ?_⟩
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
h :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w) ∧
    Function.Surjective (α := WithAbs v) (β := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
hi :
  IsEmbedding (X := WithAbs v) (Y := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
right :
  Function.Surjective (α := WithAbs v) (β := WithAbs w)
    (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
⊢ v.IsEquiv w

Tactic:
isEquiv_iff_lt_one_iff.2 fun x ↦ ?_

Premises used: Iff.mpr, AbsoluteValue.isEquiv_iff_lt_one_iff