mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Similarity

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
have h_cos := law_cos a b c

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a c * dist a c = dist a b * dist a b + dist c b * dist c b - 2 * dist a b * dist c b * Real.cos (∠ a b c)
⊢ ∠ a b c = ∠ a' b' c'
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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : {i₂, i₃}ᶜ = {i₁}
he : {i₁}ᶜ = {i₂, i₃}
⊢ altitude t i₁ = mongePlane t i₂ i₃

Tactic:
mongePlane_def,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : {i₂, i₃}ᶜ = {i₁}
he : {i₁}ᶜ = {i₂, i₃}
⊢ altitude t i₁ =
    mk' (Finset.centroid ℝ {i₂, i₃}ᶜ t.points) (ℝ ∙ (t.points i₂ -ᵥ t.points i₃))ᗮ ⊓ affineSpan ℝ (Set.range t.points)
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: P : Type u_2
inst✝ : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
⊢ s.power p ≤ 0 ↔ dist p s.center ≤ s.radius

Tactic:
by
  rw [power, sub_nonpos, pow_le_pow_iff_left₀ dist_nonneg hr two_ne_zero]

Goal state after:
Module: Mathlib.Geometry.Group.Growth.QuotientInter

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x ↦ x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' ↑A ^ m)
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' ↑A ^ m → φ a ∈ A ^ m
hπφ : ∀ {a : G ⧸ H}, a ∈ ⇑π '' ↑A ^ m → π (φ a) = a
⊢ #(image φ (image (⇑π) (A ^ m))) * #({x ∈ A ^ n | x ∈ H}) ≤ #(image φ (image (⇑π) (A ^ m)) * {x ∈ A ^ n | x ∈ H})

Tactic:
rw [Finset.card_mul_iff.2]
      simp only [Set.InjOn, coe_image, coe_pow, coe_filter, Set.mem_prod, Set.mem_image,
        exists_exists_and_eq_and, Set.mem_ofPred_eq, and_imp, forall_exists_index, Prod.forall,
        Prod.mk.injEq]
      rintro _ a₁ b₁ hb₁ rfl - ha₁ _ a₂ b₂ hb₂ rfl - ha₂ hab
      have hπa₁ : π a₁ = 1 := (QuotientGroup.eq_one_iff _).2 ha₁
      have hπa₂ : π a₂ = 1 := (QuotientGroup.eq_one_iff _).2 ha₂
      have hπb : π b₁ = π b₂ := by
        simpa [hπφ, Set.mem_image_of_mem π, hb₁, hb₂, hπa₁, hπa₂] using congr(π $hab)
      simp_all

Goal state after:
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
⊢ ⟨fun x ↦ (algebraMap 𝕜 A) 1, ⋯⟩ = 1

Tactic:
ext; exact (algebraMap 𝕜 A).map_one

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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c
this : e.target ∈ 𝓝 (↑e c)
y : E
hyt : y ∈ e.target
⊢ MDiffAt f (↑e.symm y) → DifferentiableAt ℂ (f ∘ ↑e.symm) y

Tactic:
hy₂

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c
this : e.target ∈ 𝓝 (↑e c)
y : E
hyt : y ∈ e.target
hy₂ : MDiffAt f (↑e.symm y)
⊢ DifferentiableAt ℂ (f ∘ ↑e.symm) y
Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g✝ h : G
r : 𝕜
X Y : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
g : G
⊢ (𝒅ₕ ⋯) ((Derivation.evalAt 1) 0) = (Derivation.evalAt g) 0

Tactic:
simp only [map_zero]

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
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
⊢ (MDiffAt[s] fun x ↦
        ↑((extChartAt IB (f x₀).proj).prod (PartialEquiv.refl F))
          (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)))
      x₀ ↔
    (MDiffAt[s] fun x ↦ ↑(extChartAt IB (f x₀).proj) (f x).proj) x₀ ∧
      (MDiffAt[s] fun x ↦
          ↑(extChartAt 𝓘(𝕜, F) (↑(trivializationAt F E (f x₀).proj) (f x₀)).2)
            (↑(trivializationAt F E (f x₀).proj) (f x)).2)
        x₀

Tactic:
PartialEquiv.prod_coe,

Goal state after:
𝕜 : 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
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
⊢ (MDiffAt[s] fun x ↦
        (↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).1,
          ↑(PartialEquiv.refl F) (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).2))
      x₀ ↔
    (MDiffAt[s] fun x ↦ ↑(extChartAt IB (f x₀).proj) (f x).proj) x₀ ∧
      (MDiffAt[s] fun x ↦
          ↑(extChartAt 𝓘(𝕜, F) (↑(trivializationAt F E (f x₀).proj) (f x₀)).2)
            (↑(trivializationAt F E (f x₀).proj) (f x)).2)
        x₀
Module: Mathlib.Topology.VectorBundle.Hom

Goal state before:
pp: 𝕜₁ : Type u_1
inst✝²³ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝²² : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝²¹ : NormedAddCommGroup F₁
inst✝²⁰ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁹ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁸ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹⁷ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹⁶ : NormedAddCommGroup F₂
inst✝¹⁵ : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝¹⁴ : (x : B) → AddCommGroup (E₂ x)
inst✝¹³ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝¹² : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹¹ : TopologicalSpace B
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝¹⁰ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁷ : FiberBundle F₂ E₂
inst✝⁶ : RingHomIsometric σ
inst✝⁵ : VectorBundle 𝕜₁ F₁ E₁
inst✝⁴ : VectorBundle 𝕜₂ F₂ E₂
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
⊢ ContinuousOn (continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂') (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
have h₁ := (compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)).continuous

Goal state after:
𝕜₁ : Type u_1
inst✝²³ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝²² : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝²¹ : NormedAddCommGroup F₁
inst✝²⁰ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁹ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁸ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹⁷ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹⁶ : NormedAddCommGroup F₂
inst✝¹⁵ : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝¹⁴ : (x : B) → AddCommGroup (E₂ x)
inst✝¹³ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝¹² : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹¹ : TopologicalSpace B
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝¹⁰ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁷ : FiberBundle F₂ E₂
inst✝⁶ : RingHomIsometric σ
inst✝⁵ : VectorBundle 𝕜₁ F₁ E₁
inst✝⁴ : VectorBundle 𝕜₂ F₂ E₂
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
h₁ : Continuous ⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂))
⊢ ContinuousOn (continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂') (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt (T% t) x₀
⊢ (MDiffAt fun x ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀

Tactic:
by
  simp_rw [← mdifferentiableWithinAt_univ] at ht' ⊢
  exact .sum_section_of_locallyFinite ht ht'

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
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
s : Set M
x : M
f : M → E'
h : MDiffAt[s] f x
⊢ d[s] f x =
    fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
convert! h.mfderivWithin

Goal state after:
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
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ fun x ↦ g * h * x
⊢ ((mfderiv% fun b ↦ g⁻¹ * b) (g * h)) (((mfderiv% fun x ↦ g * h * x) 1) v) =
    ((mfderiv% fun b ↦ g⁻¹ * b) (g * h * 1) ∘SL (mfderiv% fun x ↦ g * h * x) 1) v

Tactic:
congr 2
    simp

Goal state after:
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
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
fg : G → TangentBundle I G := fun g ↦ ⟨g, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := fun x ↦ ⟨1, v⟩
⊢ ContMDiff I I.tangent (minSmoothness 𝕜 2) fun g ↦ ⟨g, mulInvariantVectorField v g⟩

Tactic:
have sfv : CMDiff (minSmoothness 𝕜 2) fv := contMDiff_const

Goal state after:
𝕜 : 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
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
fg : G → TangentBundle I G := fun g ↦ ⟨g, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := fun x ↦ ⟨1, v⟩
sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv
⊢ ContMDiff I I.tangent (minSmoothness 𝕜 2) fun g ↦ ⟨g, mulInvariantVectorField v g⟩
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: case pos
𝕜 : 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
⊢ IsImmersion I J n f

Tactic:
IsImmersion

Goal state after:
case pos
𝕜 : 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
⊢ ∃ F x x_1, IsImmersionOfComplement F I J n f
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁵ : TopologicalSpace H
G : Type u_9
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersionOfComplement F I J n f
⊢ IsImmersion I J n f

Tactic:
by_cases! hM : IsEmpty M
  · rw [IsImmersion]
    use PUnit, by infer_instance, by infer_instance
    exact fun x ↦ (IsEmpty.false x).elim
  inhabit M
  let x : M := Inhabited.default
  use (h x).smallComplement, by infer_instance, by infer_instance
  exact (IsImmersionOfComplement.congr_F (h x).smallEquiv).mp h

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
n : ℕ∞ω
⊢ ContDiffOn ℝ n (stereoToFun v) {x | ((innerSL ℝ) v) x ≠ 1}

Tactic:
refine ContDiffOn.fun_smul ?_ (ℝ ∙ v)ᗮ.orthogonalProjectionOnto.contDiff.contDiffOn

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
⊢ ContDiffOn ℝ n (fun i ↦ 2 / (1 - ((innerSL ℝ) v) i)) {x | ((innerSL ℝ) v) x ≠ 1}
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ ContMDiff (𝓡 n) 𝓘(ℝ, E) m Subtype.val

Tactic:
rw [contMDiff_iff]
  constructor
  · exact continuous_subtype_val
  · intro v _
    let U : _ ≃ₗᵢ[ℝ] _ :=
      (-- Again, partially removing type ascription...
          OrthonormalBasis.fromOrthogonalSpanSingleton
          n (ne_zero_of_mem_unit_sphere (-v))).repr
    exact
      ((contDiff_stereoInvFunAux.comp (ℝ ∙ (-v : E))ᗮ.subtypeL.contDiff).comp
          U.symm.contDiff).contDiffOn

Goal state after:
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
val✝ : ℝ
ht : val✝ ∈ Ioo a b
⊢ ContinuousAt γ val✝

Tactic:
exact hγ.continuousWithinAt ht |>.continuousAt (Ioo_mem_nhds ht.1 ht.2)

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
⊢ mpullbackWithin I I' f (mlieBracketWithin I' V W t') s' x₀ =
    mlieBracketWithin I (mpullbackWithin I I' f V s') (mpullbackWithin I I' f W s') s' x₀

Tactic:
apply mpullbackWithin_mlieBracketWithin_aux (t := t') (hV.mono inter_subset_left)
      (hW.mono inter_subset_left) (hu.inter u_open) u_smooth ⟨hx₀, x₀u⟩ inter_subset_right
      (fun y hy ↦ ⟨ut hy, maps_u hy⟩)
    apply hsymm.congr_set
    have : (extChartAt I x₀).symm ⁻¹' u ∈ 𝓝 (extChartAt I x₀ x₀) := by
      apply (continuousAt_extChartAt_symm x₀).preimage_mem_nhds
      apply u_open.mem_nhds (by simpa using x₀u)
    filter_upwards [this] with y hy
    change (y ∈ (extChartAt I x₀).symm ⁻¹' s ∩ range I) =
      (y ∈ (extChartAt I x₀).symm ⁻¹' (s ∩ u) ∩ range I)
    simp [-extChartAt, hy]

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

Goal state before:
pp: case mpr
𝕜 : 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
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
⊢ IsUnit ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f)

Tactic:
have hf' : f ⟨x, hxU⟩ ≠ 0 := by
      convert! hf
      exact (smoothSheafCommRing.eval_germ U x hxU f).symm

Goal state after:
case mpr
𝕜 : 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
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
⊢ IsUnit ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f)