awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
i : AlgEquiv.{u, w, v} F L ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
x : E
e_s :
  (∃ (y : L), (algebraMap L E : (a : L) → E) y = x) ↔
    ∃ (a : E) (b : a ∈ L'), (algebraMap (↥L') E : (a : ↥L') → E) (Subtype.mk (p := fun (a : E) ↦ a ∈ L') a b) = x
⊢ Membership.mem (γ := Set E) (Set.range.{v, w + 1} (ι := L) (⇑(algebraMap L E) : (a : L) → E)) x ↔
    Membership.mem (γ := Set E) (Set.range (ι := ↥L') (⇑(algebraMap (↥L') E) : (a : ↥L') → E)) x

Tactic:
simp only [Set.mem_range, Subtype.exists]

Premises used: Set.mem_range, Subtype.exists
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
i : AlgEquiv.{u, w, v} F L ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
x : E
⊢ (∃ (y : L), (algebraMap L E : (a : L) → E) y = x) ↔
    ∃ (a : E) (b : a ∈ L'), (algebraMap (↥L') E : (a : ↥L') → E) (Subtype.mk (p := fun (a : E) ↦ a ∈ L') a b) = x

Tactic:
⟨fun ⟨y, h⟩ ↦ ⟨x, ⟨y, h⟩, rfl⟩, fun ⟨a, ⟨y, h1⟩, h2⟩ ↦ ⟨y, h1.trans h2⟩⟩

Premises used: Algebra.algebraMap, _private.0.IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic.match_3, Membership.mem, Exists, Subtype, Subtype.mk, _private.0.IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic.match_2, Iff.intro, Exists.intro, Eq, DFunLike.coe, rfl, Eq.trans
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
i : AlgEquiv.{u, w, v} F L ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
x : E
⊢ (∃ (y : L), (algebraMap L E : (a : L) → E) y = x) ↔
    ∃ (a : E) (b : a ∈ L'), (algebraMap (↥L') E : (a : ↥L') → E) (Subtype.mk (p := fun (a : E) ↦ a ∈ L') a b) = x

Tactic:
exact ⟨fun ⟨y, h⟩ ↦ ⟨x, ⟨y, h⟩, rfl⟩, fun ⟨a, ⟨y, h1⟩, h2⟩ ↦ ⟨y, h1.trans h2⟩⟩
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
i : AlgEquiv.{u, w, v} F L ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
⊢ Eq (α := Subsemiring E) (Subalgebra.toSubsemiring (toSubalgebra (adjoin L (↑A : Set E))))
    (Subalgebra.toSubsemiring (R := ↥L') (Algebra.adjoin ↥L' (↑A : Set E)))

Tactic:
have heq : (adjoin L (A : Set E)).toSubalgebra.toSubsemiring =
      (Algebra.adjoin L' (A : Set E)).toSubsemiring := by
    rw [adjoin_intermediateField_toSubalgebra_of_isAlgebraic _ _ halg.symm,
      Algebra.adjoin_toSubsemiring, Algebra.adjoin_toSubsemiring]
    congr 2
    ext x
    simp only [Set.mem_range, Subtype.exists]
    exact ⟨fun ⟨y, h⟩ ↦ ⟨x, ⟨y, h⟩, rfl⟩, fun ⟨a, ⟨y, h1⟩, h2⟩ ↦ ⟨y, h1.trans h2⟩⟩
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
i : AlgEquiv.{u, w, v} F L ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
heq :
  Eq (α := Subsemiring E) (Subalgebra.toSubsemiring (toSubalgebra (adjoin L (↑A : Set E))))
    (Subalgebra.toSubsemiring (R := ↥L') (Algebra.adjoin ↥L' (↑A : Set E)))
⊢ Module.rank L ↥(adjoin L (↑A : Set E)) = Module.rank ↥L' ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E))

Tactic:
rank_eq_of_equiv_equiv i (RingEquiv.subsemiringCongr heq).toAddEquiv
    i.bijective fun a ⟨x, hx⟩ ↦ ?_

Premises used: RingEquiv.subsemiringCongr, RingEquiv.toAddEquiv, _private.0.IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic.match_4, rank_eq_of_equiv_equiv, HSMul.hSMul, AlgEquiv.bijective, Eq, DFunLike.coe
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
i : AlgEquiv.{u, w, v} F L ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
heq :
  Eq (α := Subsemiring E) (Subalgebra.toSubsemiring (toSubalgebra (adjoin L (↑A : Set E))))
    (Subalgebra.toSubsemiring (R := ↥L') (Algebra.adjoin ↥L' (↑A : Set E)))
refine :
  ∀ (a : L) (x : ↥(adjoin L (↑A : Set E))) (x : E)
    (hx : Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x),
    ((RingEquiv.subsemiringCongr heq).toAddEquiv :
          (a : ↥(adjoin L (↑A : Set E))) → ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
        (a •
          Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x) x hx) =
      HSMul.hSMul (α := ↥L') (β := ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E))) ((i : (a : L) → ↥L') a : ↥L')
        (((RingEquiv.subsemiringCongr heq).toAddEquiv :
              (a : ↥(adjoin L (↑A : Set E))) → ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
            (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x) x
              hx) :
          ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
⊢ Module.rank L ↥(adjoin L (↑A : Set E)) = Module.rank ↥L' ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E))

Tactic:
refine rank_eq_of_equiv_equiv i (RingEquiv.subsemiringCongr heq).toAddEquiv
    i.bijective fun a ⟨x, hx⟩ ↦ ?_
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
i : AlgEquiv.{u, w, v} F L ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
heq :
  Eq (α := Subsemiring E) (Subalgebra.toSubsemiring (toSubalgebra (adjoin L (↑A : Set E))))
    (Subalgebra.toSubsemiring (R := ↥L') (Algebra.adjoin ↥L' (↑A : Set E)))
a : L
x_1 : ↥(adjoin L (↑A : Set E))
x : E
hx : Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x
a₁ :
  (↑(((RingEquiv.subsemiringCongr heq).toAddEquiv :
            (a : ↥(adjoin L (↑A : Set E))) → ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
          (a •
            Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x) x
              hx)) :
      E) =
    (↑(HSMul.hSMul (α := ↥L') (β := ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E))) ((i : (a : L) → ↥L') a : ↥L')
          (((RingEquiv.subsemiringCongr heq).toAddEquiv :
                (a : ↥(adjoin L (↑A : Set E))) → ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x) x
                hx) :
            ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))) :
      E)
⊢ ((RingEquiv.subsemiringCongr heq).toAddEquiv :
        (a : ↥(adjoin L (↑A : Set E))) → ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
      (a • Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x) x hx) =
    HSMul.hSMul (α := ↥L') (β := ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E))) ((i : (a : L) → ↥L') a : ↥L')
      (((RingEquiv.subsemiringCongr heq).toAddEquiv :
            (a : ↥(adjoin L (↑A : Set E))) → ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x) x hx) :
        ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))

Tactic:
ext
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
i : AlgEquiv.{u, w, v} F L ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
heq :
  Eq (α := Subsemiring E) (Subalgebra.toSubsemiring (toSubalgebra (adjoin L (↑A : Set E))))
    (Subalgebra.toSubsemiring (R := ↥L') (Algebra.adjoin ↥L' (↑A : Set E)))
a : L
x_1 : ↥(adjoin L (↑A : Set E))
x : E
hx : Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x
a₁ :
  (↑(((RingEquiv.subsemiringCongr heq).toAddEquiv :
            (a : ↥(adjoin L (↑A : Set E))) → ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
          (HMul.hMul (α := ↥(adjoin L (↑A : Set E)))
            ((algebraMap L ↥(adjoin L (↑A : Set E)) : (a : L) → ↥(adjoin L (↑A : Set E))) a : ↥(adjoin L (↑A : Set E)))
            (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x) x
              hx))) :
      E) =
    (↑(HMul.hMul (α := ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E))) (β :=
          ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
          ((algebraMap ↥L' ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)) :
                (a : ↥L') → ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
              ((i : (a : L) → ↥L') a) :
            ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
          (((RingEquiv.subsemiringCongr heq).toAddEquiv :
                (a : ↥(adjoin L (↑A : Set E))) → ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x) x
                hx) :
            ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))) :
      E)
⊢ (↑(((RingEquiv.subsemiringCongr heq).toAddEquiv :
            (a : ↥(adjoin L (↑A : Set E))) → ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
          (a •
            Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x) x
              hx)) :
      E) =
    (↑(HSMul.hSMul (α := ↥L') (β := ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E))) ((i : (a : L) → ↥L') a : ↥L')
          (((RingEquiv.subsemiringCongr heq).toAddEquiv :
                (a : ↥(adjoin L (↑A : Set E))) → ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x) x
                hx) :
            ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))) :
      E)

Tactic:
simp_rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
i : AlgEquiv.{u, w, v} F L ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
heq :
  Eq (α := Subsemiring E) (Subalgebra.toSubsemiring (toSubalgebra (adjoin L (↑A : Set E))))
    (Subalgebra.toSubsemiring (R := ↥L') (Algebra.adjoin ↥L' (↑A : Set E)))
a : L
x_1 : ↥(adjoin L (↑A : Set E))
x : E
hx : Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x
⊢ (↑(((RingEquiv.subsemiringCongr heq).toAddEquiv :
            (a : ↥(adjoin L (↑A : Set E))) → ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
          (HMul.hMul (α := ↥(adjoin L (↑A : Set E)))
            ((algebraMap L ↥(adjoin L (↑A : Set E)) : (a : L) → ↥(adjoin L (↑A : Set E))) a : ↥(adjoin L (↑A : Set E)))
            (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x) x
              hx))) :
      E) =
    (↑(HMul.hMul (α := ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E))) (β :=
          ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
          ((algebraMap ↥L' ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)) :
                (a : ↥L') → ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
              ((i : (a : L) → ↥L') a) :
            ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
          (((RingEquiv.subsemiringCongr heq).toAddEquiv :
                (a : ↥(adjoin L (↑A : Set E))) → ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField L E) (adjoin L (↑A : Set E)) x) x
                hx) :
            ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E)))) :
      E)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
inst_7 : Algebra.IsAlgebraic.{u, v} F ↥A
⊢ Module.rank L ↥(adjoin L (↑A : Set E)) = Module.rank F ↥A

Tactic:
H.adjoin_rank_eq_rank_left_of_isAlgebraic (.inl ‹_›)

Premises used: IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic, Or.inl
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
inst_7 : Algebra.IsAlgebraic F L
⊢ Module.rank L ↥(adjoin L (↑A : Set E)) = Module.rank F ↥A

Tactic:
H.adjoin_rank_eq_rank_left_of_isAlgebraic (.inr ‹_›)

Premises used: IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic, Or.inr
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
rw :
  Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) =
    Module.rank ↥A.toSubalgebra
      ↥(Algebra.adjoin ↥A.toSubalgebra (↑(AlgHom.range (IsScalarTower.toAlgHom F L E)) : Set E))
⊢ Cardinal.lift.{w, v} (Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯)) =
    Cardinal.lift.{v, w} (Module.rank F L)

Tactic:
rw [(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.lift_rank_eq,
    Cardinal.lift_inj, ← Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_right H]

Premises used: AlgEquiv.ofInjectiveField, LinearEquiv.lift_rank_eq, IsScalarTower.toAlgHom, Cardinal.lift_inj, AlgEquiv.toLinearEquiv, Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_right
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
set :
  let L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E);
  Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) =
    Module.rank ↥A.toSubalgebra ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E))
⊢ Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) =
    Module.rank ↥A.toSubalgebra
      ↥(Algebra.adjoin ↥A.toSubalgebra (↑(AlgHom.range (IsScalarTower.toAlgHom F L E)) : Set E))

Tactic:
set L' := (IsScalarTower.toAlgHom F L E).range

Premises used: IsScalarTower.toAlgHom, AlgHom.range
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
rw :
  Eq (α := Subsemiring E)
    (Subsemiring.closure ((↑A : Set E) ∪ Set.range.{v, w + 1} (ι := L) (⇑(algebraMap L E) : (a : L) → E)))
    (Subsemiring.closure (Set.range (ι := ↥A) (⇑(algebraMap (↥A) E) : (a : ↥A) → E) ∪ (↑L' : Set E)))
⊢ Eq (α := Subsemiring E) (Subalgebra.toSubsemiring (toSubalgebra (adjoin L (↑A : Set E))))
    (Subalgebra.toSubsemiring (R := ↥A) (Algebra.adjoin ↥A (↑L' : Set E)))

Tactic:
rw [adjoin_intermediateField_toSubalgebra_of_isAlgebraic _ _ halg.symm,
      Algebra.adjoin_toSubsemiring, Algebra.adjoin_toSubsemiring, Set.union_comm]

Premises used: IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic, Set.union_comm, Or.symm, Algebra.adjoin_toSubsemiring
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
e_s : (↑A : Set E) = Set.range (ι := ↥A) (⇑(algebraMap (↥A) E) : (a : ↥A) → E)
⊢ Eq (α := Subsemiring E)
    (Subsemiring.closure ((↑A : Set E) ∪ Set.range.{v, w + 1} (ι := L) (⇑(algebraMap L E) : (a : L) → E)))
    (Subsemiring.closure (Set.range (ι := ↥A) (⇑(algebraMap (↥A) E) : (a : ↥A) → E) ∪ (↑L' : Set E)))

Tactic:
congr 2
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
e_s :
  ∀ (x : E),
    x ∈ (↑A : Set E) ↔ Membership.mem (γ := Set E) (Set.range (ι := ↥A) (⇑(algebraMap (↥A) E) : (a : ↥A) → E)) x
⊢ (↑A : Set E) = Set.range (ι := ↥A) (⇑(algebraMap (↥A) E) : (a : ↥A) → E)

Tactic:
ext x
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
x : E
⊢ x ∈ (↑A : Set E) ↔ Membership.mem (γ := Set E) (Set.range (ι := ↥A) (⇑(algebraMap (↥A) E) : (a : ↥A) → E)) x

Tactic:
simp
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
⊢ Eq (α := Subsemiring E) (Subalgebra.toSubsemiring (toSubalgebra (adjoin L (↑A : Set E))))
    (Subalgebra.toSubsemiring (R := ↥A) (Algebra.adjoin ↥A (↑L' : Set E)))

Tactic:
have heq : (adjoin L (A : Set E)).toSubalgebra.toSubsemiring =
      (Algebra.adjoin A (L' : Set E)).toSubsemiring := by
    rw [adjoin_intermediateField_toSubalgebra_of_isAlgebraic _ _ halg.symm,
      Algebra.adjoin_toSubsemiring, Algebra.adjoin_toSubsemiring, Set.union_comm]
    congr 2
    ext x
    simp
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
heq :
  Eq (α := Subsemiring E) (Subalgebra.toSubsemiring (toSubalgebra (adjoin L (↑A : Set E))))
    (Subalgebra.toSubsemiring (R := ↥A) (Algebra.adjoin ↥A (↑L' : Set E)))
⊢ Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) =
    Module.rank ↥A.toSubalgebra ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E))

Tactic:
rank_eq_of_equiv_equiv (RingHom.id A) (RingEquiv.subsemiringCongr heq).toAddEquiv
    Function.bijective_id fun ⟨a, ha⟩ ⟨x, hx⟩ ↦ ?_

Premises used: RingEquiv.subsemiringCongr, Function.bijective_id, _private.0.IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic.match_2, RingEquiv.toAddEquiv, _private.0.IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic.match_1, Membership.mem, Subtype, Subtype.mk, rank_eq_of_equiv_equiv, HSMul.hSMul, RingHom.id, Eq, DFunLike.coe
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
heq :
  Eq (α := Subsemiring E) (Subalgebra.toSubsemiring (toSubalgebra (adjoin L (↑A : Set E))))
    (Subalgebra.toSubsemiring (R := ↥A) (Algebra.adjoin ↥A (↑L' : Set E)))
refine :
  ∀ (x : ↥A) (x : ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯)) (a : E) (ha : a ∈ A) (x : E)
    (hx :
      Membership.mem (γ := IntermediateField (↥A) E) (extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯)
        x),
    ((RingEquiv.subsemiringCongr heq).toAddEquiv :
          (a : ↥(extendScalars ⋯)) → ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
        (Subtype.mk (p := fun (x : E) ↦ x ∈ A) a ha •
          Subtype.mk (p := fun (x : E) ↦
            Membership.mem (γ := IntermediateField (↥A) E)
              (extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) x)
            x hx) =
      HSMul.hSMul (α := ↥A.toSubalgebra) (β := ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
        ((RingHom.id ↥A : (a : ↥A) → ↥A) (Subtype.mk (p := fun (x : E) ↦ x ∈ A) a ha) : ↥A)
        (((RingEquiv.subsemiringCongr heq).toAddEquiv :
              (a : ↥(extendScalars ⋯)) → ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
            (Subtype.mk (p := fun (x : E) ↦
              Membership.mem (γ := IntermediateField (↥A) E)
                (extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) x)
              x hx) :
          ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
⊢ Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) =
    Module.rank ↥A.toSubalgebra ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E))

Tactic:
refine rank_eq_of_equiv_equiv (RingHom.id A) (RingEquiv.subsemiringCongr heq).toAddEquiv
    Function.bijective_id fun ⟨a, ha⟩ ⟨x, hx⟩ ↦ ?_