mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁰ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace H N
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁵ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁴ : TopologicalSpace N'
inst✝³ : ChartedSpace H'' N'
n : ℕ∞ω
A : Type u_10
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContMDiffRing 𝓘(𝕜, A) n A
c₁ c₂ : 𝕜
⊢ ⟨fun x ↦ (algebraMap 𝕜 A) (c₁ * c₂), ⋯⟩ = ⟨fun x ↦ (algebraMap 𝕜 A) c₁, ⋯⟩ * ⟨fun x ↦ (algebraMap 𝕜 A) c₂, ⋯⟩

Tactic:
ext; exact (algebraMap 𝕜 A).map_mul _ _

Goal state after:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case right
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃✝ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
i : Fin 3
h₁₂₃ : i = i₁ ∨ i = i₂ ∨ i = i₃
⊢ dist (p i) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t

Tactic:
repeat' rcases h₁₂₃ with h₁₂₃ | h₁₂₃

Goal state after:
case right.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
⊢ dist (p i₁) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t

case right.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
⊢ dist (p i₂) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t

case right.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
⊢ dist (p i₃) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
ho : OrthocentricSystem s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
⊢ affineSpan ℝ (Set.range p) = affineSpan ℝ s

Tactic:
have ha := ho.affineIndependent hps hpi

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
ho : OrthocentricSystem s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
ha : AffineIndependent ℝ p
⊢ affineSpan ℝ (Set.range p) = affineSpan ℝ s
Module: Mathlib.Geometry.Manifold.Bordism

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹⁸ : TopologicalSpace X
inst✝¹⁷ : TopologicalSpace Y
inst✝¹⁶ : TopologicalSpace Z
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
M✝ : Type u_6
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace ℝ E
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : TopologicalSpace H
I✝ : ModelWithCorners ℝ E H
inst✝¹¹ : TopologicalSpace M✝
inst✝¹⁰ : ChartedSpace H M✝
inst✝⁹ : IsManifold I✝ k M✝
inst✝⁸ : CompactSpace M✝
inst✝⁷ : BoundarylessManifold I✝ M✝
E' : Type u_7
H' : Type u_8
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : TopologicalSpace H'
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
I : ModelWithCorners ℝ E H
inst✝¹ : IsManifold I k M
inst✝ : IsEmpty M
⊢ ∀ (x : M), ContinuousAt (fun x ↦ ⋯.elim) x

Tactic:
exact fun x ↦ (IsEmpty.false x).elim

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : NormedAddCommGroup F
inst✝¹⁹ : NormedSpace 𝕜 F
inst✝¹⁸ : TopologicalSpace (TotalSpace F E)
inst✝¹⁷ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst✝¹³ : NormedAddCommGroup EM
inst✝¹² : NormedSpace 𝕜 EM
HM : Type u_11
inst✝¹¹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace HM M
inst✝⁸ : TopologicalSpace B
inst✝⁷ : ChartedSpace HB B
inst✝⁶ : FiberBundle F E
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
inst✝³ : VectorBundle 𝕜 F E
inst✝² : ContMDiffVectorBundle 1 F E IB
e e' : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
inst✝ : MemTrivializationAtlas e'
f : M → TotalSpace F E
x₀ : M
he : f x₀ ∈ e.source
he' : f x₀ ∈ e'.source
hf : (MDiffAt fun x ↦ (f x).proj) x₀
⊢ (MDiffAt fun x ↦ (↑e (f x)).2) x₀ ↔ (MDiffAt fun x ↦ (↑e' (f x)).2) x₀

Tactic:
by
  simpa [← mdifferentiableWithinAt_univ] using
    e.mdifferentiableWithinAt_snd_comp_iff₂ IB he he' hf

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

Goal state before:
pp: case hW
𝕜 : 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 : Set M
x : M
V W : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I) (↑(extChartAt I x) x) = 0

Tactic:
· simp only [mpullbackWithin_apply]
    have : (extChartAt I x).symm ((extChartAt I x) x) = x := by simp
    rw [this, hW]
    simp +instances

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 : Set M
x : M
V : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : (MDiffAt[s] fun x ↦ ⟨x, V x⟩) x
this :
  (MDiffAt[range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s] fun x_1 ↦
      ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) x_1⟩)
    (↑(extChartAt I x) x)
⊢ MDiffAt[range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s] (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (↑(extChartAt I x) x)

Tactic:
exact (contMDiff_snd_tangentBundle_modelSpace E 𝓘(𝕜, E)).contMDiffAt.mdifferentiableAt one_ne_zero
    |>.comp_mdifferentiableWithinAt _ this

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

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
⊢ ↑((IccRightChart x y).extend (𝓡∂ 1)) ⊤ = 0

Tactic:
norm_num [IccRightChart, modelWithCornersEuclideanHalfSpace_zero]

Goal state after:
x y : ℝ
hxy : Fact (x < y)
⊢ (fun x ↦ 0) = 0
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
h : IsImmersionOfComplement F I J n f
hM : IsEmpty M
⊢ IsImmersionOfComplement PUnit.{u + 1} I J n f

Tactic:
exact fun x ↦ (IsEmpty.false x).elim

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr (↑(stereographic ⋯) v) = 0

Tactic:
simp only [EmbeddingLike.map_eq_zero_iff]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ ↑(stereographic ⋯) v = 0
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 : ℝ
ha : ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)
hlt : asup + -(ε / 2) < a
⊢ False

Tactic:
← sub_eq_add_neg

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 : ℝ
ha : ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)
hlt : asup - ε / 2 < a
⊢ 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)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
hf : ContMDiff (𝓡∂ 1) I 1 f
⊢ Path x y

Tactic:
by
    refine ⟨⟨f, hf.continuous⟩, ?_, ?_⟩ <;>
    simp [f, η, ContinuousAffineMap.coe_lineMap_eq, ha, hb]

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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
γ : Path x y
hγ : ContMDiff (𝓡∂ 1) 𝓘(ℝ, F) 1 ⇑γ
e : ℝ → F := ⇑γ ∘ projIcc 0 1 ⋯
D : ContDiffOn ℝ 1 e (Icc 0 1)
⊢ ‖e 1 - e 0‖ₑ ≤ ∫⁻ (t : ℝ) in Icc 0 1, ‖(fderivWithin ℝ (⇑γ ∘ projIcc 0 1 ⋯) (Icc 0 1) t) 1‖ₑ

Tactic:
exact (enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc D zero_le_one).trans_eq rfl

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

Goal state before:
pp: 𝕜 : 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
f : M → N
hf : ContMDiff IM IN ∞ f
x : M
U : Opens ↑↑(locallyRingedSpace IN N).toPresheafedSpace
hxU : (ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base) x ∈ U
a : ↑((locallyRingedSpace IN N).presheaf.obj (Opposite.op U))
⊢ (CommRingCat.Hom.hom
        ((locallyRingedSpaceMapAux f hf).c.app (Opposite.op U) ≫
          (locallyRingedSpace IM M).presheaf.germ ((Opens.map (locallyRingedSpaceMapAux f hf).base).obj U) x hxU ≫
            smoothSheafCommRing.evalHom IM 𝓘(𝕜, 𝕜) M 𝕜 x))
      a =
    ↑a ⟨f x, hxU⟩

Tactic:
apply smoothSheafCommRing.evalHom_germ

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

Goal state before:
pp: case h
𝕜 : 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
h : IsSubmersionOfComplement F I J n f
hM : IsEmpty M
⊢ IsSubmersionOfComplement PUnit.{u + 1} I J n f

Tactic:
exact fun x ↦ (IsEmpty.false x).elim

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

Tactic:
by
  rcases u.eq_empty_or_nonempty with rfl | ⟨x, hx⟩; · simp
  have := fintypeOfFiniteDimensional hs hx
  have this (i) : CMDiff[u] n (T% ((LinearMap.piApply (hs.coeff i)) t • s i)) :=
    (h i).smul_section (hs.contMDiffOn i)
  have almost : CMDiff[u] n (T% (fun x ↦ ∑ i, ((LinearMap.piApply (hs.coeff i)) t) x • s i x)) :=
    .sum_section fun i _ ↦ this i
  apply almost.congr
  intro y hy
  simpa using congrArg (TotalSpace.mk' F y) (hs.coeff_sum_eq t hy)

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
⊢ cov (g✝ • σ✝) x✝ + (A x✝) ((g✝ • σ✝) x✝) = g✝ x✝ • (cov σ✝ x✝ + (A x✝) (σ✝ x✝)) + (d% g✝ x✝).smulRight (σ✝ x✝)

Tactic:
simp [hcov.leibniz hσ hg]

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✝² : ∀ (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✝)
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:
by rw [← IsAddKleinFour.card_four (G := G)]; congr!

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

Goal state before:
pp: case pos
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : x = 1
hy : y = 1
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]

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

Goal state before:
pp: case neg
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : x = 1
hy : ¬y = 1
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]

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

Goal state before:
pp: case pos
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : y = 1
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]

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

Goal state before:
pp: case neg
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : ¬y = 1
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]

Goal state after:
case neg
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : ¬y = 1
⊢ e (x * y) = e x * e y
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ Submonoid.closure (Set.range ⇑inl ∪ Set.range ⇑inr) = Submonoid.map mk (Submonoid.closure (Set.range of))

Tactic:
MonoidHom.map_mclosure,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ Submonoid.closure (Set.range ⇑inl ∪ Set.range ⇑inr) = Submonoid.closure (⇑mk '' Set.range of)
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (toProd x).1 = fst x

Tactic:
← fst_comp_toProd

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (toProd x).1 = ((MonoidHom.fst M N).comp toProd) x
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: α : Type u_1
rels : Set (FreeGroup α)
this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of
⊢ Subgroup.map (QuotientGroup.mk' (Subgroup.normalClosure rels)) ⊤ = ⊤

Tactic:
← MonoidHom.range_eq_map

Goal state after:
α : Type u_1
rels : Set (FreeGroup α)
this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of
⊢ (QuotientGroup.mk' (Subgroup.normalClosure rels)).range = ⊤
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
this : cs.simple = ⇑cs.mulEquiv.symm ∘ PresentedGroup.of
⊢ Subgroup.map cs.mulEquiv.symm.toMonoidHom ⊤ = ⊤

Tactic:
← MonoidHom.range_eq_map

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
this : cs.simple = ⇑cs.mulEquiv.symm ∘ PresentedGroup.of
⊢ cs.mulEquiv.symm.toMonoidHom.range = ⊤
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.length w ≤ cs.length w⁻¹

Tactic:
rcases cs.exists_isReduced w⁻¹ with ⟨ω, hω, h'ω⟩

Goal state after:
case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
ω : List B
hω : cs.IsReduced ω
h'ω : w⁻¹ = cs.wordProd ω
⊢ cs.length w ≤ cs.length w⁻¹
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
⊢ cs.length (cs.wordProd ω) = cs.length (cs.wordProd (take j ω) * cs.wordProd (drop j ω))

Tactic:
rw [← cs.wordProd_append, ω.take_append_drop j]

Goal state after: