mathlib-initiative/mathlib-tactics huggingface dataset:
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
this✝ : ((g' x) w) w ≤ δ * C * ((g' x) w) w + ((g' y) w) w
this : (1 - δ * C) * ((g' x) w) w ≤ ((g' y) w) w
⊢ 0 ≤ (r' ^ 2)⁻¹

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I (minSmoothness 𝕜 3) M
inst✝ : CompleteSpace E
U V W : (x : M) → TangentSpace I x
x : M
hU : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U x⟩) univ x
hV : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V x⟩) univ x
hW : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W x⟩) univ x
⊢ x ∈ closure[inst✝³] (interior univ)

Tactic:
by

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

Goal state before:
pp: ⊢ Nat.card (ZMod 2 × ZMod 2) = 4

Tactic:
by

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

Goal state before:
pp: ⊢ AddMonoid.exponent (ZMod 2 × ZMod 2) = 2

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
⊢ AddMonoid.exponent (Additive G) = 2

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I (minSmoothness 𝕜 3) M
inst✝ : CompleteSpace E
U V W : (x : M) → TangentSpace I x
x : M
hU : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U x⟩) x
hV : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V x⟩) x
hW : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W x⟩) x
⊢ mlieBracket I U (mlieBracket I V W) x = mlieBracket I (mlieBracket I U V) W x + mlieBracket I V (mlieBracket I U W) x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝¹ : AddGroup G
inst✝ : IsAddKleinFour G
⊢ Monoid.exponent (Multiplicative G) = 2

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
⊢ Nat.card G ≠ 0

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
h : IsCyclic G
⊢ False

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
x : G
⊢ Monoid.exponent G = 2

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
x : G
⊢ x * x = 1

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I (minSmoothness 𝕜 3) M
inst✝ : CompleteSpace E
U V W : (x : M) → TangentSpace I x
hU : ContMDiff I I.tangent (minSmoothness 𝕜 2) fun x ↦ ⟨x, U x⟩
hV : ContMDiff I I.tangent (minSmoothness 𝕜 2) fun x ↦ ⟨x, V x⟩
hW : ContMDiff I I.tangent (minSmoothness 𝕜 2) fun x ↦ ⟨x, W x⟩
⊢ mlieBracket I U (mlieBracket I V W) = mlieBracket I (mlieBracket I U V) W + mlieBracket I V (mlieBracket I U W)

Tactic:
by

Goal state after:
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
⊢ Monoid.exponent G = 2

Tactic:
by

Goal state after:
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
⊢ {x * y, x, y, 1} = univ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
x y z : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
hz : z ≠ 1
hzx : z ≠ x
hzy : z ≠ y
⊢ z = x * y

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : ¬y = 1
hxy : ¬x = y
⊢ {e (x * y), e x, e y, 1} = univ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
⊢ ∀ (x y : G₁), e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
by

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

Goal state before:
pp: G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
_inst₁✝ : Fintype G₁ := Fintype.ofFinite G₁
_inst₁ : Fintype G₂ := Fintype.ofFinite G₂
⊢ Fintype.card G₁ = Fintype.card G₂

Tactic:
by

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

Goal state before:
pp: G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
_inst₁✝ : Fintype G₁ := Fintype.ofFinite G₁
_inst₁ : Fintype G₂ := Fintype.ofFinite G₂
⊢ ((Fintype.equivOfCardEq ⋯).setValue 1 1) 1 = 1

Tactic:
by

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

Goal state before:
pp: G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
⊢ Nonempty (G₁ ≃* G₂)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ∀ (a b c : DihedralGroup n), a * b * c = a * (b * c)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ∀ (a : DihedralGroup n), 1 * a = a

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ∀ (a : DihedralGroup n), a * 1 = a

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ∀ (a : DihedralGroup n), a.inv * a = 1

Tactic:
by

Goal state after:
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 (w✝ * y✝)) (Star.star (x✝ * z✝))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Star

Goal state before:
pp: A : Type u_1
inst✝¹ : AddMonoid A
inst✝ : StarAddMonoid A
r : A → A → Prop
hr : ∀ (a b : A), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : A
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star (w✝ + y✝)) (Star.star (x✝ + z✝))

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : ZMod n
k : ℕ
⊢ r i ^ k = r (i * ↑k)

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : ZMod n
k : ℤ
⊢ r i ^ k = r (i * ↑k)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Function.LeftInverse
    (fun x ↦
      match x with
      | Sum.inl j => r j
      | Sum.inr j => sr j)
    fun x ↦
    match x with
    | r j => Sum.inl j
    | sr j => Sum.inr j

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | Sum.inl j => r j
      | Sum.inr j => sr j)
    fun x ↦
    match x with
    | r j => Sum.inl j
    | sr j => Sum.inr j

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ r 0 ≠ sr 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (DihedralGroup n) = 2 * n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Nat.card (DihedralGroup n) = 2 * n

Tactic:
by

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

Goal state before:
pp: n k : ℕ
⊢ r 1 ^ k = r ↑k

Tactic:
by

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

Goal state before:
pp: n : ℕ
k : ℤ
⊢ r 1 ^ k = r ↑k

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ r 1 ^ n = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : ZMod n
⊢ sr i * sr i = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : ZMod n
⊢ orderOf (sr i) = 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ orderOf (r 1) = n

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r i) = n / n.gcd i.val

Tactic:
by

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

Goal state before:
pp: case hcb
n : ℕ
hn : NeZero n
⊢ 2 ∣ Monoid.exponent (DihedralGroup n)

Tactic:
· convert! Monoid.order_dvd_exponent (sr (0 : ZMod n))
      exact (orderOf_sr 0).symm

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

Goal state before:
pp: n : ℕ
⊢ Monoid.exponent (DihedralGroup n) = lcm n 2

Tactic:
by

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

Goal state before:
pp: x✝¹ : 0 ≠ 1
x✝ : 0 ≠ 2
h' : IsMulCommutative (DihedralGroup 0)
⊢ False

Tactic:
by

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

Goal state before:
pp: n : ℕ
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
h' : IsMulCommutative (DihedralGroup (n + 3))
⊢ False

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ IsMulCommutative (DihedralGroup n) → n = 1 ∨ n = 2

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b : DihedralGroup 1), a * b = b * a

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a b : DihedralGroup 2), a * b = b * a

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n = 1 ∨ n = 2 → IsMulCommutative (DihedralGroup n)

Tactic:
by

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

Goal state before:
pp: n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
⊢ False

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h : Commute (r i, sr j).1 (r i, sr j).2
⊢ (fun x ↦
        match x with
        | Sum.inl i => ⟨(sr i, r 0), ⋯⟩
        | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩
        | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)), ⋯⟩
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨(sr i, r a), property⟩ => Sum.inl i
          | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j)
          | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j))))
        ⟨(r i, sr j), h⟩) =
    ⟨(r i, sr j), h⟩

Tactic:
by

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'
⊢ commProb (M × M') = commProb M * commProb M'

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h : Commute (sr i, r j).1 (sr i, r j).2
⊢ (fun x ↦
        match x with
        | Sum.inl i => ⟨(sr i, r 0), ⋯⟩
        | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩
        | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)), ⋯⟩
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨(sr i, r a), property⟩ => Sum.inl i
          | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j)
          | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j))))
        ⟨(sr i, r j), h⟩) =
    ⟨(sr i, r j), h⟩

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ commProb ((a : α) → i a) = ∏ a, commProb (i a)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Mul β
⊢ commProb (α → β) = commProb β ^ card α

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ commProb M ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
⊢ commProb M = 1 ↔ IsMulCommutative M

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
p q : { p // Commute p.1 p.2 }
h : (fun p ↦ ⟨(↑(↑p).1, ↑(↑p).2), ⋯⟩) p = (fun p ↦ ⟨(↑(↑p).1, ↑(↑p).2), ⋯⟩) q
⊢ p = q

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ commProb ↥H ≤ commProb G * ↑H.index ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ commProb (G ⧸ H) ≤ commProb G * ↑(Nat.card ↥H)

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h : Commute (sr i, sr j).1 (sr i, sr j).2
⊢ (fun x ↦
        match x with
        | Sum.inl i => ⟨(sr i, r 0), ⋯⟩
        | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩
        | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)), ⋯⟩
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨(sr i, r a), property⟩ => Sum.inl i
          | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j)
          | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j))))
        ⟨(sr i, sr j), h⟩) =
    ⟨(sr i, sr j), h⟩

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ commProb (DihedralGroup n) = (↑n + 3) / (4 * ↑n)

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ Nat.card { p // Commute p.1 p.2 } = n * (n + 3)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: ⊢ reciprocalFactors 0 = [0]

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: ⊢ reciprocalFactors 1 = []

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
h2 : Even n
⊢ n ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
h2 : Even n
⊢ reciprocalFactors n = 3 :: reciprocalFactors (n / 2)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h1 : n ≠ 1
h2 : Odd n
⊢ n ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h1 : n ≠ 1
h2 : Odd n
⊢ reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: ⊢ commProb (Product []) = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
l : List ℕ
⊢ commProb (Product (n :: l)) = commProb (DihedralGroup n) * commProb (Product l)

Tactic:
by

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

Goal state before:
pp: n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * sr i = sr i * g
heq : i - 1 = i + 1
⊢ 1 < n

Tactic:
by

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

Goal state before:
pp: n : ℕ
hodd : Odd n
hne1 : n ≠ 1
⊢ Subgroup.center (DihedralGroup n) = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
⊢ Odd 3

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
⊢ Odd (n % 4)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
⊢ commProb (DihedralGroup (n % 4 * n)) * (1 / ↑(n / 4 + 1)) = 1 / ↑n

Tactic:
have hn : Odd (n % 4) := by grind

Goal state after:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ commProb (DihedralGroup (n % 4 * n)) * (1 / ↑(n / 4 + 1)) = 1 / ↑n
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' }
⊢ ↑b.symm = ↑b'.symm

Tactic:
by

Goal state after:
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:
exact DFunLike.congr_fun H x

Goal state after:
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
⊢ b.symm = b'.symm

Tactic:
by

Goal state after:
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
⊢ Injective fun b i ↦ b.repr.symm (FreeGroup.of i)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
G : Type u_3
inst✝ : Group G
b : FreeGroupBasis ι G
i : ι
⊢ b.repr (b i) = FreeGroup.of i

Tactic:
by

Goal state after:
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 : FreeGroupBasis ι G
f : FreeGroup ι →* H
⊢ (fun f ↦ f.comp b.repr.symm.toMonoidHom) ((fun f ↦ f.comp b.repr.toMonoidHom) f) = f

Tactic:
by

Goal state after:
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 : FreeGroupBasis ι G
f : G →* H
⊢ (fun f ↦ f.comp b.repr.toMonoidHom) ((fun f ↦ f.comp b.repr.symm.toMonoidHom) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
by

Goal state after:
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 FreeGroup.of).comp (FreeGroup.lift of) = MonoidHom.id (FreeGroup X)

Tactic:
by

Goal state after:
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:
by

Goal state after: