awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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))
have 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)))
Tactic: refine rank_eq_of_equiv_equiv i (RingEquiv.subsemiringCongr heq).toAddEquiv
    i.bijective fun a ⟨x, hx⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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)))
      (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)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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)))
          (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)
have 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)
Tactic: simp_rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ Cardinal.lift.{w, v} (Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯)) =
    Cardinal.lift.{v, w} (Module.rank F L)
have rw : Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) sorry) =
  Module.rank ↥A.toSubalgebra ↥(Algebra.adjoin ↥A.toSubalgebra (↑(AlgHom.range (IsScalarTower.toAlgHom F L E)) : Set E))
Tactic: rw [(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.lift_rank_eq,
    Cardinal.lift_inj, ← Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_right H]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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)))
have 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)))
Tactic: rw [adjoin_intermediateField_toSubalgebra_of_isAlgebraic _ _ halg.symm,
      Algebra.adjoin_toSubsemiring, Algebra.adjoin_toSubsemiring, Set.union_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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)
    (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)))
have e_s : (↑A : Set E) = Set.range (ι := ↥A) (⇑(algebraMap (↥A) E) : (a : ↥A) → E)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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)
⊢ (↑A : Set E) = Set.range (ι := ↥A) (⇑(algebraMap (↥A) E) : (a : ↥A) → E)
have e_s : ∀ (x : E), x ∈ (↑A : Set E) ↔ Membership.mem (γ := Set E) (Set.range (ι := ↥A) (⇑(algebraMap (↥A) E) : (a : ↥A) → E)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (hypothesis)
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)
⊢ Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) =
    Module.rank ↥A.toSubalgebra ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E))
have heq : 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
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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))
have refine : ∀ (x : ↥A) (x : ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) sorry)) (a : E) (ha : a ∈ A) (x : E)
  (hx :
    Membership.mem (γ := IntermediateField (↥A) E) (extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) sorry)
      x),
  ((RingEquiv.subsemiringCongr heq).toAddEquiv :
        (a : ↥(extendScalars sorry)) → ↥(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))) sorry) 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 sorry)) → ↥(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))) sorry) x)
            x hx) :
        ↥(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⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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)))
x_1 : ↥A
x_2 : ↥(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)))
have a₁ : (↑(((RingEquiv.subsemiringCongr heq).toAddEquiv :
          (a : ↥(extendScalars sorry)) → ↥(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))) sorry) x)
            x hx)) :
    E) =
  (↑(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 sorry)) → ↥(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))) sorry) x)
              x hx) :
          ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))) :
    E)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ Cardinal.lift.{v, w} (Module.rank F L) * Cardinal.lift.{w, v} (Module.rank (↥(adjoin L (↑A : Set E))) E) =
    Cardinal.lift.{w, v} (Module.rank (↥A) E)
have rw : Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) sorry) *
    Module.rank (↥(adjoin L (↑A : Set E))) E =
  Module.rank (↥A) E
Tactic: rw [← H.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic halg, ← Cardinal.lift_mul,
    Cardinal.lift_inj]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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 : (finrank.{u, v} F ↥A).Coprime (finrank F L)
this_1 : Field ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)) :=
  { toCommRing := (IsScalarTower.toAlgHom F L E).range.toCommRing, inv := of_finrank_coprime._aux_1,
    div := of_finrank_coprime._aux_2, div_eq_mul_inv := ⋯, zpow := of_finrank_coprime._aux_3, zpow_zero' := ⋯,
    zpow_succ' := ⋯, zpow_neg' := ⋯, toNontrivial := ⋯, nnratCast := of_finrank_coprime._aux_6,
    ratCast := of_finrank_coprime._aux_7, mul_inv_cancel := ⋯, inv_zero := ⋯, nnratCast_def := ⋯,
    nnqsmul := of_finrank_coprime._aux_9, nnqsmul_def := ⋯, ratCast_def := ⋯, qsmul := of_finrank_coprime._aux_11,
    qsmul_def := ⋯ }
this : Field ↥A.toSubalgebra :=
  { toCommRing := A.toCommRing, inv := fun (a : ↥A.toSubfield) ↦ ⟨(↑a : E)⁻¹, ⋯⟩,
    div := fun (a b : ↥A.toSubfield) ↦ ⟨(↑a : E) / (↑b : E), ⋯⟩, div_eq_mul_inv := ⋯,
    zpow := fun (a : ℤ) (a_1 : ↥A.toSubfield) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ A.toSubfield) ((↑a_1 : E) ^ a) ⋯,
    zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, toNontrivial := ⋯, nnratCast := fun (q : ℚ≥0) ↦ ⟨(↑q : E), ⋯⟩,
    ratCast := fun (q : ℚ) ↦ ⟨(↑q : E), ⋯⟩, mul_inv_cancel := ⋯, inv_zero := ⋯, nnratCast_def := ⋯,
    nnqsmul := fun (a : ℚ≥0) (a_1 : ↥A.toSubfield) ↦
      Subtype.mk (p := fun (x : E) ↦ x ∈ A.toSubfield) (a • (↑a_1 : E)) ⋯,
    nnqsmul_def := ⋯, ratCast_def := ⋯,
    qsmul := fun (a : ℚ) (a_1 : ↥A.toSubfield) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ A.toSubfield) (a • (↑a_1 : E)) ⋯,
    qsmul_def := ⋯ }
⊢ (finrank.{u, v} F ↥A.toSubalgebra).Coprime (finrank.{u, v} F ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)))
have rwa : ∀ (H : (finrank.{u, v} F ↥A).Coprime (finrank.{u, v} F ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)))),
  (finrank.{u, v} F ↥A.toSubalgebra).Coprime (finrank.{u, v} F ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)))
Tactic: rwa [(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.finrank_eq] at H
Cleared hypotheses: H, this_1, this
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : Type u_1
B : Type u_2
inst_3 : Field A
inst_4 : Algebra F A
inst_5 : Field B
inst_6 : Algebra F B
fa : A →ₐ[F] E
fb : B →ₐ[F] E
H : fa.fieldRange.LinearDisjoint ↥fb.fieldRange
⊢ IsDomain (A ⊗[F] B)
have H₁ : fa.range.LinearDisjoint fb.range
Tactic: simp_rw [linearDisjoint_iff', AlgHom.fieldRange_toSubalgebra] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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 : IsField (TensorProduct.{u, v, w} F (↥A) L)
⊢ A.LinearDisjoint L
have H₁ : IsField.{v} (↥A.toSubalgebra ⊗[F] ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)))
Tactic: apply Subalgebra.LinearDisjoint.of_isField
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (hypothesis)
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 : IsField (TensorProduct.{u, v, w} F (↥A) L)
⊢ IsField.{v} (↥A.toSubalgebra ⊗[F] ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)))
have this : SMulCommClass.{u, v, v} F ↥A ↥A
Tactic: haveI : SMulCommClass F A A := SMulCommClass.of_commMonoid F A A
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (hypothesis)
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 : IsField (TensorProduct.{u, v, w} F (↥A) L)
this : SMulCommClass.{u, v, v} F ↥A ↥A
⊢ IsField.{v} (↥A.toSubalgebra ⊗[F] ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)))
have this₁ : SMulCommClass.{u, v, v} F ↥A.toSubalgebra ↥A.toSubalgebra
Tactic: haveI : SMulCommClass F A.toSubalgebra A.toSubalgebra := ‹SMulCommClass F A A›
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
Goal:
F : Type u
inst : Field F
A : Type v
inst_1 : Field A
B : Type w
inst_2 : Field B
inst_3 : Algebra F A
inst_4 : Algebra F B
H : IsField (A ⊗[F] B)
K : Type u_1
inst_5 : Field K
inst_6 : Algebra F K
fa : A →ₐ[F] K
fb : B →ₐ[F] K
⊢ fa.fieldRange.LinearDisjoint ↥fb.fieldRange
have rw : fa.fieldRange.LinearDisjoint fb.fieldRange.toSubalgebra
Tactic: rw [linearDisjoint_iff']
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
Goal:
F : Type u
inst : Field F
A : Type v
inst_1 : Field A
B : Type w
inst_2 : Field B
inst_3 : Algebra F A
inst_4 : Algebra F B
H : IsField (A ⊗[F] B)
K : Type u_1
inst_5 : Field K
inst_6 : Algebra F K
fa : A →ₐ[F] K
fb : B →ₐ[F] K
⊢ fa.fieldRange.LinearDisjoint fb.fieldRange.toSubalgebra
have H₁ : IsField.{u_1} (↥fa.fieldRange.toSubalgebra ⊗[F] ↥fb.fieldRange.toSubalgebra)
Tactic: apply Subalgebra.LinearDisjoint.of_isField
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_1
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : IsDomain (E ⊗[F] K)
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F K
L : Type (max v u_1)
w : Field L
w_1 : Algebra F L
fa : E →ₐ[F] L
fb : K →ₐ[F] L
hfa : Function.Injective (α := E) (β := L) (⇑fa : (a : E) → L)
hfb : Function.Injective (α := K) (β := L) (⇑fb : (a : K) → L)
H : fa.range.LinearDisjoint fb.range
⊢ Algebra.IsAlgebraic F ↥fa.fieldRange ∨ Algebra.IsAlgebraic F ↥fb.fieldRange
have rwa : ∀ (halg : Algebra.IsAlgebraic F ↥fa.range ∨ Algebra.IsAlgebraic F K) (fb : K →ₐ[F] L)
  (hfa : Function.Injective (α := E) (β := L) (⇑fa : (a : E) → L))
  (hfb : Function.Injective (α := K) (β := L) (⇑fb : (a : K) → L)) (H : fa.range.LinearDisjoint fb.range),
  Algebra.IsAlgebraic F ↥fa.fieldRange ∨ Algebra.IsAlgebraic F ↥fb.fieldRange
Tactic: rwa [(AlgEquiv.ofInjective fa hfa).isAlgebraic_iff,
          (AlgEquiv.ofInjective fb hfb).isAlgebraic_iff] at halg
Cleared hypotheses: halg, fb, hfa, hfb, H