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₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
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₂))
ι : Type u_7
b : Basis.{u_7, u_3, u_4} ι K ↥F₂
hb :
  Eq.{u_4 + 1} (α := Submodule A ↥F₂) (span A (Set.range.{u_4, u_7 + 1} (ι := ι) (⇑b : (a : ι) → ↥F₂)))
    (LinearMap.range.{u_1, u_1, u_6, u_4} (M := R₂) (τ₁₂ := RingHom.id A)
      (↑(IsScalarTower.toAlgHom A R₂ ↥F₂) :
        [inst_56 : FunLike (R₂ →ₐ[A] ↥F₂) R₂ ↥F₂] →
          [SemilinearMapClass (R₂ →ₐ[A] ↥F₂) (RingHom.id A) R₂ ↥F₂] → R₂ →ₗ[A] ↥F₂))
h₂' : F₁ ⊔ F₂ = ⊤
this : Finite ι
⊢ Eq.{u_4 + 1} (α := Submodule R₁ L)
    (Submodule.restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (↑(dual R₁ (↥F₁) (dual R₁ (↥F₁) 1)) : Submodule B L))
    (Submodule.restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (↑1 : Submodule B L))

Tactic:
have h_main := congr_arg (Submodule.restrictScalars R₁) <|
    congr_arg coeToSubmodule <| (1 : FractionalIdeal B⁰ L).dual_dual R₁ F₁
-- 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₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
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₂))
ι : Type u_7
b : Basis.{u_7, u_3, u_4} ι K ↥F₂
hb :
  Eq.{u_4 + 1} (α := Submodule A ↥F₂) (span A (Set.range.{u_4, u_7 + 1} (ι := ι) (⇑b : (a : ι) → ↥F₂)))
    (LinearMap.range.{u_1, u_1, u_6, u_4} (M := R₂) (τ₁₂ := RingHom.id A)
      (↑(IsScalarTower.toAlgHom A R₂ ↥F₂) :
        [inst_56 : FunLike (R₂ →ₐ[A] ↥F₂) R₂ ↥F₂] →
          [SemilinearMapClass (R₂ →ₐ[A] ↥F₂) (RingHom.id A) R₂ ↥F₂] → R₂ →ₗ[A] ↥F₂))
h₂' : F₁ ⊔ F₂ = ⊤
this : Finite ι
h_main :
  Eq.{u_4 + 1} (α := Submodule R₁ L)
    (Submodule.restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (↑(dual R₁ (↥F₁) (dual R₁ (↥F₁) 1)) : Submodule B L))
    (Submodule.restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (↑1 : Submodule B L))
⊢ Ne.{u_4 + 1} (α := FractionalIdeal.{u_2, u_4} (R := B) B⁰ L) (dual R₁ (↥F₁) 1) 0

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 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₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
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₂))
ι : Type u_7
b : Basis.{u_7, u_3, u_4} ι K ↥F₂
hb :
  Eq.{u_4 + 1} (α := Submodule A ↥F₂) (span A (Set.range.{u_4, u_7 + 1} (ι := ι) (⇑b : (a : ι) → ↥F₂)))
    (LinearMap.range.{u_1, u_1, u_6, u_4} (M := R₂) (τ₁₂ := RingHom.id A)
      (↑(IsScalarTower.toAlgHom A R₂ ↥F₂) :
        [inst_56 : FunLike (R₂ →ₐ[A] ↥F₂) R₂ ↥F₂] →
          [SemilinearMapClass (R₂ →ₐ[A] ↥F₂) (RingHom.id A) R₂ ↥F₂] → R₂ →ₗ[A] ↥F₂))
h₂' : F₁ ⊔ F₂ = ⊤
this : Finite ι
h_main :
  Eq.{u_4 + 1} (α := Submodule R₁ L)
    (Submodule.restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (↑(dual R₁ (↥F₁) (dual R₁ (↥F₁) 1)) : Submodule B L))
    (Submodule.restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (↑1 : Submodule B L))
⊢ Eq (α := (a : ι) → L) (⇑(h₁.basisOfBasisRight h₂ b).traceDual : (a : ι) → L)
    (Function.comp (β := ↥F₂) (⇑(algebraMap (↥F₂) L) : (a : ↥F₂) → L) (⇑b.traceDual : (a : ι) → ↥F₂))

Tactic:
Basis.traceDual_eq_iff.mpr fun i j ↦ ?_

Premises used: Iff.mpr, 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 : 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₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
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₂))
ι : Type u_7
b : Basis.{u_7, u_3, u_4} ι K ↥F₂
hb :
  Eq.{u_4 + 1} (α := Submodule A ↥F₂) (span A (Set.range.{u_4, u_7 + 1} (ι := ι) (⇑b : (a : ι) → ↥F₂)))
    (LinearMap.range.{u_1, u_1, u_6, u_4} (M := R₂) (τ₁₂ := RingHom.id A)
      (↑(IsScalarTower.toAlgHom A R₂ ↥F₂) :
        [inst_56 : FunLike (R₂ →ₐ[A] ↥F₂) R₂ ↥F₂] →
          [SemilinearMapClass (R₂ →ₐ[A] ↥F₂) (RingHom.id A) R₂ ↥F₂] → R₂ →ₗ[A] ↥F₂))
h₂' : F₁ ⊔ F₂ = ⊤
this : Finite ι
h_main :
  Eq.{u_4 + 1} (α := Submodule R₁ L)
    (Submodule.restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (↑(dual R₁ (↥F₁) (dual R₁ (↥F₁) 1)) : Submodule B L))
    (Submodule.restrictScalars.{u_5, u_2, u_4} R₁ (R := B) (↑1 : Submodule B L))
x : ↥F₂
⊢ Membership.mem (γ := Submodule A ↥F₂) (Submodule.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_56 : FunLike (R₂ →ₐ[A] ↥F₂) R₂ ↥F₂] →
            [SemilinearMapClass (R₂ →ₐ[A] ↥F₂) (RingHom.id A) R₂ ↥F₂] → R₂ →ₗ[A] ↥F₂))
      x

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 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
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
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₂))
ι : Type u_7
b : Basis ι A R₂
this : Free A R₂
v : (i : ι) → B := fun (i : ι) ↦ (algebraMap R₂ B : (a : R₂) → B) ((b : (a : ι) → R₂) i : R₂)
b₂ : Basis.{u_7, u_3, u_4} ι K ↥F₂ := localizationLocalization.{u_1, u_3, u_6, u_4, u_7} (R := A) K A⁰ (A := R₂) (↥F₂) b
rw :
  LinearIndependent.{u_7, u_4, u_4} ↥F₁ (M := L) fun (x : ι) ↦
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R₁ B L) : B →ₗ[R₁] L) : (a : B) → L) (v x)
⊢ LinearIndependent R₁ v

Tactic:
rw [← LinearMap.linearIndependent_iff (IsScalarTower.toAlgHom R₁ B L).toLinearMap
      (LinearMap.ker_eq_bot.mpr <| FaithfulSMul.algebraMap_injective _ _),
      LinearIndependent.iff_fractionRing R₁ F₁, Function.comp_def]

Premises used: Iff.mpr, AlgHom.toLinearMap, LinearMap.ker_eq_bot, IsScalarTower.toAlgHom, Membership.mem, Subtype, LinearMap.linearIndependent_iff, LinearIndependent.iff_fractionRing, Function.comp_def, FaithfulSMul.algebraMap_injective
-- 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
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
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₂))
ι : Type u_7
b : Basis ι A R₂
this : Free A R₂
v : (i : ι) → B := fun (i : ι) ↦ (algebraMap R₂ B : (a : R₂) → B) ((b : (a : ι) → R₂) i : R₂)
b₂ : Basis.{u_7, u_3, u_4} ι K ↥F₂ := localizationLocalization.{u_1, u_3, u_6, u_4, u_7} (R := A) K A⁰ (A := R₂) (↥F₂) b
simp_rw :
  LinearIndependent.{u_7, u_4, u_4} ↥F₁ (M := L) fun (x : ι) ↦
    (algebraMap (↥F₂) L : (a : ↥F₂) → L)
      ((localizationLocalization.{u_1, u_3, u_6, u_4, u_7} (R := A) K A⁰ (A := R₂) (↥F₂) b : (a : ι) → ↥F₂) x : ↥F₂)
⊢ LinearIndependent.{u_7, u_4, u_4} ↥F₁ (M := L) fun (x : ι) ↦
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R₁ B L) : B →ₗ[R₁] L) : (a : B) → L) (v x)

Tactic:
simp_rw [AlgHom.toLinearMap_apply, IsScalarTower.coe_toAlgHom', v,
      ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R₂ F₂ L,
      ← b.localizationLocalization_apply K A⁰ F₂]

Premises used: IsScalarTower.coe_toAlgHom', Module.Basis.localizationLocalization_apply, Membership.mem, nonZeroDivisors, AlgHom.toLinearMap_apply, Subtype, 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 : 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
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
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₂))
ι : Type u_7
b : Basis ι A R₂
this : Free A R₂
v : (i : ι) → B := fun (i : ι) ↦ (algebraMap R₂ B : (a : R₂) → B) ((b : (a : ι) → R₂) i : R₂)
b₂ : Basis.{u_7, u_3, u_4} ι K ↥F₂ := localizationLocalization.{u_1, u_3, u_6, u_4, u_7} (R := A) K A⁰ (A := R₂) (↥F₂) b
⊢ LinearIndependent.{u_7, u_4, u_4} ↥F₁ (M := L) fun (x : ι) ↦
    (algebraMap (↥F₂) L : (a : ↥F₂) → L)
      ((localizationLocalization.{u_1, u_3, u_6, u_4, u_7} (R := A) K A⁰ (A := R₂) (↥F₂) b : (a : ι) → ↥F₂) x : ↥F₂)

Tactic:
h₁.linearIndependent_right b₂.linearIndependent

Premises used: Module.Basis.linearIndependent, IntermediateField.LinearDisjoint.linearIndependent_right
-- 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
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
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₂))
ι : Type u_7
b : Basis ι A R₂
this : Free A R₂
v : (i : ι) → B := fun (i : ι) ↦ (algebraMap R₂ B : (a : R₂) → B) ((b : (a : ι) → R₂) i : R₂)
b₂ : Basis.{u_7, u_3, u_4} ι K ↥F₂ := localizationLocalization.{u_1, u_3, u_6, u_4, u_7} (R := A) K A⁰ (A := R₂) (↥F₂) b
⊢ LinearIndependent.{u_7, u_4, u_4} ↥F₁ (M := L) fun (x : ι) ↦
    (algebraMap (↥F₂) L : (a : ↥F₂) → L)
      ((localizationLocalization.{u_1, u_3, u_6, u_4, u_7} (R := A) K A⁰ (A := R₂) (↥F₂) b : (a : ι) → ↥F₂) x : ↥F₂)

Tactic:
exact h₁.linearIndependent_right b₂.linearIndependent

Premises used: Module.Basis.linearIndependent, IntermediateField.LinearDisjoint.linearIndependent_right