awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : C(E, F)
simp :
  ∀ (a : Set E) (b : ℝ),
    IsCompact a →
      0 < b →
        ∃ (y : C(E, F)),
          ContDiff.{0, u_1, u_2} ℝ (E := E) (F := F) ∞ (⇑y : (a : E) → F) ∧
            ∀ x ∈ a, dist.{u_2} (α := F) ((y : (a : E) → F) x : F) ((f : (a : E) → F) x : F) < b
⊢ ∀ (i : Set E × ℝ),
    IsCompact i.1 ∧ 0 < i.2 →
      ∃ (y : C(E, F)),
        Membership.mem (γ := Set C(E, F))
            {f : C(E, F) | ContDiff.{0, u_1, u_2} ℝ (E := E) (F := F) ∞ (⇑f : (a : E) → F)} y ∧
          Membership.mem (γ := Set C(E, F))
            {y : C(E, F) |
              Membership.mem (γ := SetRel C(E, F) C(E, F))
                {fg : C(E, F) × C(E, F) |
                  ∀ x ∈ i.1,
                    Membership.mem.{u_2, u_2} (α := F × F) (γ := Set (F × F)) {p : F × F | dist p.1 p.2 < i.2}
                      (((fg.1 : (a : E) → F) x, (fg.2 : (a : E) → F) x) : F × F)}
                (y, f)}
            y

Tactic:
simp only [Prod.forall, mem_setOf_eq, and_imp]

Premises used: and_imp, Set.mem_setOf_eq, Prod.forall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : C(E, F)
K : Set E
ε : ℝ
hK : IsCompact K
hε : 0 < ε
⊢ ContinuousOn.{u_1, u_2} (Y := F) (⇑f : (a : E) → F) (cthickening 1 K)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : C(E, F)
K : Set E
ε : ℝ
hK : IsCompact K
hε : 0 < ε
⊢ UniformContinuousOn.{u_1, u_2} (β := F) (⇑f : (a : E) → F) (cthickening 1 K)

Tactic:
have : UniformContinuousOn f (cthickening 1 K) :=
    hK.cthickening.uniformContinuousOn_of_continuous <| by fun_prop
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : C(E, F)
K : Set E
ε : ℝ
hK : IsCompact K
hε : 0 < ε
this : UniformContinuousOn.{u_1, u_2} (β := F) (⇑f : (a : E) → F) (cthickening 1 K)
rcases :
  ∀ (δ : ℝ) (hδ : δ > 0)
    (hfδ :
      ∀ x ∈ cthickening 1 K,
        ∀ y ∈ cthickening 1 K,
          dist x y < δ → dist.{u_2} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F) < ε / 2),
    ∃ (y : C(E, F)),
      ContDiff.{0, u_1, u_2} ℝ (E := E) (F := F) ∞ (⇑y : (a : E) → F) ∧
        ∀ x ∈ K, dist.{u_2} (α := F) ((y : (a : E) → F) x : F) ((f : (a : E) → F) x : F) < ε
⊢ ∃ (y : C(E, F)),
    ContDiff.{0, u_1, u_2} ℝ (E := E) (F := F) ∞ (⇑y : (a : E) → F) ∧
      ∀ x ∈ K, dist.{u_2} (α := F) ((y : (a : E) → F) x : F) ((f : (a : E) → F) x : F) < ε

Tactic:
rcases Metric.uniformContinuousOn_iff.mp this (ε / 2) (half_pos hε) with ⟨δ, hδ, hfδ⟩

Premises used: half_pos, HDiv.hDiv, Metric.uniformContinuousOn_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : C(E, F)
K : Set E
ε : ℝ
hK : IsCompact K
hε : 0 < ε
this : UniformContinuousOn.{u_1, u_2} (β := F) (⇑f : (a : E) → F) (cthickening 1 K)
δ : ℝ
hδ : δ > 0
hfδ :
  ∀ x ∈ cthickening 1 K,
    ∀ y ∈ cthickening 1 K,
      dist x y < δ → dist.{u_2} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F) < ε / 2
rcases :
  ∀ (g : E → F) (hgc : ContDiff ℝ ∞ g)
    (hg :
      ∀ (a : E) (δ_1 : ℝ),
        (∀ x ∈ ball a (min 1 δ), dist.{u_2} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) a : F) ≤ δ_1) →
          dist (g a) ((f : (a : E) → F) a) ≤ δ_1),
    ∃ (y : C(E, F)),
      ContDiff.{0, u_1, u_2} ℝ (E := E) (F := F) ∞ (⇑y : (a : E) → F) ∧
        ∀ x ∈ K, dist.{u_2} (α := F) ((y : (a : E) → F) x : F) ((f : (a : E) → F) x : F) < ε
⊢ ∃ (y : C(E, F)),
    ContDiff.{0, u_1, u_2} ℝ (E := E) (F := F) ∞ (⇑y : (a : E) → F) ∧
      ∀ x ∈ K, dist.{u_2} (α := F) ((y : (a : E) → F) x : F) ((f : (a : E) → F) x : F) < ε

Tactic:
rcases (map_continuous f).exists_contDiff_dist_le_of_forall_mem_ball_dist_le
    (lt_min one_pos hδ) with ⟨g, hgc, hg⟩

Premises used: Continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le, lt_min, ContinuousMapClass.map_continuous, one_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : C(E, F)
K : Set E
ε : ℝ
hK : IsCompact K
hε : 0 < ε
this : UniformContinuousOn.{u_1, u_2} (β := F) (⇑f : (a : E) → F) (cthickening 1 K)
δ : ℝ
hδ : δ > 0
hfδ :
  ∀ x ∈ cthickening 1 K,
    ∀ y ∈ cthickening 1 K,
      dist x y < δ → dist.{u_2} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F) < ε / 2
g : E → F
hgc : ContDiff ℝ ∞ g
hg :
  ∀ (a : E) (δ_1 : ℝ),
    (∀ x ∈ ball a (min 1 δ), dist.{u_2} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) a : F) ≤ δ_1) →
      dist (g a) ((f : (a : E) → F) a) ≤ δ_1
⊢ ∃ (y : C(E, F)),
    ContDiff.{0, u_1, u_2} ℝ (E := E) (F := F) ∞ (⇑y : (a : E) → F) ∧
      ∀ x ∈ K, dist.{u_2} (α := F) ((y : (a : E) → F) x : F) ((f : (a : E) → F) x : F) < ε

Tactic:
⟨⟨g, hgc.continuous⟩, hgc, fun x hx ↦ (hg _ _ fun y hy ↦ ?_).trans_lt (half_lt_self hε)⟩

Premises used: half_lt_self, ContinuousMap.mk, ContDiff.continuous, HDiv.hDiv, And.intro, Exists.intro, OfNat.ofNat, LE.le.trans_lt
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : C(E, F)
K : Set E
ε : ℝ
hK : IsCompact K
hε : 0 < ε
this : UniformContinuousOn.{u_1, u_2} (β := F) (⇑f : (a : E) → F) (cthickening 1 K)
δ : ℝ
hδ : δ > 0
hfδ :
  ∀ x ∈ cthickening 1 K,
    ∀ y ∈ cthickening 1 K,
      dist x y < δ → dist.{u_2} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F) < ε / 2
g : E → F
hgc : ContDiff ℝ ∞ g
hg :
  ∀ (a : E) (δ_1 : ℝ),
    (∀ x ∈ ball a (min 1 δ), dist.{u_2} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) a : F) ≤ δ_1) →
      dist (g a) ((f : (a : E) → F) a) ≤ δ_1
refine :
  ∀ (x : E) (hx : x ∈ K) (y : E) (hy : y ∈ ball x (min 1 δ)),
    dist.{u_2} (α := F) ((f : (a : E) → F) y : F) ((f : (a : E) → F) x : F) ≤ ε / 2
⊢ ∃ (y : C(E, F)),
    ContDiff.{0, u_1, u_2} ℝ (E := E) (F := F) ∞ (⇑y : (a : E) → F) ∧
      ∀ x ∈ K, dist.{u_2} (α := F) ((y : (a : E) → F) x : F) ((f : (a : E) → F) x : F) < ε

Tactic:
refine ⟨⟨g, hgc.continuous⟩, hgc, fun x hx ↦ (hg _ _ fun y hy ↦ ?_).trans_lt (half_lt_self hε)⟩
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : C(E, F)
K : Set E
ε : ℝ
hK : IsCompact K
hε : 0 < ε
this : UniformContinuousOn.{u_1, u_2} (β := F) (⇑f : (a : E) → F) (cthickening 1 K)
δ : ℝ
hδ : δ > 0
hfδ :
  ∀ x ∈ cthickening 1 K,
    ∀ y ∈ cthickening 1 K,
      dist x y < δ → dist.{u_2} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F) < ε / 2
g : E → F
hgc : ContDiff ℝ ∞ g
hg :
  ∀ (a : E) (δ_1 : ℝ),
    (∀ x ∈ ball a (min 1 δ), dist.{u_2} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) a : F) ≤ δ_1) →
      dist (g a) ((f : (a : E) → F) a) ≤ δ_1
x : E
hx : x ∈ K
y : E
hy : y ∈ ball x (min 1 δ)
⊢ dist y x < 1 ∧ dist y x < δ

Tactic:
rw [mem_ball, lt_min_iff] at hy

Premises used: Metric.mem_ball, lt_min_iff
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : C(E, F)
K : Set E
ε : ℝ
hK : IsCompact K
hε : 0 < ε
this : UniformContinuousOn.{u_1, u_2} (β := F) (⇑f : (a : E) → F) (cthickening 1 K)
δ : ℝ
hδ : δ > 0
hfδ :
  ∀ x ∈ cthickening 1 K,
    ∀ y ∈ cthickening 1 K,
      dist x y < δ → dist.{u_2} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F) < ε / 2
g : E → F
hgc : ContDiff ℝ ∞ g
hg :
  ∀ (a : E) (δ_1 : ℝ),
    (∀ x ∈ ball a (min 1 δ), dist.{u_2} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) a : F) ≤ δ_1) →
      dist (g a) ((f : (a : E) → F) a) ≤ δ_1
x : E
hx : x ∈ K
y : E
hy : dist y x < 1 ∧ dist y x < δ
⊢ dist.{u_2} (α := F) ((f : (a : E) → F) y : F) ((f : (a : E) → F) x : F) ≤ ε / 2

Tactic:
hfδ _ (mem_cthickening_of_dist_le _ x _ _ hx hy.1.le) _
    (self_subset_cthickening _ hx) hy.2 |>.le

Premises used: Metric.mem_cthickening_of_dist_le, LT.lt.le, Metric.self_subset_cthickening, And.right, And.left
-- Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : C(E, F)
K : Set E
ε : ℝ
hK : IsCompact K
hε : 0 < ε
this : UniformContinuousOn.{u_1, u_2} (β := F) (⇑f : (a : E) → F) (cthickening 1 K)
δ : ℝ
hδ : δ > 0
hfδ :
  ∀ x ∈ cthickening 1 K,
    ∀ y ∈ cthickening 1 K,
      dist x y < δ → dist.{u_2} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F) < ε / 2
g : E → F
hgc : ContDiff ℝ ∞ g
hg :
  ∀ (a : E) (δ_1 : ℝ),
    (∀ x ∈ ball a (min 1 δ), dist.{u_2} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) a : F) ≤ δ_1) →
      dist (g a) ((f : (a : E) → F) a) ≤ δ_1
x : E
hx : x ∈ K
y : E
hy : dist y x < 1 ∧ dist y x < δ
⊢ dist.{u_2} (α := F) ((f : (a : E) → F) y : F) ((f : (a : E) → F) x : F) ≤ ε / 2

Tactic:
exact hfδ _ (mem_cthickening_of_dist_le _ x _ _ hx hy.1.le) _
    (self_subset_cthickening _ hx) hy.2 |>.le

Premises used: Metric.mem_cthickening_of_dist_le, LT.lt.le, Metric.self_subset_cthickening, And.right, And.left
-- Module: Mathlib.Analysis.Calculus.Conformal.InnerProduct
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E → F
x : E
rw :
  IsConformalMap (fderiv ℝ f x) ↔
    ∃ (c : ℝ),
      0 < c ∧
        ∀ (u v : E),
          inner.{0, u_2} ℝ (E := F) ((fderiv ℝ f x : (a : E) → F) u : F) ((fderiv ℝ f x : (a : E) → F) v : F) =
            c * ⟪u, v⟫
rw₁ rw₂ :
  (∃ (c : ℝ),
      0 < c ∧
        ∀ (u v : E),
          inner.{0, u_2} ℝ (E := F) ((fderiv ℝ f x : (a : E) → F) u : F) ((fderiv ℝ f x : (a : E) → F) v : F) =
            c * ⟪u, v⟫) ↔
    ∃ (c : ℝ),
      0 < c ∧
        ∀ (u v : E),
          inner.{0, u_2} ℝ (E := F) ((fderiv ℝ f x : (a : E) → F) u : F) ((fderiv ℝ f x : (a : E) → F) v : F) =
            c * ⟪u, v⟫
⊢ ConformalAt f x ↔
    ∃ (c : ℝ),
      0 < c ∧
        ∀ (u v : E),
          inner.{0, u_2} ℝ (E := F) ((fderiv ℝ f x : (a : E) → F) u : F) ((fderiv ℝ f x : (a : E) → F) v : F) =
            c * ⟪u, v⟫

Tactic:
rw [conformalAt_iff_isConformalMap_fderiv, isConformalMap_iff]

Premises used: conformalAt_iff_isConformalMap_fderiv, isConformalMap_iff
-- Module: Mathlib.Analysis.Calculus.Conformal.InnerProduct
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E → F
x : E
f' : E →L[ℝ] F
h : HasFDerivAt f f' x
⊢ ConformalAt f x ↔
    ∃ (c : ℝ),
      0 < c ∧ ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f' : (a : E) → F) u : F) ((f' : (a : E) → F) v : F) = c * ⟪u, v⟫

Tactic:
simp only [conformalAt_iff', h.fderiv]

Premises used: HasFDerivAt.fderiv, conformalAt_iff'
-- Module: Mathlib.Analysis.Calculus.Conformal.InnerProduct
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E → F
x : E
h : ConformalAt f x
⊢ 0 < conformalFactorAt h

Tactic:
(Classical.choose_spec <| conformalAt_iff'.mp h).1

Premises used: Classical.choose_spec, And.left, Iff.mp, conformalFactorAt, conformalAt_iff'
-- Module: Mathlib.Analysis.Calculus.Conformal.InnerProduct
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E → F
x : E
h : ConformalAt f x
u v : E
⊢ inner.{0, u_2} ℝ (E := F) ((fderiv ℝ f x : (a : E) → F) u : F) ((fderiv ℝ f x : (a : E) → F) v : F) =
    conformalFactorAt h * ⟪u, v⟫

Tactic:
(Classical.choose_spec <| conformalAt_iff'.mp h).2 u v

Premises used: Classical.choose_spec, And.right, Iff.mp, conformalFactorAt, conformalAt_iff'
-- Module: Mathlib.Analysis.Calculus.Conformal.InnerProduct
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E → F
x : E
f' : E →L[ℝ] F
h : HasFDerivAt f f' x
H : ConformalAt f x
u v : E
⊢ inner.{0, u_2} ℝ (E := F) ((f' : (a : E) → F) u : F) ((f' : (a : E) → F) v : F) = conformalFactorAt H * ⟪u, v⟫

Tactic:
H.differentiableAt.hasFDerivAt.unique h ▸ conformalFactorAt_inner_eq_mul_inner' H u v

Premises used: ConformalAt.differentiableAt, Eq.rec, conformalFactorAt_inner_eq_mul_inner', DifferentiableAt.hasFDerivAt, HasFDerivAt.unique
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
inst : NormedAddCommGroup X
inst_1 : NormedSpace ℝ X
x : X
⊢ ConformalAt _root_.id x

Tactic:
⟨.id ℝ X, hasFDerivAt_id _, isConformalMap_id⟩

Premises used: Real, hasFDerivAt_id, ContinuousLinearMap.id, And.intro, ConformalAt, isConformalMap_id, Exists.intro
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
inst : NormedAddCommGroup X
inst_1 : NormedSpace ℝ X
c : ℝ
h : c ≠ 0
x : X
⊢ ConformalAt (Y := X) (fun (x' : X) ↦ c • x') x

Tactic:
⟨c • ContinuousLinearMap.id ℝ X, (hasFDerivAt_id x).const_smul c, isConformalMap_const_smul h⟩

Premises used: Real, hasFDerivAt_id, ContinuousLinearMap.id, HasFDerivAt.const_smul, And.intro, ConformalAt, Exists.intro, HSMul.hSMul, isConformalMap_const_smul
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
inst_4 : Subsingleton X
f : X → Y
x : X
⊢ ConformalAt f x

Tactic:
⟨0, hasFDerivAt_of_subsingleton _ _, isConformalMap_of_subsingleton _⟩

Premises used: hasFDerivAt_of_subsingleton, isConformalMap_of_subsingleton, And.intro, ConformalAt, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
mp : ConformalAt f x → IsConformalMap (fderiv ℝ f x)
mpr : IsConformalMap (fderiv ℝ f x) → ConformalAt f x
⊢ ConformalAt f x ↔ IsConformalMap (fderiv ℝ f x)

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
f' : X →L[ℝ] Y
hf : HasFDerivAt f f' x
hf' mp mp₁ mp₂ mp₃ : IsConformalMap f'
⊢ IsConformalMap (fderiv ℝ f x)

Tactic:
rwa [hf.fderiv]

Premises used: HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
pos : ∀ (h : DifferentiableAt ℝ f x), ConformalAt f x
neg : ∀ (h : ¬DifferentiableAt ℝ f x), ConformalAt f x
⊢ ConformalAt f x

Tactic:
by_cases h : DifferentiableAt ℝ f x

Premises used: Real, DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
h : DifferentiableAt ℝ f x
⊢ ConformalAt f x

Tactic:
⟨fderiv ℝ f x, h.hasFDerivAt, H⟩

Premises used: Real, fderiv, DifferentiableAt.hasFDerivAt, And.intro, ConformalAt, Exists.intro
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
h : DifferentiableAt ℝ f x
⊢ ConformalAt f x

Tactic:
exact ⟨fderiv ℝ f x, h.hasFDerivAt, H⟩
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
h : ¬DifferentiableAt ℝ f x
⊢ Nontrivial X

Tactic:
nontriviality X
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
h : ¬DifferentiableAt ℝ f x
h_1 : Nontrivial X
⊢ ConformalAt f x

Tactic:
absurd (fderiv_zero_of_not_differentiableAt h) H.ne_zero

Premises used: IsConformalMap.ne_zero, absurd, fderiv_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
h : ¬DifferentiableAt ℝ f x
h_1 : Nontrivial X
⊢ ConformalAt f x

Tactic:
exact absurd (fderiv_zero_of_not_differentiableAt h) H.ne_zero

Premises used: IsConformalMap.ne_zero, absurd, fderiv_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
h : ConformalAt f x
⊢ DifferentiableAt ℝ f x

Tactic:
let ⟨_, h₁, _⟩ := h
  h₁.differentiableAt

Premises used: Real, DifferentiableAt, _private.0.ConformalAt.differentiableAt.match_1, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f g : X → Y
x : X
u : Set X
hx : x ∈ u
hu : IsOpen u
hf : ConformalAt f x
h : ∀ x ∈ u, g x = f x
⊢ ConformalAt g x

Tactic:
let ⟨f', hfderiv, hf'⟩ := hf
  ⟨f', hfderiv.congr_of_eventuallyEq ((hu.eventually_mem hx).mono h), hf'⟩

Premises used: _private.0.ConformalAt.congr.match_1, IsOpen.eventually_mem, HasFDerivAt.congr_of_eventuallyEq, Filter.Eventually.mono, And.intro, ConformalAt, Exists.intro
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedAddCommGroup Z
inst_3 : NormedSpace ℝ X
inst_4 : NormedSpace ℝ Y
inst_5 : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
hg : ConformalAt g (f x)
hf : ConformalAt f x
rcases : ∀ (f' : X →L[ℝ] Y) (hf₁ : HasFDerivAt f f' x) (cf : IsConformalMap f'), ConformalAt (g ∘ f) x
⊢ ConformalAt (g ∘ f) x

Tactic:
rcases hf with ⟨f', hf₁, cf⟩
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedAddCommGroup Z
inst_3 : NormedSpace ℝ X
inst_4 : NormedSpace ℝ Y
inst_5 : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
hg : ConformalAt g (f x)
f' : X →L[ℝ] Y
hf₁ : HasFDerivAt f f' x
cf : IsConformalMap f'
rcases : ∀ (g' : Y →L[ℝ] Z) (hg₁ : HasFDerivAt g g' (f x)) (cg : IsConformalMap g'), ConformalAt (g ∘ f) x
⊢ ConformalAt (g ∘ f) x

Tactic:
rcases hg with ⟨g', hg₁, cg⟩
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedAddCommGroup Z
inst_3 : NormedSpace ℝ X
inst_4 : NormedSpace ℝ Y
inst_5 : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
f' : X →L[ℝ] Y
hf₁ : HasFDerivAt f f' x
cf : IsConformalMap f'
g' : Y →L[ℝ] Z
hg₁ : HasFDerivAt g g' (f x)
cg : IsConformalMap g'
⊢ ConformalAt (g ∘ f) x

Tactic:
⟨g'.comp f', hg₁.comp x hf₁, cg.comp cf⟩

Premises used: ContinuousLinearMap.comp, And.intro, ConformalAt, Exists.intro, IsConformalMap.comp, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedAddCommGroup Z
inst_3 : NormedSpace ℝ X
inst_4 : NormedSpace ℝ Y
inst_5 : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
f' : X →L[ℝ] Y
hf₁ : HasFDerivAt f f' x
cf : IsConformalMap f'
g' : Y →L[ℝ] Z
hg₁ : HasFDerivAt g g' (f x)
cg : IsConformalMap g'
⊢ ConformalAt (g ∘ f) x

Tactic:
exact ⟨g'.comp f', hg₁.comp x hf₁, cg.comp cf⟩
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
x : X
c : ℝ
hc : c ≠ 0
hf : ConformalAt f x
⊢ ConformalAt (c • f) x

Tactic:
(conformalAt_const_smul hc <| f x).comp x hf

Premises used: conformalAt_const_smul, ConformalAt.comp
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
inst : NormedAddCommGroup X
inst_1 : NormedSpace ℝ X
⊢ Conformal.{u_1, u_1} (X := X) id

Tactic:
fun x => conformalAt_id x

Premises used: conformalAt_id, Conformal
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
inst : NormedAddCommGroup X
inst_1 : NormedSpace ℝ X
c : ℝ
h : c ≠ 0
⊢ Conformal (Y := X) fun (x : X) ↦ c • x

Tactic:
fun x =>
  conformalAt_const_smul h x

Premises used: conformalAt_const_smul, Conformal
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
h : Conformal f
x : X
⊢ ConformalAt f x

Tactic:
h x
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
h : Conformal f
⊢ Differentiable ℝ f

Tactic:
fun x =>
  (h x).differentiableAt

Premises used: ConformalAt.differentiableAt, Differentiable
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedAddCommGroup Z
inst_3 : NormedSpace ℝ X
inst_4 : NormedSpace ℝ Y
inst_5 : NormedSpace ℝ Z
f : X → Y
g : Y → Z
hf : Conformal f
hg : Conformal g
⊢ Conformal (g ∘ f)

Tactic:
fun x => (hg <| f x).comp x (hf x)

Premises used: Conformal, ConformalAt.comp
-- Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace
Goal:
X : Type u_1
Y : Type u_2
inst : NormedAddCommGroup X
inst_1 : NormedAddCommGroup Y
inst_2 : NormedSpace ℝ X
inst_3 : NormedSpace ℝ Y
f : X → Y
hf : Conformal f
c : ℝ
hc : c ≠ 0
⊢ Conformal (c • f)

Tactic:
fun x => (hf x).const_smul hc

Premises used: Conformal, ConformalAt.const_smul