theorem Q2Presentation.finite_omega2_pow_independent_of_rep.{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] (gG : GType u_1) {Nℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} (hNN ≠ 0 : Nℕ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 0)
  (hdvdorderOf g ∣ N : 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.  gG ∣Dvd.dvd.{u_1} {α : Type u_1} [self : Dvd α] : α → α → PropDivisibility. `a ∣ b` (typed as `\|`) means that there is some `c` such that `b = a * c`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∣` in identifiers is `dvd`. Nℕ) :
  gG ^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`. (Q2Presentation.omega2ModQ2Presentation.omega2Mod (n : ℕ) : ZMod nThe 2-primary idempotent `ω₂ ∈ Ẑ` reduced modulo `n`: the odd part raised to
`φ` of the 2-part.  It is `≡ 1` modulo the 2-part `ordProj[2] n = 2 ^ (v₂ n)` and
`≡ 0` modulo the odd part `ordCompl[2] n`.  Nℕ).valZMod.val {n : ℕ} : ZMod n → ℕ`val a` is a natural number defined as:
- for `a : ZMod 0` it is the absolute value of `a`
- for `a : ZMod n` with `0 < n` it is the least natural number in the equivalence class

See `ZMod.valMinAbs` for a variant that takes values in the integers.
 =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.powOmega2Q2Presentation.powOmega2.{u_1} {G : Type u_1} [Group G] [Finite G] (g : G) : G`g` raised to the `ω₂`-power in a finite group: reduce `ω₂` modulo `orderOf g`
and take the ordinary power.  This depends only on `g` (through its order), not on
any fixed verification modulus.  gG

theorem Q2Presentation.Lifting.collector_eq.{u_2} {GType u_2 : Type u_2A 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_2]
  (φG →* G : GType u_2 →*MonoidHom.{u_10, u_11} (M : Type u_10) (N : Type u_11) [MulOne M] [MulOne N] : Type (max u_10 u_11)`M →* N` is the type of functions `M → N` that preserve the `MulOne` structure.
`MonoidHom` is used for both monoid and group homomorphisms.

When possible, instead of parametrizing results over `(f : M →* N)`,
you should parametrize over `(F : Type*) [MonoidHomClass F M N] (f : F)`.

When you extend this structure, make sure to extend `MonoidHomClass`.
 GType u_2) (XG DG : GType u_2) (hsq∀ (g h : G), g ^ 2 * h = h * g ^ 2 : ∀ (gG hG : GType u_2), gG ^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`. hG =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`. hG *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`. gG ^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)
  (hk∀ (a b h : G), a⁻¹ * b⁻¹ * a * b * h = h * (a⁻¹ * b⁻¹ * a * b) : ∀ (aG bG hG : GType u_2), 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`. bG⁻¹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 *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`. bG *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`. hG =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`. hG *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`.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`. bG⁻¹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 *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`. bG)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`.)
  (hk2∀ (a b : G), (a⁻¹ * b⁻¹ * a * b) ^ 2 = 1 : ∀ (aG bG : GType u_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`.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`. bG⁻¹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 *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`. bG)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`. 2 =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)
  (h4∀ (g : G), g ^ 4 = 1 : ∀ (gG : GType u_2), gG ^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 =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) :
  Q2Presentation.Lifting.collectorQ2Presentation.Lifting.collector.{u_2} {G : Type u_2} [Group G] (φ : G →* G) (X D : G) : GThe **class-two collector word** `𝔥_φ(X,D) = φ(X)·X · φ(D)·D · D²·[φ(D),D]`
(manuscript `lem:class2square`, l.1311), with the project commutator convention
`[A,B] = A⁻¹B⁻¹AB` (= `Q2Word.commExpr`).  φG →* G XG DG =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`. φG →* G XG *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`. XG *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`. DG⁻¹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`. φG →* G DG

theorem Q2Presentation.Lifting.collector_id_eq_sq.{u_2} {GType u_2 : Type u_2A 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_2]
  (XG DG : GType u_2) (h4∀ (g : G), g ^ 4 = 1 : ∀ (gG : GType u_2), gG ^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 =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) :
  Q2Presentation.Lifting.collectorQ2Presentation.Lifting.collector.{u_2} {G : Type u_2} [Group G] (φ : G →* G) (X D : G) : GThe **class-two collector word** `𝔥_φ(X,D) = φ(X)·X · φ(D)·D · D²·[φ(D),D]`
(manuscript `lem:class2square`, l.1311), with the project commutator convention
`[A,B] = A⁻¹B⁻¹AB` (= `Q2Word.commExpr`).  (MonoidHom.idMonoidHom.id.{u_10} (M : Type u_10) [MulOne M] : M →* MThe identity map from a monoid to itself.  GType u_2) XG DG =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`. XG ^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

theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0Data
  {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|`. }
  {h¬Q2Presentation.Induction.ScalarTerminal p : ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.Q2Presentation.Induction.ScalarTerminalQ2Presentation.Induction.ScalarTerminal (p : Q2Presentation.Induction.FramedPair) : Prop**Scalar-terminal framed pair.**  pQ2Presentation.Induction.FramedPair}
  {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}
  {hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1 : Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`.  ↥(Q2Presentation.Induction.kernelFrattiniQ2Presentation.Induction.kernelFrattini {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Subgroup p.fst.YThe literal Frattini subgroup `R = Φ(K)` of the kernel, as a subgroup of `Y`
(the manuscript's `R`, l.3626).  KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) =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}
  {childQ2Presentation.Induction.Sec7FrattiniTrivialElementaryChildData p :
    Q2Presentation.Induction.Sec7FrattiniTrivialElementaryChildDataQ2Presentation.Induction.Sec7FrattiniTrivialElementaryChildData (p : Q2Presentation.Induction.FramedPair) : Type 1The exact-image child packet for the `R = 1` elementary stage.  This isolates the
manuscript's child geometry (`C = Y/K` and the proper exact-image subtraction children)
from the source-specific elementary lift counts.
 pQ2Presentation.Induction.FramedPair}
  (srcQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child :
    Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceDataQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData
  {p : Q2Presentation.Induction.FramedPair} (h : ¬Q2Presentation.Induction.ScalarTerminal p)
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1)
  (child : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryChildData p) : TypeThe missing **candidate lower source/marking** for the `R = 1` M-stage.

This is deliberately smaller and more source-specific than the former operator packet.
It records a genuine candidate epimorphism to the lower quotient `C = towerC K`, its four
marked values `σ, τ, x₀, x₁`, and the candidate relators seen in that lower quotient.
No linear operators or cocycle cardinalities are chosen here. 
      h¬Q2Presentation.Induction.ScalarTerminal p chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1 childQ2Presentation.Induction.Sec7FrattiniTrivialElementaryChildData p) :
  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`.

    (Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowManuscriptH0DataQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowManuscriptH0Data
  {p : Q2Presentation.Induction.FramedPair} {h : ¬Q2Presentation.Induction.ScalarTerminal p}
  {chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p}
  {K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor}
  {hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1}
  {child : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryChildData p}
  (src : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) : TypeThe `h₀` row of the manuscript finite-word ledger (`lem:h0shadow`): the first-order
shadow of `h₀` is the shadow of `x₀²`, hence zero in characteristic two.

      srcQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child)

theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowProductRuleCoreData
  {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|`. }
  {h¬Q2Presentation.Induction.ScalarTerminal p : ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.Q2Presentation.Induction.ScalarTerminalQ2Presentation.Induction.ScalarTerminal (p : Q2Presentation.Induction.FramedPair) : Prop**Scalar-terminal framed pair.**  pQ2Presentation.Induction.FramedPair}
  {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}
  {hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1 : Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`.  ↥(Q2Presentation.Induction.kernelFrattiniQ2Presentation.Induction.kernelFrattini {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Subgroup p.fst.YThe literal Frattini subgroup `R = Φ(K)` of the kernel, as a subgroup of `Y`
(the manuscript's `R`, l.3626).  KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) =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}
  {childQ2Presentation.Induction.Sec7FrattiniTrivialElementaryChildData p :
    Q2Presentation.Induction.Sec7FrattiniTrivialElementaryChildDataQ2Presentation.Induction.Sec7FrattiniTrivialElementaryChildData (p : Q2Presentation.Induction.FramedPair) : Type 1The exact-image child packet for the `R = 1` elementary stage.  This isolates the
manuscript's child geometry (`C = Y/K` and the proper exact-image subtraction children)
from the source-specific elementary lift counts.
 pQ2Presentation.Induction.FramedPair}
  (srcQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child :
    Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceDataQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData
  {p : Q2Presentation.Induction.FramedPair} (h : ¬Q2Presentation.Induction.ScalarTerminal p)
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1)
  (child : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryChildData p) : TypeThe missing **candidate lower source/marking** for the `R = 1` M-stage.

This is deliberately smaller and more source-specific than the former operator packet.
It records a genuine candidate epimorphism to the lower quotient `C = towerC K`, its four
marked values `σ, τ, x₀, x₁`, and the candidate relators seen in that lower quotient.
No linear operators or cocycle cardinalities are chosen here. 
      h¬Q2Presentation.Induction.ScalarTerminal p chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1 childQ2Presentation.Induction.Sec7FrattiniTrivialElementaryChildData p)
  (h0Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowH0FactorData src :
    Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowH0FactorDataQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowH0FactorData
  {p : Q2Presentation.Induction.FramedPair} {h : ¬Q2Presentation.Induction.ScalarTerminal p}
  {chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p}
  {K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor}
  {hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1}
  {child : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryChildData p}
  (src : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) : TypeThe `h₀` factor contribution in the candidate wild-row ledger. 
      srcQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child)
  (u1Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowU1InvFactorData src :
    Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowU1InvFactorDataQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowU1InvFactorData
  {p : Q2Presentation.Induction.FramedPair} {h : ¬Q2Presentation.Induction.ScalarTerminal p}
  {chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p}
  {K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor}
  {hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1}
  {child : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryChildData p}
  (src : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) : TypeThe `u₁⁻¹` factor contribution in the candidate wild-row ledger. 
      srcQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child)
  (x1Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowX1ConjFactorData src :
    Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowX1ConjFactorDataQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowX1ConjFactorData
  {p : Q2Presentation.Induction.FramedPair} {h : ¬Q2Presentation.Induction.ScalarTerminal p}
  {chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p}
  {K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor}
  {hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1}
  {child : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryChildData p}
  (src : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) : TypeThe `x₁^σ` factor contribution in the candidate wild-row ledger. 
      srcQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child)
  (c0Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowC0FactorData src :
    Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowC0FactorDataQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowC0FactorData
  {p : Q2Presentation.Induction.FramedPair} {h : ¬Q2Presentation.Induction.ScalarTerminal p}
  {chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p}
  {K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor}
  {hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1}
  {child : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryChildData p}
  (src : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) : TypeThe commutator factor `c₀=[d₀,z₀]` contribution in the candidate wild-row ledger. 
      srcQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) :
  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`.

    (Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowProductRuleDataQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowProductRuleData
  {p : Q2Presentation.Induction.FramedPair} {h : ¬Q2Presentation.Induction.ScalarTerminal p}
  {chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p}
  {K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor}
  {hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1}
  {child : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryChildData p}
  (src : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child)
  (h0 : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowH0FactorData src)
  (u1 : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowU1InvFactorData src)
  (x1 : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowX1ConjFactorData src)
  (c0 : Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowC0FactorData src) : PropThe product-rule/Fox fundamental sum for the four actual wild-row factors.

This Route241 atom contains only the formal product-rule assembly of the four already
separated factor contributions; it does not identify any individual factor. 
      srcQ2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child h0Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowH0FactorData src u1Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowU1InvFactorData src x1Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowX1ConjFactorData src c0Q2Presentation.Induction.Sec7FrattiniTrivialElementaryMStageCandidateWildRowC0FactorData src)

theorem Q2Presentation.Lifting.HeisQ.sq_eq.{u_1} {AType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  AType u_1]
  [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) AType u_1] (uQ2Presentation.Lifting.HeisQ A : Q2Presentation.Lifting.HeisQQ2Presentation.Lifting.HeisQ.{u_2} (A : Type u_2) [AddCommGroup A] [Module (ZMod 2) A] : Type u_2The **mixed Heisenberg coefficient group** `H(A) = A × A^∨ × F₂`
(manuscript l.1490): primal coordinate `v = D_u`, dual coordinate `dl = D^∨_u`,
central coordinate `z = β_u`.  AType u_1) :
  uQ2Presentation.Lifting.HeisQ A ^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 =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.Lifting.HeisQ.mk.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A] (v : A)
  (dl : Q2Presentation.Lifting.Dual A) (z : ZMod 2) : Q2Presentation.Lifting.HeisQ A vAThe primal `A`-coordinate `D_u`.  :=Q2Presentation.Lifting.HeisQ.mk.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A] (v : A)
  (dl : Q2Presentation.Lifting.Dual A) (z : ZMod 2) : Q2Presentation.Lifting.HeisQ A 0,Q2Presentation.Lifting.HeisQ.mk.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A] (v : A)
  (dl : Q2Presentation.Lifting.Dual A) (z : ZMod 2) : Q2Presentation.Lifting.HeisQ A dlQ2Presentation.Lifting.Dual AThe dual `A^∨`-coordinate `D^∨_u`.  :=Q2Presentation.Lifting.HeisQ.mk.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A] (v : A)
  (dl : Q2Presentation.Lifting.Dual A) (z : ZMod 2) : Q2Presentation.Lifting.HeisQ A 0,Q2Presentation.Lifting.HeisQ.mk.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A] (v : A)
  (dl : Q2Presentation.Lifting.Dual A) (z : ZMod 2) : Q2Presentation.Lifting.HeisQ A zZMod 2The central `F₂`-coordinate `β_u`.  :=Q2Presentation.Lifting.HeisQ.mk.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A] (v : A)
  (dl : Q2Presentation.Lifting.Dual A) (z : ZMod 2) : Q2Presentation.Lifting.HeisQ A uQ2Presentation.Lifting.HeisQ A.dlQ2Presentation.Lifting.HeisQ.dl.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A]
  (self : Q2Presentation.Lifting.HeisQ A) : Q2Presentation.Lifting.Dual AThe dual `A^∨`-coordinate `D^∨_u`.  uQ2Presentation.Lifting.HeisQ A.vQ2Presentation.Lifting.HeisQ.v.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A]
  (self : Q2Presentation.Lifting.HeisQ A) : AThe primal `A`-coordinate `D_u`.  }Q2Presentation.Lifting.HeisQ.mk.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A] (v : A)
  (dl : Q2Presentation.Lifting.Dual A) (z : ZMod 2) : Q2Presentation.Lifting.HeisQ A

theorem Q2Presentation.Lifting.d1_comp_d0_ofRep_tameFactor.{u_1, u_2}
  {AType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  AType u_1] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) AType u_1] {CType u_2 : Type u_2A 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.
 CType u_2] (ρC →* Module.End (ZMod 2) A : CType u_2 →*MonoidHom.{u_10, u_11} (M : Type u_10) (N : Type u_11) [MulOne M] [MulOne N] : Type (max u_10 u_11)`M →* N` is the type of functions `M → N` that preserve the `MulOne` structure.
`MonoidHom` is used for both monoid and group homomorphisms.

When possible, instead of parametrizing results over `(f : M →* N)`,
you should parametrize over `(F : Type*) [MonoidHomClass F M N] (f : F)`.

When you extend this structure, make sure to extend `MonoidHomClass`.
 Module.EndModule.End.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vLinear endomorphisms of a module, with associated ring structure
`Module.End.semiring` and algebra structure `Module.End.algebra`.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) AType u_1) (sC tC x₀C x₁C : CType u_2)
  (hrels⁻¹ * t * s = t ^ 2 : sC⁻¹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`. tC *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`. sC =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`. tC ^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) (hx1ρ x₁ = 1 : ρC →* Module.End (ZMod 2) A x₁C =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) :
  Q2Presentation.Lifting.d1Q2Presentation.Lifting.d1.{u_1} {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] (Sinv T P : Module.End (ZMod 2) A) :
  A × A × A × A →ₗ[ZMod 2] A × AThe candidate `d¹`, the evaluated Fox Jacobian (manuscript `lem:jacobian`,
eq:simplejac): tame row `(S⁻¹(1+T), S⁻¹+1+T, 0, 0)` and wild row
`(0, P, 0, P+S⁻¹)`, where `P` is the norm of `⟨T⟩` and `Sinv = S⁻¹`.  (ρC →* Module.End (ZMod 2) A sC⁻¹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`.) (ρC →* Module.End (ZMod 2) A tC)
        (Q2Presentation.Lifting.repNormQ2Presentation.Lifting.repNorm.{u_1, u_2} {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] {C : Type u_2} [Group C]
  (ρ : C →* Module.End (ZMod 2) A) (t : C) : Module.End (ZMod 2) AThe norm element `P = 1 + (ρ t) + ⋯ + (ρ t)^{e-1}` of the cyclic group `⟨ρ t⟩`,
`e = orderOf t`.  ρC →* Module.End (ZMod 2) A tC) ∘ₗLinearMap.comp.{u_2, u_3, u_4, u_9, u_10, u_11} {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9}
  {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂]
  [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) :
  M₁ →ₛₗ[σ₁₃] M₃Composition of two linear maps is a linear map 
      Q2Presentation.Lifting.d0Q2Presentation.Lifting.d0.{u_1} {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A]
  (S T X₀ X₁ : Module.End (ZMod 2) A) : A →ₗ[ZMod 2] A × A × A × AThe candidate `d⁰` (manuscript eq:d0explicit):
`v ↦ ((S-1)v, (T-1)v, (X₀-1)v, (X₁-1)v)`.  (ρC →* Module.End (ZMod 2) A sC) (ρC →* Module.End (ZMod 2) A tC) (ρC →* Module.End (ZMod 2) A x₀C) (ρC →* Module.End (ZMod 2) A x₁C) =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`.
    0

theorem Q2Presentation.Quadratic.Extraspecial.extraspecialForm_eq_heisSquare.{u_1}
  {VType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType u_1] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) VType u_1]
  (φV →ₗ[ZMod 2] Module.Dual (ZMod 2) V : VType u_1 →ₗ[LinearMap.{u_14, u_15, u_16, u_17} {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (σ : R →+* S)
  (M : Type u_16) (M₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] :
  Type (max u_16 u_17)A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`. Elements of `LinearMap σ M M₂` (available under the notation
`M →ₛₗ[σ] M₂`) are bundled versions of such maps. For plain linear maps (i.e. for which
`σ = RingHom.id R`), the notation `M →ₗ[R] M₂` is available. An unbundled version of plain linear
maps is available with the predicate `IsLinearMap`, but it should be avoided most of the time. ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2]LinearMap.{u_14, u_15, u_16, u_17} {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (σ : R →+* S)
  (M : Type u_16) (M₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] :
  Type (max u_16 u_17)A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`. Elements of `LinearMap σ M M₂` (available under the notation
`M →ₛₗ[σ] M₂`) are bundled versions of such maps. For plain linear maps (i.e. for which
`σ = RingHom.id R`), the notation `M →ₗ[R] M₂` is available. An unbundled version of plain linear
maps is available with the predicate `IsLinearMap`, but it should be avoided most of the time.  Module.DualModule.Dual.{u_4, u_5} (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] : Type (max u_5 u_4)The left dual space of an R-module M is the R-module of linear maps `M → R`.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) VType u_1) (cV : VType u_1) :
  (Q2Presentation.Quadratic.Extraspecial.extraspecialFormQ2Presentation.Quadratic.Extraspecial.extraspecialForm.{u_1} {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V]
  (φ : V →ₗ[ZMod 2] Module.Dual (ZMod 2) V) : Q2Presentation.Quadratic.QuadF2 V**The extraspecial pushout quadratic obstruction** `κ_q^0` as a `QuadF2`:
`form c = φ(c)(c)`, polar form `bcl`.  This is the fibre square map of the central
double cover (l.2043), *proven quadratic* with the commutator polar form.  φV →ₗ[ZMod 2] Module.Dual (ZMod 2) V).formQ2Presentation.Quadratic.QuadF2.form.{u_2} {V : Type u_2} [AddCommGroup V] [Module (ZMod 2) V]
  (self : Q2Presentation.Quadratic.QuadF2 V) : V → ZMod 2the quadratic map `q : V → F₂`  cV =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`.
    (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`.{Q2Presentation.Lifting.HeisQ.mk.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A] (v : A)
  (dl : Q2Presentation.Lifting.Dual A) (z : ZMod 2) : Q2Presentation.Lifting.HeisQ A vVThe primal `A`-coordinate `D_u`.  :=Q2Presentation.Lifting.HeisQ.mk.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A] (v : A)
  (dl : Q2Presentation.Lifting.Dual A) (z : ZMod 2) : Q2Presentation.Lifting.HeisQ A cV,Q2Presentation.Lifting.HeisQ.mk.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A] (v : A)
  (dl : Q2Presentation.Lifting.Dual A) (z : ZMod 2) : Q2Presentation.Lifting.HeisQ A dlModule.Dual (ZMod 2) VThe dual `A^∨`-coordinate `D^∨_u`.  :=Q2Presentation.Lifting.HeisQ.mk.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A] (v : A)
  (dl : Q2Presentation.Lifting.Dual A) (z : ZMod 2) : Q2Presentation.Lifting.HeisQ A φV →ₗ[ZMod 2] Module.Dual (ZMod 2) V cV,Q2Presentation.Lifting.HeisQ.mk.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A] (v : A)
  (dl : Q2Presentation.Lifting.Dual A) (z : ZMod 2) : Q2Presentation.Lifting.HeisQ A zZMod 2The central `F₂`-coordinate `β_u`.  :=Q2Presentation.Lifting.HeisQ.mk.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A] (v : A)
  (dl : Q2Presentation.Lifting.Dual A) (z : ZMod 2) : Q2Presentation.Lifting.HeisQ A 0 }Q2Presentation.Lifting.HeisQ.mk.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A] (v : A)
  (dl : Q2Presentation.Lifting.Dual A) (z : ZMod 2) : Q2Presentation.Lifting.HeisQ A ^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`..zQ2Presentation.Lifting.HeisQ.z.{u_2} {A : Type u_2} [AddCommGroup A] [Module (ZMod 2) A]
  (self : Q2Presentation.Lifting.HeisQ A) : ZMod 2The central `F₂`-coordinate `β_u`. 

theorem Q2Presentation.Lifting.d1_trivial
  (xZMod 2 × ZMod 2 × ZMod 2 × ZMod 2 : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) :
  (Q2Presentation.Lifting.d1Q2Presentation.Lifting.d1.{u_1} {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] (Sinv T P : Module.End (ZMod 2) A) :
  A × A × A × A →ₗ[ZMod 2] A × AThe candidate `d¹`, the evaluated Fox Jacobian (manuscript `lem:jacobian`,
eq:simplejac): tame row `(S⁻¹(1+T), S⁻¹+1+T, 0, 0)` and wild row
`(0, P, 0, P+S⁻¹)`, where `P` is the norm of `⟨T⟩` and `Sinv = S⁻¹`.  1 1 1) xZMod 2 × ZMod 2 × ZMod 2 × ZMod 2 =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`. (Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.xZMod 2 × ZMod 2 × ZMod 2 × ZMod 2.2.1,Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. xZMod 2 × ZMod 2 × ZMod 2 × ZMod 2.2.1)Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.

theorem Q2Presentation.Lifting.betaShadow_natural
  {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. } [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.
 YtQ2Presentation.BoundaryFramedTarget.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ] {VType V'Type : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) VType] [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  V'Type]
  [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) V'Type] {ΦQ2Presentation.Lifting.OperatorFamily Yt V : Q2Presentation.Lifting.OperatorFamilyQ2Presentation.Lifting.OperatorFamily (Yt : Q2Presentation.BoundaryFramedTarget) (V : Type) [AddCommGroup V]
  [Module (ZMod 2) V] : TypeAn operator family with the conjugation antihomomorphism laws.  YtQ2Presentation.BoundaryFramedTarget VType}
  {Φ'Q2Presentation.Lifting.OperatorFamily Yt V' : Q2Presentation.Lifting.OperatorFamilyQ2Presentation.Lifting.OperatorFamily (Yt : Q2Presentation.BoundaryFramedTarget) (V : Type) [AddCommGroup V]
  [Module (ZMod 2) V] : TypeAn operator family with the conjugation antihomomorphism laws.  YtQ2Presentation.BoundaryFramedTarget V'Type}
  {fV →ₗ[ZMod 2] V' : VType →ₗ[LinearMap.{u_14, u_15, u_16, u_17} {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (σ : R →+* S)
  (M : Type u_16) (M₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] :
  Type (max u_16 u_17)A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`. Elements of `LinearMap σ M M₂` (available under the notation
`M →ₛₗ[σ] M₂`) are bundled versions of such maps. For plain linear maps (i.e. for which
`σ = RingHom.id R`), the notation `M →ₗ[R] M₂` is available. An unbundled version of plain linear
maps is available with the predicate `IsLinearMap`, but it should be avoided most of the time. ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2]LinearMap.{u_14, u_15, u_16, u_17} {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (σ : R →+* S)
  (M : Type u_16) (M₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] :
  Type (max u_16 u_17)A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`. Elements of `LinearMap σ M M₂` (available under the notation
`M →ₛₗ[σ] M₂`) are bundled versions of such maps. For plain linear maps (i.e. for which
`σ = RingHom.id R`), the notation `M →ₗ[R] M₂` is available. An unbundled version of plain linear
maps is available with the predicate `IsLinearMap`, but it should be avoided most of the time.  V'Type}
  (hf∀ (y : Yt.Y) (x : V), f ((Φ.op y) x) = (Φ'.op y) (f x) : ∀ (yYt.Y : YtQ2Presentation.BoundaryFramedTarget.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ) (xV : VType), fV →ₗ[ZMod 2] V' ((ΦQ2Presentation.Lifting.OperatorFamily Yt V.opQ2Presentation.Lifting.OperatorFamily.op {Yt : Q2Presentation.BoundaryFramedTarget} {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (self : Q2Presentation.Lifting.OperatorFamily Yt V) : Yt.Y → Module.End (ZMod 2) V yYt.Y) xV) =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.Lifting.OperatorFamily Yt V'.opQ2Presentation.Lifting.OperatorFamily.op {Yt : Q2Presentation.BoundaryFramedTarget} {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (self : Q2Presentation.Lifting.OperatorFamily Yt V) : Yt.Y → Module.End (ZMod 2) V yYt.Y) (fV →ₗ[ZMod 2] V' xV))
  (qQ2Presentation.Marking Yt.Y : 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.  YtQ2Presentation.BoundaryFramedTarget.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ) (nQ2Presentation.Gen → V : Q2Presentation.GenQ2Presentation.Gen : TypeThe four marked generators of the candidate presentation.  → VType)
  (φ'Q2Presentation.Gen → Module.Dual (ZMod 2) V' : Q2Presentation.GenQ2Presentation.Gen : TypeThe four marked generators of the candidate presentation.  → Module.DualModule.Dual.{u_4, u_5} (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] : Type (max u_5 u_4)The left dual space of an R-module M is the R-module of linear maps `M → R`.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) V'Type)
  (wQ2Presentation.GExpr : Q2Presentation.GExprQ2Presentation.GExpr : TypeAbstract syntax for words in the generators: the identity, a generator,
products, inverses, `ℕ`-powers, and the profinite `ω₂`-power. ) :
  Q2Presentation.Lifting.betaShadowQ2Presentation.Lifting.betaShadow {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (Φ : Q2Presentation.Lifting.OperatorFamily Yt V) (q : Q2Presentation.Marking Yt.Y)
  (n : Q2Presentation.Gen → V) (φ : Q2Presentation.Gen → Module.Dual (ZMod 2) V) (w : Q2Presentation.GExpr) : ZMod 2**The mixed central coordinate** — the cup pairing of the word.  Φ'Q2Presentation.Lifting.OperatorFamily Yt V' qQ2Presentation.Marking Yt.Y (fun gQ2Presentation.Gen => fV →ₗ[ZMod 2] V' (nQ2Presentation.Gen → V gQ2Presentation.Gen)) φ'Q2Presentation.Gen → Module.Dual (ZMod 2) V' wQ2Presentation.GExpr =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.Lifting.betaShadowQ2Presentation.Lifting.betaShadow {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (Φ : Q2Presentation.Lifting.OperatorFamily Yt V) (q : Q2Presentation.Marking Yt.Y)
  (n : Q2Presentation.Gen → V) (φ : Q2Presentation.Gen → Module.Dual (ZMod 2) V) (w : Q2Presentation.GExpr) : ZMod 2**The mixed central coordinate** — the cup pairing of the word.  ΦQ2Presentation.Lifting.OperatorFamily Yt V qQ2Presentation.Marking Yt.Y nQ2Presentation.Gen → V (fun gQ2Presentation.Gen => φ'Q2Presentation.Gen → Module.Dual (ZMod 2) V' gQ2Presentation.Gen ∘ₗLinearMap.comp.{u_2, u_3, u_4, u_9, u_10, u_11} {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9}
  {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂]
  [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) :
  M₁ →ₛₗ[σ₁₃] M₃Composition of two linear maps is a linear map  fV →ₗ[ZMod 2] V') wQ2Presentation.GExpr

theorem Q2Presentation.Lifting.traced_stokes
  {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. } [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.
 YtQ2Presentation.BoundaryFramedTarget.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ] {VType : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) VType]
  (ΦQ2Presentation.Lifting.OperatorFamily Yt V : Q2Presentation.Lifting.OperatorFamilyQ2Presentation.Lifting.OperatorFamily (Yt : Q2Presentation.BoundaryFramedTarget) (V : Type) [AddCommGroup V]
  [Module (ZMod 2) V] : TypeAn operator family with the conjugation antihomomorphism laws.  YtQ2Presentation.BoundaryFramedTarget VType)
  (qQ2Presentation.Marking Yt.Y : 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.  YtQ2Presentation.BoundaryFramedTarget.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ) (nQ2Presentation.Gen → V : Q2Presentation.GenQ2Presentation.Gen : TypeThe four marked generators of the candidate presentation.  → VType)
  (hoddOdd (Q2Presentation.omega2Mod (Nat.card Yt.Y)).val : 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`.  (Q2Presentation.omega2ModQ2Presentation.omega2Mod (n : ℕ) : ZMod nThe 2-primary idempotent `ω₂ ∈ Ẑ` reduced modulo `n`: the odd part raised to
`φ` of the 2-part.  It is `≡ 1` modulo the 2-part `ordProj[2] n = 2 ^ (v₂ n)` and
`≡ 0` modulo the odd part `ordCompl[2] n`.  (Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`.  YtQ2Presentation.BoundaryFramedTarget.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. )).valZMod.val {n : ℕ} : ZMod n → ℕ`val a` is a natural number defined as:
- for `a : ZMod 0` it is the absolute value of `a`
- for `a : ZMod n` with `0 < n` it is the least natural number in the equivalence class

See `ZMod.valMinAbs` for a variant that takes values in the integers.
)
  (lamModule.Dual (ZMod 2) V : Module.DualModule.Dual.{u_4, u_5} (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] : Type (max u_5 u_4)The left dual space of an R-module M is the R-module of linear maps `M → R`.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) VType) :
  Q2Presentation.Lifting.betaShadowQ2Presentation.Lifting.betaShadow {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (Φ : Q2Presentation.Lifting.OperatorFamily Yt V) (q : Q2Presentation.Marking Yt.Y)
  (n : Q2Presentation.Gen → V) (φ : Q2Presentation.Gen → Module.Dual (ZMod 2) V) (w : Q2Presentation.GExpr) : ZMod 2**The mixed central coordinate** — the cup pairing of the word.  ΦQ2Presentation.Lifting.OperatorFamily Yt V qQ2Presentation.Marking Yt.Y nQ2Presentation.Gen → V
        (fun gQ2Presentation.Gen => (Q2Presentation.Lifting.dualOpQ2Presentation.Lifting.dualOp {Yt : Q2Presentation.BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V]
  (Φ : Q2Presentation.Lifting.OperatorFamily Yt V) (y : Yt.Y) : Module.Dual (ZMod 2) V →ₗ[ZMod 2] Module.Dual (ZMod 2) VThe dual operator: precomposition with the inverse operator.  ΦQ2Presentation.Lifting.OperatorFamily Yt V (qQ2Presentation.Marking Yt.Y gQ2Presentation.Gen)) lamModule.Dual (ZMod 2) V +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. lamModule.Dual (ZMod 2) V)
        Q2Presentation.Q2Word.tameRelatorQ2Presentation.Q2Word.tameRelator : Q2Presentation.GExprThe tame relator `τ^σ · (τ²)⁻¹` (the relation `τ^σ = τ²`).  +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.
      Q2Presentation.Lifting.betaShadowQ2Presentation.Lifting.betaShadow {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (Φ : Q2Presentation.Lifting.OperatorFamily Yt V) (q : Q2Presentation.Marking Yt.Y)
  (n : Q2Presentation.Gen → V) (φ : Q2Presentation.Gen → Module.Dual (ZMod 2) V) (w : Q2Presentation.GExpr) : ZMod 2**The mixed central coordinate** — the cup pairing of the word.  ΦQ2Presentation.Lifting.OperatorFamily Yt V qQ2Presentation.Marking Yt.Y nQ2Presentation.Gen → V
        (fun gQ2Presentation.Gen => (Q2Presentation.Lifting.dualOpQ2Presentation.Lifting.dualOp {Yt : Q2Presentation.BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V]
  (Φ : Q2Presentation.Lifting.OperatorFamily Yt V) (y : Yt.Y) : Module.Dual (ZMod 2) V →ₗ[ZMod 2] Module.Dual (ZMod 2) VThe dual operator: precomposition with the inverse operator.  ΦQ2Presentation.Lifting.OperatorFamily Yt V (qQ2Presentation.Marking Yt.Y gQ2Presentation.Gen)) lamModule.Dual (ZMod 2) V +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. lamModule.Dual (ZMod 2) V)
        Q2Presentation.Q2Word.wildRelatorQ2Presentation.Q2Word.wildRelator : Q2Presentation.GExprThe wild relator `h₀ · u₁⁻¹ · x₁^σ · c₀` (the relation `h₀ u₁⁻¹ x₁^σ c₀ = 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`.
    lamModule.Dual (ZMod 2) V
        ((ΦQ2Presentation.Lifting.OperatorFamily Yt V.opQ2Presentation.Lifting.OperatorFamily.op {Yt : Q2Presentation.BoundaryFramedTarget} {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (self : Q2Presentation.Lifting.OperatorFamily Yt V) : Yt.Y → Module.End (ZMod 2) V (Q2Presentation.Q2Word.tameRelatorQ2Presentation.Q2Word.tameRelator : Q2Presentation.GExprThe tame relator `τ^σ · (τ²)⁻¹` (the relation `τ^σ = τ²`). .evalQ2Presentation.GExpr.eval.{u_1} {G : Type u_1} [Group G] [Finite G] :
  Q2Presentation.GExpr → Q2Presentation.Marking G → GEvaluate a `GExpr` in a finite group `G` under a marking `q : Gen → G`.
The `powOmega2` case is the finite `ω₂`-power `Q2Presentation.powOmega2`.  qQ2Presentation.Marking Yt.Y)⁻¹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`.)
          (Q2Presentation.Lifting.foxShadowGenQ2Presentation.Lifting.foxShadowGen {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (Φ : Yt.Y → Module.End (ZMod 2) V) (q : Q2Presentation.Marking Yt.Y)
  (n : Q2Presentation.Gen → V) : Q2Presentation.GExpr → VThe shadow recursion over an abstract operator family.  ΦQ2Presentation.Lifting.OperatorFamily Yt V.opQ2Presentation.Lifting.OperatorFamily.op {Yt : Q2Presentation.BoundaryFramedTarget} {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (self : Q2Presentation.Lifting.OperatorFamily Yt V) : Yt.Y → Module.End (ZMod 2) V qQ2Presentation.Marking Yt.Y nQ2Presentation.Gen → V
            Q2Presentation.Q2Word.tameRelatorQ2Presentation.Q2Word.tameRelator : Q2Presentation.GExprThe tame relator `τ^σ · (τ²)⁻¹` (the relation `τ^σ = τ²`). )) +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.
      lamModule.Dual (ZMod 2) V
        ((ΦQ2Presentation.Lifting.OperatorFamily Yt V.opQ2Presentation.Lifting.OperatorFamily.op {Yt : Q2Presentation.BoundaryFramedTarget} {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (self : Q2Presentation.Lifting.OperatorFamily Yt V) : Yt.Y → Module.End (ZMod 2) V (Q2Presentation.Q2Word.wildRelatorQ2Presentation.Q2Word.wildRelator : Q2Presentation.GExprThe wild relator `h₀ · u₁⁻¹ · x₁^σ · c₀` (the relation `h₀ u₁⁻¹ x₁^σ c₀ = 1`). .evalQ2Presentation.GExpr.eval.{u_1} {G : Type u_1} [Group G] [Finite G] :
  Q2Presentation.GExpr → Q2Presentation.Marking G → GEvaluate a `GExpr` in a finite group `G` under a marking `q : Gen → G`.
The `powOmega2` case is the finite `ω₂`-power `Q2Presentation.powOmega2`.  qQ2Presentation.Marking Yt.Y)⁻¹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`.)
          (Q2Presentation.Lifting.foxShadowGenQ2Presentation.Lifting.foxShadowGen {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (Φ : Yt.Y → Module.End (ZMod 2) V) (q : Q2Presentation.Marking Yt.Y)
  (n : Q2Presentation.Gen → V) : Q2Presentation.GExpr → VThe shadow recursion over an abstract operator family.  ΦQ2Presentation.Lifting.OperatorFamily Yt V.opQ2Presentation.Lifting.OperatorFamily.op {Yt : Q2Presentation.BoundaryFramedTarget} {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (self : Q2Presentation.Lifting.OperatorFamily Yt V) : Yt.Y → Module.End (ZMod 2) V qQ2Presentation.Marking Yt.Y nQ2Presentation.Gen → V
            Q2Presentation.Q2Word.wildRelatorQ2Presentation.Q2Word.wildRelator : Q2Presentation.GExprThe wild relator `h₀ · u₁⁻¹ · x₁^σ · c₀` (the relation `h₀ u₁⁻¹ x₁^σ c₀ = 1`). ))

theorem Q2Presentation.Induction.levelTrace_add
  (AQ2Presentation.AdmissibleIndex : Q2Presentation.AdmissibleIndexQ2Presentation.AdmissibleIndex : TypeA concrete admissible marked finite group with carrier the skeleton `Fin n`.

Fixing the carrier to `Fin n` (rather than an arbitrary finite type) keeps the
index category used to build `Γ_A` small.  The fields are the size `n`, a proof
that the carrier is nonempty (`0 < n`), the group structure `groupFin`, the
marking `q`, and a proof that `q` is `Admissible` for that structure. )
  (zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 :
    (Q2Presentation.Induction.levelBaseQ2Presentation.Induction.levelBase (A : Q2Presentation.AdmissibleIndex) : Q2Presentation.BoundaryFramedTarget AQ2Presentation.AdmissibleIndex).YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`.  →
      (Q2Presentation.Induction.levelBaseQ2Presentation.Induction.levelBase (A : Q2Presentation.AdmissibleIndex) : Q2Presentation.BoundaryFramedTarget AQ2Presentation.AdmissibleIndex).YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`.  → ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2)
  (h11∀ (y : (Q2Presentation.Induction.levelBase A).Y), zeta₁ 1 y = 0 :
    ∀ (y(Q2Presentation.Induction.levelBase A).Y : (Q2Presentation.Induction.levelBaseQ2Presentation.Induction.levelBase (A : Q2Presentation.AdmissibleIndex) : Q2Presentation.BoundaryFramedTarget AQ2Presentation.AdmissibleIndex).YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ), zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 1 y(Q2Presentation.Induction.levelBase A).Y =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`. 0)
  (h12∀ (y : (Q2Presentation.Induction.levelBase A).Y), zeta₁ y 1 = 0 :
    ∀ (y(Q2Presentation.Induction.levelBase A).Y : (Q2Presentation.Induction.levelBaseQ2Presentation.Induction.levelBase (A : Q2Presentation.AdmissibleIndex) : Q2Presentation.BoundaryFramedTarget AQ2Presentation.AdmissibleIndex).YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ), zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 y(Q2Presentation.Induction.levelBase A).Y 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`. 0)
  (h1c∀ (a b c : (Q2Presentation.Induction.levelBase A).Y), zeta₁ a b + zeta₁ (a * b) c = zeta₁ b c + zeta₁ a (b * c) :
    ∀ (a(Q2Presentation.Induction.levelBase A).Y b(Q2Presentation.Induction.levelBase A).Y c(Q2Presentation.Induction.levelBase A).Y : (Q2Presentation.Induction.levelBaseQ2Presentation.Induction.levelBase (A : Q2Presentation.AdmissibleIndex) : Q2Presentation.BoundaryFramedTarget AQ2Presentation.AdmissibleIndex).YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ),
      zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 a(Q2Presentation.Induction.levelBase A).Y b(Q2Presentation.Induction.levelBase A).Y +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 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`.a(Q2Presentation.Induction.levelBase A).Y *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`. b(Q2Presentation.Induction.levelBase A).Y)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`. c(Q2Presentation.Induction.levelBase A).Y =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`. zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 b(Q2Presentation.Induction.levelBase A).Y c(Q2Presentation.Induction.levelBase A).Y +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 a(Q2Presentation.Induction.levelBase A).Y (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`.b(Q2Presentation.Induction.levelBase A).Y *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`. c(Q2Presentation.Induction.levelBase A).Y)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`.)
  (zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 :
    (Q2Presentation.Induction.levelBaseQ2Presentation.Induction.levelBase (A : Q2Presentation.AdmissibleIndex) : Q2Presentation.BoundaryFramedTarget AQ2Presentation.AdmissibleIndex).YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`.  →
      (Q2Presentation.Induction.levelBaseQ2Presentation.Induction.levelBase (A : Q2Presentation.AdmissibleIndex) : Q2Presentation.BoundaryFramedTarget AQ2Presentation.AdmissibleIndex).YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`.  → ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2)
  (h21∀ (y : (Q2Presentation.Induction.levelBase A).Y), zeta₂ 1 y = 0 :
    ∀ (y(Q2Presentation.Induction.levelBase A).Y : (Q2Presentation.Induction.levelBaseQ2Presentation.Induction.levelBase (A : Q2Presentation.AdmissibleIndex) : Q2Presentation.BoundaryFramedTarget AQ2Presentation.AdmissibleIndex).YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ), zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 1 y(Q2Presentation.Induction.levelBase A).Y =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`. 0)
  (h22∀ (y : (Q2Presentation.Induction.levelBase A).Y), zeta₂ y 1 = 0 :
    ∀ (y(Q2Presentation.Induction.levelBase A).Y : (Q2Presentation.Induction.levelBaseQ2Presentation.Induction.levelBase (A : Q2Presentation.AdmissibleIndex) : Q2Presentation.BoundaryFramedTarget AQ2Presentation.AdmissibleIndex).YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ), zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 y(Q2Presentation.Induction.levelBase A).Y 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`. 0)
  (h2c∀ (a b c : (Q2Presentation.Induction.levelBase A).Y), zeta₂ a b + zeta₂ (a * b) c = zeta₂ b c + zeta₂ a (b * c) :
    ∀ (a(Q2Presentation.Induction.levelBase A).Y b(Q2Presentation.Induction.levelBase A).Y c(Q2Presentation.Induction.levelBase A).Y : (Q2Presentation.Induction.levelBaseQ2Presentation.Induction.levelBase (A : Q2Presentation.AdmissibleIndex) : Q2Presentation.BoundaryFramedTarget AQ2Presentation.AdmissibleIndex).YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ),
      zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 a(Q2Presentation.Induction.levelBase A).Y b(Q2Presentation.Induction.levelBase A).Y +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 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`.a(Q2Presentation.Induction.levelBase A).Y *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`. b(Q2Presentation.Induction.levelBase A).Y)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`. c(Q2Presentation.Induction.levelBase A).Y =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`. zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 b(Q2Presentation.Induction.levelBase A).Y c(Q2Presentation.Induction.levelBase A).Y +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 a(Q2Presentation.Induction.levelBase A).Y (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`.b(Q2Presentation.Induction.levelBase A).Y *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`. c(Q2Presentation.Induction.levelBase A).Y)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`.)
  (h121∀ (y : (Q2Presentation.Induction.levelBase A).Y), (fun u v => zeta₁ u v + zeta₂ u v) 1 y = 0 :
    ∀ (y(Q2Presentation.Induction.levelBase A).Y : (Q2Presentation.Induction.levelBaseQ2Presentation.Induction.levelBase (A : Q2Presentation.AdmissibleIndex) : Q2Presentation.BoundaryFramedTarget AQ2Presentation.AdmissibleIndex).YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ),
      (fun u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y => zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y) 1 y(Q2Presentation.Induction.levelBase A).Y =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`. 0)
  (h122∀ (y : (Q2Presentation.Induction.levelBase A).Y), (fun u v => zeta₁ u v + zeta₂ u v) y 1 = 0 :
    ∀ (y(Q2Presentation.Induction.levelBase A).Y : (Q2Presentation.Induction.levelBaseQ2Presentation.Induction.levelBase (A : Q2Presentation.AdmissibleIndex) : Q2Presentation.BoundaryFramedTarget AQ2Presentation.AdmissibleIndex).YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ),
      (fun u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y => zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y) y(Q2Presentation.Induction.levelBase A).Y 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`. 0)
  (h12c∀ (a b c : (Q2Presentation.Induction.levelBase A).Y),
  (fun u v => zeta₁ u v + zeta₂ u v) a b + (fun u v => zeta₁ u v + zeta₂ u v) (a * b) c =
    (fun u v => zeta₁ u v + zeta₂ u v) b c + (fun u v => zeta₁ u v + zeta₂ u v) a (b * c) :
    ∀ (a(Q2Presentation.Induction.levelBase A).Y b(Q2Presentation.Induction.levelBase A).Y c(Q2Presentation.Induction.levelBase A).Y : (Q2Presentation.Induction.levelBaseQ2Presentation.Induction.levelBase (A : Q2Presentation.AdmissibleIndex) : Q2Presentation.BoundaryFramedTarget AQ2Presentation.AdmissibleIndex).YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ),
      (fun u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y => zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y) a(Q2Presentation.Induction.levelBase A).Y b(Q2Presentation.Induction.levelBase A).Y +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.
          (fun u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y => zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y) (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`.a(Q2Presentation.Induction.levelBase A).Y *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`. b(Q2Presentation.Induction.levelBase A).Y)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`. c(Q2Presentation.Induction.levelBase A).Y =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`.
        (fun u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y => zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y) b(Q2Presentation.Induction.levelBase A).Y c(Q2Presentation.Induction.levelBase A).Y +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.
          (fun u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y => zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y) a(Q2Presentation.Induction.levelBase A).Y (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`.b(Q2Presentation.Induction.levelBase A).Y *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`. c(Q2Presentation.Induction.levelBase A).Y)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.Induction.levelTraceQ2Presentation.Induction.levelTrace (A : Q2Presentation.AdmissibleIndex)
  (zeta : (Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2)
  (hz1 : ∀ (y : (Q2Presentation.Induction.levelBase A).Y), zeta 1 y = 0)
  (hz2 : ∀ (y : (Q2Presentation.Induction.levelBase A).Y), zeta y 1 = 0)
  (hzc : ∀ (a b c : (Q2Presentation.Induction.levelBase A).Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) :
  ZMod 2**The candidate level trace** `ι_A(ζ)` (the `prop:chainmap` trace,
l.1687): the sum of the scalar reads of the two marked relators, evaluated
in the ζ-extension at the canonical marking.  `levelTrace_eq_of_base` shows
it is marking-independent; `cochainSolvable_iff_levelTrace_eq_zero` shows it
is THE solvability functional.  AQ2Presentation.AdmissibleIndex
      (fun u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y => zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 u(Q2Presentation.Induction.levelBase A).Y v(Q2Presentation.Induction.levelBase A).Y) h121∀ (y : (Q2Presentation.Induction.levelBase A).Y), (fun u v => zeta₁ u v + zeta₂ u v) 1 y = 0 h122∀ (y : (Q2Presentation.Induction.levelBase A).Y), (fun u v => zeta₁ u v + zeta₂ u v) y 1 = 0 h12c∀ (a b c : (Q2Presentation.Induction.levelBase A).Y),
  (fun u v => zeta₁ u v + zeta₂ u v) a b + (fun u v => zeta₁ u v + zeta₂ u v) (a * b) c =
    (fun u v => zeta₁ u v + zeta₂ u v) b c + (fun u v => zeta₁ u v + zeta₂ u v) a (b * c) =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.levelTraceQ2Presentation.Induction.levelTrace (A : Q2Presentation.AdmissibleIndex)
  (zeta : (Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2)
  (hz1 : ∀ (y : (Q2Presentation.Induction.levelBase A).Y), zeta 1 y = 0)
  (hz2 : ∀ (y : (Q2Presentation.Induction.levelBase A).Y), zeta y 1 = 0)
  (hzc : ∀ (a b c : (Q2Presentation.Induction.levelBase A).Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) :
  ZMod 2**The candidate level trace** `ι_A(ζ)` (the `prop:chainmap` trace,
l.1687): the sum of the scalar reads of the two marked relators, evaluated
in the ζ-extension at the canonical marking.  `levelTrace_eq_of_base` shows
it is marking-independent; `cochainSolvable_iff_levelTrace_eq_zero` shows it
is THE solvability functional.  AQ2Presentation.AdmissibleIndex zeta₁(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 h11∀ (y : (Q2Presentation.Induction.levelBase A).Y), zeta₁ 1 y = 0 h12∀ (y : (Q2Presentation.Induction.levelBase A).Y), zeta₁ y 1 = 0 h1c∀ (a b c : (Q2Presentation.Induction.levelBase A).Y), zeta₁ a b + zeta₁ (a * b) c = zeta₁ b c + zeta₁ a (b * c) +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.
      Q2Presentation.Induction.levelTraceQ2Presentation.Induction.levelTrace (A : Q2Presentation.AdmissibleIndex)
  (zeta : (Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2)
  (hz1 : ∀ (y : (Q2Presentation.Induction.levelBase A).Y), zeta 1 y = 0)
  (hz2 : ∀ (y : (Q2Presentation.Induction.levelBase A).Y), zeta y 1 = 0)
  (hzc : ∀ (a b c : (Q2Presentation.Induction.levelBase A).Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) :
  ZMod 2**The candidate level trace** `ι_A(ζ)` (the `prop:chainmap` trace,
l.1687): the sum of the scalar reads of the two marked relators, evaluated
in the ζ-extension at the canonical marking.  `levelTrace_eq_of_base` shows
it is marking-independent; `cochainSolvable_iff_levelTrace_eq_zero` shows it
is THE solvability functional.  AQ2Presentation.AdmissibleIndex zeta₂(Q2Presentation.Induction.levelBase A).Y → (Q2Presentation.Induction.levelBase A).Y → ZMod 2 h21∀ (y : (Q2Presentation.Induction.levelBase A).Y), zeta₂ 1 y = 0 h22∀ (y : (Q2Presentation.Induction.levelBase A).Y), zeta₂ y 1 = 0 h2c∀ (a b c : (Q2Presentation.Induction.levelBase A).Y), zeta₂ a b + zeta₂ (a * b) c = zeta₂ b c + zeta₂ a (b * c)