DoubleCoset.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

40 declarations, 0 contain sorry, 0 declared as axioms

Double Coset

Material destined for Mathlib.

Imports (4)

Imported by 5 files

theorem DoubleCoset.isOpen_doubleCoset line 21 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, ContinuousMul, Subgroup, IsOpen, DoubleCoset.Quotient, DoubleCoset.doubleCoset, Quotient.out, DoubleCoset.setoid
Proof uses: id, IsOpen.mul_left, HMul.hMul, Set, Set.mul, Singleton.singleton
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma DoubleCoset.mk_surjective line 26 source
standard axioms: propext what this means
Statement uses: Group, Subgroup, Function.Surjective, DoubleCoset.Quotient, DoubleCoset.mk
Proof uses: Quotient.mk_surjective, DoubleCoset.setoid
4 instances, coercions and auxiliary constants left out.
theorem DoubleCoset.isOpen_doubleCoset_rightrel_mk line 29 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, TopologicalSpace, ContinuousMul, Subgroup, IsOpen, DoubleCoset.Quotient, Quot, QuotientGroup.rightRel, Set.image, Quot.mk, DoubleCoset.doubleCoset, Quotient.out, DoubleCoset.setoid
Proof uses: IsOpenQuotientMap.isOpenMap, QuotientGroup.isOpenQuotientMap_rightrel_mk, DoubleCoset.isOpen_doubleCoset
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def DoubleCoset.map Mapping double cosets across MonoidHoms line 36 source
Source documentation
Mapping double cosets across MonoidHoms.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, MonoidHom, LE.le, Subgroup.comap, DoubleCoset.Quotient
Proof uses: Quotient.map, DoubleCoset.setoid, HasEquiv.Equiv
22 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def DoubleCoset.map {G₁ G₂ : Type*} [Group G₁] [Group G₂] (H₁ K₁ : Subgroup G₁)
    (H₂ K₂ : Subgroup G₂) (e : G₁ →* G₂) (eH : H₁ ≤ H₂.comap e) (eK : K₁ ≤ K₂.comap e) :
    DoubleCoset.Quotient (G := G₁) H₁ K₁ → DoubleCoset.Quotient (G := G₂) H₂ K₂ :=
…
```
lemma DoubleCoset.map_mk line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, MonoidHom, LE.le, Subgroup.comap, Eq, DoubleCoset.Quotient, DoubleCoset.map, DoubleCoset.mk
Proof uses: rfl
20 instances, coercions and auxiliary constants left out.
def DoubleCoset.quotientEquiv Mapping double cosets across MulEquivs line 50 source
Source documentation
Mapping double cosets across MulEquivs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Set, MulEquiv, Eq, Set.preimage, Equiv, DoubleCoset.Quotient
Proof uses: Quotient.congr, DoubleCoset.setoid
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def DoubleCoset.quotientEquiv {G₁ G₂ : Type*} [Group G₁] [Group G₂] (H₁ K₁ : Set G₁)
    (H₂ K₂ : Set G₂) (e : G₁ ≃* G₂) (eH : e ⁻¹' H₂ = H₁) (eK : e ⁻¹' K₂ = K₁) :
    DoubleCoset.Quotient H₁ K₁ ≃ DoubleCoset.Quotient H₂ K₂ :=
…
```
lemma DoubleCoset.quotientEquiv_mk line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, MulEquiv, Eq, Set, Set.preimage, DoubleCoset.Quotient, Equiv, DoubleCoset.quotientEquiv, DoubleCoset.mk
Proof uses: rfl
22 instances, coercions and auxiliary constants left out.
lemma Set.mul_right_singleton_bijective line 64 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Function.Bijective, Set, HMul.hMul, Set.mul, Singleton.singleton
Proof uses: Eq.mpr, HSMul.hSMul, MulOpposite, Set.mulActionSet, MulOpposite.op, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, funext, Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Inv.inv, True, congr and 9 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def DoubleCoset.mulRightEquiv The isomorphism H\G/K ≃ H\G/g⁻¹Kg sending HaK to H(ag)(g⁻¹Kg) line 71 source
Source documentation
The isomorphism H\G/K ≃ H\G/g⁻¹Kg sending HaK to H(ag)(g⁻¹Kg).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Set, Eq, HSMul.hSMul, ConjAct, Set.smulSet, MulEquiv, ConjAct.toConjAct, Inv.inv, Equiv, DoubleCoset.Quotient
Proof uses: Quotient.congr, DoubleCoset.setoid, Equiv.mulRight
31 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
def DoubleCoset.mulRightEquiv {G : Type*} [Group G] (H K gK : Set G) (g : G)
    (hgK : gK = ConjAct.toConjAct g⁻¹ • K) :
    DoubleCoset.Quotient H K ≃ DoubleCoset.Quotient H gK :=
…
```
lemma DoubleCoset.mulRightEquiv_mk line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Eq, Set, HSMul.hSMul, ConjAct, Set.smulSet, MulEquiv, ConjAct.toConjAct, Inv.inv, DoubleCoset.Quotient, Equiv, DoubleCoset.mulRightEquiv, DoubleCoset.mk, HMul.hMul
Proof uses: rfl
37 instances, coercions and auxiliary constants left out.
lemma DoubleCoset.mulRightEquiv_symm_mk line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Eq, Set, HSMul.hSMul, ConjAct, Set.smulSet, MulEquiv, ConjAct.toConjAct, Inv.inv, DoubleCoset.Quotient, Equiv, Equiv.symm, DoubleCoset.mulRightEquiv, DoubleCoset.mk, HMul.hMul
Proof uses: rfl
37 instances, coercions and auxiliary constants left out.
def DoubleCoset.ofLeft The projection G/K → H\G/K line 100 source
Source documentation
The projection G/K → H\G/K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, HasQuotient.Quotient, DoubleCoset.Quotient
Proof uses: Quotient.map, QuotientGroup.leftRel, DoubleCoset.setoid, id
6 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
def DoubleCoset.ofLeft : G ⧸ K → H＼G／K :=
…
```
lemma DoubleCoset.ofLeft_mk line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Eq, DoubleCoset.Quotient, DoubleCoset.ofLeft, DoubleCoset.mk
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
lemma DoubleCoset.ofLeft_surjective line 109 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Function.Surjective, HasQuotient.Quotient, DoubleCoset.Quotient, DoubleCoset.ofLeft
Proof uses: Quotient.map_surjective, QuotientGroup.leftRel, DoubleCoset.setoid, id, Function.surjective_id
6 instances, coercions and auxiliary constants left out.
def DoubleCoset.ofRight The projection H\G → H\G/K line 113 source
Source documentation
The projection H\G → H\G/K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Quotient, QuotientGroup.rightRel, DoubleCoset.Quotient
Proof uses: Quotient.map, DoubleCoset.setoid, id
5 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
def DoubleCoset.ofRight : H﹨G → H＼G／K :=
…
```
lemma DoubleCoset.ofRight_mk'' line 120 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Eq, DoubleCoset.Quotient, DoubleCoset.ofRight, Quotient.mk'', QuotientGroup.rightRel, DoubleCoset.mk
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
lemma DoubleCoset.ofRight_surjective line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Function.Surjective, Quotient, QuotientGroup.rightRel, DoubleCoset.Quotient, DoubleCoset.ofRight
Proof uses: Quotient.map_surjective, DoubleCoset.setoid, id, Function.surjective_id
5 instances, coercions and auxiliary constants left out.
def DoubleCoset.toMapIdPreimage line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, LE.le, HasQuotient.Quotient, Subtype, Membership.mem, Subgroup.subgroupOf, DoubleCoset.Quotient, Set.preimage, DoubleCoset.map, MonoidHom.id, le_rfl, Singleton.singleton, Set, DoubleCoset.mk
Proof uses: Quotient.lift, QuotientGroup.leftRel, Subtype.mk, HMul.hMul
34 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma DoubleCoset.toMapIdPreimage_surjective line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, LE.le, Function.Surjective, HasQuotient.Quotient, Subtype, Membership.mem, Subgroup.subgroupOf, DoubleCoset.Quotient, Set.preimage, DoubleCoset.map, MonoidHom.id, le_rfl, Singleton.singleton, Set, DoubleCoset.mk, DoubleCoset.toMapIdPreimage
Proof uses: Quotient.lift_surjective, QuotientGroup.leftRel, Subtype.mk, HMul.hMul, Eq, Exists, And, Eq.mpr, id, forall_congr, implies_congr, congrArg, funext, Exists.intro, Inv.inv, And.intro, InvMemClass.inv_mem, OfNat.ofNat, of_eq_true, Eq.trans and 19 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def _root_.QuotientGroup.quotientConjActEquivImageMulSingleton line 156 source
lemma DoubleCoset.toMapIdPreimage_preimage Given K₁ ≤ K₂, the map f : H\G/K₁ → H\G/K₂ is surjective line 177 source
Source documentation
Given K₁ ≤ K₂, the map f : H\G/K₁ → H\G/K₂ is surjective. For HgK₂ : H\G/K₂, there is a surjection g : K₂/K₁ → f⁻¹(HgK₂), k ↦ H(gk)K₁. And for H(gk)K₁ : f⁻¹(HgK₂), there set g⁻¹(H(gk)K₁) = { aK₁ ∈ K₂/K₁ | a ∈ (gHg⁻¹ ∩ K₂)xK₁ }

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, LE.le, HasQuotient.Quotient, Subtype, Membership.mem, Subgroup.subgroupOf, Eq, Set, Set.preimage, DoubleCoset.Quotient, DoubleCoset.map, MonoidHom.id, le_rfl, Singleton.singleton, DoubleCoset.mk, DoubleCoset.toMapIdPreimage, HSMul.hSMul, ConjAct, Subgroup.pointwiseMulAction and 4 more
Proof uses: Set.ext, Exists, Iff, QuotientGroup.mk_surjective, Trans.simple, HMul.hMul, of_eq_true, Eq.trans, True, congrFun', congrArg, Quotient.lift, QuotientGroup.leftRel, Subtype.mk, iff_self, Eq.mpr, And, id, congr, funext and 22 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma DoubleCoset.toMapIdPreimage_preimage
    {G : Type*} [Group G] (H K₁ K₂ : Subgroup G) (eK : K₁ ≤ K₂) (g : G) (x) :
    (toMapIdPreimage H K₁ K₂ eK g ⁻¹' {toMapIdPreimage H K₁ K₂ eK g x}) =
      DoubleCoset.ofLeft ((ConjAct.toConjAct g⁻¹ • H).subgroupOf K₂) _ ⁻¹'
        {DoubleCoset.ofLeft ((ConjAct.toConjAct g⁻¹ • H).subgroupOf K₂) _ x} := by
…
```
Mentions: DoubleCoset.toMapIdPreimage, DoubleCoset.ofLeft
theorem Subgroup.conjAct_smul_subgroupOf line 200 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Subgroup, Subtype, Membership.mem, Eq, HSMul.hSMul, ConjAct, Subgroup.pointwiseMulAction, MulEquiv, ConjAct.toConjAct, Subgroup.subgroupOf
Proof uses: Subgroup.ext, of_eq_true, Iff, Eq.trans, HMul.hMul, Inv.inv, True, congr, congrArg, ConjAct.toConjAct_inv_smul', iff_self
45 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma DoubleCoset.ncard_toMapIdPreimage_preimage Given K₁ ≤ K₂, the map f : H\G/K₁ → H\G/K₂ is surjective line 210 source
Source documentation
Given K₁ ≤ K₂, the map f : H\G/K₁ → H\G/K₂ is surjective. For HgK₂ : H\G/K₂, there is a surjection g : K₂/K₁ → f⁻¹(HgK₂), x ↦ H(gx)K₁. This sends [K₂ ⊓ gx⁻¹Hgx : K₁ ⊓ (gx)⁻¹Hgx] elements to H(gx)K₁.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, LE.le, Subtype, Membership.mem, Eq, Nat, Set.ncard, HasQuotient.Quotient, Subgroup.subgroupOf, Set.preimage, DoubleCoset.Quotient, DoubleCoset.map, MonoidHom.id, le_rfl, Singleton.singleton, Set, DoubleCoset.mk, DoubleCoset.toMapIdPreimage, Subgroup.relIndex and 8 more
Proof uses: Eq.mpr, DoubleCoset.ofLeft, id, congrArg, DoubleCoset.toMapIdPreimage_preimage, Nat.card, Set.image, Set.mul, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Eq.rec, Set.ext, Exists, Iff, QuotientGroup.mk_surjective, Subtype.mk, And and 53 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma DoubleCoset.ncard_toMapIdPreimage_preimage
    {G : Type*} [Group G] (H K₁ K₂ : Subgroup G) (eK : K₁ ≤ K₂) (g : G) (x : K₂) :
    Set.ncard (toMapIdPreimage H K₁ K₂ eK g ⁻¹'
      {toMapIdPreimage H K₁ K₂ eK g (QuotientGroup.mk x)}) =
      (K₁).relIndex (K₂ ⊓ ConjAct.toConjAct (g * x)⁻¹ • H) := by
…
```
Mentions: DoubleCoset.toMapIdPreimage
lemma DoubleCoset.sum_filter_map_eq_relIndex_eq_relIndex line 242 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, LE.le, DoubleCoset.Quotient, Fintype, DecidableEq, Subgroup.IsFiniteRelIndex, Eq, Nat, Finset.sum, Finset.filter, DoubleCoset.map, MonoidHom.id, le_rfl, Finset.univ, Quotient.lift, DoubleCoset.setoid, Subgroup.relIndex, Min.min, HSMul.hSMul and 5 more
Proof uses: DoubleCoset.mk, Exists, DoubleCoset.mk_surjective, Trans.simple, Set.preimage, Singleton.singleton, Set, Membership.mem, Classical.propDecidable, Set.ncard, HasQuotient.Quotient, Subtype, Subgroup.subgroupOf, DoubleCoset.toMapIdPreimage, Eq.mpr, Finset, Finset.attach, id, congrArg, Eq.symm and 50 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
lemma DoubleCoset.σ_exists line 278 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Exists, DoubleCoset.Quotient, Subtype, Membership.mem, And, Eq, HMul.hMul, DoubleCoset.mk, OfNat.ofNat
Proof uses: HasQuotient.Quotient, DoubleCoset.ofLeft, Ne, Or, eq_or_ne, of_eq_true, Eq.trans, True, congrArg, funext, implies_congr, eq_self, Eq.refl, Eq.symm, DoubleCoset.ofLeft_surjective, Exists.intro, congr, False, eq_false, and_self and 33 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
def DoubleCoset.σ An arbitrary section of G → H＼G／K line 324 source
Source documentation
An arbitrary section of G → H＼G／K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, DoubleCoset.Quotient
Proof uses: Exists.choose, Exists, Subtype, Membership.mem, And, Eq, HMul.hMul, DoubleCoset.mk, OfNat.ofNat, DoubleCoset.σ_exists
18 instances, coercions and auxiliary constants left out.
```
noncomputable def DoubleCoset.σ (g : H＼G／K) : G := (DoubleCoset.σ_exists H K).choose g
```
Mentions: DoubleCoset.σ_exists
def DoubleCoset.σLeft An arbitrary choice of h such that h * σ(g) * K = g line 327 source
Source documentation
An arbitrary choice of h such that h * σ(g) * K = g.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Subtype, Membership.mem
Proof uses: Exists.choose, Exists, And, Eq, HMul.hMul, DoubleCoset.Quotient, DoubleCoset.mk, OfNat.ofNat, DoubleCoset.σ_exists
19 instances, coercions and auxiliary constants left out.
```
noncomputable def DoubleCoset.σLeft (g : G) : H := (DoubleCoset.σ_exists H K).choose_spec.choose g
```
Mentions: DoubleCoset.σ_exists
def DoubleCoset.σRight An arbitrary choice of k such that h * σ(g) * K = g line 330 source
Source documentation
An arbitrary choice of k such that h * σ(g) * K = g.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Subtype, Membership.mem
Proof uses: Exists.choose, And, Eq, HMul.hMul, Exists, DoubleCoset.Quotient, DoubleCoset.mk, OfNat.ofNat, DoubleCoset.σ_exists
20 instances, coercions and auxiliary constants left out.
```
noncomputable def DoubleCoset.σRight (g : G) : K :=
…
```
lemma DoubleCoset.σ_spec line 333 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Eq, HMul.hMul, Membership.mem, DoubleCoset.σLeft, DoubleCoset.σ, DoubleCoset.mk, DoubleCoset.σRight
Proof uses: Eq.symm, Exists.choose, Subtype, Exists, And, DoubleCoset.Quotient, OfNat.ofNat, DoubleCoset.σ_exists, Exists.choose_spec, And.left
25 instances, coercions and auxiliary constants left out.
lemma DoubleCoset.σLeft_σ line 337 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, DoubleCoset.Quotient, Eq, Subtype, Membership.mem, DoubleCoset.σLeft, DoubleCoset.σ, OfNat.ofNat
Proof uses: And.left, Exists.choose, Exists, And, HMul.hMul, DoubleCoset.mk, DoubleCoset.σ_exists, Exists.choose_spec, And.right
21 instances, coercions and auxiliary constants left out.
lemma DoubleCoset.σRight_σ line 340 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, DoubleCoset.Quotient, Eq, Subtype, Membership.mem, DoubleCoset.σRight, DoubleCoset.σ, OfNat.ofNat
Proof uses: And.left, Exists.choose, And, HMul.hMul, Exists, DoubleCoset.mk, DoubleCoset.σ_exists, Exists.choose_spec, And.right
21 instances, coercions and auxiliary constants left out.
lemma DoubleCoset.σ_one line 343 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Eq, DoubleCoset.σ, DoubleCoset.mk, OfNat.ofNat
Proof uses: And.left, Exists.choose, DoubleCoset.Quotient, Exists, Subtype, Membership.mem, And, HMul.hMul, DoubleCoset.σ_exists, Exists.choose_spec, And.right
21 instances, coercions and auxiliary constants left out.
lemma DoubleCoset.σLeft_mul line 346 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Subtype, Membership.mem, Eq, DoubleCoset.σLeft, HMul.hMul
Proof uses: And.right, Exists.choose, DoubleCoset.Quotient, Exists, And, DoubleCoset.mk, OfNat.ofNat, DoubleCoset.σ_exists, Exists.choose_spec
25 instances, coercions and auxiliary constants left out.
lemma DoubleCoset.σRight_mul line 349 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Subtype, Membership.mem, Eq, DoubleCoset.σRight, HMul.hMul
Proof uses: Subtype.ext, mul_right_injective, DoubleCoset.σLeft, DoubleCoset.σ, DoubleCoset.mk, Eq.mpr, id, congrArg, Eq.trans, congrFun', DoubleCoset.σ_spec, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, HMul, of_eq_true, True and 12 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma DoubleCoset.σLeft_one line 356 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Eq, Subtype, Membership.mem, DoubleCoset.σLeft, OfNat.ofNat
Proof uses: Eq.mpr, DoubleCoset.σ, DoubleCoset.mk, id, congrArg, Eq.symm, DoubleCoset.σ_one, DoubleCoset.σLeft_σ, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma DoubleCoset.σRight_one line 358 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Eq, Subtype, Membership.mem, DoubleCoset.σRight, OfNat.ofNat
Proof uses: Eq.mpr, DoubleCoset.σ, DoubleCoset.mk, id, congrArg, Eq.symm, DoubleCoset.σ_one, DoubleCoset.σRight_σ, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma DoubleCoset.σ_of_mem_left line 360 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Membership.mem, Eq, DoubleCoset.σ, DoubleCoset.mk, OfNat.ofNat
Proof uses: Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, DoubleCoset.Quotient, Iff.mpr, Exists, And, HMul.hMul, DoubleCoset.eq, Exists.intro, And.intro, of_eq_true, Eq.trans, True, congr, congrArg, congrFun' and 4 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma DoubleCoset.σ_of_mem_right line 363 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Membership.mem, Eq, DoubleCoset.σ, DoubleCoset.mk, OfNat.ofNat
Proof uses: Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, DoubleCoset.Quotient, Iff.mpr, Exists, And, HMul.hMul, DoubleCoset.eq, Exists.intro, And.intro, of_eq_true, Eq.trans, True, congr, congrArg, eq_true and 6 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma DoubleCoset.σRight_eq_self line 366 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Subtype, Membership.mem, Eq, DoubleCoset.σRight
Proof uses: Eq.mp, HMul.hMul, OfNat.ofNat, congr, congrArg, one_mul, Eq.trans, congrFun', DoubleCoset.σRight_one, DoubleCoset.σRight_mul
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma DoubleCoset.σLeft_of_mem line 369 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Membership.mem, Eq, Subtype, DoubleCoset.σLeft, OfNat.ofNat
Proof uses: Exists, CanLift.prf, Eq.mp, HMul.hMul, DoubleCoset.σ, DoubleCoset.mk, DoubleCoset.σRight, Eq.trans, congrFun', congrArg, congr, DoubleCoset.σ_of_mem_right, of_eq_true, mul_one, DoubleCoset.σRight_eq_self, DoubleCoset.σ_spec
34 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.