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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM : ContMDiffAt (I.tangent.prod I'.tangent) I.tangent n Prod.fst (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E → E := fun x ↦ ↑I (↑(chartAt H a.proj) (↑(chartAt H p.1.proj).symm (↑I.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj))
D :
  ∀ (w : TangentBundle I' M'),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.fst) (range (Prod.map ↑I ↑I'))
      (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' w.proj) w.proj))
φ' : E' → E' := fun x ↦ ↑I' (↑(chartAt H' b.proj) (↑(chartAt H' p.2.proj).symm (↑I'.symm x)))
D0' : DifferentiableWithinAt 𝕜 φ' (range ↑I') (↑I' (↑(chartAt H' p.2.proj) p.2.proj))
⊢ DifferentiableWithinAt 𝕜 φ' (range ↑I') (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj)).2

Tactic:
exact D0'

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E' → E' := fun x ↦ ↑I' (↑(chartAt H' b.proj) (↑(chartAt H' p.2.proj).symm (↑I'.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I') (↑I' (↑(chartAt H' p.2.proj) p.2.proj))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map ↑I ↑I'))
      (↑I (↑(chartAt H w.proj) w.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj))
φ' : E → E := fun x ↦ ↑I (↑(chartAt H a.proj) (↑(chartAt H p.1.proj).symm (↑I.symm x)))
D0' : DifferentiableWithinAt 𝕜 φ' (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj))
⊢ DifferentiableWithinAt 𝕜 φ' (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj)).1

Tactic:
exact D0'

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.UnitInterval

Goal state before:
pp: x : ↑I
⊢ volume (Ioi x) = ENNReal.ofReal (1 - ↑x)

Tactic:
by
  simp only [volume_apply, image_subtype_val_Icc_Ioi, Real.volume_Ioc]

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b)

Tactic:
rcases h.eq_or_lt with rfl | h

Goal state after:
case inl
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h : a ≤ a
hf : MonotoneOn f (Icc a a)
h'f : DifferentiableOn ℝ f (Icc a a)
hγ : MDiff[Icc (f a) (f a)] γ
⊢ pathELength I (γ ∘ f) a a = pathELength I γ (f a) (f a)

case inr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
h : a < b
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b)
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h : a ≤ b
hf : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f b) (f a)] γ
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f b) (f a)

Tactic:
rcases h.eq_or_lt with rfl | h

Goal state after:
case inl
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h : a ≤ a
hf : AntitoneOn f (Icc a a)
h'f : DifferentiableOn ℝ f (Icc a a)
hγ : MDiff[Icc (f a) (f a)] γ
⊢ pathELength I (γ ∘ f) a a = pathELength I γ (f a) (f a)

case inr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f b) (f a)] γ
h : a < b
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f b) (f a)
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := fun t ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
B : ∀ (t : ℝ), b' < t → η t = 1
B' : ∀ (t : ℝ), b' < t → (γ ∘ η) t = y
⊢ pathELength I (γ ∘ η) a b = pathELength I γ 0 1

Tactic:
rw [← A a haa', ← B b hb'b]

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := fun t ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
B : ∀ (t : ℝ), b' < t → η t = 1
B' : ∀ (t : ℝ), b' < t → (γ ∘ η) t = y
⊢ pathELength I (γ ∘ η) a b = pathELength I γ (η a) (η b)
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 := ⋯
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' := ⋯
ht' : t' = t ∩ (extChartAt I' (f x₀)).source
⊢ mpullbackWithin I I' f W s' =ᶠ[𝓝[s] x₀] mpullbackWithin I I' f W s

Tactic:
· apply nhdsWithin_le_nhds
      filter_upwards [mfderivWithin_eventually_congr_set (I := I) (I' := I') (f := f) s'_eq]
        with y hy using by simp [mpullbackWithin, hy]

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

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✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
hx : (chartAt H x).source ∈ 𝓝 x
⊢ ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ < C

Tactic:
filter_upwards [hC, hx] with y hy h'y

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
hx : (chartAt H x).source ∈ 𝓝 x
y : M
hy : ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
h'y : y ∈ (chartAt H x).source
⊢ ‖mfderiv% ↑(extChartAt I x) y‖ < C
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

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✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖Trivialization.symmL ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
hx : (chartAt H x).source ∈ 𝓝 x
⊢ ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y)‖ < C

Tactic:
filter_upwards [hC, hx] with y hy h'y

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖Trivialization.symmL ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
hx : (chartAt H x).source ∈ 𝓝 x
y : M
hy : ‖Trivialization.symmL ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
h'y : y ∈ (chartAt H x).source
⊢ ‖mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y)‖ < C
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
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : CompleteSpace E
n : ℕ∞ω
inst✝ : IsManifold I (n + 1) M
m : ℕ∞ω
U V : (x : M) → TangentSpace I x
s : Set M
x : M
hU : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[s]
hx : x ∈ s
hmn : minSmoothness 𝕜 (m + 1) ≤ n
min2 : minSmoothness 𝕜 2 ≤ n + 1
m' : ℕ∞ω
hm' : m' ≤ m
h'm' : m' ≠ ∞
hn : 1 ≤ m' + 1
⊢ m' + 1 ≤ n

Tactic:
grw [hm', ← hmn, ← le_minSmoothness]

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) ≠ 0

Tactic:
rw [card_commutatorSet_closureCommutatorRepresentatives]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Nat.card ↑(commutatorSet G) ≠ 0
Module: Mathlib.GroupTheory.Congruence.Star

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : StarMul M
r : M → M → Prop
hr : ∀ (a b : M), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : M
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star y✝ * Star.star w✝) (Star.star z✝ * Star.star x✝)

Tactic:
exact (h2.star hr).mul (h1.star hr)

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card M * Nat.card M') ^ 2 =
    ↑(Nat.card { p // Commute p.1 p.2 }) * ↑(Nat.card { p // Commute p.1 p.2 }) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)

Tactic:
Nat.cast_mul,

Goal state after:
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) / (↑(Nat.card M) * ↑(Nat.card M')) ^ 2 =
    ↑(Nat.card { p // Commute p.1 p.2 }) * ↑(Nat.card { p // Commute p.1 p.2 }) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝ : Group G
⊢ ↑(Nat.card (ConjClasses G) * Nat.card G) / ↑(Nat.card G) ^ 2 = ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)

Tactic:
Nat.cast_mul,

Goal state after:
G : Type u_2
inst✝ : Group G
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / ↑(Nat.card G) ^ 2 = ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
⊢ inl.range ⊔ inr.range = inl.range ⊔ Subgroup.closure ↑inr.range

Tactic:
Subgroup.closure_eq

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
⊢ inl.range ⊔ inr.range = inl.range ⊔ inr.range
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case neg
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
hm : ¬Even m
h₁ : Even (m + 1)
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)

Tactic:
have h₂ : (m + 1) / 2 = m / 2 + 1 := Nat.succ_div_of_dvd h₁.two_dvd

Goal state after:
case neg
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
hm : ¬Even m
h₁ : Even (m + 1)
h₂ : (m + 1) / 2 = m / 2 + 1
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ Even (2 * k)

Tactic:
use k

Goal state after:
case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ 2 * k = k + k
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case h₁
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.length (cs.simple i) ≤ 1

Tactic:
simpa using cs.length_wordProd_le [i]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case empty
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
⊢ empty.prod • empty = empty

Tactic:
rw [prod_empty, one_smul]

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
⊢ List.map (fun x ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = List.map id (cs.rightInvSeq ω.reverse)

Tactic:
apply List.map_congr_left
        intro t ht
        exact (cs.isReflection_of_mem_rightInvSeq _ ht).inv

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ (x : M i✝) (hnotone : x ≠ 1), (replaceHead x hnotone _w₁✝).head = x
_w₂_ih✝ : ∀ (x : M k✝) (hnotone : x ≠ 1), (replaceHead x hnotone _w₂✝).head = x
x : M i✝
hnotone : x ≠ 1
⊢ (replaceHead x hnotone (_w₁✝.append _hne✝ _w₂✝)).head = x

Tactic:
simp [*, replaceHead]

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out (mk H K x) = h * x * k
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out (mk H K x) * y

Tactic:
refine ⟨h⁻¹, H.inv_mem h3, k⁻¹, K.inv_mem h4, ?_⟩

Goal state after:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out (mk H K x) = h * x * k
⊢ x = h⁻¹ * Quotient.out (mk H K x) * k⁻¹
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
this : FreeGroup.lift a = (lift fun i ↦ FreeGroup.lift fun x ↦ a i).comp freeGroupEquivCoprodI.toMonoidHom
⊢ Function.Injective ⇑((lift fun i ↦ FreeGroup.lift fun x ↦ a i).comp freeGroupEquivCoprodI.toMonoidHom)

Tactic:
MonoidHom.coe_comp

Goal state after:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
this : FreeGroup.lift a = (lift fun i ↦ FreeGroup.lift fun x ↦ a i).comp freeGroupEquivCoprodI.toMonoidHom
⊢ Function.Injective (⇑(lift fun i ↦ FreeGroup.lift fun x ↦ a i) ∘ ⇑freeGroupEquivCoprodI.toMonoidHom)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
⊢ 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)

Tactic:
show _ ∨ ∃ i, 3 ≤ #(H i)

Goal state after:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
⊢ 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : ↥H →* A
inst✝¹ : H.FiniteIndex
g : G
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ ∏ a,
      ∏ s,
        ϕ
          ⟨(↑(⋯.leftQuotientEquiv ((H.quotientEquivSigmaZMod g).symm ⟨a, s⟩)))⁻¹ *
              ↑(⋯.leftQuotientEquiv ((H.quotientEquivSigmaZMod g).symm ⟨a, s⟩)),
            ⋯⟩ =
    ∏ q, ϕ ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x ↦ g • x) q.out * Quotient.out q.out, ⋯⟩

Tactic:
refine Fintype.prod_congr _ _ (fun q => ?_)
      simp only [quotientEquivSigmaZMod_symm_apply, transferTransversal_apply',
        transferTransversal_apply'']
      rw [Fintype.prod_eq_single (0 : ZMod (Function.minimalPeriod (g • ·) q.out)) _]
      · simp only [if_pos, ZMod.cast_zero, zpow_zero, one_mul, mul_assoc]
      · intro k hk
        simp only [if_neg hk, inv_mul_cancel]
        exact map_one ϕ

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
x : ↥H
⊢ H.transferFocal ↑x = ↑x ^ H.index

Tactic:
have : Fintype (Quotient (MulAction.orbitRel (zpowers (x : G)) (G ⧸ H))) :=
    Fintype.ofFinite _

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
x : ↥H
this : Fintype (Quotient (MulAction.orbitRel (↥(zpowers ↑x)) (G ⧸ H)))
⊢ H.transferFocal ↑x = ↑x ^ H.index
Module: Mathlib.Order.Radical

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : ⊤ ≤ m
⊢ a = ⊤

Tactic:
top_le_iff

Goal state after:
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : m = ⊤
⊢ a = ⊤
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
⊢ IsCyclicallyReduced (replicate (n + 1) (head :: tail)).flatten

Tactic:
rw [isCyclicallyReduced_iff, IsReduced, List.isChain_flatten (by simp)]
    refine ⟨⟨by simpa [IsReduced] using h.isReduced, List.isChain_replicate_of_rel _ h.2⟩,
      fun _ ha _ hb ↦ ?_⟩
    rw [Option.mem_def, List.getLast?_flatten_replicate (h := by simp +arith)] at ha
    rw [Option.mem_def, List.head?_flatten_replicate (h := by simp +arith)] at hb
    exact h.2 _ ha _ hb

Goal state after: