mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

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
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
hγ2 : IsMIntegralCurveOn γ2 v {t | t - (asup - ε / 2) ∈ Ioo (-ε) ε}
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
⊢ False

Tactic:
Set.mem_Ioo,

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
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | -ε < t - (asup - ε / 2) ∧ t - (asup - ε / 2) < ε}
⊢ False
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 : ℝ
γ γ' : ℝ → M
h : EqOn γ γ' (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
A : γ t = γ' t
⊢ ‖(mfderiv% γ t) 1‖ₑ = ‖(mfderiv% γ' t) 1‖ₑ

Tactic:
congr! 2

Goal state after:
case e'_3.e'_5
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 : ℝ
γ γ' : ℝ → M
h : EqOn γ γ' (Ioo a b)
t : ℝ
ht : t ∈ Ioo a b
A : γ t = γ' t
e_1✝¹ : TangentSpace I (γ t) = TangentSpace I (γ' t)
e_1✝ : (TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I (γ t)) = (TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I (γ' t))
⊢ mfderiv% γ t = mfderiv% γ' t
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'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E' → E' := fun x ↦ ↑I' (↑(chartAt H' b.proj) (↑(chartAt H' p.2.proj).symm (↑I'.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I') (↑I' (↑(chartAt H' p.2.proj) p.2.proj))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map ↑I ↑I'))
      (↑I (↑(chartAt H w.proj) w.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj))
φ' : E → E := fun x ↦ ↑I (↑(chartAt H a.proj) (↑(chartAt H p.1.proj).symm (↑I.symm x)))
D0' : DifferentiableWithinAt 𝕜 φ' (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj))
D' :
  DifferentiableWithinAt 𝕜 (φ' ∘ Prod.fst) (range (Prod.map ↑I ↑I'))
    (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj))
⊢ DifferentiableWithinAt 𝕜
    (fun x ↦
      ↑I
        (↑(chartAt H a.proj)
          (↑((chartAt H p.1.proj).prod (chartAt H' p.2.proj).toPartialEquiv).symm
              (↑(I.prod I'.toPartialEquiv).symm x)).1))
    (range (Prod.map ↑I ↑I')) (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj))

Tactic:
exact D'

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 a' b' : ℝ
γ : ℝ → M
h : a' ≤ a
h' : b ≤ b'
⊢ pathELength I γ a b ≤ pathELength I γ a' b'

Tactic:
simpa [pathELength_eq_lintegral_mfderiv_Icc] using lintegral_mono_set (Icc_subset_Icc h h')

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
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
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 : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
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₀
hfi : (mfderiv[s] f x₀).IsInvertible
this : CompleteSpace E'
u : Set M
u_open : IsOpen[inst✝⁹] u
x₀u : x₀ ∈ u
u_mem : u ∈ 𝓝 x₀
s' : Set M := s ∩ u
ut : s' ⊆ f ⁻¹' t
maps_u : s' ⊆ f ⁻¹' (extChartAt I' (f x₀)).source
u_smooth : ContMDiffOn I I' 2 f s'
hs' : s' = s ∩ u
s'_eq : s' =ᶠ[𝓝 x₀] s
t' : Set M' := t ∩ (extChartAt I' (f x₀)).source
ht' : t' = t ∩ (extChartAt I' (f x₀)).source
⊢ ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) ∈ u

Tactic:
by simpa using x₀u

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

Goal state before:
pp: case hγ
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)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := fun t ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
B : ∀ (t : ℝ), b' < t → η t = 1
B' : ∀ (t : ℝ), b' < t → (γ ∘ η) t = y
⊢ MDiff[Icc 0 (η b)] γ

Tactic:
B b hb'b

Goal state after:
case hγ
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)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := fun t ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
B : ∀ (t : ℝ), b' < t → η t = 1
B' : ∀ (t : ℝ), b' < t → (γ ∘ η) t = y
⊢ MDiff[Icc 0 1] γ
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: case refine_4
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)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := fun t ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
B : ∀ (t : ℝ), b' < t → η t = 1
B' : ∀ (t : ℝ), b' < t → (γ ∘ η) t = y
⊢ γ ∘ η =ᶠ[𝓝 b] fun x ↦ y

Tactic:
filter_upwards [Ioi_mem_nhds hb'b] with t ht using B' t ht

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

Goal state before:
pp: H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
U V : Opens ↑(TopCat.of M)
⊢ ∀ (i : U ⟶ V) (f : ↥V → M'), ChartedSpace.LiftProp P f → ChartedSpace.LiftProp P fun x ↦ f (i x)

Tactic:
i

Goal state after:
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
U V : Opens ↑(TopCat.of M)
i : U ⟶ V
⊢ ∀ (f : ↥V → M'), ChartedSpace.LiftProp P f → ChartedSpace.LiftProp P fun x ↦ f (i x)
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
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✝⁵ : 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
h : IsSubmersion I J n f
x : M
⊢ ∃ F x_1 x_2, IsSubmersionAtOfComplement F I J n f x

Tactic:
use h.complement, by infer_instance, by infer_instance

Goal state after:
case h
𝕜 : Type u_1
E'' : Type u_3
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✝⁵ : 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
h : IsSubmersion I J n f
x : M
⊢ IsSubmersionAtOfComplement h.complement I J n f x
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:
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
inst✝⁵ : VectorBundle 𝕜 F V
inst✝⁴ : ContMDiffVectorBundle 1 F V I
e : Trivialization F TotalSpace.proj
inst✝³ : MemTrivializationAtlas e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
k : ℕ∞ω
x : M
inst✝² : FiniteDimensional 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : ContMDiffVectorBundle k F V I
hxe : x ∈ e.baseSet
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) k (fun x ↦ ⟨x, s x⟩) x
i : ι
aux : M → 𝕜 := fun x ↦ (b.repr (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) i
h₁ : ContMDiffAt I 𝓘(𝕜, F) k (fun x ↦ (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) x
breprl : F →ₗ[𝕜] 𝕜 := { toFun := fun v ↦ (b.repr v) i, map_add' := ⋯, map_smul' := ⋯ }
this : ContMDiffAt 𝓘(𝕜, F) 𝓘(𝕜, 𝕜) k (⇑(LinearMap.toContinuousLinearMap breprl)) (↑e ((fun x ↦ ⟨x, s x⟩) x)).2
⊢ ContMDiffAt I 𝓘(𝕜, 𝕜) k (fun x ↦ (b.repr (↑e ⟨x, s x⟩).2) i) x

Tactic:
exact this.comp x h₁

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
inst✝⁴ : VectorBundle 𝕜 F V
inst✝³ : ContMDiffVectorBundle 1 F V I
e : Trivialization F TotalSpace.proj
inst✝² : MemTrivializationAtlas e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
x : M
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) x
i : ι
aux : M → 𝕜 := fun x ↦ (b.repr (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) i
h₁ : (MDiffAt fun x ↦ (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) x
breprl : F →ₗ[𝕜] 𝕜 := { toFun := fun v ↦ (b.repr v) i, map_add' := ⋯, map_smul' := ⋯ }
this : MDiffAt ⇑(LinearMap.toContinuousLinearMap breprl) (↑e ((fun x ↦ ⟨x, s x⟩) x)).2
⊢ (MDiffAt fun x ↦ (b.repr (↑e ⟨x, s x⟩).2) i) x

Tactic:
exact this.comp x h₁

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

Goal state before:
pp: case empty
𝕜 : 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
inst✝ : VectorBundle 𝕜 F V
hΦ : TensorialAt I F Φ x
ι : Type u_10
σ : ι → (x : M) → V x
hσ : ∀ i ∈ ∅, MDiffAt (T% σ) x
⊢ (Φ fun x' ↦ ∑ i ∈ ∅, σ i x') = ∑ i ∈ ∅, Φ (σ i)

Tactic:
rw [Finset.sum_empty]

Goal state after:
case empty
𝕜 : 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
inst✝ : VectorBundle 𝕜 F V
hΦ : TensorialAt I F Φ x
ι : Type u_10
σ : ι → (x : M) → V x
hσ : ∀ i ∈ ∅, MDiffAt (T% σ) x
⊢ (Φ fun x' ↦ ∑ i ∈ ∅, σ i x') = 0
Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality

Goal state before:
pp: case insert
𝕜 : 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
inst✝ : VectorBundle 𝕜 F V
hΦ : TensorialAt I F Φ x
ι : Type u_10
σ : ι → (x : M) → V x
a : ι
s : Finset ι
ha : a ∉ s
h : (∀ i ∈ s, MDiffAt (T% σ) x) → (Φ fun x' ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)
hσ : ∀ i ∈ insert a s, MDiffAt (T% σ) x
⊢ (Φ fun x' ↦ ∑ i ∈ insert a s, σ i x') = ∑ i ∈ insert a s, Φ (σ i)

Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at hσ

Goal state after:
case insert
𝕜 : 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
inst✝ : VectorBundle 𝕜 F V
hΦ : TensorialAt I F Φ x
ι : Type u_10
σ : ι → (x : M) → V x
a : ι
s : Finset ι
ha : a ∉ s
h : (∀ i ∈ s, MDiffAt (T% σ) x) → (Φ fun x' ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)
hσ : MDiffAt (T% σ) x ∧ ∀ a ∈ s, MDiffAt (T% σ) x
⊢ (Φ fun x' ↦ ∑ i ∈ insert a s, σ i x') = ∑ i ∈ insert a s, Φ (σ i)
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₁)
this✝ : ‖γ' t₁ - γ' 0‖ₑ < ↑r
this : γ' t₁ ∈ ↑(extChartAt I x).symm ⁻¹' v
⊢ γ t₁ ∈ v

Tactic:
convert! mem_preimage.1 this

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✝³ : 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₁)
this✝ : ‖γ' t₁ - γ' 0‖ₑ < ↑r
this : γ' t₁ ∈ ↑(extChartAt I x).symm ⁻¹' v
⊢ γ t₁ = ↑(extChartAt I x).symm (γ' t₁)
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: case «0»
P : Type u_3
n : ℕ
inst✝ : NeZero 0
poly : Polygon P 0
h : poly.HasNondegenerateEdges
hlt : 0 < 2
⊢ False

pp: case «1»
P : Type u_3
n : ℕ
inst✝ : NeZero 1
poly : Polygon P 1
h : poly.HasNondegenerateEdges
hlt : 1 < 2
⊢ False

Tactic:
· simp_all only [neZero_zero_iff_false]

Goal state after:
case «1»
P : Type u_3
n : ℕ
inst✝ : NeZero 1
poly : Polygon P 1
h : poly.HasNondegenerateEdges
hlt : 1 < 2
⊢ False
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card ↑(noncenter G)ᶜ = (Finset.univ \ (noncenter G).toFinset).card

Tactic:
rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]

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

Goal state before:
pp: case inl
n : ℕ
hn : 0 < n
⊢ r 1 ^ n ≠ 1

Tactic:
rw [r_one_pow, one_def]

Goal state after:
case inl
n : ℕ
hn : 0 < n
⊢ r ↑n ≠ r 0
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ Function.Surjective (ConjClasses.map (QuotientGroup.mk' H))

Tactic:
exact ConjClasses.map_surjective Quotient.mk''_surjective

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
⊢ Surjective ⇑↑(FreeGroup.freeGroupCongr e)

Tactic:
simpa using (FreeGroup.freeGroupCongr e).surjective

Goal state after: