mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z ↦ {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → ↑T → ℕ → Set E :=
  fun n z p ↦ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))
K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
this : Encodable ↑T
⊢ ∃ F, Function.Surjective F

Tactic:
have : Nonempty T := by
      rcases hs with ⟨x, xs⟩
      rcases s_subset x xs with ⟨n, z, _⟩
      exact ⟨z⟩

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z ↦ {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → ↑T → ℕ → Set E :=
  fun n z p ↦ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))
K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
this✝ : Encodable ↑T
this : Nonempty ↑T
⊢ ∃ F, Function.Surjective F
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atBot
b : ℝ
hb : IntegrableOn f (Iic b) μ
i : ι
hi : a i ∈ Iic b
⊢ ∫ (x : ℝ) in Iic b, f x ∂μ - ∫ (x : ℝ) in Iic (a i), f x ∂μ = ∫ (x : ℝ) in a i..b, f x ∂μ

Tactic:
intervalIntegral.integral_Iic_sub_Iic (hb.mono_set (Iic_subset_Iic.2 hi)) hb

Goal state after:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atBot
b : ℝ
hb : IntegrableOn f (Iic b) μ
i : ι
hi : a i ∈ Iic b
⊢ ∫ (x : ℝ) in a i..b, f x ∂μ = ∫ (x : ℝ) in a i..b, f x ∂μ
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
⊢ ∫ (x : ℝ) in Icc a b, f' x • g (f x) = -∫ (u : ℝ) in Icc (f b) (f a), g u

Tactic:
have A : ∫ u in Icc (f b) (f a), g u = ∫ u in f '' (Ioo a b), g u := by
    apply setIntegral_congr_set
    rw [← hf.image_Icc_of_antitoneOn hab M]
    refine ae_eq_set.2 ⟨?_, by simp [show f '' Ioo a b \ f '' Icc a b = ∅ by grind]⟩
    have : f '' (Icc a b) \ f '' Ioo a b ⊆ {f a, f b} := by grind
    apply measure_mono_null this
    apply Finite.measure_zero (by simp)

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A : ∫ (u : ℝ) in Icc (f b) (f a), g u = ∫ (u : ℝ) in f '' Ioo a b, g u
⊢ ∫ (x : ℝ) in Icc a b, f' x • g (f x) = -∫ (u : ℝ) in Icc (f b) (f a), g u
Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Goal state before:
pp: E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) μ
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) μ
hfg : Integrable (fun x ↦ (B (f x)) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ
Hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) (ν.prod volume)
Hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) (ν.prod volume)
Hfg : Integrable (fun x ↦ (B (f x)) (g x)) (ν.prod volume)
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ

Tactic:
isAddLeftInvariant_eq_smul μ (ν.prod volume)

Goal state after:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) μ
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) μ
hfg : Integrable (fun x ↦ (B (f x)) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ
Hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) (ν.prod volume)
Hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) (ν.prod volume)
Hfg : Integrable (fun x ↦ (B (f x)) (g x)) (ν.prod volume)
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ.addHaarScalarFactor (ν.prod volume) • ν.prod volume =
    -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ.addHaarScalarFactor (ν.prod volume) • ν.prod volume
Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Goal state before:
pp: E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) μ
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) μ
hfg : Integrable (fun x ↦ (B (f x)) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
⊢ ∃ L, L v = (0, 1)

Tactic:
by
    have : finrank ℝ (E' × ℝ) = n := by simpa [this, E'] using Nat.sub_add_cancel finrank_pos
    have L₀ : E ≃L[ℝ] (E' × ℝ) := (ContinuousLinearEquiv.ofFinrankEq this).symm
    obtain ⟨M, hM⟩ : ∃ M : (E' × ℝ) ≃L[ℝ] (E' × ℝ), M (L₀ v) = (0, 1) := by
      apply SeparatingDual.exists_continuousLinearEquiv_apply_eq
      · simpa using hv
      · simp
    exact ⟨L₀.trans M, by simp [hM]⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a) volume
hg2 : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) (Ici a) volume
⊢ ∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Ioi (f a), g u

Tactic:
have eq : ∀ b : ℝ, a < b → (∫ x in a..b, f' x • (g ∘ f) x) = ∫ u in f a..f b, g u := fun b hb ↦ by
    have i1 : Ioo (min a b) (max a b) ⊆ Ioi a := by
      rw [min_eq_left hb.le]
      exact Ioo_subset_Ioi_self
    have i2 : [[a, b]] ⊆ Ici a := by rw [uIcc_of_le hb.le]; exact Icc_subset_Ici_self
    refine
      intervalIntegral.integral_deriv_smul_comp''' (hf.mono i2)
        (fun x hx => hff' x <| mem_of_mem_of_subset hx i1) (hg_cont.mono <| image_mono ?_)
        (hg1.mono_set <| image_mono ?_) (hg2.mono_set i2) <;> assumption
  rw [integrableOn_Ici_iff_integrableOn_Ioi] at hg2
  have t2 := intervalIntegral_tendsto_integral_Ioi _ hg2 tendsto_id
  have : Ioi (f a) ⊆ f '' Ici a :=
    Ioi_subset_Ici_self.trans <|
      IsPreconnected.intermediate_value_Ici isPreconnected_Ici self_mem_Ici
        (le_principal_iff.mpr <| Ici_mem_atTop _) hf hft
  have t1 := (intervalIntegral_tendsto_integral_Ioi _ (hg1.mono_set this) tendsto_id).comp hft
  exact tendsto_nhds_unique (Tendsto.congr' (eventuallyEq_of_mem (Ioi_mem_atTop a) eq) t2) t1

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f.extend I).target

Tactic:
by
  rw [extend_target, I.range_eq_univ, inter_univ]
  exact I.continuous_symm.isOpen_preimage _ f.open_target

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
hs : s ⊆ f.source
⊢ MapsTo (↑(f.extend I)) s (↑(f.extend I).symm ⁻¹' s ∩ range ↑I)

Tactic:
mapsTo_iff_image_subset,

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
hs : s ⊆ f.source
⊢ ↑(f.extend I) '' s ⊆ ↑(f.extend I).symm ⁻¹' s ∩ range ↑I
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
⊢ P (↑e' ∘ f) s x ↔ P f s x

Tactic:
have h2f := hfs.preimage_mem_nhdsWithin (e'.open_source.mem_nhds hxe')

Goal state after:
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
⊢ P (↑e' ∘ f) s x ↔ P f s x
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : H
hy : y ∈ f.target
hy' : ↑I y ∈ interior (range ↑I)
⊢ ↑I y ∈ ↑I.symm ⁻¹' f.target ∧ ↑I y ∈ interior (range ↑I)

Tactic:
mem_preimage

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : H
hy : y ∈ f.target
hy' : ↑I y ∈ interior (range ↑I)
⊢ ↑I.symm (↑I y) ∈ f.target ∧ ↑I y ∈ interior (range ↑I)
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝 x
⊢ ↑(f.extend I).symm ⁻¹' t ∈ 𝓝 (↑(f.extend I) x)

Tactic:
apply (continuousAt_extend_symm f h).preimage_mem_nhds

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝 x
⊢ t ∈ 𝓝 (↑(f.extend I).symm (↑(f.extend I) x))
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type w
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this : (range fun x ↦ (↑I x.1, ↑I' x.2)) = range (Prod.map ↑I ↑I')
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range ↑I ×ˢ range ↑I') else range ↑I ×ˢ range ↑I' = univ

Tactic:
split_ifs with h

Goal state after:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type w
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this : (range fun x ↦ (↑I x.1, ↑I' x.2)) = range (Prod.map ↑I ↑I')
h : IsRCLikeNormedField 𝕜
⊢ Convex ℝ (range ↑I ×ˢ range ↑I')

case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type w
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this : (range fun x ↦ (↑I x.1, ↑I' x.2)) = range (Prod.map ↑I ↑I')
h : ¬IsRCLikeNormedField 𝕜
⊢ range ↑I ×ˢ range ↑I' = univ
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type v
inst✝³ : Fintype ι
E : ι → Type w
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
H : ι → Type u'
inst✝ : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners 𝕜 (E i) (H i)
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (univ.pi fun i ↦ range ↑(I i).toPartialEquiv)
  else (univ.pi fun i ↦ range ↑(I i).toPartialEquiv) = univ

Tactic:
split_ifs with h

Goal state after:
case pos
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type v
inst✝³ : Fintype ι
E : ι → Type w
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
H : ι → Type u'
inst✝ : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners 𝕜 (E i) (H i)
h : IsRCLikeNormedField 𝕜
⊢ Convex ℝ (univ.pi fun i ↦ range ↑(I i).toPartialEquiv)

case neg
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type v
inst✝³ : Fintype ι
E : ι → Type w
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
H : ι → Type u'
inst✝ : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners 𝕜 (E i) (H i)
h : ¬IsRCLikeNormedField 𝕜
⊢ (univ.pi fun i ↦ range ↑(I i).toPartialEquiv) = univ
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
y : H
hy : ↑(chartAt H x).symm y ∈ t
⊢ y ∈ ↑(chartAt H x).symm ⁻¹' s

Tactic:
simp only [hy, hts _, mfld_simps]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case left
n : ℕ∞ω
𝕜 : 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
f : OpenPartialHomeomorph H H
hf : f.source = ∅
x : E
hx : x ∈ ↑I.symm ⁻¹' f.source
right✝ : x ∈ range ↑I
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ range ↑I) x

Tactic:
mem_preimage

Goal state after:
case left
n : ℕ∞ω
𝕜 : 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
f : OpenPartialHomeomorph H H
hf : f.source = ∅
x : E
hx : ↑I.symm x ∈ f.source
right✝ : x ∈ range ↑I
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ range ↑I) x
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
⊢ ∫ (x : ↑s), (g ∘ f) ↑x ∂Measure.comap Subtype.val (μ.withDensity fun x ↦ ↑|(f' x).det|.toNNReal) =
    ∫ (x : E) in s, |(f' x).det| • (g ∘ f) x ∂μ

Tactic:
← (MeasurableEmbedding.subtype_coe hs).integral_map,

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
⊢ ∫ (y : E),
      (g ∘ f) y ∂Measure.map Subtype.val (Measure.comap Subtype.val (μ.withDensity fun x ↦ ↑|(f' x).det|.toNNReal)) =
    ∫ (x : E) in s, |(f' x).det| • (g ∘ f) x ∂μ
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: 𝕜 : 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
n : ℕ∞ω
x : H
y : E
hy : y ∈ range ↑I
⊢ (↑I ∘ ↑I.symm) y = id y

Tactic:
by simp [hy]

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: 𝕜 : 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
n : ℕ∞ω
x : E
hx : x ∈ range ↑I
y : E
hy : y ∈ range ↑I
⊢ (↑I ∘ ↑I.symm) y = id y

Tactic:
by simp [hy]

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: 𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
⊢ MDiffAt[s] f x ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
        ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
        (↑(extChartAt I x) x)

Tactic:
simp only [MDifferentiableWithinAt, liftPropWithinAt_iff']
  exact and_congr_right fun hc => differentiableWithinAt_congr_nhds <|
    hc.nhdsWithin_extChartAt_symm_preimage_inter_range

Goal state after:
Module: Mathlib.Topology.FiberBundle.Constructions

Goal state before:
pp: case refine_2
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x ↦ E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p ↦ ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p ↦ (↑e₁ p.1, ↑e₂ p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet
right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet
⊢ { proj := b, snd := v₁ } ∈ TotalSpace.proj ⁻¹' e₁.baseSet

Tactic:
mem_preimage

Goal state after:
case refine_2
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x ↦ E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p ↦ ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p ↦ (↑e₁ p.1, ↑e₂ p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet
right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet
⊢ { proj := b, snd := v₁ }.proj ∈ e₁.baseSet
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: 𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
⊢ HasMFDerivAt[univ] f x f' ↔ HasMFDerivAt% f x f'

Tactic:
by
  simp only [HasMFDerivWithinAt, HasMFDerivAt, continuousWithinAt_univ, mfld_simps]

Goal state after: