theorem Q2Presentation.BoundaryFramedTarget.exactImageTarget_boundaryFramed
  (YtQ2Presentation.BoundaryFramedTarget :
    Q2Presentation.BoundaryFramedTargetQ2Presentation.BoundaryFramedTarget : Type 1A **boundary-framed marked target** `𝒴 = (Y, L_Y, π_Y, θ_Y)` (manuscript
Definition 4.1, `def:framed`): a finite group `Y` with a normal finite `2`-subgroup
`L_Y`, a surjection `π_Y : Y ↠ H` onto a finite *tame* quotient with kernel exactly
`L_Y`, and an *elementary decoration* `θ_Y : Y → Multiplicative E` into the
multiplicative image of a finite `𝔽₂`-vector space `E`.  The pair
`q_Y = (π_Y, θ_Y)` fixes both the tame quotient `Y / L_Y ≅ H` and the decoration. )
  (JSubgroup Yt.Y : 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.  YtQ2Presentation.BoundaryFramedTarget.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. )
  (hJFunction.Surjective ⇑(Yt.piY.comp J.subtype) :
    Function.SurjectiveFunction.Surjective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : PropA function `f : α → β` is called surjective if every `b : β` is equal to `f a`
for some `a : α`. 
      ⇑(YtQ2Presentation.BoundaryFramedTarget.piYQ2Presentation.BoundaryFramedTarget.piY (self : Q2Presentation.BoundaryFramedTarget) : self.Y →* self.HThe tame quotient map `π_Y : Y ↠ H`. .compMonoidHom.comp.{u_4, u_5, u_6} {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOne M] [MulOne N] [MulOne P]
  (hnp : N →* P) (hmn : M →* N) : M →* PComposition of monoid morphisms as a monoid morphism.  JSubgroup Yt.Y.subtypeSubgroup.subtype.{u_1} {G : Type u_1} [Group G] (H : Subgroup G) : ↥H →* GThe natural group hom from a subgroup of group `G` to `G`. )) :
  (YtQ2Presentation.BoundaryFramedTarget.exactImageTargetQ2Presentation.BoundaryFramedTarget.exactImageTarget (Yt : Q2Presentation.BoundaryFramedTarget) (J : Subgroup Yt.Y)
  (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) : Q2Presentation.BoundaryFramedTarget**The exact-image stratum** `𝒥 = (J, J ∩ L_Y, π_Y|_J, θ_Y|_J)` (manuscript
Definition 4.1, exact-image paragraph), as a genuine `BoundaryFramedTarget`.

The hypothesis `hJ` says `J` *projects onto* `H` (`π_Y|_J` surjective), which is the
manuscript's "`J ≤ Y` projects onto `H`".  All four boundary-framed axioms are
inherited:

* `J ∩ L_Y` is normal in `J` (`Normal.subgroupOf`);
* `J ∩ L_Y` is a `2`-group (`subgroupOf_LY_isTwoGroup`);
* `π_Y|_J : J ↠ H` is surjective (the hypothesis `hJ`) with kernel `J ∩ L_Y`
  (`ker_piY_comp_subtype`).

The tame quotient `H` and the elementary decoration `E` are preserved on the nose.
This *is* the inheritance lemma: it being well-typed is the content.  JSubgroup Yt.Y hJFunction.Surjective ⇑(Yt.piY.comp J.subtype)).LYQ2Presentation.BoundaryFramedTarget.LY (self : Q2Presentation.BoundaryFramedTarget) : Subgroup self.YThe marked normal `2`-subgroup `L_Y ◁ Y` (the wild part).  =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`.
      YtQ2Presentation.BoundaryFramedTarget.LYQ2Presentation.BoundaryFramedTarget.LY (self : Q2Presentation.BoundaryFramedTarget) : Subgroup self.YThe marked normal `2`-subgroup `L_Y ◁ Y` (the wild part). .subgroupOfSubgroup.subgroupOf.{u_1} {G : Type u_1} [Group G] (H K : Subgroup G) : Subgroup ↥KFor any subgroups `H` and `K`, view `H ⊓ K` as a subgroup of `K`.  JSubgroup Yt.Y ∧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 `/\`).
    (YtQ2Presentation.BoundaryFramedTarget.exactImageTargetQ2Presentation.BoundaryFramedTarget.exactImageTarget (Yt : Q2Presentation.BoundaryFramedTarget) (J : Subgroup Yt.Y)
  (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) : Q2Presentation.BoundaryFramedTarget**The exact-image stratum** `𝒥 = (J, J ∩ L_Y, π_Y|_J, θ_Y|_J)` (manuscript
Definition 4.1, exact-image paragraph), as a genuine `BoundaryFramedTarget`.

The hypothesis `hJ` says `J` *projects onto* `H` (`π_Y|_J` surjective), which is the
manuscript's "`J ≤ Y` projects onto `H`".  All four boundary-framed axioms are
inherited:

* `J ∩ L_Y` is normal in `J` (`Normal.subgroupOf`);
* `J ∩ L_Y` is a `2`-group (`subgroupOf_LY_isTwoGroup`);
* `π_Y|_J : J ↠ H` is surjective (the hypothesis `hJ`) with kernel `J ∩ L_Y`
  (`ker_piY_comp_subtype`).

The tame quotient `H` and the elementary decoration `E` are preserved on the nose.
This *is* the inheritance lemma: it being well-typed is the content.  JSubgroup Yt.Y hJFunction.Surjective ⇑(Yt.piY.comp J.subtype)).LYQ2Presentation.BoundaryFramedTarget.LY (self : Q2Presentation.BoundaryFramedTarget) : Subgroup self.YThe marked normal `2`-subgroup `L_Y ◁ Y` (the wild part). .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`  ∧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 `/\`).
      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
          ↥(YtQ2Presentation.BoundaryFramedTarget.exactImageTargetQ2Presentation.BoundaryFramedTarget.exactImageTarget (Yt : Q2Presentation.BoundaryFramedTarget) (J : Subgroup Yt.Y)
  (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) : Q2Presentation.BoundaryFramedTarget**The exact-image stratum** `𝒥 = (J, J ∩ L_Y, π_Y|_J, θ_Y|_J)` (manuscript
Definition 4.1, exact-image paragraph), as a genuine `BoundaryFramedTarget`.

The hypothesis `hJ` says `J` *projects onto* `H` (`π_Y|_J` surjective), which is the
manuscript's "`J ≤ Y` projects onto `H`".  All four boundary-framed axioms are
inherited:

* `J ∩ L_Y` is normal in `J` (`Normal.subgroupOf`);
* `J ∩ L_Y` is a `2`-group (`subgroupOf_LY_isTwoGroup`);
* `π_Y|_J : J ↠ H` is surjective (the hypothesis `hJ`) with kernel `J ∩ L_Y`
  (`ker_piY_comp_subtype`).

The tame quotient `H` and the elementary decoration `E` are preserved on the nose.
This *is* the inheritance lemma: it being well-typed is the content.  JSubgroup Yt.Y hJFunction.Surjective ⇑(Yt.piY.comp J.subtype)).LYQ2Presentation.BoundaryFramedTarget.LY (self : Q2Presentation.BoundaryFramedTarget) : Subgroup self.YThe marked normal `2`-subgroup `L_Y ◁ Y` (the wild part).  ∧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 `/\`).
        (YtQ2Presentation.BoundaryFramedTarget.exactImageTargetQ2Presentation.BoundaryFramedTarget.exactImageTarget (Yt : Q2Presentation.BoundaryFramedTarget) (J : Subgroup Yt.Y)
  (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) : Q2Presentation.BoundaryFramedTarget**The exact-image stratum** `𝒥 = (J, J ∩ L_Y, π_Y|_J, θ_Y|_J)` (manuscript
Definition 4.1, exact-image paragraph), as a genuine `BoundaryFramedTarget`.

The hypothesis `hJ` says `J` *projects onto* `H` (`π_Y|_J` surjective), which is the
manuscript's "`J ≤ Y` projects onto `H`".  All four boundary-framed axioms are
inherited:

* `J ∩ L_Y` is normal in `J` (`Normal.subgroupOf`);
* `J ∩ L_Y` is a `2`-group (`subgroupOf_LY_isTwoGroup`);
* `π_Y|_J : J ↠ H` is surjective (the hypothesis `hJ`) with kernel `J ∩ L_Y`
  (`ker_piY_comp_subtype`).

The tame quotient `H` and the elementary decoration `E` are preserved on the nose.
This *is* the inheritance lemma: it being well-typed is the content.  JSubgroup Yt.Y
                hJFunction.Surjective ⇑(Yt.piY.comp J.subtype)).piYQ2Presentation.BoundaryFramedTarget.piY (self : Q2Presentation.BoundaryFramedTarget) : self.Y →* self.HThe tame quotient map `π_Y : Y ↠ H`. .kerMonoidHom.ker.{u_1, u_7} {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) : Subgroup GThe multiplicative kernel of a monoid homomorphism is the subgroup of elements `x : G` such that
`f x = 1`  =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`.
          (YtQ2Presentation.BoundaryFramedTarget.exactImageTargetQ2Presentation.BoundaryFramedTarget.exactImageTarget (Yt : Q2Presentation.BoundaryFramedTarget) (J : Subgroup Yt.Y)
  (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) : Q2Presentation.BoundaryFramedTarget**The exact-image stratum** `𝒥 = (J, J ∩ L_Y, π_Y|_J, θ_Y|_J)` (manuscript
Definition 4.1, exact-image paragraph), as a genuine `BoundaryFramedTarget`.

The hypothesis `hJ` says `J` *projects onto* `H` (`π_Y|_J` surjective), which is the
manuscript's "`J ≤ Y` projects onto `H`".  All four boundary-framed axioms are
inherited:

* `J ∩ L_Y` is normal in `J` (`Normal.subgroupOf`);
* `J ∩ L_Y` is a `2`-group (`subgroupOf_LY_isTwoGroup`);
* `π_Y|_J : J ↠ H` is surjective (the hypothesis `hJ`) with kernel `J ∩ L_Y`
  (`ker_piY_comp_subtype`).

The tame quotient `H` and the elementary decoration `E` are preserved on the nose.
This *is* the inheritance lemma: it being well-typed is the content.  JSubgroup Yt.Y hJFunction.Surjective ⇑(Yt.piY.comp J.subtype)).LYQ2Presentation.BoundaryFramedTarget.LY (self : Q2Presentation.BoundaryFramedTarget) : Subgroup self.YThe marked normal `2`-subgroup `L_Y ◁ Y` (the wild part). 

theorem Q2Presentation.Induction.boundaryFramed_counts_equal
  (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|`. ) :
  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|`. 
      pQ2Presentation.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`.
    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|`. 
      pQ2Presentation.Induction.FramedPair