mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
y : B
hy : y ∈ univ
U : Set B
hu : U ∈ 𝓝 y
hfin : {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ U).Nonempty}.Finite
x : ι
hx : x ∈ {x | t x y ≠ 0}
⊢ x ∈ {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ U).Nonempty}

Tactic:
Set.mem_ofPred

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
y : B
hy : y ∈ univ
U : Set B
hu : U ∈ 𝓝 y
hfin : {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ U).Nonempty}.Finite
x : ι
hx : t x y ≠ 0
⊢ ((fun i ↦ {x | t i x ≠ 0}) x ∩ U).Nonempty
Module: Mathlib.Topology.VectorBundle.Hom

Goal state before:
pp: 𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B₁) → AddCommGroup (E₁ x)
inst✝¹⁷ : (x : B₁) → Module 𝕜 (E₁ x)
inst✝¹⁶ : NormedAddCommGroup F₁
inst✝¹⁵ : NormedSpace 𝕜 F₁
inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹³ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝¹² : (x : B₂) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B₂) → TopologicalSpace (E₂ x)
inst✝⁶ : TopologicalSpace B₁
inst✝⁵ : TopologicalSpace B₂
inst✝⁴ : TopologicalSpace M
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ : ContinuousWithinAt (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) (insert m₀ s) m₀
hv :
  ContinuousWithinAt (fun x ↦ { proj := b₁ x, snd := v x }.proj) (insert m₀ s) m₀ ∧
    ContinuousWithinAt
      (fun x ↦ (↑(trivializationAt F₁ E₁ { proj := b₁ m₀, snd := v m₀ }.proj) { proj := b₁ x, snd := v x }).2)
      (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
⊢ (trivializationAt F₁ E₁ (b₁ m₀)).baseSet ∈ 𝓝 ((fun x ↦ { proj := b₁ x, snd := v x }.proj) m₀)

Tactic:
apply (trivializationAt F₁ E₁ (b₁ m₀)).open_baseSet.mem_nhds

Goal state after:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B₁) → AddCommGroup (E₁ x)
inst✝¹⁷ : (x : B₁) → Module 𝕜 (E₁ x)
inst✝¹⁶ : NormedAddCommGroup F₁
inst✝¹⁵ : NormedSpace 𝕜 F₁
inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹³ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝¹² : (x : B₂) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B₂) → TopologicalSpace (E₂ x)
inst✝⁶ : TopologicalSpace B₁
inst✝⁵ : TopologicalSpace B₂
inst✝⁴ : TopologicalSpace M
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ : ContinuousWithinAt (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) (insert m₀ s) m₀
hv :
  ContinuousWithinAt (fun x ↦ { proj := b₁ x, snd := v x }.proj) (insert m₀ s) m₀ ∧
    ContinuousWithinAt
      (fun x ↦ (↑(trivializationAt F₁ E₁ { proj := b₁ m₀, snd := v m₀ }.proj) { proj := b₁ x, snd := v x }).2)
      (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
⊢ (fun x ↦ { proj := b₁ x, snd := v x }.proj) m₀ ∈ (trivializationAt F₁ E₁ (b₁ m₀)).baseSet
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

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
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set M
g g' : M → F
x : M
hg : MDiffAt[s] g x
hg' : MDiffAt[s] g' x
hs : UniqueMDiffAt[s] x
⊢ d[s] (g - g') x = d[s] g x - d[s] g' x

Tactic:
by
  simp [mvfderivWithin, mfderivWithin_sub hg hg' hs]
  rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁵ : TopologicalSpace H
G : Type u_9
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
h : IsImmersionAtOfComplement F I J n f x
⊢ ↑(h.codChart.extend J) '' f '' ↑(h.domChart.extend I).symm '' (h.domChart.extend I).target ⊆
    (h.codChart.extend J).target

Tactic:
PartialEquiv.symm_image_target_eq_source,

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁵ : TopologicalSpace H
G : Type u_9
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
h : IsImmersionAtOfComplement F I J n f x
⊢ ↑(h.codChart.extend J) '' f '' (h.domChart.extend I).source ⊆ (h.codChart.extend J).target
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H : Type u_7
inst✝⁵ : TopologicalSpace H
G : Type u_9
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
⊢ IsOpen[inst✝³] {x | IsImmersionAt I J n f x}

Tactic:
by
  rw [isOpen_iff_forall_mem_open]
  exact fun x hx ↦ ⟨{x | IsImmersionAtOfComplement hx.complement I J n f x },
    fun y hy ↦ hy.isImmersionAt, .isImmersionAtOfComplement,
    by simp [hx.isImmersionAtOfComplement_complement]⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

Goal state before:
pp: case e'_12
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
hγ : IsMIntegralCurveAt (γ ∘ fun x ↦ x + dt) v (t₀ - dt)
⊢ t₀ = t₀ - dt - -dt

Tactic:
simp only [sub_neg_eq_add, sub_add_cancel]

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : 1 ≤ n
hs : UniqueMDiff[s]
⊢ ContinuousOn (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s)

Tactic:
have : CMDiff[π E (TangentSpace I) ⁻¹' s] 0 (tangentMap[s] f) :=
    hf.contMDiffOn_tangentMapWithin hmn hs

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : 1 ≤ n
hs : UniqueMDiff[s]
this : ContMDiffOn I.tangent I'.tangent 0 (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s)
⊢ ContinuousOn (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s)
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: case ht
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
w : H
w' : H'
⊢ UniqueDiffWithinAt 𝕜 (range ↑I') (↑I' w')

Tactic:
· exact ModelWithCorners.uniqueDiffWithinAt_image I'

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : (x : M) → ENorm (TangentSpace I x)
a b c : ℝ
γ : ℝ → M
h : a ≤ b
h' : b ≤ c
⊢ pathELength I γ a b + pathELength I γ b c = pathELength I γ a c

Tactic:
by
  symm
  have : Icc a c = Icc a b ∪ Ioc b c := (Icc_union_Ioc_eq_Icc h h').symm
  rw [pathELength, this, lintegral_union measurableSet_Ioc]; swap
  · exact disjoint_iff_forall_ne.mpr (fun a ha b hb ↦ (ha.2.trans_lt hb.1).ne)
  simp [restrict_Ioc_eq_restrict_Icc, pathELength]

Goal state after:
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
h : IsSubmersionAtOfComplement F I J n f x
⊢ ↑(h.codChart.extend J) '' f '' ↑(h.domChart.extend I).symm '' (h.domChart.extend I).target ⊆
    (h.codChart.extend J).target

Tactic:
PartialEquiv.symm_image_target_eq_source,

Goal state after:
𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
h : IsSubmersionAtOfComplement F I J n f x
⊢ ↑(h.codChart.extend J) '' f '' (h.domChart.extend I).source ⊆ (h.codChart.extend J).target
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type u_2
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : RiemannianBundle fun x ↦ TangentSpace I x
inst✝² : IsManifold I 1 M
inst✝¹ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
inst✝ : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC✝ : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst✝⁵] u
us : u ⊆ s
hu : u ⊆ {y | ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (chartAt H x).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst✝⁵] v
r : ℝ≥0
hr : ball (↑(extChartAt I x) x) ↑r ⊆ ↑(extChartAt I x).symm ⁻¹' v
r_pos : 0 < r
y : M
hy : y ∈ {y | riemannianEDist I x y < ↑(r / C)}
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < ↑(r / C)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := ↑(extChartAt I x) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
⊢ ↑C * pathELength I γ 0 1 < ↑C * (↑r / ↑C)

Tactic:
gcongr
      · exact ENNReal.coe_ne_top
      · exact hγ.trans_eq (ENNReal.coe_div C_pos.ne')

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality

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
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
A : Type u_9
inst✝¹ : AddCommGroup A
inst✝ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : M → 𝕜 := fun x' ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
this : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
hψ' : MDiffAt ψ x
⊢ Φ (ψ • σ) = Φ (ψ • σ')

Tactic:
funext this

Goal state after:
𝕜 : 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
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
A : Type u_9
inst✝¹ : AddCommGroup A
inst✝ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : M → 𝕜 := fun x' ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
this : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
hψ' : MDiffAt ψ x
⊢ Φ (ψ • σ') = Φ (ψ • σ')
Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality

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
F : Type u_5
inst✝²⁵ : NormedAddCommGroup F
inst✝²⁴ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝²³ : TopologicalSpace (TotalSpace F V)
inst✝²² : (x : M) → AddCommGroup (V x)
inst✝²¹ : (x : M) → Module 𝕜 (V x)
inst✝²⁰ : (x : M) → TopologicalSpace (V x)
inst✝¹⁹ : FiberBundle F V
F' : Type u_7
inst✝¹⁸ : NormedAddCommGroup F'
inst✝¹⁷ : NormedSpace 𝕜 F'
V' : M → Type u_8
inst✝¹⁶ : TopologicalSpace (TotalSpace F' V')
inst✝¹⁵ : (x : M) → AddCommGroup (V' x)
inst✝¹⁴ : (x : M) → Module 𝕜 (V' x)
inst✝¹³ : (x : M) → TopologicalSpace (V' x)
inst✝¹² : FiberBundle F' V'
A : Type u_9
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Module 𝕜 A
Φ✝ : ((x : M) → V x) → A
x✝ : M
inst✝⁹ : VectorBundle 𝕜 F V
inst✝⁸ : VectorBundle 𝕜 F' V'
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : FiniteDimensional 𝕜 F
inst✝⁵ : FiniteDimensional 𝕜 F'
inst✝⁴ : ContMDiffVectorBundle 1 F V I
inst✝³ : ContMDiffVectorBundle 1 F' V' I
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalAddGroup A
inst✝ : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
this✝² : T2Space (V x)
this✝¹ : FiniteDimensional 𝕜 (V x)
this✝ : IsTopologicalAddGroup (V x)
this : ∀ (x : M), ContinuousSMul 𝕜 (V x)
c : 𝕜
v : V x
⊢ Φ (extend F (c • v)) = (RingHom.id 𝕜) c • Φ (extend F v)

Tactic:
dsimp
      rw [← hΦ.smul (f := fun _ ↦ c) (mdifferentiable_const ..) (mdifferentiableAt_extend ..)]
      apply hΦ.pointwise (mdifferentiableAt_extend ..) <|
        mdifferentiableAt_const.smul_section (mdifferentiableAt_extend ..)
      simp

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Pullback

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B) → AddCommMonoid (E x)
inst✝¹⁷ : (x : B) → Module 𝕜 (E x)
inst✝¹⁶ : NormedAddCommGroup F
inst✝¹⁵ : NormedSpace 𝕜 F
inst✝¹⁴ : TopologicalSpace (TotalSpace F E)
inst✝¹³ : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst✝¹² : NormedAddCommGroup EB
inst✝¹¹ : NormedSpace 𝕜 EB
HB : Type u_7
inst✝¹⁰ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁹ : TopologicalSpace B
inst✝⁸ : ChartedSpace HB B
EB' : Type u_8
inst✝⁷ : NormedAddCommGroup EB'
inst✝⁶ : NormedSpace 𝕜 EB'
HB' : Type u_9
inst✝⁵ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁴ : TopologicalSpace B'
inst✝³ : ChartedSpace HB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
⊢ ∀ y ∈ ⇑f ⁻¹' (e.baseSet ∩ e'.baseSet),
    ↑(Trivialization.coordChangeL 𝕜 (e.pullback f) (e'.pullback f) y) =
      ((fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ⇑f) y

Tactic:
rintro b (hb : f b ∈ e.baseSet ∩ e'.baseSet)

Goal state after:
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B) → AddCommMonoid (E x)
inst✝¹⁷ : (x : B) → Module 𝕜 (E x)
inst✝¹⁶ : NormedAddCommGroup F
inst✝¹⁵ : NormedSpace 𝕜 F
inst✝¹⁴ : TopologicalSpace (TotalSpace F E)
inst✝¹³ : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst✝¹² : NormedAddCommGroup EB
inst✝¹¹ : NormedSpace 𝕜 EB
HB : Type u_7
inst✝¹⁰ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁹ : TopologicalSpace B
inst✝⁸ : ChartedSpace HB B
EB' : Type u_8
inst✝⁷ : NormedAddCommGroup EB'
inst✝⁶ : NormedSpace 𝕜 EB'
HB' : Type u_9
inst✝⁵ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁴ : TopologicalSpace B'
inst✝³ : ChartedSpace HB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : f b ∈ e.baseSet ∩ e'.baseSet
⊢ ↑(Trivialization.coordChangeL 𝕜 (e.pullback f) (e'.pullback f) b) =
    ((fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ⇑f) b
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
n : ℕ
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : NeZero n
inst✝ : Nontrivial R
poly : Polygon P n
h : HasNondegenerateVertices R poly
⊢ 3 ≤ n

Tactic:
have := h.hasNondegenerateEdges.two_le

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
n : ℕ
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : NeZero n
inst✝ : Nontrivial R
poly : Polygon P n
h : HasNondegenerateVertices R poly
this : 2 ≤ n
⊢ 3 ≤ n
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card ↥(Subgroup.center G) + ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card = Fintype.card G

Tactic:
by
  convert! Group.nat_card_center_add_sum_card_noncenter_eq_card G using 2
  · simp
  · rw [← finsum_set_coe_eq_finsum_mem (noncenter G), finsum_eq_sum_of_fintype,
      ← Finset.sum_set_coe]
    simp
  · simp

Goal state after:
Module: Mathlib.Geometry.Manifold.WhitneyEmbedding

Goal state before:
pp: E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
ι : Type u_1
inst✝ : Finite ι
f : SmoothBumpCovering ι I M
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ Injective e ∧ ∀ (x : M), Injective ⇑(mfderiv% e x)

Tactic:
by
  cases nonempty_fintype ι
  set F := EuclideanSpace ℝ (Fin <| finrank ℝ (ι → E × ℝ))
  let : IsNoetherian ℝ (E × ℝ) := IsNoetherian.iff_fg.2 inferInstance
  let : FiniteDimensional ℝ (ι → E × ℝ) := IsNoetherian.iff_fg.1 inferInstance
  set eEF : (ι → E × ℝ) ≃L[ℝ] F :=
    ContinuousLinearEquiv.ofFinrankEq finrank_euclideanSpace_fin.symm
  refine ⟨_, eEF ∘ f.embeddingPiTangent,
    eEF.toDiffeomorph.contMDiff.comp f.embeddingPiTangent.contMDiff,
    eEF.injective.comp f.embeddingPiTangent_injective, fun x => ?_⟩
  rw [mfderiv_comp _ eEF.differentiableAt.mdifferentiableAt
      (f.embeddingPiTangent.contMDiff.mdifferentiableAt (by simp)),
    eEF.mfderiv_eq]
  exact eEF.injective.comp (f.embeddingPiTangent_injective_mfderiv _ trivial)

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝¹ : AddGroup G
inst✝ : IsAddKleinFour G
⊢ Nat.card (Multiplicative G) = 4

Tactic:
← IsAddKleinFour.card_four (G := G)

Goal state after:
G : Type u_1
inst✝¹ : AddGroup G
inst✝ : IsAddKleinFour G
⊢ Nat.card (Multiplicative G) = Nat.card G
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: case of_mul
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
motive : M ∗ N → Prop
one : motive 1
inl_mul : ∀ (m : M) (x : M ∗ N), motive x → motive (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), motive x → motive (inr n * x)
x : M ⊕ N
xs : FreeMonoid (M ⊕ N)
ih : motive (mk xs)
⊢ motive (mk (of x * xs))

Tactic:
cases x with

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
⊢ (if Even (p + (k + 1)) then i else j) = (alternatingWord j i p)[k]

Tactic:
getElem_alternatingWord j i p k (by lia)

Goal state after:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i