awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
⊢ Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) g ↔ ∀ (h : G), h ∈ H ↔ g * h * g⁻¹ ∈ H

Tactic:
mem_set_normalizer_iff

Premises used: Subgroup.mem_set_normalizer_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
⊢ Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) g ↔ ∀ (h : G), h ∈ H ↔ g⁻¹ * h * g ∈ H

Tactic:
mem_set_normalizer_iff''

Premises used: Subgroup.mem_set_normalizer_iff''
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
⊢ Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G)) g ↔ ∀ (n : G), n * g ∈ H ↔ g * n ∈ H

Tactic:
mem_set_normalizer_iff'

Premises used: Subgroup.mem_set_normalizer_iff'
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
rw : n ∈ H ↔ x * n * x⁻¹ ∈ (↑H : Set G)
rw₁ : n ∈ H ↔ x * n * x⁻¹ ∈ H
rw₂ : n ∈ H ↔ x * n ∈ H
rw₃ rw₄ : n ∈ H ↔ n ∈ H
⊢ n ∈ (↑H : Set G) ↔ x * n * x⁻¹ ∈ (↑H : Set G)

Tactic:
rw [SetLike.mem_coe, SetLike.mem_coe, H.mul_mem_cancel_right <| H.inv_mem xH,
    H.mul_mem_cancel_left xH]

Premises used: Subgroup.mul_mem_cancel_left, Subgroup.mul_mem_cancel_right, Subgroup.inv_mem, SetLike.mem_coe
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_3
inst : CommGroup G
H : Subgroup G
⊢ IsMulCommutative.{u_3} ↥H

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
a b : G
ha : a ∈ H
hb : b ∈ H
⊢ a * b = b * a

Tactic:
setLike_mul_comm ha hb

Premises used: setLike_mul_comm
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst : Group G
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
inst_4 : SetLike S G
inst_5 : OneMemClass S G
inst_6 : MulMemClass S G
inst_7 : InvMemClass S G
s : S
h : InjOn.{u_4, u_5} (β := H) (⇑f : (a : G) → H) (↑s : Set G)
a : G
ha : a ∈ s
ha' : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H)
⊢ a = 1

Tactic:
h ha (one_mem s) ?_

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst : Group G
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
inst_4 : SetLike S G
inst_5 : OneMemClass S G
inst_6 : MulMemClass S G
inst_7 : InvMemClass S G
s : S
h : InjOn.{u_4, u_5} (β := H) (⇑f : (a : G) → H) (↑s : Set G)
a : G
ha : a ∈ s
ha' : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H)
refine : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) 1 : H)
⊢ a = 1

Tactic:
refine h ha (one_mem s) ?_

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst : Group G
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
inst_4 : SetLike S G
inst_5 : OneMemClass S G
inst_6 : MulMemClass S G
inst_7 : InvMemClass S G
s : S
h : InjOn.{u_4, u_5} (β := H) (⇑f : (a : G) → H) (↑s : Set G)
a : G
ha : a ∈ s
ha' rwa rwa₁ rwa₂ rwa₃ : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H)
⊢ Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) ((f : (a : G) → H) 1 : H)

Tactic:
rwa [map_one]

Premises used: map_one
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst : Group G
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
inst_4 : SetLike S G
inst_5 : OneMemClass S G
inst_6 : MulMemClass S G
inst_7 : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H) → a = 1
x : G
hx : x ∈ (↑s : Set G)
y : G
hy : y ∈ (↑s : Set G)
hxy : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
⊢ x = y

Tactic:
mul_inv_eq_one.1 <| h _ (mul_mem ?_ (inv_mem ?_)) ?_

Premises used: mul_inv_eq_one, InvMemClass.inv_mem, Iff.mp, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst : Group G
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
inst_4 : SetLike S G
inst_5 : OneMemClass S G
inst_6 : MulMemClass S G
inst_7 : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H) → a = 1
x : G
hx : x ∈ (↑s : Set G)
y : G
hy : y ∈ (↑s : Set G)
hxy : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
refine_1 : x ∈ s
refine_2 : y ∈ s
refine_3 : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) (x * y⁻¹) : H) (1 : H)
⊢ x = y

Tactic:
refine mul_inv_eq_one.1 <| h _ (mul_mem ?_ (inv_mem ?_)) ?_

Premises used: mul_inv_eq_one, InvMemClass.inv_mem, Iff.mp, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst : Group G
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
inst_4 : SetLike S G
inst_5 : OneMemClass S G
inst_6 : MulMemClass S G
inst_7 : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H) → a = 1
x : G
hx : x ∈ (↑s : Set G)
y : G
hy : y ∈ (↑s : Set G)
hxy : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
⊢ x ∈ s

Tactic:
simp_all
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst : Group G
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
inst_4 : SetLike S G
inst_5 : OneMemClass S G
inst_6 : MulMemClass S G
inst_7 : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H) → a = 1
x : G
hx : x ∈ (↑s : Set G)
y : G
hy : y ∈ (↑s : Set G)
hxy : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
⊢ y ∈ s

Tactic:
simp_all
-- Module: Mathlib.Algebra.Group.Subgroup.Defs
Goal:
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst : Group G
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
inst_4 : SetLike S G
inst_5 : OneMemClass S G
inst_6 : MulMemClass S G
inst_7 : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) a : H) (1 : H) → a = 1
x : G
hx : x ∈ (↑s : Set G)
y : G
hy : y ∈ (↑s : Set G)
hxy : Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) y : H)
⊢ Eq.{u_5 + 1} (α := H) ((f : (a : G) → H) (x * y⁻¹) : H) (1 : H)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Group.Subgroup.Even
Goal:
S : Type u_1
inst : CommSemigroup S
a : S
⊢ Membership.mem (γ := Subsemigroup S) (square S) a ↔ IsSquare a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, IsSquare
-- Module: Mathlib.Algebra.Group.Subgroup.Even
Goal:
S : Type u_1
inst : CommSemigroup S
⊢ (↑(square S) : Set S) = {s : S | IsSquare s}

Tactic:
rfl

Premises used: setOf, IsSquare, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Even
Goal:
M : Type u_1
inst : CommMonoid M
⊢ Eq (α := Subsemigroup M) (toSubsemigroup (square M)) (Subsemigroup.square M)

Tactic:
rfl

Premises used: Subsemigroup.square, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Even
Goal:
M : Type u_1
inst : CommMonoid M
a : M
⊢ Membership.mem (γ := Submonoid M) (square M) a ↔ IsSquare a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, IsSquare
-- Module: Mathlib.Algebra.Group.Subgroup.Even
Goal:
M : Type u_1
inst : CommMonoid M
⊢ (↑(square M) : Set M) = {s : M | IsSquare s}

Tactic:
rfl

Premises used: setOf, IsSquare, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Even
Goal:
G : Type u_1
inst : CommGroup G
⊢ Eq (α := Submonoid G) (toSubmonoid (square G)) (Submonoid.square G)

Tactic:
rfl

Premises used: Submonoid.square, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Even
Goal:
G : Type u_1
inst : CommGroup G
a : G
⊢ Membership.mem (γ := Subgroup G) (square G) a ↔ IsSquare a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, IsSquare
-- Module: Mathlib.Algebra.Group.Subgroup.Even
Goal:
G : Type u_1
inst : CommGroup G
⊢ (↑(square G) : Set G) = {s : G | IsSquare s}

Tactic:
rfl

Premises used: setOf, IsSquare, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
K : Subgroup G
inst_2 : Finite G
⊢ Finite.{u_1 + 1} ↥K

Tactic:
Subtype.finite

Premises used: Subtype.finite
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
l : List G
⊢ (∀ x ∈ l, x ∈ K) → l.prod ∈ K

Tactic:
list_prod_mem

Premises used: list_prod_mem, Set.Mem
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_3
inst : CommGroup G
K : Subgroup G
g : Multiset G
⊢ (∀ a ∈ g, a ∈ K) → g.prod ∈ K

Tactic:
multiset_prod_mem g

Premises used: multiset_prod_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
g : Multiset G
comm : Set.Pairwise.{u_1} (α := G) {x : G | x ∈ g} Commute
⊢ (∀ a ∈ g, a ∈ K) → g.noncommProd comm ∈ K

Tactic:
K.toSubmonoid.multiset_noncommProd_mem g comm

Premises used: Set.Mem, Submonoid.multiset_noncommProd_mem, Subgroup.toSubmonoid
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_3
inst : CommGroup G
K : Subgroup G
ι : Type u_4
t : Finset ι
f : ι → G
h : ∀ c ∈ t, f c ∈ K
⊢ ∏ c ∈ t, f c ∈ K

Tactic:
prod_mem h

Premises used: prod_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
ι : Type u_3
t : Finset ι
f : ι → G
comm : (↑t : Set ι).Pairwise (Function.onFun Commute f)
⊢ (∀ c ∈ t, f c ∈ K) → t.noncommProd f comm ∈ K

Tactic:
K.toSubmonoid.noncommProd_mem t f comm

Premises used: Set.Mem, Submonoid.noncommProd_mem, Subgroup.toSubmonoid
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
l : List ↥H
⊢ (↑l.prod : G) = (List.map (Subtype.val (p := fun (x : G) ↦ x ∈ H)) l).prod

Tactic:
SubmonoidClass.coe_list_prod l

Premises used: Set.Mem, SubmonoidClass.coe_list_prod
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_3
inst : CommGroup G
H : Subgroup G
m : Multiset ↥H
⊢ (↑m.prod : G) = (Multiset.map (Subtype.val (p := fun (x : G) ↦ x ∈ H)) m).prod

Tactic:
SubmonoidClass.coe_multiset_prod m

Premises used: SubmonoidClass.coe_multiset_prod
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
ι : Type u_3
G : Type u_4
inst : CommGroup G
H : Subgroup G
f : ι → ↥H
s : Finset ι
⊢ Eq.{u_4 + 1} (α := G) (↑(∏ i ∈ s, f i) : G) (∏ i ∈ s, (↑(f i) : G))

Tactic:
SubmonoidClass.coe_finsetProd f s

Premises used: SubmonoidClass.coe_finsetProd
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H K : Subgroup G
⊢ Membership.mem (α := ↥⊥) (γ := Finset ↥⊥) {1}
    (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) ⊥ x) 1 ⋯ : ↥⊥)

Tactic:
Finset.mem_singleton_self _

Premises used: Finset.mem_singleton_self, Set.Mem, setOf
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
H K : Subgroup G
⊢ Membership.mem (α := ↥⊥) (γ := Finset ↥⊥) {1}
    (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) ⊥ x) 1 ⋯ : ↥⊥)

Tactic:
exact Finset.mem_singleton_self _

Premises used: Finset.mem_singleton_self
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
⊢ Nat.card.{u_1} ↥⊥ = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
⊢ Nat.card.{u_1} ↥⊤ = Nat.card G

Tactic:
Nat.card_congr Subgroup.topEquiv.toEquiv

Premises used: MulEquiv.toEquiv, Nat.card_congr, Subgroup.topEquiv
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : Finite.{u_1 + 1} ↥K
hle : H ≤ K
hcard : Nat.card.{u_1} ↥K ≤ Nat.card.{u_1} ↥H
⊢ H = K

Tactic:
SetLike.coe_injective <| Set.Finite.eq_of_subset_of_card_le (Set.toFinite _) hle hcard

Premises used: SetLike.coe_injective, Set.toFinite, Set.Finite.eq_of_subset_of_card_le
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Finite G
h : Nat.card G ≤ Nat.card.{u_1} ↥H
⊢ H = ⊤

Tactic:
eq_of_le_of_card_ge le_top (Nat.card_congr (Equiv.Set.univ G) ▸ h)

Premises used: Eq.rec, Nat.card_congr, le_top, Subgroup.eq_of_le_of_card_ge, Eq.symm, Equiv.Set.univ
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_1 + 1} ↥H
h : Nat.card.{u_1} ↥H = Nat.card G
⊢ Finite G

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero (h ▸ Nat.card_pos.ne')
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_1 + 1} ↥H
h : Nat.card.{u_1} ↥H = Nat.card G
this : Finite G
⊢ H = ⊤

Tactic:
eq_top_of_le_card _ (Nat.le_of_eq h.symm)

Premises used: Nat.le_of_eq, Eq.symm, Subgroup.eq_top_of_le_card
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_1 + 1} ↥H
h : Nat.card.{u_1} ↥H = Nat.card G
this : Finite G
⊢ H = ⊤

Tactic:
exact eq_top_of_le_card _ (Nat.le_of_eq h.symm)

Premises used: Nat.le_of_eq, Eq.symm, Subgroup.eq_top_of_le_card
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_1 + 1} ↥H
h : H = ⊤
⊢ Nat.card.{u_1} ↥H = Nat.card G

Tactic:
simpa only [h] using card_top

Premises used: Subgroup.card_top
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_1 + 1} ↥H
h : Nat.card.{u_1} ↥H ≤ 1
⊢ H = ⊥

Tactic:
let _ := Finite.card_le_one_iff_subsingleton.mp h
  eq_bot_of_subsingleton H

Premises used: Finite.card_le_one_iff_subsingleton, Iff.mp, Subgroup.eq_bot_of_subsingleton
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : Nat.card.{u_1} ↥H = 1
⊢ H = ⊥

Tactic:
let _ := (Nat.card_eq_one_iff_unique.mp h).1
  eq_bot_of_subsingleton H

Premises used: Nat.card_eq_one_iff_unique, And.left, Iff.mp, Subgroup.eq_bot_of_subsingleton
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_1 + 1} ↥H
h : H = ⊥
⊢ Nat.card.{u_1} ↥H ≤ 1

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
⊢ Nat.card.{u_1} ↥⊥ = 1

Tactic:
card_bot

Premises used: Subgroup.card_bot
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
⊢ Nat.card.{u_1} ↥⊥ = 1

Tactic:
exact card_bot

Premises used: Subgroup.card_bot
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_1 + 1} ↥H
⊢ 1 < Nat.card.{u_1} ↥H ↔ H ≠ ⊥

Tactic:
lt_iff_not_ge.trans H.card_le_one_iff_eq_bot.not

Premises used: lt_iff_not_ge, Iff.not, Iff.trans, Subgroup.card_le_one_iff_eq_bot
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Finite G
⊢ Nat.card.{u_1} ↥H ≤ Nat.card G

Tactic:
Nat.card_le_card_of_injective _ Subtype.coe_injective

Premises used: Nat.card_le_card_of_injective, Subtype.coe_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : Finite.{u_1 + 1} ↥K
h : H ≤ K
⊢ Nat.card.{u_1} ↥H ≤ Nat.card.{u_1} ↥K

Tactic:
Nat.card_le_card_of_injective _ (Subgroup.inclusion_injective h)

Premises used: Nat.card_le_card_of_injective, Subgroup.inclusion_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H : Type u_3
inst_1 : Group H
K : Subgroup G
f : G →* H
hf : Function.Injective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
⊢ Nat.card.{u_3} ↥(map f K) = Nat.card.{u_1} ↥K

Tactic:
apply Nat.card_image_of_injective hf

Premises used: Nat.card_image_of_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
L : Subgroup ↥K
⊢ Nat.card.{u_1} ↥(map K.subtype L) = Nat.card.{u_1} ↥L

Tactic:
card_map_of_injective K.subtype_injective

Premises used: Subgroup.card_map_of_injective, Subgroup.subtype_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
G' : Type u_3
inst_1 : Group G'
e : G ≃* G'
⊢ Nat.card.{u_3} ↥((e.mapSubgroup : (a : Subgroup G) → Subgroup G') H : Subgroup G') = Nat.card.{u_1} ↥H

Tactic:
Subgroup.card_map_of_injective e.injective

Premises used: Subgroup.card_map_of_injective, Set.Mem, MulEquiv.injective
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
η : Type u_3
f : η → Type u_4
inst : (i : η) → Group (f i)
inst_1 : Finite η
inst_2 : DecidableEq η
H : Subgroup ((i : η) → f i)
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle (M := f) i (x i) ∈ H
⊢ x ∈ H

Tactic:
Submonoid.pi_mem_of_mulSingle_mem x h

Premises used: Submonoid.pi_mem_of_mulSingle_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
η : Type u_3
f : η → Type u_4
inst : (i : η) → Group (f i)
inst_1 : DecidableEq η
inst_2 : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ pi (f := f) univ H ≤ J ↔ ∀ (i : η), map (MonoidHom.mulSingle f i) (H i) ≤ J

Tactic:
Submonoid.pi_le_iff

Premises used: Set.Mem, Submonoid.pi_le_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
η : Type u_3
f : η → Type u_4
inst : (i : η) → Group (f i)
inst_1 : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
pos :
  ∀ (H : j = i),
    Membership.mem (α := f j) (s j)
      (((MonoidHom.mulSingle f i : f i →* (i : η) → f i) : (a : f i) → (i : η) → f i) _x j : f j)
neg :
  ∀ (H : ¬j = i),
    Membership.mem (α := f j) (s j)
      (((MonoidHom.mulSingle f i : f i →* (i : η) → f i) : (a : f i) → (i : η) → f i) _x j : f j)
⊢ Membership.mem (α := f j) (s j)
    (((MonoidHom.mulSingle f i : f i →* (i : η) → f i) : (a : f i) → (i : η) → f i) _x j : f j)

Tactic:
by_cases H : j = i
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
η : Type u_3
f : η → Type u_4
inst : (i : η) → Group (f i)
inst_1 : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : j = i
pos :
  ∀ (_x : f j) (hx : _x ∈ s j),
    Membership.mem (α := f j) (s j)
      (((MonoidHom.mulSingle f j : f j →* (i : η) → f i) : (a : f j) → (i : η) → f i) _x j : f j)
⊢ Membership.mem (α := f j) (s j)
    (((MonoidHom.mulSingle f i : f i →* (i : η) → f i) : (a : f i) → (i : η) → f i) _x j : f j)

Tactic:
subst H
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
η : Type u_3
f : η → Type u_4
inst : (i : η) → Group (f i)
inst_1 : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
j : η
_x : f j
hx : _x ∈ s j
⊢ Membership.mem (α := f j) (s j)
    (((MonoidHom.mulSingle f j : f j →* (i : η) → f i) : (a : f j) → (i : η) → f i) _x j : f j)

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
η : Type u_3
f : η → Type u_4
inst : (i : η) → Group (f i)
inst_1 : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : ¬j = i
⊢ Membership.mem (α := f j) (s j)
    (((MonoidHom.mulSingle f i : f i →* (i : η) → f i) : (a : f i) → (i : η) → f i) _x j : f j)

Tactic:
simpa [H] using hs _
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
η : Type u_3
f : η → Type u_4
inst : (i : η) → Group (f i)
inst_1 : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
⊢ LE.le (α := Subgroup ((i : η) → f i)) (pi (f := f) univ fun (i : η) ↦ closure (s i))
    (closure (Set.pi (α := f) univ fun (i : η) ↦ s i))

Tactic:
exact pi_le_iff.mpr fun i => (gc_map_comap _).l_le <| (closure_le _).2 fun _x hx =>
          subset_closure <| mem_univ_pi.mpr fun j => by
        by_cases H : j = i
        · subst H
          simpa
        · simpa [H] using hs _

Premises used: Iff.mpr, Subgroup.gc_map_comap, Subgroup.pi_le_iff, Subgroup.closure_le, MonoidHom.mulSingle, GaloisConnection.l_le, Subgroup.comap
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
η : Type u_3
f : η → Type u_4
inst : (i : η) → Group (f i)
inst_1 : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
⊢ LE.le (α := Subgroup ((i : η) → f i)) (pi (f := f) univ fun (i : η) ↦ closure (s i))
    (closure (Set.pi (α := f) univ fun (i : η) ↦ s i))

Tactic:
classical
      exact pi_le_iff.mpr fun i => (gc_map_comap _).l_le <| (closure_le _).2 fun _x hx =>
          subset_closure <| mem_univ_pi.mpr fun j => by
        by_cases H : j = i
        · subst H
          simpa
        · simpa [H] using hs _

Premises used: Iff.mpr, Subgroup.gc_map_comap, Subgroup.pi_le_iff, Subgroup.closure_le, MonoidHom.mulSingle, GaloisConnection.l_le, Subgroup.comap
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
S : Set G
inst_1 : Finite.{u_1 + 1} (↑S : Type u_1)
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
haveI : ∀ (this : (a : Prop) → Decidable a), Membership.mem (γ := Subgroup G) (normalizer S) x
⊢ Membership.mem (γ := Subgroup G) (normalizer S) x

Tactic:
haveI := Classical.propDecidable
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
S : Set G
inst_1 : Finite.{u_1 + 1} (↑S : Type u_1)
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
intro : ∀ (val : Fintype (↑S : Type u_1)), Membership.mem (γ := Subgroup G) (normalizer S) x
⊢ Membership.mem (γ := Subgroup G) (normalizer S) x

Tactic:
cases nonempty_fintype S

Premises used: Set.Elem, nonempty_fintype
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
S : Set G
inst_1 : Finite.{u_1 + 1} (↑S : Type u_1)
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
val : Fintype (↑S : Type u_1)
n : G
h₁ : x * n * x⁻¹ ∈ S
rw rw₁ : Fintype.card.{u_1} (↑S : Type u_1) ≤ Fintype.card.{u_1} (↑S : Type u_1)
⊢ Fintype.card.{u_1} (↑S : Type u_1) ≤ Fintype.card.{u_1} (↑((fun (n : G) ↦ x * n * x⁻¹) '' S) : Type u_1)

Tactic:
rw [Set.card_image_of_injective S conj_injective]

Premises used: conj_injective, Set.card_image_of_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
S : Set G
inst_1 : Finite.{u_1 + 1} (↑S : Type u_1)
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
val : Fintype (↑S : Type u_1)
⊢ Membership.mem (γ := Subgroup G) (normalizer S) x

Tactic:
exact fun n =>
    ⟨h n, fun h₁ =>
      have heq : (fun n => x * n * x⁻¹) '' S = S :=
        Set.eq_of_subset_of_card_le (fun n ⟨y, hy⟩ => hy.2 ▸ h y hy.1)
          (by rw [Set.card_image_of_injective S conj_injective])
      have : x * n * x⁻¹ ∈ (fun n => x * n * x⁻¹) '' S := heq.symm ▸ h₁
      let ⟨y, hy⟩ := this
      conj_injective hy.2 ▸ hy.1⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
inst_2 : Fintype M
inst_3 : DecidableEq N
f : M →* N
hf : Function.Injective.{u_4 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Fintype.card.{u_5} ↥(mrange f) = Fintype.card M

Tactic:
Set.card_range_of_injective hf

Premises used: Set.Mem, setOf, Set.card_range_of_injective, Set.range
-- Module: Mathlib.Algebra.Group.Subgroup.Finite
Goal:
G : Type u_1
inst : Group G
N : Type u_3
inst_1 : Group N
inst_2 : Fintype G
inst_3 : DecidableEq N
f : G →* N
hf : Function.Injective.{u_1 + 1, u_3 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ Fintype.card.{u_3} ↥f.range = Fintype.card G

Tactic:
Set.card_range_of_injective hf

Premises used: Set.Mem, setOf, Set.card_range_of_injective, Set.range
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x_1 x : M
h : x ∈ Set.range f
mem : ∀ (i : ι), ∃ (a : ι →₀ ℤ), f i = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2
⊢ ∃ (a : ι →₀ ℤ), x = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2

Tactic:
obtain ⟨i, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ f i = Finsupp.prod (Finsupp.single i 1) fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Finsupp
Goal:
M : Type u_1
inst : CommGroup M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ ∃ (a : ι →₀ ℤ), f i = a.prod fun (x1 : ι) (x2 : ℤ) ↦ f x1 ^ x2

Tactic:
exact ⟨Finsupp.single i 1, by simp⟩