awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
U_1 : Set M
hU : IsOpen[inst_7] U_1
hSig : IsSigmaCompact U_1
hf : LocallyIntegrableOn f U_1 μ
meas_U : MeasurableSet U_1
U : Opens M := { carrier := U_1, is_open' := hU }
this : SigmaCompactSpace.{u_4} ↥U
g : ↥U → ℝ
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
h :
  Eq.{u_2 + 1} (α := F)
    (∫ (x : M) in (↑U : Set M), Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x ∂μ) 0
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ U_1))
      (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ) fun (x : ↥U) ↦ g x • f (↑x : M))
    0
have refine_2 : ∀
  (h :
    Eq.{u_2 + 1} (α := F)
      (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ (↑U : Set M)))
        (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ (↑U : Set M))) μ) fun (x : (↑(↑U : Set M) : Type u_4)) ↦
        Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 (↑x : M) • f (↑x : M))
      0),
  Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ U_1))
      (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ) fun (x : ↥U) ↦ g x • f (↑x : M))
    0
Tactic: rw [← integral_subtype_comap] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
U_1 : Set M
hU : IsOpen[inst_7] U_1
hSig : IsSigmaCompact U_1
hf : LocallyIntegrableOn f U_1 μ
meas_U : MeasurableSet U_1
U : Opens M := { carrier := U_1, is_open' := hU }
this : SigmaCompactSpace.{u_4} ↥U
g : ↥U → ℝ
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
h :
  Eq.{u_2 + 1} (α := F)
    (∫ (x : M) in (↑U : Set M), Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x ∂μ) 0
refine_2 :
  ∀
    (h :
      Eq.{u_2 + 1} (α := F)
        (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ (↑U : Set M)))
          (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ (↑U : Set M))) μ) fun (x : (↑(↑U : Set M) : Type u_4)) ↦
          Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 (↑x : M) • f (↑x : M))
        0),
    Eq.{u_2 + 1} (α := F)
      (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ U_1))
        (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ) fun (x : ↥U) ↦ g x • f (↑x : M))
      0
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ U_1))
      (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ) fun (x : ↥U) ↦ g x • f (↑x : M))
    0
have refine_2₁ : MeasurableSet (↑U : Set M)
Tactic: rw [← integral_subtype_comap] at h
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
U_1 : Set M
hU : IsOpen[inst_7] U_1
hSig : IsSigmaCompact U_1
hf : LocallyIntegrableOn f U_1 μ
meas_U : MeasurableSet U_1
U : Opens M := { carrier := U_1, is_open' := hU }
this : SigmaCompactSpace.{u_4} ↥U
g : ↥U → ℝ
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
h :
  Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ (↑U : Set M)))
      (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ (↑U : Set M))) μ) fun (x : (↑(↑U : Set M) : Type u_4)) ↦
      Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 (↑x : M) • f (↑x : M))
    0
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ U_1))
      (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ) fun (x : ↥U) ↦ g x • f (↑x : M))
    0
have h₁ : Eq.{u_2 + 1} (α := F)
  (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ (↑U : Set M)))
    (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ (↑U : Set M))) μ) fun (x : (↑(↑U : Set M) : Type u_4)) ↦
    g x • f (↑x : M))
  0
Tactic: simp_rw [Subtype.val_injective.extend_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
U_1 : Set M
hU : IsOpen[inst_7] U_1
hSig : IsSigmaCompact U_1
hf : LocallyIntegrableOn f U_1 μ
meas_U : MeasurableSet U_1
U : Opens M := { carrier := U_1, is_open' := hU }
this : SigmaCompactSpace.{u_4} ↥U
g : ↥U → ℝ
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
h : Eq.{u_2 + 1} (α := F) (∫ (x : M), Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x ∂μ) 0
x : M
hx : x ∉ (↑U : Set M)
⊢ Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x = 0
have rw : HSMul.hSMul (α := ℝ) (0 x) (f x) = 0
Tactic: rw [Function.extend_apply' _ _ _ (mt _ hx)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
U_1 : Set M
hU : IsOpen[inst_7] U_1
hSig : IsSigmaCompact U_1
hf : LocallyIntegrableOn f U_1 μ
meas_U : MeasurableSet U_1
U : Opens M := { carrier := U_1, is_open' := hU }
this : SigmaCompactSpace.{u_4} ↥U
g : ↥U → ℝ
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
h : Eq.{u_2 + 1} (α := F) (∫ (x : M), Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x ∂μ) 0
x : M
hx : x ∉ (↑U : Set M)
rw : HSMul.hSMul (α := ℝ) (0 x) (f x) = 0
⊢ Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x = 0
have rw₁ : (∃ (a : ↥U), (↑a : M) = x) → x ∈ (↑U : Set M)
Tactic: rw [Function.extend_apply' _ _ _ (mt _ hx)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
⊢ ∀ᵐ (x : M) ∂μ, (f - f') x = 0
have apply : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • (f - f') x ∂μ) 0
Tactic: apply ae_eq_zero_of_integral_contMDiff_smul_eq_zero I (hf.sub hf')
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
g : M → ℝ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • (f - f') x ∂μ) 0
have simp : Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x - g x • f' x ∂μ) 0
Tactic: simp only [Pi.sub_apply, smul_sub]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
g : M → ℝ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x - g x • f' x ∂μ) 0
have rw : Eq.{u_2 + 1} (α := F) (∫ (a : M), g a • f a ∂μ) (∫ (a : M), g a • f' a ∂μ)
Tactic: rw [integral_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
g : M → ℝ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
rw : Eq.{u_2 + 1} (α := F) (∫ (a : M), g a • f a ∂μ) (∫ (a : M), g a • f' a ∂μ)
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x - g x • f' x ∂μ) 0
have hf₁ : Integrable.{u_2, u_4} (ε := F) (fun (x : M) ↦ g x • f x) μ
Tactic: rw [integral_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
g : M → ℝ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
rw : Eq.{u_2 + 1} (α := F) (∫ (a : M), g a • f a ∂μ) (∫ (a : M), g a • f' a ∂μ)
hf₁ : Integrable.{u_2, u_4} (ε := F) (fun (x : M) ↦ g x • f x) μ
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x - g x • f' x ∂μ) 0
have hg : Integrable.{u_2, u_4} (ε := F) (fun (x : M) ↦ g x • f' x) μ
Tactic: rw [integral_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
⊢ ∀ᵐ (x : M) ∂μ, f x = f' x
have this : ∀ᵐ (x : M) ∂μ, (f - f') x = 0
Tactic: have : ∀ᵐ x ∂μ, (f - f') x = 0 := by
    apply ae_eq_zero_of_integral_contMDiff_smul_eq_zero I (hf.sub hf')
    intro g g_diff g_supp
    simp only [Pi.sub_apply, smul_sub]
    rw [integral_sub, sub_eq_zero]
    · exact h g g_diff g_supp
    · exact hf.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
    · exact hf'.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
this : ∀ᵐ (x : M) ∂μ, (f - f') x = 0
⊢ ∀ᵐ (x : M) ∂μ, f x = f' x
have h₁ : ∀ (x : M) (hx : (f - f') x = 0), f x = f' x
Tactic: filter_upwards [this] with x hx
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (hypothesis)
Goal:
𝕜 : Type u_1
E_1 : Type u_2
F_1 : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace ℝ E_1
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : NormedSpace 𝕜 F_1
inst_6 : SMulCommClass ℝ 𝕜 F_1
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n_1 n₁ n₂ k : ℕ∞
K_1 K₁ K₂ : Compacts E_1
B : Type u_5
E : Type u_6
F : Type u_7
inst_11 : NormedAddCommGroup E
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace ℝ E
inst_14 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
inst_15 : ContDiffMapSupportedInClass B E F n K
f : B
⊢ ∃ (C : ℝ), ∀ (x y : E), dist ((f : (a : E) → F) x) ((f : (a : E) → F) y) ≤ C
have this : HasCompactSupport (⇑f : (a : E) → F)
Tactic: have := HasCompactSupport.intro K.isCompact (map_zero_on_compl f)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E_1 : Type u_2
F_1 : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace ℝ E_1
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : NormedSpace 𝕜 F_1
inst_6 : SMulCommClass ℝ 𝕜 F_1
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n_1 n₁ n₂ k : ℕ∞
K_1 K₁ K₂ : Compacts E_1
B : Type u_5
E : Type u_6
F : Type u_7
inst_11 : NormedAddCommGroup E
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace ℝ E
inst_14 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
inst_15 : ContDiffMapSupportedInClass B E F n K
f : B
this : HasCompactSupport (⇑f : (a : E) → F)
⊢ ∃ (C : ℝ), ∀ (x y : E), dist ((f : (a : E) → F) x) ((f : (a : E) → F) y) ≤ C
have rcases : ∀ (C : ℝ) (hC : ∀ (x : E), ‖(f : (a : E) → F) x‖ ≤ C),
  ∃ (C : ℝ), ∀ (x y : E), dist ((f : (a : E) → F) x) ((f : (a : E) → F) y) ≤ C
Tactic: rcases (map_continuous f).bounded_above_of_compact_support this with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
h : Eq (α := (a : E) → F) ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun) f) ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun) g)
⊢ f = g
have mk : ∀ (toFun : E → F) (contDiff' : ContDiff ℝ (↑n : ℕ∞ω) toFun) (zero_on_compl' : EqOn toFun 0 (↑K : Set E)ᶜ)
  (h :
    Eq (α := (a : E) → F)
      ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun)
        { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' })
      ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun) g)),
  { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' : 𝓓^{n}_{K}(E, F) } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
g : 𝓓^{n}_{K}(E, F)
toFun : E → F
contDiff' : ContDiff ℝ (↑n : ℕ∞ω) toFun
zero_on_compl' : EqOn toFun 0 (↑K : Set E)ᶜ
h :
  Eq (α := (a : E) → F)
    ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun) { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' })
    ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun) g)
⊢ { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' : 𝓓^{n}_{K}(E, F) } = g
have mk : ∀ (toFun_1 : E → F) (contDiff'_1 : ContDiff ℝ (↑n : ℕ∞ω) toFun_1) (zero_on_compl'_1 : EqOn toFun_1 0 (↑K : Set E)ᶜ)
  (h :
    Eq (α := (a : E) → F)
      ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun)
        { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' })
      ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun)
        { toFun := toFun_1, contDiff' := contDiff'_1, zero_on_compl' := zero_on_compl'_1 })),
  { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' : 𝓓^{n}_{K}(E, F) } =
    { toFun := toFun_1, contDiff' := contDiff'_1, zero_on_compl' := zero_on_compl'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
⊢ EqOn ((⇑f : (a : E) → F) + (⇑g : (a : E) → F)) 0 (↑K : Set E)ᶜ
have rw : EqOn ((⇑f : (a : E) → F) + (⇑g : (a : E) → F)) (HAdd.hAdd (α := E → F) 0 0) (↑K : Set E)ᶜ
Tactic: rw [← add_zero 0]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ EqOn (-(⇑f : (a : E) → F)) 0 (↑K : Set E)ᶜ
have rw : EqOn (-(⇑f : (a : E) → F)) (-0) (↑K : Set E)ᶜ
Tactic: rw [← neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
⊢ EqOn ((⇑f : (a : E) → F) - (⇑g : (a : E) → F)) 0 (↑K : Set E)ᶜ
have rw : EqOn ((⇑f : (a : E) → F) - (⇑g : (a : E) → F)) (HSub.hSub (α := E → F) 0 0) (↑K : Set E)ᶜ
Tactic: rw [← sub_zero 0]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
R : Type u_5
inst_11 : Semiring R
inst_12 : Module R F
inst_13 : SMulCommClass ℝ R F
inst_14 : ContinuousConstSMul R F
c : R
f : 𝓓^{n}_{K}(E, F)
⊢ EqOn (c • (⇑f : (a : E) → F)) 0 (↑K : Set E)ᶜ
have rw : EqOn (c • (⇑f : (a : E) → F)) (HSMul.hSMul (β := E → F) c 0) (↑K : Set E)ᶜ
Tactic: rw [← smul_zero c]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
⊢ Injective (α := 𝓓^{n}_{K}(E, F)) (β := E → F) (⇑(coeHom E F n K) : (a : 𝓓^{n}_{K}(E, F)) → E → F)
have rw : Injective (α := 𝓓^{n}_{K}(E, F)) (DFunLike.coe (β := fun (a : E) ↦ F))
Tactic: rw [coe_coeHom]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
i : ℕ
x : E
⊢ x ∈ (↑K : Set E)ᶜ →
    Eq (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
      (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) (0 x)
have x₁ : ∀ (hx : x ∉ K),
  Eq (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
    (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) (0 x)
Tactic: (hx : x ∉ K)