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
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:
exact IsScalarTower.algebraMap_apply _ 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 :
  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
-- 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:
exact IsScalarTower.algebraMap_apply _ 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
⊢ A.LinearDisjoint F

Tactic:
Subalgebra.LinearDisjoint.bot_right _

Premises used: Subalgebra.LinearDisjoint.bot_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
⊢ A.LinearDisjoint ↥⊥

Tactic:
linearDisjoint_iff'.2 (Subalgebra.LinearDisjoint.bot_right _)

Premises used: Iff.mpr, IntermediateField.linearDisjoint_iff', Subalgebra.LinearDisjoint.bot_right
-- 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
⊢ IntermediateField.LinearDisjoint.{u, v, w} (F := F) (E := E) ⊥ L

Tactic:
Subalgebra.LinearDisjoint.bot_left _

Premises used: Subalgebra.LinearDisjoint.bot_left
-- 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
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
⊢ ∀ (r : L),
    Eq.{v + 1} (α := ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)))
        ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E) : (a : L) → ↥(IsScalarTower.toAlgHom F L E).range)
            r :
          ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)))
        (0 : ↥(AlgHom.range (IsScalarTower.toAlgHom F L E))) →
      r = 0

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
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
⊢ ∀ (m : E), Eq (α := E) ((AddMonoidHom.id E : (a : E) → E) m : E) (0 : E) → m = 0

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
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
x : L
x_1 : E
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)
⊢ (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)

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
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
x : L
x_1 : E
⊢ (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:
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
ι : 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))
⊢ ∀ (m : E), Eq (α := E) ((AddMonoidHom.id E : (a : E) → E) m : E) (0 : E) → m = 0

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
ι : 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
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)
⊢ (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)

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
ι : 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) (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:
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
H : A.LinearDisjoint ↥B
ι : Type u_1
b : ι → ↥B
hb : LinearIndependent F b
⊢ LinearIndependent ↥A (M := E) ((⇑B.val : (a : ↥B) → E) ∘ b)

Tactic:
(linearDisjoint_iff'.1 H).linearIndependent_right_of_flat hb

Premises used: Set.Mem, IntermediateField.linearDisjoint_iff', Subalgebra.LinearDisjoint.linearIndependent_right_of_flat, 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
H : A.LinearDisjoint ↥B
H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤
ι : Type u_1
b : Basis.{u_1, u, v} ι F ↥B
i : ι
⊢ Eq.{v + 1} (α := E) ((H.basisOfBasisRight H' b : (a : ι) → E) i : E)
    ((algebraMap (↥B) E : (a : ↥B) → E) ((b : (a : ι) → ↥B) i : ↥B) : E)

Tactic:
(linearDisjoint_iff'.mp H).algebraMap_basisOfBasisRight_apply H' b i

Premises used: Set.Mem, IntermediateField.linearDisjoint_iff', Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_apply, 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
H : A.LinearDisjoint ↥B
H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤
ι : Type u_1
b : Basis.{u_1, u, v} ι F ↥B
x : ↥B
i : ι
⊢ Eq (α := E)
    ((algebraMap (↥A) E : (a : ↥A) → E)
        (((((H.basisOfBasisRight H' b).repr : (a : E) → ι →₀ ↥A) (↑x : E) : Finsupp.{u_1, v} ι ↥A) : (a : ι) → ↥A) i :
          ↥A) :
      E)
    ((algebraMap F E : (a : F) → E) ((((b.repr : (a : ↥B) → ι →₀ F) x : ι →₀ F) : (a : ι) → F) i : F) : E)

Tactic:
(linearDisjoint_iff'.mp H).algebraMap_basisOfBasisRight_repr_apply H' b x i

Premises used: IntermediateField.linearDisjoint_iff', Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, 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
H : A.LinearDisjoint ↥B
H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤
ι : Type u_1
b : Basis.{u_1, u, v} ι F ↥A
i : ι
⊢ Eq.{v + 1} (α := E) ((H.basisOfBasisLeft H' b : (a : ι) → E) i : E)
    ((algebraMap (↥A) E : (a : ↥A) → E) ((b : (a : ι) → ↥A) i : ↥A) : E)

Tactic:
(linearDisjoint_iff'.mp H).basisOfBasisLeft_apply H' b i

Premises used: Set.Mem, IntermediateField.linearDisjoint_iff', Subalgebra.LinearDisjoint.basisOfBasisLeft_apply, 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
H : A.LinearDisjoint ↥B
H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤
ι : Type u_1
b : Basis.{u_1, u, v} ι F ↥A
x : ↥A
i : ι
⊢ Eq (α := E)
    ((algebraMap (↥B) E : (a : ↥B) → E)
        (((((H.basisOfBasisLeft H' b).repr : (a : E) → ι →₀ ↥B) (↑x : E) : Finsupp.{u_1, v} ι ↥B) : (a : ι) → ↥B) i :
          ↥B) :
      E)
    ((algebraMap F E : (a : F) → E) ((((b.repr : (a : ↥A) → ι →₀ F) x : ι →₀ F) : (a : ι) → F) i : F) : E)

Tactic:
(linearDisjoint_iff'.mp H).basisOfBasisLeft_repr_apply H' b x i

Premises used: IntermediateField.linearDisjoint_iff', Iff.mp, Subalgebra.LinearDisjoint.basisOfBasisLeft_repr_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 B : IntermediateField F E
ι : Type u_1
b : Basis.{u_1, u, v} ι F ↥B
H :
  LinearIndependent.{u_1, v, v} (ι := ι) ↥A (M := E)
    (Function.comp (β := ↥B) (⇑B.val : (a : ↥B) → E) (⇑b : (a : ι) → ↥B))
⊢ A.LinearDisjoint ↥B

Tactic:
linearDisjoint_iff'.2 (.of_basis_right _ _ b H)

Premises used: Iff.mpr, IntermediateField.linearDisjoint_iff', Subalgebra.LinearDisjoint.of_basis_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
ι : Type u_1
b : ι → L
hb : LinearIndependent F b
⊢ LinearIndependent.{u_1, v, v} ↥A (M := E) ((⇑(algebraMap L E) : (a : L) → E) ∘ b)

Tactic:
apply Subalgebra.LinearDisjoint.linearIndependent_right_of_flat H <| hb.map' _
    (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.ker

Premises used: AlgEquiv.ofInjectiveField, IsScalarTower.toAlgHom, LinearIndependent.map', Subalgebra.LinearDisjoint.linearIndependent_right_of_flat, AlgEquiv.toLinearEquiv, LinearEquiv.ker
-- 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
ι : Type u_1
b : Basis ι F L
H :
  LinearIndependent.{u_1, v, v} (ι := ι) ↥A (M := E)
    (Function.comp.{u_1 + 1, w + 1, v + 1} (β := L) (⇑(algebraMap L E) : (a : L) → E) (⇑b : (a : ι) → L))
⊢ A.LinearDisjoint L

Tactic:
Subalgebra.LinearDisjoint.of_basis_right _ _
    (b.map (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv) H

Premises used: AlgEquiv.ofInjectiveField, Module.Basis.map, IsScalarTower.toAlgHom, AlgEquiv.toLinearEquiv, Subalgebra.LinearDisjoint.of_basis_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 B : IntermediateField F E
H : A.LinearDisjoint ↥B
κ : Type u_1
ι : Type u_2
a : κ → ↥A
b : ι → ↥B
ha : LinearIndependent F a
hb : LinearIndependent F b
⊢ LinearIndependent F (M := E) fun (i : κ × ι) ↦ (↑(a i.1) : E) * (↑(b i.2) : E)

Tactic:
(linearDisjoint_iff'.1 H).linearIndependent_mul_of_flat_left ha hb

Premises used: Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat_left, 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 : 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
ι : Type u_2
a : κ → ↥A
b : ι → L
ha : LinearIndependent F a
hb : LinearIndependent F b
⊢ LinearIndependent F (M := E) fun (i : κ × ι) ↦
    HMul.hMul (β := E) (↑(a i.1) : E) ((algebraMap L E : (a : L) → E) (b i.2) : E)

Tactic:
apply Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat_left H ha <| hb.map' _
    (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.ker

Premises used: AlgEquiv.ofInjectiveField, Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat_left, IsScalarTower.toAlgHom, LinearIndependent.map', AlgEquiv.toLinearEquiv, LinearEquiv.ker
-- 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
κ : Type u_1
ι : Type u_2
a : Basis.{u_1, u, v} κ F ↥A
b : Basis.{u_2, u, v} ι F ↥B
H :
  LinearIndependent F (M := E) fun (i : κ × ι) ↦
    HMul.hMul (α := E) (↑((a : (a : κ) → ↥A) i.1) : E) (↑((b : (a : ι) → ↥B) i.2) : E)
⊢ A.LinearDisjoint ↥B

Tactic:
linearDisjoint_iff'.2 (.of_basis_mul _ _ a b H)

Premises used: Iff.mpr, Subalgebra.LinearDisjoint.of_basis_mul, 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
κ : Type u_1
ι : Type u_2
a : Basis.{u_1, u, v} κ F ↥A
b : Basis ι F L
H :
  LinearIndependent F (M := E) fun (i : κ × ι) ↦
    HMul.hMul (α := E) (β := E) ((↑((a : (a : κ) → ↥A) i.1) : E) : E)
      ((algebraMap L E : (a : L) → E) ((b : (a : ι) → L) i.2 : L) : E)
⊢ A.LinearDisjoint L

Tactic:
Subalgebra.LinearDisjoint.of_basis_mul _ _ a
    (b.map (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv) H

Premises used: AlgEquiv.ofInjectiveField, Subalgebra.LinearDisjoint.of_basis_mul, Module.Basis.map, IsScalarTower.toAlgHom, AlgEquiv.toLinearEquiv
-- 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' : IntermediateField F E
H : A.LinearDisjoint L
h : A' ≤ A
⊢ A'.LinearDisjoint L

Tactic:
Subalgebra.LinearDisjoint.of_le_left_of_flat H h

Premises used: Subalgebra.LinearDisjoint.of_le_left_of_flat
-- 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 B' : IntermediateField F E
H : A.LinearDisjoint ↥B
h : B' ≤ B
⊢ A.LinearDisjoint ↥B'

Tactic:
linearDisjoint_iff'.2 ((linearDisjoint_iff'.1 H).of_le_right_of_flat h)

Premises used: Iff.mpr, IntermediateField.linearDisjoint_iff', Iff.mp, Subalgebra.LinearDisjoint.of_le_right_of_flat
-- 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
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'

Tactic:
Subalgebra.LinearDisjoint.of_le_right_of_flat H ?_

Premises used: Subalgebra.LinearDisjoint.of_le_right_of_flat
-- 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
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
refine :
  LE.le (α := Subalgebra F E) (AlgHom.range (IsScalarTower.toAlgHom F L' E))
    (AlgHom.range (IsScalarTower.toAlgHom F L E))
⊢ A.LinearDisjoint L'

Tactic:
refine Subalgebra.LinearDisjoint.of_le_right_of_flat H ?_

Premises used: Subalgebra.LinearDisjoint.of_le_right_of_flat
-- 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
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 (AlgHom.comp (IsScalarTower.toAlgHom F L E) (IsScalarTower.toAlgHom F L' L)))
    (AlgHom.range (IsScalarTower.toAlgHom F L E))

Tactic:
AlgHom.range_comp_le_range (IsScalarTower.toAlgHom F L' L) (IsScalarTower.toAlgHom F L E)

Premises used: AlgHom.range_comp_le_range, IsScalarTower.toAlgHom