-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : isGood (π C fun (x : I) ↦ ord I x < o₁) l
hl' :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₂)) {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o₂) l)
rwa :
  ∀
    (hl' :
      Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ))
        (span ℤ
          ((⇑(πs' C h) :
              (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) ''
            Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
        (eval (π C fun (x : I) ↦ ord I x < o₂) l)),
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ))
      (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
      (eval (π C fun (x : I) ↦ ord I x < o₁) l)
rwa₁ :
  ∀
    (hl' :
      Membership.mem (α := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) (γ :=
        Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ))
        (span ℤ
          ((⇑(πs' C h) :
              (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) ''
            Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
        ((πs' C h :
              (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
            (eval (π C fun (x : I) ↦ ord I x < o₁) l) :
          LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)),
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ))
      (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
      (eval (π C fun (x : I) ↦ ord I x < o₁) l)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (hl' :
      Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ))
        (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
        (eval (π C fun (x : I) ↦ ord I x < o₁) l)),
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ))
      (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
      (eval (π C fun (x : I) ↦ ord I x < o₁) l)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o₁)) {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o₁) l)

Tactic:
rwa [eval_πs_image' C h (prop_of_isGood C _ hl), ← eval_πs' C h (prop_of_isGood C _ hl),
    Submodule.apply_mem_span_image_iff_mem_span (injective_πs' C h)] at hl'

Premises used: Profinite.NobelingProof.injective_πs', Profinite.NobelingProof.Products.eval_πs', Submodule.apply_mem_span_image_iff_mem_span, Profinite.NobelingProof.Products.eval_πs_image', Profinite.NobelingProof.Products.prop_of_isGood