mathlib-initiative/mathlib-tactics huggingface dataset:
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; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
⊢ ⁅X, ⁅Y, Z⁆⁆ = ⁅⁅X, Y⁆, Z⁆ + ⁅Y, ⁅X, Z⁆⁆

Tactic:
ext1

Goal state after:
𝕜 : 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; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y Z : LeftInvariantDerivation I G
f✝ : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ⁅X, ⁅Y, Z⁆⁆ f✝ = (⁅⁅X, Y⁆, Z⁆ + ⁅Y, ⁅X, Z⁆⁆) f✝
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; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
Y Z : LeftInvariantDerivation I G
⊢ ⁅Y, r • Z⁆ = r • ⁅Y, Z⁆

Tactic:
ext1

Goal state after:
𝕜 : 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; 𝓘(𝕜, 𝕜), 𝕜⟯
r : 𝕜
Y Z : LeftInvariantDerivation I G
f✝ : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ⁅Y, r • Z⁆ f✝ = (r • ⁅Y, Z⁆) f✝
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_sub hg hg']
  rfl

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

Goal state before:
pp: case hxV
𝕜 : 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 t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ V₁ y = V y

Tactic:
exact hVy

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

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'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
y₀ : M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
hV : ContMDiffWithinAt I' I'.tangent m (fun x ↦ ⟨x, V x⟩) t y₀
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hy₀ : f x₀ = y₀
⊢ ContMDiffWithinAt I I.tangent m (fun x ↦ ⟨x, mpullbackWithin I I' f V s x⟩) s x₀

Tactic:
subst hy₀
  exact ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem hV hf hf' hx₀ hs hmn hst

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

Goal state before:
pp: case mem_codChart_source
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
H : Type u_6
H' : Type u_7
G : Type u_8
G' : Type u_9
inst✝²⁴ : NontriviallyNormedField 𝕜
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace 𝕜 E
inst✝²¹ : NormedAddCommGroup E'
inst✝²⁰ : NormedSpace 𝕜 E'
inst✝¹⁹ : NormedAddCommGroup F
inst✝¹⁸ : NormedSpace 𝕜 F
inst✝¹⁷ : NormedAddCommGroup F'
inst✝¹⁶ : NormedSpace 𝕜 F'
inst✝¹⁵ : TopologicalSpace H
inst✝¹⁴ : TopologicalSpace H'
inst✝¹³ : TopologicalSpace G
inst✝¹² : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
M : Type u_10
M' : Type u_11
N : Type u_12
N' : Type u_13
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : ChartedSpace H' M'
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
inst✝³ : IsManifold I n M
inst✝² : IsManifold I' n M'
inst✝¹ : IsManifold J n N
inst✝ : IsManifold J' n N'
Q : (M' → N') → OpenPartialHomeomorph M' H' → OpenPartialHomeomorph N' G' → Prop
R : (M × M' → N × N') → OpenPartialHomeomorph (M × M') (H × H') → OpenPartialHomeomorph (N × N') (G × G') → Prop
hf : LiftSourceTargetPropertyAt I J n f x P
g : M' → N'
x' : M'
hg : LiftSourceTargetPropertyAt I' J' n g x' Q
h :
  ∀ {f : M → N} {φ₁ : OpenPartialHomeomorph M H} {ψ₁ : OpenPartialHomeomorph N G} {g : M' → N'}
    {φ₂ : OpenPartialHomeomorph M' H'} {ψ₂ : OpenPartialHomeomorph N' G'},
    P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
⊢ Prod.map f g (x, x') ∈ (hf.codChart.prod hg.codChart).source

Tactic:
simp [mem_codChart_source hf, mem_codChart_source hg]

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

Goal state before:
pp: case domChart_mem_maximalAtlas
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
H : Type u_6
H' : Type u_7
G : Type u_8
G' : Type u_9
inst✝²⁴ : NontriviallyNormedField 𝕜
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace 𝕜 E
inst✝²¹ : NormedAddCommGroup E'
inst✝²⁰ : NormedSpace 𝕜 E'
inst✝¹⁹ : NormedAddCommGroup F
inst✝¹⁸ : NormedSpace 𝕜 F
inst✝¹⁷ : NormedAddCommGroup F'
inst✝¹⁶ : NormedSpace 𝕜 F'
inst✝¹⁵ : TopologicalSpace H
inst✝¹⁴ : TopologicalSpace H'
inst✝¹³ : TopologicalSpace G
inst✝¹² : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
M : Type u_10
M' : Type u_11
N : Type u_12
N' : Type u_13
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : ChartedSpace H' M'
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
inst✝³ : IsManifold I n M
inst✝² : IsManifold I' n M'
inst✝¹ : IsManifold J n N
inst✝ : IsManifold J' n N'
Q : (M' → N') → OpenPartialHomeomorph M' H' → OpenPartialHomeomorph N' G' → Prop
R : (M × M' → N × N') → OpenPartialHomeomorph (M × M') (H × H') → OpenPartialHomeomorph (N × N') (G × G') → Prop
hf : LiftSourceTargetPropertyAt I J n f x P
g : M' → N'
x' : M'
hg : LiftSourceTargetPropertyAt I' J' n g x' Q
h :
  ∀ {f : M → N} {φ₁ : OpenPartialHomeomorph M H} {ψ₁ : OpenPartialHomeomorph N G} {g : M' → N'}
    {φ₂ : OpenPartialHomeomorph M' H'} {ψ₂ : OpenPartialHomeomorph N' G'},
    P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
⊢ hf.domChart.prod hg.domChart ∈ IsManifold.maximalAtlas (I.prod I') n (M × M')

Tactic:
exact IsManifold.mem_maximalAtlas_prod
      (domChart_mem_maximalAtlas hf) (domChart_mem_maximalAtlas hg)

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
⊢ ContMDiffOn 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y) ↔ ContMDiff (𝓡∂ 1) I n f

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ hf.comp_contMDiffOn contMDiffOn_projIcc⟩
  convert! hf.comp_contMDiff (contMDiff_subtypeVal_Icc (x := x) (y := y)) (fun z ↦ z.2)
  ext z
  simp

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
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(ℝ ∙ v)ᗮ := (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
⊢ (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • ↑((2 / (1 - a)) • y) +
      (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v =
    ↑x

Tactic:
have pythag : 1 = a ^ 2 + ‖y‖ ^ 2 := by
    have hvy' : ⟪a • v, y⟫_ℝ = 0 := by simp only [inner_smul_left, hvy, mul_zero]
    convert! norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ hvy' using 2
    · simp [← split]
    · simp [norm_smul, hv, ← sq, sq_abs]
    · exact sq _

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(ℝ ∙ v)ᗮ := (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
pythag : 1 = a ^ 2 + ‖y‖ ^ 2
⊢ (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • ↑((2 / (1 - a)) • y) +
      (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v =
    ↑x
Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic

Goal state before:
pp: case mp
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
t₀ : ℝ
h : ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt% γ y (ContinuousLinearMap.smulRight 1 (v (γ y)))
⊢ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s

Tactic:
obtain ⟨s, hs, h⟩ := h

Goal state after:
case mp
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
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : ∀ y ∈ s, HasMFDerivAt% γ y (ContinuousLinearMap.smulRight 1 (v (γ y)))
⊢ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : ↑(sphere 0 1)
⊢ v = - -v

Tactic:
ext1

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : ↑(sphere 0 1)
⊢ ↑v = ↑(- -v)
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ ∀ (x : { x // x ∈ sphere 0 1 }) (y : E),
    ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) x).symm)
      ((extChartAt (𝓡 n) x).target ∩ ↑(extChartAt (𝓡 n) x).symm ⁻¹' Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y).source)

Tactic:
intro v _

Goal state after:
case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : { x // x ∈ sphere 0 1 }
y✝ : E
⊢ ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y✝) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) v).symm)
    ((extChartAt (𝓡 n) v).target ∩ ↑(extChartAt (𝓡 n) v).symm ⁻¹' Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y✝).source)
Module: Mathlib.MeasureTheory.Constructions.UnitInterval

Goal state before:
pp: ⊢ map σ volume = volume

Tactic:
ext s hs

Goal state after:
s : Set ↑I
hs : MeasurableSet s
⊢ (map σ volume) s = volume s
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
F : Type u_5
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F V)
inst✝⁹ : (x : M) → AddCommGroup (V x)
inst✝⁸ : (x : M) → Module 𝕜 (V x)
inst✝⁷ : (x : M) → TopologicalSpace (V x)
inst✝⁶ : FiberBundle F V
inst✝⁵ : VectorBundle 𝕜 F V
inst✝⁴ : ContMDiffVectorBundle 1 F V I
e : Trivialization F TotalSpace.proj
inst✝³ : MemTrivializationAtlas e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
k : ℕ∞ω
inst✝² : FiniteDimensional 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : ContMDiffVectorBundle k F V I
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) k (fun x ↦ ⟨x, s x⟩) e.baseSet ↔
    ∀ (i : ι), ContMDiffOn I 𝓘(𝕜, 𝕜) k ((LinearMap.piApply (Trivialization.localFrameCoeff I e b i)) s) e.baseSet

Tactic:
by
  rw [contMDiffOn_iff_localFrameCoeff b e.open_baseSet (subset_refl _)]

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
x✝ : M
hσ : MDiffAt (T% σ✝) x✝
hσ' : MDiffAt (T% σ'✝) x✝
hx : x✝ ∈ s
⊢ cov (σ✝ + σ'✝) x✝ + (A x✝) ((σ✝ + σ'✝) x✝) = cov σ✝ x✝ + (A x✝) (σ✝ x✝) + (cov σ'✝ x✝ + (A x✝) (σ'✝ x✝))

Tactic:
by
    simp [hcov.add hσ hσ']
    abel

Goal state after:
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
hδ : (r' ^ 2)⁻¹ < 1 - δ * C
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' x - g' y‖ ≤ δ
v : E y
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y) v
hgy : ((g y) v) v = ((g' y) w) w
hgx : ((g x) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) = ((g' x) w) w
⊢ δ * C * ((g x) (G.symm w)) (G.symm w) + ((g' y) w) w = δ * C * ((g' x) w) w + ((g' y) w) w

Tactic:
by
      rw [← hgx]; rfl

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

Goal state before:
pp: case inr.a.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ r m ^ lcm n 2 = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_r]
      refine Nat.dvd_trans ⟨gcd n m.val, ?_⟩ (dvd_lcm_left n 2)
      exact (Nat.div_mul_cancel (Nat.gcd_dvd_left n m.val)).symm

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ card ↑{x | Commute x.1 x.2} = card (M × M) ↔ IsMulCommutative M

pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card M) ^ 2 ≠ 0

Tactic:
set_fintype_card_eq_univ_iff,

Goal state after:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ {x | Commute x.1 x.2} = Set.univ ↔ IsMulCommutative M

M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card M) ^ 2 ≠ 0
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ fst.prod snd = toProd

Tactic:
ext1

Goal state after:
case h₁
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (fst.prod snd).comp inl = toProd.comp inl

case h₂
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (fst.prod snd).comp inr = toProd.comp inr
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ Submonoid.closure (⋃ a, range fun b ↦ (f ⟨a, b⟩.fst) ⟨a, b⟩.snd) = ⨆ i, MonoidHom.mrange (f i)

Tactic:
Submonoid.closure_iUnion

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ ⨆ i, Submonoid.closure (range fun b ↦ (f ⟨i, b⟩.fst) ⟨i, b⟩.snd) = ⨆ i, MonoidHom.mrange (f i)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case mul_left
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
one : motive 1
mul : ∀ {i : ι} (m : M i) (x : CoprodI M), motive x → motive (of m * x)
x : CoprodI M
hx : x ∈ ⋃ i, range ⇑of
y : CoprodI M
ihy : motive y
⊢ motive (x * y)

Tactic:
obtain ⟨i, m, rfl⟩ : ∃ (i : ι) (m : M i), of m = x := by simpa using hx

Goal state after:
case mul_left
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
one : motive 1
mul : ∀ {i : ι} (m : M i) (x : CoprodI M), motive x → motive (of m * x)
y : CoprodI M
ihy : motive y
i : ι
m : M i
hx : of m ∈ ⋃ i, range ⇑of
⊢ motive (of m * y)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case one
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
N : Type u_3
inst✝¹ : Monoid N
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
⊢ MulOpposite.unop ((lift fun i ↦ (MonoidHom.op of).comp (MulEquiv.inv' (G i)).toMonoidHom) 1) * 1 = 1

Tactic:
map_one,

Goal state after:
case one
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
N : Type u_3
inst✝¹ : Monoid N
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
⊢ MulOpposite.unop 1 * 1 = 1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : p.head = 1
⊢ p.tail.prod = of 1 * p.tail.prod

Tactic:
map_one,

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : p.head = 1
⊢ p.tail.prod = 1 * p.tail.prod
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
i i' : B
m : ℕ
⊢ alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m

Tactic:
induction m generalizing i i' with

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

Goal state before:
pp: B : Type u_1
i i' : B
m : ℕ
⊢ (alternatingWord i i' m).length = m

Tactic:
induction m generalizing i i' with

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
motive : Word M → Sort u_4
empty : motive Word.empty
cons :
  (i : ι) → (m : M i) → (w : Word M) → (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons m w h1 h2)
w : List ((i : ι) × M i)
h1 : ∀ l ∈ w, l.snd ≠ 1
h2 : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w
⊢ motive { toList := w, ne_one := h1, chain_ne := h2 }

Tactic:
induction w with

Goal state after:
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
w : W
i : B
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
rcases (cs.length_mul_simple_ne w i).lt_or_gt with h | h <;> rw [← Nat.add_one_le_iff] at h

Goal state after:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length (w * cs.simple i) + 1 ≤ cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length w + 1 ≤ cs.length (w * cs.simple i)
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
⊢ w.toList.getLast? = some ⟨j, w.last⟩

Tactic:
rw [← Option.mem_def]
  induction w
  · rw [Option.mem_def]
    rfl
  · exact List.mem_getLast?_append_of_mem_getLast? (by assumption)

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

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 : ℕ
hj✝ : j < (cs.rightInvSeq ω).length
hj : j < ω.length
ht : (cs.rightInvSeq ω)[j] ∈ cs.rightInvSeq ω
⊢ (ω.eraseIdx j).length < ω.length

Tactic:
rw [← List.length_eraseIdx_add_one hj]; exact lt_add_one _

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

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 : ℕ
hj✝ : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : (cs.leftInvSeq ω)[j] ∈ cs.leftInvSeq ω
⊢ (ω.eraseIdx j).length < ω.length

Tactic:
rw [← List.length_eraseIdx_add_one hj]; exact lt_add_one _

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
x : M i
hnotone : x * w.head ≠ 1
⊢ (replaceHead (x * w.head) hnotone w).prod = of x * w.prod

Tactic:
induction w with

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
x : DivisibleHull M
⊢ (a * b) • x = a • b • x

Tactic:
induction x with | mk m s
    simp_rw [qsmul_mk, mk_eq_mk]
    use 1
    suffices ((a * b).num * a.den * b.den * s) • m = (a.num * b.num * (a * b).den * s) • m by
      convert! this using 1
      all_goals
      simp [← natCast_zsmul, smul_smul]
      ring_nf
    rw [Rat.mul_num_den']

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s t : Set α
a b : α
⊢ b ∈ doubleCoset a s t ↔ ∃ x ∈ s, ∃ y ∈ t, b = x * a * y

Tactic:
simp only [doubleCoset_eq_image2, Set.mem_image2, eq_comm]

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a h : G
hh : h ∈ ↑H
k : G
hk : k ∈ ↑K
hb : h * a * k ∈ doubleCoset a ↑H ↑K
⊢ ↑H * {h * a * k} * ↑K = ↑H * {a} * ↑K

Tactic:
← Set.singleton_mul_singleton,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a h : G
hh : h ∈ ↑H
k : G
hk : k ∈ ↑K
hb : h * a * k ∈ doubleCoset a ↑H ↑K
⊢ ↑H * ({h * a} * {k}) * ↑K = ↑H * {a} * ↑K