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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
F : Type u_5
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F V)
inst✝⁹ : (x : M) → AddCommGroup (V x)
inst✝⁸ : (x : M) → Module 𝕜 (V x)
inst✝⁷ : (x : M) → TopologicalSpace (V x)
inst✝⁶ : FiberBundle F V
A : Type u_9
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst✝³ : VectorBundle 𝕜 F V
inst✝² : CompleteSpace 𝕜
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : ContMDiffVectorBundle 1 F V I
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : σ x = σ' x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
x_mem : x ∈ t.baseSet
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 F)) 𝕜 F := Basis.ofVectorSpace 𝕜 F
s : ↑(Basis.ofVectorSpaceIndex 𝕜 F) → (x : M) → V x := t.localFrame b
⊢ Φ σ = Φ σ'

Tactic:
let c := t.localFrameCoeff I b

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✝⁶ : FiberBundle F V
A : Type u_9
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst✝³ : VectorBundle 𝕜 F V
inst✝² : CompleteSpace 𝕜
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : ContMDiffVectorBundle 1 F V I
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : σ x = σ' x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
x_mem : x ∈ t.baseSet
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 F)) 𝕜 F := Basis.ofVectorSpace 𝕜 F
s : ↑(Basis.ofVectorSpaceIndex 𝕜 F) → (x : M) → V x := t.localFrame b
c : ↑(Basis.ofVectorSpaceIndex 𝕜 F) → (x : M) → V x →ₗ[𝕜] 𝕜 := Trivialization.localFrameCoeff I t b
⊢ Φ σ = Φ σ'
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
s : Set M
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov : IsCovariantDerivativeOn F cov s
cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov' : IsCovariantDerivativeOn F cov' s
g : M → 𝕜
σ✝ σ'✝ : (x : M) → V x
x✝ : M
hσ : MDiffAt (T% σ✝) x✝
hσ' : MDiffAt (T% σ'✝) x✝
hx : x✝ ∈ s
⊢ (g • cov (σ✝ + σ'✝) + (1 - g) • cov' (σ✝ + σ'✝)) x✝ =
    (g • cov σ✝ + (1 - g) • cov' σ✝) x✝ + (g • cov σ'✝ + (1 - g) • cov' σ'✝) x✝

Tactic:
simp [hcov.add hσ hσ', hcov'.add hσ hσ']
    module

Goal state after:
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)
h : cov.torsion = 0
⊢ ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
    MDiffAt (T% X) x → MDiffAt (T% Y) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x

Tactic:
X

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)
h : cov.torsion = 0
X : (x : M) → TangentSpace I x
⊢ ∀ {Y : (x : M) → TangentSpace I x} {x : M},
    MDiffAt (T% X) x → MDiffAt (T% Y) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x
Module: Mathlib.Geometry.Manifold.WhitneyEmbedding

Goal state before:
pp: ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
⊢ y ∈ s → f.embeddingPiTangent x = f.embeddingPiTangent y → x = y

Tactic:
_

Goal state after:
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
⊢ f.embeddingPiTangent x = f.embeddingPiTangent y → x = y
Module: Mathlib.Geometry.Manifold.WhitneyEmbedding

Goal state before:
pp: case convert_2
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
L : (ι → E × ℝ) →L[ℝ] E := ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (f.ind x hx)
this : HasMFDerivAt% (⇑L ∘ ⇑f.embeddingPiTangent) x (L ∘SL mfderiv% ⇑f.embeddingPiTangent x)
y : M
hy : ↑(f.toFun (f.ind x hx)) y = 1 y
⊢ 1 y • ↑(extChartAt I (f.c (f.ind x hx))) y = ↑(extChartAt I (f.c (f.ind x hx))) y

Tactic:
Pi.one_apply,

Goal state after:
case convert_2
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
L : (ι → E × ℝ) →L[ℝ] E := ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (f.ind x hx)
this : HasMFDerivAt% (⇑L ∘ ⇑f.embeddingPiTangent) x (L ∘SL mfderiv% ⇑f.embeddingPiTangent x)
y : M
hy : ↑(f.toFun (f.ind x hx)) y = 1 y
⊢ 1 • ↑(extChartAt I (f.c (f.ind x hx))) y = ↑(extChartAt I (f.c (f.ind x hx))) y
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:
let _inst₁ := Fintype.ofFinite G₁

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₁
⊢ ∀ (x y : G₁), e.toFun (x * y) = e.toFun x * e.toFun y
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:
let _inst₁ := Fintype.ofFinite G₁

Goal state after:
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₁
⊢ Nonempty (G₁ ≃* G₂)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

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

Tactic:
apply Monoid.exponent_dvd_of_forall_pow_eq_one

Goal state after:
case inr.a
n : ℕ
hn : NeZero n
⊢ ∀ (g : DihedralGroup n), g ^ lcm n 2 = 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✝
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.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
⊢ (Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P))).comp
      (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr)) =
    MonoidHom.id ((M ∗ N) ∗ P)

Tactic:
by ext <;> rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
⊢ (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr)).comp
      (Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P))) =
    MonoidHom.id (M ∗ (N ∗ P))

Tactic:
by ext <;> rfl

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

Goal state before:
pp: case pos
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : Even (p + k)
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i

Tactic:
rw [if_pos h_even, ← add_assoc]
    simp only [ite_eq_right_iff, isEmpty_Prop, Nat.not_even_iff_odd, Even.add_one h_even,
      IsEmpty.forall_iff]

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

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < r' ^ 2
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
⊢ ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ

Tactic:
Metric.continuousAt_iff'

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'δ : 1 + δ * C < r' ^ 2
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' : ∀ ε > 0, ∀ᶠ (x_1 : B) in 𝓝 x, dist (g' x_1) (g' x) < ε
⊢ ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : ⟨j, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
h : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = j
⊢ m₁ = m₂ * ⋯ ▸ (w.toList.head ⋯).snd ↔
    (∃ m', w.toList.head? = some ⟨j, m'⟩ ∧ m₁ = m₂ * m') ∨ ¬w.fstIdx = some j ∧ m₁ = m₂

Tactic:
rcases h with ⟨hnil, rfl⟩

Goal state after:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList = []
m₂ m₁ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
⊢ m₁ = m₂ * ⋯ ▸ (w.toList.head ⋯).snd ↔
    (∃ m', w.toList.head? = some ⟨(w.toList.head hnil).fst, m'⟩ ∧ m₁ = m₂ * m') ∨
      ¬w.fstIdx = some (w.toList.head hnil).fst ∧ m₁ = m₂
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
w : W
ω : List B
hω : cs.IsReduced ω
h'ω : w⁻¹ = cs.wordProd ω
this : cs.length w⁻¹⁻¹ ≤ cs.length (cs.wordProd ω)
⊢ cs.length w ≤ cs.length w⁻¹

Tactic:
inv_inv,

Goal state after:
case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
ω : List B
hω : cs.IsReduced ω
h'ω : w⁻¹ = cs.wordProd ω
this : cs.length w ≤ cs.length (cs.wordProd ω)
⊢ cs.length w ≤ cs.length w⁻¹
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
w t : W
ht : cs.IsReflection t
⊢ cs.length (t⁻¹ * w⁻¹⁻¹) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w

Tactic:
inv_inv,

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
ht : cs.IsReflection t
⊢ cs.length (t⁻¹ * w) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case cons
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
motive : Word M → Prop
empty : motive Word.empty
smul : ∀ (i : ι) (m : M i) (w : Word M), motive w → motive (of m • w)
i✝ : ι
m✝ : M i✝
w✝ : Word M
h1✝ : w✝.fstIdx ≠ some i✝
h2✝ : m✝ ≠ 1
ih : motive w✝
⊢ motive (cons m✝ w✝ h1✝ h2✝)

Tactic:
| cons _ _ _ _ _ ih =>

Goal state after:
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
f : G →* G := powMonoidHom n
q : G → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
x : G
| ∃ y ∈ ↑f.range, qi (q x) * y = x

Tactic:
1,

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
f : G →* G := powMonoidHom n
q : G → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
x : G
| fun y ↦ y ∈ ↑f.range ∧ qi (q x) * y = x
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
c : DivisibleHull M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
hbc : mk mb sb ≤ c
hab : mk ma sa ≤ mk mb sb
⊢ mk ma sa ≤ c

Tactic:
induction c with | mk mc sc
     =>  _ 

Goal state after:
case mk.mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
hab : mk ma sa ≤ mk mb sb
mc : M
sc : ℕ+
hbc : mk mb sb ≤ mk mc sc
⊢ mk ma sa ≤ mk mc sc
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
c : DivisibleHull M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
h : mk mb sb < c
⊢ mk ma sa + mk mb sb < mk ma sa + c

Tactic:
induction c with | mk mc sc
     =>  _ 

Goal state after:
case mk.mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : mk mb sb < mk mc sc
⊢ mk ma sa + mk mb sb < mk ma sa + mk mc sc
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : ℚ≥0
ha : 0 < a
c : DivisibleHull M
mb : M
sb : ℕ+
h : mk mb sb < c
⊢ a • mk mb sb < a • c

Tactic:
induction c with | mk mc sc
     =>  _ 

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : mk mb sb < mk mc sc
⊢ a • mk mb sb < a • mk mc sc
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H : Subgroup G
⊢ Function.Surjective ⇑(domRestrictHom H Mˣ)

Tactic:
by
  have : Fintype H := Fintype.ofFinite H
  have : HasEnoughRootsOfUnity M (Monoid.exponent H) :=
    hM.of_dvd M <| Monoid.exponent_submonoid_dvd H.toSubmonoid
  have : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H)) :=
    hM.of_dvd M <| Group.exponent_quotient_dvd H
  refine MonoidHom.surjective_of_card_ker_le_div _ (le_of_eq ?_)
  rw [card_monoidHom_of_hasEnoughRootsOfUnity, card_monoidHom_of_hasEnoughRootsOfUnity,
    H.card_eq_card_quotient_mul_card_subgroup,
    mul_div_cancel_right₀ _ (Fintype.card_eq_nat_card ▸ Fintype.card_ne_zero),
    ← card_monoidHom_of_hasEnoughRootsOfUnity (G ⧸ H) M,
    Nat.card_congr (domRestrictHomKerEquiv Mˣ H).toEquiv]

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
⊢ g ^ H.index ∈ H

Tactic:
by_cases hH : H.index = 0
  · rw [hH, pow_zero]
    exact H.one_mem
  let := fintypeOfIndexNeZero hH
  classical
    replace key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H := fun k g₀ hk =>
      (congr_arg (· ∈ H) (key k g₀ hk)).mp hk
    replace key : ∀ q : G ⧸ H, g ^ Function.minimalPeriod (g • ·) q ∈ H := fun q =>
      key (Function.minimalPeriod (g • ·) q) q.out
        (QuotientGroup.out_conj_pow_minimalPeriod_mem H g q)
    let f : Quotient (orbitRel (zpowers g) (G ⧸ H)) → zpowers g := fun q =>
      (⟨g, mem_zpowers g⟩ : zpowers g) ^ Function.minimalPeriod (g • ·) q.out
    have hf : ∀ q, f q ∈ H.subgroupOf (zpowers g) := fun q => key q.out
    replace key :=
      Subgroup.prod_mem (H.subgroupOf (zpowers g)) fun q (_ : q ∈ Finset.univ) => hf q
    simpa only [f, Finset.prod_pow_eq_pow_sum, index_eq_sum_minimalPeriod H g] using! key

Goal state after:
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
N : Subgroup G
f : G →* H
hf : Function.Surjective ⇑f
S : Set G
hSfinite : S.Finite
hSclosure : normalClosure S = N
⊢ normalClosure (⇑f '' S) = map f N

Tactic:
← hSclosure,

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
N : Subgroup G
f : G →* H
hf : Function.Surjective ⇑f
S : Set G
hSfinite : S.Finite
hSclosure : normalClosure S = N
⊢ normalClosure (⇑f '' S) = map f (normalClosure S)
Module: Mathlib.GroupTheory.FixedPointFree

Goal state before:
pp: F : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : FunLike F G G
inst✝ : MonoidHomClass F G G
φ : F
hφ : FixedPointFree ⇑φ
x y : G
h : commutatorMap (⇑φ) x = commutatorMap (⇑φ) y
⊢ x * (φ x)⁻¹ * φ y = y

Tactic:
← eq_div_iff_mul_eq',

Goal state after:
F : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : FunLike F G G
inst✝ : MonoidHomClass F G G
φ : F
hφ : FixedPointFree ⇑φ
x y : G
h : commutatorMap (⇑φ) x = commutatorMap (⇑φ) y
⊢ x * (φ x)⁻¹ = y / φ y
Module: Mathlib.GroupTheory.FixedPointFree

Goal state before:
pp: F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g h : G
key : g * h = ((fun x ↦ x⁻¹) h)⁻¹ * ((fun x ↦ x⁻¹) g)⁻¹
⊢ Commute g h

Tactic:
inv_inv,

Goal state after:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g h : G
key : g * h = h * ((fun x ↦ x⁻¹) g)⁻¹
⊢ Commute g h
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (h k : G), h ∈ H.focalSubgroup → k ∈ H → k * h * k⁻¹ ∈ H.focalSubgroup

Tactic:
intro n g hn hg

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
n g : G
hn : n ∈ H.focalSubgroup
hg : g ∈ H
⊢ g * n * g⁻¹ ∈ H.focalSubgroup
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ ((↑P).transferFocal.domRestrict P).ker = (↑P).focalSubgroupOf

Tactic:
by
  ext g
  have hQ : IsPGroup p (P ⧸ P.focalSubgroupOf) := P.2.to_quotient P.focalSubgroupOf
  rw [MonoidHom.mem_ker, MonoidHom.domRestrict_apply, transferFocal_eq_pow]
  simpa using (hQ.powEquiv' P.not_dvd_index).apply_eq_iff_eq (x := g) (y := 1)

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
⊢ IsCyclicallyReduced (reduceCyclically L)

Tactic:
induction L using List.bidirectionalRec
  case nil => simp
  case singleton => simp
  case cons_append a l b ih =>
    rw [reduceCyclically.cons_append]
    split
    case isTrue => exact ih (h.infix ⟨[a], [b], rfl⟩)
    case isFalse h' =>
      rw [isCyclicallyReduced_cons_append_iff]
      exact ⟨h, by simpa using h'⟩

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

Goal state before:
pp: G A : Type u
inst✝² : Group G
inst✝¹ : IsFreeGroup G
inst✝ : MulAction G A
X : Type u
⊢ ∀ [inst : Group X] (f : Labelling (Generators (ActionCategory G A)) X),
    ∃! F, ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), F.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g

Tactic:
_

Goal state after:
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
⊢ ∀ (f : Labelling (Generators (ActionCategory G A)) X),
    ∃! F, ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), F.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g