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 : Free A R₂
inst_34 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
x : L
hx : Membership.mem (γ := Submodule R₁ L) (restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (traceDual R₁ (↥F₁) 1)) x
h₂' : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
b₂ : Basis.{u_6, u_3, u_4} (Free.ChooseBasisIndex A R₂) K ↥F₂ :=
  Basis.localizationLocalization.{u_1, u_3, u_6, u_4, u_6} (R := A) K A⁰ (A := R₂) (↥F₂) (Free.chooseBasis A R₂)
B₁ : Basis.{u_6, u_4, u_4} (Free.ChooseBasisIndex A R₂) (↥F₁) L := h₁.basisOfBasisRight h₂' b₂
h_main :
  Membership.mem (γ := Submodule R₁ L)
    (span R₁
      (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂)
        (⇑B₁.traceDual : (a : Free.ChooseBasisIndex A R₂) → L)))
    x
refine :
  ∀ (i j : Free.ChooseBasisIndex A R₂),
    Eq (α := ↥F₁)
      (((traceForm (↥F₁) L : (a : L) → L →ₗ[↥F₁] ↥F₁)
              (Function.comp (β := ↥F₂) (⇑(IsScalarTower.toAlgHom A (↥F₂) L) : (a : ↥F₂) → L)
                (⇑b₂.traceDual : (a : Free.ChooseBasisIndex A R₂) → ↥F₂) i) :
            (a : L) → ↥F₁)
          ((B₁ : (a : Free.ChooseBasisIndex A R₂) → L) j) :
        ↥F₁)
      (if j = i then 1 else 0 : ↥F₁)
⊢ Eq (α := Set L)
    (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂) (⇑B₁.traceDual : (a : Free.ChooseBasisIndex A R₂) → L))
    (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂)
      (Function.comp (β := ↥F₂) (⇑(IsScalarTower.toAlgHom A (↥F₂) L) : (a : ↥F₂) → L)
        (⇑b₂.traceDual : (a : Free.ChooseBasisIndex A R₂) → ↥F₂)))

Tactic:
refine congr_arg Set.range <| B₁.traceDual_eq_iff.mpr fun i j ↦ ?_

Premises used: Iff.mpr, congr_arg, Set.range, Module.Basis.traceDual_eq_iff
-- 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 : Free A R₂
inst_34 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
x : L
hx : Membership.mem (γ := Submodule R₁ L) (restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (traceDual R₁ (↥F₁) 1)) x
h₂' : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
b₂ : Basis.{u_6, u_3, u_4} (Free.ChooseBasisIndex A R₂) K ↥F₂ :=
  Basis.localizationLocalization.{u_1, u_3, u_6, u_4, u_6} (R := A) K A⁰ (A := R₂) (↥F₂) (Free.chooseBasis A R₂)
B₁ : Basis.{u_6, u_4, u_4} (Free.ChooseBasisIndex A R₂) (↥F₁) L := h₁.basisOfBasisRight h₂' b₂
h_main :
  Membership.mem (γ := Submodule R₁ L)
    (span R₁
      (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂)
        (⇑B₁.traceDual : (a : Free.ChooseBasisIndex A R₂) → L)))
    x
⊢ Eq (α := Set L)
    (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂) (⇑B₁.traceDual : (a : Free.ChooseBasisIndex A R₂) → L))
    (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂)
      (Function.comp (β := ↥F₂) (⇑(IsScalarTower.toAlgHom A (↥F₂) L) : (a : ↥F₂) → L)
        (⇑b₂.traceDual : (a : Free.ChooseBasisIndex A R₂) → ↥F₂)))

Tactic:
have h : Set.range B₁.traceDual =
      Set.range (IsScalarTower.toAlgHom A F₂ L ∘ b₂.traceDual) := by
    refine congr_arg Set.range <| B₁.traceDual_eq_iff.mpr fun i j ↦ ?_
    rw [LinearDisjoint.basisOfBasisRight_apply, traceForm_apply, Function.comp_apply,
      IsScalarTower.coe_toAlgHom', ← map_mul, h₁.trace_algebraMap h₂, b₂.trace_traceDual_mul,
      MonoidWithZeroHom.map_ite_one_zero]
-- 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 : Free A R₂
inst_34 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
x : L
hx : Membership.mem (γ := Submodule R₁ L) (restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (traceDual R₁ (↥F₁) 1)) x
h₂' : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
b₂ : Basis.{u_6, u_3, u_4} (Free.ChooseBasisIndex A R₂) K ↥F₂ :=
  Basis.localizationLocalization.{u_1, u_3, u_6, u_4, u_6} (R := A) K A⁰ (A := R₂) (↥F₂) (Free.chooseBasis A R₂)
B₁ : Basis.{u_6, u_4, u_4} (Free.ChooseBasisIndex A R₂) (↥F₁) L := h₁.basisOfBasisRight h₂' b₂
h_main :
  Membership.mem (γ := Submodule R₁ L)
    (span R₁
      (↑(map (M := ↥F₂) (AlgHom.toLinearMap (IsScalarTower.toAlgHom A (↥F₂) L))
            (span A
              (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂)
                (⇑b₂.traceDual : (a : Free.ChooseBasisIndex A R₂) → ↥F₂)))) :
        Set L))
    x
h :
  Eq (α := Set L)
    (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂) (⇑B₁.traceDual : (a : Free.ChooseBasisIndex A R₂) → L))
    (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂)
      (Function.comp (β := ↥F₂) (⇑(IsScalarTower.toAlgHom A (↥F₂) L) : (a : ↥F₂) → L)
        (⇑b₂.traceDual : (a : Free.ChooseBasisIndex A R₂) → ↥F₂)))
rw :
  Eq.{u_4 + 1} (α := Submodule A ↥F₂) (restrictScalars.{u_1, u_6, u_4} A (R := R₂) 1)
    (LinearMap.range.{u_1, u_1, u_6, u_4} (M := R₂) (τ₁₂ := RingHom.id A)
      (↑(IsScalarTower.toAlgHom A R₂ ↥F₂) :
        [inst_35 : FunLike (R₂ →ₐ[A] ↥F₂) R₂ ↥F₂] →
          [SemilinearMapClass (R₂ →ₐ[A] ↥F₂) (RingHom.id A) R₂ ↥F₂] → R₂ →ₗ[A] ↥F₂))
⊢ Eq.{u_4 + 1} (α := Submodule A ↥F₂) (restrictScalars.{u_1, u_6, u_4} A (R := R₂) 1)
    (span A (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂) (⇑b₂ : (a : Free.ChooseBasisIndex A R₂) → ↥F₂)))

Tactic:
rw [Basis.localizationLocalization_span K A⁰ F₂]

Premises used: Membership.mem, nonZeroDivisors, Subtype, Module.Basis.localizationLocalization_span
-- 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 : Free A R₂
inst_34 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
x : L
hx : Membership.mem (γ := Submodule R₁ L) (restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (traceDual R₁ (↥F₁) 1)) x
h₂' : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
b₂ : Basis.{u_6, u_3, u_4} (Free.ChooseBasisIndex A R₂) K ↥F₂ :=
  Basis.localizationLocalization.{u_1, u_3, u_6, u_4, u_6} (R := A) K A⁰ (A := R₂) (↥F₂) (Free.chooseBasis A R₂)
B₁ : Basis.{u_6, u_4, u_4} (Free.ChooseBasisIndex A R₂) (↥F₁) L := h₁.basisOfBasisRight h₂' b₂
h_main :
  Membership.mem (γ := Submodule R₁ L)
    (span R₁
      (↑(map (M := ↥F₂) (AlgHom.toLinearMap (IsScalarTower.toAlgHom A (↥F₂) L))
            (span A
              (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂)
                (⇑b₂.traceDual : (a : Free.ChooseBasisIndex A R₂) → ↥F₂)))) :
        Set L))
    x
h :
  Eq (α := Set L)
    (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂) (⇑B₁.traceDual : (a : Free.ChooseBasisIndex A R₂) → L))
    (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂)
      (Function.comp (β := ↥F₂) (⇑(IsScalarTower.toAlgHom A (↥F₂) L) : (a : ↥F₂) → L)
        (⇑b₂.traceDual : (a : Free.ChooseBasisIndex A R₂) → ↥F₂)))
h₃ :
  ∀ (x : ↥F₂),
    Membership.mem (γ := Submodule A ↥F₂) (restrictScalars.{u_1, u_6, u_4} A (R := R₂) 1) x ↔
      Membership.mem (γ := Submodule A ↥F₂)
        (LinearMap.range.{u_1, u_1, u_6, u_4} (M := R₂) (τ₁₂ := RingHom.id A)
          (↑(IsScalarTower.toAlgHom A R₂ ↥F₂) :
            [inst_35 : FunLike (R₂ →ₐ[A] ↥F₂) R₂ ↥F₂] →
              [SemilinearMapClass (R₂ →ₐ[A] ↥F₂) (RingHom.id A) R₂ ↥F₂] → R₂ →ₗ[A] ↥F₂))
        x
⊢ Eq.{u_4 + 1} (α := Submodule A ↥F₂) (restrictScalars.{u_1, u_6, u_4} A (R := R₂) 1)
    (LinearMap.range.{u_1, u_1, u_6, u_4} (M := R₂) (τ₁₂ := RingHom.id A)
      (↑(IsScalarTower.toAlgHom A R₂ ↥F₂) :
        [inst_35 : FunLike (R₂ →ₐ[A] ↥F₂) R₂ ↥F₂] →
          [SemilinearMapClass (R₂ →ₐ[A] ↥F₂) (RingHom.id A) R₂ ↥F₂] → R₂ →ₗ[A] ↥F₂))

Tactic:
ext
-- 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 : Free A R₂
inst_34 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
x : L
hx : Membership.mem (γ := Submodule R₁ L) (restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (traceDual R₁ (↥F₁) 1)) x
h₂' : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
b₂ : Basis.{u_6, u_3, u_4} (Free.ChooseBasisIndex A R₂) K ↥F₂ :=
  Basis.localizationLocalization.{u_1, u_3, u_6, u_4, u_6} (R := A) K A⁰ (A := R₂) (↥F₂) (Free.chooseBasis A R₂)
B₁ : Basis.{u_6, u_4, u_4} (Free.ChooseBasisIndex A R₂) (↥F₁) L := h₁.basisOfBasisRight h₂' b₂
h_main :
  Membership.mem (γ := Submodule R₁ L)
    (span R₁
      (↑(map (M := ↥F₂) (AlgHom.toLinearMap (IsScalarTower.toAlgHom A (↥F₂) L))
            (span A
              (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂)
                (⇑b₂.traceDual : (a : Free.ChooseBasisIndex A R₂) → ↥F₂)))) :
        Set L))
    x
h :
  Eq (α := Set L)
    (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂) (⇑B₁.traceDual : (a : Free.ChooseBasisIndex A R₂) → L))
    (Set.range.{u_4, u_6 + 1} (ι := Free.ChooseBasisIndex A R₂)
      (Function.comp (β := ↥F₂) (⇑(IsScalarTower.toAlgHom A (↥F₂) L) : (a : ↥F₂) → L)
        (⇑b₂.traceDual : (a : Free.ChooseBasisIndex A R₂) → ↥F₂)))
x_1 : ↥F₂
⊢ Membership.mem (γ := Submodule A ↥F₂) (restrictScalars.{u_1, u_6, u_4} A (R := R₂) 1) x_1 ↔
    Membership.mem (γ := Submodule A ↥F₂)
      (LinearMap.range.{u_1, u_1, u_6, u_4} (M := R₂) (τ₁₂ := RingHom.id A)
        (↑(IsScalarTower.toAlgHom A R₂ ↥F₂) :
          [inst_35 : FunLike (R₂ →ₐ[A] ↥F₂) R₂ ↥F₂] →
            [SemilinearMapClass (R₂ →ₐ[A] ↥F₂) (RingHom.id A) R₂ ↥F₂] → R₂ →ₗ[A] ↥F₂))
      x_1

Tactic:
simp
-- 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.IsIntegral R₂ B
inst_45 : Free A R₂
inst_46 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
⊢ 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.IsIntegral R₂ B
inst_45 : Free A R₂
inst_46 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
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.IsIntegral R₂ B
inst_45 : Free A R₂
inst_46 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
a :
  ∀ (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₂)
⊢ 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₂))

Tactic:
ext _
-- 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.IsIntegral R₂ B
inst_45 : Free A R₂
inst_46 : IsLocalization.{u_6, u_4} (algebraMapSubmonoid.{u_1, u_6} (R := A) R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
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