mathlib-initiative/mathlib-tactics huggingface dataset:
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
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
inst✝ : VectorBundle 𝕜 F V
hcov : IsCovariantDerivativeOn F cov s
x : M
hx : x ∈ s
⊢ cov 0 x = 0

Tactic:
simpa using

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
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
inst✝ : VectorBundle 𝕜 F V
hcov : IsCovariantDerivativeOn F cov s
x : M
hx : x ∈ s
⊢ cov 0 x = 0
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
inst✝¹ : IsManifold I 1 M
n : ℕ∞ω
inst✝ : VectorBundle 𝕜 F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov : ∀ i ∈ s, ContMDiffCovariantDerivativeOn F n (cov i) u
f : ι → M → 𝕜
hf : ∀ i ∈ s, ContMDiffOn I 𝓘(𝕜, 𝕜) n (f i) u
σ : (x : M) → V x
hσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (n + 1) (fun x ↦ ⟨x, σ x⟩) u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, E →L[𝕜] F)) n (fun x ↦ ⟨x, ∑ i ∈ s, f i x • cov i σ x⟩) u

Tactic:
simpa using

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
inst✝¹ : IsManifold I 1 M
n : ℕ∞ω
inst✝ : VectorBundle 𝕜 F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov : ∀ i ∈ s, ContMDiffCovariantDerivativeOn F n (cov i) u
f : ι → M → 𝕜
hf : ∀ i ∈ s, ContMDiffOn I 𝓘(𝕜, 𝕜) n (f i) u
σ : (x : M) → V x
hσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (n + 1) (fun x ↦ ⟨x, σ x⟩) u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, E →L[𝕜] F)) n (fun x ↦ ⟨x, ∑ i ∈ s, f i x • cov i σ x⟩) u
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

Goal state before:
pp: case mp
𝕜 : 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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
X Y : (x : M) → TangentSpace I x
x : M
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
h : (↑cov Y x) (X x) - (↑cov X x) (Y x) - mlieBracket I X Y x = ((0 x) (X x)) (Y x)
⊢ (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x

Tactic:
simpa using

Goal state after:
case mp
𝕜 : 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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
X Y : (x : M) → TangentSpace I x
x : M
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
h : (↑cov Y x) (X x) - (↑cov X x) (Y x) - mlieBracket I X Y x = ((0 x) (X x)) (Y x)
⊢ (↑cov Y x) (X x) = (↑cov X x) (Y x) + mlieBracket I X Y x
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : Nontrivial R
m : ℕ
inst✝ : NeZero m.succ
poly : Polygon P m.succ
h : HasNondegenerateVertices R poly
i : Fin m.succ
⊢ poly.vertices i ≠ poly.vertices ((finRotate m.succ) i)

Tactic:
simpa using

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : Nontrivial R
m : ℕ
inst✝ : NeZero m.succ
poly : Polygon P m.succ
h : HasNondegenerateVertices R poly
i : Fin m.succ
⊢ ¬poly.vertices i = poly.vertices (i + 1)
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R ![t.points 0, t.points 1, t.points 2]

Tactic:
simpa using

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R t.points
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ ↑(carrier (Quot.mk (⇑(IsConj.setoid G)) g)).toFinset = ↑{g}

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ carrier (Quot.mk (⇑(IsConj.setoid G)) g) = {g}
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case pos
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs j
hx : x ∈ ↑(H j)
⊢ (MonoidHom.mulSingle Gs j) x ∈ comap (Pi.evalMonoidHom Gs j) (H j)

Tactic:
simpa using

Goal state after:
case pos
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs j
hx : x ∈ ↑(H j)
⊢ x ∈ H j
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case pos
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs j
hx : x ∈ ↑(K j)
⊢ (MonoidHom.mulSingle Gs j) x ∈ comap (Pi.evalMonoidHom Gs j) (K j)

Tactic:
simpa using

Goal state after:
case pos
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs j
hx : x ∈ ↑(K j)
⊢ x ∈ K j
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

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

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
h : IsCyclic G
⊢ False
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}

Tactic:
simpa using

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
⊢ ¬y = 1 ∧ ¬x = 1 ∧ ¬x * y = 1
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
x✝ : Fintype G := ⋯
⊢ z ∉ {x, y, 1}

Tactic:
simpa using

Goal state after:
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
x✝ : Fintype G := Fintype.ofFinite G
⊢ ¬z = x ∧ ¬z = y ∧ ¬z = 1
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:
simpa using

Goal state after:
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
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: case neg
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₁ := ⋯
_inst₂ : Fintype G₂ := ⋯
x y : G₁
hx : e x ≠ 1
hy : e y ≠ 1
hxy : e x ≠ e y
univ₂ : {e (x * y), e x, e y, 1} = univ
⊢ e x * e y ∉ {e x, e y, 1}

Tactic:
simpa using

Goal state after:
case neg
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 : e x ≠ 1
hy : e y ≠ 1
hxy : e x ≠ e y
univ₂ : {e (x * y), e x, e y, 1} = univ
⊢ ¬e y = 1 ∧ ¬e x = 1 ∧ ¬e x * e y = 1
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inl
n : ℕ
hn : 0 < n
⊢ ¬↑n = 0

Tactic:
simpa using

Goal state after:
case inl
n : ℕ
hn : 0 < n
⊢ ¬n = 0
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

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

Tactic:
simpa using

Goal state after:
x✝¹ : 0 ≠ 1
x✝ : 0 ≠ 2
h' : IsMulCommutative (DihedralGroup 0)
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

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

Tactic:
simpa using

Goal state after:
n : ℕ
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
h' : IsMulCommutative (DihedralGroup (n + 3))
this : 2 % (n + 3) = 0
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

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

Tactic:
simpa using

Goal state after:
case pos
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : n = 2
⊢ False
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:
simpa using

Goal state after:
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
⊢ 0 = i
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:
simpa using

Goal state after:
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
⊢ 0 = j
Module: Mathlib.GroupTheory.CommutingProbability

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

Tactic:
commProb,

Goal state after:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card M) ^ 2 = 1 ↔ IsMulCommutative M
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:
commProb,

Goal state after:
G : Type u_2
inst✝ : Group G
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card G) ^ 2 = ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
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:
rw [commProb, card_comm_eq_card_conjClasses_mul_card, Nat.cast_mul, sq]
  by_cases h : (Nat.card G : ℚ) = 0
  · rw [h, zero_mul, div_zero, div_zero]
  · exact mul_div_mul_right _ _ h

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:
simpa using

Goal state after:
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).1 = ↑(↑q).1 ∧ ↑(↑p).2 = ↑(↑q).2
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 intro H _ f a; simp [← lift_of (lift.symm f)]

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

Goal state before:
pp: case of_mul.inl
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
motive : M ∗ N → Prop
one : motive 1
inl_mul : ∀ (m : M) (x : M ∗ N), motive x → motive (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), motive x → motive (inr n * x)
xs : FreeMonoid (M ⊕ N)
ih : motive (mk xs)
m : M
⊢ motive (mk (of (Sum.inl m) * xs))

Tactic:
simpa using

Goal state after:
case of_mul.inl
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
motive : M ∗ N → Prop
one : motive 1
inl_mul : ∀ (m : M) (x : M ∗ N), motive x → motive (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), motive x → motive (inr n * x)
xs : FreeMonoid (M ⊕ N)
ih : motive (mk xs)
m : M
⊢ motive (inl m * mk xs)
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: case of_mul.inr
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
motive : M ∗ N → Prop
one : motive 1
inl_mul : ∀ (m : M) (x : M ∗ N), motive x → motive (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), motive x → motive (inr n * x)
xs : FreeMonoid (M ⊕ N)
ih : motive (mk xs)
n : N
⊢ motive (mk (of (Sum.inr n) * xs))

Tactic:
simpa using

Goal state after:
case of_mul.inr
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
motive : M ∗ N → Prop
one : motive 1
inl_mul : ∀ (m : M) (x : M ∗ N), motive x → motive (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), motive x → motive (inr n * x)
xs : FreeMonoid (M ⊕ N)
ih : motive (mk xs)
n : N
⊢ motive (inr n * mk xs)
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
motive : M ∗ N → Prop
m : M ∗ N
inl : ∀ (m : M), motive (Coprod.inl m)
inr : ∀ (n : N), motive (Coprod.inr n)
mul : ∀ (x y : M ∗ N), motive x → motive y → motive (x * y)
⊢ motive 1

Tactic:
simpa using

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
motive : M ∗ N → Prop
m : M ∗ N
inl : ∀ (m : M), motive (Coprod.inl m)
inr : ∀ (n : N), motive (Coprod.inr n)
mul : ∀ (x y : M ∗ N), motive x → motive y → motive (x * y)
⊢ motive 1
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : FreeMonoid (G ⊕ H)
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList x)).reverse) * mk x = 1

Tactic:
induction x using FreeMonoid.inductionOn' with
  | one => simp
  | of_mul x xs ihx =>
    simp only [toList_of_mul, map_cons, reverse_cons, ofList_append, map_mul, ofList_singleton]
    rwa [mul_assoc, ← mul_assoc (mk (of _)), mk_of_inv_mul, one_mul]

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
⊢ Surjective ⇑↑(FreeGroup.freeGroupCongr e)

Tactic:
simpa using

Goal state after:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
⊢ Surjective ⇑(FreeGroup.freeGroupCongr e)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : 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
⊢ ∃ i m, of m = x

Tactic:
simpa using

Goal state after:
ι : 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
⊢ ∃ i m, of m = x
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
⊢ (lift f).range ≤ s

Tactic:
by
  rintro _ ⟨x, rfl⟩
  induction x using CoprodI.induction_on with
  | one => exact s.one_mem
  | of i x =>
    simp only [lift_of]
    exact h i (Set.mem_range_self x)
  | mul x y hx hy =>
    simp only [map_mul]
    exact s.mul_mem hx hy

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

Goal state before:
pp: case cons
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
x : B
ω' : List B
ih : cs.wordProd ω'.reverse = (cs.wordProd ω')⁻¹
⊢ cs.wordProd (x :: ω').reverse = (cs.wordProd (x :: ω'))⁻¹

Tactic:
simpa using

Goal state after:
case cons
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
x : B
ω' : List B
ih : cs.wordProd ω'.reverse = (cs.wordProd ω')⁻¹
⊢ cs.wordProd ω'.reverse = (cs.wordProd ω')⁻¹
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 := ⋯
C : ℝ := ⋯
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 0 < δ
B : Tendsto (fun δ ↦ 1 + δ * C) (𝓝[>] 0) (𝓝 (1 + 0 * C))
⊢ r' ^ 2 > 1 + 0 * C

Tactic:
simpa using

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
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 0 < δ
B : Tendsto (fun δ ↦ 1 + δ * C) (𝓝[>] 0) (𝓝 (1 + 0 * C))
⊢ 1 < |r'|
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), (alternatingWord i i' m).length = m
i i' : B
⊢ (alternatingWord i i' (m + 1)).length = m + 1

Tactic:
simpa using

Goal state after:
case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), (alternatingWord i i' m).length = m
i i' : B
⊢ (alternatingWord i' i m).length = m
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 : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : ¬m = 1
hm' : ¬m' = 1
⊢ m = m' ∧ w.toList = w'.toList

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : ¬m = 1
hm' : ¬m' = 1
⊢ m = m' ∧ w.toList = w'.toList
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ Odd ?m.111

Tactic:
simpa using

Goal state after:
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ Odd ?m.111