theorem Q2Presentation.Induction.frame_decomposition
  {ΓProfiniteGrp.{0} : ProfiniteGrp.{0}ProfiniteGrp.{u_1} : Type (u_1 + 1)The category of profinite groups. A term of this type consists of a profinite
set with a topological group structure.
}
  (BQ2Presentation.BoundaryPackage Γ : Q2Presentation.BoundaryPackageQ2Presentation.BoundaryPackage (Γ : ProfiniteGrp.{0}) : TypeA **boundary package** on a profinite group `Γ`: the uniform Stage-C data of a tame
quotient, a maximal pro-`2` quotient, and a common unramified character `ℤ₂` through which
both factor (manuscript Prop 3.14, `prop:compatiblemarking`; plan Turn 4 §6).  The
compatibility `tameMap ≫ ν_t = ν = pro2Map ≫ ν_2` records that the two markings agree on
the full unramified coordinate, not merely modulo `2`.  ΓProfiniteGrp.{0})
  (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]
  (hfac∀ (f : Q2Presentation.Profinite.SurjContHom Γ (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))),
  ∃ α,
    ∀ (γ : ↑Γ.toProfinite.toTop),
      (QuotientGroup.mk' (Q2Presentation.twoCore G)) ((ProfiniteGrp.Hom.hom f.hom) γ) =
        (ProfiniteGrp.Hom.hom α) ((ProfiniteGrp.Hom.hom B.tameMap) γ) :
    ∀
      (fQ2Presentation.Profinite.SurjContHom Γ (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). 
          ΓProfiniteGrp.{0}
          (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)),
        ∀ (γ↑Γ.toProfinite.toTop : ↑ΓProfiniteGrp.{0}.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 Γ (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. )
                γ↑Γ.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`. 
                  BQ2Presentation.BoundaryPackage Γ.tameMapQ2Presentation.BoundaryPackage.tameMap {Γ : ProfiniteGrp.{0}} (self : Q2Presentation.BoundaryPackage Γ) :
  Γ ⟶ Q2Presentation.TtameThe tame quotient map `Γ ↠ T_A`. )
                γ↑Γ.toProfinite.toTop)) :
  Cardinal.mkCardinal.mk.{u} : Type u → Cardinal.{u}The cardinal number of a type 
      (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). 
        ΓProfiniteGrp.{0}
        (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))) =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`.
    Cardinal.sumCardinal.sum.{u_1, u_2} {ι : Type u_1} (f : ι → Cardinal.{u_2}) : Cardinal.{max u_2 u_1}The indexed sum of cardinals is the cardinality of the
indexed disjoint union, i.e. sigma type.  fun φQ2Presentation.Induction.Frames G =>
      Cardinal.mkCardinal.mk.{u} : Type u → Cardinal.{u}The cardinal number of a type 
        (Q2Presentation.boundaryFramedSurjQ2Presentation.boundaryFramedSurj {Γ : ProfiniteGrp.{0}} (B : Q2Presentation.BoundaryPackage Γ)
  (Yt : Q2Presentation.BoundaryFramedTarget) (F : Q2Presentation.BoundaryFrame Yt) : TypeThe **boundary-framed surjections** `e_Γ^β(𝒴)` (manuscript `eq:eGamma`): the
continuous surjections `f : Γ ↠ Y` whose induced map to `H × E` is the prescribed
`β ∘ b_Γ`, i.e. `q_Y ∘ f = β ∘ b_Γ`.  This is the subtype counted in Theorem 4.2;
its cardinality is `e_Γ^β(𝒴)`. 
          BQ2Presentation.BoundaryPackage Γ
          (Q2Presentation.Induction.tameTargetQ2Presentation.Induction.tameTarget (G : Type) [Group G] [Finite G] : Q2Presentation.BoundaryFramedTargetThe **canonical boundary-framed marked target** `𝒴_G` attached to a finite group
`G` (manuscript `lem:tameframeexhaustion`, the `E = 0` framed target): the target is
`G`, the marked `2`-kernel is the `2`-core `O₂(G) = twoCore G` (a `2`-group by
`twoCore_isPGroup`, the wild part), the tame quotient is the canonical projection
`π_Y : G ↠ G/O₂(G)` (kernel exactly `O₂(G)` by `QuotientGroup.ker_mk'`), and the
decoration is trivial (`E = ℤ/2`, `θ_Y = 1`). 
            GType)
          (Q2Presentation.Induction.frameOfQ2Presentation.Induction.frameOf (G : Type) [Group G] [Finite G]
  (α : Q2Presentation.Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (G ⧸ Q2Presentation.twoCore G)))
  (hα : Function.Surjective ⇑(ProfiniteGrp.Hom.hom α)) :
  Q2Presentation.BoundaryFrame (Q2Presentation.Induction.tameTarget G)The **boundary frame attached to a tame frame** `α : T_A ↠ G/O₂(G)` (manuscript
`eq:beta` with trivial elementary marking): `(α, ψ = 1, β = boundaryBeta α 1)`.  The
frame index `Frames G` is exactly the surjections `α`. 
            GType φQ2Presentation.Induction.Frames G.homQ2Presentation.Profinite.SurjContHom.hom.{u} {P Q : ProfiniteGrp.{u}}
  (self : Q2Presentation.Profinite.SurjContHom P Q) : P ⟶ QThe underlying morphism of profinite groups.  ⋯))

theorem Q2Presentation.Induction.tameFrameExhaustion_proven
  (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] :
  ∃ FramesType YFrames → Q2Presentation.Induction.FramedPair,
    (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`.Cardinal.mkCardinal.mk.{u} : Type u → Cardinal.{u}The cardinal number of a type 
          (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))) =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`.
        Cardinal.sumCardinal.sum.{u_1, u_2} {ι : Type u_1} (f : ι → Cardinal.{u_2}) : Cardinal.{max u_2 u_1}The indexed sum of cardinals is the cardinality of the
indexed disjoint union, i.e. sigma type.  fun φFrames =>
          Q2Presentation.Induction.framedCountAQ2Presentation.Induction.framedCountA (p : Q2Presentation.Induction.FramedPair) : Cardinal.{0}The **candidate** boundary-framed surjection count `e_{Γ_A}^β(𝒴)`
(`eq:eGamma`), as a cardinal `|boundaryFramedSurj boundaryPackage_GammaA 𝒴 F|`. 
            (YFrames → Q2Presentation.Induction.FramedPair φFrames))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`. ∧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 `/\`).
      Cardinal.mkCardinal.mk.{u} : Type u → Cardinal.{u}The cardinal number of a type 
          (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))) =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`.
        Cardinal.sumCardinal.sum.{u_1, u_2} {ι : Type u_1} (f : ι → Cardinal.{u_2}) : Cardinal.{max u_2 u_1}The indexed sum of cardinals is the cardinality of the
indexed disjoint union, i.e. sigma type.  fun φFrames =>
          Q2Presentation.Induction.framedCountQQ2Presentation.Induction.framedCountQ (p : Q2Presentation.Induction.FramedPair) : Cardinal.{0}The **local** boundary-framed surjection count `e_{G_{ℚ₂}}^β(𝒴)`
(`eq:eGamma`), as a cardinal `|boundaryFramedSurj boundaryPackage_GQ2 𝒴 F|`. 
            (YFrames → Q2Presentation.Induction.FramedPair φFrames)