awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
x : E
hx : x ∉ closedBall c f.rOut
⊢ (↑f : E → ℝ) x = 0
have apply : f.rOut < dist x c
Tactic: apply f.zero_of_le_dist (le_of_lt _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
⊢ LE.le (α := ℝ) (∫ (x : E) in closedBall c f.rOut, (↑f : E → ℝ) x ∂μ) (∫ (x : E) in closedBall c f.rOut, 1 ∂μ)
have apply : IntegrableOn (ε := ℝ) (fun (x : E) ↦ 1) (closedBall c f.rOut) μ
Tactic: apply setIntegral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
⊢ ∫ (x : E), (↑f : E → ℝ) x ∂μ ≤ μ.real (closedBall c f.rOut)
have f₁ : Eq (α := ℝ) (∫ (x : E), (↑f : E → ℝ) x ∂μ) (∫ (x : E) in closedBall c f.rOut, (↑f : E → ℝ) x ∂μ)
Tactic: calc
  ∫ x, f x ∂μ = ∫ x in closedBall c f.rOut, f x ∂μ := by
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
    apply f.zero_of_le_dist (le_of_lt _)
    simpa using hx
  _ ≤ ∫ x in closedBall c f.rOut, 1 ∂μ := by
    apply setIntegral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)
    simp [measure_closedBall_lt_top]
  _ = μ.real (closedBall c f.rOut) := by simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
f₁ : Eq (α := ℝ) (∫ (x : E), (↑f : E → ℝ) x ∂μ) (∫ (x : E) in closedBall c f.rOut, (↑f : E → ℝ) x ∂μ)
⊢ ∫ (x : E), (↑f : E → ℝ) x ∂μ ≤ μ.real (closedBall c f.rOut)
have f₂ : LE.le (α := ℝ) (∫ (x : E) in closedBall c f.rOut, (↑f : E → ℝ) x ∂μ) (∫ (x : E) in closedBall c f.rOut, 1 ∂μ)
Tactic: calc
  ∫ x, f x ∂μ = ∫ x in closedBall c f.rOut, f x ∂μ := by
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
    apply f.zero_of_le_dist (le_of_lt _)
    simpa using hx
  _ ≤ ∫ x in closedBall c f.rOut, 1 ∂μ := by
    apply setIntegral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)
    simp [measure_closedBall_lt_top]
  _ = μ.real (closedBall c f.rOut) := by simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
f₁ : Eq (α := ℝ) (∫ (x : E), (↑f : E → ℝ) x ∂μ) (∫ (x : E) in closedBall c f.rOut, (↑f : E → ℝ) x ∂μ)
f₂ : LE.le (α := ℝ) (∫ (x : E) in closedBall c f.rOut, (↑f : E → ℝ) x ∂μ) (∫ (x : E) in closedBall c f.rOut, 1 ∂μ)
⊢ ∫ (x : E), (↑f : E → ℝ) x ∂μ ≤ μ.real (closedBall c f.rOut)
have f₃ : ∫ (x : E) in closedBall c f.rOut, 1 ∂μ = μ.real (closedBall c f.rOut)
Tactic: calc
  ∫ x, f x ∂μ = ∫ x in closedBall c f.rOut, f x ∂μ := by
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
    apply f.zero_of_le_dist (le_of_lt _)
    simpa using hx
  _ ≤ ∫ x in closedBall c f.rOut, 1 ∂μ := by
    apply setIntegral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)
    simp [measure_closedBall_lt_top]
  _ = μ.real (closedBall c f.rOut) := by simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
⊢ μ.real (closedBall c f.rOut) / K ^ finrank ℝ E ≤ ∫ (x : E), (↑f : E → ℝ) x ∂μ
have K_pos : 0 < K
Tactic: have K_pos : 0 < K := by
    simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ μ.real (closedBall c f.rOut) / K ^ finrank ℝ E ≤ ∫ (x : E), (↑f : E → ℝ) x ∂μ
have apply : μ.real (closedBall c f.rOut) / K ^ finrank ℝ E ≤ μ.real (closedBall c f.rIn)
Tactic: apply le_trans _ (f.measure_closedBall_le_integral μ)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ μ.real (closedBall c f.rOut) / K ^ finrank ℝ E ≤ μ.real (closedBall c f.rIn)
have rw : f.rOut ^ finrank ℝ E * μ.real (closedBall 0 1) ≤ (K * f.rIn) ^ finrank ℝ E * μ.real (closedBall 0 1)
Tactic: rw [div_le_iff₀ (pow_pos K_pos _), addHaar_real_closedBall' _ _ f.rIn_pos.le,
    addHaar_real_closedBall' _ _ f.rOut_pos.le, mul_assoc, mul_comm _ (K ^ _), ← mul_assoc,
    ← mul_pow, mul_comm _ K]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ f.rOut ^ finrank ℝ E * μ.real (closedBall 0 1) ≤ (K * f.rIn) ^ finrank ℝ E * μ.real (closedBall 0 1)
have hbc : 0 ≤ f.rOut
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
⊢ f.normed μ x ≤ K ^ finrank ℝ E / μ.real (closedBall c f.rOut)
have K_pos : 0 < K
Tactic: have K_pos : 0 < K := by
    simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ (↑f : E → ℝ) x / ∫ (y : E), (↑f : E → ℝ) y ∂μ ≤ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
have hc : LE.le (α := ℝ) 0 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
hc : LE.le (α := ℝ) 0 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
⊢ (↑f : E → ℝ) x / ∫ (y : E), (↑f : E → ℝ) y ∂μ ≤ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
have hab : (↑f : E → ℝ) x ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
⊢ f.normed μ x ≤ K ^ finrank ℝ E / μ.real (closedBall c f.rOut)
have this : (↑f : E → ℝ) x / ∫ (y : E), (↑f : E → ℝ) y ∂μ ≤ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
Tactic: have : f x / ∫ y, f y ∂μ ≤ 1 / ∫ y, f y ∂μ := by
    gcongr
    · exact f.integral_pos.le
    · exact f.le_one
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : (↑f : E → ℝ) x / ∫ (y : E), (↑f : E → ℝ) y ∂μ ≤ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
⊢ f.normed μ x ≤ K ^ finrank ℝ E / μ.real (closedBall c f.rOut)
have apply : HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ) ≤ K ^ finrank ℝ E / μ.real (closedBall c f.rOut)
Tactic: apply this.trans
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : (↑f : E → ℝ) x / ∫ (y : E), (↑f : E → ℝ) y ∂μ ≤ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
⊢ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ) ≤ K ^ finrank ℝ E / μ.real (closedBall c f.rOut)
have rw : μ.real (closedBall c f.rOut) / K ^ finrank ℝ E ≤ ∫ (x : E), (↑f : E → ℝ) x ∂μ
Tactic: rw [div_le_div_iff₀ f.integral_pos, one_mul, ← div_le_iff₀' (pow_pos K_pos _)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Normed (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
x : E
K_pos : 0 < K
this : (↑f : E → ℝ) x / ∫ (y : E), (↑f : E → ℝ) y ∂μ ≤ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ)
rw : μ.real (closedBall c f.rOut) / K ^ finrank ℝ E ≤ ∫ (x : E), (↑f : E → ℝ) x ∂μ
⊢ HDiv.hDiv (α := ℝ) 1 (∫ (y : E), (↑f : E → ℝ) y ∂μ) ≤ K ^ finrank ℝ E / μ.real (closedBall c f.rOut)
have rw₁ : 0 < μ.real (closedBall c f.rOut)
Tactic: rw [div_le_div_iff₀ f.integral_pos, one_mul, ← div_le_iff₀' (pow_pos K_pos _)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox (goal)
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 : E → F
ε : ℝ
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
μ : Measure E
inst_8 : μ.IsAddHaarMeasure
hf : LocallyIntegrable f μ
hε : 0 < ε
φ : ContDiffBump.{u_1} (E := E) 0 := { rIn := ε / 2, rOut := ε, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
⊢ ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E) (δ : ℝ), (∀ x ∈ ball a ε, dist (f x) (f a) ≤ δ) → dist (g a) (f a) ≤ δ
have refine : ContDiff.{0, u_1, u_2} ℝ (F := F) ∞ fun (a : E) ↦ convolution (φ.normed μ) f (ContinuousLinearMap.lsmul ℝ ℝ) μ a
Tactic: refine ⟨_, ?_, fun a δ ↦ φ.dist_normed_convolution_le hf.aestronglyMeasurable⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox (hypothesis)
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 : E → F
ε : ℝ
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hε : 0 < ε
⊢ ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E) (δ : ℝ), (∀ x ∈ ball a ε, dist (f x) (f a) ≤ δ) → dist (g a) (f a) ≤ δ
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox (goal)
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 : E → F
ε : ℝ
hf : UniformContinuous f
hε : 0 < ε
⊢ ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E), dist (g a) (f a) < ε
have rcases : ∀ (δ : ℝ) (hδ : δ > 0) (hfδ : ∀ ⦃a b : E⦄, dist a b < δ → dist (f a) (f b) < ε / 2),
  ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E), dist (g a) (f a) < ε
Tactic: rcases Metric.uniformContinuous_iff.mp hf (ε / 2) (half_pos hε) with ⟨δ, hδ, hfδ⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox (goal)
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 : E → F
ε : ℝ
hf : UniformContinuous f
hε : 0 < ε
δ : ℝ
hδ : δ > 0
hfδ : ∀ ⦃a b : E⦄, dist a b < δ → dist (f a) (f b) < ε / 2
⊢ ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E), dist (g a) (f a) < ε
have rcases : ∀ (g : E → F) (hgc : ContDiff ℝ ∞ g)
  (hg : ∀ (a : E) (δ_1 : ℝ), (∀ x ∈ ball a δ, dist (f x) (f a) ≤ δ_1) → dist (g a) (f a) ≤ δ_1),
  ∃ (g : E → F), ContDiff ℝ ∞ g ∧ ∀ (a : E), dist (g a) (f a) < ε
Tactic: rcases hf.continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le hδ with ⟨g, hgc, hg⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox (goal)
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)
⊢ Membership.mem (γ := Set C(E, F))
    (closure {f : C(E, F) | ContDiff.{0, u_1, u_2} ℝ (E := E) (F := F) ∞ (⇑f : (a : E) → F)}) f
have rw : ∀ (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: rw [mem_closure_iff_nhds_basis
    (nhds_basis_uniformity uniformity_basis_dist.compactConvergenceUniformity)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox (goal)
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)
⊢ ∀ (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
have 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
Tactic: simp only [Prod.forall, mem_setOf_eq, and_imp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox (hypothesis)
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 < ε
⊢ ∃ (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) < ε
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox (goal)
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)
⊢ ∃ (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) < ε
have 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) < ε
Tactic: rcases Metric.uniformContinuousOn_iff.mp this (ε / 2) (half_pos hε) with ⟨δ, hδ, hfδ⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox (goal)
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
⊢ ∃ (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) < ε
have 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) < ε
Tactic: rcases (map_continuous f).exists_contDiff_dist_le_of_forall_mem_ball_dist_le
    (lt_min one_pos hδ) with ⟨g, hgc, hg⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox (goal)
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) < ε
have 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
Tactic: refine ⟨⟨g, hgc.continuous⟩, hgc, fun x hx ↦ (hg _ _ fun y hy ↦ ?_).trans_lt (half_lt_self hε)⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox (hypothesis)
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.{u_2} (α := F) ((f : (a : E) → F) y : F) ((f : (a : E) → F) x : F) ≤ ε / 2
have hy₁ : dist y x < 1 ∧ dist y x < δ
Tactic: rw [mem_ball, lt_min_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Conformal.InnerProduct (goal)
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
⊢ 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⟫
have 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⟫
Tactic: rw [conformalAt_iff_isConformalMap_fderiv, isConformalMap_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Conformal.InnerProduct (goal)
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⟫
⊢ 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⟫
have 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⟫
Tactic: rw [conformalAt_iff_isConformalMap_fderiv, isConformalMap_iff]