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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⁅⊤, ⊤⁆ = ⊤ ↔ ⁅⊤, ⊤⁆ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H : Subgroup G
f : G →* G'
inst✝ : IsPerfect ↥H
⊢ map f H = map f H

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsPerfect G
⊢ IsPerfect ↥(map f ⊤)

Tactic:
]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsPerfect G
⊢ IsPerfect ↥(map f ⊤)
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsPerfect G
hf : Function.Surjective ⇑f
⊢ IsPerfect ↥f.range

Tactic:
]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsPerfect G
hf : Function.Surjective ⇑f
⊢ IsPerfect ↥f.range
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n✝ n : ℕ
⊢ ⊤ = ⊤

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ IsCoatom (stabilizer ↥(alternatingGroup α) ↑s)

Tactic:
]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ IsCoatom (stabilizer ↥(alternatingGroup α) ↑s)
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : IsPerfect ↥H
n✝ n : ℕ
⊢ H = H

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ Subgroup.upperCentralSeries G 1 = Subgroup.upperCentralSeries G n

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ Subgroup.upperCentralSeries G 1 = Subgroup.upperCentralSeries G n
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case h0
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ 1 ≤ n

Tactic:
]

Goal state after:
case h0
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ 1 ≤ n
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ ⁅⁅⊤, ⊤⁆, Subgroup.upperCentralSeries G 2⁆ = ⊥

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ ⁅⁅⊤, ⊤⁆, Subgroup.upperCentralSeries G 2⁆ = ⊥
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ ⁅Subgroup.upperCentralSeries G 2, ⊤⁆ ≤ Subgroup.upperCentralSeries G 1

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ ⁅Subgroup.upperCentralSeries G 2, ⊤⁆ ≤ Subgroup.upperCentralSeries G 1
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
⊢ center G = center G

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(powersetCard α n)

Tactic:
have : IsPretransitive (alternatingGroup α) (powersetCard α n) :=
    isPretransitive_alternatingGroup (le_trans h_three_le hn.le)
  have : Nontrivial (powersetCard α n) := nontrivial (by positivity) (by simpa using hn)
  obtain ⟨s⟩ := this.to_nonempty
  rw [← isCoatom_stabilizer_iff_preprimitive _ s, stabilizer_coe]
  apply alternatingGroup.isCoatom_stabilizer
  · rw [powersetCard.coe_nonempty_iff]
    exact le_trans (by norm_num) h_three_le
  · simpa [nonempty_compl, ne_eq, eq_univ_iff_ncard, ncard_eq] using ne_of_lt hn
  · simpa only [ncard_eq]

Goal state after:
Module: Mathlib.GroupTheory.IndexNSmul

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module.Finite ℤ M
inst✝¹ : IsTorsionFree ℤ M
A : AddSubgroup M
inst✝ : A.FiniteIndex
this : finrank ℤ ↥(DistribSMul.toLinearMap ℤ M A.index).range = finrank ℤ M
⊢ finrank ℤ ↥(DistribSMul.toLinearMap ℤ M A.index).range ≤ finrank ℤ ↥A

Tactic:
]

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module.Finite ℤ M
inst✝¹ : IsTorsionFree ℤ M
A : AddSubgroup M
inst✝ : A.FiniteIndex
this : finrank ℤ ↥(DistribSMul.toLinearMap ℤ M A.index).range = finrank ℤ M
⊢ finrank ℤ ↥(DistribSMul.toLinearMap ℤ M A.index).range ≤ finrank ℤ ↥A
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ of ↑b * t = of ↑(φ (φ.symm b)) * t

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ of ↑b * t = of ↑(φ (φ.symm b)) * t
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ of ↑(φ a) = of ↑(φ a) * t * t⁻¹

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ of ↑(φ a) = of ↑(φ a) * t * t⁻¹
Module: Mathlib.GroupTheory.IndexNSmul

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
A B : AddSubgroup M
inst✝² : Module.Finite ℤ ↥B
inst✝¹ : IsTorsionFree ℤ ↥B
h : A ≤ B
inst✝ : A.IsFiniteRelIndex B
this : (A.addSubgroupOf B).FiniteIndex
⊢ finrank ℤ ↥A = finrank ℤ ↥(A.addSubgroupOf B)

Tactic:
]

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
A B : AddSubgroup M
inst✝² : Module.Finite ℤ ↥B
inst✝¹ : IsTorsionFree ℤ ↥B
h : A ≤ B
inst✝ : A.IsFiniteRelIndex B
this : (A.addSubgroupOf B).FiniteIndex
⊢ finrank ℤ ↥A = finrank ℤ ↥(A.addSubgroupOf B)
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ of ↑(φ.symm b) = t⁻¹ * (t * of ↑(φ.symm b))

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ of ↑(φ.symm b) = t⁻¹ * (t * of ↑(φ.symm b))
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ t⁻¹ * of ↑b = t⁻¹ * of ↑b * t * t⁻¹

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ t⁻¹ * of ↑b = t⁻¹ * of ↑b * t * t⁻¹
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ of ↑a * t⁻¹ = t⁻¹ * (t * of ↑a * t⁻¹)

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ of ↑a * t⁻¹ = t⁻¹ * (t * of ↑a * t⁻¹)
Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁴ : Finite ι
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
S : Submonoid M
hf : S.IsLocalizationMap ⇑f
n : ι → N
x : N → M × ↥S
hx : ∀ (z : N), z * f ↑(x z).2 = f (x z).1
val✝ : Fintype ι
i : ι
⊢ f (x (n i)).1 * f ↑(∏ x_1 ∈ univ.erase i, (x (n x_1)).2) = f (x (n i)).1 * f ↑(∏ j ∈ univ.erase i, (x (n j)).2)

Tactic:
]

Goal state after:
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⟩ ⋯
hf : S.subtype.comp f = MonoidHom.id (HNNExtension G A B φ)
⊢ motive ((S.subtype.comp f) 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⟩ ⋯
hf : S.subtype.comp f = MonoidHom.id (HNNExtension G A B φ)
⊢ motive ((S.subtype.comp f) x)
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inl
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
ne_top : H ≠ ⊤
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : H.Normal
ih : ⊤ ≠ ⊤ → ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
]

Goal state after:
case step.inl
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
ne_top : H ≠ ⊤
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : H.Normal
ih : ⊤ ≠ ⊤ → ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case top
G : Type u_1
inst✝ : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
⊢ K.IsSubnormal

Tactic:
]

Goal state after:
case top
G : Type u_1
inst✝ : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
⊢ K.IsSubnormal
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₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ ↑d₂ * b₁ ≤ ↑b₂ * d₁ ↔ ↑d₂ * b₁ ≤ ↑b₂ * d₁

Tactic:
]

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

Goal state before:
pp: 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)
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
]

Goal state after:
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)
⊢ f m ∣ n₁ ∨ f m ∣ n₂
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝ : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
A B : Subgroup ↥K
h_le : A ≤ B
hSubn : B.IsSubnormal
hN : B ≤ normalizer ↑A
ih : (map K.subtype B).IsSubnormal
⊢ ((map K.subtype A).subgroupOf (map K.subtype B)).Normal

Tactic:
]

Goal state after:
case step
G : Type u_1
inst✝ : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
A B : Subgroup ↥K
h_le : A ≤ B
hSubn : B.IsSubnormal
hN : B ≤ normalizer ↑A
ih : (map K.subtype B).IsSubnormal
⊢ ((map K.subtype A).subgroupOf (map K.subtype B)).Normal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝ : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
A B : Subgroup ↥K
h_le : A ≤ B
hSubn : B.IsSubnormal
hN : B ≤ normalizer ↑A
ih : (map K.subtype B).IsSubnormal
⊢ map K.subtype B ≤ normalizer ↑(map K.subtype A)

Tactic:
]

Goal state after:
case step
G : Type u_1
inst✝ : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
A B : Subgroup ↥K
h_le : A ≤ B
hSubn : B.IsSubnormal
hN : B ≤ normalizer ↑A
ih : (map K.subtype B).IsSubnormal
⊢ map K.subtype B ≤ normalizer ↑(map K.subtype A)
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: 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
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
]

Goal state after:
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
⊢ f m ∣ n₁ ∨ f m ∣ n₂
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
HK : H ≤ K
Hsn : (H.subgroupOf K).IsSubnormal
Ksn : K.IsSubnormal
key : H.IsSubnormal
⊢ H.IsSubnormal

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
HK : H ≤ K
Hsn : (H.subgroupOf K).IsSubnormal
Ksn : K.IsSubnormal
key : H.IsSubnormal
⊢ H.IsSubnormal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case top
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
⊢ ⊤.IsSubnormal

Tactic:
]

Goal state after:
case top
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
⊢ ⊤.IsSubnormal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer ↑H
ih : (map f K).IsSubnormal
⊢ ((map f H).subgroupOf (map f K)).Normal

Tactic:
]

Goal state after:
case step
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer ↑H
ih : (map f K).IsSubnormal
⊢ ((map f H).subgroupOf (map f K)).Normal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer ↑H
ih : (comap f K).IsSubnormal
⊢ ((comap f H).subgroupOf (comap f K)).Normal

Tactic:
]

Goal state after:
case step
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer ↑H
ih : (comap f K).IsSubnormal
⊢ ((comap f H).subgroupOf (comap f K)).Normal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer ↑H
ih : (comap f K).IsSubnormal
⊢ comap f K ≤ normalizer ↑(comap f H)

Tactic:
]

Goal state after:
case step
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer ↑H
ih : (comap f K).IsSubnormal
⊢ comap f K ≤ normalizer ↑(comap f H)
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
this✝ : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem : ↑(⋯.equiv w.head).2 ∈ toSubgroup A B u
this : w.head⁻¹ ∈ toSubgroup A B u
⊢ w.head ∈ toSubgroup A B u

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
this✝ : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem : ↑(⋯.equiv w.head).2 ∈ toSubgroup A B u
this : w.head⁻¹ ∈ toSubgroup A B u
⊢ w.head ∈ toSubgroup A B u
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₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ ↑d₂ * b₁ < ↑b₂ * d₁ ↔ ↑d₂ * b₁ < ↑b₂ * d₁

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Semigroup P
f : M →ₙ* P
g : N →ₙ* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
mn : M × N
⊢ f mn.1 * g mn.2 = f mn.1 * g mn.2

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : Monoid P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
mn : M × N
⊢ f mn.1 * g mn.2 = f mn.1 * g mn.2

Tactic:
]

Goal state after:
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✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ ↑c.2 * (↑a.2 * b.1) ≤ ↑b.2 * (↑a.2 * c.1)

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ ↑c.2 * (↑a.2 * b.1) ≤ ↑b.2 * (↑a.2 * c.1)
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✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ ↑c.2 * b.1 ≤ ↑b.2 * c.1

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ ↑c.2 * b.1 ≤ ↑b.2 * c.1
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case inl
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 ∣ s * (m₁, s₁).1
this : f m ∣ n₁
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
]

Goal state after:
case inl
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 ∣ s * (m₁, s₁).1
this : f m ∣ n₁
⊢ f m ∣ n₁ ∨ f m ∣ n₂
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✝¹ : ↥s
a✝ : α
b✝ : ↥s
hab : ↑b✝ * a✝¹ ≤ ↑b✝¹ * a✝
hba : ↑b✝¹ * a✝ ≤ ↑b✝ * a✝¹
⊢ ↑1 * (↑b✝¹ * a✝) = ↑1 * (↑b✝¹ * a✝)

Tactic:
]

Goal state after:
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 → b ≤ a → a = b

Tactic:
induction a using Localization.rec
    on_goal 1 =>
      induction b using Localization.rec
      · simp_rw [mk_le_mk, mk_eq_mk_iff, r_iff_exists]
        exact fun hab hba => ⟨1, by rw [hab.antisymm hba]⟩
    all_goals rfl

Goal state after:
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
hw : w.head ∈ toSubgroup A B u
x : G
h2 : ∀ u' ∈ Option.map Prod.fst (some (-u, x)), w.head ∈ toSubgroup A B u → u = u'
hx : w.toList.head? = some (-u, x)
⊢ False

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hw : w.head ∈ toSubgroup A B u
x : G
h2 : ∀ u' ∈ Option.map Prod.fst (some (-u, x)), w.head ∈ toSubgroup A B u → u = u'
hx : w.toList.head? = some (-u, x)
⊢ False
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.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
l : List ℕ
hl : l ∈ c.ranges
n : ℕ
hn : n ∈ l
⊢ ∃ s ∈ c.ranges, n ∈ s

Tactic:
]

Goal state after:
α : 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
l : List ℕ
hl : l ∈ c.ranges
n : ℕ
hn : n ∈ l
⊢ ∃ s ∈ c.ranges, n ∈ s