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

Goal state before:
pp: E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → NormedAddCommGroup (V x)
inst✝³ : (x : M) → InnerProductSpace ℝ (V x)
inst✝² : FiberBundle F V
cov : CovariantDerivative I F V
inst✝¹ : VectorBundle ℝ F V
inst✝ : IsContMDiffRiemannianBundle I 1 F V
x : M
τ : (x : M) → V x
hτ : MDiffAt (T% τ) x
f✝ : M → ℝ
σ✝ : (x : M) → V x
hf : MDiffAt f✝ x
hσ : MDiffAt (T% σ✝) x
⊢ derivMetricTensorAux I cov (f✝ • σ✝) τ x = f✝ x • derivMetricTensorAux I cov σ✝ τ x

Tactic:
ext X₀
    simp [mvfderiv_fun_mul hf (hσ.inner_bundle hτ),
      cov.isCovariantDerivativeOn.leibniz hσ hf, inner_add_left, inner_smul_left]
    ring

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

Goal state before:
pp: E : Type u_1
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
H : Type u_2
inst✝¹² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → NormedAddCommGroup (V x)
inst✝⁵ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁴ : FiberBundle F V
cov : CovariantDerivative I F V
inst✝³ : VectorBundle ℝ F V
inst✝² : IsContMDiffRiemannianBundle I 1 F V
inst✝¹ : ContMDiffVectorBundle 1 F V I
inst✝ : FiniteDimensional ℝ F
hcov : cov.IsMetricCompatible
x : M
X : (x : M) → TangentSpace I x
σ τ : (x : M) → V x
hσ : MDiffAt (T% σ) x
hτ : MDiffAt (T% τ) x
⊢ ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) =
    (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x + (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x

Tactic:
have H := congr($hcov x (σ x) (τ x) (X x))
  simp [derivMetricTensor_apply _ _ hσ hτ] at H
  linear_combination H

Goal state after:
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
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
⊢ ∑ i ∈ s, f i x • cov i (g • σ) x = g x • ∑ i ∈ s, f i x • cov i σ x + (d% g x).smulRight (σ x)

Tactic:
by
    calc ∑ i ∈ s, f i x • cov i (g • σ) x
      _ = ∑ i ∈ s, (g x • f i x • cov i σ x + f i x • (d% g x).smulRight (σ x)) := by
          congr! 1 with i hi
          rw [(h i).leibniz hσ hg]
          simp [mvfderiv]
          module
      _ = g x • ∑ i ∈ s, f i x • cov i σ x + (∑ i ∈ s, f i) x • (d% g x).smulRight (σ x) := by
          rw [Finset.sum_add_distrib, Finset.smul_sum, Finset.sum_apply, Finset.sum_smul]
      _ = g x • ∑ i ∈ s, f i x • cov i σ x + (d% g x).smulRight (σ x) := by rw [hf]; simp

Goal state after:
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
⊢ (↑(mfderiv% ⇑f.embeddingPiTangent x)).ker ≤ (↑(mfderiv% ↑(chartAt H (f.c (f.ind x hx))) x)).ker

Tactic:
← comp_embeddingPiTangent_mfderiv

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
⊢ (↑(mfderiv% ⇑f.embeddingPiTangent x)).ker ≤
    (↑((ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (f.ind x hx)) ∘SL
          mfderiv% ⇑f.embeddingPiTangent x)).ker
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

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

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

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case pos
n : ℕ
h0 : n = 0
⊢ commProb (DihedralGroup 0) * commProb (Product []) = 1 / ↑0

Tactic:
commProb_nil,

Goal state after:
case pos
n : ℕ
h0 : n = 0
⊢ commProb (DihedralGroup 0) * 1 = 1 / ↑0
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case pos
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ commProb (Product []) = 1 / ↑1

Tactic:
commProb_nil,

Goal state after:
case pos
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ 1 = 1 / ↑1
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 * 2 / 2) = 1 * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') - k) * 2 / 2)

Tactic:
repeat rw [Int.mul_ediv_cancel _ (by simp)]

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') - k)
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
ω : List B
⊢ (cs.rightInvSeq ω).length = ω.length

Tactic:
induction ω with
  | nil => simp
  | cons i ω ih => simpa [rightInvSeq]

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
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
hm : m > M.M i i'
⊢ ¬cs.IsReduced (alternatingWord i i' m)

Tactic:
induction hm with
  | refl => -- Base case; m = M i i' + 1
    suffices h : ℓ (π (alternatingWord i i' (M i i' + 1))) < M i i' + 1 by
      unfold IsReduced
      rw [Nat.succ_eq_add_one, length_alternatingWord]
      lia
    have : M i i' + 1 ≤ M i i' * 2 := by linarith [Nat.one_le_iff_ne_zero.mpr hM]
    rw [cs.prod_alternatingWord_eq_prod_alternatingWord_sub i i' _ this]
    have : M i i' * 2 - (M i i' + 1) = M i i' - 1 := by lia
    rw [this]
    calc
      ℓ (π (alternatingWord i' i (M i i' - 1)))
      _ ≤ (alternatingWord i' i (M i i' - 1)).length := cs.length_wordProd_le _
      _ = M i i' - 1 := length_alternatingWord _ _ _
      _ ≤ M i i' := Nat.sub_le _ _
      _ < M i i' + 1 := Nat.lt_succ_self _
  | step m ih => -- Inductive step
    contrapose ih
    rw [alternatingWord_succ'] at ih
    apply IsReduced.drop (j := 1) at ih
    simpa using ih

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
w : W
i : B
⊢ ¬cs.IsRightDescent w i ↔ cs.length (w * cs.simple i) = cs.length w + 1

Tactic:
unfold IsRightDescent
  constructor
  · intro _
    exact (cs.length_mul_simple w i).resolve_right (by lia)
  · lia

Goal state after:
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 M
⊢ ((archimedeanClassOrderHomInv M).comp (archimedeanClassOrderHom M)) a = OrderHom.id a

Tactic:
induction a with | mk _
     =>  _ 

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✝ : M
⊢ ((archimedeanClassOrderHomInv M).comp (archimedeanClassOrderHom M)) (ArchimedeanClass.mk a✝) =
    OrderHom.id (ArchimedeanClass.mk a✝)
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)
⊢ HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))

Tactic:
by
    rwa [Monoid.exponent_eq_of_mulEquiv (monoidHom_mulEquiv_of_hasEnoughRootsOfUnity G M).some]

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 : ℤ
h1n : 1 ≤ n
⊢ a i ^ n • (Y i)ᶜ ⊆ X i

Tactic:
induction n, h1n using Int.leInduction with
          | base => rw [zpow_one]; exact hX i
          | succ n _hle hi =>
            calc
              a i ^ (n + 1) • (Y i)ᶜ = (a i ^ n * a i) • (Y i)ᶜ := by rw [zpow_add, zpow_one]
              _ = a i ^ n • a i • (Y i)ᶜ := mul_smul _ _ _
              _ ⊆ a i ^ n • X i := smul_set_mono <| hX i
              _ ⊆ a i ^ n • (Y i)ᶜ := smul_set_mono (hXYdisj i i).subset_compl_right
              _ ⊆ X i := hi

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x✝¹ : α × Bool
ha : (head :: tail).getLast? = some x✝¹
x✝ : α × Bool
hb : x✝ ∈ (replicate (n + 1) (head :: tail)).flatten.head?
⊢ x✝¹.1 = x✝.1 → x✝¹.2 = x✝.2

Tactic:
rw [Option.mem_def, List.head?_flatten_replicate (h := by simp +arith)] at hb

Goal state after:
α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x✝¹ : α × Bool
ha : (head :: tail).getLast? = some x✝¹
x✝ : α × Bool
hb : (head :: tail).head? = some x✝
⊢ x✝¹.1 = x✝.1 → x✝¹.2 = x✝.2
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ : G
⊢ x✝ ∈ N.upperCentralSeriesStep ↔ ∀ (x : G), ↑x * (mk' N) x✝ = (mk' N) x✝ * ↑x

Tactic:
refine forall_congr' fun y => ?_

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ y : G
⊢ ⁅x✝, y⁆ ∈ N ↔ ↑y * (mk' N) x✝ = (mk' N) x✝ * ↑y
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α × Bool
h : startsWith a = startsWith b
⊢ a = b

Tactic:
by
  simp only [startsWith, Set.ext_iff, Set.mem_ofPred_eq] at h
  simpa using h (mk [a])

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
H : ℕ → Subgroup ↥S
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ S.lowerCentralSeries n = ⊥

Tactic:
have h1 := descending_central_series_ge_lower H hH n

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
H : ℕ → Subgroup ↥S
hH : IsDescendingCentralSeries H
hn : H n = ⊥
h1 : ⊤.lowerCentralSeries n ≤ H n
⊢ S.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), ⊤.lowerCentralSeries n = ⊥ → ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
rintro n h
    exact ⟨lowerCentralSeries ⊤, ⟨lowerCentralSeries_isDescendingCentralSeries, h⟩⟩

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
⊢ Setoid.IsPartition (range fun a ↦ orbit G a)

Tactic:
by
  apply orbit.pairwiseDisjoint.isPartition_of_exists_of_ne_empty
  · intro x
    exact ⟨_, ⟨x, rfl⟩, mem_orbit_self x⟩
  · rintro ⟨a, ha : orbit G a = ∅⟩
    exact (MulAction.nonempty_orbit a).ne_empty ha

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

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ (g * k) • a = g • k • a

Tactic:
← smul_smul

Goal state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ g • k • a = g • k • a
Module: Mathlib.GroupTheory.GroupAction.Iwasawa

Goal state before:
pp: M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
x✝ : fixedPoints (↥N) α = Set.univ ∨ commutator M ≤ N
⊢ N = ⊥ ∨ N = ⊤

Tactic:
cases or_iff_not_imp_left.mpr (IwaS.commutator_le N) with

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * ↑⟨σ, hσ✝⟩ * π⁻¹ = ↑⟨τ, hτ⟩
⊢ IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩

Tactic:
rw [Subtype.coe_mk, Subtype.coe_mk] at hπ

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
⊢ IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ -1 * sign (swap a b) = 1

Tactic:
sign_swap ab,

Goal state after:
case inr.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = -1
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ -1 * -1 = 1
Module: Mathlib.SetTheory.Cardinal.Embedding

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : ↑s.ncard + ↑n ≤ ENat.card α
hα : Finite α
x✝ : Fintype α := Fintype.ofFinite α
⊢ n ≤ Fintype.card ↑sᶜ

Tactic:
← add_le_add_iff_left s.ncard,

Goal state after:
case inl
α : Type u_1
n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : ↑s.ncard + ↑n ≤ ENat.card α
hα : Finite α
x✝ : Fintype α := Fintype.ofFinite α
⊢ s.ncard + n ≤ s.ncard + Fintype.card ↑sᶜ
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : ∀ (x_1 : Fin n.succ), (g • snoc x) x_1 = (snoc y) x_1
⊢ g ∈ stabilizer G a

Tactic:
convert! hgxy (last n)

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : ∀ (x_1 : Fin n.succ), (g • snoc x) x_1 = (snoc y) x_1
⊢ g ∈ stabilizer G a ↔ (g • snoc x) (last n) = (snoc y) (last n)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case mp
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
⊢ IsMultiplyPreprimitive M α n.succ → IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n

pp: case mpr
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n → IsMultiplyPreprimitive M α n.succ

Tactic:
· apply isMultiplyPreprimitive_ofStabilizer

Goal state after:
case mpr
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n → IsMultiplyPreprimitive M α n.succ
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: α : 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'
x : Fin (Fintype.card α) ↪ α
⊢ Function.Surjective x.toFun

Tactic:
apply Function.Bijective.surjective

Goal state after:
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := ⋯
k : Perm α
a✝ : k ∈ ⊤
x✝ : Fin (Fintype.card α) ↪ α := ⋯
x' : Fin (Fintype.card α - 1) ↪ α := ⋯
g : ↥G
hg' : g • x' = k • x'
x : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective x.toFun
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case h
α : Type u_2
inst✝² : DecidableEq α
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : ¬AddAction.toPerm g = 1
a : α
ha : g +ᵥ a ≠ a
s : ↑(powersetCard α n)
has : a ∈ s
has' : (AddAction.toPerm g) s = 1 s
⊢ g +ᵥ a ∈ s

Tactic:
simp only [AddAction.toPerm_apply, coe_one, id_eq] at has'

Goal state after:
case h
α : Type u_2
inst✝² : DecidableEq α
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : ¬AddAction.toPerm g = 1
a : α
ha : g +ᵥ a ≠ a
s : ↑(powersetCard α n)
has : a ∈ s
has' : g +ᵥ s = s
⊢ g +ᵥ a ∈ s
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝ : Group H
f : G →* H
x : H
hx : ∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x
g : G
⊢ (lift f x hx) (of g) = f g

Tactic:
delta HNNExtension; simp [lift, of]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝ : Group H
f : G →* H
x : H
hx : ∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x
g : G
⊢ (lift f x hx) (of g) = f g

Tactic:
by
  delta HNNExtension; simp [lift, of]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
motive : NormalWord d → Sort u_4
w : NormalWord d
ofGroup : (g : G) → motive (NormalWord.ofGroup g)
cons :
  (g : G) →
    (u : ℤˣ) →
      (w : NormalWord d) →
        (h1 : w.head ∈ d.set u) →
          (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') →
            motive w → motive (NormalWord.cons g u w h1 h2)
⊢ motive w

Tactic:
rcases w with ⟨⟨g, l, chain⟩, mem_set⟩

Goal state after:
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
motive : NormalWord d → Sort u_4
ofGroup : (g : G) → motive (NormalWord.ofGroup g)
cons :
  (g : G) →
    (u : ℤˣ) →
      (w : NormalWord d) →
        (h1 : w.head ∈ d.set u) →
          (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') →
            motive w → motive (NormalWord.cons g u w h1 h2)
g : G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l
mem_set : ∀ (u : ℤˣ) (g_1 : G), (u, g_1) ∈ { head := g, toList := l, chain := chain }.toList → g_1 ∈ d.set u
⊢ motive { head := g, toList := l, chain := chain, mem_set := mem_set }
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg.cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
u' : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u'
h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1
hcan✝ :
  ¬Cancels (-u)
      (if h : Cancels u (cons g u' w h1 h2) then unitsSMulWithCancel φ u (cons g u' w h1 h2) h
      else
        let g' := unitsSMulGroup φ d u (cons g u' w h1 h2).head;
        cons (↑g'.1) u ((↑g'.2 * (cons g u' w h1 h2).head⁻¹) • cons g u' w h1 h2) ⋯ ⋯)
hcan2 : Cancels u (cons g u' w h1 h2)
hcan : ¬Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2)
⊢ cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head).1) (-u)
      ((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head).2 *
          (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2).head⁻¹) •
        unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2)
      ⋯ ⋯ =
    cons g u' w h1 h2

Tactic:
simp only [unitsSMulGroup, SetLike.coe_sort_coe, unitsSMulWithCancel, consRecOn_cons,
        group_smul_head,
        mul_inv_rev]

Goal state after:
case neg.cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g : G
u' : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u'
h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1
hcan✝ :
  ¬Cancels (-u)
      (if h : Cancels u (cons g u' w h1 h2) then unitsSMulWithCancel φ u (cons g u' w h1 h2) h
      else
        let g' := unitsSMulGroup φ d u (cons g u' w h1 h2).head;
        cons (↑g'.1) u ((↑g'.2 * (cons g u' w h1 h2).head⁻¹) • cons g u' w h1 h2) ⋯ ⋯)
hcan2 : Cancels u (cons g u' w h1 h2)
hcan : ¬Cancels (-u) (unitsSMulWithCancel φ u (cons g u' w h1 h2) hcan2)
⊢ cons (↑((toSubgroupEquiv φ (-u)) (⋯.equiv (↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩) * w.head)).1)) (-u)
      ((↑(⋯.equiv (↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩) * w.head)).2 * (w.head⁻¹ * (↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩))⁻¹)) •
        ↑((toSubgroupEquiv φ u) ⟨g, ⋯⟩) • w)
      ⋯ ⋯ =
    cons g u' w h1 h2
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : M
⊢ (f.noncommCoprod g comm) (a, 1) = f a

Tactic:
by rw [noncommCoprod_apply, map_one, mul_one]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan✝ :
  ¬Cancels (-u)
      (if h : Cancels u w then unitsSMulWithCancel φ u w h
      else
        let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯)
hcan2 : Cancels u w
hcan : ¬Cancels (-u) (unitsSMulWithCancel φ u w hcan2)
⊢ cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u w hcan2).head).1) (-u)
      ((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u w hcan2).head).2 *
          (unitsSMulWithCancel φ u w hcan2).head⁻¹) •
        unitsSMulWithCancel φ u w hcan2)
      ⋯ ⋯ =
    w

Tactic:
cases w using consRecOn with

Goal state after: