mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

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
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁸ : TopologicalSpace (TotalSpace F V)
inst✝⁷ : (x : M) → NormedAddCommGroup (V x)
inst✝⁶ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁵ : FiberBundle F V
cov : CovariantDerivative I F V
inst✝⁴ : VectorBundle ℝ F V
inst✝³ : IsContMDiffRiemannianBundle I 1 F V
inst✝² : ContMDiffVectorBundle 1 F V I
inst✝¹ : IsManifold I 1 M
inst✝ : FiniteDimensional ℝ F
h :
  ∀ {x : M} {X : (x : M) → TangentSpace I x} {σ τ : (x : M) → V x},
    MDiffAt (T% X) x →
      MDiffAt (T% σ) x →
        MDiffAt (T% τ) x →
          ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) =
            (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x +
              (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x
x : M
σ : (x : M) → V x
hσ : MDiffAt (T% σ) x
τ : (x : M) → V x
hτ : MDiffAt (T% τ) x
⊢ (fun A Z x_1 ↦ A (Z x)) ((fun A Z x_1 ↦ A (Z x)) ((fun A Z x_1 ↦ A (Z x)) (cov.derivMetricTensor x) σ hσ) τ hτ) =
    (fun A Z x_1 ↦ A (Z x)) ((fun A Z x_1 ↦ A (Z x)) ((fun A Z x_1 ↦ A (Z x)) (0 x) σ hσ) τ hτ)

Tactic:
;

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
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁸ : TopologicalSpace (TotalSpace F V)
inst✝⁷ : (x : M) → NormedAddCommGroup (V x)
inst✝⁶ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁵ : FiberBundle F V
cov : CovariantDerivative I F V
inst✝⁴ : VectorBundle ℝ F V
inst✝³ : IsContMDiffRiemannianBundle I 1 F V
inst✝² : ContMDiffVectorBundle 1 F V I
inst✝¹ : IsManifold I 1 M
inst✝ : FiniteDimensional ℝ F
h :
  ∀ {x : M} {X : (x : M) → TangentSpace I x} {σ τ : (x : M) → V x},
    MDiffAt (T% X) x →
      MDiffAt (T% σ) x →
        MDiffAt (T% τ) x →
          ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) =
            (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x +
              (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x
x : M
σ : (x : M) → V x
hσ : MDiffAt (T% σ) x
τ : (x : M) → V x
hτ : MDiffAt (T% τ) x
⊢ (fun A Z x_1 ↦ A (Z x)) ((fun A Z x_1 ↦ A (Z x)) ((fun A Z x_1 ↦ A (Z x)) (cov.derivMetricTensor x) σ hσ) τ hτ) =
    (fun A Z x_1 ↦ A (Z x)) ((fun A Z x_1 ↦ A (Z x)) ((fun A Z x_1 ↦ A (Z x)) (0 x) σ hσ) τ hτ)
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
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
⊢ g x • ∑ i ∈ s, f i x • cov i σ x + 1 x • (d% g x).smulRight (σ x) =
    g x • ∑ i ∈ s, f i x • cov i σ x + (d% g x).smulRight (σ x)

Tactic:
;

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
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
⊢ g x • ∑ i ∈ s, f i x • cov i σ x + 1 x • (d% g x).smulRight (σ x) =
    g x • ∑ i ∈ s, f i x • cov i σ x + (d% g x).smulRight (σ x)
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
⊢ ‖g' x - g' y‖ * (‖w‖ * ‖w‖) + ((g' y) w) w ≤ δ * (‖w‖ * ‖w‖) + ((g' y) w) w

Tactic:
;

Goal state after:
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
⊢ ‖g' x - g' y‖ * (‖w‖ * ‖w‖) + ((g' y) w) w ≤ δ * (‖w‖ * ‖w‖) + ((g' y) w) w
Module: Mathlib.Geometry.Manifold.VectorBundle.Pullback

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B) → AddCommMonoid (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_6
inst✝¹² : NormedAddCommGroup EB
inst✝¹¹ : NormedSpace 𝕜 EB
HB : Type u_7
inst✝¹⁰ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁹ : TopologicalSpace B
inst✝⁸ : ChartedSpace HB B
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✝ : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : f b ∈ e.baseSet ∩ e'.baseSet
⊢ ↑(Trivialization.coordChangeL 𝕜 (e.pullback f) (e'.pullback f) b) =
    ((fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ⇑f) b

Tactic:
;

Goal state after:
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B) → AddCommMonoid (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_6
inst✝¹² : NormedAddCommGroup EB
inst✝¹¹ : NormedSpace 𝕜 EB
HB : Type u_7
inst✝¹⁰ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁹ : TopologicalSpace B
inst✝⁸ : ChartedSpace HB B
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✝ : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : f b ∈ e.baseSet ∩ e'.baseSet
⊢ ↑(Trivialization.coordChangeL 𝕜 (e.pullback f) (e'.pullback f) b) =
    ((fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ⇑f) b
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.FG ↥(closure (commutatorSet G))

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.FG ↥(closure (commutatorSet G))
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) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) + ((g' y) w) w

Tactic:
;

Goal state after:
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) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) + ((g' y) w) w
Module: Mathlib.GroupTheory.GroupAction.CardCommute

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Mul α
inst✝ : Infinite α
a₁✝ : α
⊢ ∀ ⦃a₂ : α⦄, (fun a ↦ ⟨(a, a), ⋯⟩) a₁✝ = (fun a ↦ ⟨(a, a), ⋯⟩) a₂ → a₁✝ = a₂

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Mul α
inst✝ : Infinite α
a₁✝ : α
⊢ ∀ ⦃a₂ : α⦄, (fun a ↦ ⟨(a, a), ⋯⟩) a₁✝ = (fun a ↦ ⟨(a, a), ⋯⟩) a₂ → a₁✝ = a₂
Module: Mathlib.GroupTheory.GroupAction.CardCommute

Goal state before:
pp: case inl
G : Type u_3
inst✝ : Group G
val✝ : Fintype G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

pp: case inr
G : Type u_3
inst✝ : Group G
val✝ : Infinite G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

Tactic:
;

Goal state after:
case inl
G : Type u_3
inst✝ : Group G
val✝ : Fintype G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

case inr
G : Type u_3
inst✝ : Group G
val✝ : Infinite G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G
Module: Mathlib.GroupTheory.GroupAction.CardCommute

Goal state before:
pp: case e_a
G : Type u_3
inst✝ : Group G
val✝ : Fintype G
⊢ card (Quotient (MulAction.orbitRel (ConjAct G) G)) = card (ConjClasses G)

Tactic:
;

Goal state after:
case e_a
G : Type u_3
inst✝ : Group G
val✝ : Fintype G
⊢ card (Quotient (MulAction.orbitRel (ConjAct G) G)) = card (ConjClasses G)
Module: Mathlib.GroupTheory.GroupAction.CardCommute

Goal state before:
pp: case e_a
G : Type u_3
inst✝ : Group G
val✝ : Fintype G
⊢ Quotient (MulAction.orbitRel (ConjAct G) G) = ConjClasses G

Tactic:
;

Goal state after:
case e_a
G : Type u_3
inst✝ : Group G
val✝ : Fintype G
⊢ Quotient (MulAction.orbitRel (ConjAct G) G) = ConjClasses G
Module: Mathlib.GroupTheory.GroupAction.CardCommute

Goal state before:
pp: case e_a
G : Type u_3
inst✝ : Group G
val✝ : Fintype G
⊢ MulAction.orbitRel (ConjAct G) G = IsConj.setoid G

Tactic:
;

Goal state after:
case e_a
G : Type u_3
inst✝ : Group G
val✝ : Fintype G
⊢ MulAction.orbitRel (ConjAct G) G = IsConj.setoid G
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
⊢ Nat.card (Additive G) = Nat.card G

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
⊢ Nat.card (Additive G) = Nat.card G
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝¹ : AddGroup G
inst✝ : IsAddKleinFour G
⊢ Nat.card (Multiplicative G) = Nat.card G

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : AddGroup G
inst✝ : IsAddKleinFour G
⊢ Nat.card (Multiplicative G) = Nat.card G
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ #{1} + 1 + 1 + 1 = 4

pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ y ∉ {1}

pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x ∉ {y, 1}

pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x * y ∉ {x, y, 1}

Tactic:
on_goal 4 => simpa using mul_notMem_of_exponent_two (by simp) hx hy hxy

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ #{1} + 1 + 1 + 1 = 4

G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ y ∉ {1}

G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x ∉ {y, 1}
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
h : r 0 = sr 0
⊢ False

Tactic:
;

Goal state after:
n : ℕ
h : r 0 = sr 0
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
⊢ n ≠ 1 ∧ n ≠ 2 → ¬IsMulCommutative (DihedralGroup n)

Tactic:
;

Goal state after:
n : ℕ
⊢ n ≠ 1 ∧ n ≠ 2 → ¬IsMulCommutative (DihedralGroup n)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
h1 : n ≠ 1
h2 : n ≠ 2
⊢ ¬IsMulCommutative (DihedralGroup n)

Tactic:
;

Goal state after:
n : ℕ
h1 : n ≠ 1
h2 : n ≠ 2
⊢ ¬IsMulCommutative (DihedralGroup n)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case pos
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : n = 2
⊢ False

pp: case neg
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : ¬n = 2
⊢ False

Tactic:
· simpa [exponent, card, h2] using h.exponent_eq_card

Goal state after:
case neg
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : ¬n = 2
⊢ False
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: ⊢ (if x : 0 = 0 then [0]
    else
      if x : 0 = 1 then []
      else if Even 0 then 3 :: reciprocalFactors (0 / 2) else 0 % 4 * 0 :: reciprocalFactors (0 / 4 + 1)) =
    [0]

Tactic:
;

Goal state after:
⊢ (if x : 0 = 0 then [0]
    else
      if x : 0 = 1 then []
      else if Even 0 then 3 :: reciprocalFactors (0 / 2) else 0 % 4 * 0 :: reciprocalFactors (0 / 4 + 1)) =
    [0]
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: ⊢ (if x : 1 = 0 then [0]
    else
      if x : 1 = 1 then []
      else if Even 1 then 3 :: reciprocalFactors (1 / 2) else 1 % 4 * 1 :: reciprocalFactors (1 / 4 + 1)) =
    []

Tactic:
;

Goal state after:
⊢ (if x : 1 = 0 then [0]
    else
      if x : 1 = 1 then []
      else if Even 1 then 3 :: reciprocalFactors (1 / 2) else 1 % 4 * 1 :: reciprocalFactors (1 / 4 + 1)) =
    []
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : Group H
b b' : G ≃* FreeGroup ι
hbb' : (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b } = (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b' }
i : ι
⊢ ↑b.symm (FreeGroup.of i) = ↑b'.symm (FreeGroup.of i)

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : Group H
b b' : G ≃* FreeGroup ι
hbb' : (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b } = (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b' }
i : ι
⊢ ↑b.symm (FreeGroup.of i) = ↑b'.symm (FreeGroup.of i)
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
H✝ : Type u_4
inst✝¹ : Group G
inst✝ : Group H✝
b b' : G ≃* FreeGroup ι
hbb' : (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b } = (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b' }
H : ↑b.symm = ↑b'.symm
x : FreeGroup ι
⊢ b.symm x = b'.symm x

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H✝ : Type u_4
inst✝¹ : Group G
inst✝ : Group H✝
b b' : G ≃* FreeGroup ι
hbb' : (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b } = (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b' }
H : ↑b.symm = ↑b'.symm
x : FreeGroup ι
⊢ b.symm x = b'.symm x
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G✝ : Type u_3
H : Type u_4
inst✝² : Group G✝
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
⊢ ∀ (a : X),
    ((lift FreeGroup.of).comp (FreeGroup.lift of)) (FreeGroup.of a) = (MonoidHom.id (FreeGroup X)) (FreeGroup.of a)

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
G✝ : Type u_3
H : Type u_4
inst✝² : Group G✝
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
⊢ ∀ (a : X),
    ((lift FreeGroup.of).comp (FreeGroup.lift of)) (FreeGroup.of a) = (MonoidHom.id (FreeGroup X)) (FreeGroup.of a)
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G✝ : Type u_3
H✝ : Type u_4
inst✝³ : Group G✝
inst✝² : Group H✝
G : Type u
inst✝¹ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
H : Type u
inst✝ : Group H
f : G →* H
a : X
⊢ lift.symm f a = f (of a)

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
G✝ : Type u_3
H✝ : Type u_4
inst✝³ : Group G✝
inst✝² : Group H✝
G : Type u
inst✝¹ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
H : Type u
inst✝ : Group H
f : G →* H
a : X
⊢ lift.symm f a = f (of a)
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G✝ : Type u_3
H : Type u_4
inst✝² : Group G✝
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
lift_symm_of : ∀ {H : Type u} [inst : Group H] (f : G →* H) (a : X), lift.symm f a = f (of a) := ⋯
⊢ lift.symm ((FreeGroup.lift of).comp (lift FreeGroup.of)) = lift.symm (MonoidHom.id G)

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
G✝ : Type u_3
H : Type u_4
inst✝² : Group G✝
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
lift_symm_of : ∀ {H : Type u} [inst : Group H] (f : G →* H) (a : X), lift.symm f a = f (of a) := ⋯
⊢ lift.symm ((FreeGroup.lift of).comp (lift FreeGroup.of)) = lift.symm (MonoidHom.id G)
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.closure (Set.range ((⇑mk ∘ of) ∘ Sum.inl) ∪ Set.range ((⇑mk ∘ of) ∘ Sum.inr))

Tactic:
;

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 (Set.range ((⇑mk ∘ of) ∘ Sum.inl) ∪ Set.range ((⇑mk ∘ of) ∘ Sum.inr))