awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a : α
ha : a ∈ s
⊢ ∀ (x : α), x ∈ a • (↑s : Set α) ↔ x ∈ (↑s : Set α)

Tactic:
simp [mem_leftCoset_iff, mul_mem_cancel_left (s.inv_mem ha)]

Premises used: mem_leftCoset_iff, Subgroup.inv_mem, mul_mem_cancel_left
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a : α
ha : a ∈ s
b : α
⊢ b ∈ op a • (↑s : Set α) ↔ b ∈ (↑s : Set α)

Tactic:
simp [mem_rightCoset_iff, mul_mem_cancel_right (s.inv_mem ha)]

Premises used: Subgroup.inv_mem, mem_rightCoset_iff, mul_mem_cancel_right
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a : α
⊢ MulAction.orbit (↥s) a = op a • (↑s : Set α)

Tactic:
Set.ext fun _b => ⟨fun ⟨c, d⟩ => ⟨c, c.2, d⟩, fun ⟨c, d, e⟩ => ⟨⟨c, d⟩, e⟩⟩

Premises used: Set.ext, _private.0.orbit_subgroup_eq_rightCoset.match_2, Membership.mem, Subtype, Subtype.mk, MulAction.orbit, SetLike.coe, And.intro, Iff.intro, Exists.intro, _private.0.orbit_subgroup_eq_rightCoset.match_1, HSMul.hSMul, Subtype.val, Subtype.property, MulOpposite.op
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
a : α
ha : a ∈ s
⊢ MulAction.orbit (↥s) a = (↑s : Set α)

Tactic:
(orbit_subgroup_eq_rightCoset s a).trans (rightCoset_mem_rightCoset s ha)

Premises used: rightCoset_mem_rightCoset, orbit_subgroup_eq_rightCoset, Eq.trans
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ MulAction.orbit (↥s) 1 = (↑s : Set α)

Tactic:
orbit_subgroup_eq_self_of_mem s s.one_mem

Premises used: orbit_subgroup_eq_self_of_mem, Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
N : s.Normal
g a : α
⊢ a ∈ g • (↑s : Set α) ↔ a ∈ op g • (↑s : Set α)

Tactic:
simp [mem_leftCoset_iff, mem_rightCoset_iff, N.mem_comm_iff]

Premises used: mem_leftCoset_iff, Subgroup.Normal.mem_comm_iff, mem_rightCoset_iff
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
h : ∀ (g : α), g • (↑s : Set α) = op g • (↑s : Set α)
a : α
ha : a ∈ s
g : α
rw : g * a ∈ g • (↑s : Set α)
⊢ g * a * g⁻¹ ∈ (↑s : Set α)

Tactic:
rw [← mem_rightCoset_iff, ← h]

Premises used: mem_rightCoset_iff
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
h : ∀ (g : α), g • (↑s : Set α) = op g • (↑s : Set α)
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ g • (↑s : Set α)

Tactic:
mem_leftCoset g ha

Premises used: mem_leftCoset
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
h : ∀ (g : α), g • (↑s : Set α) = op g • (↑s : Set α)
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ g • (↑s : Set α)

Tactic:
exact mem_leftCoset g ha

Premises used: mem_leftCoset
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ s.Normal ↔ ∀ (g : α), g • (↑s : Set α) = op g • (↑s : Set α)

Tactic:
⟨@eq_cosets_of_normal _ _ s, normal_of_eq_cosets s⟩

Premises used: Iff.intro, eq_cosets_of_normal, normal_of_eq_cosets
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
rw : (∀ (x_1 : α), x_1 ∈ x • (↑s : Set α) ↔ x_1 ∈ y • (↑s : Set α)) ↔ x⁻¹ * y ∈ s
⊢ x • (↑s : Set α) = y • (↑s : Set α) ↔ x⁻¹ * y ∈ s

Tactic:
rw [Set.ext_iff]

Premises used: Set.ext_iff
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
simp_rw : (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) ↔ x⁻¹ * y ∈ s
⊢ (∀ (x_1 : α), x_1 ∈ x • (↑s : Set α) ↔ x_1 ∈ y • (↑s : Set α)) ↔ x⁻¹ * y ∈ s

Tactic:
simp_rw [mem_leftCoset_iff, SetLike.mem_coe]

Premises used: mem_leftCoset_iff, SetLike.mem_coe
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
mp : (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ s
mpr : x⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) ↔ x⁻¹ * y ∈ s

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
mp : y⁻¹ * y ∈ s
⊢ x⁻¹ * y ∈ s

Tactic:
apply (h y).mpr

Premises used: Iff.mpr
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
mp : 1 ∈ s
⊢ y⁻¹ * y ∈ s

Tactic:
rw [inv_mul_cancel]

Premises used: inv_mul_cancel
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ 1 ∈ s

Tactic:
s.one_mem

Premises used: Set.Mem, Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ 1 ∈ s

Tactic:
exact s.one_mem

Premises used: Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
mpr : x⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
⊢ x⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s

Tactic:
rw [← mul_inv_cancel_right x⁻¹ y]

Premises used: mul_inv_cancel_right, Inv.inv
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
mpr : x⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s
⊢ x⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s

Tactic:
s.mul_mem_cancel_left h

Premises used: Set.Mem, Subgroup.mul_mem_cancel_left
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s

Tactic:
exact s.mul_mem_cancel_left h

Premises used: Subgroup.mul_mem_cancel_left
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
rw : (∀ (x_1 : α), x_1 ∈ op x • (↑s : Set α) ↔ x_1 ∈ op y • (↑s : Set α)) ↔ y * x⁻¹ ∈ s
⊢ op x • (↑s : Set α) = op y • (↑s : Set α) ↔ y * x⁻¹ ∈ s

Tactic:
rw [Set.ext_iff]

Premises used: Set.ext_iff
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
simp_rw : (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s
⊢ (∀ (x_1 : α), x_1 ∈ op x • (↑s : Set α) ↔ x_1 ∈ op y • (↑s : Set α)) ↔ y * x⁻¹ ∈ s

Tactic:
simp_rw [mem_rightCoset_iff, SetLike.mem_coe]

Premises used: SetLike.mem_coe, mem_rightCoset_iff
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
mp : (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ s
mpr : y * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
mp : y * y⁻¹ ∈ s
⊢ y * x⁻¹ ∈ s

Tactic:
apply (h y).mpr

Premises used: Iff.mpr
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
mp : 1 ∈ s
⊢ y * y⁻¹ ∈ s

Tactic:
rw [mul_inv_cancel]

Premises used: mul_inv_cancel
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ 1 ∈ s

Tactic:
s.one_mem

Premises used: Set.Mem, Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ 1 ∈ s

Tactic:
exact s.one_mem

Premises used: Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
mpr : z * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s
⊢ z * x⁻¹ ∈ s ↔ z * y⁻¹ ∈ s

Tactic:
rw [← inv_mul_cancel_left y x⁻¹]

Premises used: inv_mul_cancel_left, Inv.inv
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
mpr : z * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s
⊢ z * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s

Tactic:
s.mul_mem_cancel_right h

Premises used: Set.Mem, Subgroup.mul_mem_cancel_right
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s

Tactic:
exact s.mul_mem_cancel_right h

Premises used: Subgroup.mul_mem_cancel_right
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
h : ∀ (x x_1 : α), (leftRel s : α → α → Prop) x x_1 ↔ LeftCosetEquivalence (↑s : Set α) x x_1
⊢ (⇑(leftRel s) : α → α → Prop) = LeftCosetEquivalence (↑s : Set α)

Tactic:
ext
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x x_1 : α
h : (fun (x y : α) ↦ x⁻¹ * y ∈ s) x x_1 ↔ LeftCosetEquivalence (↑s : Set α) x x_1
⊢ (leftRel s : α → α → Prop) x x_1 ↔ LeftCosetEquivalence (↑s : Set α) x x_1

Tactic:
rw [leftRel_eq]

Premises used: QuotientGroup.leftRel_eq
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x x_1 : α
⊢ (fun (x y : α) ↦ x⁻¹ * y ∈ s) x x_1 ↔ LeftCosetEquivalence (↑s : Set α) x x_1

Tactic:
(leftCoset_eq_iff s).symm

Premises used: LeftCosetEquivalence, leftCoset_eq_iff, Iff.symm
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x x_1 : α
⊢ (fun (x y : α) ↦ x⁻¹ * y ∈ s) x x_1 ↔ LeftCosetEquivalence (↑s : Set α) x x_1

Tactic:
exact (leftCoset_eq_iff s).symm

Premises used: leftCoset_eq_iff, Iff.symm
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
β : Type u_2
inst_1 : Group β
s' : Subgroup β
⊢ leftRel (s.prod s') = (leftRel s).prod (leftRel s')

Tactic:
Setoid.ext fun x y ↦ ?_

Premises used: Setoid.ext
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
β : Type u_2
inst_1 : Group β
s' : Subgroup β
refine :
  ∀ (x y : α × β),
    (leftRel (s.prod s') : α × β → α × β → Prop) x y ↔ ((leftRel s).prod (leftRel s') : α × β → α × β → Prop) x y
⊢ leftRel (s.prod s') = (leftRel s).prod (leftRel s')

Tactic:
refine Setoid.ext fun x y ↦ ?_

Premises used: Setoid.ext
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
β : Type u_2
inst_1 : Group β
s' : Subgroup β
x y : α × β
simp_rw : x⁻¹ * y ∈ s.prod s' ↔ x.1⁻¹ * y.1 ∈ s ∧ x.2⁻¹ * y.2 ∈ s'
⊢ (leftRel (s.prod s') : α × β → α × β → Prop) x y ↔
    (leftRel s : α → α → Prop) x.1 y.1 ∧ (leftRel s' : β → β → Prop) x.2 y.2

Tactic:
simp_rw [leftRel_apply]

Premises used: QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
β : Type u_2
inst_1 : Group β
s' : Subgroup β
x y : α × β
⊢ x⁻¹ * y ∈ s.prod s' ↔ x.1⁻¹ * y.1 ∈ s ∧ x.2⁻¹ * y.2 ∈ s'

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
⊢ leftRel (Subgroup.pi (f := β) univ s') = piSetoid (α := β)

Tactic:
Setoid.ext fun x y ↦ ?_

Premises used: Setoid.ext
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
refine :
  ∀ (x y : (i : ι) → β i),
    (leftRel (Subgroup.pi univ s') : ((i : ι) → β i) → ((i : ι) → β i) → Prop) x y ↔
      (piSetoid : ((i : ι) → β i) → ((i : ι) → β i) → Prop) x y
⊢ leftRel (Subgroup.pi (f := β) univ s') = piSetoid (α := β)

Tactic:
refine Setoid.ext fun x y ↦ ?_

Premises used: Setoid.ext
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
x y : (i : ι) → β i
⊢ (leftRel (Subgroup.pi univ s') : ((i : ι) → β i) → ((i : ι) → β i) → Prop) x y ↔
    (piSetoid : ((i : ι) → β i) → ((i : ι) → β i) → Prop) x y

Tactic:
simp [Setoid.piSetoid_apply, leftRel_apply, Subgroup.mem_pi]

Premises used: Subgroup.mem_pi, Setoid.piSetoid_apply, QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
h : ∀ (x x_1 : α), (rightRel s : α → α → Prop) x x_1 ↔ RightCosetEquivalence (↑s : Set α) x x_1
⊢ (⇑(rightRel s) : α → α → Prop) = RightCosetEquivalence (↑s : Set α)

Tactic:
ext
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x x_1 : α
h : (fun (x y : α) ↦ y * x⁻¹ ∈ s) x x_1 ↔ RightCosetEquivalence (↑s : Set α) x x_1
⊢ (rightRel s : α → α → Prop) x x_1 ↔ RightCosetEquivalence (↑s : Set α) x x_1

Tactic:
rw [rightRel_eq]

Premises used: QuotientGroup.rightRel_eq
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x x_1 : α
⊢ (fun (x y : α) ↦ y * x⁻¹ ∈ s) x x_1 ↔ RightCosetEquivalence (↑s : Set α) x x_1

Tactic:
(rightCoset_eq_iff s).symm

Premises used: rightCoset_eq_iff, RightCosetEquivalence, Iff.symm
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x x_1 : α
⊢ (fun (x y : α) ↦ y * x⁻¹ ∈ s) x x_1 ↔ RightCosetEquivalence (↑s : Set α) x x_1

Tactic:
exact (rightCoset_eq_iff s).symm

Premises used: rightCoset_eq_iff, Iff.symm
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
β : Type u_2
inst_1 : Group β
s' : Subgroup β
⊢ rightRel (s.prod s') = (rightRel s).prod (rightRel s')

Tactic:
Setoid.ext fun x y ↦ ?_

Premises used: Setoid.ext
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
β : Type u_2
inst_1 : Group β
s' : Subgroup β
refine :
  ∀ (x y : α × β),
    (rightRel (s.prod s') : α × β → α × β → Prop) x y ↔ ((rightRel s).prod (rightRel s') : α × β → α × β → Prop) x y
⊢ rightRel (s.prod s') = (rightRel s).prod (rightRel s')

Tactic:
refine Setoid.ext fun x y ↦ ?_

Premises used: Setoid.ext
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
β : Type u_2
inst_1 : Group β
s' : Subgroup β
x y : α × β
simp_rw : y * x⁻¹ ∈ s.prod s' ↔ y.1 * x.1⁻¹ ∈ s ∧ y.2 * x.2⁻¹ ∈ s'
⊢ (rightRel (s.prod s') : α × β → α × β → Prop) x y ↔
    (rightRel s : α → α → Prop) x.1 y.1 ∧ (rightRel s' : β → β → Prop) x.2 y.2

Tactic:
simp_rw [rightRel_apply]

Premises used: QuotientGroup.rightRel_apply
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
β : Type u_2
inst_1 : Group β
s' : Subgroup β
x y : α × β
⊢ y * x⁻¹ ∈ s.prod s' ↔ y.1 * x.1⁻¹ ∈ s ∧ y.2 * x.2⁻¹ ∈ s'

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
⊢ rightRel (Subgroup.pi (f := β) univ s') = piSetoid (α := β)

Tactic:
Setoid.ext fun x y ↦ ?_

Premises used: Setoid.ext
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
refine :
  ∀ (x y : (i : ι) → β i),
    (rightRel (Subgroup.pi univ s') : ((i : ι) → β i) → ((i : ι) → β i) → Prop) x y ↔
      (piSetoid : ((i : ι) → β i) → ((i : ι) → β i) → Prop) x y
⊢ rightRel (Subgroup.pi (f := β) univ s') = piSetoid (α := β)

Tactic:
refine Setoid.ext fun x y ↦ ?_

Premises used: Setoid.ext
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
x y : (i : ι) → β i
⊢ (rightRel (Subgroup.pi univ s') : ((i : ι) → β i) → ((i : ι) → β i) → Prop) x y ↔
    (piSetoid : ((i : ι) → β i) → ((i : ι) → β i) → Prop) x y

Tactic:
simp [Setoid.piSetoid_apply, rightRel_apply, Subgroup.mem_pi]

Premises used: Subgroup.mem_pi, Setoid.piSetoid_apply, QuotientGroup.rightRel_apply
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ StrictMono (β := Subgroup ↥s × Set (α ⧸ s)) fun (t : Subgroup α) ↦ (Subgroup.comap s.subtype t, mk '' (↑t : Set α))

Tactic:
fun t₁ t₂ h ↦ ⟨⟨Subgroup.comap_mono h.1, Set.image_mono h.1⟩,
    mt (fun ⟨le1, le2⟩ a ha ↦ ?_) h.2⟩

Premises used: StrictMono, Set.image_mono, mt, And.right, And.left, And.intro, Subgroup.comap_mono
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
refine :
  ∀ (t₁ t₂ : Subgroup α) (h : t₁ < t₂),
    LE.le.{u_1} (α := Subgroup ↥s × Set (α ⧸ s))
        ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂)
        ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁) →
      ∀ (a : α) (ha : a ∈ (↑t₂ : Set α))
        (le1 :
          LE.le.{u_1} (α := Subgroup ↥s)
            ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s)))
                t₂).1
            ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s)))
                t₁).1)
        (le2 :
          LE.le.{u_1} (α := Set (α ⧸ s))
            ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s)))
                t₂).2
            ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s)))
                t₁).2),
        a ∈ (↑t₁ : Set α)
⊢ StrictMono (β := Subgroup ↥s × Set (α ⧸ s)) fun (t : Subgroup α) ↦ (Subgroup.comap s.subtype t, mk '' (↑t : Set α))

Tactic:
refine fun t₁ t₂ h ↦ ⟨⟨Subgroup.comap_mono h.1, Set.image_mono h.1⟩,
    mt (fun ⟨le1, le2⟩ a ha ↦ ?_) h.2⟩
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
h_1 :
  LE.le.{u_1} (α := Subgroup ↥s × Set (α ⧸ s))
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂)
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁)
a : α
ha : a ∈ (↑t₂ : Set α)
le1 :
  LE.le.{u_1} (α := Subgroup ↥s)
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂).1
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁).1
le2 :
  LE.le.{u_1} (α := Set (α ⧸ s))
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂).2
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁).2
obtain : ∀ (a' : α) (h' : a' ∈ (↑t₁ : Set α)) (eq : Eq (α := α ⧸ s) (↑a' : α ⧸ s) (↑a : α ⧸ s)), a ∈ (↑t₁ : Set α)
⊢ a ∈ (↑t₁ : Set α)

Tactic:
obtain ⟨a', h', eq⟩ := le2 ⟨_, ha, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
h_1 :
  LE.le.{u_1} (α := Subgroup ↥s × Set (α ⧸ s))
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂)
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁)
a : α
ha : a ∈ (↑t₂ : Set α)
le1 :
  LE.le.{u_1} (α := Subgroup ↥s)
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂).1
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁).1
le2 :
  LE.le.{u_1} (α := Set (α ⧸ s))
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂).2
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁).2
a' : α
h' : a' ∈ (↑t₁ : Set α)
eq : Eq (α := α ⧸ s) (↑a' : α ⧸ s) (↑a : α ⧸ s)
⊢ HMul.hMul (β := α) a' ((s.subtype : (a : ↥s) → α) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (a'⁻¹ * a) ⋯) : α) ∈ t₁

Tactic:
t₁.mul_mem h' (@le1 ⟨_, QuotientGroup.eq.1 eq⟩ <| t₂.mul_mem (t₂.inv_mem <| h.1 h') ha)

Premises used: Subgroup.inv_mem, And.left, Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
h_1 :
  LE.le.{u_1} (α := Subgroup ↥s × Set (α ⧸ s))
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂)
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁)
a : α
ha : a ∈ (↑t₂ : Set α)
le1 :
  LE.le.{u_1} (α := Subgroup ↥s)
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂).1
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁).1
le2 :
  LE.le.{u_1} (α := Set (α ⧸ s))
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂).2
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁).2
a' : α
h' : a' ∈ (↑t₁ : Set α)
eq : Eq (α := α ⧸ s) (↑a' : α ⧸ s) (↑a : α ⧸ s)
h₁ : HMul.hMul (β := α) a' ((s.subtype : (a : ↥s) → α) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (a'⁻¹ * a) ⋯) : α) = a
⊢ a ∈ (↑t₁ : Set α)

Tactic:
convert! ← t₁.mul_mem h' (@le1 ⟨_, QuotientGroup.eq.1 eq⟩ <| t₂.mul_mem (t₂.inv_mem <| h.1 h') ha)

Premises used: Subgroup.inv_mem, And.left, Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t₁ t₂ : Subgroup α
h : t₁ < t₂
h_1 :
  LE.le.{u_1} (α := Subgroup ↥s × Set (α ⧸ s))
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂)
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁)
a : α
ha : a ∈ (↑t₂ : Set α)
le1 :
  LE.le.{u_1} (α := Subgroup ↥s)
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂).1
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁).1
le2 :
  LE.le.{u_1} (α := Set (α ⧸ s))
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₂).2
    ((fun (t : Subgroup α) ↦ ((Subgroup.comap s.subtype t, mk '' (↑t : Set α)) : Subgroup ↥s × Set (α ⧸ s))) t₁).2
a' : α
h' : a' ∈ (↑t₁ : Set α)
eq : Eq (α := α ⧸ s) (↑a' : α ⧸ s) (↑a : α ⧸ s)
⊢ HMul.hMul (β := α) a' ((s.subtype : (a : ↥s) → α) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (a'⁻¹ * a) ⋯) : α) = a

Tactic:
apply mul_inv_cancel_left

Premises used: mul_inv_cancel_left
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g z : α
rw : Membership.mem (γ := Set α) {x : α | Eq (α := α ⧸ s) (↑x : α ⧸ s) (↑g : α ⧸ s)} z ↔ g⁻¹ * z ∈ (↑s : Set α)
rw₁ : Eq (α := α ⧸ s) (↑z : α ⧸ s) (↑g : α ⧸ s) ↔ g⁻¹ * z ∈ (↑s : Set α)
rw₂ : Eq (α := α ⧸ s) (↑g : α ⧸ s) (↑z : α ⧸ s) ↔ g⁻¹ * z ∈ (↑s : Set α)
rw₃ : g⁻¹ * z ∈ s ↔ g⁻¹ * z ∈ (↑s : Set α)
rw₄ rw₅ : g⁻¹ * z ∈ s ↔ g⁻¹ * z ∈ s
⊢ Membership.mem (γ := Set α) {x : α | Eq (α := α ⧸ s) (↑x : α ⧸ s) (↑g : α ⧸ s)} z ↔ z ∈ g • (↑s : Set α)

Tactic:
rw [mem_leftCoset_iff, Set.mem_setOf_eq, eq_comm, QuotientGroup.eq, SetLike.mem_coe]

Premises used: mem_leftCoset_iff, QuotientGroup.eq, Set.mem_setOf_eq, eq_comm, SetLike.mem_coe
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x : α
h : ∀ (x_1 : α), x_1 ∈ orbitRel.Quotient.orbit (G := ↥s.op) (↑x : α ⧸ s) ↔ x_1 ∈ x • (↑s : Set α)
⊢ orbitRel.Quotient.orbit (G := ↥s.op) (↑x : α ⧸ s) = x • (↑s : Set α)

Tactic:
ext
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x x_1 : α
h : Eq (α := Quotient (orbitRel (↥s.op) α)) (Quotient.mk'' x_1) (↑x : α ⧸ s) ↔ x_1 ∈ x • (↑s : Set α)
⊢ x_1 ∈ orbitRel.Quotient.orbit (G := ↥s.op) (↑x : α ⧸ s) ↔ x_1 ∈ x • (↑s : Set α)

Tactic:
rw [orbitRel.Quotient.mem_orbit]

Premises used: MulAction.orbitRel.Quotient.mem_orbit