awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
inst_1 : IsDomain R
x : R
rw :
  Eq (α := R⟮X⟯)
    ((laurent r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x)) :
      R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x) : R⟮X⟯)
rw₁ :
  Eq (α := R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) ((Polynomial.C : (a : R) → R[X]) x)) :
      R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x) : R⟮X⟯)
⊢ Eq (α := R⟮X⟯) ((laurent r : (a : R⟮X⟯) → R⟮X⟯) ((C : (a : R) → R⟮X⟯) x) : R⟮X⟯) ((C : (a : R) → R⟮X⟯) x : R⟮X⟯)
have rw₂ : Eq (α := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x) : R⟮X⟯)
  ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x) : R⟮X⟯)
Tactic: rw [← algebraMap_C, laurent_algebraMap, taylor_C]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
f : R⟮X⟯
inst_1 : IsDomain R
⊢ (laurent 0 : (a : R⟮X⟯) → R⟮X⟯) f = f
have f₁ : ∀ (p q : R[X]),
  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: induction f using RatFunc.induction_on
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r s : R
f : R⟮X⟯
inst_1 : IsDomain R
⊢ 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⟯)
have 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⟯)
Tactic: induction f using RatFunc.induction_on
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r s : R
f : R⟮X⟯
inst_1 : IsDomain R
p q : R[X]
h : 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⟯)
have 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⟯)
Tactic: simp_rw [laurent_div, taylor_taylor]
-- 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 B : IntermediateField F E
⊢ A.LinearDisjoint (AlgHom.range (A := ↥B) (IsScalarTower.toAlgHom F (↥B) E)) ↔ A.LinearDisjoint B.toSubalgebra
have a : AlgHom.range (A := ↥B) (IsScalarTower.toAlgHom F (↥B) E) = B.toSubalgebra
Tactic: congr!
-- 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 B : IntermediateField F E
⊢ AlgHom.range (A := ↥B) (IsScalarTower.toAlgHom F (↥B) E) = B.toSubalgebra
have a : ∀ (x : E),
  Membership.mem (γ := Subalgebra F E) (AlgHom.range (A := ↥B) (IsScalarTower.toAlgHom F (↥B) E)) x ↔ x ∈ B.toSubalgebra
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
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
⊢ IntermediateField.LinearDisjoint (IntermediateField.map (IsScalarTower.toAlgHom F E K) A) L
have 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))
Tactic: rw [linearDisjoint_iff] at H ⊢
Cleared hypotheses: H, K, inst_7, inst_8, inst_9, inst_10, inst_11, inst_12, inst_13
-- 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 (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 (toSubalgebra (IntermediateField.map (IsScalarTower.toAlgHom F E K) A))
    (AlgHom.range (IsScalarTower.toAlgHom F L K))
have 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)))
Tactic: have := H.map (IsScalarTower.toAlgHom F E K) (RingHom.injective _)
-- 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 (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 (toSubalgebra (IntermediateField.map (IsScalarTower.toAlgHom F E K) A))
    (AlgHom.range (IsScalarTower.toAlgHom F L K))
have 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)))
Tactic: rw [← AlgHom.range_comp] at this
Cleared hypotheses: this
-- 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 (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 (toSubalgebra (IntermediateField.map (IsScalarTower.toAlgHom F E K) A))
    (AlgHom.range (IsScalarTower.toAlgHom F L K))
have h : Eq (α := L →ₐ[F] K) (IsScalarTower.toAlgHom F L K)
  (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E))
Tactic: convert! this
-- 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 (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)))
⊢ Eq (α := L →ₐ[F] K) (IsScalarTower.toAlgHom F L K)
    (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E))
have 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)
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
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
⊢ IntermediateField.LinearDisjoint (AlgHom.fieldRange (IsScalarTower.toAlgHom F L K)) L'
have 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))
Tactic: rw [linearDisjoint_iff] at H ⊢
Cleared hypotheses: H, K, inst_11, inst_12, inst_13, inst_14, inst_15, inst_16, inst_17, inst_18, inst_19, inst_20
-- 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
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 (toSubalgebra (AlgHom.fieldRange (IsScalarTower.toAlgHom F L K)))
    (AlgHom.range (IsScalarTower.toAlgHom F L' K))
have 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)))
Tactic: have := H.map (IsScalarTower.toAlgHom F E K) (RingHom.injective _)
-- 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
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 (toSubalgebra (AlgHom.fieldRange (IsScalarTower.toAlgHom F L K)))
    (AlgHom.range (IsScalarTower.toAlgHom F L' K))
have 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)))
Tactic: simp_rw [AlgHom.fieldRange_toSubalgebra, ← AlgHom.range_comp] at this
Cleared hypotheses: this
-- 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
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 (IsScalarTower.toAlgHom F L K)) (AlgHom.range (IsScalarTower.toAlgHom F L' K))
have h : Eq (α := L →ₐ[F] K) (IsScalarTower.toAlgHom F L K)
  (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E))
Tactic: convert! this
-- 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
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))
⊢ Subalgebra.LinearDisjoint (AlgHom.range (IsScalarTower.toAlgHom F L K)) (AlgHom.range (IsScalarTower.toAlgHom F L' K))
have h₁ : Eq (α := L' →ₐ[F] K) (IsScalarTower.toAlgHom F L' K)
  (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L' E))
Tactic: convert! this
-- 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
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)))
⊢ Eq (α := L →ₐ[F] K) (IsScalarTower.toAlgHom F L K)
    (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L E))
have 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)
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
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)))
⊢ Eq (α := L' →ₐ[F] K) (IsScalarTower.toAlgHom F L' K)
    (AlgHom.comp (IsScalarTower.toAlgHom F E K) (IsScalarTower.toAlgHom F L' E))
have 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)
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
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
x : L
x_1 : E
⊢ (AddMonoidHom.id E : (a : E) → E)
      (HSMul.hSMul (α := ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)))
        ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E) : (a : L) → ↥(IsScalarTower.toAlgHom F L E).range)
            x :
          ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)))
        x_1) =
    HSMul.hSMul (β := E) x ((AddMonoidHom.id E : (a : E) → E) x_1 : E)
have simp_rw : (AddMonoidHom.id E : (a : E) → E)
    (HMul.hMul (α := E)
      ((algebraMap (↥(AlgHom.range (IsScalarTower.toAlgHom F L E))) E : (a : ↥(IsScalarTower.toAlgHom F L E).range) → E)
          ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E) : (a : L) → ↥(IsScalarTower.toAlgHom F L E).range)
              x :
            ↥(AlgHom.range (IsScalarTower.toAlgHom F L E))) :
        E)
      x_1) =
  HMul.hMul (α := E) (β := E) ((algebraMap L E : (a : L) → E) x : E) ((AddMonoidHom.id E : (a : E) → E) x_1 : 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
ι : Type u_1
a : Basis.{u_1, u, v} ι F ↥A
H :
  LinearIndependent.{u_1, w, v} (ι := ι) L (M := E)
    (Function.comp (β := ↥A) (⇑A.val : (a : ↥A) → E) (⇑a : (a : ι) → ↥A))
x : L
x_1 : E
⊢ (AddMonoidHom.id E : (a : E) → E) (x • x_1) =
    HSMul.hSMul (α := ↥(AlgHom.range (IsScalarTower.toAlgHom F L E))) (β := E)
      ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E) : (a : L) → ↥(IsScalarTower.toAlgHom F L E).range) x :
        ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)))
      ((AddMonoidHom.id E : (a : E) → E) x_1 : E)
have simp_rw : (AddMonoidHom.id E : (a : E) → E) (HMul.hMul (α := E) ((algebraMap L E : (a : L) → E) x : E) x_1) =
  HMul.hMul (α := E) (β := E)
    ((algebraMap (↥(AlgHom.range (IsScalarTower.toAlgHom F L E))) E : (a : ↥(IsScalarTower.toAlgHom F L E).range) → E)
        ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E) : (a : L) → ↥(IsScalarTower.toAlgHom F L E).range)
            x :
          ↥(AlgHom.range (IsScalarTower.toAlgHom F L E))) :
      E)
    ((AddMonoidHom.id E : (a : E) → E) x_1 : 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
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' L
inst_10 : IsScalarTower F L' L
inst_11 : Algebra L' E
inst_12 : IsScalarTower F L' E
inst_13 : IsScalarTower L' L E
⊢ A.LinearDisjoint L'
have refine : LE.le (α := Subalgebra F E) (AlgHom.range (IsScalarTower.toAlgHom F L' E)) (AlgHom.range (IsScalarTower.toAlgHom F L E))
Tactic: refine Subalgebra.LinearDisjoint.of_le_right_of_flat 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
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' L
inst_10 : IsScalarTower F L' L
inst_11 : Algebra L' E
inst_12 : IsScalarTower F L' E
inst_13 : IsScalarTower L' L E
⊢ LE.le (α := Subalgebra F E) (AlgHom.range (IsScalarTower.toAlgHom F L' E))
    (AlgHom.range (IsScalarTower.toAlgHom F L E))
have h : Eq (α := L' →ₐ[F] E) (IsScalarTower.toAlgHom F L' E)
  (AlgHom.comp (IsScalarTower.toAlgHom F L E) (IsScalarTower.toAlgHom F L' L))
Tactic: convert! AlgHom.range_comp_le_range (IsScalarTower.toAlgHom F L' L) (IsScalarTower.toAlgHom F L E)