-- Mathlib/FieldTheory/LinearDisjoint.lean
theorem of_isField (H : IsField (A ⊗[F] L)) : A.LinearDisjoint L

Proof state:
case H
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : IsField (↥A ⊗[F] L)
⊢ IsField (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range)

Tactic:
haveI : SMulCommClass F A A := SMulCommClass.of_commMonoid F A A

Result:
case H
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : IsField (↥A ⊗[F] L)
this : SMulCommClass F ↥A ↥A
⊢ IsField (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range)

Proof state:
case H
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : IsField (↥A ⊗[F] L)
this✝ : SMulCommClass F ↥A ↥A
this : SMulCommClass F ↥A.toSubalgebra ↥A.toSubalgebra
⊢ IsField (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range)

Tactic:
letI : Mul (A ⊗[F] L) := Algebra.TensorProduct.instMul

Result:
case H
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : IsField (↥A ⊗[F] L)
this✝¹ : SMulCommClass F ↥A ↥A
this✝ : SMulCommClass F ↥A.toSubalgebra ↥A.toSubalgebra
this : Mul (↥A ⊗[F] L) := Algebra.TensorProduct.instMul
⊢ IsField (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range)

Proof state:
case H
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : IsField (↥A ⊗[F] L)
this : SMulCommClass F ↥A ↥A
⊢ IsField (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range)

Tactic:
haveI : SMulCommClass F A.toSubalgebra A.toSubalgebra := ‹SMulCommClass F A A›

Result:
case H
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : IsField (↥A ⊗[F] L)
this✝ : SMulCommClass F ↥A ↥A
this : SMulCommClass F ↥A.toSubalgebra ↥A.toSubalgebra
⊢ IsField (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range)

Proof state:
case H
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : IsField (↥A ⊗[F] L)
this✝² : SMulCommClass F ↥A ↥A
this✝¹ : SMulCommClass F ↥A.toSubalgebra ↥A.toSubalgebra
this✝ : Mul (↥A ⊗[F] L) := Algebra.TensorProduct.instMul
this : Mul (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range) := Algebra.TensorProduct.instMul
⊢ IsField (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range)

Tactic:
exact Algebra.TensorProduct.congr (AlgEquiv.refl : A ≃ₐ[F] A)
  (AlgEquiv.ofInjective (IsScalarTower.toAlgHom F L E) (RingHom.injective _))
    |>.symm.toMulEquiv.isField _ H

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : IsField (↥A ⊗[F] L)
⊢ A.LinearDisjoint L

Tactic:
apply Subalgebra.LinearDisjoint.of_isField

Result:
case H
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : IsField (↥A ⊗[F] L)
⊢ IsField (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range)

Proof state:
case H
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : IsField (↥A ⊗[F] L)
this✝¹ : SMulCommClass F ↥A ↥A
this✝ : SMulCommClass F ↥A.toSubalgebra ↥A.toSubalgebra
this : Mul (↥A ⊗[F] L) := Algebra.TensorProduct.instMul
⊢ IsField (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range)

Tactic:
letI : Mul (A.toSubalgebra ⊗[F] (IsScalarTower.toAlgHom F L E).range) :=
  Algebra.TensorProduct.instMul

Result:
case H
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : IsField (↥A ⊗[F] L)
this✝² : SMulCommClass F ↥A ↥A
this✝¹ : SMulCommClass F ↥A.toSubalgebra ↥A.toSubalgebra
this✝ : Mul (↥A ⊗[F] L) := Algebra.TensorProduct.instMul
this : Mul (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range) := Algebra.TensorProduct.instMul
⊢ IsField (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range)