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
⊢ F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤

Tactic:
have h₂' : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤ := by
    simpa [sup_toSubalgebra_of_isAlgebraic_right] using congr_arg IntermediateField.toSubalgebra h₂
-- 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₂
rw :
  ∀ (i : Free.ChooseBasisIndex A R₂),
    Membership.mem.{u_4, u_4} (α := ↥F₁) (γ := Set ↥F₁)
      (Set.range.{u_4, u_5 + 1} (ι := R₁) (⇑(algebraMap R₁ ↥F₁) : (a : R₁) → ↥F₁))
      ((((B₁.traceDual.repr : (a : L) → Free.ChooseBasisIndex A R₂ →₀ ↥F₁) x :
              Finsupp.{u_6, u_4} (Free.ChooseBasisIndex A R₂) ↥F₁) :
            (a : Free.ChooseBasisIndex A R₂) → ↥F₁)
          i :
        ↥F₁)
⊢ 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

Tactic:
rw [B₁.traceDual.mem_span_iff_repr_mem R₁ x]

Premises used: Module.Basis.traceDual, Module.Basis.mem_span_iff_repr_mem
-- 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₂
i : Free.ChooseBasisIndex A R₂
rw :
  Membership.mem (α := ↥F₁) (γ := Set ↥F₁) (Set.range.{u_4, u_5 + 1} (ι := R₁) (⇑(algebraMap R₁ ↥F₁) : (a : R₁) → ↥F₁))
    ((((traceForm (↥F₁) L : (a : L) → L →ₗ[↥F₁] ↥F₁) x : LinearMap (R := ↥F₁) (RingHom.id ↥F₁) L ↥F₁) : (a : L) → ↥F₁)
        ((B₁ : (a : Free.ChooseBasisIndex A R₂) → L) i) :
      ↥F₁)
⊢ Membership.mem.{u_4, u_4} (α := ↥F₁) (γ := Set ↥F₁)
    (Set.range.{u_4, u_5 + 1} (ι := R₁) (⇑(algebraMap R₁ ↥F₁) : (a : R₁) → ↥F₁))
    ((((B₁.traceDual.repr : (a : L) → Free.ChooseBasisIndex A R₂ →₀ ↥F₁) x :
            Finsupp.{u_6, u_4} (Free.ChooseBasisIndex A R₂) ↥F₁) :
          (a : Free.ChooseBasisIndex A R₂) → ↥F₁)
        i :
      ↥F₁)

Tactic:
rw [B₁.traceDual_repr_apply]

Premises used: Module.Basis.traceDual_repr_apply
-- 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₂
i : Free.ChooseBasisIndex A R₂
⊢ Membership.mem (α := ↥F₁) (γ := Set ↥F₁) (Set.range.{u_4, u_5 + 1} (ι := R₁) (⇑(algebraMap R₁ ↥F₁) : (a : R₁) → ↥F₁))
    ((((traceForm (↥F₁) L : (a : L) → L →ₗ[↥F₁] ↥F₁) x : LinearMap (R := ↥F₁) (RingHom.id ↥F₁) L ↥F₁) : (a : L) → ↥F₁)
        ((B₁ : (a : Free.ChooseBasisIndex A R₂) → L) i) :
      ↥F₁)

Tactic:
mem_traceDual.mp hx _ ?_

Premises used: Set.Mem, setOf, Submodule.mem_traceDual, Iff.mp, Set.range
-- 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₂
i : Free.ChooseBasisIndex A R₂
refine : Membership.mem.{u_4, u_4} (α := L) (γ := Submodule B L) 1 ((B₁ : (a : Free.ChooseBasisIndex A R₂) → L) i : L)
⊢ Membership.mem (α := ↥F₁) (γ := Set ↥F₁) (Set.range.{u_4, u_5 + 1} (ι := R₁) (⇑(algebraMap R₁ ↥F₁) : (a : R₁) → ↥F₁))
    ((((traceForm (↥F₁) L : (a : L) → L →ₗ[↥F₁] ↥F₁) x : LinearMap (R := ↥F₁) (RingHom.id ↥F₁) L ↥F₁) : (a : L) → ↥F₁)
        ((B₁ : (a : Free.ChooseBasisIndex A R₂) → L) i) :
      ↥F₁)

Tactic:
refine mem_traceDual.mp hx _ ?_

Premises used: Submodule.mem_traceDual, Iff.mp
-- 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₂
i : Free.ChooseBasisIndex A R₂
rw :
  ∃ (y : B),
    Eq.{u_4 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L)
      ((algebraMap B L : (a : B) → L)
          ((algebraMap R₂ B : (a : R₂) → B) ((Free.chooseBasis A R₂ : (a : Free.ChooseBasisIndex A R₂) → R₂) i : R₂) :
            B) :
        L)
⊢ Membership.mem.{u_4, u_4} (α := L) (γ := Submodule B L) 1 ((B₁ : (a : Free.ChooseBasisIndex A R₂) → L) i : L)

Tactic:
rw [LinearDisjoint.basisOfBasisRight_apply, Basis.localizationLocalization_apply,
      ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R₂ B L, mem_one]

Premises used: Module.Basis.localizationLocalization_apply, IntermediateField.LinearDisjoint.basisOfBasisRight_apply, Submodule.mem_one, IsScalarTower.algebraMap_apply
-- 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₂
i : Free.ChooseBasisIndex A R₂
⊢ ∃ (y : B),
    Eq.{u_4 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L)
      ((algebraMap B L : (a : B) → L)
          ((algebraMap R₂ B : (a : R₂) → B) ((Free.chooseBasis A R₂ : (a : Free.ChooseBasisIndex A R₂) → R₂) i : R₂) :
            B) :
        L)

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- 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₂
i : Free.ChooseBasisIndex A R₂
⊢ ∃ (y : B),
    Eq.{u_4 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L)
      ((algebraMap B L : (a : B) → L)
          ((algebraMap R₂ B : (a : R₂) → B) ((Free.chooseBasis A R₂ : (a : Free.ChooseBasisIndex A R₂) → R₂) i : R₂) :
            B) :
        L)

Tactic:
exact ⟨_, rfl⟩
-- 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₂
⊢ 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

Tactic:
have h_main : x ∈ span R₁ (Set.range B₁.traceDual) := by
    rw [B₁.traceDual.mem_span_iff_repr_mem R₁ x]
    intro i
    rw [B₁.traceDual_repr_apply]
    refine mem_traceDual.mp hx _ ?_
    rw [LinearDisjoint.basisOfBasisRight_apply, Basis.localizationLocalization_apply,
      ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R₂ B L, mem_one]
    exact ⟨_, rfl⟩
-- 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:
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