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

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
hs :
  SignType.sign
      (s.touchpointWeights signs i j * ‖s.points j -ᵥ ↑((s.faceOpposite j).orthogonalProjectionSpan (s.points j))‖) =
    SignType.sign (s.excenterWeights signs j)
⊢ SignType.sign (s.touchpointWeights signs i j) = SignType.sign (s.excenterWeights signs j)

Tactic:
rw [← hs, sign_mul]

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
hs :
  SignType.sign
      (s.touchpointWeights signs i j * ‖s.points j -ᵥ ↑((s.faceOpposite j).orthogonalProjectionSpan (s.points j))‖) =
    SignType.sign (s.excenterWeights signs j)
⊢ SignType.sign (s.touchpointWeights signs i j) =
    SignType.sign (s.touchpointWeights signs i j) *
      SignType.sign ‖s.points j -ᵥ ↑((s.faceOpposite j).orthogonalProjectionSpan (s.points j))‖
Module: Mathlib.Geometry.Euclidean.Congruence

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₂
h : ∠ a b c = ∠ a' b' c'
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
⊢ dist a c * dist a c = dist a' c' * dist a' c'

Tactic:
EuclideanGeometry.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₂
h : ∠ a b c = ∠ a' b' c'
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' 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) = dist a' c' * dist a' c'
Module: Mathlib.Geometry.Euclidean.Inversion.Calculus

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x ↦ c + x) x ≠ c
this :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y ↦ y⁻¹) ∘ fun x ↦ ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      (R ^ 2 •
            -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
              2 • (innerSL ℝ) (_root_.id (c + x) - c) ∘SL ContinuousLinearMap.id ℝ F).smulRight
        (_root_.id (c + x) - c))
    (c + x)
⊢ ((‖x‖ ^ 2) ^ 2)⁻¹ * ‖x‖ ^ 2 = (‖x‖ ^ 2)⁻¹

Tactic:
rw [← div_eq_inv_mul, sq (‖x‖ ^ 2), div_self_mul_self']

Goal state after:
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
n : ℕ
s₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
⊢ (↑(n + 1) / ↑(n - 1)) • (Finset.centroid ℝ univ s₁.points -ᵥ s₁.circumcenter) +ᵥ s₁.circumcenter =
    (↑(n + 1) / ↑(n - 1)) • (Finset.centroid ℝ univ s₂.points -ᵥ s₂.circumcenter) +ᵥ s₂.circumcenter

Tactic:
centroid_eq_of_range_eq h,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
⊢ (↑(n + 1) / ↑(n - 1)) • (Finset.centroid ℝ univ s₂.points -ᵥ s₁.circumcenter) +ᵥ s₁.circumcenter =
    (↑(n + 1) / ↑(n - 1)) • (Finset.centroid ℝ univ s₂.points -ᵥ s₂.circumcenter) +ᵥ s₂.circumcenter
Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy

Goal state before:
pp: V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : dist d a = dist a p / dist b p * dist b c
⊢ dist d p = dist a p * dist c p / dist b p

Tactic:
simp [field, hmul]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
⊢ ↑X ^ (n - 1) = ↑(closure ↑X)

Tactic:
obtain rfl | hm₀ := m.eq_zero_or_pos

Goal state after:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
hmn : 0 ≤ n
hm : ↑X ^ (0 - 1) = ↑(closure ↑X)
⊢ ↑X ^ (n - 1) = ↑(closure ↑X)

case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ ↑X ^ (n - 1) = ↑(closure ↑X)
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₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ t₁.points i₁ ≠ t₂.points j₂ ∧
    t₁.points i₁ ∈ affineSpan ℝ (Set.range t₂.points) ∧
      t₁.points i₁ -ᵥ t₂.points j₂ ∈ (affineSpan ℝ (t₂.points '' {j₂}ᶜ)).directionᗮ

Tactic:
rw [h₂]

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₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ t₁.points i₁ ≠ t₁.points i₂ ∧
    t₁.points i₁ ∈ affineSpan ℝ (Set.range t₂.points) ∧
      t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ (t₂.points '' {j₂}ᶜ)).directionᗮ
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₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)
⊢ t₁.points i₁ ∈ affineSpan ℝ (Set.range t₂.points) ∧
    t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ (t₂.points '' {j₂}ᶜ)).directionᗮ

Tactic:
rw [he]

Goal state after:
case right
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)
⊢ t₁.points i₁ ∈ affineSpan ℝ (Set.range t₁.points) ∧
    t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ (t₂.points '' {j₂}ᶜ)).directionᗮ
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 : ℕ∞ω
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : ContMDiffMul I' n G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : ContMDiffMul I'' n G''
φ : G' →* G''
hφ : ContMDiff I' I'' n ⇑φ
f g : C^n⟮I, N; I', G'⟯
x : N
⊢ ⟨⇑φ ∘ ⇑(f * g), ⋯⟩ x = (⟨⇑φ ∘ ⇑f, ⋯⟩ * ⟨⇑φ ∘ ⇑g, ⋯⟩) x

Tactic:
change φ (f x * g x) = φ (f x) * φ (g x)

Goal state after:
𝕜 : 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 : ℕ∞ω
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : ContMDiffMul I' n G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : ContMDiffMul I'' n G''
φ : G' →* G''
hφ : ContMDiff I' I'' n ⇑φ
f g : C^n⟮I, N; I', G'⟯
x : N
⊢ φ (f x * g x) = φ (f x) * φ (g x)
Module: Mathlib.Geometry.Manifold.VectorBundle.Hom

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝²⁷ : NontriviallyNormedField 𝕜
inst✝²⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁵ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁴ : NormedAddCommGroup F₁
inst✝²³ : NormedSpace 𝕜 F₁
inst✝²² : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²¹ : (x : B) → TopologicalSpace (E₁ x)
inst✝²⁰ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁸ : NormedAddCommGroup F₂
inst✝¹⁷ : NormedSpace 𝕜 F₂
inst✝¹⁶ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁵ : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_8
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : VectorBundle 𝕜 F₁ E₁
inst✝⁷ : FiberBundle F₂ E₂
inst✝⁶ : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁵ : ContMDiffVectorBundle n F₁ E₁ IB
inst✝⁴ : ContMDiffVectorBundle n F₂ E₂ IB
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
⊢ ContMDiffOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) n (continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
have h₁ := contMDiffOn_coordChangeL (IB := IB) e₁' e₁ (n := n)

Goal state after:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝²⁷ : NontriviallyNormedField 𝕜
inst✝²⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁵ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁴ : NormedAddCommGroup F₁
inst✝²³ : NormedSpace 𝕜 F₁
inst✝²² : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²¹ : (x : B) → TopologicalSpace (E₁ x)
inst✝²⁰ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁸ : NormedAddCommGroup F₂
inst✝¹⁷ : NormedSpace 𝕜 F₂
inst✝¹⁶ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁵ : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_8
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : VectorBundle 𝕜 F₁ E₁
inst✝⁷ : FiberBundle F₂ E₂
inst✝⁶ : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁵ : ContMDiffVectorBundle n F₁ E₁ IB
inst✝⁴ : ContMDiffVectorBundle n F₂ E₂ IB
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
h₁ : ContMDiffOn IB 𝓘(𝕜, F₁ →L[𝕜] F₁) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)
⊢ ContMDiffOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) n (continuousLinearMapCoordChange (RingHom.id 𝕜) 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
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
y : B
hy : y ∈ univ
U : Set B
hu : U ∈ 𝓝 y
hfin : {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ U).Nonempty}.Finite
x : ι
hx : x ∈ {x | t x y ≠ 0}
⊢ x ∈ {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ U).Nonempty}

Tactic:
rw [Set.mem_ofPred] at hx ⊢

Goal state after:
𝕜 : 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
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
y : B
hy : y ∈ univ
U : Set B
hu : U ∈ 𝓝 y
hfin : {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ U).Nonempty}.Finite
x : ι
hx : t x y ≠ 0
⊢ ((fun i ↦ {x | t i x ≠ 0}) x ∩ U).Nonempty
Module: Mathlib.Topology.VectorBundle.Hom

Goal state before:
pp: 𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B₁) → AddCommGroup (E₁ x)
inst✝¹⁷ : (x : B₁) → Module 𝕜 (E₁ x)
inst✝¹⁶ : NormedAddCommGroup F₁
inst✝¹⁵ : NormedSpace 𝕜 F₁
inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹³ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝¹² : (x : B₂) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B₂) → TopologicalSpace (E₂ x)
inst✝⁶ : TopologicalSpace B₁
inst✝⁵ : TopologicalSpace B₂
inst✝⁴ : TopologicalSpace M
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)
v : (m : M) → E₁ (b₁ m)
hϕ : ContinuousAt (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv : ContinuousAt (fun m ↦ { proj := b₁ m, snd := v m }) m₀
hb₂ : ContinuousAt b₂ m₀
⊢ ContinuousAt (fun m ↦ { proj := b₂ m, snd := (ϕ m) (v m) }) m₀

Tactic:
← continuousWithinAt_univ

Goal state after:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B₁) → AddCommGroup (E₁ x)
inst✝¹⁷ : (x : B₁) → Module 𝕜 (E₁ x)
inst✝¹⁶ : NormedAddCommGroup F₁
inst✝¹⁵ : NormedSpace 𝕜 F₁
inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹³ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝¹² : (x : B₂) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B₂) → TopologicalSpace (E₂ x)
inst✝⁶ : TopologicalSpace B₁
inst✝⁵ : TopologicalSpace B₂
inst✝⁴ : TopologicalSpace M
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)
v : (m : M) → E₁ (b₁ m)
hϕ : ContinuousWithinAt (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) univ m₀
hv : ContinuousWithinAt (fun m ↦ { proj := b₁ m, snd := v m }) univ m₀
hb₂ : ContinuousWithinAt b₂ univ m₀
⊢ ContinuousWithinAt (fun m ↦ { proj := b₂ m, snd := (ϕ m) (v m) }) univ m₀
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
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
g g' : M → F
x : M
hg : MDiffAt g x
hg' : MDiffAt g' x
⊢ d% (g + g') x = d% g x + d% g' x

Tactic:
simp [mvfderiv, mfderiv_add hg 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_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
g g' : M → F
x : M
hg : MDiffAt g x
hg' : MDiffAt g' x
⊢ ↑(NormedSpace.fromTangentSpace (g x + g' x)) ∘SL (mfderiv% g x + mfderiv% g' x) =
    ↑(NormedSpace.fromTangentSpace (g x)) ∘SL mfderiv% g x + ↑(NormedSpace.fromTangentSpace (g' x)) ∘SL mfderiv% g' x
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v + mulInvariantVectorField w) 1 =
    mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v) 1 +
      mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w) 1

Tactic:
mlieBracket_add_right

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
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v) 1 +
      mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w) 1 =
    mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v) 1 +
      mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w) 1

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
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField v x⟩) 1

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
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField w x⟩) 1
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ ⁅u, ⁅v, w⁆⁆ = ⁅⁅u, v⁆, w⁆ + ⁅v, ⁅u, w⁆⁆

Tactic:
simp only [GroupLieAlgebra.bracket_def, mulInvariantVector_mlieBracket]
    apply leibniz_identity_mlieBracket_apply <;>
      exact contMDiff_mulInvariantVectorField _ _

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

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
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : ↑(Icc x y) → M
hf : ContMDiffOn 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y)
⊢ ContMDiff (𝓡∂ 1) I n f

Tactic:
convert! hf.comp_contMDiff (contMDiff_subtypeVal_Icc (x := x) (y := y)) (fun z ↦ z.2)

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
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : ↑(Icc x y) → M
hf : ContMDiffOn 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y)
⊢ f = (f ∘ projIcc x y ⋯) ∘ fun z ↦ ↑z
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

Goal state before:
pp: case e'_10
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
dt : ℝ
hγ : IsMIntegralCurveOn (γ ∘ fun x ↦ x + dt) v {t | t + dt ∈ s}
⊢ γ = (γ ∘ fun x ↦ x + dt) ∘ fun x ↦ x + -dt

Tactic:
ext t
    simp

Goal state after: