mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by
      rintro ⟨⟨x, hx⟩, hx'⟩
      simp only [Set.mem_preimage] at hx'
      simp only [← SetLike.coe_eq_coe, SubMulAction.val_smul_of_tower]
      exact (mem_fixingSubgroup_union_iff.mp m.prop).2 ⟨x, hx'⟩

Goal state after:
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
⊢ k ∈ G

Tactic:
let x' := j.trans x

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 α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x
⊢ k ∈ G
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Equiv.Perm.sign g = 1
⊢ ∃ g, g • x = y

pp: case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Equiv.Perm.sign g = -1
⊢ ∃ g, g • x = y

Tactic:
· exact ⟨⟨g, h⟩, hg⟩

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Equiv.Perm.sign g = -1
⊢ ∃ g, g • x = y
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case right
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)

pp: case right.hφ
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
⊢ Function.Surjective ψ

pp: case right.hf
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
⊢ Function.Bijective ⇑g

Tactic:
· apply H.isPreprimitive_ofFixingSubgroup
      simp [← hs, t, hf.injective.injOn.encard_image]

Goal state after:
case right.hφ
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
⊢ Function.Surjective ψ

case right.hf
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
⊢ Function.Bijective ⇑g
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case pos.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
c : α
hct : c ∈ t
hc : ¬c = a ∧ c ∉ {b}
⊢ ⟨swap c a * swap a b, ⋯⟩ • a = b

Tactic:
simp only [Subgroup.mk_smul, Perm.smul_def, coe_mul]

Goal state after:
case pos.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
c : α
hct : c ∈ t
hc : ¬c = a ∧ c ∉ {b}
⊢ (⇑(swap c a) ∘ ⇑(swap a b)) a = b
Module: Mathlib.GroupTheory.GroupAction.Support

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Group H
inst✝⁵ : SMul G α
inst✝⁴ : SMul G β
inst✝³ : MulAction H α
inst✝² : SMul H β
inst✝¹ : SMulCommClass G H β
inst✝ : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
⊢ Supports G (g • s) (g • b)

Tactic:
by
  rintro g' hg'
  rw [smul_comm, h]
  rintro a ha
  have := Set.forall_mem_image.1 hg' ha
  rwa [smul_comm, smul_left_cancel_iff] at this

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

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
σ σ' : S.Section
g✝ g₁ g₂ : G
equiv : S.Equiv S'
g : G
⊢ S'.rightHom ((⇑equiv ∘ ⇑σ) g) = g

Tactic:
by
    rw [Function.comp_apply, equiv.rightHom_map, rightHom_section]

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

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this✝ : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support)ᶜ.ncard = n + 1
this : IsMultiplyPreprimitive (↥G) α (Nat.card α - 1)
⊢ IsMultiplyPretransitive (↥G) α (Nat.card α - 1)

Tactic:
apply IsMultiplyPreprimitive.isMultiplyPretransitive

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

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
⊢ Nat.factorial 3 = 2 * 3

Tactic:
simp [Nat.factorial]

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

Goal state before:
pp: case inr.inl
α✝ : Type u_2
n : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * 1 ≤ Nat.card α
hn0 : 1 ≠ 0
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 1

pp: case inr.inr
α✝ : Type u_2
n✝ : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n

Tactic:
· rw [is_one_pretransitive_iff]
    exact alternatingGroup.isPretransitive_of_three_le_card α hα

Goal state after:
case inr.inr
α✝ : Type u_2
n✝ : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
⊢ w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)

Tactic:
intro hw

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
hw : w.head ∈ toSubgroup A B u
⊢ ∀ (x : G), ¬w.toList.head? = some (-u, x)
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ ∃ o, map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o

Tactic:
use l.map (List.map (Fintype.equivFin α).symm)

Goal state after:
case h
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ map length (map (map ⇑(Fintype.equivFin α).symm) l) = c ∧
    (∀ s ∈ map (map ⇑(Fintype.equivFin α).symm) l, s.Nodup) ∧ Pairwise Disjoint (map (map ⇑(Fintype.equivFin α).symm) l)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nonempty g.Basis

Tactic:
have (c : g.cycleFactorsFinset) : c.val.support.Nonempty :=
    IsCycle.nonempty_support (mem_cycleFactorsFinset_iff.mp c.prop).1
  exact ⟨fun c ↦ (this c).choose, fun c ↦ (this c).choose_spec⟩

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

Goal state before:
pp: case refine_3
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
⊢ Equiv.swap y y ∈ closure S

Tactic:
Equiv.swap_self

Goal state after:
case refine_3
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
⊢ Equiv.refl α ∈ closure S
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ Function.fixedPoints ⇑g
this : ∀ (d : ↥g.cycleFactorsFinset), x ∉ (↑d).support
⊢ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
simp only [this]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ a.ofPermHomFun 1 x = x

Tactic:
rw [ofPermHomFun_apply_of_cycleOf_mem a _ hc hm, OneMemClass.coe_one, coe_one, id_eq, hm]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
x : α
h : x = f x
⊢ Equiv.swap x x ∈ closure fun x ↦ ∃ x_1 y, x_1 ≠ y ∧ x = Equiv.swap x_1 y

Tactic:
Equiv.swap_self

Goal state after:
case pos
α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
x : α
h : x = f x
⊢ Equiv.refl α ∈ closure fun x ↦ ∃ x_1 y, x_1 ≠ y ∧ x = Equiv.swap x_1 y
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ (∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1) ↔ ∀ (g : G), g ≠ 1 → ∃ H, g ∉ H

Tactic:
← not_forall,

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ (∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1) ↔
    ∀ (g : G), g ≠ 1 → ¬∀ (x : FiniteIndexNormalSubgroup G), g ∈ x
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ (∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1) ↔ ∀ (g : G), g ≠ 1 → ∃ H, ¬(H.FiniteIndex → g ∈ H)

Tactic:
← not_forall,

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ (∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1) ↔
    ∀ (g : G), g ≠ 1 → ¬∀ (x : Subgroup G), x.FiniteIndex → g ∈ x
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
⊢ empty.prod = 1

Tactic:
by
  simp [prod, empty]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
x : ↥g.cycleFactorsFinset
⊢ #(↑(τ x)).support = #(↑x).support

Tactic:
by
    by_cases hx : x = ⟨c, hc⟩
    · rw [hx, Equiv.swap_apply_left]; exact hm.symm
    by_cases hx' : x = ⟨d, hd⟩
    · rw [hx', Equiv.swap_apply_right]; exact hm
    · rw [Equiv.swap_apply_of_ne_of_ne hx hx']

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case refine_1.right
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
⊢ ⟨i, (φ i) h * if h : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1⟩ ∈
      w.toList.tail ∨
    w.toList.head? =
        some ⟨i, if h : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1⟩ ∨
      ¬w.fstIdx = some i ∧
        (if h : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1) = 1

Tactic:
split_ifs with hep

Goal state after:
case pos
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
hep : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = i
⊢ ⟨i, (φ i) h * ⋯ ▸ (w.toList.head ⋯).snd⟩ ∈ w.toList.tail ∨
    w.toList.head? = some ⟨i, ⋯ ▸ (w.toList.head ⋯).snd⟩ ∨ ¬w.fstIdx = some i ∧ ⋯ ▸ (w.toList.head ⋯).snd = 1

case neg
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
hep : ¬∃ (h : ¬w.toList = []), (w.toList.head h).fst = i
⊢ ⟨i, (φ i) h * 1⟩ ∈ w.toList.tail ∨ w.toList.head? = some ⟨i, 1⟩ ∨ ¬w.fstIdx = some i ∧ 1 = 1
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
this : 12 = 2 ^ 2 * 3
⊢ 2 ^ ((2 • Nat.factorization 2) 2 + (Nat.factorization 3) 2) = 4

Tactic:
Finsupp.coe_smul,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
this : 12 = 2 ^ 2 * 3
⊢ 2 ^ ((2 • ⇑(Nat.factorization 2)) 2 + (Nat.factorization 3) 2) = 4
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
⊢ (kleinFour α).Normal

Tactic:
have _ := characteristic_kleinFour hα4
  apply Subgroup.normal_of_characteristic

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

Goal state before:
pp: case a
n : ℕ
i : ZMod (2 * n)
⊢ (a i).inv * a i = 1

pp: case xa
n : ℕ
i : ZMod (2 * n)
⊢ (xa i).inv * xa i = 1

Tactic:
· exact congr_arg a (neg_add_cancel i)

Goal state after:
case xa
n : ℕ
i : ZMod (2 * n)
⊢ (xa i).inv * xa i = 1
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inl
n : ℕ
h : 0 < n
⊢ a 1 ^ n ≠ a 0

Tactic:
a_one_pow

Goal state after:
case inl
n : ℕ
h : 0 < n
⊢ a ↑n ≠ a 0
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a 1 ^ orderOf (a 1) = 1
⊢ False

Tactic:
a_one_pow

Goal state after:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a ↑(orderOf (a 1)) = 1
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_2
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : Finite G
P : Sylow p G
inst✝¹ : IsCyclic ↥↑P
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : ⁅K, ↑P⁆ = ↑P
⊢ ↑P ≤ commutator G

Tactic:
rw [← h, commutator_def]

Goal state after:
case refine_2
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : Finite G
P : Sylow p G
inst✝¹ : IsCyclic ↥↑P
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : ⁅K, ↑P⁆ = ↑P
⊢ ⁅K, ↑P⁆ ≤ ⁅⊤, ⊤⁆
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
h : ∀ (p : ℕ), Nat.Prime p → ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index
⊢ (Nat.card ↥(commutator G)).Coprime (commutator G).index

Tactic:
by
    contrapose! h
    exact Nat.Prime.not_coprime_iff_dvd.mp h

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((copy β ∘ₖ κ) a) (s ×ˢ t) = (κ a) (s ∩ t)

Tactic:
rw [comp_apply' _ _ _ <| hs.prod ht]
  simp_rw [copy_apply, Measure.dirac_apply' _ <| hs.prod ht, Set.indicator_prod_one]
  calc
  _ = ∫⁻ b, (s ∩ t).indicator 1 b ∂κ a := by
    congr with b
    simp [Set.inter_indicator_one]
  _ = κ a (s ∩ t) := lintegral_indicator_one <| hs.inter ht

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
t₁ : Set α
t₂ : Set β
⊢ MeasurableSet t₁ →
    MeasurableSet t₂ →
      ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
intro ht₁

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
⊢ MeasurableSet t₂ →
    ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
      ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
⊢ ∫⁻ (a_1 : β), ‖((η (a, a_1)) (Prod.mk a_1 ⁻¹' s)).toReal‖ₑ ∂κ a < ∞

Tactic:
enorm_eq_ofReal toReal_nonneg

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
⊢ ∫⁻ (a_1 : β), ENNReal.ofReal ((η (a, a_1)) (Prod.mk a_1 ⁻¹' s)).toReal ∂κ a < ∞
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : μ Set.univ = ∞
⊢ ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) • μ = (μ Set.univ)⁻¹ • μ

pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ∞
⊢ ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) • μ = (μ Set.univ)⁻¹ • μ

Tactic:
· simp only [measureReal_def, h_univ, ENNReal.toReal_top, zero_mul, div_zero,
      ENNReal.ofReal_zero, zero_smul, ENNReal.inv_top]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h0 : NeZero μ
h_univ : ¬μ Set.univ = ∞
⊢ ENNReal.ofReal (rexp c / (μ.real Set.univ * rexp c)) • μ = (μ Set.univ)⁻¹ • μ
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → ℝ
hg : Integrable (fun x ↦ rexp (g x)) μ
⊢ μ.tilted (g + f) = (μ.tilted g).tilted f

Tactic:
tilted_tilted hg

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → ℝ
hg : Integrable (fun x ↦ rexp (g x)) μ
⊢ μ.tilted (g + f) = μ.tilted (g + f)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim

Goal state before:
pp: α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : AEStronglyMeasurable f (μ.trim hm)
⊢ eLpNorm (AEStronglyMeasurable.mk f hf) p (μ.trim hm) = eLpNorm (AEStronglyMeasurable.mk f hf) p μ

Tactic:
exact eLpNorm_trim hm hf.stronglyMeasurable_mk

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
h_contra : μ ≪ c • ν
⊢ μ ≪ c⁻¹ • c • ν

Tactic:
exact h_contra.smul_right (by simpa)

Goal state after: