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
⊢ ∃ C > 0, ∀ᶠ (y : B) in 𝓝 x, ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ < C

Tactic:
by
  refine ⟨(1 + ‖(trivializationAt F E x).continuousLinearMapAt ℝ  x‖) * 2, by positivity, ?_⟩
  filter_upwards [eventually_norm_symmL_trivializationAt_self_comp_lt F E x one_lt_two] with y hy
  have A : ((trivializationAt F E x).continuousLinearMapAt ℝ x) ∘L
      ((trivializationAt F E x).symmL ℝ x) = ContinuousLinearMap.id _ _ := by
    ext v
    have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x
    simp only [Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply,
      mem_baseSet_trivializationAt, comp_apply, id_apply]
    convert! ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v
    simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
  have : (trivializationAt F E x).continuousLinearMapAt ℝ y =
    (ContinuousLinearMap.id _ _) ∘L ((trivializationAt F E x).continuousLinearMapAt ℝ y) := by simp
  grw [this, ← A, comp_assoc, opNorm_comp_le]
  gcongr
  linarith

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

Goal state before:
pp: case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.wordProd [] = 1

Tactic:
rw [wordProd_nil]

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

Goal state before:
pp: B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
⊢ (alternatingWord i j p)[k + 1] = (alternatingWord j i p)[k]

Tactic:
by
  rw [getElem_alternatingWord i j p (k + 1) (by lia),
    getElem_alternatingWord j i p k (by lia)]
  by_cases h_even : Even (p + k)
  · 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]
  · rw [if_neg h_even, ← add_assoc]
    simp [Odd.add_one (Nat.not_even_iff_odd.mp h_even)]

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

Goal state before:
pp: case neg
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 [Odd.add_one (by simpa using 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.odd_add.mpr; simp [h_even] : Odd (2 * p + k))]

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
i i' : B
m : ℕ
hm : m ≤ M.M i i' * 2
⊢ (if Even ↑m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ↑(m / 2) =
    (if Even ↑(M.M i i' * 2 - m) then 1 else cs.simple i) * (cs.simple i' * cs.simple i) ^ ↑((M.M i i' * 2 - m) / 2)

Tactic:
Int.natCast_ediv,

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hm : m ≤ M.M i i' * 2
⊢ (if Even ↑m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (↑m / ↑2) =
    (if Even ↑(M.M i i' * 2 - m) then 1 else cs.simple i) * (cs.simple i' * cs.simple i) ^ (↑(M.M i i' * 2 - m) / ↑2)
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 : ℤ
⊢ (if Even (2 * k) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (2 * k / 2) =
    (if Even (↑(M.M i i') * 2 - 2 * k) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - 2 * k) / 2)

Tactic:
rw [if_pos (by use k; ring), if_pos (by use -k + (M i i'); ring), mul_comm 2 k, ← sub_mul]
    repeat rw [Int.mul_ediv_cancel _ (by simp)]
    rw [zpow_sub, zpow_natCast, simple_mul_simple_pow' cs i i', ← inv_zpow]
    simp

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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m m' : M i
w : Word M
⊢ (m * m') • w = m • m' • w

Tactic:
by
    dsimp +instances [instHSMul]
    simp [mul_assoc, ← equivPair_symm, Equiv.apply_symm_apply]

Goal state after:
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
⊢ cs.length (cs.wordProd ω) ≤ ω.length

Tactic:
by
  classical
  exact Nat.find_min' (cs.exists_word_with_prod (π ω)) ⟨ω, rfl, rfl⟩

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

Goal state before:
pp: case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
length_lt_one : cs.length (cs.simple i) < 1
this✝ : cs.lengthParity (cs.simple i) = Multiplicative.ofAdd 0
this : Multiplicative.ofAdd 0 = Multiplicative.ofAdd 1
⊢ False

Tactic:
contradiction

Goal state after:
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
⊢ w.toList.head? = some ⟨i, w.head⟩

Tactic:
fun_induction toList with grind [head]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case nil
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
hnot1 : ∀ l ∈ [], l.snd ≠ 1
hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) []
h : { toList := [], ne_one := hnot1, chain_ne := hchain } ≠ empty
⊢ ∃ i j w', w'.toWord.toList = { toList := [], ne_one := hnot1, chain_ne := hchain }.toList

Tactic:
contradiction

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case cons.cons
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hi :
  ∀ (hnot1 : ∀ l_1 ∈ y :: l, l_1.snd ≠ 1) (hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (y :: l)),
    { toList := y :: l, ne_one := hnot1, chain_ne := hchain } ≠ empty →
      ∃ i j w', w'.toWord.toList = { toList := y :: l, ne_one := hnot1, chain_ne := hchain }.toList
hnot1✝ : ∀ l_1 ∈ x :: y :: l, l_1.snd ≠ 1
hnot1 : x.snd ≠ 1 ∧ ∀ x ∈ y :: l, x.snd ≠ 1
hchain✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (x :: y :: l)
hchain : x.fst ≠ y.fst ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (y :: l)
h : { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain✝ } ≠ empty
⊢ ∃ i j w', w'.toWord.toList = { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain✝ }.toList

Tactic:
specialize hi hnot1.2 hchain.2 (by rintro ⟨rfl⟩)

Goal state after:
case cons.cons
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hnot1✝ : ∀ l_1 ∈ x :: y :: l, l_1.snd ≠ 1
hnot1 : x.snd ≠ 1 ∧ ∀ x ∈ y :: l, x.snd ≠ 1
hchain✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (x :: y :: l)
hchain : x.fst ≠ y.fst ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (y :: l)
hi : ∃ i j w', w'.toWord.toList = { toList := y :: l, ne_one := ⋯, chain_ne := ⋯ }.toList
h : { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain✝ } ≠ empty
⊢ ∃ i j w', w'.toWord.toList = { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain✝ }.toList
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ H, ∃ b_1 ∈ ⊥, b = a_1 * a * b_1) → b * a⁻¹ ∈ H

pp: case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ b * a⁻¹ ∈ H → ∃ a_2 ∈ H, ∃ b_1 ∈ ⊥, b = a_2 * a * b_1

Tactic:
· rintro ⟨b, hb, a, rfl : a = 1, rfl⟩
    rwa [mul_one, mul_inv_cancel_right]

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ b * a⁻¹ ∈ H → ∃ a_2 ∈ H, ∃ b_1 ∈ ⊥, b = a_2 * a * b_1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case refine_4
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
⊢ (FreeGroup.lift fun i ↦ of (FreeGroup.of ())).comp (lift fun i ↦ FreeGroup.lift fun x ↦ FreeGroup.of i) =
    MonoidHom.id (CoprodI fun x ↦ FreeGroup Unit)

Tactic:
ext i a

Goal state after:
case refine_4
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
i : ι
a : Unit
⊢ (((FreeGroup.lift fun i ↦ of (FreeGroup.of ())).comp (lift fun i ↦ FreeGroup.lift fun x ↦ FreeGroup.of i)).comp of)
      (FreeGroup.of a) =
    ((MonoidHom.id (CoprodI fun x ↦ FreeGroup Unit)).comp of) (FreeGroup.of a)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a b : DivisibleHull M
h : ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b
⊢ a.liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯ ≤ b.liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯

Tactic:
induction a with | mk _ _
       =>  _ 

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
b : DivisibleHull M
num✝ : M
den✝ : ℕ+
h : ArchimedeanClass.mk (mk num✝ den✝) ≤ ArchimedeanClass.mk b
⊢ (mk num✝ den✝).liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯ ≤ b.liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case h₁
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : ArchimedeanClass (DivisibleHull M)
⊢ ((archimedeanClassOrderHom M).comp (archimedeanClassOrderHomInv M)) a = OrderHom.id a

Tactic:
induction a with | mk a
     =>  _ 

Goal state after:
case h₁.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : DivisibleHull M
⊢ ((archimedeanClassOrderHom M).comp (archimedeanClassOrderHomInv M)) (ArchimedeanClass.mk a) =
    OrderHom.id (ArchimedeanClass.mk a)
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
hG : IsFinitelyPresented G
f : G →* H
hf_surj : Function.Surjective ⇑f
hf_ker : f.ker.IsFinitelyNormallyGenerated
⊢ IsFinitelyPresented H

Tactic:
obtain ⟨n, φ, hφ_surj, hφ_ker⟩ := hG.out

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
hG : IsFinitelyPresented G
f : G →* H
hf_surj : Function.Surjective ⇑f
hf_ker : f.ker.IsFinitelyNormallyGenerated
n : ℕ
φ : FreeGroup (Fin n) →* G
hφ_surj : Function.Surjective ⇑φ
hφ_ker : φ.ker.IsFinitelyNormallyGenerated
⊢ IsFinitelyPresented H
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 : G
hg : 1 = 2
key : φ g = g
⊢ False

Tactic:
contradiction

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

Goal state before:
pp: α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n : ℕ
hn : 0 ≠ 0
⊢ IsReduced (L₁ ++ (replicate 0 L₂).flatten ++ L₃)

Tactic:
contradiction

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H (n - n) = ⊥

Tactic:
rw [tsub_self]

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H 0 = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H (n - n) = ⊤

Tactic:
rw [tsub_self]

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H 0 = ⊤
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 := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
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'
t✝ : A
g✝ : G
⊢ E.map (homOfPair t✝ g✝) ≍ (uncurry F' ⋯).map (homOfPair t✝ g✝)

Tactic:
simp only [← this, uncurry_map, curry_apply_left, coe_back, homOfPair.val]

Goal state after:
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 := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
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'
t✝ : A
g✝ : G
⊢ E.map (homOfPair t✝ g✝) ≍ E.map (homOfPair t✝ g✝)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H (n - n) = ⊥

Tactic:
rw [tsub_self]

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H 0 = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H (n - n) = ⊤

Tactic:
rw [tsub_self]

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H 0 = ⊤
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
⊢ ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          map (G'.subtype.prodMap H'.subtype)
            (comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)

Tactic:
let H' := I.map (MonoidHom.snd ..)

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
⊢ ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          map (G'.subtype.prodMap H'.subtype)
            (comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
N : Subgroup G
inst✝⁴ : N.Normal
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsNilpotent G₁
inst✝ : IsNilpotent G₂
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥

Tactic:
refine ⟨max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂), ?_⟩

Goal state after:
G : Type u_1
inst✝⁵ : Group G
N : Subgroup G
inst✝⁴ : N.Normal
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsNilpotent G₁
inst✝ : IsNilpotent G₂
⊢ ⊤.lowerCentralSeries (max (nilpotencyClass G₁) (nilpotencyClass G₂)) = ⊥
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
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
⊢ δ * ‖w‖ ^ 2 + ((g' x) w) w ≤ δ * (‖↑G‖ * ‖G.symm w‖) ^ 2 + ((g' x) w) w

Tactic:
by
      grw [← le_opNorm]
      simp

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : IsTrivialBlock B
⊢ IsBlock G B

Tactic:
obtain hB | rfl := hB
  · exact .of_subsingleton hB
  · exact .univ

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

Goal state before:
pp: case inl
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

pp: case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

Tactic:
· simp [hfB_e]

Goal state after:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G✝ : Type u_1
inst✝³ : Group G✝
α✝ : Type u_2
inst✝² : MulAction G✝ α✝
G : Type u_3
inst✝¹ : AddGroup G
α : Type u_4
inst✝ : AddAction G α
g : G
a b : α
hg : b = g +ᵥ a
x : ↥(SubAddAction.ofStabilizer G a)
hy : g +ᵥ ↑x ∈ {b}
⊢ ↑x ∈ {a}

Tactic:
simpa [hg] using hy

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(ofStabilizer G a)
hy : g • ↑x ∈ {b}
⊢ ↑x ∈ {a}

Tactic:
simpa [hg] using hy

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

Goal state before:
pp: case «3»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 3
ha : Even 3
h2 : g.cycleType = Multiset.replicate 3 2
h✝ : 3 * 2 ≤ card (Fin 5)
h : 3 ≤ 3
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 3 2

Tactic:
contradiction

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

Goal state before:
pp: case h.inl
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn✝ : n + 1 < 2
hn : n = 0
hsn : ∃ a, s = {a}
⊢ (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)

Tactic:
obtain ⟨a, hsa⟩ := hsn

Goal state after:
case h.inl
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn✝ : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
⊢ (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
⊢ Injective ⇑(conjMap_ofFixingSubgroup hst)

pp: case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
⊢ Surjective ⇑(conjMap_ofFixingSubgroup hst)

Tactic:
· rintro x y hxy
    simpa [← SetLike.coe_eq_coe] using hxy

Goal state after:
case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
⊢ Surjective ⇑(conjMap_ofFixingSubgroup hst)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
hst : t ⊆ s
⊢ Injective ⇑(ofFixingSubgroup_of_inclusion M hst)

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
  rw [← SetLike.coe_eq_coe] at hxy ⊢
  exact hxy

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
⊢ (g • x) i = (k • x) i

Tactic:
obtain ⟨j, hxj : (k • x) j = (g • x) i⟩ := hx (k • x) ((g • x) i)
      rcases lt_or_eq_of_le (le_sub_one_of_lt j.prop) with hj | hj
      · suffices i = j by
          rw [← this, ← hi] at hj
          exact (lt_irrefl _ hj).elim
        apply EmbeddingLike.injective (g • x)
        rw [hgk' j hj, hxj]
      · rw [← hxj]
        apply congr_arg
        rw [Fin.ext_iff, hi, hj]

Goal state after: