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

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
equiv : E ≃L[𝕜] E'' × F
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hsource : domChart.source ⊆ f ⁻¹' codChart.source
hwrittenInExtend :
  EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (Prod.fst ∘ ⇑equiv) (domChart.extend I).target
aux : IsSubmersionAtOfComplement F I J n f x
⊢ IsSubmersionAt I J n f x

Tactic:
use aux.smallComplement, by infer_instance, by infer_instance

Goal state after:
case h
𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
equiv : E ≃L[𝕜] E'' × F
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hsource : domChart.source ⊆ f ⁻¹' codChart.source
hwrittenInExtend :
  EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (Prod.fst ∘ ⇑equiv) (domChart.extend I).target
aux : IsSubmersionAtOfComplement F I J n f x
⊢ IsSubmersionAtOfComplement aux.smallComplement I J n f x
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
hf : ContinuousAt f x
equiv : E ≃L[𝕜] E'' × F
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hwrittenInExtend :
  EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (Prod.fst ∘ ⇑equiv) (domChart.extend I).target
aux : IsSubmersionAtOfComplement F I J n f x
⊢ IsSubmersionAt I J n f x

Tactic:
use aux.smallComplement, by infer_instance, by infer_instance

Goal state after:
case h
𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
hf : ContinuousAt f x
equiv : E ≃L[𝕜] E'' × F
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hwrittenInExtend :
  EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (Prod.fst ∘ ⇑equiv) (domChart.extend I).target
aux : IsSubmersionAtOfComplement F I J n f x
⊢ IsSubmersionAtOfComplement aux.smallComplement I J n f x
Module: Mathlib.GroupTheory.Coprod.Basic

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

Tactic:
exact one

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

Goal state before:
pp: case one
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
⊢ p 1

Tactic:
exact one

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

Goal state before:
pp: case one
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
⊢ p 1

Tactic:
exact one

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case one
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
one : motive 1
mul : ∀ {i : ι} (m : M i) (x : CoprodI M), motive x → motive (of m * x)
⊢ motive 1

Tactic:
exact one

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
⊢ ((equivPair i) w).head = if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1

Tactic:
by
  simp only [equivPair, equivPairAux]
  induction w using consRecOn with
  | empty => simp
  | cons head =>
    by_cases hi : i = head
    · subst hi; simp
    · simp [hi, Ne.symm hi]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
x y : DivisibleHull M
⊢ a • (x + y) = a • x + a • y

Tactic:
by simp [qsmul_def, smul_add]

Goal state after:
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Finite α
n : ℕ
toFun✝ : α → Fin n
f : Fin n → α
hf_surj : Function.LeftInverse f toFun✝
hf_inj : Function.RightInverse f toFun✝
⊢ (FreeGroup.map f).ker.IsFinitelyNormallyGenerated

Tactic:
(FreeGroup.map f).ker_eq_bot (FreeGroup.map_injective hf_inj.injective)

Goal state after:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Finite α
n : ℕ
toFun✝ : α → Fin n
f : Fin n → α
hf_surj : Function.LeftInverse f toFun✝
hf_inj : Function.RightInverse f toFun✝
⊢ ⊥.IsFinitelyNormallyGenerated
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : IsFinitelyPresented G
inst✝ : IsFinitelyPresented H
⊢ IsFinitelyPresented (Monoid.Coprod G H)

Tactic:
obtain ⟨_, sG, ⟨_ : Finite sG, ⟨φG⟩⟩⟩ := exists_mulEquiv_presentedGroup (G := G)

Goal state after:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : IsFinitelyPresented G
inst✝ : IsFinitelyPresented H
w✝ : ℕ
sG : Set (FreeGroup (Fin w✝))
left✝ : Finite ↑sG
φG : G ≃* PresentedGroup sG
⊢ IsFinitelyPresented (Monoid.Coprod G H)
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ map H.subtype H.focalSubgroupOf ≤ H.focalSubgroup

Tactic:
map_focalSubgroupOf

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.focalSubgroup ≤ H.focalSubgroup
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w w' : α × Bool
⊢ Disjoint (startsWith w) (startsWith w') ↔ w ≠ w'

Tactic:
by
  simp_all only [ne_eq, startsWith, Set.disjoint_iff_inter_eq_empty, Set.ext_iff, Set.mem_inter_iff,
    Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false, not_and, Option.some.injEq]
  exact Iff.intro (fun h ↦ h (mk [w]) (by simp)) (by grind)

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

Goal state before:
pp: case refine_1.cons.inr
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : c✝ ⟶ b✝
eT : Sum.inr e ∈ T b✝ c✝
⊢ F'.map (Sum.recOn (↑⟨Sum.inr e, eT⟩) (fun e ↦ of e) fun e ↦ inv (of e)) = 1

Tactic:
rw [F'.map_inv, inv_as_inv, inv_eq_one, hF']

Goal state after:
case refine_1.cons.inr
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : c✝ ⟶ b✝
eT : Sum.inr e ∈ T b✝ c✝
⊢ f' e = 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
i j : ℕ
hi : i < a + 1
hj : j < a + 1
⊢ upperCentralSeries G i = upperCentralSeries G j → i = j

Tactic:
refine (upperCentralSeries.StrictMonoOn G).injOn ?_ ?_ <;> grind

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

Goal state before:
pp: case e_5
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g ↦ FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ F.map (of e✝) = 1

Tactic:
differenceFunctor_map,

Goal state after:
case e_5
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g ↦ FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ f b✝ *
      (f
          (have this := a✝;
          this))⁻¹ =
    1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
N : Subgroup G
inst✝³ : N.Normal
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
⊢ IsNilpotent ((i : η) → Gs i)

Tactic:
by
  cases nonempty_fintype η
  rw [nilpotent_iff_lowerCentralSeries]
  refine ⟨Finset.univ.sup fun i => Group.nilpotencyClass (Gs i), ?_⟩
  rw [top_lowerCentralSeries_pi_of_finite, pi_eq_bot_iff]
  intro i
  rw [lowerCentralSeries_eq_bot_iff_nilpotencyClass_le]
  exact Finset.le_sup (f := fun i => Group.nilpotencyClass (Gs i)) (Finset.mem_univ i)

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

Goal state before:
pp: M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
a✝ : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock (⇑f ⁻¹' ⇑f '' B)

Tactic:
exact IsTrivialBlock.preimage hf.injective
          (isTrivialBlock_of_isBlock (hB.image f hφ hf.injective))

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
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype ↑(Set.range fun g ↦ g • B)
g : H
h : Set.range ⇑f ⊆ g • B
⊢ B = Set.univ

Tactic:
apply hB.eq_univ_of_card_lt

Goal state after:
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
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype ↑(Set.range fun g ↦ g • B)
g : H
h : Set.range ⇑f ⊆ g • B
⊢ Nat.card Y < B.ncard * 2
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.sum ≤ card (Fin 5)
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
h2,

Goal state after:
g : Perm (Fin 5)
ha : g ∈ alternatingGroup (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h : (Multiset.replicate g.cycleType.card 2).sum ≤ card (Fin 5)
⊢ IsConj (swap 0 4 * swap 1 3) g
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: g : Perm (Fin 5)
ha : (-1) ^ (g.cycleType.sum + g.cycleType.card) = 1
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g

Tactic:
h2,

Goal state after:
g : Perm (Fin 5)
ha : (-1) ^ ((Multiset.replicate g.cycleType.card 2).sum + (Multiset.replicate g.cycleType.card 2).card) = 1
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h✝ : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (swap 0 4 * swap 1 3) g
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

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

Tactic:
exact (h1 (card_cycleType_eq_zero.1 h_1)).elim

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

Goal state before:
pp: case neg
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
a b : α
h : ¬a = b
⊢ ∃ g, g • a = b

Tactic:
rw [is_two_pretransitive_iff] at h2

Goal state after:
case neg
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
a b : α
h : ¬a = b
⊢ ∃ g, g • a = b
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case neg
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B

Tactic:
rw [is_two_pretransitive_iff] at h2

Goal state after:
case neg
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case inr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
h : B.Nontrivial
⊢ IsTrivialBlock B

Tactic:
· right
    obtain ⟨a, ha, b, hb, h⟩ := h
    rw [← top_eq_univ, eq_top_iff]
    intro c _
    by_cases h' : a = c
    · rw [← h']; exact ha
    · rw [is_two_pretransitive_iff] at h2
      obtain ⟨g, hga, hgb⟩ := h2 h h'
      rw [MulAction.isBlock_iff_smul_eq_of_mem] at hB
      rw [← hB (g := g) ha (by rw [hga]; exact ha), ← hgb]
      exact smul_mem_smul_set hb

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

Goal state before:
pp: case succ
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
htcard : t.ncard = k
⊢ (fixingSubgroup (↥(stabilizer G a)) t).index * (Nat.card α - 1 - k)! = (Nat.card α - 1)!

Tactic:
convert! hrec (ofStabilizer.isMultiplyPretransitive.mp Hk) htcard

Goal state after:
case e'_2
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
htcard : t.ncard = k
⊢ Nat.card α - 1 = Nat.card ↥(ofStabilizer G a)

case e'_3
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
htcard : t.ncard = k
⊢ Nat.card α - 1 = Nat.card ↥(ofStabilizer G a)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
⊢ ⟨↑m, ⋯⟩ ∈ fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)

Tactic:
rintro ⟨⟨x, hx⟩, hx'⟩

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
x : α
hx : x ∈ ofFixingSubgroup M s
hx' : ⟨x, hx⟩ ∈ Subtype.val ⁻¹' t
⊢ ⟨↑m, ⋯⟩ • ↑⟨⟨x, hx⟩, hx'⟩ = ↑⟨⟨x, hx⟩, hx'⟩
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
hm : ↑m ∈ fixingSubgroup M s ∧ ↑m ∈ fixingSubgroup M t
⊢ ⟨↑m, ⋯⟩ ∈ fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)

Tactic:
rintro ⟨⟨x, hx⟩, hx'⟩

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
hm : ↑m ∈ fixingSubgroup M s ∧ ↑m ∈ fixingSubgroup M t
x : α
hx : x ∈ ofFixingSubgroup M s
hx' : ⟨x, hx⟩ ∈ Subtype.val ⁻¹' t
⊢ ⟨↑m, ⋯⟩ • ↑⟨⟨x, hx⟩, hx'⟩ = ↑⟨⟨x, hx⟩, hx'⟩
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case mpr.right
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := Subtype.val ⁻¹' s'
hst : s' = insert a (Subtype.val '' t)
⊢ t.encard + 1 + 1 = ↑n + 1

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, ← hs]

Goal state after:
case mpr.right
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := Subtype.val ⁻¹' s'
hst : s' = insert a (Subtype.val '' t)
⊢ t.encard + ↑1 + ↑1 = s.encard + 1
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ swap a b ∈ stabilizer (Perm α) s

Tactic:
suffices swap a b • s ⊆ s by
    rw [mem_stabilizer_iff]
    apply Set.Subset.antisymm this
    exact Set.subset_smul_set_iff.mpr this

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ swap a b • s ⊆ s
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
hG : stabilizer (↥G) s = ⊤
⊢ G = Subgroup.map G.subtype ⊤

Tactic:
rw [← MonoidHom.range_eq_map, Subgroup.range_subtype]

Goal state after:
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝¹ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this✝ : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
this : sᶜ ⊆ B
⊢ B = univ

Tactic:
apply hB.eq_univ_of_card_lt

Goal state after:
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝¹ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this✝ : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
this : sᶜ ⊆ B
⊢ Nat.card α < B.ncard * 2