awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : Decidable (IsField A)
⊢ Eq.{u + 1} (α := Submodule B L) ⊤ᵛ
    (if LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1 then ⊤ else ⊥)

Tactic:
traceDual_top'

Premises used: Submodule.traceDual_top'
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : Decidable (IsField A)
h : IsField A ↔ LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1
⊢ Eq.{u + 1} (α := Submodule B L) ⊤ᵛ (if IsField A then ⊤ else ⊥)

Tactic:
convert! traceDual_top'

Premises used: Submodule.traceDual_top'
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : Decidable (IsField A)
h :
  LE.le.{u_2} (α := Subring K) ⊤ (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K)) ↔
    LE.le.{u_2} (α := Submodule A K) (restrictScalars A (R := K) ⊤) 1
⊢ IsField A ↔ LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1

Tactic:
rw [← IsFractionRing.surjective_iff_isField (R := A) (K := K),
    LinearMap.range_eq_top.mpr (Algebra.trace_surjective K L),
    ← RingHom.range_eq_top, _root_.eq_top_iff]

Premises used: Iff.mpr, eq_top_iff, IsFractionRing.surjective_iff_isField, LinearMap.range_eq_top, Algebra.trace_surjective, RingHom.range_eq_top
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : Decidable (IsField A)
⊢ LE.le.{u_2} (α := Subring K) ⊤ (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K)) ↔
    LE.le.{u_2} (α := Submodule A K) (restrictScalars A (R := K) ⊤) 1

Tactic:
simp [SetLike.le_def]

Premises used: SetLike.le_def
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
rw :
  Eq (α := Submodule B L)
    (comap (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B)
      (traceDual A (FractionRing A) I))
    (comap (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B) I)ᵛ
⊢ Eq (α := Submodule B L)
    (Submodule.map (↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L)
      (traceDual A (FractionRing A) I))
    (Submodule.map (↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L) I)ᵛ

Tactic:
rw [Submodule.map_equiv_eq_comap_symm, Submodule.map_equiv_eq_comap_symm]

Premises used: Submodule.map_equiv_eq_comap_symm
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
h :
  ∀ (x : L),
    Membership.mem (γ := Submodule B L)
        (comap (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B)
          (traceDual A (FractionRing A) I))
        x ↔
      Membership.mem (γ := Submodule B L)
        (comap (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B)
            I)ᵛ
        x
⊢ Eq (α := Submodule B L)
    (comap (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B)
      (traceDual A (FractionRing A) I))
    (comap (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B) I)ᵛ

Tactic:
ext x
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
h :
  ∀ (a : FractionRing B),
    Membership.mem (γ := Submodule A (FractionRing B)) (Submodule.restrictScalars A I) a →
        Membership.mem.{u_1, u_1} (α := FractionRing A) (γ := Submodule A (FractionRing A)) 1
          ((((traceForm (FractionRing A) (FractionRing B) :
                      (a : FractionRing B) → FractionRing B →ₗ[FractionRing A] FractionRing A)
                    ((((↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) :
                            L →ₗ[B] FractionRing B) :
                          L →ₗ[B] FractionRing B) :
                        (a : L) → FractionRing B)
                      x) :
                  LinearMap.{u_1, u_1, u_3, u_1} (R := FractionRing A) (RingHom.id (FractionRing A)) (FractionRing B)
                    (FractionRing A)) :
                (a : FractionRing B) → FractionRing A)
              a :
            FractionRing A) ↔
      Membership.mem (α := L) (γ := Submodule A L)
          (Submodule.restrictScalars A
            (comap
              (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B) I))
          ((AlgEquiv.toEquiv (FractionRing.algEquiv B L) : (a : FractionRing B) → L) a : L) →
        Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1
          ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K)
              ((AlgEquiv.toEquiv (FractionRing.algEquiv B L) : (a : FractionRing B) → L) a : L) :
            K)
⊢ Membership.mem (α := FractionRing B)
      (toAddSubmonoid
        (LinearMap.BilinForm.dualSubmodule (S := FractionRing A) (traceForm (FractionRing A) (FractionRing B))
          (Submodule.restrictScalars A I)))
      ((((↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B) :
              L →ₗ[B] FractionRing B) :
            (a : L) → FractionRing B)
          x :
        FractionRing B) ↔
    Membership.mem (γ := AddSubmonoid L)
      (toAddSubmonoid.{u_1, u} (R := A)
        (LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (R := A) (S := K) (M := L) (traceForm K L)
          (Submodule.restrictScalars A
            (comap
              (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B)
              I))))
      x

Tactic:
apply (FractionRing.algEquiv B L).forall_congr

Premises used: FractionRing.algEquiv, Equiv.forall_congr, AlgEquiv.toEquiv
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
⊢ ∀ (a : FractionRing B),
    (a ∈ I →
        ∃ (y : A),
          Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y : FractionRing A)
            ((Algebra.trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
                (HMul.hMul (α := FractionRing B)
                  (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B) x :
                    FractionRing B)
                  a) :
              FractionRing A)) ↔
      a ∈ I →
        ∃ (y : A),
          Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y : K)
            ((Algebra.trace K L : (a : L) → K)
                (HMul.hMul (β := L) x ((FractionRing.algEquiv B L : (a : FractionRing B) → L) a : L)) :
              K)

Tactic:
fun {y} ↦ (forall_congr' fun hy ↦ ?_)

Premises used: Set.Mem, forall_congr'
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
h :
  ∀ {y : FractionRing B} (hy : y ∈ I),
    (∃ (y_1 : A),
        Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y_1 : FractionRing A)
          ((Algebra.trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
              (HMul.hMul (α := FractionRing B)
                (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B) x :
                  FractionRing B)
                y) :
            FractionRing A)) ↔
      ∃ (y_1 : A),
        Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y_1 : K)
          ((Algebra.trace K L : (a : L) → K)
              (HMul.hMul (β := L) x ((FractionRing.algEquiv B L : (a : FractionRing B) → L) y : L)) :
            K)
⊢ ∀ (a : FractionRing B),
    (a ∈ I →
        ∃ (y : A),
          Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y : FractionRing A)
            ((Algebra.trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
                (HMul.hMul (α := FractionRing B)
                  (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B) x :
                    FractionRing B)
                  a) :
              FractionRing A)) ↔
      a ∈ I →
        ∃ (y : A),
          Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y : K)
            ((Algebra.trace K L : (a : L) → K)
                (HMul.hMul (β := L) x ((FractionRing.algEquiv B L : (a : FractionRing B) → L) a : L)) :
              K)

Tactic:
refine fun {y} ↦ (forall_congr' fun hy ↦ ?_)

Premises used: forall_congr'
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
h :
  (∃ (y_1 : A),
      Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y_1 : FractionRing A)
        (((RingEquiv.symm (AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) :
                RingEquiv.{u_2, u_1} K (FractionRing A)) :
              (a : K) → FractionRing A)
            ((Algebra.trace K L : (a : L) → K)
              ((AlgEquiv.toRingEquiv (FractionRing.algEquiv B L) : (a : FractionRing B) → L)
                  (HMul.hMul (α := FractionRing B)
                    (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B)
                        x :
                      FractionRing B)
                    y) :
                L)) :
          FractionRing A)) ↔
    ∃ (y_1 : A),
      Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y_1 : K)
        ((Algebra.trace K L : (a : L) → K)
            (HMul.hMul (β := L) x ((FractionRing.algEquiv B L : (a : FractionRing B) → L) y : L)) :
          K)
h₁ :
  Eq (α := RingHom.{u_1, u} (FractionRing A) L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
      (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
      (algebraMap (FractionRing A) (FractionRing B)))
⊢ (∃ (y_1 : A),
      Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y_1 : FractionRing A)
        ((Algebra.trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
            (HMul.hMul (α := FractionRing B)
              (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B) x :
                FractionRing B)
              y) :
          FractionRing A)) ↔
    ∃ (y_1 : A),
      Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y_1 : K)
        ((Algebra.trace K L : (a : L) → K)
            (HMul.hMul (β := L) x ((FractionRing.algEquiv B L : (a : FractionRing B) → L) y : L)) :
          K)

Tactic:
rw [Algebra.trace_eq_of_equiv_equiv (FractionRing.algEquiv A K).toRingEquiv
    (FractionRing.algEquiv B L).toRingEquiv]

Premises used: FractionRing.algEquiv, AlgEquiv.toRingEquiv, Algebra.trace_eq_of_equiv_equiv
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
h :
  ∀ (x : FractionRing A),
    Eq.{u + 1} (α := L)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
              (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K) :
            (a : FractionRing A) → L)
          x :
        L)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
              (algebraMap (FractionRing A) (FractionRing B)) :
            (a : FractionRing A) → L)
          x :
        L)
⊢ Eq (α := RingHom.{u_1, u} (FractionRing A) L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
      (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
      (algebraMap (FractionRing A) (FractionRing B)))

Tactic:
ext
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
x_1 : FractionRing A
⊢ Eq.{u + 1} (α := L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
            (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K) :
          (a : FractionRing A) → L)
        x_1 :
      L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
            (algebraMap (FractionRing A) (FractionRing B)) :
          (a : FractionRing A) → L)
        x_1 :
      L)

Tactic:
IsFractionRing.algEquiv_commutes (FractionRing.algEquiv A K) (FractionRing.algEquiv B L) _

Premises used: FractionRing.algEquiv, IsFractionRing.algEquiv_commutes
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
x_1 : FractionRing A
⊢ Eq.{u + 1} (α := L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
            (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K) :
          (a : FractionRing A) → L)
        x_1 :
      L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
            (algebraMap (FractionRing A) (FractionRing B)) :
          (a : FractionRing A) → L)
        x_1 :
      L)

Tactic:
exact IsFractionRing.algEquiv_commutes (FractionRing.algEquiv A K) (FractionRing.algEquiv B L) _

Premises used: FractionRing.algEquiv, IsFractionRing.algEquiv_commutes
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
⊢ (∃ (y_1 : A),
      Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y_1 : FractionRing A)
        (((RingEquiv.symm (AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) :
                RingEquiv.{u_2, u_1} K (FractionRing A)) :
              (a : K) → FractionRing A)
            ((Algebra.trace K L : (a : L) → K)
              ((AlgEquiv.toRingEquiv (FractionRing.algEquiv B L) : (a : FractionRing B) → L)
                  (HMul.hMul (α := FractionRing B)
                    (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B)
                        x :
                      FractionRing B)
                    y) :
                L)) :
          FractionRing A)) ↔
    ∃ (y_1 : A),
      Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y_1 : K)
        ((Algebra.trace K L : (a : L) → K)
            (HMul.hMul (β := L) x ((FractionRing.algEquiv B L : (a : FractionRing B) → L) y : L)) :
          K)

Tactic:
simp only [map_mul, AlgEquiv.coe_ringEquiv,
    AlgEquiv.apply_symm_apply, ← AlgEquiv.symm_toRingEquiv, AlgEquiv.algebraMap_eq_apply]

Premises used: AlgEquiv.apply_symm_apply, AlgEquiv.coe_ringEquiv, map_mul, AlgEquiv.algebraMap_eq_apply, AlgEquiv.symm_toRingEquiv
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
I : Submodule B L
x : L
⊢ x ∈ Iᵛ ↔
    ∀ a ∈ I,
      IsIntegral.{u_1, u_2} A (A := K) ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) a : K)

Tactic:
forall₂_congr fun _ _ ↦ mem_one.trans IsIntegrallyClosed.isIntegral_iff.symm

Premises used: IsIntegrallyClosed.isIntegral_iff, Set.Mem, setOf, forall₂_congr, Submodule.mem_one, Iff.trans, Iff.symm
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
rw :
  LE.le (α := Submodule A K)
    (map
      ((↑A :
          {S : Type u_2} →
            {M : Type u} →
              {M₂ : Type u_2} →
                [inst : Semiring A] →
                  [inst_15 : Semiring S] →
                    [inst_16 : AddCommMonoid M] →
                      [inst_17 : AddCommMonoid M₂] →
                        [inst_18 : Module A M] →
                          [inst_19 : Module A M₂] →
                            [inst_20 : Module S M] →
                              [inst_21 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
        (Algebra.trace K L))
      (restrictScalars A (LinearMap.range (Algebra.linearMap B L))))
    1
⊢ LE.le.{u} (α := Submodule B L) 1 1ᵛ

Tactic:
rw [le_traceDual_iff_map_le_one, mul_one, one_eq_range]

Premises used: mul_one, Submodule.one_eq_range, Submodule.le_traceDual_iff_map_le_one