theorem Q2Presentation.finite_tame_tau_odd.{u_1}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType u_1] [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 GType u_1]
  {sG tG : GType u_1}
  (hQ2Presentation.rconj t s = t ^ 2 : Q2Presentation.rconjQ2Presentation.rconj.{u_1} {G : Type u_1} [Group G] (x g : G) : GRight conjugation `x^g = g⁻¹ * x * g` (manuscript convention).  tG sG =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. tG ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. 2) :
  OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  (orderOforderOf.{u_1} {G : Type u_1} [Monoid G] (x : G) : ℕ`orderOf x` is the order of the element `x`, i.e. the `n ≥ 1`, s.t. `x ^ n = 1` if it exists.
Otherwise, i.e. if `x` is of infinite order, then `orderOf x` is `0` by convention.  tG)

theorem Q2Presentation.finite_tame_normal_two_subgroup_unramified.{u_1}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType u_1] [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 GType u_1]
  {sG tG : GType u_1}
  (hgenSubgroup.closure {s, t} = ⊤ : Subgroup.closureSubgroup.closure.{u_1} {G : Type u_1} [Group G] (k : Set G) : Subgroup GThe `Subgroup` generated by a set.  {Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`. sG,Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`.  tG}Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. ⊤Top.top.{u_1} {α : Type u_1} [self : Top α] : αThe top (`⊤`, `\top`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊤` in identifiers is `top`.)
  (htameQ2Presentation.rconj t s = t ^ 2 :
    Q2Presentation.rconjQ2Presentation.rconj.{u_1} {G : Type u_1} [Group G] (x g : G) : GRight conjugation `x^g = g⁻¹ * x * g` (manuscript convention).  tG sG =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. tG ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. 2)
  (NSubgroup G : SubgroupSubgroup.{u_3} (G : Type u_3) [Group G] : Type u_3A subgroup of a group `G` is a subset containing 1, closed under multiplication
and closed under multiplicative inverse.  GType u_1) [NSubgroup G.NormalSubgroup.Normal.{u_1} {G : Type u_1} [Group G] (H : Subgroup G) : PropA subgroup `H` is normal if whenever `n ∈ H`, then `g * n * g⁻¹ ∈ H` for every `g : G` ]
  (hN2IsPGroup 2 ↥N : IsPGroupIsPGroup.{u_1} (p : ℕ) (G : Type u_1) [Group G] : PropA p-group is a group in which the order of every element is a power of `p`.  2 ↥NSubgroup G) :
  NSubgroup G ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`). Subgroup.centerSubgroup.center.{u_1} (G : Type u_1) [Group G] : Subgroup GThe center of a group `G` is the set of elements that commute with everything in `G`  GType u_1 ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
    NSubgroup G ⊓ Subgroup.zpowersSubgroup.zpowers.{u_1} {G : Type u_1} [Group G] (g : G) : Subgroup GThe subgroup generated by an element.  tG =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. ⊥Bot.bot.{u_1} {α : Type u_1} [self : Bot α] : αThe bot (`⊥`, `\bot`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊥` in identifiers is `bot`.

theorem Q2Presentation.Induction.headTau_zpowers_normal
  {pQ2Presentation.Induction.FramedPair :
    Q2Presentation.Induction.FramedPairQ2Presentation.Induction.FramedPair : Type 1A **framed pair** `(𝒴, F)`: a boundary-framed marked target together with a
boundary frame for it (manuscript Definition 4.1 + `eq:beta`).  This is the index of
Theorem 4.2: the boundary-framed surjection count `e_Γ^β` is a function of the pair.
The induction of `sec:induction` ranges over *all* such pairs simultaneously
("the induction is stated globally", l.1213), ordered by `|L_Y|`. }
  (chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p :
    Q2Presentation.Induction.FirstNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA non-scalar chief factor of `L_Y` that is **first**: every chief factor strictly
below it (i.e. with upper term contained in `lower`) is scalar.  This is the manuscript's
choice `S ◁ P` at l.3616–3623 ("all chief factors below `S` are scalar and `V` is the
first non-scalar simple factor"), which `lem:collapse` requires for the coprime step
`[S, Ñ] = 1`. 
      pQ2Presentation.Induction.FramedPair)
  (KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.) 
      chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p.toNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor.toNonScalarChiefFactor {p : Q2Presentation.Induction.FramedPair}
  (self : Q2Presentation.Induction.FirstNonScalarChiefFactor p) : Q2Presentation.Induction.NonScalarChiefFactor p) :
  (Subgroup.zpowersSubgroup.zpowers.{u_1} {G : Type u_1} [Group G] (g : G) : Subgroup GThe subgroup generated by an element. 
      (Q2Presentation.Induction.headTauQ2Presentation.Induction.headTau {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) : Q2Presentation.Induction.HeadIm chief K**`τ̃` — THE canonical ramification operator of the block** (design
§4.2/§4.5: `headTau = 1` exactly captures the unramified discharge
below; when P8-S2a lands, `blockTameRamFlag` is to be DEFINED as the
Bool-spelling of `headTau ≠ 1`, so the F-ram gate and the sign-lane
flag are the same object). 
        chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)).NormalSubgroup.Normal.{u_1} {G : Type u_1} [Group G] (H : Subgroup G) : PropA subgroup `H` is normal if whenever `n ∈ H`, then `g * n * g⁻¹ ∈ H` for every `g : G` 

theorem Q2Presentation.OddSplitting.tame_zpowers_normal.{u_4}
  {GType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType u_4] [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 GType u_4]
  {sG tG : GType u_4}
  (hgenSubgroup.closure {s, t} = ⊤ : Subgroup.closureSubgroup.closure.{u_1} {G : Type u_1} [Group G] (k : Set G) : Subgroup GThe `Subgroup` generated by a set.  {Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`. sG,Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`.  tG}Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. ⊤Top.top.{u_1} {α : Type u_1} [self : Top α] : αThe top (`⊤`, `\top`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊤` in identifiers is `top`.)
  (htames⁻¹ * t * s = t ^ 2 : sG⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`. *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. tG *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. sG =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. tG ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. 2)
  (htoddOdd (orderOf t) : OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  (orderOforderOf.{u_1} {G : Type u_1} [Monoid G] (x : G) : ℕ`orderOf x` is the order of the element `x`, i.e. the `n ≥ 1`, s.t. `x ^ n = 1` if it exists.
Otherwise, i.e. if `x` is of infinite order, then `orderOf x` is `0` by convention.  tG)) :
  (Subgroup.zpowersSubgroup.zpowers.{u_1} {G : Type u_1} [Group G] (g : G) : Subgroup GThe subgroup generated by an element.  tG).NormalSubgroup.Normal.{u_1} {G : Type u_1} [Group G] (H : Subgroup G) : PropA subgroup `H` is normal if whenever `n ∈ H`, then `g * n * g⁻¹ ∈ H` for every `g : G` 

theorem Q2Presentation.Induction.gammaA_tameQuotientFactor
  (GType : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType] [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 GType]
  [NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 GType]
  (fQ2Presentation.Profinite.SurjContHom Q2Presentation.GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)) :
    Q2Presentation.Profinite.SurjContHomQ2Presentation.Profinite.SurjContHom.{u} (P Q : ProfiniteGrp.{u}) : Type uA surjective continuous homomorphism of profinite groups (a profinite
"epimorphism", recorded as data: the morphism together with surjectivity of the
underlying map). 
      Q2Presentation.GammaAQ2Presentation.GammaA : ProfiniteGrp.{0}The candidate profinite group `Γ_A`, the cofiltered inverse limit (in
`ProfiniteGrp`) of all admissible finite marked quotients (manuscript
eq. `candidateinverse`). 
      (ProfiniteGrp.ofFiniteGrpProfiniteGrp.ofFiniteGrp.{u_1} (G : FiniteGrp.{u_1}) : ProfiniteGrp.{u_1}A `FiniteGrp` when given the discrete topology can be considered as a profinite group. 
        (FiniteGrp.ofFiniteGrp.of.{u} (G : Type u) [Group G] [Finite G] : FiniteGrp.{u}Construct a term of `FiniteGrp` from a type endowed with the structure of a finite group.  GType))) :
  ∃ αQ2Presentation.Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (G ⧸ Q2Presentation.twoCore G)),
    ∀
      (γ↑Q2Presentation.GammaA.toProfinite.toTop :
        ↑Q2Presentation.GammaAQ2Presentation.GammaA : ProfiniteGrp.{0}The candidate profinite group `Γ_A`, the cofiltered inverse limit (in
`ProfiniteGrp`) of all admissible finite marked quotients (manuscript
eq. `candidateinverse`). .toProfiniteProfiniteGrp.toProfinite.{u_1} (self : ProfiniteGrp.{u_1}) : ProfiniteThe underlying profinite topological space. .toTopCompHausLike.toTop.{u} {P : TopCat → Prop} (self : CompHausLike P) : TopCatThe underlying topological space of an object of `CompHausLike P`. ),
      (QuotientGroup.mk'QuotientGroup.mk'.{u_1} {G : Type u_1} [Group G] (N : Subgroup G) [nN : N.Normal] : G →* G ⧸ NThe group homomorphism from `G` to `G/N`. 
            (Q2Presentation.twoCoreQ2Presentation.twoCore.{u_1} (G : Type u_1) [Group G] : Subgroup GThe **2-core** `O₂(G)` — the wild subgroup of the `Q₂` presentation.  GType))
          ((ProfiniteGrp.Hom.homProfiniteGrp.Hom.hom.{u} {M N : ProfiniteGrp.{u}} (f : M.Hom N) : ↑M.toProfinite.toTop →ₜ* ↑N.toProfinite.toTopThe underlying `ContinuousMonoidHom`.  fQ2Presentation.Profinite.SurjContHom Q2Presentation.GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)).homQ2Presentation.Profinite.SurjContHom.hom.{u} {P Q : ProfiniteGrp.{u}}
  (self : Q2Presentation.Profinite.SurjContHom P Q) : P ⟶ QThe underlying morphism of profinite groups. )
            γ↑Q2Presentation.GammaA.toProfinite.toTop) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
        (ProfiniteGrp.Hom.homProfiniteGrp.Hom.hom.{u} {M N : ProfiniteGrp.{u}} (f : M.Hom N) : ↑M.toProfinite.toTop →ₜ* ↑N.toProfinite.toTopThe underlying `ContinuousMonoidHom`.  αQ2Presentation.Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (G ⧸ Q2Presentation.twoCore G)))
          ((ProfiniteGrp.Hom.homProfiniteGrp.Hom.hom.{u} {M N : ProfiniteGrp.{u}} (f : M.Hom N) : ↑M.toProfinite.toTop →ₜ* ↑N.toProfinite.toTopThe underlying `ContinuousMonoidHom`. 
              Q2Presentation.boundaryPackage_GammaAQ2Presentation.boundaryPackage_GammaA : Q2Presentation.BoundaryPackage Q2Presentation.GammaA**The candidate boundary package** (manuscript Prop 3.14, `prop:compatiblemarking`;
plan Turn 4 §6).  The Stage-C data of `Γ_A`: the common tame quotient `gammaTameMap`,
the maximal pro-`2` quotient `p : Γ_A ⟶ Π`, and the common unramified character
`ν = gammaTameMap ≫ ν_t`, through which both factor. .tameMapQ2Presentation.BoundaryPackage.tameMap {Γ : ProfiniteGrp.{0}} (self : Q2Presentation.BoundaryPackage Γ) :
  Γ ⟶ Q2Presentation.TtameThe tame quotient map `Γ ↠ T_A`. )
            γ↑Q2Presentation.GammaA.toProfinite.toTop)

theorem Q2Presentation.Induction.gq2_tameQuotientFactor
  (GType : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType] [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 GType]
  [NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 GType]
  (fQ2Presentation.Profinite.SurjContHom Q2Presentation.GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)) :
    Q2Presentation.Profinite.SurjContHomQ2Presentation.Profinite.SurjContHom.{u} (P Q : ProfiniteGrp.{u}) : Type uA surjective continuous homomorphism of profinite groups (a profinite
"epimorphism", recorded as data: the morphism together with surjectivity of the
underlying map). 
      Q2Presentation.GQ2ProfiniteQ2Presentation.GQ2Profinite : ProfiniteGrp.{0}The absolute Galois group `G_{ℚ₂} = Gal(Q̄₂/ℚ₂)` of the `2`-adic field
`ℚ₂ = ℚ_[2]`, as a profinite group.

Concretely it is `Gal(SeparableClosure ℚ_[2] / ℚ_[2])`, packaged as an object of
`ProfiniteGrp` by `InfiniteGalois.profiniteGalGrp`.  Since `ℚ_[2]` has
characteristic `0` its separable closure is an algebraic closure, so this is the
absolute Galois group in the usual sense, matching the manuscript's `G_{ℚ₂}`. 
      (ProfiniteGrp.ofFiniteGrpProfiniteGrp.ofFiniteGrp.{u_1} (G : FiniteGrp.{u_1}) : ProfiniteGrp.{u_1}A `FiniteGrp` when given the discrete topology can be considered as a profinite group. 
        (FiniteGrp.ofFiniteGrp.of.{u} (G : Type u) [Group G] [Finite G] : FiniteGrp.{u}Construct a term of `FiniteGrp` from a type endowed with the structure of a finite group.  GType))) :
  ∃ αQ2Presentation.Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (G ⧸ Q2Presentation.twoCore G)),
    ∀
      (γ↑Q2Presentation.GQ2Profinite.toProfinite.toTop :
        ↑Q2Presentation.GQ2ProfiniteQ2Presentation.GQ2Profinite : ProfiniteGrp.{0}The absolute Galois group `G_{ℚ₂} = Gal(Q̄₂/ℚ₂)` of the `2`-adic field
`ℚ₂ = ℚ_[2]`, as a profinite group.

Concretely it is `Gal(SeparableClosure ℚ_[2] / ℚ_[2])`, packaged as an object of
`ProfiniteGrp` by `InfiniteGalois.profiniteGalGrp`.  Since `ℚ_[2]` has
characteristic `0` its separable closure is an algebraic closure, so this is the
absolute Galois group in the usual sense, matching the manuscript's `G_{ℚ₂}`. .toProfiniteProfiniteGrp.toProfinite.{u_1} (self : ProfiniteGrp.{u_1}) : ProfiniteThe underlying profinite topological space. .toTopCompHausLike.toTop.{u} {P : TopCat → Prop} (self : CompHausLike P) : TopCatThe underlying topological space of an object of `CompHausLike P`. ),
      (QuotientGroup.mk'QuotientGroup.mk'.{u_1} {G : Type u_1} [Group G] (N : Subgroup G) [nN : N.Normal] : G →* G ⧸ NThe group homomorphism from `G` to `G/N`. 
            (Q2Presentation.twoCoreQ2Presentation.twoCore.{u_1} (G : Type u_1) [Group G] : Subgroup GThe **2-core** `O₂(G)` — the wild subgroup of the `Q₂` presentation.  GType))
          ((ProfiniteGrp.Hom.homProfiniteGrp.Hom.hom.{u} {M N : ProfiniteGrp.{u}} (f : M.Hom N) : ↑M.toProfinite.toTop →ₜ* ↑N.toProfinite.toTopThe underlying `ContinuousMonoidHom`.  fQ2Presentation.Profinite.SurjContHom Q2Presentation.GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)).homQ2Presentation.Profinite.SurjContHom.hom.{u} {P Q : ProfiniteGrp.{u}}
  (self : Q2Presentation.Profinite.SurjContHom P Q) : P ⟶ QThe underlying morphism of profinite groups. )
            γ↑Q2Presentation.GQ2Profinite.toProfinite.toTop) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
        (ProfiniteGrp.Hom.homProfiniteGrp.Hom.hom.{u} {M N : ProfiniteGrp.{u}} (f : M.Hom N) : ↑M.toProfinite.toTop →ₜ* ↑N.toProfinite.toTopThe underlying `ContinuousMonoidHom`.  αQ2Presentation.Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (G ⧸ Q2Presentation.twoCore G)))
          ((ProfiniteGrp.Hom.homProfiniteGrp.Hom.hom.{u} {M N : ProfiniteGrp.{u}} (f : M.Hom N) : ↑M.toProfinite.toTop →ₜ* ↑N.toProfinite.toTopThe underlying `ContinuousMonoidHom`. 
              Q2Presentation.boundaryPackage_GQ2Q2Presentation.boundaryPackage_GQ2 : Q2Presentation.BoundaryPackage Q2Presentation.GQ2Profinite**The local boundary package** `boundaryPackage_GQ2 : BoundaryPackage G_{ℚ₂}`
(manuscript Prop 3.14 `prop:compatiblemarking` for `Γ = G_{ℚ₂}`; plan Turn 4 §6),
the `G_{ℚ₂}`-side instance of the uniform Stage-C boundary datum.

* `tameMap`/`tame_surj`/`tame_nu` — the local tame quotient `G_{ℚ₂} ↠ T_A` with
  unramified marking `ν_loc`, from the axiom `gq2_tame_quotient` (Prop 3.2 + the
  local half of Prop `compatiblemarking`);
* `pro2Map`/`pro2_surj`/`pro2_nu` — the local maximal pro-`2` quotient
  `G_{ℚ₂} ↠ Π` with the *same* unramified marking `ν_loc`, proved from the fully
  marked Labute comparison `labute_GQ2_maxPro2_marked` (`pro2Map_loc`,
  `pro2Map_loc_surjective`, `pro2Map_loc_nu`);
* `nu := ν_loc` — the common unramified character through which both factor. .tameMapQ2Presentation.BoundaryPackage.tameMap {Γ : ProfiniteGrp.{0}} (self : Q2Presentation.BoundaryPackage Γ) :
  Γ ⟶ Q2Presentation.TtameThe tame quotient map `Γ ↠ T_A`. )
            γ↑Q2Presentation.GQ2Profinite.toProfinite.toTop)

theorem Q2Presentation.quotient_by_twoCore_has_no_nontrivial_normal_two_subgroup.{u_1}
  (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType u_1] [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 GType u_1]
  (NSubgroup (G ⧸ Q2Presentation.twoCore G) :
    SubgroupSubgroup.{u_3} (G : Type u_3) [Group G] : Type u_3A subgroup of a group `G` is a subset containing 1, closed under multiplication
and closed under multiplicative inverse. 
      (HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
GType u_1 ⧸HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
 Q2Presentation.twoCoreQ2Presentation.twoCore.{u_1} (G : Type u_1) [Group G] : Subgroup GThe **2-core** `O₂(G)` — the wild subgroup of the `Q₂` presentation.  GType u_1)HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
)
  (hNN.Normal : NSubgroup (G ⧸ Q2Presentation.twoCore G).NormalSubgroup.Normal.{u_1} {G : Type u_1} [Group G] (H : Subgroup G) : PropA subgroup `H` is normal if whenever `n ∈ H`, then `g * n * g⁻¹ ∈ H` for every `g : G` ) (h2IsPGroup 2 ↥N : IsPGroupIsPGroup.{u_1} (p : ℕ) (G : Type u_1) [Group G] : PropA p-group is a group in which the order of every element is a power of `p`.  2 ↥NSubgroup (G ⧸ Q2Presentation.twoCore G)) :
  NSubgroup (G ⧸ Q2Presentation.twoCore G) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. ⊥Bot.bot.{u_1} {α : Type u_1} [self : Bot α] : αThe bot (`⊥`, `\bot`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊥` in identifiers is `bot`.

theorem Q2Presentation.admissible_twoGroup_iff_piMarked.{u_1}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType u_1] [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 GType u_1]
  (hG2IsPGroup 2 G : IsPGroupIsPGroup.{u_1} (p : ℕ) (G : Type u_1) [Group G] : PropA p-group is a group in which the order of every element is a power of `p`.  2 GType u_1)
  (qQ2Presentation.Marking G : Q2Presentation.MarkingQ2Presentation.Marking.{u_1} (G : Type u_1) [Group G] : Type u_1A marking assigns a group element to each of the four generators.  GType u_1) :
  Q2Presentation.AdmissibleQ2Presentation.Admissible.{u_1} {G : Type u_1} [Group G] [Finite G] (q : Q2Presentation.Marking G) : PropA marking is **admissible** when it generates, satisfies the tame and wild
relators, and sends `x₀, x₁` into the 2-core.  qQ2Presentation.Marking G ↔Iff (a b : Prop) : PropIf and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.

 * The recommended spelling of `<->` in identifiers is `iff` (prefer `↔` over `<->`).
    qQ2Presentation.Marking G Q2Presentation.Gen.tauQ2Presentation.Gen.tau : Q2Presentation.Gen =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1 ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
      Subgroup.closureSubgroup.closure.{u_1} {G : Type u_1} [Group G] (k : Set G) : Subgroup GThe `Subgroup` generated by a set. 
            {Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`. qQ2Presentation.Marking G Q2Presentation.Gen.sigmaQ2Presentation.Gen.sigma : Q2Presentation.Gen,Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`. 
              qQ2Presentation.Marking G Q2Presentation.Gen.x0Q2Presentation.Gen.x0 : Q2Presentation.Gen,Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`. 
              qQ2Presentation.Marking G Q2Presentation.Gen.x1Q2Presentation.Gen.x1 : Q2Presentation.Gen}Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
          ⊤Top.top.{u_1} {α : Type u_1} [self : Top α] : αThe top (`⊤`, `\top`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊤` in identifiers is `top`. ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
        Q2Presentation.rconjQ2Presentation.rconj.{u_1} {G : Type u_1} [Group G] (x g : G) : GRight conjugation `x^g = g⁻¹ * x * g` (manuscript convention). 
                (qQ2Presentation.Marking G Q2Presentation.Gen.x0Q2Presentation.Gen.x0 : Q2Presentation.Gen)
                (HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`.qQ2Presentation.Marking G
                    Q2Presentation.Gen.sigmaQ2Presentation.Gen.sigma : Q2Presentation.Gen ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`.
                  2)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
              qQ2Presentation.Marking G Q2Presentation.Gen.x0Q2Presentation.Gen.x0 : Q2Presentation.Gen *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
            Q2Presentation.commutatorWQ2Presentation.commutatorW.{u_1} {G : Type u_1} [Group G] (x y : G) : GCommutator `(x, y) = x⁻¹ * y⁻¹ * x * y` (manuscript convention). 
              (qQ2Presentation.Marking G Q2Presentation.Gen.x1Q2Presentation.Gen.x1 : Q2Presentation.Gen)
              (qQ2Presentation.Marking G
                Q2Presentation.Gen.sigmaQ2Presentation.Gen.sigma : Q2Presentation.Gen) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
          1

theorem Q2Presentation.nielsen_rel_equiv.{u_1}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType u_1] (aG sG yG : GType u_1) :
  aG ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. 2 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. sG ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. 4 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
        Q2Presentation.commutatorWQ2Presentation.commutatorW.{u_1} {G : Type u_1} [Group G] (x y : G) : GCommutator `(x, y) = x⁻¹ * y⁻¹ * x * y` (manuscript convention).  sG yG =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      1 ↔Iff (a b : Prop) : PropIf and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.

 * The recommended spelling of `<->` in identifiers is `iff` (prefer `↔` over `<->`).
    Q2Presentation.rconjQ2Presentation.rconj.{u_1} {G : Type u_1} [Group G] (x g : G) : GRight conjugation `x^g = g⁻¹ * x * g` (manuscript convention).  (HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.(HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`.sG ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. 2)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`.⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`. *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. aG⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`.)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
            (HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`.sG ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. 2)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
          (HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.(HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`.sG ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. 2)HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`.⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`. *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. aG⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`.)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
        Q2Presentation.commutatorWQ2Presentation.commutatorW.{u_1} {G : Type u_1} [Group G] (x y : G) : GCommutator `(x, y) = x⁻¹ * y⁻¹ * x * y` (manuscript convention).  yG sG =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      1

theorem Q2Presentation.gammaA_pro2_nu :
  CategoryTheory.CategoryStruct.compCategoryTheory.CategoryStruct.comp.{v, u} {obj : Type u} [self : CategoryTheory.CategoryStruct.{v, u} obj]
  {X Y Z : obj} : (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)Composition of morphisms in a category, written `f ≫ g`. 
      Q2Presentation.pQ2Presentation.p : Q2Presentation.GammaA ⟶ Q2Presentation.PiGrp**The canonical surjection** `p : Γ_A ⟶ Π`. 
      Q2Presentation.nu_2Q2Presentation.nu_2 : Q2Presentation.PiGrp ⟶ Q2Presentation.ProfiniteZ2**The unramified character** `ν₂ : PiGrp ⟶ ℤ₂`, `σ ↦ 1`, `x₀ ↦ 0`, `x₁ ↦ 0`.  Built as
the map into `ℤ₂ = lim_n ZMod(2ⁿ)` whose `n`-th coordinate is `piLayerHom n`.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    CategoryTheory.CategoryStruct.compCategoryTheory.CategoryStruct.comp.{v, u} {obj : Type u} [self : CategoryTheory.CategoryStruct.{v, u} obj]
  {X Y Z : obj} : (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)Composition of morphisms in a category, written `f ≫ g`. 
      Q2Presentation.gammaTameMapQ2Presentation.gammaTameMap : Q2Presentation.GammaA ⟶ Q2Presentation.Ttame**The common tame quotient map** `gammaTameMap : Γ_A ⟶ T_A` (Proposition 3.2). 
      Q2Presentation.nu_tQ2Presentation.nu_t : Q2Presentation.Ttame ⟶ Q2Presentation.ProfiniteZ2**The unramified character** `ν_t : Ttame ⟶ ℤ₂`, `σ ↦ 1`, `τ ↦ 0`.  Built as the
map into `ℤ₂ = lim_n ZMod(2ⁿ)` whose `n`-th coordinate is `tameLayerHom n`.