awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
x y : α
rw : Decidable ((fun (x y : α) ↦ x⁻¹ * y ∈ s) x y)
⊢ Decidable ((leftRel s : α → α → Prop) x y)

Tactic:
rw [leftRel_eq]

Premises used: QuotientGroup.leftRel_eq
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
x y : α
⊢ Decidable ((fun (x y : α) ↦ x⁻¹ * y ∈ s) x y)

Tactic:
exact ‹DecidablePred (· ∈ s)› _
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
⊢ (∃ (a : ↥s), (↑a : α) * y = x) ↔ ∃ (a : ↥s), y * x⁻¹ = (↑a⁻¹ : α)

Tactic:
simp only [mul_inv_eq_iff_eq_mul, Subgroup.coe_inv, eq_inv_mul_iff_mul_eq]

Premises used: Subgroup.coe_inv, eq_inv_mul_iff_mul_eq, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
⊢ (∃ (a : ↥s), y * x⁻¹ = (↑a⁻¹ : α)) ↔ y * x⁻¹ ∈ s

Tactic:
simp [exists_inv_mem_iff_exists_mem]

Premises used: exists_inv_mem_iff_exists_mem
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
simp : ∀ (a b : α), (rightRel s : α → α → Prop) a b ↔ b * a⁻¹ ∈ s
⊢ ∀ (a b : α), (rightRel s : α → α → Prop) a b = (b * a⁻¹ ∈ s)

Tactic:
simp only [eq_iff_iff]

Premises used: eq_iff_iff
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ ∀ (a b : α), (rightRel s : α → α → Prop) a b ↔ b * a⁻¹ ∈ s

Tactic:
apply rightRel_apply

Premises used: QuotientGroup.rightRel_apply
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
x y : α
rw : Decidable ((fun (x y : α) ↦ y * x⁻¹ ∈ s) x y)
⊢ Decidable ((rightRel s : α → α → Prop) x y)

Tactic:
rw [rightRel_eq]

Premises used: QuotientGroup.rightRel_eq
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
x y : α
⊢ Decidable ((fun (x y : α) ↦ y * x⁻¹ ∈ s) x y)

Tactic:
exact ‹DecidablePred (· ∈ s)› _
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a b : α
rw : b * a⁻¹ ∈ s → HMul.hMul (α := α) ((fun (g : α) ↦ g⁻¹) a)⁻¹ ((fun (g : α) ↦ g⁻¹) b) ∈ s
⊢ (rightRel s : α → α → Prop) a b → (leftRel s : α → α → Prop) ((fun (g : α) ↦ g⁻¹) a) ((fun (g : α) ↦ g⁻¹) b)

Tactic:
rw [leftRel_apply, rightRel_apply]

Premises used: QuotientGroup.rightRel_apply, QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a b : α
h : b * a⁻¹ ∈ s
⊢ (b * a⁻¹)⁻¹ = HMul.hMul (α := α) ((fun (g : α) ↦ g⁻¹) a)⁻¹ ((fun (g : α) ↦ g⁻¹) b)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a b : α
⊢ b * a⁻¹ ∈ s → HMul.hMul (α := α) ((fun (g : α) ↦ g⁻¹) a)⁻¹ ((fun (g : α) ↦ g⁻¹) b) ∈ s

Tactic:
exact fun h => (congr_arg (· ∈ s) (by simp)).mp (s.inv_mem h)

Premises used: Membership.mem, Eq.mp, congr_arg, Subgroup.inv_mem
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a b : α
rw : a⁻¹ * b ∈ s → HMul.hMul (α := α) ((fun (g : α) ↦ g⁻¹) b) ((fun (g : α) ↦ g⁻¹) a)⁻¹ ∈ s
⊢ (leftRel s : α → α → Prop) a b → (rightRel s : α → α → Prop) ((fun (g : α) ↦ g⁻¹) a) ((fun (g : α) ↦ g⁻¹) b)

Tactic:
rw [leftRel_apply, rightRel_apply]

Premises used: QuotientGroup.rightRel_apply, QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a b : α
h : a⁻¹ * b ∈ s
⊢ (a⁻¹ * b)⁻¹ = HMul.hMul (α := α) ((fun (g : α) ↦ g⁻¹) b) ((fun (g : α) ↦ g⁻¹) a)⁻¹

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a b : α
⊢ a⁻¹ * b ∈ s → HMul.hMul (α := α) ((fun (g : α) ↦ g⁻¹) b) ((fun (g : α) ↦ g⁻¹) a)⁻¹ ∈ s

Tactic:
exact fun h => (congr_arg (· ∈ s) (by simp)).mp (s.inv_mem h)

Premises used: Membership.mem, Eq.mp, congr_arg, Subgroup.inv_mem
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g_1 : Quotient (rightRel s)
g : α
simp : (rightRel s : α → α → Prop) g g
⊢ (rightRel s : α → α → Prop) ((fun (g : α) ↦ g⁻¹) ((fun (g : α) ↦ g⁻¹) g)) g

Tactic:
simp only [inv_inv]

Premises used: inv_inv
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g_1 : Quotient (rightRel s)
g : α
⊢ (rightRel s : α → α → Prop) g g

Tactic:
Quotient.exact' rfl

Premises used: Quotient.exact', rfl
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g_1 : Quotient (rightRel s)
g : α
⊢ (rightRel s : α → α → Prop) g g

Tactic:
exact Quotient.exact' rfl

Premises used: Quotient.exact', rfl
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g_1 : α ⧸ s
g : α
simp : (leftRel s : α → α → Prop) g g
⊢ (leftRel s : α → α → Prop) ((fun (g : α) ↦ g⁻¹) ((fun (g : α) ↦ g⁻¹) g)) g

Tactic:
simp only [inv_inv]

Premises used: inv_inv
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g_1 : α ⧸ s
g : α
⊢ (leftRel s : α → α → Prop) g g

Tactic:
Quotient.exact' rfl

Premises used: Quotient.exact', rfl
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g_1 : α ⧸ s
g : α
⊢ (leftRel s : α → α → Prop) g g

Tactic:
exact Quotient.exact' rfl

Premises used: Quotient.exact', rfl
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ Surjective.{u_1 + 1, u_1 + 1} (α := α) (β := α ⧸ s) mk

Tactic:
Quotient.mk''_surjective

Premises used: Quotient.mk''_surjective
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ Eq.{u_1 + 1} (α := Set (α ⧸ s)) (range mk) univ

Tactic:
range_eq_univ.mpr mk_surjective

Premises used: Iff.mpr, Set.range_eq_univ, QuotientGroup.mk_surjective
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
C : α ⧸ s → Prop
x : α ⧸ s
H : ∀ (z : α), C (↑z : α ⧸ s)
⊢ C x

Tactic:
Quotient.inductionOn' x H

Premises used: Quotient.inductionOn'
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
β : Sort u_2
f : α → β
h : ∀ (a b : α), (leftRel s : α → α → Prop) a b → f a = f b
x : α
⊢ Quotient.liftOn' (↑x : α ⧸ s) f h = f x

Tactic:
rfl

Premises used: Quotient.liftOn', rfl
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
C : α ⧸ s → Prop
⊢ (∀ (x : α ⧸ s), C x) ↔ ∀ (x : α), C (↑x : α ⧸ s)

Tactic:
mk_surjective.forall

Premises used: Function.Surjective.forall, QuotientGroup.mk_surjective
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
C : α ⧸ s → Prop
⊢ (∃ (x : α ⧸ s), C x) ↔ ∃ (x : α), C (↑x : α ⧸ s)

Tactic:
mk_surjective.exists

Premises used: Function.Surjective.exists, QuotientGroup.mk_surjective
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a b : α
rw rw₁ : a⁻¹ * b ∈ s ↔ a⁻¹ * b ∈ s
⊢ (leftRel s : α → α → Prop) a b ↔ a⁻¹ * b ∈ s

Tactic:
rw [leftRel_apply]

Premises used: QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a : α ⧸ s
⊢ (↑(Quotient.out a) : α ⧸ s) = a

Tactic:
Quotient.out_eq' a

Premises used: Quotient.out_eq'
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g : α
rw rw₁ : Quotient.out (s := leftRel s) (↑g : α ⧸ s) = Quotient.out (s := leftRel s) (↑g : α ⧸ s)
⊢ Quotient.out (s := leftRel s) (↑g : α ⧸ s) =
    g * (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) (g⁻¹ * Quotient.out (s := leftRel s) (↑g : α ⧸ s)) ⋯) : α)

Tactic:
rw [mul_inv_cancel_left]

Premises used: mul_inv_cancel_left
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
b a : α
hb : b ∈ s
rwa : (a * b)⁻¹ * a ∈ s
rwa₁ : b⁻¹ * a⁻¹ * a ∈ s
rwa₂ : b⁻¹ ∈ s
rwa₃ rwa₄ rwa₅ rwa₆ : b ∈ s
⊢ Eq (α := α ⧸ s) (↑(a * b) : α ⧸ s) (↑a : α ⧸ s)

Tactic:
rwa [QuotientGroup.eq, mul_inv_rev, inv_mul_cancel_right, s.inv_mem_iff]

Premises used: QuotientGroup.eq, Subgroup.inv_mem_iff, mul_inv_rev, inv_mul_cancel_right
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
s : Set α
h :
  ∀ (x : α),
    x ∈ preimage (β := α ⧸ N) mk (mk '' s) ↔
      Membership.mem (γ := Set α) (⋃ (x : ↥N), (fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' s) x
⊢ preimage (β := α ⧸ N) mk (mk '' s) = ⋃ (x : ↥N), (fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' s

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
s : Set α
x : α
h : (∃ x_1 ∈ s, x_1⁻¹ * x ∈ N) ↔ ∃ x_1 ∈ N, x * x_1 ∈ s
⊢ x ∈ preimage (β := α ⧸ N) mk (mk '' s) ↔
    Membership.mem (γ := Set α) (⋃ (x : ↥N), (fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' s) x

Tactic:
simp only [QuotientGroup.eq, SetLike.exists, exists_prop, Set.mem_preimage, Set.mem_iUnion,
    Set.mem_image]

Premises used: Set.mem_iUnion, Set.mem_image, QuotientGroup.eq, exists_prop, SetLike.exists, Set.mem_preimage
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
s : Set α
x : α
h : ∃ x_1 ∈ s, x_1⁻¹ * x ∈ N
y : α
hs : y ∈ s
hN : y⁻¹ * x ∈ N
⊢ x * (y⁻¹ * x)⁻¹ ∈ s

Tactic:
simpa using hs
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
s : Set α
x : α
h : ∃ x_1 ∈ N, x * x_1 ∈ s
z : α
hz : z ∈ N
hxz : x * z ∈ s
⊢ (x * z)⁻¹ * x ∈ N

Tactic:
simpa using hz
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
s : Set α
x : α
⊢ (∃ x_1 ∈ s, x_1⁻¹ * x ∈ N) ↔ ∃ x_1 ∈ N, x * x_1 ∈ s

Tactic:
exact
    ⟨fun ⟨y, hs, hN⟩ => ⟨_, N.inv_mem hN, by simpa using hs⟩, fun ⟨z, hz, hxz⟩ =>
      ⟨x * z, hxz, by simpa using hz⟩⟩
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
s : Set α
rw : ∀ (x : ↥N), Eq (α := Set α) ((fun (x_1 : α) ↦ x_1 * (↑x⁻¹ : α)) '' s) ((fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' s)
⊢ preimage (β := α ⧸ N) mk (mk '' s) = ⋃ (x : ↥N), (fun (x_1 : α) ↦ x_1 * (↑x : α)) '' s

Tactic:
rw [preimage_image_mk, iUnion_congr_of_surjective (·⁻¹) inv_surjective]

Premises used: QuotientGroup.preimage_image_mk, inv_surjective, Set.iUnion_congr_of_surjective, Inv.inv
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
s : Set α
⊢ ∀ (x : ↥N), Eq (α := Set α) ((fun (x_1 : α) ↦ x_1 * (↑x⁻¹ : α)) '' s) ((fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' s)

Tactic:
fun x ↦ image_mul_right'

Premises used: Set.image_mul_right'
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
s : Set α
⊢ ∀ (x : ↥N), Eq (α := Set α) ((fun (x_1 : α) ↦ x_1 * (↑x⁻¹ : α)) '' s) ((fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' s)

Tactic:
exact fun x ↦ image_mul_right'

Premises used: Set.image_mul_right'
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
s : Set α
rw :
  Eq.{u_1 + 1} (α := Set α)
    (⋃ (x : α), ⋃ (hx : x ∈ N), (fun (x_1 : α) ↦ x_1 * (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ N) x hx) : α)) '' s)
    (⋃ b ∈ (↑N : Set α), (fun (x : α) ↦ x * b) '' s)
⊢ preimage (β := α ⧸ N) mk (mk '' s) = s * (↑N : Set α)

Tactic:
rw [preimage_image_mk_eq_iUnion_image, iUnion_subtype, ← image2_mul, ← iUnion_image_right]

Premises used: QuotientGroup.preimage_image_mk_eq_iUnion_image, Set.image2_mul, Set.iUnion_image_right, Set.iUnion_subtype
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
s : Set α
⊢ Eq.{u_1 + 1} (α := Set α)
    (⋃ (x : α), ⋃ (hx : x ∈ N), (fun (x_1 : α) ↦ x_1 * (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ N) x hx) : α)) '' s)
    (⋃ b ∈ (↑N : Set α), (fun (x : α) ↦ x * b) '' s)

Tactic:
simp only [SetLike.mem_coe]

Premises used: SetLike.mem_coe
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
rw : {1} * (↑N : Set α) = (↑N : Set α)
⊢ preimage (β := α ⧸ N) mk {(↑1 : α ⧸ N)} = (↑N : Set α)

Tactic:
rw [← image_singleton, preimage_image_mk_eq_mul]

Premises used: Set.image_singleton, QuotientGroup.preimage_image_mk_eq_mul
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
N : Subgroup α
⊢ {1} * (↑N : Set α) = (↑N : Set α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h : s = t
a : α
⊢ Eq (α := α ⧸ t) ((quotientEquivOfEq h : (a : α ⧸ s) → α ⧸ t) (↑a : α ⧸ s) : α ⧸ t) ((↑a : α ⧸ t) : α ⧸ t)

Tactic:
rfl

Premises used: Quot.map, Quotient.map', rfl
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
have :
  ∀ (t : Set ↥H) (ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t),
    ∃ (t : Finset ↥H),
      IsComplement (↑t : Set ↥H) (↑(D.subgroupOf H) : Set ↥H) ∧ ⋃ g ∈ t, (↑g : G) • (↑D : Set G) = (↑H : Set G)
⊢ ∃ (t : Finset ↥H),
    IsComplement (↑t : Set ↥H) (↑(D.subgroupOf H) : Set ↥H) ∧ ⋃ g ∈ t, (↑g : G) • (↑D : Set G) = (↑H : Set G)

Tactic:
have ⟨t, ht⟩ := (D.subgroupOf H).exists_isComplement_left 1
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
⊢ t.Finite

Tactic:
have hf : t.Finite := ht.1.finite_left_iff.mpr inferInstance
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
⊢ ∃ (t : Finset ↥H),
    IsComplement (↑t : Set ↥H) (↑(D.subgroupOf H) : Set ↥H) ∧ ⋃ g ∈ t, (↑g : G) • (↑D : Set G) = (↑H : Set G)

Tactic:
⟨hf.toFinset, hf.coe_toFinset.symm ▸ ht.1, ?_⟩

Premises used: Eq.rec, Set.Finite.coe_toFinset, And.left, Set.Finite.toFinset, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
refine : ⋃ g ∈ hf.toFinset (s := t), (↑g : G) • (↑D : Set G) = (↑H : Set G)
⊢ ∃ (t : Finset ↥H),
    IsComplement (↑t : Set ↥H) (↑(D.subgroupOf H) : Set ↥H) ∧ ⋃ g ∈ t, (↑g : G) • (↑D : Set G) = (↑H : Set G)

Tactic:
refine ⟨hf.toFinset, hf.coe_toFinset.symm ▸ ht.1, ?_⟩
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
h : ∀ (x : G), Membership.mem (γ := Set G) (⋃ g ∈ hf.toFinset (s := t), (↑g : G) • (↑D : Set G)) x ↔ x ∈ (↑H : Set G)
⊢ ⋃ g ∈ hf.toFinset (s := t), (↑g : G) • (↑D : Set G) = (↑H : Set G)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
x : G
this : (∃ y ∈ t, ∃ d ∈ D, (↑y : G) * d = x) ↔ x ∈ H
⊢ Membership.mem (γ := Set G) (⋃ g ∈ hf.toFinset (s := t), (↑g : G) • (↑D : Set G)) x ↔ x ∈ (↑H : Set G)

Tactic:
simpa using this
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
x : G
h : (∃ y ∈ t, ∃ d ∈ D, (↑y : G) * d = x) ↔ x ∈ H
⊢ Membership.mem (γ := Set G) (⋃ g ∈ hf.toFinset (s := t), (↑g : G) • (↑D : Set G)) x ↔ x ∈ (↑H : Set G)

Tactic:
suffices (∃ y ∈ t, ∃ d ∈ D, y * d = x) ↔ x ∈ H by simpa using this
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
x : G
h : (∃ y ∈ t, ∃ d ∈ D, (↑y : G) * d = x) → x ∈ H
h₁ : x ∈ H → ∃ y ∈ t, ∃ d ∈ D, (↑y : G) * d = x
⊢ (∃ y ∈ t, ∃ d ∈ D, (↑y : G) * d = x) ↔ x ∈ H

Tactic:
constructor
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
y : G
hy : y ∈ H
d : G
h : d ∈ D
⊢ (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) y hy) : G) * d ∈ H

Tactic:
H.mul_mem hy (hD_le_H h)

Premises used: Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
y : G
hy : y ∈ H
d : G
h : d ∈ D
⊢ (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) y hy) : G) * d ∈ H

Tactic:
exact H.mul_mem hy (hD_le_H h)

Premises used: Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
x : G
hx : x ∈ H
⊢ ∃ y ∈ t, ∃ d ∈ D, (↑y : G) * d = x

Tactic:
⟨_, (ht.1.toLeftFun ⟨x, hx⟩).2, _,
      ht.1.inv_toLeftFun_mul_mem ⟨x, hx⟩, mul_inv_cancel_left _ _⟩

Premises used: Subtype.mk, And.left, Subgroup.IsComplement.inv_toLeftFun_mul_mem, And.intro, Exists.intro, mul_inv_cancel_left, Subgroup.IsComplement.toLeftFun, Subtype.property
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
D H : Subgroup G
inst_1 : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t (↑(D.subgroupOf H) : Set ↥H) ∧ 1 ∈ t
hf : t.Finite
x : G
hx : x ∈ H
⊢ ∃ y ∈ t, ∃ d ∈ D, (↑y : G) * d = x

Tactic:
exact ⟨_, (ht.1.toLeftFun ⟨x, hx⟩).2, _,
      ht.1.inv_toLeftFun_mul_mem ⟨x, hx⟩, mul_inv_cancel_left _ _⟩
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
⊢ Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑H : Set G)) Set.univ ↔
    Set.SurjOn.{u_2, u_1} (β := G ⧸ H) (fun (x : ι) ↦ (↑(g x) : G ⧸ H)) (↑s : Set ι) Set.univ

Tactic:
simp [Set.eq_univ_iff_forall, mem_leftCoset_iff, Set.SurjOn,
    QuotientGroup.forall_mk, QuotientGroup.eq]

Premises used: mem_leftCoset_iff, Set.eq_univ_iff_forall, Set.SurjOn, QuotientGroup.eq, QuotientGroup.forall_mk
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑H : Set G)) Set.univ
⊢ Set.SurjOn.{u_2, u_1} (β := G ⧸ H) (fun (x : ι) ↦ (↑(g x) : G ⧸ H)) (↑s : Set ι) Set.univ

Tactic:
simp_rw [leftCoset_cover_const_iff_surjOn] at hcovers

Premises used: Subgroup.leftCoset_cover_const_iff_surjOn
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Set.SurjOn.{u_2, u_1} (β := G ⧸ H) (fun (x : ι) ↦ (↑(g x) : G ⧸ H)) (↑s : Set ι) Set.univ
⊢ Finite.{u_1 + 1} (G ⧸ H)

Tactic:
have := Set.finite_univ_iff.mp <| Set.Finite.of_surjOn _ hcovers s.finite_toSet
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Set.SurjOn.{u_2, u_1} (β := G ⧸ H) (fun (x : ι) ↦ (↑(g x) : G ⧸ H)) (↑s : Set ι) Set.univ
this : Finite.{u_1 + 1} (G ⧸ H)
⊢ H.FiniteIndex

Tactic:
H.finiteIndex_of_finite_quotient

Premises used: Subgroup.finiteIndex_of_finite_quotient
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Set.SurjOn.{u_2, u_1} (β := G ⧸ H) (fun (x : ι) ↦ (↑(g x) : G ⧸ H)) (↑s : Set ι) Set.univ
this : Finite.{u_1 + 1} (G ⧸ H)
⊢ H.FiniteIndex

Tactic:
exact H.finiteIndex_of_finite_quotient

Premises used: Subgroup.finiteIndex_of_finite_quotient
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑H : Set G)) Set.univ
h : H.index = 0
⊢ H.index ≤ s.card

Tactic:
h ▸ s.card.zero_le

Premises used: Nat.zero_le, Eq.rec, Finset.card, Eq.symm
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑H : Set G)) Set.univ
h : H.index = 0
⊢ H.index ≤ s.card

Tactic:
exact h ▸ s.card.zero_le
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑H : Set G)) Set.univ
h : H.index > 0
⊢ Function.Surjective.{u_2 + 1, u_1 + 1} (α := (↑(↑s : Set ι) : Type u_2)) (β := G ⧸ H)
    ((↑s : Set ι).restrict (π := fun (a : ι) ↦ G ⧸ H) fun (x : ι) ↦ (↑(g x) : G ⧸ H))

Tactic:
rw [leftCoset_cover_const_iff_surjOn, Set.surjOn_iff_surjective] at hcovers

Premises used: Set.surjOn_iff_surjective, Subgroup.leftCoset_cover_const_iff_surjOn
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑H : Set G)) Set.univ
h : H.index > 0
hcovers₁ :
  Function.Surjective.{u_2 + 1, u_1 + 1} (α := (↑(↑s : Set ι) : Type u_2)) (β := G ⧸ H)
    ((↑s : Set ι).restrict (π := fun (a : ι) ↦ G ⧸ H) fun (x : ι) ↦ (↑(g x) : G ⧸ H))
⊢ H.index > 0

Tactic:
rw [leftCoset_cover_const_iff_surjOn, Set.surjOn_iff_surjective] at hcovers

Premises used: Set.surjOn_iff_surjective, Subgroup.leftCoset_cover_const_iff_surjOn
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers :
  Function.Surjective.{u_2 + 1, u_1 + 1} (α := (↑(↑s : Set ι) : Type u_2)) (β := G ⧸ H)
    ((↑s : Set ι).restrict (π := fun (a : ι) ↦ G ⧸ H) fun (x : ι) ↦ (↑(g x) : G ⧸ H))
h : H.index > 0
⊢ H.index ≤ s.card

Tactic:
(Nat.card_le_card_of_surjective _ hcovers).trans_eq (Nat.card_eq_finsetCard _)

Premises used: LE.le.trans_eq, Nat.card_eq_finsetCard, Nat.card_le_card_of_surjective, Subgroup.index
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers :
  Function.Surjective.{u_2 + 1, u_1 + 1} (α := (↑(↑s : Set ι) : Type u_2)) (β := G ⧸ H)
    ((↑s : Set ι).restrict (π := fun (a : ι) ↦ G ⧸ H) fun (x : ι) ↦ (↑(g x) : G ⧸ H))
h : H.index > 0
⊢ H.index ≤ s.card

Tactic:
exact (Nat.card_le_card_of_surjective _ hcovers).trans_eq (Nat.card_eq_finsetCard _)

Premises used: LE.le.trans_eq, Nat.card_eq_finsetCard, Nat.card_le_card_of_surjective
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑H : Set G)) Set.univ
⊢ H.index = 0 ∨ H.index > 0

Tactic:
cases H.index.eq_zero_or_pos with
  | inl h => exact h ▸ s.card.zero_le
  | inr h =>
    rw [leftCoset_cover_const_iff_surjOn, Set.surjOn_iff_surjective] at hcovers
    exact (Nat.card_le_card_of_surjective _ hcovers).trans_eq (Nat.card_eq_finsetCard _)

Premises used: Set.surjOn_iff_surjective, Subgroup.leftCoset_cover_const_iff_surjOn, Subgroup.index, Nat.eq_zero_or_pos
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑H : Set G)) Set.univ
hind : H.index = s.card
h : H.index = 0
⊢ s = ∅

Tactic:
rw [hind, Finset.card_eq_zero] at h

Premises used: Finset.card_eq_zero
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑H : Set G)) Set.univ
hind : H.index = s.card
h : s = ∅
⊢ Eq.{u_1 + 1} (α := Set G) ∅ Set.univ

Tactic:
rw [h, ← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers

Premises used: Finset.coe_empty, Finset.set_biUnion_coe, Set.biUnion_empty