awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
inst_55 : Free A R₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
⊢ Dvd.dvd (α := Ideal B) (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂)) (differentIdeal R₁ B)

Tactic:
map_differentIdeal_dvd_differentIdeal A B R₁ R₂ h₃

Premises used: Set.Mem, IsDedekindDomain.map_differentIdeal_dvd_differentIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
inst_55 : Free A R₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
⊢ Dvd.dvd (α := Ideal B) (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂)) (differentIdeal R₁ B)

Tactic:
exact map_differentIdeal_dvd_differentIdeal A B R₁ R₂ h₃

Premises used: IsDedekindDomain.map_differentIdeal_dvd_differentIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
inst_55 : Free A R₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
⊢ differentIdeal A B =
    HMul.hMul (α := Ideal B) (differentIdeal R₂ B) (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))

Tactic:
have := differentIdeal_eq_differentIdeal_mul_differentIdeal A R₂ B
-- Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
inst_55 : Free A R₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
this :
  differentIdeal A B =
    HMul.hMul (α := Ideal B) (differentIdeal R₂ B) (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
rwa :
  ∀ (this : differentIdeal A B = HMul.hMul (α := Ideal B) (differentIdeal R₂ B) (differentIdeal R₁ B)),
    differentIdeal A B = HMul.hMul (α := Ideal B) (differentIdeal R₁ B) (differentIdeal R₂ B)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : differentIdeal A B = HMul.hMul (α := Ideal B) (differentIdeal R₁ B) (differentIdeal R₂ B)),
    differentIdeal A B = HMul.hMul (α := Ideal B) (differentIdeal R₁ B) (differentIdeal R₂ B)
⊢ differentIdeal A B = HMul.hMul (α := Ideal B) (differentIdeal R₁ B) (differentIdeal R₂ B)

Tactic:
rwa [← differentIdeal_eq_map_differentIdeal A B R₁ R₂ h₁ h₂ h₃,
    mul_comm] at this

Premises used: IsDedekindDomain.differentIdeal_eq_map_differentIdeal, mul_comm
-- Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
inst_55 : Free A R₂
inst_56 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
⊢ Algebra.IsSeparable.{u_1, u_6} (FractionRing A) (FractionRing R₂)

Tactic:
Algebra.IsSeparable.of_equiv_equiv (FractionRing.algEquiv A K).symm.toRingEquiv
          (FractionRing.algEquiv R₂ F₂).symm.toRingEquiv ?_

Premises used: Algebra.IsSeparable.of_equiv_equiv, AlgEquiv.symm, Membership.mem, Subtype, FractionRing.algEquiv, AlgEquiv.toRingEquiv
-- Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
inst_55 : Free A R₂
inst_56 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
refine :
  Eq (α := RingHom.{u_3, u_6} K (FractionRing R₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing A) (FractionRing R₂))
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv A K))) : K →+* FractionRing A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv R₂ ↥F₂))) : ↥F₂ →+* FractionRing R₂)
      (algebraMap K ↥F₂))
⊢ Algebra.IsSeparable.{u_1, u_6} (FractionRing A) (FractionRing R₂)

Tactic:
refine Algebra.IsSeparable.of_equiv_equiv (FractionRing.algEquiv A K).symm.toRingEquiv
          (FractionRing.algEquiv R₂ F₂).symm.toRingEquiv ?_

Premises used: Algebra.IsSeparable.of_equiv_equiv, AlgEquiv.symm, Membership.mem, Subtype, FractionRing.algEquiv, AlgEquiv.toRingEquiv
-- Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
inst_55 : Free A R₂
inst_56 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
x : K
⊢ Eq.{u_6 + 1} (α := FractionRing R₂)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing A) (FractionRing R₂))
            (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv A K))) : K →+* FractionRing A) :
          (a : K) → FractionRing R₂)
        x :
      FractionRing R₂)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv R₂ ↥F₂))) : ↥F₂ →+* FractionRing R₂)
              (algebraMap K ↥F₂) :
            RingHom.{u_3, u_6} K (FractionRing R₂)) :
          (a : K) → FractionRing R₂)
        x :
      FractionRing R₂)

Tactic:
IsFractionRing.algEquiv_commutes (FractionRing.algEquiv A K).symm
      (FractionRing.algEquiv R₂ ↥F₂).symm _

Premises used: AlgEquiv.symm, Membership.mem, Subtype, FractionRing.algEquiv, IsFractionRing.algEquiv_commutes, OreLocalization.liftExpand
-- Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
inst_55 : Free A R₂
inst_56 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
x : K
⊢ Eq.{u_6 + 1} (α := FractionRing R₂)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing A) (FractionRing R₂))
            (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv A K))) : K →+* FractionRing A) :
          (a : K) → FractionRing R₂)
        x :
      FractionRing R₂)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv R₂ ↥F₂))) : ↥F₂ →+* FractionRing R₂)
              (algebraMap K ↥F₂) :
            RingHom.{u_3, u_6} K (FractionRing R₂)) :
          (a : K) → FractionRing R₂)
        x :
      FractionRing R₂)

Tactic:
exact IsFractionRing.algEquiv_commutes (FractionRing.algEquiv A K).symm
      (FractionRing.algEquiv R₂ ↥F₂).symm _

Premises used: AlgEquiv.symm, Membership.mem, Subtype, FractionRing.algEquiv, IsFractionRing.algEquiv_commutes
-- Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Goal:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : CommRing B
inst_5 : Field L
inst_6 : Algebra B L
inst_7 : Algebra A L
inst_8 : Algebra K L
inst_9 : FiniteDimensional K L
inst_10 : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst_11 : CommRing R₁
inst_12 : CommRing R₂
inst_13 : IsDomain R₁
inst_14 : Algebra A R₁
inst_15 : Algebra A R₂
inst_16 : Algebra R₁ B
inst_17 : Algebra R₂ B
inst_18 : Algebra R₁ L
inst_19 : Algebra R₂ L
inst_20 : IsScalarTower A R₁ L
inst_21 : IsScalarTower R₁ B L
inst_22 : IsScalarTower R₂ B L
inst_23 : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst_24 : Algebra.{u_5, u_4} R₁ ↥F₁
inst_25 : Algebra.{u_6, u_4} R₂ ↥F₂
inst_26 : IsTorsionFree.{u_5, u_4} R₁ ↥F₁
inst_27 : IsScalarTower A (↥F₂) L
inst_28 : IsScalarTower.{u_1, u_6, u_4} A R₂ ↥F₂
inst_29 : IsScalarTower R₁ (↥F₁) L
inst_30 : IsScalarTower R₂ (↥F₂) L
inst_31 : Algebra.IsSeparable.{u_3, u_4} K ↥F₂
inst_32 : Algebra.IsSeparable (↥F₁) L
inst_33 : IsDomain A
inst_34 : IsDedekindDomain B
inst_35 : IsDedekindDomain R₁
inst_36 : IsDedekindDomain R₂
inst_37 : IsFractionRing B L
inst_38 : IsFractionRing.{u_5, u_4} R₁ ↥F₁
inst_39 : IsFractionRing.{u_6, u_4} R₂ ↥F₂
inst_40 : IsIntegrallyClosed A
inst_41 : IsIntegralClosure B R₁ L
inst_42 : IsTorsionFree R₁ B
inst_43 : IsTorsionFree R₂ B
inst_44 : Algebra A B
inst_45 : Module.Finite A B
inst_46 : IsTorsionFree A B
inst_47 : IsTorsionFree A R₁
inst_48 : IsTorsionFree A R₂
inst_49 : Module.Finite A R₁
inst_50 : Module.Finite R₂ B
inst_51 : IsScalarTower A R₂ B
inst_52 : Module.Finite R₁ B
inst_53 : Algebra.IsSeparable.{u_1, u_2} (FractionRing A) (FractionRing B)
inst_54 : IsScalarTower A R₁ B
inst_55 : Free A R₂
inst_56 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
h₃ :
  IsCoprime.{u_2} (R := Ideal B) (Ideal.map (F := R₁ →+* B) (algebraMap R₁ B) (differentIdeal A R₁))
    (Ideal.map (F := R₂ →+* B) (algebraMap R₂ B) (differentIdeal A R₂))
⊢ Algebra.IsSeparable.{u_1, u_6} (FractionRing A) (FractionRing R₂)

Tactic:
have : Algebra.IsSeparable (FractionRing A) (FractionRing R₂) := by
    refine Algebra.IsSeparable.of_equiv_equiv (FractionRing.algEquiv A K).symm.toRingEquiv
          (FractionRing.algEquiv R₂ F₂).symm.toRingEquiv ?_
    ext x
    exact IsFractionRing.algEquiv_commutes (FractionRing.algEquiv A K).symm
      (FractionRing.algEquiv R₂ ↥F₂).symm _