mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: case neg
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ¬↑z < y
⊢ z ∈ (IccRightChart x y).source

Tactic:
apply lt_of_lt_of_le h.out

Goal state after:
case neg
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ¬↑z < y
⊢ y ≤ ↑z
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: case inr.inl
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p = y
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}

Tactic:
have : p = ⊤ := SetCoe.ext hp
    rw [this]
    apply iff_of_true Icc_isBoundaryPoint_top (mem_insert_of_mem ⊥ rfl)

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

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < 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✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
⊢ ∀ (e e' : OpenPartialHomeomorph (↑(Icc x y)) (EuclideanHalfSpace 1)),
    e ∈ atlas (EuclideanHalfSpace 1) ↑(Icc x y) →
      e' ∈ atlas (EuclideanHalfSpace 1) ↑(Icc x y) →
        ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑(e.symm ≫ₕ e') ∘ ↑(𝓡∂ 1).symm)
          (↑(𝓡∂ 1).symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑(𝓡∂ 1))

Tactic:
intro e

Goal state after:
x✝ y✝ : ℝ
hxy : Fact (x✝ < 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✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
e : OpenPartialHomeomorph (↑(Icc x y)) (EuclideanHalfSpace 1)
⊢ ∀ (e' : OpenPartialHomeomorph (↑(Icc x y)) (EuclideanHalfSpace 1)),
    e ∈ atlas (EuclideanHalfSpace 1) ↑(Icc x y) →
      e' ∈ atlas (EuclideanHalfSpace 1) ↑(Icc x y) →
        ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑(e.symm ≫ₕ e') ∘ ↑(𝓡∂ 1).symm)
          (↑(𝓡∂ 1).symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑(𝓡∂ 1))
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: case h
𝕜 : 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
equiv : (E × F) ≃L[𝕜] E''
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hsource : domChart.source ⊆ f ⁻¹' codChart.source
hwrittenInExtend :
  EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (⇑equiv ∘ fun x ↦ (x, 0)) (domChart.extend I).target
aux : IsImmersionAtOfComplement F I J n f x
⊢ IsImmersionAtOfComplement aux.smallComplement I J n f x

Tactic:
rwa [← IsImmersionAtOfComplement.congr_F aux.smallEquiv]

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

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) :=
  ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := φ₀.trans (PiLp.equivOfUnique 2 ℝ fun x ↦ ℝ)
hz : ¬↑z < y
⊢ (Homeomorph.pointReflection (y / 2)).toOpenPartialHomeomorph ∈ maximalAtlas 𝓘(ℝ, ℝ) n ℝ

Tactic:
apply OpenPartialHomeomorph.mem_maximalAtlas_of_contMDiffOn
      · have : ContDiff ℝ n ((fun v ↦ v + y / 2) ∘ fun x ↦ y / 2 - x) := by fun_prop
        simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ]
      · have : ContDiff ℝ n ((fun v ↦ -v + y / 2) ∘ fun p' ↦ p' - y / 2) := by fun_prop
        simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ]

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

Goal state before:
pp: case h
𝕜 : 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
hf : ContinuousAt f x
equiv : (E × F) ≃L[𝕜] E''
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hwrittenInExtend :
  EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (⇑equiv ∘ fun x ↦ (x, 0)) (domChart.extend I).target
aux : IsImmersionAtOfComplement F I J n f x
⊢ IsImmersionAtOfComplement aux.smallComplement I J n f x

Tactic:
rwa [← IsImmersionAtOfComplement.congr_F aux.smallEquiv]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ ContMDiff 𝓘(𝕜, R) 𝓘(𝕜, R) n fun a ↦ a⁻¹

Tactic:
by
    apply ContMDiff.of_comp_isOpenEmbedding Units.isOpenEmbedding_val
    have : (val : Rˣ → R) ∘ (fun x : Rˣ => x⁻¹) = Ring.inverse ∘ val := by ext; simp
    rw [this, ContMDiff]
    refine fun x => ContMDiffAt.comp x ?_ (contMDiff_val x)
    rw [contMDiffAt_iff_contDiffAt]
    exact contDiffAt_ringInverse _ _

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

Goal state before:
pp: case hf
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
t u : ℝ
⊢ t ≤ u → (fun t ↦ (b' - a')⁻¹ * (t - a')) t ≤ (fun t ↦ (b' - a')⁻¹ * (t - a')) u

Tactic:
htu

Goal state after:
case hf
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
t u : ℝ
htu : t ≤ u
⊢ (fun t ↦ (b' - a')⁻¹ * (t - a')) t ≤ (fun t ↦ (b' - a')⁻¹ * (t - a')) u
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
x : M
⊢ ∃ C > 0, ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ < C

Tactic:
by
  rcases eventually_norm_trivializationAt_lt E (fun (x : M) ↦ TangentSpace% x) x
    with ⟨C, C_pos, hC⟩
  refine ⟨C, C_pos, ?_⟩
  have hx : (chartAt H x).source ∈ 𝓝 x := chart_source_mem_nhds H x
  filter_upwards [hC, hx] with y hy h'y
  rwa [← TangentBundle.continuousLinearMapAt_trivializationAt h'y]

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 s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F n s u
hs' : ∀ (i : ι), ∀ x ∈ u, s i x = s' i x
⊢ ∀ {x : M}, x ∈ u → LinearIndependent 𝕜 fun x_1 ↦ s' x_1 x

Tactic:
intro x hx
    have := hs.linearIndependent hx
    simp_all

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
x : M
n : ℕ∞ω
hs : IsLocalFrameOn I F n s u
hx : x ∈ u
i : ι
⊢ (hs.toBasisAt hx) i = s i x

Tactic:
simpa only [toBasisAt] using Basis.mk_apply (hs.linearIndependent hx) (hs.generating hx) i

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.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
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✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
s : Set M
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov : IsCovariantDerivativeOn F cov s
cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov' : IsCovariantDerivativeOn F cov' s
g : M → 𝕜
σ✝ σ'✝ : (x : M) → V x
x✝ : M
hσ : MDiffAt (T% σ✝) x✝
hσ' : MDiffAt (T% σ'✝) x✝
hx : x✝ ∈ s
⊢ g x✝ • cov σ✝ x✝ + g x✝ • cov σ'✝ x✝ + ((1 - g x✝) • cov' σ✝ x✝ + (1 - g x✝) • cov' σ'✝ x✝) =
    g x✝ • cov σ✝ x✝ + (1 - g x✝) • cov' σ✝ x✝ + (g x✝ • cov σ'✝ x✝ + (1 - g x✝) • cov' σ'✝ x✝)

Tactic:
module

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.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
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✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
s : Set M
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov : IsCovariantDerivativeOn F cov s
cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov' : IsCovariantDerivativeOn F cov' s
g : M → 𝕜
σ✝ : (x : M) → V x
g✝ : M → 𝕜
x✝ : M
hσ : MDiffAt (T% σ✝) x✝
hφ : MDiffAt g✝ x✝
hx : x✝ ∈ s
⊢ g x✝ • g✝ x✝ • cov σ✝ x✝ + g x✝ • (d% g✝ x✝).smulRight (σ✝ x✝) +
      ((1 - g x✝) • g✝ x✝ • cov' σ✝ x✝ + (1 - g x✝) • (d% g✝ x✝).smulRight (σ✝ x✝)) =
    g✝ x✝ • g x✝ • cov σ✝ x✝ + g✝ x✝ • (1 - g x✝) • cov' σ✝ x✝ + (d% g✝ x✝).smulRight (σ✝ x✝)

Tactic:
module

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

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
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E cov
x : M
Y : (x : M) → TangentSpace I x
f✝ : M → 𝕜
σ✝ : (x : M) → TangentSpace I x
hf : MDiffAt f✝ x
hX : MDiffAt (T% σ✝) x
⊢ f✝ x • (cov Y x) (σ✝ x) - (f✝ x • (cov σ✝ x) (Y x) + (d% f✝ x) (Y x) • σ✝ x) -
      (-((d% f✝ x) (Y x) • σ✝ x) + f✝ x • VectorField.mlieBracket I σ✝ Y x) =
    f✝ x • ((cov Y x) (σ✝ x) - (cov σ✝ x) (Y x) - VectorField.mlieBracket I σ✝ Y x)

Tactic:
module

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

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
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E cov
x : M
Y σ✝ σ'✝ : (x : M) → TangentSpace I x
hX : MDiffAt (T% σ✝) x
hX' : MDiffAt (T% σ'✝) x
⊢ (cov Y x) (σ✝ x) + (cov Y x) (σ'✝ x) - ((cov σ✝ x) (Y x) + (cov σ'✝ x) (Y x)) -
      (VectorField.mlieBracket I σ✝ Y x + VectorField.mlieBracket I σ'✝ Y x) =
    (cov Y x) (σ✝ x) - (cov σ✝ x) (Y x) - VectorField.mlieBracket I σ✝ Y x +
      ((cov Y x) (σ'✝ x) - (cov σ'✝ x) (Y x) - VectorField.mlieBracket I σ'✝ Y x)

Tactic:
module

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

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
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E cov
x : M
X : (x : M) → TangentSpace I x
f✝ : M → 𝕜
σ✝ : (x : M) → TangentSpace I x
hf : MDiffAt f✝ x
hY : MDiffAt (T% σ✝) x
⊢ f✝ x • (cov σ✝ x) (X x) + (d% f✝ x) (X x) • σ✝ x - f✝ x • (cov X x) (σ✝ x) -
      ((d% f✝ x) (X x) • σ✝ x + f✝ x • VectorField.mlieBracket I X σ✝ x) =
    f✝ x • ((cov σ✝ x) (X x) - (cov X x) (σ✝ x) - VectorField.mlieBracket I X σ✝ x)

Tactic:
module

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

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
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E cov
x : M
X σ✝ σ'✝ : (x : M) → TangentSpace I x
hY : MDiffAt (T% σ✝) x
hY' : MDiffAt (T% σ'✝) x
⊢ (cov σ✝ x) (X x) + (cov σ'✝ x) (X x) - ((cov X x) (σ✝ x) + (cov X x) (σ'✝ x)) -
      (VectorField.mlieBracket I X σ✝ x + VectorField.mlieBracket I X σ'✝ x) =
    (cov σ✝ x) (X x) - (cov X x) (σ✝ x) - VectorField.mlieBracket I X σ✝ x +
      ((cov σ'✝ x) (X x) - (cov X x) (σ'✝ x) - VectorField.mlieBracket I X σ'✝ x)

Tactic:
module

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Goal state before:
pp: case a
𝕜 : 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✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
i : ι
hi : i ∈ s
⊢ f i x • g x • cov i σ x = g x • f i x • cov i σ x

Tactic:
module

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

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
x : M
inst✝³ : IsManifold I 2 M
inst✝² : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
hcov : IsCovariantDerivativeOn E cov
X₀ Y₀ : TangentSpace I x
⊢ (cov (extend E Y₀) x) X₀ - (cov (extend E X₀) x) Y₀ - -VectorField.mlieBracket I (extend E Y₀) (extend E X₀) x =
    VectorField.mlieBracket I (extend E Y₀) (extend E X₀) x - ((cov (extend E X₀) x) Y₀ - (cov (extend E Y₀) x) X₀)

Tactic:
module

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.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
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✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
s : Set M
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov : IsCovariantDerivativeOn F cov s
A : (x : M) → V x →L[𝕜] TangentSpace I x →L[𝕜] V x
σ✝ : (x : M) → V x
g✝ : M → 𝕜
x✝ : M
hσ : MDiffAt (T% σ✝) x✝
hg : MDiffAt g✝ x✝
hx : x✝ ∈ s
⊢ g✝ x✝ • cov σ✝ x✝ + (d% g✝ x✝).smulRight (σ✝ x✝) + g✝ x✝ • (A x✝) (σ✝ x✝) =
    g✝ x✝ • cov σ✝ x✝ + g✝ x✝ • (A x✝) (σ✝ x✝) + (d% g✝ x✝).smulRight (σ✝ x✝)

Tactic:
module

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.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
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✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
cov cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
hcov' : IsCovariantDerivativeOn F cov' s
x : M
hx : x ∈ s
f✝ : M → 𝕜
σ✝ : (x : M) → V x
hf : MDiffAt f✝ x
hσ : MDiffAt (T% σ✝) x
⊢ f✝ x • cov σ✝ x - f✝ x • cov' σ✝ x = f✝ x • (cov σ✝ x - cov' σ✝ x)

Tactic:
module

Goal state after:
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier = Nat.card G

Tactic:
rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
    Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]

Goal state after:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier =
    ∑ x ∈ Finset.univ \ (noncenter G).toFinset, x.carrier.toFinset.card +
      ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card
Module: Mathlib.Geometry.Manifold.WhitneyEmbedding

Goal state before:
pp: ι : Type uι
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
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ (↑(mfderiv% ⇑f.embeddingPiTangent x)).ker ≤ ⊥

Tactic:
← (mdifferentiable_chart (f.c (f.ind x hx))).ker_mfderiv_eq_bot
      (f.mem_chartAt_ind_source x hx),

Goal state after:
ι : Type uι
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
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ (↑(mfderiv% ⇑f.embeddingPiTangent x)).ker ≤ (↑(mfderiv% ↑(chartAt H (f.c (f.ind x hx))) x)).ker
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case pos
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

pp: case neg
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
· rw [h1, reciprocalFactors_one, commProb_nil, Nat.cast_one, div_one]

Goal state after:
case neg
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : FreeMonoid (G ⊕ H)
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList x)).reverse) * mk x = mk 1

Tactic:
map_one

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : FreeMonoid (G ⊕ H)
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList x)).reverse) * mk x = 1
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: case of_mul
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : G ⊕ H
xs : FreeMonoid (G ⊕ H)
ihx : mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList xs)).reverse) * mk xs = 1
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList (of x * xs))).reverse) * mk (of x * xs) = 1

Tactic:
| of_mul x xs ihx =>

Goal state after: