harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem uniqueMDiffWithinAt_univ : UniqueMDiffWithinAt I univ x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
⊢ UniqueDiffWithinAt 𝕜 (range ↑I) (↑(extChartAt I x) x)

Tactic:
exact I.uniqueDiffOn _ (mem_range_self _)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
⊢ UniqueMDiffWithinAt I univ x

Tactic:
unfold UniqueMDiffWithinAt

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
⊢ UniqueDiffWithinAt 𝕜 (↑(extChartAt I x).symm ⁻¹' univ ∩ range ↑I) (↑(extChartAt I x) x)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
⊢ UniqueDiffWithinAt 𝕜 (↑(extChartAt I x).symm ⁻¹' univ ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
simp only [preimage_univ, univ_inter]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
⊢ UniqueDiffWithinAt 𝕜 (range ↑I) (↑(extChartAt I x) x)
-- Mathlib/Data/List/Sublists.lean
theorem mem_sublistsLen_self {l l' : List α} (h : l' <+ l) :
    l' ∈ sublistsLen (length l') l

Proof state:
case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (b :: l₁).length (a :: l₂)

Tactic:
rw [length, sublistsLen_succ_cons]

Result:
case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)

Proof state:
α : Type u
l l' : List α
h : l' <+ l
⊢ l' ∈ sublistsLen l'.length l

Tactic:
induction' h with l₁ l₂ a s IH l₁ l₂ a s IH

Result:
case slnil
α : Type u
l l' : List α
⊢ [] ∈ sublistsLen [].length []

case cons
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
⊢ l₁ ∈ sublistsLen l₁.length (a :: l₂)

case cons₂
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
⊢ a :: l₁ ∈ sublistsLen (a :: l₁).length (a :: l₂)

Proof state:
case cons₂
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
⊢ a :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)

Tactic:
exact mem_append_right _ (mem_map.2 ⟨_, IH, rfl⟩)

Result:
no goals

Proof state:
case cons₂
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
⊢ a :: l₁ ∈ sublistsLen (a :: l₁).length (a :: l₂)

Tactic:
rw [length, sublistsLen_succ_cons]

Result:
case cons₂
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
⊢ a :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)

Proof state:
case cons.nil
α : Type u
l l' l₂ : List α
a : α
s : [] <+ l₂
IH : [] ∈ sublistsLen [].length l₂
⊢ [] ∈ sublistsLen [].length (a :: l₂)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
⊢ l₁ ∈ sublistsLen l₁.length (a :: l₂)

Tactic:
rcases l₁ with - | ⟨b, l₁⟩

Result:
case cons.nil
α : Type u
l l' l₂ : List α
a : α
s : [] <+ l₂
IH : [] ∈ sublistsLen [].length l₂
⊢ [] ∈ sublistsLen [].length (a :: l₂)

case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (b :: l₁).length (a :: l₂)

Proof state:
case slnil
α : Type u
l l' : List α
⊢ [] ∈ sublistsLen [].length []

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)

Tactic:
exact mem_append_left _ IH

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem integrable_rnDeriv (s : SignedMeasure α) (μ : Measure α) : Integrable (rnDeriv s μ) μ

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Integrable (fun x => (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ

Tactic:
constructor

Result:
case refine_2.left
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ AEStronglyMeasurable (fun x => (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ

case refine_2.right
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ HasFiniteIntegral (fun x => (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ

Proof state:
case refine_2.left
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ AEStronglyMeasurable (fun x => (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ

Tactic:
apply Measurable.aestronglyMeasurable

Result:
case refine_2.left.hf
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Measurable fun x => (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal

Proof state:
case refine_2.right
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ HasFiniteIntegral (fun x => (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ

Tactic:
exact hasFiniteIntegral_toReal_of_lintegral_ne_top (lintegral_rnDeriv_lt_top _ μ).ne

Result:
no goals

Proof state:
case refine_2.left.hf
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Measurable fun x => (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Data/Finsupp/BigOperators.lean
theorem List.support_sum_eq [AddMonoid M] (l : List (ι →₀ M))
    (hl : l.Pairwise (_root_.Disjoint on Finsupp.support)) :
    l.sum.support = l.foldr (Finsupp.support · ⊔ ·) ∅

Proof state:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
f : Finset ι
hf : f ∈ (map Finsupp.support tl).toFinset
⊢ _root_.Disjoint hd.support (id f)

Tactic:
simp only [List.mem_toFinset, List.mem_map] at hf

Result:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
f : Finset ι
hf : ∃ a ∈ tl, a.support = f
⊢ _root_.Disjoint hd.support (id f)

Proof state:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ _root_.Disjoint hd.support (foldr (fun x y => x.support ⊔ y) ∅ tl)

Tactic:
rw [← List.foldr_map, ← Finset.bot_eq_empty, List.foldr_sup_eq_sup_toFinset,
  Finset.disjoint_sup_right]

Result:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ ∀ ⦃i : Finset ι⦄, i ∈ (map Finsupp.support tl).toFinset → _root_.Disjoint hd.support (id i)
-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem of_s_head (h : fract v ≠ 0) : (of v).s.head = some ⟨1, ⌊(fract v)⁻¹⌋⟩

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : fract v ≠ 0
⊢ (some ∘ fun p => { a := 1, b := ↑p.b }) (IntFractPair.of (IntFractPair.of v).fr⁻¹) =
    some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : fract v ≠ 0
⊢ (of v).s.head = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }

Tactic:
change (of v).s.get? 0 = _

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : fract v ≠ 0
⊢ (of v).s.get? 0 = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : fract v ≠ 0
⊢ (of v).s.get? 0 = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }

Tactic:
rw [of_s_head_aux, stream_succ_of_some (stream_zero v) h, Option.bind]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : fract v ≠ 0
⊢ (some ∘ fun p => { a := 1, b := ↑p.b }) (IntFractPair.of (IntFractPair.of v).fr⁻¹) =
    some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
-- Mathlib/Probability/Kernel/RadonNikodym.lean
/-- For two kernels `κ, η`, the singular part of `κ a` with respect to `η a` is a measurable
function of `a`. -/
lemma measurable_singularPart (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] :
    Measurable (fun a ↦ (κ a).singularPart (η a))

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ Measurable fun a => (κ a).singularPart (η a)

Tactic:
refine Measure.measurable_of_measurable_coe _ (fun s hs ↦ ?_)

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
s : Set γ
hs : MeasurableSet s
⊢ Measurable fun b => ((κ b).singularPart (η b)) s

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
s : Set γ
hs : MeasurableSet s
⊢ Measurable fun b => ((κ b).singularPart (η b)) s

Tactic:
simp_rw [← κ.singularPart_eq_singularPart_measure, κ.singularPart_def η]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
s : Set γ
hs : MeasurableSet s
⊢ Measurable fun b =>
    (((κ + η).withDensity fun a x =>
          ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x)
        b)
      s

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
s : Set γ
hs : MeasurableSet s
⊢ Measurable fun b =>
    (((κ + η).withDensity fun a x =>
          ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x)
        b)
      s

Tactic:
exact Kernel.measurable_coe _ hs

Result:
no goals
-- Mathlib/Probability/ConditionalProbability.lean
theorem cond_apply (hms : MeasurableSet s) (μ : Measure Ω) (t : Set Ω) :
    μ[t|s] = (μ s)⁻¹ * μ (s ∩ t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
μ : Measure Ω
t : Set Ω
⊢ μ[t | s] = (μ s)⁻¹ * μ (s ∩ t)

Tactic:
rw [cond, Measure.smul_apply, Measure.restrict_apply' hms, Set.inter_comm, smul_eq_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem dirac_prod (x : α) : (dirac x).prod ν = map (Prod.mk x) ν

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
⊢ (dirac x).prod ν = map (Prod.mk x) ν

Tactic:
rw [← sum_sfiniteSeq ν, prod_sum_right, map_sum measurable_prod_mk_left.aemeasurable]

Result:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
⊢ (sum fun p => (dirac x).prod (sfiniteSeq ν p)) = sum fun i => map (Prod.mk x) (sfiniteSeq ν i)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
⊢ (dirac x).prod ν = map (Prod.mk x) ν

Tactic:
classical
rw [← sum_sfiniteSeq ν, prod_sum_right, map_sum measurable_prod_mk_left.aemeasurable]
congr
ext1 i
refine prod_eq fun s t hs ht => ?_
simp_rw [map_apply measurable_prod_mk_left (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if,
  dirac_apply' _ hs, ← indicator_mul_left _ _ fun _ => sfiniteSeq ν i t, Pi.one_apply, one_mul]

Result:
no goals

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (map (Prod.mk x) (sfiniteSeq ν i)) (s ×ˢ t) = (dirac x) s * (sfiniteSeq ν i) t

Tactic:
simp_rw [map_apply measurable_prod_mk_left (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if,
  dirac_apply' _ hs, ← indicator_mul_left _ _ fun _ => sfiniteSeq ν i t, Pi.one_apply, one_mul]

Result:
no goals

Proof state:
case e_f
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
⊢ (fun p => (dirac x).prod (sfiniteSeq ν p)) = fun i => map (Prod.mk x) (sfiniteSeq ν i)

Tactic:
ext1 i

Result:
case e_f.h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
i : ℕ
⊢ (dirac x).prod (sfiniteSeq ν i) = map (Prod.mk x) (sfiniteSeq ν i)

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
i : ℕ
⊢ (dirac x).prod (sfiniteSeq ν i) = map (Prod.mk x) (sfiniteSeq ν i)

Tactic:
refine prod_eq fun s t hs ht => ?_

Result:
case e_f.h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (map (Prod.mk x) (sfiniteSeq ν i)) (s ×ˢ t) = (dirac x) s * (sfiniteSeq ν i) t

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
⊢ (sum fun p => (dirac x).prod (sfiniteSeq ν p)) = sum fun i => map (Prod.mk x) (sfiniteSeq ν i)

Tactic:
congr

Result:
case e_f
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
⊢ (fun p => (dirac x).prod (sfiniteSeq ν p)) = fun i => map (Prod.mk x) (sfiniteSeq ν i)
-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux {Du Eu Fu Gu : Type u}
    [NormedAddCommGroup Du] [NormedSpace 𝕜 Du] [NormedAddCommGroup Eu] [NormedSpace 𝕜 Eu]
    [NormedAddCommGroup Fu] [NormedSpace 𝕜 Fu] [NormedAddCommGroup Gu] [NormedSpace 𝕜 Gu]
    (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} {n : ℕ} {s : Set Du} {x : Du}
    (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    ‖iteratedFDerivWithin 𝕜 n (fun y => B (f y) (g y)) s x‖ ≤
      ‖B‖ * ∑ i ∈ Finset.range (n + 1), (n.choose i : ℝ) * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
Du : Type u
inst✝⁷ : NormedAddCommGroup Du
inst✝⁶ : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst : NormedAddCommGroup Eu] [inst_1 : NormedSpace 𝕜 Eu] [inst_2 : NormedAddCommGroup Fu]
    [inst_3 : NormedSpace 𝕜 Fu] [inst_4 : NormedAddCommGroup Gu] [inst_5 : NormedSpace 𝕜 Gu] (B : Eu →L[𝕜] Fu →L[𝕜] Gu)
    {f : Du → Eu} {g : Du → Fu},
    ContDiffOn 𝕜 (↑n) f s →
      ContDiffOn 𝕜 (↑n) g s →
        ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤
          ‖B‖ *
            ∑ i ∈ Finset.range (n + 1),
              ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
Eu Fu Gu : Type u
inst✝⁵ : NormedAddCommGroup Eu
inst✝⁴ : NormedSpace 𝕜 Eu
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hg : ContDiffOn 𝕜 (↑(n + 1)) g s
In : ↑n + 1 ≤ ↑n.succ
norm✝ : Norm (Eu →L[𝕜] (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) := hasOpNorm
I1 :
  ‖iteratedFDerivWithin 𝕜 n (fun y => ((precompR Du B) (f y)) (fderivWithin 𝕜 g s y)) s x‖ ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n + 1 - i) g s x‖
norm : Norm ((Du →L[𝕜] Eu) →L[𝕜] Fu →L[𝕜] Du →L[𝕜] Gu) := hasOpNorm
i : ℕ
x✝ : i ∈ Finset.range (n + 1)
⊢ ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 f s) s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖ =
    ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 (i + 1) f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖

Tactic:
rw [← norm_iteratedFDerivWithin_fderivWithin hs hx]

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
Du : Type u
inst✝⁷ : NormedAddCommGroup Du
inst✝⁶ : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
Eu Fu Gu : Type u
inst✝⁵ : NormedAddCommGroup Eu
inst✝⁴ : NormedSpace 𝕜 Eu
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑0) f s
hg : ContDiffOn 𝕜 (↑0) g s
⊢ ‖(B (f x)) (g x)‖ ≤ ‖B‖ * ‖f x‖ * ‖g x‖

Tactic:
apply B.le_opNorm₂

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux {Du Eu Fu Gu : Type u}
    [NormedAddCommGroup Du] [NormedSpace 𝕜 Du] [NormedAddCommGroup Eu] [NormedSpace 𝕜 Eu]
    [NormedAddCommGroup Fu] [NormedSpace 𝕜 Fu] [NormedAddCommGroup Gu] [NormedSpace 𝕜 Gu]
    (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} {n : ℕ} {s : Set Du} {x : Du}
    (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    ‖iteratedFDerivWithin 𝕜 n (fun y => B (f y) (g y)) s x‖ ≤
      ‖B‖ * ∑ i ∈ Finset.range (n + 1), (n.choose i : ℝ) * ‖iteratedFDerivWithin 𝕜 i f s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
Du : Type u
inst✝⁷ : NormedAddCommGroup Du
inst✝⁶ : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst : NormedAddCommGroup Eu] [inst_1 : NormedSpace 𝕜 Eu] [inst_2 : NormedAddCommGroup Fu]
    [inst_3 : NormedSpace 𝕜 Fu] [inst_4 : NormedAddCommGroup Gu] [inst_5 : NormedSpace 𝕜 Gu] (B : Eu →L[𝕜] Fu →L[𝕜] Gu)
    {f : Du → Eu} {g : Du → Fu},
    ContDiffOn 𝕜 (↑n) f s →
      ContDiffOn 𝕜 (↑n) g s →
        ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤
          ‖B‖ *
            ∑ i ∈ Finset.range (n + 1),
              ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
Eu Fu Gu : Type u
inst✝⁵ : NormedAddCommGroup Eu
inst✝⁴ : NormedSpace 𝕜 Eu
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hg : ContDiffOn 𝕜 (↑(n + 1)) g s
In : ↑n + 1 ≤ ↑n.succ
norm : Norm (Eu →L[𝕜] (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) := hasOpNorm
⊢ 0 ≤
    ∑ i ∈ Finset.range (n + 1),
      ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x‖

Tactic:
positivity

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
theorem singletonSubgraph_connected {v : V} : (G.singletonSubgraph v).Connected

Proof state:
case mk.mk
V : Type u
G : SimpleGraph V
b : V
ha hb : b = b
⊢ (G.singletonSubgraph b).coe.Reachable ⟨b, ⋯⟩ ⟨b, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mk
V : Type u
G : SimpleGraph V
v a : V
ha : a ∈ (G.singletonSubgraph v).verts
b : V
hb : b ∈ (G.singletonSubgraph v).verts
⊢ (G.singletonSubgraph v).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
simp only [singletonSubgraph_verts, Set.mem_singleton_iff] at ha hb

Result:
case mk.mk
V : Type u
G : SimpleGraph V
v a : V
ha✝ : a ∈ (G.singletonSubgraph v).verts
b : V
hb✝ : b ∈ (G.singletonSubgraph v).verts
ha : a = v
hb : b = v
⊢ (G.singletonSubgraph v).coe.Reachable ⟨a, ha✝⟩ ⟨b, hb✝⟩

Proof state:
V : Type u
G : SimpleGraph V
v : V
⊢ (G.singletonSubgraph v).coe.Preconnected

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Result:
case mk.mk
V : Type u
G : SimpleGraph V
v a : V
ha : a ∈ (G.singletonSubgraph v).verts
b : V
hb : b ∈ (G.singletonSubgraph v).verts
⊢ (G.singletonSubgraph v).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩

Proof state:
case mk.mk
V : Type u
G : SimpleGraph V
v a : V
ha✝ : a ∈ (G.singletonSubgraph v).verts
b : V
hb✝ : b ∈ (G.singletonSubgraph v).verts
ha : a = v
hb : b = v
⊢ (G.singletonSubgraph v).coe.Reachable ⟨a, ha✝⟩ ⟨b, hb✝⟩

Tactic:
subst_vars

Result:
case mk.mk
V : Type u
G : SimpleGraph V
b : V
ha hb : b = b
⊢ (G.singletonSubgraph b).coe.Reachable ⟨b, ⋯⟩ ⟨b, ⋯⟩

Proof state:
V : Type u
G : SimpleGraph V
v : V
⊢ (G.singletonSubgraph v).Connected

Tactic:
refine ⟨⟨?_⟩⟩

Result:
V : Type u
G : SimpleGraph V
v : V
⊢ (G.singletonSubgraph v).coe.Preconnected
-- Mathlib/MeasureTheory/Constructions/Projective.lean
lemma congr_cylinder (hP : IsProjectiveMeasureFamily P)
    {S : Set (∀ i : I, α i)} {T : Set (∀ i : J, α i)} (hS : MeasurableSet S) (hT : MeasurableSet T)
    (h_eq : cylinder I S = cylinder J T) :
    P I S = P J T

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
⊢ cylinder I S = cylinder (I ∪ J) U

Tactic:
rw [← inter_cylinder, h_eq, inter_self]

Result:
no goals