mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: case ha
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 : ((g' x) w) w ≤ (1 - δ * C)⁻¹ * ((g' y) w) w
⊢ 0 ≤ ‖v‖ ^ 2

Tactic:
positivity

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δ : (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 : ((g' x) w) w ≤ (1 - δ * C)⁻¹ * ((g' y) w) w
⊢ 0 < r' ^ 2

Tactic:
positivity

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
⊢ Function.LeftInverse (fun f x ↦ f.comp of) fun fi ↦ (conGen (Rel M)).lift (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) ⋯

Tactic:
intro fi
    ext i x
    rfl

Goal state after:
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
a : PresentedGroup M.relationsSet
⊢ cs.mulEquiv (cs.mulEquiv.symm a) = a

Tactic:
MulEquiv.apply_symm_apply

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
a : PresentedGroup M.relationsSet
⊢ a = a
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
⊢ (1 + ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖) * 2 > 0

Tactic:
positivity

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

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
⊢ Injective simple

Tactic:
intro cs1 cs2 h
  apply CoxeterSystem.ext
  apply MulEquiv.toMonoidHom_injective
  apply cs1.ext_simple
  nth_rw 2 [h]
  simp [simple]

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 < 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
hk : take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h_even : Even k
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)

Tactic:
simp only [h_even, ↓reduceIte] at hk
        simp only [Nat.not_even_iff_odd.mpr (Even.add_one h_even), ↓reduceIte]
        rw [← List.take_concat_get (by simp; lia), alternatingWord_succ, ← hk]
        apply congr_arg
        rw [getElem_alternatingWord i j (2 * p) k (by lia)]
        simp [(by apply Nat.even_add.mpr; simp [h_even] : Even (2 * p + k))]

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

Goal state before:
pp: case inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ k = 1 * (cs.simple i' * cs.simple i) ^ (↑(M.M i i') - k)

Tactic:
zpow_sub,

Goal state after:
case inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ k =
    1 * ((cs.simple i' * cs.simple i) ^ ↑(M.M i i') * ((cs.simple i' * cs.simple i) ^ k)⁻¹)
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
⊢ cs.lengthParity (cs.wordProd ω) = Multiplicative.ofAdd ↑(cs.length (cs.wordProd ω))

Tactic:
hω,

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
⊢ cs.lengthParity (cs.wordProd ω) = Multiplicative.ofAdd ↑ω.length
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
by
  rcases (cs.length_mul_simple_ne w i).lt_or_gt with h | h <;> rw [← Nat.add_one_le_iff] at h
  · refine .inr (h.antisymm ?_)
    simpa using cs.length_le_length_mul_add_right w (s i)
  · refine .inl (h.antisymm' ?_)
    simpa using cs.length_mul_le w (s i)

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

Goal state before:
pp: case succ.cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
k : B
ω : List B
tail_ih✝ : cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
⊢ cs.rightInvSeq (drop (j + 1) (k :: ω)) = drop (j + 1) (cs.rightInvSeq (k :: ω))

Tactic:
rw [drop_succ_cons, ih₁ ω, rightInvSeq, drop_succ_cons]

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

Goal state before:
pp: case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.leftInvSeq ω).length
ht : (cs.leftInvSeq ω)[j] ∈ cs.leftInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)

Tactic:
cs.length_leftInvSeq

Goal state after:
case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj✝ : j < (cs.leftInvSeq ω).length
hj : j < ω.length
ht : (cs.leftInvSeq ω)[j] ∈ cs.leftInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
x : M i
hnotone : x * w.head ≠ 1
⊢ (w.mulHead x hnotone).prod = of x * w.prod

Tactic:
unfold mulHead
  induction w with
  | singleton => simp [replaceHead]
  | append _ _ _ w_ih_w₁ w_ih_w₂ =>
    specialize w_ih_w₁ _ hnotone
    simp only [replaceHead, append_prod, ← mul_assoc]
    congr 1

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑K
hxy : x✝ = x * a * y
⊢ ∃ i, a⁻¹ * (↑i)⁻¹ * x✝ ∈ ↑K

Tactic:
refine ⟨⟨x, hx⟩, ?_⟩

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑K
hxy : x✝ = x * a * y
⊢ a⁻¹ * (↑⟨x, hx⟩)⁻¹ * x✝ ∈ ↑K
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
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' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
this : ‖(Trivialization.symmL ℝ (trivializationAt F E x) y) w‖ ^ 2 ≤ r' ^ 2 * ‖v‖ ^ 2
⊢ 0 ≤ r' * ‖v‖

Tactic:
positivity

Goal state after:
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
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h.some
⊢ ∃ i, e a i ≠ 1

Tactic:
by
    contrapose! ha
    exact (MulEquiv.map_eq_one_iff e).mp <| funext ha

Goal state after:
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 := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n✝ n : ℤ
hle : n ≤ -1
hi : a i ^ n • (X i)ᶜ ⊆ Y i
⊢ a i ^ (n - 1) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ

Tactic:
zpow_sub,

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 := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n✝ n : ℤ
hle : n ≤ -1
hi : a i ^ n • (X i)ᶜ ⊆ Y i
⊢ (a i ^ n * (a i ^ 1)⁻¹) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  (center ↥(closureCommutatorRepresentatives G)).index ^
      ((center ↥(closureCommutatorRepresentatives G)).index *
          Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) +
        1) =
    0
h : Nat.card ↥(_root_.commutator G) = 0
⊢ False

Tactic:
exact FiniteIndex.index_ne_zero (eq_zero_of_pow_eq_zero h2)

Goal state after:
Module: Mathlib.Order.Radical

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ f (Order.radical α) = Order.radical β

Tactic:
by
  unfold Order.radical
  simp only [OrderIso.map_iInf]
  fapply Equiv.iInf_congr
  · exact f.toEquiv
  · simp

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
⊢ reduceCyclically [] = []

Tactic:
simp [reduceCyclically]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a : α × Bool
⊢ reduceCyclically [a] = [a]

Tactic:
simp [reduceCyclically]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a b : α × Bool
L : List (α × Bool)
⊢ reduceCyclically (a :: (L ++ [b])) = if b.1 = a.1 ∧ (!b.2) = a.2 then reduceCyclically L else a :: L ++ [b]

Tactic:
simp [reduceCyclically]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
⊢ N.upperCentralSeriesStep = comap (mk' N) (center (G ⧸ N))

Tactic:
by
  ext
  rw [mem_comap, mem_center_iff, forall_mk]
  refine forall_congr' fun y => ?_
  rw [coe_mk', ← QuotientGroup.mk_mul, ← QuotientGroup.mk_mul, eq_comm, eq_iff_div_mem,
    div_eq_mul_inv, mul_inv_rev, commutatorElement_def]
  simp_rw [mul_assoc]

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

Goal state before:
pp: case h_map
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' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := ⋯
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE : ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), E.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g
this : curry E = F'
⊢ ∀ (X_1 Y : ActionCategory G A) (f : X_1 ⟶ Y), E.map f ≍ (uncurry F' ⋯).map f

Tactic:
refine ActionCategory.cases ?_
        intros
        simp only [← this, uncurry_map, curry_apply_left, coe_back, homOfPair.val]
        rfl

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝ : Group G
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G n.succ
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) (n + 1)) = upperCentralSeries G (n + 1).succ

Tactic:
let Hn := upperCentralSeries (G ⧸ center G) n

Goal state after:
case succ
G : Type u_1
inst✝ : Group G
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G n.succ
Hn : Subgroup (G ⧸ center G) := upperCentralSeries (G ⧸ center G) n
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) (n + 1)) = upperCentralSeries G (n + 1).succ
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a x : X
⊢ (∃ g, g • a = x) ↔ (x ∈ orbit G a ↔ x ∈ Set.univ)

Tactic:
Set.mem_univ,

Goal state after:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a x : X
⊢ (∃ g, g • a = x) ↔ (x ∈ orbit G a ↔ True)
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
⊢ IsPretransitive N β

Tactic:
apply MulAction.IsPretransitive.mk
  intro x y
  obtain ⟨x', rfl⟩ := hf x
  obtain ⟨y', rfl⟩ := hf y
  obtain ⟨g, rfl⟩ := h.exists_smul_eq x' y'
  exact ⟨φ g, by simp only [map_smulₛₗ]⟩

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
H : Subgroup G
hH : normalizer ↑H = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := ⋯
⊢ comap (mk' (center G)) (normalizer ↑H') = comap (mk' (center G)) H'

Tactic:
comap_normalizer_eq_of_surjective _ hsur,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
H : Subgroup G
hH : normalizer ↑H = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ normalizer ↑(comap (mk' (center G)) H') = comap (mk' (center G)) H'
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s✝ s : Set α
g : G
h : g ∈ stabilizer G s
⊢ g ∈ stabilizer G sᶜ

Tactic:
simp [Set.smul_set_compl, mem_stabilizer_iff.1 h]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
⊢ IsPreprimitive H Y

Tactic:
by
  refine ⟨fun {B} hB ↦ ?_⟩
  rcases B.eq_empty_or_nonempty with hB' | hB'; · simp [IsTrivialBlock, hB']
  rw [IsTrivialBlock, or_iff_not_imp_right]
  intro hB_ne_top
  -- we need Set.Subsingleton B ↔ Set.ncard B ≤ 1
  suffices Set.ncard B < 2 by simpa [Nat.lt_succ_iff] using this
  -- We reduce to proving that (Set.range f).ncard ≤ (orbit N B).ncard
  apply lt_of_mul_lt_mul_right' (hf'.trans_le' _)
  simp only [← hB.ncard_block_mul_ncard_orbit_eq hB']
  apply Nat.mul_le_mul_left
  -- We reduce to proving that (Set.range f ∩ g • B).ncard ≤ 1 for every g
  have hfin := Fintype.ofFinite (Set.range fun g : H ↦ g • B)
  rw [(hB.isBlockSystem hB').left.ncard_eq_finsum, finsum_eq_sum_of_fintype]
  apply le_trans (Finset.sum_le_card_nsmul _ _ 1 _)
  · rw [nsmul_one, Finset.card_univ, ← Set.toFinset_card, ← Set.ncard_eq_toFinset_card',
      orbit, Nat.cast_id]
  · rintro ⟨x, ⟨g, rfl⟩⟩ -
    suffices Set.Subsingleton (Set.range f ∩ g • B) by simpa
    -- It suffices to prove that the preimage is subsingleton
    rw [← Set.image_preimage_eq_range_inter]
    apply Set.Subsingleton.image
    -- Since the action of M on α is primitive, it suffices to prove that
    -- the preimage is a block which is not ⊤
    apply Or.resolve_right (isTrivialBlock_of_isBlock ((hB.translate g).preimage f))
    intro h
    simp only [Set.preimage_eq_univ_iff] at h
    -- We will prove that B is large, which will contradict the assumption that it is not ⊤
    apply hB_ne_top
    apply hB.eq_univ_of_card_lt
    -- It remains to show that Nat.card β < Set.ncard B * 2
    apply lt_of_lt_of_le hf'
    rw [mul_comm, mul_le_mul_iff_left₀ Nat.succ_pos']
    apply le_trans (Set.ncard_le_ncard h) (Set.ncard_image_le B.toFinite)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ closure {g | g.cycleType = {2, 2}} = alternatingGroup α

Tactic:
apply le_antisymm
  · rw [Subgroup.closure_le]
    intro g hg
    simp only [Set.mem_ofPred_eq] at hg
    simp [mem_alternatingGroup, sign_of_cycleType, hg, ← Units.val_inj]
  · rw [← Equiv.Perm.closure_three_cycles_eq_alternating, Subgroup.closure_le]
    intro g hg3
    obtain ⟨a, ha⟩ := hg3.isCycle.nonempty_support
    have h_support := hg3.support_eq_iff_mem_support.mpr ha
    have h_nodup := hg3.nodup_iff_mem_support.mpr ha
    have : 1 < g.supportᶜ.card := by grind [Finset.card_compl, Nat.card_eq_fintype_card]
    obtain ⟨b, c, hb, hc, hbc⟩ := Finset.one_lt_card_iff.mp this
    have H : g = (swap a (g a) * (swap b c)) * (swap b c * (swap (g a) (g (g a)))) := by
      simp [mul_assoc, ← hg3.eq_swap_mul_swap_iff_mem_support.mpr ha]
    rw [H]
    apply mul_mem <;>
    · apply Subgroup.subset_closure
      exact cycleType_swap_mul_swap_of_nodup (by grind [Finset.mem_compl])

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

Goal state before:
pp: g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h : g.cycleType.card * 2 ≤ card (Fin 5)
⊢ card (Fin 5) ≤ 3 * 2

Tactic:
norm_num only [card_fin]

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

Goal state before:
pp: case ha
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
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' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
hgx : ((g x) v) v = ((g' x) w) w
hgy : ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w
⊢ 0 ≤ ‖v‖ ^ 2

Tactic:
positivity

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
⊢ 2 * (1 + ‖Trivialization.symmL ℝ (trivializationAt F E x) x‖) > 0

Tactic:
positivity

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
x : ↥(alternatingGroup ↥s)
⊢ Perm.ofSubtype ↑x ∈ alternatingGroup α

Tactic:
rw [mem_alternatingGroup, sign_ofSubtype, mem_alternatingGroup.mp x.prop]

Goal state after: