awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Laurent
Goal:
R : Type u
inst : CommRing R
f : R⟮X⟯
inst_1 : IsDomain R
p q : R[X]
h : q ≠ 0
⊢ (laurent 0 : (a : R⟮X⟯) → R⟮X⟯)
      (HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
        ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) q : R⟮X⟯)) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) q : R⟮X⟯)

Tactic:
simp
-- Module: Mathlib.FieldTheory.Laurent
Goal:
R : Type u
inst : CommRing R
r s : R
f : R⟮X⟯
inst_1 : IsDomain R
f₁ :
  ∀ (p q : R[X]),
    q ≠ 0 →
      Eq (α := R⟮X⟯)
        ((laurent r : (a : R⟮X⟯) → R⟮X⟯)
            ((laurent s : (a : R⟮X⟯) → R⟮X⟯)
              (HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
                ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) q : R⟮X⟯))) :
          R⟮X⟯)
        ((laurent (r + s) : (a : R⟮X⟯) → R⟮X⟯)
            (HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
              ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) q : R⟮X⟯)) :
          R⟮X⟯)
⊢ Eq (α := R⟮X⟯) ((laurent r : (a : R⟮X⟯) → R⟮X⟯) ((laurent s : (a : R⟮X⟯) → R⟮X⟯) f) : R⟮X⟯)
    ((laurent (r + s) : (a : R⟮X⟯) → R⟮X⟯) f : R⟮X⟯)

Tactic:
induction f using RatFunc.induction_on

Premises used: RatFunc.induction_on
-- Module: Mathlib.FieldTheory.Laurent
Goal:
R : Type u
inst : CommRing R
r s : R
f : R⟮X⟯
inst_1 : IsDomain R
p q : R[X]
h : q ≠ 0
f₁ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) ((taylor s : (a : R[X]) → R[X]) p)) :
        R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) ((taylor s : (a : R[X]) → R[X]) q)) :
        R⟮X⟯) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor (r + s) : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor (r + s) : (a : R[X]) → R[X]) q) : R⟮X⟯)
⊢ Eq (α := R⟮X⟯)
    ((laurent r : (a : R⟮X⟯) → R⟮X⟯)
        ((laurent s : (a : R⟮X⟯) → R⟮X⟯)
          (HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
            ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) q : R⟮X⟯))) :
      R⟮X⟯)
    ((laurent (r + s) : (a : R⟮X⟯) → R⟮X⟯)
        (HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
          ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) q : R⟮X⟯)) :
      R⟮X⟯)

Tactic:
simp_rw [laurent_div, taylor_taylor]

Premises used: RatFunc.laurent_div, Polynomial.taylor_taylor
-- Module: Mathlib.FieldTheory.Laurent
Goal:
R : Type u
inst : CommRing R
r : R
inst_1 : IsDomain R
x x_1 : R⟮X⟯
h : Eq (α := R⟮X⟯) ((laurent r : (a : R⟮X⟯) → R⟮X⟯) x : R⟮X⟯) ((laurent r : (a : R⟮X⟯) → R⟮X⟯) x_1 : R⟮X⟯)
⊢ x = x_1

Tactic:
simpa [laurent_laurent] using congr_arg (laurent (-r)) h

Premises used: RatFunc.laurent, RatFunc.laurent_laurent, congr_arg, DFunLike.coe, Neg.neg
-- 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
⊢ A.LinearDisjoint L ↔ A.LinearDisjoint (AlgHom.range (IsScalarTower.toAlgHom F L E))

Tactic:
Iff.rfl

Premises used: Iff.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 B : IntermediateField F E
a : AlgHom.range (A := ↥B) (IsScalarTower.toAlgHom F (↥B) E) = B.toSubalgebra
⊢ A.LinearDisjoint (AlgHom.range (A := ↥B) (IsScalarTower.toAlgHom F (↥B) E)) ↔ A.LinearDisjoint B.toSubalgebra

Tactic:
congr!
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
a :
  ∀ (x : E),
    Membership.mem (γ := Subalgebra F E) (AlgHom.range (A := ↥B) (IsScalarTower.toAlgHom F (↥B) E)) x ↔
      x ∈ B.toSubalgebra
⊢ AlgHom.range (A := ↥B) (IsScalarTower.toAlgHom F (↥B) E) = B.toSubalgebra

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 B : IntermediateField F E
x : E
⊢ Membership.mem (γ := Subalgebra F E) (AlgHom.range (A := ↥B) (IsScalarTower.toAlgHom F (↥B) E)) x ↔ x ∈ B.toSubalgebra

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 B : IntermediateField F E
H : A.LinearDisjoint ↥B
⊢ B.LinearDisjoint ↥A

Tactic:
linearDisjoint_iff'.2 (linearDisjoint_iff'.1 H).symm

Premises used: Iff.mpr, Subalgebra.LinearDisjoint.symm, IntermediateField.linearDisjoint_iff', Iff.mp
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
⊢ A.LinearDisjoint ↥B ↔ B.LinearDisjoint ↥A

Tactic:
⟨LinearDisjoint.symm, LinearDisjoint.symm⟩

Premises used: IntermediateField.LinearDisjoint.symm, Iff.intro
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra 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
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' E
inst_10 : IsScalarTower F L' E
H : IntermediateField.LinearDisjoint (AlgHom.fieldRange (IsScalarTower.toAlgHom F L E)) L'
⊢ IntermediateField.LinearDisjoint (AlgHom.fieldRange (IsScalarTower.toAlgHom F L' E)) L

Tactic:
Subalgebra.LinearDisjoint.symm H

Premises used: Subalgebra.LinearDisjoint.symm
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra 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
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' E
inst_10 : IsScalarTower F L' E
⊢ IntermediateField.LinearDisjoint (AlgHom.fieldRange (IsScalarTower.toAlgHom F L E)) L' ↔
    IntermediateField.LinearDisjoint (AlgHom.fieldRange (IsScalarTower.toAlgHom F L' E)) L

Tactic:
⟨LinearDisjoint.symm', LinearDisjoint.symm'⟩

Premises used: IntermediateField.LinearDisjoint.symm', Iff.intro
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
H : A.LinearDisjoint ↥B
K : Type u_1
inst_3 : Field K
inst_4 : Algebra F K
f : E →ₐ[F] K
⊢ (IntermediateField.map f A).LinearDisjoint ↥(IntermediateField.map f B)

Tactic:
linearDisjoint_iff'.2 ((linearDisjoint_iff'.1 H).map f f.injective)

Premises used: Iff.mpr, IntermediateField.linearDisjoint_iff', Subalgebra.LinearDisjoint.map, RingHom.injective, AlgHom.toRingHom, Iff.mp
-- 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
K : Type u_1
inst_7 : Field K
inst_8 : Algebra F K
inst_9 : Algebra L K
inst_10 : IsScalarTower F L K
inst_11 : Algebra E K
inst_12 : IsScalarTower F E K
inst_13 : IsScalarTower L E K
rw :
  ∀ (H : A.LinearDisjoint (AlgHom.range (IsScalarTower.toAlgHom F L E))) (K : Type u_1) [inst_14 : Field K]
    [inst_15 : Algebra F K] [inst_16 : Algebra L K] [inst_17 : IsScalarTower F L K] [inst_18 : Algebra E K]
    [inst_19 : IsScalarTower F E K] [IsScalarTower L E K],
    Subalgebra.LinearDisjoint (toSubalgebra (IntermediateField.map (IsScalarTower.toAlgHom F E K) A))
      (AlgHom.range (IsScalarTower.toAlgHom F L K))
⊢ IntermediateField.LinearDisjoint (IntermediateField.map (IsScalarTower.toAlgHom F E K) A) L

Tactic:
rw [linearDisjoint_iff] at H ⊢

Premises used: IntermediateField.linearDisjoint_iff
-- 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 (AlgHom.range (IsScalarTower.toAlgHom F L E))
K : Type u_1
inst_7 : Field K
inst_8 : Algebra F K
inst_9 : Algebra L K
inst_10 : IsScalarTower F L K
inst_11 : Algebra E K
inst_12 : IsScalarTower F E K
inst_13 : IsScalarTower L E K
⊢ Subalgebra.LinearDisjoint (Subalgebra.map (IsScalarTower.toAlgHom F E K) A.toSubalgebra)
    (Subalgebra.map (IsScalarTower.toAlgHom F E K) (AlgHom.range (IsScalarTower.toAlgHom F L E)))

Tactic:
have := H.map (IsScalarTower.toAlgHom F E K) (RingHom.injective _)
-- 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 (AlgHom.range (IsScalarTower.toAlgHom F L E))
K : Type u_1
inst_7 : Field K
inst_8 : Algebra F K
inst_9 : Algebra L K
inst_10 : IsScalarTower F L K
inst_11 : Algebra E K
inst_12 : IsScalarTower F E K
inst_13 : IsScalarTower L E K
this :
  Subalgebra.LinearDisjoint (Subalgebra.map (IsScalarTower.toAlgHom F E K) A.toSubalgebra)
    (Subalgebra.map (IsScalarTower.toAlgHom F E K) (AlgHom.range (IsScalarTower.toAlgHom F L E)))
⊢ Subalgebra.LinearDisjoint (Subalgebra.map (IsScalarTower.toAlgHom F E K) A.toSubalgebra)
    (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E)))

Tactic:
rw [← AlgHom.range_comp] at this

Premises used: AlgHom.range_comp
-- 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 (AlgHom.range (IsScalarTower.toAlgHom F L E))
K : Type u_1
inst_7 : Field K
inst_8 : Algebra F K
inst_9 : Algebra L K
inst_10 : IsScalarTower F L K
inst_11 : Algebra E K
inst_12 : IsScalarTower F E K
inst_13 : IsScalarTower L E K
this :
  Subalgebra.LinearDisjoint (Subalgebra.map (IsScalarTower.toAlgHom F E K) A.toSubalgebra)
    (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E)))
⊢ Subalgebra.LinearDisjoint (Subalgebra.map (IsScalarTower.toAlgHom F E K) A.toSubalgebra)
    (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E)))

Tactic:
this
-- 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 (AlgHom.range (IsScalarTower.toAlgHom F L E))
K : Type u_1
inst_7 : Field K
inst_8 : Algebra F K
inst_9 : Algebra L K
inst_10 : IsScalarTower F L K
inst_11 : Algebra E K
inst_12 : IsScalarTower F E K
inst_13 : IsScalarTower L E K
this :
  Subalgebra.LinearDisjoint (Subalgebra.map (IsScalarTower.toAlgHom F E K) A.toSubalgebra)
    (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E)))
h :
  Eq (α := L →ₐ[F] K) (IsScalarTower.toAlgHom F L K)
    (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E))
⊢ Subalgebra.LinearDisjoint (toSubalgebra (IntermediateField.map (IsScalarTower.toAlgHom F E K) A))
    (AlgHom.range (IsScalarTower.toAlgHom F L K))

Tactic:
convert! this
-- 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 (AlgHom.range (IsScalarTower.toAlgHom F L E))
K : Type u_1
inst_7 : Field K
inst_8 : Algebra F K
inst_9 : Algebra L K
inst_10 : IsScalarTower F L K
inst_11 : Algebra E K
inst_12 : IsScalarTower F E K
inst_13 : IsScalarTower L E K
this :
  Subalgebra.LinearDisjoint (Subalgebra.map (IsScalarTower.toAlgHom F E K) A.toSubalgebra)
    (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E)))
h :
  ∀ (x : L),
    Eq.{u_1 + 1} (α := K) ((IsScalarTower.toAlgHom F L K : (a : L) → K) x : K)
      ((AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E) : (a : L) → K) x : K)
⊢ Eq (α := L →ₐ[F] K) (IsScalarTower.toAlgHom F L K)
    (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L 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 (AlgHom.range (IsScalarTower.toAlgHom F L E))
K : Type u_1
inst_7 : Field K
inst_8 : Algebra F K
inst_9 : Algebra L K
inst_10 : IsScalarTower F L K
inst_11 : Algebra E K
inst_12 : IsScalarTower F E K
inst_13 : IsScalarTower L E K
this :
  Subalgebra.LinearDisjoint (Subalgebra.map (IsScalarTower.toAlgHom F E K) A.toSubalgebra)
    (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E)))
x : L
⊢ Eq.{u_1 + 1} (α := K) ((IsScalarTower.toAlgHom F L K : (a : L) → K) x : K)
    ((AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E) : (a : L) → K) x : K)

Tactic:
IsScalarTower.algebraMap_apply L E K _

Premises used: IsScalarTower.algebraMap_apply
-- 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 (AlgHom.range (IsScalarTower.toAlgHom F L E))
K : Type u_1
inst_7 : Field K
inst_8 : Algebra F K
inst_9 : Algebra L K
inst_10 : IsScalarTower F L K
inst_11 : Algebra E K
inst_12 : IsScalarTower F E K
inst_13 : IsScalarTower L E K
this :
  Subalgebra.LinearDisjoint (Subalgebra.map (IsScalarTower.toAlgHom F E K) A.toSubalgebra)
    (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E)))
x : L
⊢ Eq.{u_1 + 1} (α := K) ((IsScalarTower.toAlgHom F L K : (a : L) → K) x : K)
    ((AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E) : (a : L) → K) x : K)

Tactic:
exact IsScalarTower.algebraMap_apply L E K _

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra 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
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' E
inst_10 : IsScalarTower F L' E
H : IntermediateField.LinearDisjoint (AlgHom.fieldRange (IsScalarTower.toAlgHom F L E)) L'
K : Type u_2
inst_11 : Field K
inst_12 : Algebra F K
inst_13 : Algebra L K
inst_14 : IsScalarTower F L K
inst_15 : Algebra L' K
inst_16 : IsScalarTower F L' K
inst_17 : Algebra E K
inst_18 : IsScalarTower F E K
inst_19 : IsScalarTower L E K
inst_20 : IsScalarTower L' E K
rw :
  ∀
    (H :
      Subalgebra.LinearDisjoint (toSubalgebra (AlgHom.fieldRange (IsScalarTower.toAlgHom F L E)))
        (AlgHom.range (IsScalarTower.toAlgHom F L' E)))
    (K : Type u_2) [inst_21 : Field K] [inst_22 : Algebra F K] [inst_23 : Algebra L K] [inst_24 : IsScalarTower F L K]
    [inst_25 : Algebra L' K] [inst_26 : IsScalarTower F L' K] [inst_27 : Algebra E K] [IsScalarTower F E K]
    [IsScalarTower L E K] [IsScalarTower L' E K],
    Subalgebra.LinearDisjoint (toSubalgebra (AlgHom.fieldRange (IsScalarTower.toAlgHom F L K)))
      (AlgHom.range (IsScalarTower.toAlgHom F L' K))
⊢ IntermediateField.LinearDisjoint (AlgHom.fieldRange (IsScalarTower.toAlgHom F L K)) L'

Tactic:
rw [linearDisjoint_iff] at H ⊢

Premises used: IntermediateField.linearDisjoint_iff
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra 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
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' E
inst_10 : IsScalarTower F L' E
H :
  Subalgebra.LinearDisjoint (toSubalgebra (AlgHom.fieldRange (IsScalarTower.toAlgHom F L E)))
    (AlgHom.range (IsScalarTower.toAlgHom F L' E))
K : Type u_2
inst_11 : Field K
inst_12 : Algebra F K
inst_13 : Algebra L K
inst_14 : IsScalarTower F L K
inst_15 : Algebra L' K
inst_16 : IsScalarTower F L' K
inst_17 : Algebra E K
inst_18 : IsScalarTower F E K
inst_19 : IsScalarTower L E K
inst_20 : IsScalarTower L' E K
⊢ Subalgebra.LinearDisjoint
    (Subalgebra.map (IsScalarTower.toAlgHom F E K) (toSubalgebra (AlgHom.fieldRange (IsScalarTower.toAlgHom F L E))))
    (Subalgebra.map (IsScalarTower.toAlgHom F E K) (AlgHom.range (IsScalarTower.toAlgHom F L' E)))

Tactic:
have := H.map (IsScalarTower.toAlgHom F E K) (RingHom.injective _)
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra 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
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' E
inst_10 : IsScalarTower F L' E
H :
  Subalgebra.LinearDisjoint (toSubalgebra (AlgHom.fieldRange (IsScalarTower.toAlgHom F L E)))
    (AlgHom.range (IsScalarTower.toAlgHom F L' E))
K : Type u_2
inst_11 : Field K
inst_12 : Algebra F K
inst_13 : Algebra L K
inst_14 : IsScalarTower F L K
inst_15 : Algebra L' K
inst_16 : IsScalarTower F L' K
inst_17 : Algebra E K
inst_18 : IsScalarTower F E K
inst_19 : IsScalarTower L E K
inst_20 : IsScalarTower L' E K
this :
  Subalgebra.LinearDisjoint
    (Subalgebra.map (IsScalarTower.toAlgHom F E K) (toSubalgebra (AlgHom.fieldRange (IsScalarTower.toAlgHom F L E))))
    (Subalgebra.map (IsScalarTower.toAlgHom F E K) (AlgHom.range (IsScalarTower.toAlgHom F L' E)))
⊢ Subalgebra.LinearDisjoint (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E)))
    (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L' E)))

Tactic:
simp_rw [AlgHom.fieldRange_toSubalgebra, ← AlgHom.range_comp] at this

Premises used: AlgHom.fieldRange_toSubalgebra, AlgHom.range_comp
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra 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
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' E
inst_10 : IsScalarTower F L' E
H :
  Subalgebra.LinearDisjoint (toSubalgebra (AlgHom.fieldRange (IsScalarTower.toAlgHom F L E)))
    (AlgHom.range (IsScalarTower.toAlgHom F L' E))
K : Type u_2
inst_11 : Field K
inst_12 : Algebra F K
inst_13 : Algebra L K
inst_14 : IsScalarTower F L K
inst_15 : Algebra L' K
inst_16 : IsScalarTower F L' K
inst_17 : Algebra E K
inst_18 : IsScalarTower F E K
inst_19 : IsScalarTower L E K
inst_20 : IsScalarTower L' E K
this :
  Subalgebra.LinearDisjoint (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E)))
    (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L' E)))
⊢ Subalgebra.LinearDisjoint (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E)))
    (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L' E)))

Tactic:
this
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra 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
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' E
inst_10 : IsScalarTower F L' E
H :
  Subalgebra.LinearDisjoint (toSubalgebra (AlgHom.fieldRange (IsScalarTower.toAlgHom F L E)))
    (AlgHom.range (IsScalarTower.toAlgHom F L' E))
K : Type u_2
inst_11 : Field K
inst_12 : Algebra F K
inst_13 : Algebra L K
inst_14 : IsScalarTower F L K
inst_15 : Algebra L' K
inst_16 : IsScalarTower F L' K
inst_17 : Algebra E K
inst_18 : IsScalarTower F E K
inst_19 : IsScalarTower L E K
inst_20 : IsScalarTower L' E K
this :
  Subalgebra.LinearDisjoint (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E)))
    (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L' E)))
h :
  Eq (α := L →ₐ[F] K) (IsScalarTower.toAlgHom F L K)
    (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E))
h₁ :
  Eq (α := L' →ₐ[F] K) (IsScalarTower.toAlgHom F L' K)
    (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L' E))
⊢ Subalgebra.LinearDisjoint (AlgHom.range (IsScalarTower.toAlgHom F L K)) (AlgHom.range (IsScalarTower.toAlgHom F L' K))

Tactic:
convert! this
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra 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
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' E
inst_10 : IsScalarTower F L' E
H :
  Subalgebra.LinearDisjoint (toSubalgebra (AlgHom.fieldRange (IsScalarTower.toAlgHom F L E)))
    (AlgHom.range (IsScalarTower.toAlgHom F L' E))
K : Type u_2
inst_11 : Field K
inst_12 : Algebra F K
inst_13 : Algebra L K
inst_14 : IsScalarTower F L K
inst_15 : Algebra L' K
inst_16 : IsScalarTower F L' K
inst_17 : Algebra E K
inst_18 : IsScalarTower F E K
inst_19 : IsScalarTower L E K
inst_20 : IsScalarTower L' E K
this :
  Subalgebra.LinearDisjoint (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E)))
    (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L' E)))
h :
  ∀ (x : L),
    Eq.{u_2 + 1} (α := K) ((IsScalarTower.toAlgHom F L K : (a : L) → K) x : K)
      ((AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E) : (a : L) → K) x : K)
⊢ Eq (α := L →ₐ[F] K) (IsScalarTower.toAlgHom F L K)
    (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L 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
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' E
inst_10 : IsScalarTower F L' E
H :
  Subalgebra.LinearDisjoint (toSubalgebra (AlgHom.fieldRange (IsScalarTower.toAlgHom F L E)))
    (AlgHom.range (IsScalarTower.toAlgHom F L' E))
K : Type u_2
inst_11 : Field K
inst_12 : Algebra F K
inst_13 : Algebra L K
inst_14 : IsScalarTower F L K
inst_15 : Algebra L' K
inst_16 : IsScalarTower F L' K
inst_17 : Algebra E K
inst_18 : IsScalarTower F E K
inst_19 : IsScalarTower L E K
inst_20 : IsScalarTower L' E K
this :
  Subalgebra.LinearDisjoint (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E)))
    (AlgHom.range (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L' E)))
x : L
⊢ Eq.{u_2 + 1} (α := K) ((IsScalarTower.toAlgHom F L K : (a : L) → K) x : K)
    ((AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E) : (a : L) → K) x : K)

Tactic:
IsScalarTower.algebraMap_apply _ E K _

Premises used: IsScalarTower.algebraMap_apply