mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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'✝
N✝ : Type u_7
inst✝¹² : TopologicalSpace N✝
inst✝¹¹ : ChartedSpace H'✝ 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
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'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hf' : Surjective ⇑(mfderiv% f x)
hx : I.IsInteriorPoint x
h✝ : IsRCLikeNormedField 𝕜
x✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ I'.IsInteriorPoint (f x)

Tactic:
let _ : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'

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✝
E'✝ : Type u_5
inst✝¹⁵ : NormedAddCommGroup E'✝
inst✝¹⁴ : NormedSpace 𝕜✝ E'✝
H'✝ : Type u_6
inst✝¹³ : TopologicalSpace H'✝
I'✝ : ModelWithCorners 𝕜✝ E'✝ H'✝
N✝ : Type u_7
inst✝¹² : TopologicalSpace N✝
inst✝¹¹ : ChartedSpace H'✝ 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
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'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hf' : Surjective ⇑(mfderiv% f x)
hx : I.IsInteriorPoint x
h✝ : IsRCLikeNormedField 𝕜
x✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝ : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
⊢ I'.IsInteriorPoint (f x)
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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
u : Opens M
⊢ ModelWithCorners.boundary ↥u = Subtype.val ⁻¹' ModelWithCorners.boundary M

Tactic:
simp [← I.compl_interior, I.interior_open]

Goal state after:
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
s : Set M
f g : M → 𝕜
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
hs : UniqueMDiffAt[s] x
⊢ d[s] (f * g) x = f x • d[s] g x + g x • d[s] f x

Tactic:
convert! mvfderivWithin_smul hf hg hs

Goal state after:
case e'_3
𝕜 : 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
s : Set M
f g : M → 𝕜
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
hs : UniqueMDiffAt[s] x
⊢ g x • d[s] f x = (d[s] f x).smulRight (g x)
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G✝ : Type u_4
inst✝⁸ : TopologicalSpace G✝
inst✝⁷ : ChartedSpace H G✝
inst✝⁶ : Group G✝
inst✝⁵ : LieGroup I (minSmoothness 𝕜 3) G✝
inst✝⁴ : CompleteSpace E
G : Type u_5
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : AddGroup G
inst✝ : LieAddGroup I (minSmoothness 𝕜 3) G
c : 𝕜
v w : AddGroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, addInvariantVectorField w x⟩) 0

Tactic:
exact mdifferentiableAt_addInvariantVectorField _

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hVs : EqOn V₁ V t
hVx : V₁ x = V x
hW : MDiffAt[s] (T% W) x
hWs : EqOn W₁ W t
hWx : W₁ x = W x
hxt : UniqueMDiffAt[t] x
h₁ : t ⊆ s
⊢ mlieBracketWithin I V W t x = mlieBracketWithin I V W s x

Tactic:
exact mlieBracketWithin_subset h₁ hxt hV hW

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case hg
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
E' : Type u_6
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
inst✝³ : IsManifold I 2 M
inst✝² : IsManifold I' 2 M'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
A' : x₀ = ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)
h'f : MDiffAt[s] f x₀
this : (mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse = mfderiv% ↑(extChartAt I x₀) x₀
⊢ MDiffAt[s] (↑(extChartAt I' (f x₀)) ∘ f) x₀

Tactic:
apply MDifferentiableAt.comp_mdifferentiableWithinAt (I' := I') _ _ h'f
    exact mdifferentiableAt_extChartAt (ChartedSpace.mem_chart_source (f x₀))

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun x ↦ ℝ) → ℝ := fun x ↦ x.ofLp i
⊢ (fun f ↦ f.ofLp i) ⁻¹' closure (Ici a) = f ⁻¹' Ici a

pp: case hfc
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun x ↦ ℝ) → ℝ := fun x ↦ x.ofLp i
⊢ Continuous fun f ↦ f.ofLp i

Tactic:
closure_Ici

Goal state after:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun x ↦ ℝ) → ℝ := fun x ↦ x.ofLp i
⊢ (fun f ↦ f.ofLp i) ⁻¹' Ici a = f ⁻¹' Ici a

case hfc
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun x ↦ ℝ) → ℝ := fun x ↦ x.ofLp i
⊢ Continuous fun f ↦ f.ofLp i
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
z : ↑(Icc x y)
⊢ 0 ≤ (toLp 2 fun x_1 ↦ ↑z - x).ofLp 0

Tactic:
aesop

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
z : ↑(Icc x y)
⊢ 0 ≤ (toLp 2 fun x_1 ↦ y - ↑z).ofLp 0

Tactic:
aesop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
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
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
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' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f : M → N
φ : N → N'
h : IsImmersionAtOfComplement F J J' n φ (f x)
h' : ContMDiffAt I J' n (φ ∘ f) x
t : Set M
ht : t ⊆ f ⁻¹' h.domChart.source
hxt : x ∈ t
⊢ ContDiffWithinAt 𝕜 n (↑(h.domChart.extend J) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I)
    (↑(extChartAt I x) x)

Tactic:
by
  -- Consider the local expressions of `f`, `φ`, `x` and `s'` in the charts we're considering.
  set f' := (h.domChart.extend J) ∘ f ∘ (extChartAt I x).symm
  set φ' := (h.codChart.extend J') ∘ φ ∘ (h.domChart.extend J).symm
  set x' := (extChartAt I x) x
  set s := (extChartAt I x).symm ⁻¹' t ∩ range I
  have hx' : extChartAt I x x ∈ s := ⟨by simp [mem_chart_source H x, hxt], mem_range_self _⟩
  have h'loc : ContDiffWithinAt 𝕜 n ((h.codChart.extend J') ∘ (φ ∘ f) ∘ (extChartAt I x).symm)
      ((extChartAt I x).symm ⁻¹' t ∩ range I) (extChartAt I x x) := by
    replace h' : CMDiffAt[t] n (φ ∘ f) x := h'.contMDiffWithinAt
    rw [contMDiffWithinAt_iff_of_mem_maximalAtlas' h.codChart_mem_maximalAtlas] at h'
    exacts [h'.2, h.mem_codChart_source]
  -- By hypothesis, `φ ∘ f` (read in our charts) is `C^n` at `x'` within `s`.
  have h'' : ContDiffWithinAt 𝕜 n (φ' ∘ f') s x' := by
    apply h'loc.congr_of_mem (fun y hy ↦ ?_) hx'
    simp only [mfld_simps, φ', f']
    rw [h.domChart.left_inv]
    apply ht hy.1
  -- On the other hand, composing `f'` with the inclusion `u ↦ (u, 0)` is also `C^n`
  -- (as a composition of `C^n` functions); this locally equals `φ ∘ f` in coordinates
  -- (since `f` is an immersion).
  set f'' := (h.equiv ∘ fun x ↦ (x, 0)) ∘ f'
  have h''' : ContDiffWithinAt 𝕜 n f'' s x' := by
    refine h''.congr_of_mem (fun y hy ↦ ?_) hx'
    simp only [f'', φ', f']
    nth_rw 2 [comp_apply]
    rw [Function.comp_apply, h.writtenInCharts]
    rw [h.domChart.extend_target_eq_image_source]
    exact ⟨(f ∘ (extChartAt I x).symm) y, ht hy.1, by simp⟩
  -- Composing with a suitable projection to cancel the inclusion, we deduce that `f` is `C^n`.
  have h'''' : ContDiffWithinAt 𝕜 n ((Prod.fst ∘ h.equiv.symm) ∘ f'') s x' :=
    ContDiffWithinAt.comp x' (by fun_prop) h''' (mapsTo_univ _ _)
  exact h''''.congr_of_mem (fun y hy ↦ by simp [f'']) hx'

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
⊢ (‖(2 / (1 - ((innerSL ℝ) v) ↑x)) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x‖ ^ 2 + 4)⁻¹ •
        4 • ↑((2 / (1 - ((innerSL ℝ) v) ↑x)) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x) +
      (‖(2 / (1 - ((innerSL ℝ) v) ↑x)) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x‖ ^ 2 + 4)⁻¹ •
        (‖(2 / (1 - ((innerSL ℝ) v) ↑x)) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x‖ ^ 2 - 4) • v =
    ↑x

Tactic:
set a : ℝ := innerSL _ v x

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
⊢ (‖(2 / (1 - a)) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x‖ ^ 2 + 4)⁻¹ •
        4 • ↑((2 / (1 - a)) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x) +
      (‖(2 / (1 - a)) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x‖ ^ 2 + 4)⁻¹ •
        (‖(2 / (1 - a)) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x‖ ^ 2 - 4) • v =
    ↑x
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

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✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t | γ t = γ' t} ∩ Ioo a b
hs : s = {t | γ t = γ' t} ∩ Ioo a b
⊢ ∀ ⦃t : { x // x ∈ Ioo a b }⦄, t ∈ closure {a_1 | γ ↑a_1 = γ' ↑a_1} → t ∈ {a_1 | γ ↑a_1 = γ' ↑a_1}

Tactic:
apply IsClosed.closure_subset (isClosed_eq _ _)

Goal state after:
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✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := ⋯
hs : s = {t | γ t = γ' t} ∩ Ioo a b
⊢ Continuous[_, inst✝³] fun y ↦ γ ↑y

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✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := ⋯
hs : s = {t | γ t = γ' t} ∩ Ioo a b
⊢ Continuous[_, inst✝³] fun y ↦ γ' ↑y
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 0 < δ
⊢ ∃ δ, 0 < δ ∧ (r' ^ 2)⁻¹ < 1 - δ * C

Tactic:
have B : Tendsto (fun δ ↦ 1 - δ * C) (𝓝[>] 0) (𝓝 (1 - 0 * C)) := by
      apply tendsto_inf_left
      exact tendsto_const_nhds.sub (tendsto_id.mul tendsto_const_nhds)

Goal state after:
B✝ : Type u_1
inst✝⁷ : TopologicalSpace B✝
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B✝ → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B✝) → NormedAddCommGroup (E x)
inst✝² : (x : B✝) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B✝
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 0 < δ
B : Tendsto (fun δ ↦ 1 - δ * C) (𝓝[>] 0) (𝓝 (1 - 0 * C))
⊢ ∃ δ, 0 < δ ∧ (r' ^ 2)⁻¹ < 1 - δ * C
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: case refine_2
𝕜 : Type u
inst✝¹⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
EN : Type u_3
inst✝⁹ : NormedAddCommGroup EN
inst✝⁸ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝⁷ : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace HN N
EP : Type u_5
inst✝⁴ : NormedAddCommGroup EP
inst✝³ : NormedSpace 𝕜 EP
HP : Type u_6
inst✝² : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace HP P
U : Opens M
V : Opens ↑↑(ChartedSpace.locallyRingedSpace IM ↥U).toPresheafedSpace
x✝ :
  ↑(((TopCat.Presheaf.pushforward CommRingCat
              (LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base).obj
          (ChartedSpace.locallyRingedSpace IM ↥U).presheaf).obj
      (Opposite.op (⋯.functor.obj V)))
g :
  (x :
      ↥(Opposite.unop
          ((Opens.map
                  (LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base).op.obj
            (Opposite.op (⋯.functor.obj V))))) →
    (fun x ↦ 𝕜) ↑x
hg : (StructureGroupoid.LocalInvariantProp.localPredicate (↥U) 𝕜 ⋯).pred g
⊢ ∃ a,
    (ConcreteCategory.hom
          ((LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.c.app
            (Opposite.op (⋯.functor.obj V))))
        a =
      ⟨g, hg⟩

Tactic:
· let a : TopCat.of U ⟶ TopCat.of M := TopCat.ofHom ⟨Subtype.val, continuous_subtype_val⟩
      have ha : IsOpenEmbedding a.hom := U.isOpenEmbedding'
      let V' : Opens U := (Opens.map a).obj (ha.isOpenMap.functor.obj V)
      let b : V' ≃ₜ ha.isOpenMap.functor.obj V :=
        U.isOpenEmbedding'.homeomorphOfSubsetRange <| Set.image_subset_range _ V.1
      refine ⟨⟨g ∘ b.symm, ContMDiff.comp hg ?_⟩, Subtype.ext <| funext fun _ ↦ ?_⟩
      · refine (ContMDiff.subtypeVal_comp_iff V' _).mp ?_
        rw [← ContMDiff.subtypeVal_comp_iff]
        convert! contMDiff_subtype_val
        ext x
        exact congr($(b.apply_symm_apply x).1)
      · change g _ = _
        congr
        apply b.symm_apply_apply

Goal state after:
Module: Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear

Goal state before:
pp: 𝕜 : Type u_1
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : CompleteSpace 𝕜
E : Type u_2
inst✝¹⁸ : AddCommGroup E
inst✝¹⁷ : Module 𝕜 E
inst✝¹⁶ : TopologicalSpace E
inst✝¹⁵ : IsTopologicalAddGroup E
inst✝¹⁴ : ContinuousSMul 𝕜 E
inst✝¹³ : FiniteDimensional 𝕜 E
inst✝¹² : T2Space E
F : Type u_3
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : TopologicalSpace F
inst✝⁸ : IsTopologicalAddGroup F
inst✝⁷ : ContinuousSMul 𝕜 F
inst✝⁶ : FiniteDimensional 𝕜 F
inst✝⁵ : T2Space F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousSMul 𝕜 G
f : E →ₗ[𝕜] F →ₗ[𝕜] G
⊢ IsLinearMap 𝕜 fun x ↦ toContinuousLinearMap (f x)

Tactic:
by constructor <;> (intros; simp)

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

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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t : (x : M) → V x
hs : IsLocalFrameOn I F n s u
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : FiniteDimensional 𝕜 F
h : ∀ (i : ι), ContMDiffAt I 𝓘(𝕜, 𝕜) n ((LinearMap.piApply (hs.coeff i)) t) x
hu : u ∈ 𝓝 x
this : Fintype ι
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t x⟩) x

Tactic:
have almost : CMDiffAt n (T% (fun x ↦ ∑ i, ((LinearMap.piApply (hs.coeff i)) t) x • s i x)) x :=
    .sum_section (fun i _ ↦ (h i).smul_section <| (hs.contMDiffOn i).contMDiffAt hu)

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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t : (x : M) → V x
hs : IsLocalFrameOn I F n s u
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : FiniteDimensional 𝕜 F
h : ∀ (i : ι), ContMDiffAt I 𝓘(𝕜, 𝕜) n ((LinearMap.piApply (hs.coeff i)) t) x
hu : u ∈ 𝓝 x
this : Fintype ι
almost : ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, ∑ i, (LinearMap.piApply (hs.coeff i)) t x • s i x⟩) x
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t x⟩) x
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

Goal state before:
pp: case inr
𝕜 : 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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
t : (x : M) → V x
inst✝¹ : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F 1 s u
inst✝ : FiniteDimensional 𝕜 F
h : ∀ (i : ι), MDiff[u] ((LinearMap.piApply (hs.coeff i)) t)
x : M
hx : x ∈ u
this : Fintype ι
⊢ MDiff[u] (T% t)

Tactic:
have this (i) : MDiff[u] (T% ((LinearMap.piApply (hs.coeff i)) t • s i)) :=
    (h i).smul_section ((hs.contMDiffOn i).mdifferentiableOn one_ne_zero)

Goal state after:
case inr
𝕜 : 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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
t : (x : M) → V x
inst✝¹ : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F 1 s u
inst✝ : FiniteDimensional 𝕜 F
h : ∀ (i : ι), MDiff[u] ((LinearMap.piApply (hs.coeff i)) t)
x : M
hx : x ∈ u
this✝ : Fintype ι
this : ∀ (i : ι), MDiff[u] fun x ↦ ⟨x, ((LinearMap.piApply (hs.coeff i)) t • s i) x⟩
⊢ MDiff[u] (T% t)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ (∀ (x : M × M), x ∈ {x | Commute x.1 x.2}) ↔ IsMulCommutative M

Tactic:
exact ⟨fun h ↦ ⟨⟨fun x y ↦ h (x, y)⟩⟩, fun h x ↦ mul_comm' ..⟩

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

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ cs.wordProd ω.reverse = (cs.wordProd ω)⁻¹

Tactic:
induction ω with
  | nil => simp
  | cons x ω' ih => simpa [wordProd_cons, wordProd_append] using ih

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ (Matrix.of fun i j ↦ if i = j then 1 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2).transpose =
    Matrix.of fun i j ↦ if i = j then 1 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2

Tactic:
aesop

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i i' : Fin n),
    i ≠ i' → Matrix.of (fun i j ↦ if i = j then 1 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2) i i' ≠ 1

Tactic:
aesop

Goal state after: