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
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
a₁ :
  (↑(((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)) :
      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 ⋯)) → ↥(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)))) :
      E)
⊢ ((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)))

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 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)))
          (HMul.hMul (α := ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯))
            ((algebraMap ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) :
                  (a : ↥A) → ↥(extendScalars ⋯))
                (Subtype.mk (p := fun (x : E) ↦ x ∈ A) a ha) :
              ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : 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))) :
      E) =
    (↑(HMul.hMul (α := ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E))) (β :=
          ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
          ((algebraMap ↥A.toSubalgebra ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)) :
                (a : ↥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)) :
            ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
          (((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)))) :
      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
H : A.LinearDisjoint L
inst_7 : Algebra.IsAlgebraic.{u, v} F ↥A
⊢ Cardinal.lift.{w, v} (Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯)) =
    Cardinal.lift.{v, w} (Module.rank F L)

Tactic:
H.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic (.inl ‹_›)

Premises used: IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic, Or.inl
-- 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
inst_7 : 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)

Tactic:
H.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic (.inr ‹_›)

Premises used: IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic, Or.inr
-- 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
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
rw :
  Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) *
      Module.rank (↥(adjoin L (↑A : Set E))) E =
    Module.rank (↥A) E
⊢ 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)

Tactic:
rw [← H.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic halg, ← Cardinal.lift_mul,
    Cardinal.lift_inj]

Premises used: Cardinal.lift_inj, Cardinal.lift_mul, IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic
-- 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
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) *
      Module.rank (↥(adjoin L (↑A : Set E))) E =
    Module.rank (↥A) E

Tactic:
rank_mul_rank A (extendScalars
    (show A ≤ (adjoin L (A : Set E)).restrictScalars F from subset_adjoin L (A : Set E))) E

Premises used: iInf, Submonoid.copy, Set.Mem, Set.iInter, rank_mul_rank, Membership.mem, Subtype, IntermediateField.extendScalars, IntermediateField.subset_adjoin, SetLike.coe, IntermediateField.adjoin, Subfield.extendScalars, Subfield.toIntermediateField
-- 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
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) *
      Module.rank (↥(adjoin L (↑A : Set E))) E =
    Module.rank (↥A) E

Tactic:
exact rank_mul_rank A (extendScalars
    (show A ≤ (adjoin L (A : Set E)).restrictScalars F from subset_adjoin L (A : Set E))) E

Premises used: rank_mul_rank, Membership.mem, Subtype, IntermediateField.extendScalars, IntermediateField.subset_adjoin, SetLike.coe
-- 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
inst_7 : Algebra.IsAlgebraic.{u, v} F ↥A
⊢ 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)

Tactic:
H.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic (.inl ‹_›)

Premises used: IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic, Or.inl
-- 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
inst_7 : 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)

Tactic:
H.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic (.inr ‹_›)

Premises used: IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic, Or.inr
-- 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 v
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
⊢ Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) = Module.rank F L

Tactic:
simpa only [Cardinal.lift_id] using H.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic halg

Premises used: IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic, Cardinal.lift_id
-- 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 v
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
inst_7 : Algebra.IsAlgebraic.{u, v} F ↥A
⊢ Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) = Module.rank F L

Tactic:
H.adjoin_rank_eq_rank_right_of_isAlgebraic (.inl ‹_›)

Premises used: Or.inl, IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic
-- 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 v
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
inst_7 : Algebra.IsAlgebraic F L
⊢ Module.rank ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) = Module.rank F L

Tactic:
H.adjoin_rank_eq_rank_right_of_isAlgebraic (.inr ‹_›)

Premises used: IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic, Or.inr
-- 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 v
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
⊢ Module.rank F L * Module.rank (↥(adjoin L (↑A : Set E))) E = Module.rank (↥A) E

Tactic:
simpa only [Cardinal.lift_id] using H.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic halg

Premises used: IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic, Cardinal.lift_id
-- 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 v
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
inst_7 : Algebra.IsAlgebraic.{u, v} F ↥A
⊢ Module.rank F L * Module.rank (↥(adjoin L (↑A : Set E))) E = Module.rank (↥A) E

Tactic:
H.rank_right_mul_adjoin_rank_eq_of_isAlgebraic (.inl ‹_›)

Premises used: IntermediateField.LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic, Or.inl
-- 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 v
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
inst_7 : Algebra.IsAlgebraic F L
⊢ Module.rank F L * Module.rank (↥(adjoin L (↑A : Set E))) E = Module.rank (↥A) E

Tactic:
H.rank_right_mul_adjoin_rank_eq_of_isAlgebraic (.inr ‹_›)

Premises used: IntermediateField.LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic, Or.inr
-- 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 : (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 := ⋯ }
rwa rwa₁ rwa₂ 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)))
⊢ (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

Premises used: AlgEquiv.ofInjectiveField, IsScalarTower.toAlgHom, LinearEquiv.finrank_eq, 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
H : A.LinearDisjoint L
⊢ IsDomain (TensorProduct.{u, v, w} F (↥A) L)

Tactic:
have : IsDomain (A ⊗[F] _) := Subalgebra.LinearDisjoint.isDomain H
  (Algebra.TensorProduct.congr (AlgEquiv.refl : A ≃ₐ[F] A)
    (AlgEquiv.ofInjective (IsScalarTower.toAlgHom F L E) (RingHom.injective _))).toMulEquiv.isDomain

Premises used: Set.Mem, IsScalarTower.toAlgHom, Membership.mem, Subtype, AlgEquiv.toMulEquiv, RingHom.injective, AlgHom.toRingHom, AlgEquiv.ofInjective, MulEquiv.isDomain, TensorProduct, Algebra.TensorProduct.congr, Subalgebra.LinearDisjoint.isDomain, AlgEquiv.refl, AlgHom.range
-- Module: Mathlib.FieldTheory.LinearDisjoint
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
⊢ fa.range.LinearDisjoint fb.range

Tactic:
simp_rw [linearDisjoint_iff', AlgHom.fieldRange_toSubalgebra] at H

Premises used: AlgHom.fieldRange_toSubalgebra, 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 : 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.range.LinearDisjoint fb.range
⊢ IsDomain (A ⊗[F] B)

Tactic:
H.isDomain_of_injective fa.injective fb.injective

Premises used: RingHom.injective, AlgHom.toRingHom, Subalgebra.LinearDisjoint.isDomain_of_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 : 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.range.LinearDisjoint fb.range
⊢ IsDomain (A ⊗[F] B)

Tactic:
exact H.isDomain_of_injective fa.injective fb.injective

Premises used: RingHom.injective, AlgHom.toRingHom, Subalgebra.LinearDisjoint.isDomain_of_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 : IsField (TensorProduct.{u, v, w} F (↥A) L)
H₁ : IsField.{v} (↥A.toSubalgebra ⊗[F] ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)))
⊢ A.LinearDisjoint L

Tactic:
apply Subalgebra.LinearDisjoint.of_isField

Premises used: Subalgebra.LinearDisjoint.of_isField
-- 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 : IsField (TensorProduct.{u, v, w} F (↥A) L)
⊢ SMulCommClass.{u, v, v} F ↥A ↥A

Tactic:
haveI : SMulCommClass F A A := SMulCommClass.of_commMonoid F A A
-- 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 : IsField (TensorProduct.{u, v, w} F (↥A) L)
this : SMulCommClass.{u, v, v} F ↥A ↥A
⊢ SMulCommClass.{u, v, v} F ↥A.toSubalgebra ↥A.toSubalgebra

Tactic:
haveI : SMulCommClass F A.toSubalgebra A.toSubalgebra := ‹SMulCommClass F A A›
-- 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 : IsField (TensorProduct.{u, v, w} F (↥A) L)
this_1 : SMulCommClass.{u, v, v} F ↥A ↥A
this_2 : SMulCommClass.{u, v, v} F ↥A.toSubalgebra ↥A.toSubalgebra
this_3 : Mul (TensorProduct.{u, v, w} F (↥A) L) := Algebra.TensorProduct.instMul
this : Mul (↥A.toSubalgebra ⊗[F] ↥(AlgHom.range (IsScalarTower.toAlgHom F L E))) := Algebra.TensorProduct.instMul
⊢ IsField.{v} (↥A.toSubalgebra ⊗[F] ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)))

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

Premises used: AlgEquiv.symm, IsScalarTower.toAlgHom, AlgEquiv.toMulEquiv, RingHom.injective, AlgEquiv.ofInjective, MulEquiv.isField, Algebra.TensorProduct.congr, AlgEquiv.refl
-- 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 : IsField (TensorProduct.{u, v, w} F (↥A) L)
this_1 : SMulCommClass.{u, v, v} F ↥A ↥A
this_2 : SMulCommClass.{u, v, v} F ↥A.toSubalgebra ↥A.toSubalgebra
this_3 : Mul (TensorProduct.{u, v, w} F (↥A) L) := Algebra.TensorProduct.instMul
this : Mul (↥A.toSubalgebra ⊗[F] ↥(AlgHom.range (IsScalarTower.toAlgHom F L E))) := Algebra.TensorProduct.instMul
⊢ IsField.{v} (↥A.toSubalgebra ⊗[F] ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)))

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

Premises used: AlgEquiv.symm, IsScalarTower.toAlgHom, AlgEquiv.toMulEquiv, RingHom.injective, AlgEquiv.ofInjective, MulEquiv.isField, Algebra.TensorProduct.congr, AlgEquiv.refl
-- Module: Mathlib.FieldTheory.LinearDisjoint
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
rw : fa.fieldRange.LinearDisjoint fb.fieldRange.toSubalgebra
⊢ fa.fieldRange.LinearDisjoint ↥fb.fieldRange

Tactic:
rw [linearDisjoint_iff']

Premises used: IntermediateField.linearDisjoint_iff'
-- Module: Mathlib.FieldTheory.LinearDisjoint
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
H₁ : IsField.{u_1} (↥fa.fieldRange.toSubalgebra ⊗[F] ↥fb.fieldRange.toSubalgebra)
⊢ fa.fieldRange.LinearDisjoint fb.fieldRange.toSubalgebra

Tactic:
apply Subalgebra.LinearDisjoint.of_isField

Premises used: Subalgebra.LinearDisjoint.of_isField
-- Module: Mathlib.FieldTheory.LinearDisjoint
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
⊢ IsField.{u_1} (↥fa.fieldRange.toSubalgebra ⊗[F] ↥fb.fieldRange.toSubalgebra)

Tactic:
Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa fa.injective)
    (AlgEquiv.ofInjective fb fb.injective) |>.symm.toMulEquiv.isField H

Premises used: AlgEquiv.symm, AlgEquiv.toMulEquiv, RingHom.injective, AlgHom.toRingHom, AlgEquiv.ofInjective, MulEquiv.isField, Algebra.TensorProduct.congr