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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive (HNNExtension.of g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := Set.ofPred motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
f : HNNExtension G A B φ →* ↥S := lift (HNNExtension.of.codRestrict S of) ⟨HNNExtension.t, t⟩ ⋯
x✝ : G
⊢ ((S.subtype.comp f).comp HNNExtension.of) x✝ = ((MonoidHom.id (HNNExtension G A B φ)).comp HNNExtension.of) x✝

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive (HNNExtension.of g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := Set.ofPred motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
f : HNNExtension G A B φ →* ↥S := lift (HNNExtension.of.codRestrict S of) ⟨HNNExtension.t, t⟩ ⋯
x✝ : G
⊢ ((S.subtype.comp f).comp HNNExtension.of) x✝ = ((MonoidHom.id (HNNExtension G A B φ)).comp HNNExtension.of) x✝
Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst✝¹ : (i : ι) → CommMonoid (M i)
inst✝ : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
z : (i : ι) → N i
⊢ ∃ x, z * Pi.map f ↑x.2 = Pi.map f x.1

Tactic:
choose x hx using fun i ↦ (hf i).surj

Goal state after:
ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst✝¹ : (i : ι) → CommMonoid (M i)
inst✝ : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
z : (i : ι) → N i
x : (i : ι) → N i → M i × ↥(S i)
hx : ∀ (i : ι) (z : N i), z * f i ↑(x i z).2 = f i (x i z).1
⊢ ∃ x, z * Pi.map f ↑x.2 = Pi.map f x.1
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
w' : NormalWord d
head✝ : G
toList✝ : List (ℤˣ × G)
chain✝ : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) toList✝
mem_set✝ : ∀ (u : ℤˣ) (g : G), (u, g) ∈ { head := head✝, toList := toList✝, chain := chain✝ }.toList → g ∈ d.set u
h1 : { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ }.head = w'.head
h2 : { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ }.toList = w'.toList
⊢ { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ } = w'

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
w' : NormalWord d
head✝ : G
toList✝ : List (ℤˣ × G)
chain✝ : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) toList✝
mem_set✝ : ∀ (u : ℤˣ) (g : G), (u, g) ∈ { head := head✝, toList := toList✝, chain := chain✝ }.toList → g ∈ d.set u
h1 : { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ }.head = w'.head
h2 : { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ }.toList = w'.toList
⊢ { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ } = w'
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case mk
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
head✝ : G
toList✝ : List (ℤˣ × G)
chain✝ : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) toList✝
mem_set✝¹ : ∀ (u : ℤˣ) (g : G), (u, g) ∈ { head := head✝, toList := toList✝, chain := chain✝ }.toList → g ∈ d.set u
toReducedWord✝ : ReducedWord G A B
mem_set✝ : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toReducedWord✝.toList → g ∈ d.set u
h1 :
  { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝¹ }.head =
    { toReducedWord := toReducedWord✝, mem_set := mem_set✝ }.head
h2 :
  { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝¹ }.toList =
    { toReducedWord := toReducedWord✝, mem_set := mem_set✝ }.toList
⊢ { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝¹ } =
    { toReducedWord := toReducedWord✝, mem_set := mem_set✝ }

Tactic:
;

Goal state after:
case mk
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
head✝ : G
toList✝ : List (ℤˣ × G)
chain✝ : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) toList✝
mem_set✝¹ : ∀ (u : ℤˣ) (g : G), (u, g) ∈ { head := head✝, toList := toList✝, chain := chain✝ }.toList → g ∈ d.set u
toReducedWord✝ : ReducedWord G A B
mem_set✝ : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toReducedWord✝.toList → g ∈ d.set u
h1 :
  { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝¹ }.head =
    { toReducedWord := toReducedWord✝, mem_set := mem_set✝ }.head
h2 :
  { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝¹ }.toList =
    { toReducedWord := toReducedWord✝, mem_set := mem_set✝ }.toList
⊢ { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝¹ } =
    { toReducedWord := toReducedWord✝, mem_set := mem_set✝ }
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
u : ℤˣ
w : NormalWord d
⊢ (g : G) → g ∈ toSubgroup A B u ∧ none = some (-u) → NormalWord d

Tactic:
;

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
u : ℤˣ
w : NormalWord d
⊢ (g : G) → g ∈ toSubgroup A B u ∧ none = some (-u) → NormalWord d
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
⊢ ↑c₂ * a₁ ≤ ↑a₂ * c₁ ↔ ↑d₂ * b₁ ≤ ↑b₂ * d₁

Tactic:
obtain ⟨e, he⟩ := r_iff_exists.1 hab
        obtain ⟨f, hf⟩ := r_iff_exists.1 hcd
        simp only [mul_right_inj] at he hf
        rw [← mul_le_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_le_mul_iff_right, ← mul_le_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_le_mul_iff_left]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case inr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ (m₂, s₂).1
this : f m ∣ n₂
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
;

Goal state after:
case inr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ (m₂, s₂).1
this : f m ∣ n₂
⊢ f m ∣ n₁ ∨ f m ∣ n₂
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (Perm α)ᵈᵐᵃ
⊢ g • f = f ↔ f ∘ ⇑(mk.symm g) = f

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
f : α → ι
g : (Perm α)ᵈᵐᵃ
⊢ g • f = f ↔ f ∘ ⇑(mk.symm g) = f
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
⊢ stabilizerEquiv_invFun g a = ↑((g (f a)) ⟨a, ⋯⟩)

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
⊢ stabilizerEquiv_invFun g a = ↑((g (f a)) ⟨a, ⋯⟩)
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
i : ι
a : { x // f x = i }
⊢ ↑(((fun g i ↦ (mk.symm ↑(MulOpposite.unop g)).subtypePerm ⋯)
          ((fun g ↦ { unop' := ⟨mk (stabilizerEquiv_invFun_aux g), ⋯⟩ }) g) i)
        a) =
    ↑((g i) a)

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
i : ι
a : { x // f x = i }
⊢ ↑(((fun g i ↦ (mk.symm ↑(MulOpposite.unop g)).subtypePerm ⋯)
          ((fun g ↦ { unop' := ⟨mk (stabilizerEquiv_invFun_aux g), ⋯⟩ }) g) i)
        a) =
    ↑((g i) a)
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case e'_7
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
w : NormalWord d
⊢ 1 = - -1

Tactic:
;

Goal state after:
case e'_7
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
w : NormalWord d
⊢ 1 = - -1
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos.cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
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'
this : Cancels 1 (↑g • cons g✝ u✝ w✝ h1✝ h2✝) ↔ Cancels 1 (cons g✝ u✝ w✝ h1✝ h2✝)
hcan : Cancels 1 (cons g✝ u✝ w✝ h1✝ h2✝)
a✝ :
  cons g✝ u✝ w✝ h1✝ h2✝ = w✝ →
    consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (↑g • cons g✝ u✝ w✝ h1✝ h2✝)
        (fun g_1 a ↦ ↑g • cons g✝ u✝ w✝ h1✝ h2✝) (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) ⋯ =
      ↑(φ g) •
        consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (cons g✝ u✝ w✝ h1✝ h2✝)
          (fun g a ↦ cons g✝ u✝ w✝ h1✝ h2✝) (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) hcan
⊢ ↑(φ ⟨↑g * g✝, ⋯⟩) • w✝ = ↑(φ g) • ↑(φ ⟨g✝, ⋯⟩) • w✝

Tactic:
← mul_smul,

Goal state after:
case pos.cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
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'
this : Cancels 1 (↑g • cons g✝ u✝ w✝ h1✝ h2✝) ↔ Cancels 1 (cons g✝ u✝ w✝ h1✝ h2✝)
hcan : Cancels 1 (cons g✝ u✝ w✝ h1✝ h2✝)
a✝ :
  cons g✝ u✝ w✝ h1✝ h2✝ = w✝ →
    consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (↑g • cons g✝ u✝ w✝ h1✝ h2✝)
        (fun g_1 a ↦ ↑g • cons g✝ u✝ w✝ h1✝ h2✝) (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) ⋯ =
      ↑(φ g) •
        consRecOn (motive := fun x ↦ Cancels 1 x → NormalWord d) (cons g✝ u✝ w✝ h1✝ h2✝)
          (fun g a ↦ cons g✝ u✝ w✝ h1✝ h2✝) (fun g x w x_1 x_2 x_3 can ↦ ↑(φ ⟨g, ⋯⟩) • w) hcan
⊢ ↑(φ ⟨↑g * g✝, ⋯⟩) • w✝ = (↑(φ g) * ↑(φ ⟨g✝, ⋯⟩)) • w✝
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.map ((Finset.card ∘ support) ∘ fun l ↦ l.formPerm) p = m.toList

Tactic:
;

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.map ((Finset.card ∘ support) ∘ fun l ↦ l.formPerm) p = m.toList
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ ((Finset.card ∘ support) ∘ fun l ↦ l.formPerm) x = x.length

Tactic:
;

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ ((Finset.card ∘ support) ∘ fun l ↦ l.formPerm) x = x.length
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ ReducedWord.prod φ (cons g u w h1 h2).toReducedWord • empty = cons g u w h1 h2

Tactic:
prod_cons,

Goal state after:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
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'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (of g * (t ^ ↑u * ReducedWord.prod φ w.toReducedWord)) • empty = cons g u w h1 h2
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Perm α
a' : g.Basis
toFun✝ : ↥g.cycleFactorsFinset → α
mem_support_self'✝ : ∀ (c : ↥g.cycleFactorsFinset), toFun✝ c ∈ (↑c).support
x✝ : (fun a ↦ a.toFun) { toFun := toFun✝, mem_support_self' := mem_support_self'✝ } = (fun a ↦ a.toFun) a'
⊢ { toFun := toFun✝, mem_support_self' := mem_support_self'✝ } = a'

Tactic:
;

Goal state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Perm α
a' : g.Basis
toFun✝ : ↥g.cycleFactorsFinset → α
mem_support_self'✝ : ∀ (c : ↥g.cycleFactorsFinset), toFun✝ c ∈ (↑c).support
x✝ : (fun a ↦ a.toFun) { toFun := toFun✝, mem_support_self' := mem_support_self'✝ } = (fun a ↦ a.toFun) a'
⊢ { toFun := toFun✝, mem_support_self' := mem_support_self'✝ } = a'
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Perm α
toFun✝¹ : ↥g.cycleFactorsFinset → α
mem_support_self'✝¹ : ∀ (c : ↥g.cycleFactorsFinset), toFun✝¹ c ∈ (↑c).support
toFun✝ : ↥g.cycleFactorsFinset → α
mem_support_self'✝ : ∀ (c : ↥g.cycleFactorsFinset), toFun✝ c ∈ (↑c).support
x✝ :
  (fun a ↦ a.toFun) { toFun := toFun✝¹, mem_support_self' := mem_support_self'✝¹ } =
    (fun a ↦ a.toFun) { toFun := toFun✝, mem_support_self' := mem_support_self'✝ }
⊢ { toFun := toFun✝¹, mem_support_self' := mem_support_self'✝¹ } =
    { toFun := toFun✝, mem_support_self' := mem_support_self'✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Perm α
toFun✝¹ : ↥g.cycleFactorsFinset → α
mem_support_self'✝¹ : ∀ (c : ↥g.cycleFactorsFinset), toFun✝¹ c ∈ (↑c).support
toFun✝ : ↥g.cycleFactorsFinset → α
mem_support_self'✝ : ∀ (c : ↥g.cycleFactorsFinset), toFun✝ c ∈ (↑c).support
x✝ :
  (fun a ↦ a.toFun) { toFun := toFun✝¹, mem_support_self' := mem_support_self'✝¹ } =
    (fun a ↦ a.toFun) { toFun := toFun✝, mem_support_self' := mem_support_self'✝ }
⊢ { toFun := toFun✝¹, mem_support_self' := mem_support_self'✝¹ } =
    { toFun := toFun✝, mem_support_self' := mem_support_self'✝ }
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
g : G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l
hw1 : g = 1
⊢ ∃ w',
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := g, toList := l, chain := chain } ∧
      List.map Prod.fst w'.toList = List.map Prod.fst { head := g, toList := l, chain := chain }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := g, toList := l, chain := chain }.toList.head?, w'.head ∈ toSubgroup A B (-u)

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
g : G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l
hw1 : g = 1
⊢ ∃ w',
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := g, toList := l, chain := chain } ∧
      List.map Prod.fst w'.toList = List.map Prod.fst { head := g, toList := l, chain := chain }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := g, toList := l, chain := chain }.toList.head?, w'.head ∈ toSubgroup A B (-u)
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_1
α : 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
x y : α
hf : Equiv.swap x y ∈ S
⊢ (Equiv.swap x y)⁻¹ ∈ S

Tactic:
;

Goal state after:
case refine_1
α : 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
x y : α
hf : Equiv.swap x y ∈ S
⊢ (Equiv.swap x y)⁻¹ ∈ S
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.refl α ∈ closure S

Tactic:
;

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.ClosureSwap

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp : Set α
fin : supp.Finite
supp_eq : supp = (fixedBy α f)ᶜ
⊢ (fixedBy α f)ᶜ ⊆ supp → f ∈ closure S

Tactic:
;

Goal state after:
case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp : Set α
fin : supp.Finite
supp_eq : supp = (fixedBy α f)ᶜ
⊢ (fixedBy α f)ᶜ ⊆ supp → f ∈ closure S
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp : Set α
fin : supp.Finite
⊢ (fixedBy α f)ᶜ ⊆ supp → f ∈ closure S

Tactic:
;

Goal state after:
case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp : Set α
fin : supp.Finite
⊢ (fixedBy α f)ᶜ ⊆ supp → f ∈ closure S
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
⊢ f ∈ closure S

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
⊢ f ∈ closure S
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
⊢ f = 1

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
⊢ f = 1
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
x✝ : α
⊢ f x✝ = 1 x✝

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
x✝ : α
⊢ f x✝ = 1 x✝
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
x✝ : α
h : ¬f x✝ = 1 x✝
⊢ False

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
x✝ : α
h : ¬f x✝ = 1 x✝
⊢ False
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
⊢ (if f b = f a then a else if f b = a then f a else f b) ∈ orbit (↥(closure S)) b

Tactic:
;

Goal state after:
case refine_1
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
⊢ (if f b = f a then a else if f b = a then f a else f b) ∈ orbit (↥(closure S)) b
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case pos
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : f b = f a
⊢ a ∈ orbit (↥(closure S)) a

Tactic:
;

Goal state after:
case pos
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : f b = f a
⊢ a ∈ orbit (↥(closure S)) a
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 d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
h : ¬c = d
H : (↑c).Disjoint ↑d
h' : ↑(↑τ c) = ↑(↑τ d)
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
h : ¬c = d
H : (↑c).Disjoint ↑d
h' : ↑(↑τ c) = ↑(↑τ d)
⊢ False