-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f :
  ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i : IntermediateField F E) →ₐ[F] Ē
h : ¬Nonempty.{v + 1} (↑(Iio i) : Type v)
neg :
  ∀ («b» : F),
    Eq (α := Ē)
      (((fun
                  (f :
                    (↑(limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
                          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
                                IntermediateField F E) →ₐ[F]
                            Ē)
                          (embFunctor F E) i) :
                      Type v)) ↦
                (AlgHom.comp (Algebra.ofId F Ē)
                    (↑(AlgEquiv.trans (equivOfEq ⋯) (botEquiv F E)) :
                      ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i) →ₐ[F] F) :
                  ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i :
                        IntermediateField F E) →ₐ[F]
                    Ē))
              ((fun
                    (f :
                      ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i :
                            IntermediateField F E) →ₐ[F]
                        Ē) ↦
                  (Subtype.mk (p :=
                      fun
                        (x :
                          (l : (↑(Iio i) : Type v)) →
                            ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                    (↑l : WithTop (Module.rank F E).ord.ToType) :
                                  IntermediateField F E) →ₐ[F]
                              Ē) ↦
                      Membership.mem (γ :=
                        Set
                          ((l : (↑(Iio i) : Type v)) →
                            ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                    (↑l : WithTop (Module.rank F E).ord.ToType) :
                                  IntermediateField F E) →ₐ[F]
                              Ē))
                        (limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
                          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
                                IntermediateField F E) →ₐ[F]
                            Ē)
                          (embFunctor F E) i)
                        x)
                      (fun (j : (↑(Iio i) : Type v)) ↦ embFunctor F E ⋯ f) ⋯ :
                    { x :
                      (l : (↑(Iio i) : Type v)) →
                        ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                (↑l : WithTop (Module.rank F E).ord.ToType) :
                              IntermediateField F E) →ₐ[F]
                          Ē //
                      Membership.mem (γ :=
                        Set
                          ((l : (↑(Iio i) : Type v)) →
                            ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                    (↑l : WithTop (Module.rank F E).ord.ToType) :
                                  IntermediateField F E) →ₐ[F]
                              Ē))
                        (limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
                          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
                                IntermediateField F E) →ₐ[F]
                            Ē)
                          (embFunctor F E) i)
                        x }))
                f) :
            (a : ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) → Ē)
          (((Equiv.symm (AlgEquiv.toEquiv (AlgEquiv.trans (equivOfEq ⋯) (botEquiv F E))) :
                Equiv.{u + 1, v + 1} F
                  ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i :
                      IntermediateField F E)) :
              (a : F) → ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i))
            «b») :
        Ē)
      ((f : (a : ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) → Ē)
          (((Equiv.symm (AlgEquiv.toEquiv (AlgEquiv.trans (equivOfEq ⋯) (botEquiv F E))) :
                Equiv.{u + 1, v + 1} F
                  ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i :
                      IntermediateField F E)) :
              (a : F) → ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i))
            «b») :
        Ē)
⊢ ∀
    (x :
      ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i : IntermediateField F E)),
    Eq (α := Ē)
      (((fun
                  (f :
                    (↑(limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
                          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
                                IntermediateField F E) →ₐ[F]
                            Ē)
                          (embFunctor F E) i) :
                      Type v)) ↦
                (AlgHom.comp (Algebra.ofId F Ē)
                    (↑(AlgEquiv.trans (equivOfEq ⋯) (botEquiv F E)) :
                      ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i) →ₐ[F] F) :
                  ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i :
                        IntermediateField F E) →ₐ[F]
                    Ē))
              ((fun
                    (f :
                      ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i :
                            IntermediateField F E) →ₐ[F]
                        Ē) ↦
                  (Subtype.mk (p :=
                      fun
                        (x :
                          (l : (↑(Iio i) : Type v)) →
                            ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                    (↑l : WithTop (Module.rank F E).ord.ToType) :
                                  IntermediateField F E) →ₐ[F]
                              Ē) ↦
                      Membership.mem (γ :=
                        Set
                          ((l : (↑(Iio i) : Type v)) →
                            ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                    (↑l : WithTop (Module.rank F E).ord.ToType) :
                                  IntermediateField F E) →ₐ[F]
                              Ē))
                        (limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
                          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
                                IntermediateField F E) →ₐ[F]
                            Ē)
                          (embFunctor F E) i)
                        x)
                      (fun (j : (↑(Iio i) : Type v)) ↦ embFunctor F E ⋯ f) ⋯ :
                    { x :
                      (l : (↑(Iio i) : Type v)) →
                        ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                (↑l : WithTop (Module.rank F E).ord.ToType) :
                              IntermediateField F E) →ₐ[F]
                          Ē //
                      Membership.mem (γ :=
                        Set
                          ((l : (↑(Iio i) : Type v)) →
                            ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                    (↑l : WithTop (Module.rank F E).ord.ToType) :
                                  IntermediateField F E) →ₐ[F]
                              Ē))
                        (limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
                          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
                                IntermediateField F E) →ₐ[F]
                            Ē)
                          (embFunctor F E) i)
                        x }))
                f) :
            (a : ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) → Ē)
          x :
        Ē)
      ((f : (a : ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) → Ē) x : Ē)

Tactic:
rw [((equivOfEq (eq_bot_of_not_nonempty hi h)).trans <| botEquiv F E).forall_congr_left]

Premises used: Equiv.forall_congr_left, IntermediateField.equivOfEq, Field.Emb.Cardinal.eq_bot_of_not_nonempty, AlgEquiv.trans, AlgEquiv.toEquiv, IntermediateField.botEquiv