mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Descent

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

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

Tactic:
· obtain ⟨u', hu₁, rfl⟩ := mem_map.mp hu
    exact U.pow_mem hu₁ n

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
f : G →* G := powMonoidHom n
q : G → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
H₁' : s * ↑f.range = Set.univ
c' : ℝ := max c₀ (c g)
H₃' : ∀ (x : G), b * h x - c' ≤ h (f x)
g' : G
hg' : g' ∈ s
x : G
⊢ h x ≤ a * h (g' * x) + c'
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
⊢ List.map (fun x ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = List.map id (cs.rightInvSeq ω.reverse)

Tactic:
by
        apply List.map_congr_left
        intro t ht
        exact (cs.isReflection_of_mem_rightInvSeq _ ht).inv

Goal state after:
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
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
⊢ (cs.rightInvSeq ω).getD j' 1 * (cs.rightInvSeq ω).getD j' 1 = 1

Tactic:
exact cs.getD_rightInvSeq_mul_self _ _

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
m m' : M
s s' : ℕ+
⊢ LocalizedModule.mk m (↑ⁿ s) = LocalizedModule.mk m' (↑ⁿ s') ↔ ∃ u, ↑u • ↑s' • m = ↑u • ↑s • m'

Tactic:
LocalizedModule.mk_eq,

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
m m' : M
s s' : ℕ+
⊢ (∃ u, u • ↑ⁿ s' • m = u • ↑ⁿ s • m') ↔ ∃ u, ↑u • ↑s' • m = ↑u • ↑s • m'
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
infer_instance

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
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
a : G
ha : a ≠ 1
⊢ ∃ φ, φ a ≠ 1

Tactic:
refine exists_apply_ne_one_aux G Mˣ (fun n hn a ha₀ ↦ ?_) ha
  have : NeZero n := ⟨fun H ↦ NeZero.ne _ <| Nat.eq_zero_of_zero_dvd (H ▸ hn)⟩
  have := HasEnoughRootsOfUnity.of_dvd M hn
  exact ZMod.exists_monoidHom_apply_ne_one (HasEnoughRootsOfUnity.exists_primitiveRoot M n) ha₀

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: case refine_1
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
x✝¹ x✝ : G
h :
  (fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }) x✝¹ =
    (fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }) x✝
⊢ x✝¹ = x✝

pp: case refine_2
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
⊢ Nat.card G = Nat.card ((G →* Mˣ) →* Mˣ)

Tactic:
· rwa [mk.injEq, OneHom.mk.injEq, funext_iff, forall_apply_eq_apply_iff] at h

Goal state after:
case refine_2
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
⊢ Nat.card G = Nat.card ((G →* Mˣ) →* Mˣ)
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
iso : G ≃* H
h : IsFinitelyPresented G
⊢ IsFinitelyPresented H

Tactic:
by
  obtain ⟨n, φ, hφsurj, hNC⟩ := h
  refine ⟨n, (iso : G →* H).comp φ, iso.surjective.comp hφsurj, ?_⟩
  rwa [φ.ker_mulEquiv_comp iso]

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg.inr
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime ((Nat.card G).minFac ^ (k - 1) * ((Nat.card G).minFac - 1))

Tactic:
refine (Nat.Coprime.pow_right _ ?_).mul_right ?_

Goal state after:
case neg.inr.refine_1
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime (Nat.card G).minFac

case neg.inr.refine_2
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime ((Nat.card G).minFac - 1)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : n ≤ m
⊢ ⁅x, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)

Tactic:
rw [tsub_eq_zero_of_le hm, h0, Subgroup.mem_bot] at hx

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x = 1
g : G
hm : n ≤ m
⊢ ⁅x, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_3.h_obj
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 : ActionCategory G A), E.obj X_1 = (uncurry F' ⋯).obj X_1

Tactic:
intro

Goal state after:
case refine_3.h_obj
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'
X✝ : ActionCategory G A
⊢ E.obj X✝ = (uncurry F' ⋯).obj X✝
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Characteristic
d : ℕ
a✝ : (S.lowerCentralSeries d).Characteristic
⊢ ⁅S.lowerCentralSeries d, S⁆.Characteristic

Tactic:
infer_instance

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ nilpotencyClass G ≤ n

Tactic:
nilpotencyClass_def

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ Nat.find ⋯ ≤ n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ = nilpotencyClass G

Tactic:
nilpotencyClass_def

Goal state after:
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ = Nat.find ⋯
Module: Mathlib.GroupTheory.Generators

Goal state before:
pp: G : Type u_1
H : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Group G
inst✝ : Group H
P✝ P : Generators G ι
e : ι' ≃ ι
⊢ Subgroup.closure (P.val '' Set.range ⇑e) = ⊤

Tactic:
EquivLike.range_eq_univ,

Goal state after:
G : Type u_1
H : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Group G
inst✝ : Group H
P✝ P : Generators G ι
e : ι' ≃ ι
⊢ Subgroup.closure (P.val '' Set.univ) = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Normal
n : ℕ
a✝ : (S.lowerCentralSeries n).Normal
⊢ ⁅S.lowerCentralSeries n, S⁆.Normal

Tactic:
infer_instance

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
this : IsNilpotent G'
⊢ Nat.find ⋯ ≤ nilpotencyClass G

Tactic:
nilpotencyClass_def

Goal state after:
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
this : IsNilpotent G'
⊢ Nat.find ⋯ ≤ Nat.find ⋯
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G✝ : Type u_1
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
ab : a < b
⊢ upperCentralSeries G (a + 1) ≤ upperCentralSeries G a

Tactic:
· rw [hn]
    exact upperCentralSeries_mono _ (by grind)

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
⊢ ∀ (a : X), ∃ x ∈ range fun x ↦ orbit G x, a ∈ x

Tactic:
intro x
    exact ⟨_, ⟨x, rfl⟩, mem_orbit_self x⟩

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case hbase
G : Type u_1
inst✝² : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
α✝ : Type u_1
inst✝¹ : Finite α✝
inst✝ : Subsingleton α✝
hG : Group α✝
h : IsPGroup p α✝
⊢ Group.IsNilpotent α✝

Tactic:
infer_instance

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
hg' : g₁ • B ≠ g₂ • B
⊢ B = ∅

Tactic:
simpa using (hB hg').eq_bot_of_le hg

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

Goal state before:
pp: case f
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
⊢ ⟨h, hH⟩ • B = B → g • h • B = g • B

Tactic:
intro

Goal state after:
case f
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
a✝ : ⟨h, hH⟩ • B = B
⊢ g • h • B = g • B
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H = ⊤
⊢ ⊤.Normal

Tactic:
infer_instance

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nat.card α ≤ 3
h✝ : Subsingleton α
⊢ IsCyclic ↥(alternatingGroup α)

Tactic:
infer_instance

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
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
a : α
ha : a ∉ fixedPoints (↥N) α
h : (orbit (↥N) a).Subsingleton
n : ↥N
b : α
⊢ b ∈ orbit (↥N) a ↔ b ∈ {a}

Tactic:
rw [Set.Subsingleton.eq_singleton_of_mem h (MulAction.mem_orbit_self a)]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ map (alternatingGroup α).subtype (closure {g | (↑g).IsThreeCycle}) = map (alternatingGroup α).subtype ⊤

Tactic:
MonoidHom.map_closure

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ closure (⇑(alternatingGroup α).subtype '' {g | (↑g).IsThreeCycle}) = map (alternatingGroup α).subtype ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

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

Tactic:
MonoidHom.map_closure

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ closure (⇑(alternatingGroup α).subtype '' {g | (↑g).cycleType = {2, 2}}) = map (alternatingGroup α).subtype ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ center ↥(alternatingGroup α)
a : α
ha : a ∈ g.support
hab : g a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ g a
hd : d ≠ a ∧ d ≠ g a
k : Perm α := swap (g a) d * swap (g a) c
hka : k • a = a
hkga : k • g a = c
this : k • ⟨g, hg⟩ • a ≠ c
⊢ False

Tactic:
by
    apply this; simp [← hkga]

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✝
B : Type u_4
inst✝¹⁰ : TopologicalSpace B
F : Type u_5
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
E : B → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (b : B) → TopologicalSpace (E b)
inst✝⁵ : (b : B) → AddCommGroup (E b)
inst✝⁴ : (b : B) → Module ℝ (E b)
inst✝³ : ∀ (b : B), IsTopologicalAddGroup (E b)
inst✝² : ∀ (b : B), ContinuousConstSMul ℝ (E b)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
g : ContinuousRiemannianMetric F E
b : B
e : E b ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E b) b ⋯
m : (E b →L[ℝ] E b →L[ℝ] ℝ) ≃L[ℝ] F →L[ℝ] F →L[ℝ] ℝ := e.arrowCongr (e.arrowCongr (ContinuousLinearEquiv.refl ℝ ℝ))
v : E b
⊢ ((g.inner b) v) v = ((fun w ↦ ((m (g.inner b)) w) w) ∘ ⇑e) v

Tactic:
simp [m]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
⊢ IsMultiplyPretransitive G α n

Tactic:
infer_instance

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ : Set α
a : α
s : Set ↥(ofStabilizer M a)
x : ↥(ofFixingSubgroup M (insert a (Subtype.val '' s)))
⊢ ↥(ofFixingSubgroup (↥(stabilizer M a)) s)

Tactic:
choose hx hx' using (mem_ofFixingSubgroup_insert_iff.mp x.prop)
    exact ⟨_, hx'⟩

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : Function.Surjective toPerm
φ : ↥(stabilizer M s) → Perm ↑s := toPerm
⊢ IsPreprimitive ↥(stabilizer M s) ↑s

Tactic:
let f : s →ₑ[φ] s := {
    toFun := id
    map_smul' _ _ := rfl }

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : Function.Surjective toPerm
φ : ↥(stabilizer M s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
⊢ IsPreprimitive ↥(stabilizer M 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 α
hs : Function.Surjective toPerm
φ : ↥(stabilizer M s) → Perm ↑s := toPerm
f : ↑s →ₑ[φ] ↑s := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ IsPreprimitive (Perm ↑s) ↑s

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_2
s : Set α
g : Perm ↑s
⊢ ∃ a, toPerm a = g

Tactic:
use! Perm.ofSubtype g

Goal state after:
case property
α : Type u_2
s : Set α
g : Perm ↑s
⊢ ofSubtype g ∈ stabilizer (Perm α) s

case h
α : Type u_2
s : Set α
g : Perm ↑s
⊢ toPerm ⟨ofSubtype g, ?property⟩ = g
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : 2 < s.ncard
⊢ ∃ g ∈ stabilizer (Perm α) s, g.IsThreeCycle

Tactic:
rw [two_lt_ncard_iff] at hs

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ ∃ g ∈ stabilizer (Perm α) s, g.IsThreeCycle
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Nat.card α
hs : 2 ≥ s.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
⊢ ∃ g ∈ stabilizer (Perm α) s, g.IsThreeCycle

Tactic:
← stabilizer_compl

Goal state after:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Nat.card α
hs : 2 ≥ s.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
⊢ ∃ g ∈ stabilizer (Perm α) sᶜ, g.IsThreeCycle
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
x : α
hx : x ∈ s
⊢ x ∉ k.support

Tactic:
exact (Set.disjoint_left.mp hk_support) hx

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s B : Set α
G : Subgroup M
inst✝ : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
hB : IsBlock (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s

Tactic:
infer_instance

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

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝ : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
h : sᶜ.ncard < s.ncard
⊢ IsCoatom (stabilizer (Perm α) s)

Tactic:
← stabilizer_compl

Goal state after:
case inr.inr
α : Type u_2
inst✝ : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
h : sᶜ.ncard < s.ncard
⊢ IsCoatom (stabilizer (Perm α) sᶜ)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
this :
  ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
    s.Nonempty →
      sᶜ.Nonempty → ¬sᶜ.ncard = s.ncard → s.ncard < sᶜ.ncard → IsCoatom (stabilizer (↥(alternatingGroup α)) s)
hs' : ¬s.ncard < sᶜ.ncard
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

Tactic:
← stabilizer_compl

Goal state after:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
this :
  ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
    s.Nonempty →
      sᶜ.Nonempty → ¬sᶜ.ncard = s.ncard → s.ncard < sᶜ.ncard → IsCoatom (stabilizer (↥(alternatingGroup α)) s)
hs' : ¬s.ncard < sᶜ.ncard
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) sᶜ)
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
s : S.Splitting
⊢ S.rightHom.comp ↑s = MonoidHom.id G

Tactic:
by
  ext g
  simp only [MonoidHom.comp_apply, MonoidHom.id_apply, MonoidHom.coe_coe, rightHom_splitting]

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

Goal state before:
pp: α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝¹ : Finite α
this✝ : Fintype α
h2 : IsMultiplyPretransitive K α 2
hn : ¬n ≤ 2
this : IsEmpty (Fin n ↪ α)
⊢ IsMultiplyPretransitive K α n

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
⊢ IsPreprimitive (Perm α) ↑(powersetCard α n)

Tactic:
have : Finite α := Nat.finite_of_card_ne_zero (Nat.ne_zero_of_lt hn)
  have : Fintype α := Fintype.ofFinite α
  -- The action is pretransitive.
  have : IsPretransitive (Perm α) (powersetCard α n) := powersetCard.isPretransitive
  -- The type on which the group acts is nontrivial.
  have : Nontrivial (powersetCard α n) := powersetCard.nontrivial' h_one_le hn
  obtain ⟨s⟩ := this.to_nonempty
  -- It remains to prove that stabilizer of some point is maximal.
  rw [← isCoatom_stabilizer_iff_preprimitive _ s]
  -- The stabilizer of a combination is the stabilizer of the underlying set.
  rw [stabilizer_coe]
  -- We conclude by `Equiv.Perm.isCoatom_stabilizer`
  apply isCoatom_stabilizer
  -- `s` is nonempty because `n ≠ 0`.
  · rwa [powersetCard.coe_nonempty_iff]
  -- `sᶜ` is nonempty because `n < Nat.card α`.
  · rw [nonempty_compl, ne_eq, eq_univ_iff_ncard, ncard_eq]
    exact hn.ne
  -- `Nat.card α ≠ 2 * s.ncard` because `Nat.card α ≠ 2 * s`.
  · rwa [ncard_eq]

Goal state after: