-- Mathlib/NumberTheory/Dioph.lean
theorem diophFn_compn :
    ∀ {n} {S : Set (α ⊕ (Fin2 n) → ℕ)} (_ : Dioph S) {f : Vector3 ((α → ℕ) → ℕ) n}
      (_ : VectorAllP DiophFn f), Dioph {v : α → ℕ | (v ⊗ fun i => f i v) ∈ S}
  | 0, S, d, f => fun _ =>
    ext (reindex_dioph _ (id ⊗ Fin2.elim0) d) fun v => by
      dsimp
      -- Porting note: `congr` use to be enough here
      suffices v ∘ (id ⊗ elim0) = v ⊗ fun i ↦ f i v by rw [this]
      ext x; obtain _ | _ | _ := x; rfl
  | succ n, S, d, f =>
    f.consElim fun f fl => by
        simp only [vectorAllP_cons, and_imp]
        exact fun df dfl =>
          have : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl)::v ∘ inr) ∈ S} :=
            ext (diophFn_comp1 (reindex_dioph _ (some ∘ inl ⊗ none::some ∘ inr) d) <|
                reindex_diophFn inl df)
              fun v => by
                dsimp
                -- Porting note: `congr` use to be enough here
                suffices (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) =
                    v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr by rw [this]
                ext x; obtain _ | _ | _ := x <;> rfl
          have : Dioph {v | (v ⊗ f v::fun i : Fin2 n => fl i v) ∈ S} :=
            @diophFn_compn n (fun v => S (v ∘ inl ⊗ f (v ∘ inl)::v ∘ inr)) this _ dfl
          ext this fun v => by
            dsimp
            -- Porting note: `congr` use to be enough here
            suffices (v ⊗ f v :: fun i ↦ fl i v) = v ⊗ fun i ↦ (f :: fl) i v by rw [this]
            ext x; obtain _ | _ | _ := x <;> rfl

Proof state:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
⊢ DiophFn f → VectorAllP DiophFn fl → Dioph {v | (v ⊗ fun i => (f :: fl) i v) ∈ S}

Tactic:
exact fun df dfl =>
  have : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl)::v ∘ inr) ∈ S} :=
    ext (diophFn_comp1 (reindex_dioph _ (some ∘ inl ⊗ none::some ∘ inr) d) <|
        reindex_diophFn inl df)
      fun v => by
        dsimp
        suffices (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) =
            v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr by rw [this]
        ext x; obtain _ | _ | _ := x <;> rfl
  have : Dioph {v | (v ⊗ f v::fun i : Fin2 n => fl i v) ∈ S} :=
    @diophFn_compn n (fun v => S (v ∘ inl ⊗ f (v ∘ inl)::v ∘ inr)) this _ dfl
  ext this fun v => by
    dsimp
    suffices (v ⊗ f v :: fun i ↦ fl i v) = v ⊗ fun i ↦ (f :: fl) i v by rw [this]
    ext x; obtain _ | _ | _ := x <;> rfl

Result:
no goals

Proof state:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
⊢ v ∘ (id ⊗ elim0) = v ⊗ fun i => f i v

Tactic:
ext x

Result:
case h
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
x : α ⊕ Fin2 0
⊢ (v ∘ (id ⊗ elim0)) x = (v ⊗ fun i => f i v) x

Proof state:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
⊢ v ∘ (id ⊗ elim0) ∈ S ↔ (v ⊗ fun i => f i v) ∈ S

Tactic:
suffices v ∘ (id ⊗ elim0) = v ⊗ fun i ↦ f i v by rw [this]

Result:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
⊢ v ∘ (id ⊗ elim0) = v ⊗ fun i => f i v

Proof state:
case h
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
x : α ⊕ Fin2 0
⊢ (v ∘ (id ⊗ elim0)) x = (v ⊗ fun i => f i v) x

Tactic:
obtain _ | _ | _ := x

Result:
case h.inl
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
val✝ : α
⊢ (v ∘ (id ⊗ elim0)) (inl val✝) = (v ⊗ fun i => f i v) (inl val✝)

Proof state:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i => fl i v) ∈ S}
v : α → ℕ
⊢ (v ⊗ f v :: fun i => fl i v) = v ⊗ fun i => (f :: fl) i v

Tactic:
ext x

Result:
case h
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i => fl i v) ∈ S}
v : α → ℕ
x : α ⊕ Fin2 (n + 1)
⊢ (v ⊗ f v :: fun i => fl i v) x = (v ⊗ fun i => (f :: fl) i v) x

Proof state:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
this : v ∘ (id ⊗ elim0) = v ⊗ fun i => f i v
⊢ v ∘ (id ⊗ elim0) ∈ S ↔ (v ⊗ fun i => f i v) ∈ S

Tactic:
rw [this]

Result:
no goals

Proof state:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
⊢ (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) ∈ S ↔ (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S

Tactic:
suffices (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) =
    v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr by rw [this]

Result:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
⊢ (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) = v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr

Proof state:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
this : (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) = v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr
⊢ (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) ∈ S ↔ (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S

Tactic:
rw [this]

Result:
no goals

Proof state:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
⊢ v ∈ {v | v ∘ (id ⊗ elim0) ∈ S} ↔ v ∈ {v | (v ⊗ fun i => f i v) ∈ S}

Tactic:
dsimp

Result:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
⊢ v ∘ (id ⊗ elim0) ∈ S ↔ (v ⊗ fun i => f i v) ∈ S

Proof state:
case h
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i => fl i v) ∈ S}
v : α → ℕ
x : α ⊕ Fin2 (n + 1)
⊢ (v ⊗ f v :: fun i => fl i v) x = (v ⊗ fun i => (f :: fl) i v) x

Tactic:
obtain _ | _ | _ := x <;> rfl

Result:
no goals

Proof state:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝¹ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this✝ : Dioph {v | (v ⊗ f v :: fun i => fl i v) ∈ S}
v : α → ℕ
this : (v ⊗ f v :: fun i => fl i v) = v ⊗ fun i => (f :: fl) i v
⊢ (v ⊗ f v :: fun i => fl i v) ∈ S ↔ (v ⊗ fun i => (f :: fl) i v) ∈ S

Tactic:
rw [this]

Result:
no goals

Proof state:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
⊢ VectorAllP DiophFn (f :: fl) → Dioph {v | (v ⊗ fun i => (f :: fl) i v) ∈ S}

Tactic:
simp only [vectorAllP_cons, and_imp]

Result:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
⊢ DiophFn f → VectorAllP DiophFn fl → Dioph {v | (v ⊗ fun i => (f :: fl) i v) ∈ S}