awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (hypothesis)
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 v) (γ := Set (WithAbs v)) (Metric.ball 0 ε)
    (((WithAbs.congr v w (RingEquiv.refl F)).symm : (a : WithAbs w) → WithAbs v) x : WithAbs v)
have hx₁ : (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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
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)
have 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
Tactic: refine IsInducing.isEmbedding <| isInducing_iff_nhds_zero.2 <| Filter.ext fun U ↦
    ⟨fun hU ↦ ?_, fun hU ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
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
⊢ IsEmbedding (X := WithAbs v) (Y := WithAbs w) (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
have 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
Tactic: refine IsInducing.isEmbedding <| isInducing_iff_nhds_zero.2 <| Filter.ext fun U ↦
    ⟨fun hU ↦ ?_, fun hU ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
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
⊢ 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
have 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
Tactic: rw [RingEquiv.image_eq_preimage_symm, Set.preimage_preimage]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (hypothesis)
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)) (𝓝 0) U
have 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
Tactic: rw [← RingEquiv.coe_toEquiv, ← Filter.map_equiv_symm] at hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
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
⊢ Membership.mem (γ := Filter (WithAbs v)) (𝓝 0) U
have 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
Tactic: obtain ⟨s, hs, hss⟩ := Filter.mem_map_iff_exists_image.1 hU
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (hypothesis)
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
⊢ Membership.mem (γ := Filter (WithAbs v)) (𝓝 0) U
have hss₁ : (⇑(↑(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
Cleared hypotheses: hss
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
F : Type u_1
inst : Field F
v w : AbsoluteValue F ℝ
⊢ v.IsEquiv w ↔
    IsHomeomorph (X := WithAbs v) (Y := WithAbs w)
      (⇑(WithAbs.congr v w (RingEquiv.refl F)) : (a : WithAbs v) → WithAbs w)
have 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)
Tactic: rw [isHomeomorph_iff_isEmbedding_surjective]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
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)
have 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
Tactic: refine ⟨fun h ↦ ⟨h.isEmbedding_equivWithAbs, RingEquiv.surjective _⟩, fun ⟨hi, _⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
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
have refine : ∀ (x : F), LT.lt (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) (1 : ℝ) ↔ LT.lt (α := ℝ) ((w : (a : F) → ℝ) x : ℝ) (1 : ℝ)
Tactic: refine isEquiv_iff_lt_one_iff.2 fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
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)
x : F
| LT.lt (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) (1 : ℝ)
have rw : LT.lt (α := ℝ) ((v : (a : F) → ℝ) (WithAbs.toAbs v x).ofAbs : ℝ) (1 : ℝ)
Tactic: rw [← WithAbs.ofAbs_toAbs v x]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
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)
x : F
⊢ LT.lt (α := ℝ) ((v : (a : F) → ℝ) x : ℝ) (1 : ℝ) ↔ LT.lt (α := ℝ) ((w : (a : F) → ℝ) x : ℝ) (1 : ℝ)
have conv_lhs : LT.lt (α := ℝ) ((v : (a : F) → ℝ) (WithAbs.toAbs v x).ofAbs : ℝ) (1 : ℝ) ↔
  LT.lt (α := ℝ) ((w : (a : F) → ℝ) x : ℝ) (1 : ℝ)
Tactic: conv_lhs => rw [← WithAbs.ofAbs_toAbs v x]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
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)
x : F
| LT.lt (α := ℝ) ((w : (a : F) → ℝ) x : ℝ) (1 : ℝ)
have rw : LT.lt (α := ℝ) ((w : (a : F) → ℝ) (WithAbs.toAbs w x).ofAbs : ℝ) (1 : ℝ)
Tactic: rw [← WithAbs.ofAbs_toAbs w x]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
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)
x : F
⊢ LT.lt (α := ℝ) ((v : (a : F) → ℝ) (WithAbs.toAbs v x).ofAbs : ℝ) (1 : ℝ) ↔
    LT.lt (α := ℝ) ((w : (a : F) → ℝ) x : ℝ) (1 : ℝ)
have conv_rhs : LT.lt (α := ℝ) ((v : (a : F) → ℝ) (WithAbs.toAbs v x).ofAbs : ℝ) (1 : ℝ) ↔
  LT.lt (α := ℝ) ((w : (a : F) → ℝ) (WithAbs.toAbs w x).ofAbs : ℝ) (1 : ℝ)
Tactic: conv_rhs => rw [← WithAbs.ofAbs_toAbs w x]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
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)
x : F
⊢ LT.lt (α := ℝ) ((v : (a : F) → ℝ) (WithAbs.toAbs v x).ofAbs : ℝ) (1 : ℝ) ↔
    LT.lt (α := ℝ) ((w : (a : F) → ℝ) (WithAbs.toAbs w x).ofAbs : ℝ) (1 : ℝ)
have rw : Filter.Tendsto.{0, u_1} (β := WithAbs v) (fun (n : ℕ) ↦ WithAbs.toAbs v x ^ n) Filter.atTop (𝓝 0) ↔
  Filter.Tendsto.{0, u_1} (β := WithAbs w) (fun (n : ℕ) ↦ WithAbs.toAbs w x ^ n) Filter.atTop (𝓝 0)
Tactic: rw [← WithAbs.norm_eq_apply_ofAbs, ← WithAbs.norm_eq_apply_ofAbs,
    ← tendsto_pow_atTop_nhds_zero_iff_norm_lt_one, ← tendsto_pow_atTop_nhds_zero_iff_norm_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y z : E
hz : Membership.mem (γ := Set E) (Metric.eball 0 r) z
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) (f (x + y + z - y))
have h : x + y + z - y = x + z
Tactic: convert! hf.hasSum hz using 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y z : E
hz1 : x + y + z ∈ insert (x + y) (s + {y})
hz2 : Membership.mem (γ := Set E) (Metric.eball 0 r) z
⊢ x + z ∈ insert x s
have simp : ∀ (hz1 : z = 0 ∨ x + y + z + -y ∈ s), z = 0 ∨ x + z ∈ s
Tactic: simp only [add_singleton, image_add_right, mem_insert_iff, add_eq_left, mem_preimage] at hz1 ⊢
Cleared hypotheses: hz1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y z : E
hz1 : x + y + z ∈ insert (x + y) (s + {y})
hz2 : Membership.mem (γ := Set E) (Metric.eball 0 r) z
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) (f (x + y + z - y))
have this : x + z ∈ insert x s
Tactic: have : x + z ∈ insert x s := by
      simp only [add_singleton, image_add_right, mem_insert_iff, add_eq_left, mem_preimage] at hz1 ⊢
      abel_nf at hz1
      assumption
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y z : E
hz1 : x + y + z ∈ insert (x + y) (s + {y})
hz2 : Membership.mem (γ := Set E) (Metric.eball 0 r) z
this : x + z ∈ insert x s
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) (f (x + y + z - y))
have h : x + y + z - y = x + z
Tactic: convert! hf.hasSum this hz2 using 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f p x
y : E
⊢ HasFPowerSeriesAt (fun (z : E) ↦ f (z - y)) p (x + y)
have obtain : ∀ (r : ℝ≥0∞) (hf : HasFPowerSeriesOnBall f p x r), HasFPowerSeriesAt (fun (z : E) ↦ f (z - y)) p (x + y)
Tactic: obtain ⟨r, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f p s x
y : E
⊢ HasFPowerSeriesWithinAt (fun (z : E) ↦ f (z - y)) p (s + {y}) (x + y)
have obtain : ∀ (r : ℝ≥0∞) (hf : HasFPowerSeriesWithinOnBall f p s x r),
  HasFPowerSeriesWithinAt (fun (z : E) ↦ f (z - y)) p (s + {y}) (x + y)
Tactic: obtain ⟨r, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
hf : AnalyticAt 𝕜 f x
y : E
⊢ AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (x + y)
have obtain : ∀ (p : FormalMultilinearSeries 𝕜 E F) (hf : HasFPowerSeriesAt f p x),
  AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (x + y)
Tactic: obtain ⟨p, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x ∈ s + {y}
⊢ AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) x
have hx₁ : x + -y ∈ s
Tactic: simp only [add_singleton, image_add_right, mem_preimage] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) x
have rw : AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (x - y + y)
Tactic: rw [show x = (x - y) + y by abel]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ x - y ∈ s
have h : x - y = x + -y
Tactic: convert! hx using 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
y : E
⊢ AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (s + {y}) (x + y)
have obtain : ∀ (p : FormalMultilinearSeries 𝕜 E F) (hf : HasFPowerSeriesWithinAt f p s x),
  AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (s + {y}) (x + y)
Tactic: obtain ⟨p, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x ∈ s + {y}
⊢ AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (s + {y}) x
have hx₁ : x + -y ∈ s
Tactic: simp only [add_singleton, image_add_right, mem_preimage] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (s + {y}) x
have rw : AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (s + {y}) (x - y + y)
Tactic: rw [show x = (x - y) + y by abel]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ x - y ∈ s
have h : x - y = x + -y
Tactic: convert! hx using 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ Metric.eball x r
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f y)
have this : Membership.mem (γ := Set E) (Metric.eball 0 r) (y - x)
Tactic: have : y - x ∈ Metric.eball 0 r := by simpa [edist_eq_enorm_sub] using hy.2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y : E
hy : y ∈ Metric.eball x r
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f y)
have this : Membership.mem (γ := Set E) (Metric.eball 0 r) (y - x)
Tactic: have : y - x ∈ Metric.eball 0 r := by simpa [edist_eq_enorm_sub] using hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
⊢ HasFPowerSeriesWithinOnBall g p s x r
have refine : ∀ {y : E},
  x + y ∈ insert x s →
    Membership.mem (γ := Set E) (Metric.eball 0 r) y →
      HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (g (x + y))
Tactic: refine ⟨h.r_le, h.r_pos, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (g (x + y))
have h₁ : g (x + y) = f (x + y)
Tactic: convert! h.hasSum hy h'y using 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ g (x + y) = f (x + y)
have hy₁ : y = 0 ∨ x + y ∈ s
Tactic: simp only [mem_insert_iff, add_eq_left] at hy
Cleared hypotheses: hy