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 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
inst_19 : IsFractionRing B L
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
rw :
  (↑I⁻¹ : Submodule B L) ≤ traceDual A K 1 ↔
    LE.le (α := Submodule A K)
      (Submodule.map
        ((↑A :
            {S : Type u_2} →
              {M : Type u} →
                {M₂ : Type u_2} →
                  [inst : Semiring A] →
                    [inst_20 : Semiring S] →
                      [inst_21 : AddCommMonoid M] →
                        [inst_22 : AddCommMonoid M₂] →
                          [inst_23 : Module A M] →
                            [inst_24 : Module A M₂] →
                              [inst_25 : Module S M] →
                                [inst_26 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
          (Algebra.trace K L))
        (Submodule.restrictScalars A (↑I⁻¹ : Submodule B L)))
      1
⊢ (↑(differentIdeal A B) : FractionalIdeal B⁰ L) ≤ I ↔
    LE.le (α := Submodule A K)
      (Submodule.map
        ((↑A :
            {S : Type u_2} →
              {M : Type u} →
                {M₂ : Type u_2} →
                  [inst : Semiring A] →
                    [inst_20 : Semiring S] →
                      [inst_21 : AddCommMonoid M] →
                        [inst_22 : AddCommMonoid M₂] →
                          [inst_23 : Module A M] →
                            [inst_24 : Module A M₂] →
                              [inst_25 : Module S M] →
                                [inst_26 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
          (Algebra.trace K L))
        (Submodule.restrictScalars A (↑I⁻¹ : Submodule B L)))
      1

Tactic:
rw [coeIdeal_differentIdeal A K L B, FractionalIdeal.inv_le_comm (by simp) hI,
    ← FractionalIdeal.coe_le_coe, FractionalIdeal.coe_dual_one]

Premises used: FractionalIdeal.coe_le_coe, FractionalIdeal.coe_dual_one, coeIdeal_differentIdeal, FractionalIdeal.inv_le_comm
-- 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 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
inst_19 : IsFractionRing B L
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
⊢ (↑I⁻¹ : Submodule B L) ≤ traceDual A K 1 ↔
    LE.le (α := Submodule A K)
      (Submodule.map
        ((↑A :
            {S : Type u_2} →
              {M : Type u} →
                {M₂ : Type u_2} →
                  [inst : Semiring A] →
                    [inst_20 : Semiring S] →
                      [inst_21 : AddCommMonoid M] →
                        [inst_22 : AddCommMonoid M₂] →
                          [inst_23 : Module A M] →
                            [inst_24 : Module A M₂] →
                              [inst_25 : Module S M] →
                                [inst_26 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
          (Algebra.trace K L))
        (Submodule.restrictScalars A (↑I⁻¹ : Submodule B L)))
      1

Tactic:
le_traceDual_iff_map_le_one.trans ?_

Premises used: Set.Mem, Iff.trans, Submodule.le_traceDual_iff_map_le_one
-- 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 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
inst_19 : IsFractionRing B L
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
refine :
  LE.le (α := Submodule A K)
      (Submodule.map
        ((↑A :
            {S : Type u_2} →
              {M : Type u} →
                {M₂ : Type u_2} →
                  [inst : Semiring A] →
                    [inst_20 : Semiring S] →
                      [inst_21 : AddCommMonoid M] →
                        [inst_22 : AddCommMonoid M₂] →
                          [inst_23 : Module A M] →
                            [inst_24 : Module A M₂] →
                              [inst_25 : Module S M] →
                                [inst_26 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
          (Algebra.trace K L))
        (Submodule.restrictScalars A ((↑I⁻¹ : Submodule B L) * 1)))
      1 ↔
    LE.le (α := Submodule A K)
      (Submodule.map
        ((↑A :
            {S : Type u_2} →
              {M : Type u} →
                {M₂ : Type u_2} →
                  [inst : Semiring A] →
                    [inst_20 : Semiring S] →
                      [inst_21 : AddCommMonoid M] →
                        [inst_22 : AddCommMonoid M₂] →
                          [inst_23 : Module A M] →
                            [inst_24 : Module A M₂] →
                              [inst_25 : Module S M] →
                                [inst_26 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
          (Algebra.trace K L))
        (Submodule.restrictScalars A (↑I⁻¹ : Submodule B L)))
      1
⊢ (↑I⁻¹ : Submodule B L) ≤ traceDual A K 1 ↔
    LE.le (α := Submodule A K)
      (Submodule.map
        ((↑A :
            {S : Type u_2} →
              {M : Type u} →
                {M₂ : Type u_2} →
                  [inst : Semiring A] →
                    [inst_20 : Semiring S] →
                      [inst_21 : AddCommMonoid M] →
                        [inst_22 : AddCommMonoid M₂] →
                          [inst_23 : Module A M] →
                            [inst_24 : Module A M₂] →
                              [inst_25 : Module S M] →
                                [inst_26 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
          (Algebra.trace K L))
        (Submodule.restrictScalars A (↑I⁻¹ : Submodule B L)))
      1

Tactic:
refine le_traceDual_iff_map_le_one.trans ?_

Premises used: Iff.trans, Submodule.le_traceDual_iff_map_le_one
-- 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 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
inst_19 : IsFractionRing B L
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
⊢ LE.le (α := Submodule A K)
      (Submodule.map
        ((↑A :
            {S : Type u_2} →
              {M : Type u} →
                {M₂ : Type u_2} →
                  [inst : Semiring A] →
                    [inst_20 : Semiring S] →
                      [inst_21 : AddCommMonoid M] →
                        [inst_22 : AddCommMonoid M₂] →
                          [inst_23 : Module A M] →
                            [inst_24 : Module A M₂] →
                              [inst_25 : Module S M] →
                                [inst_26 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
          (Algebra.trace K L))
        (Submodule.restrictScalars A ((↑I⁻¹ : Submodule B L) * 1)))
      1 ↔
    LE.le (α := Submodule A K)
      (Submodule.map
        ((↑A :
            {S : Type u_2} →
              {M : Type u} →
                {M₂ : Type u_2} →
                  [inst : Semiring A] →
                    [inst_20 : Semiring S] →
                      [inst_21 : AddCommMonoid M] →
                        [inst_22 : AddCommMonoid M₂] →
                          [inst_23 : Module A M] →
                            [inst_24 : Module A M₂] →
                              [inst_25 : Module S M] →
                                [inst_26 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
          (Algebra.trace K L))
        (Submodule.restrictScalars A (↑I⁻¹ : Submodule B L)))
      1

Tactic:
simp
-- 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 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
inst_19 : IsFractionRing B L
I : Ideal B
hI : I ≠ ⊥
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑I : FractionalIdeal B⁰ L) 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
C : Type u_3
inst_7 : IsDomain B
inst_8 : CommRing C
inst_9 : Algebra B C
inst_10 : Algebra A C
inst_11 : IsDedekindDomain C
inst_12 : Module.Finite A B
inst_13 : Module.Finite A C
inst_14 : Module.Finite B C
inst_15 : IsTorsionFree A C
inst_16 : IsTorsionFree B C
inst_17 : IsScalarTower A B C
inst_18 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing C)
⊢ Algebra.IsSeparable.{u_4, u_3} (FractionRing B) (FractionRing C)

Tactic:
have : Algebra.IsSeparable (FractionRing B) (FractionRing C) :=
    isSeparable_tower_top_of_isSeparable (FractionRing A) _ _
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
C : Type u_3
inst_7 : IsDomain B
inst_8 : CommRing C
inst_9 : Algebra B C
inst_10 : Algebra A C
inst_11 : IsDedekindDomain C
inst_12 : Module.Finite A B
inst_13 : Module.Finite A C
inst_14 : Module.Finite B C
inst_15 : IsTorsionFree A C
inst_16 : IsTorsionFree B C
inst_17 : IsScalarTower A B C
inst_18 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing C)
this : Algebra.IsSeparable.{u_4, u_3} (FractionRing B) (FractionRing C)
⊢ Algebra.IsSeparable.{u_1, u_4} (FractionRing A) (FractionRing B)

Tactic:
have : Algebra.IsSeparable (FractionRing A) (FractionRing B) :=
    isSeparable_tower_bot_of_isSeparable _ _ (FractionRing C)
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
C : Type u_3
inst_7 : IsDomain B
inst_8 : CommRing C
inst_9 : Algebra B C
inst_10 : Algebra A C
inst_11 : IsDedekindDomain C
inst_12 : Module.Finite A B
inst_13 : Module.Finite A C
inst_14 : Module.Finite B C
inst_15 : IsTorsionFree A C
inst_16 : IsTorsionFree B C
inst_17 : IsScalarTower A B C
inst_18 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing C)
this_1 : Algebra.IsSeparable.{u_4, u_3} (FractionRing B) (FractionRing C)
this : Algebra.IsSeparable.{u_1, u_4} (FractionRing A) (FractionRing B)
⊢ FiniteDimensional.{u_1, u_4} (FractionRing A) (FractionRing B)

Tactic:
haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
C : Type u_3
inst_7 : IsDomain B
inst_8 : CommRing C
inst_9 : Algebra B C
inst_10 : Algebra A C
inst_11 : IsDedekindDomain C
inst_12 : Module.Finite A B
inst_13 : Module.Finite A C
inst_14 : Module.Finite B C
inst_15 : IsTorsionFree A C
inst_16 : IsTorsionFree B C
inst_17 : IsScalarTower A B C
inst_18 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing C)
this_1 : Algebra.IsSeparable.{u_4, u_3} (FractionRing B) (FractionRing C)
this_2 : Algebra.IsSeparable.{u_1, u_4} (FractionRing A) (FractionRing B)
this : FiniteDimensional.{u_1, u_4} (FractionRing A) (FractionRing B)
⊢ FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing C)

Tactic:
haveI : FiniteDimensional (FractionRing A) (FractionRing C) := .of_isLocalization A C A⁰
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
C : Type u_3
inst_7 : IsDomain B
inst_8 : CommRing C
inst_9 : Algebra B C
inst_10 : Algebra A C
inst_11 : IsDedekindDomain C
inst_12 : Module.Finite A B
inst_13 : Module.Finite A C
inst_14 : Module.Finite B C
inst_15 : IsTorsionFree A C
inst_16 : IsTorsionFree B C
inst_17 : IsScalarTower A B C
inst_18 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing C)
this_1 : Algebra.IsSeparable.{u_4, u_3} (FractionRing B) (FractionRing C)
this_2 : Algebra.IsSeparable.{u_1, u_4} (FractionRing A) (FractionRing B)
this_3 : FiniteDimensional.{u_1, u_4} (FractionRing A) (FractionRing B)
this : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing C)
⊢ FiniteDimensional.{u_4, u_3} (FractionRing B) (FractionRing C)

Tactic:
haveI : FiniteDimensional (FractionRing B) (FractionRing C) := .of_isLocalization B C B⁰
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
C : Type u_3
inst_7 : IsDomain B
inst_8 : CommRing C
inst_9 : Algebra B C
inst_10 : Algebra A C
inst_11 : IsDedekindDomain C
inst_12 : Module.Finite A B
inst_13 : Module.Finite A C
inst_14 : Module.Finite B C
inst_15 : IsTorsionFree A C
inst_16 : IsTorsionFree B C
inst_17 : IsScalarTower A B C
inst_18 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing C)
this_1 : Algebra.IsSeparable.{u_4, u_3} (FractionRing B) (FractionRing C)
this_2 : Algebra.IsSeparable.{u_1, u_4} (FractionRing A) (FractionRing B)
this_3 : FiniteDimensional.{u_1, u_4} (FractionRing A) (FractionRing B)
this_4 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing C)
this : FiniteDimensional.{u_4, u_3} (FractionRing B) (FractionRing C)
rw :
  (dual A (FractionRing A) 1)⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := C) C⁰ (FractionRing C)) (dual B (FractionRing B) 1)⁻¹
      (↑(Ideal.map (F := B →+* C) (algebraMap B C) (differentIdeal A B)) : FractionalIdeal C⁰ (FractionRing C))
⊢ differentIdeal A C =
    HMul.hMul (α := Ideal C) (differentIdeal B C) (Ideal.map (F := B →+* C) (algebraMap B C) (differentIdeal A B))

Tactic:
rw [← coeIdeal_inj (K := FractionRing C), coeIdeal_mul, coeIdeal_differentIdeal A
    (FractionRing A), coeIdeal_differentIdeal B (FractionRing B)]

Premises used: FractionalIdeal.coeIdeal_inj, FractionRing, coeIdeal_differentIdeal, FractionalIdeal.coeIdeal_mul
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
C : Type u_3
inst_7 : IsDomain B
inst_8 : CommRing C
inst_9 : Algebra B C
inst_10 : Algebra A C
inst_11 : IsDedekindDomain C
inst_12 : Module.Finite A B
inst_13 : Module.Finite A C
inst_14 : Module.Finite B C
inst_15 : IsTorsionFree A C
inst_16 : IsTorsionFree B C
inst_17 : IsScalarTower A B C
inst_18 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing C)
this_1 : Algebra.IsSeparable.{u_4, u_3} (FractionRing B) (FractionRing C)
this_2 : Algebra.IsSeparable.{u_1, u_4} (FractionRing A) (FractionRing B)
this_3 : FiniteDimensional.{u_1, u_4} (FractionRing A) (FractionRing B)
this_4 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing C)
this : FiniteDimensional.{u_4, u_3} (FractionRing B) (FractionRing C)
rw :
  dual A (FractionRing A) 1 =
    HMul.hMul (α := FractionalIdeal (R := C) C⁰ (FractionRing C)) (β := FractionalIdeal (R := C) C⁰ (FractionRing C))
      (dual B (FractionRing B) 1)
      ((extendedHom (FractionRing C) C :
            (a : FractionalIdeal B⁰ (FractionRing B)) → FractionalIdeal C⁰ (FractionRing C))
          (dual A (FractionRing A) 1) :
        FractionalIdeal (R := C) C⁰ (FractionRing C))
⊢ (dual A (FractionRing A) 1)⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := C) C⁰ (FractionRing C)) (dual B (FractionRing B) 1)⁻¹
      (↑(Ideal.map (F := B →+* C) (algebraMap B C) (differentIdeal A B)) : FractionalIdeal C⁰ (FractionRing C))

Tactic:
rw [← extendedHom_coeIdeal_eq_map (K := FractionRing B), coeIdeal_differentIdeal A
    (FractionRing A), map_inv₀, ← mul_inv, ← inv_eq_iff_eq_inv, inv_inv]

Premises used: mul_inv, FractionRing, map_inv₀, coeIdeal_differentIdeal, FractionalIdeal.extendedHom_coeIdeal_eq_map, inv_inv, inv_eq_iff_eq_inv
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
C : Type u_3
inst_7 : IsDomain B
inst_8 : CommRing C
inst_9 : Algebra B C
inst_10 : Algebra A C
inst_11 : IsDedekindDomain C
inst_12 : Module.Finite A B
inst_13 : Module.Finite A C
inst_14 : Module.Finite B C
inst_15 : IsTorsionFree A C
inst_16 : IsTorsionFree B C
inst_17 : IsScalarTower A B C
inst_18 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing C)
this_1 : Algebra.IsSeparable.{u_4, u_3} (FractionRing B) (FractionRing C)
this_2 : Algebra.IsSeparable.{u_1, u_4} (FractionRing A) (FractionRing B)
this_3 : FiniteDimensional.{u_1, u_4} (FractionRing A) (FractionRing B)
this_4 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing C)
this : FiniteDimensional.{u_4, u_3} (FractionRing B) (FractionRing C)
⊢ dual A (FractionRing A) 1 =
    HMul.hMul (α := FractionalIdeal (R := C) C⁰ (FractionRing C)) (β := FractionalIdeal (R := C) C⁰ (FractionRing C))
      (dual B (FractionRing B) 1)
      ((extendedHom (FractionRing C) C :
            (a : FractionalIdeal B⁰ (FractionRing B)) → FractionalIdeal C⁰ (FractionRing C))
          (dual A (FractionRing A) 1) :
        FractionalIdeal (R := C) C⁰ (FractionRing C))

Tactic:
dual_eq_dual_mul_dual A (FractionRing A) (FractionRing B) B C (FractionRing C)

Premises used: FractionalIdeal.dual_eq_dual_mul_dual, FractionRing
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
C : Type u_3
inst_7 : IsDomain B
inst_8 : CommRing C
inst_9 : Algebra B C
inst_10 : Algebra A C
inst_11 : IsDedekindDomain C
inst_12 : Module.Finite A B
inst_13 : Module.Finite A C
inst_14 : Module.Finite B C
inst_15 : IsTorsionFree A C
inst_16 : IsTorsionFree B C
inst_17 : IsScalarTower A B C
inst_18 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing C)
this_1 : Algebra.IsSeparable.{u_4, u_3} (FractionRing B) (FractionRing C)
this_2 : Algebra.IsSeparable.{u_1, u_4} (FractionRing A) (FractionRing B)
this_3 : FiniteDimensional.{u_1, u_4} (FractionRing A) (FractionRing B)
this_4 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing C)
this : FiniteDimensional.{u_4, u_3} (FractionRing B) (FractionRing C)
⊢ dual A (FractionRing A) 1 =
    HMul.hMul (α := FractionalIdeal (R := C) C⁰ (FractionRing C)) (β := FractionalIdeal (R := C) C⁰ (FractionRing C))
      (dual B (FractionRing B) 1)
      ((extendedHom (FractionRing C) C :
            (a : FractionalIdeal B⁰ (FractionRing B)) → FractionalIdeal C⁰ (FractionRing C))
          (dual A (FractionRing A) 1) :
        FractionalIdeal (R := C) C⁰ (FractionRing C))

Tactic:
exact dual_eq_dual_mul_dual A (FractionRing A) (FractionRing B) B C (FractionRing C)

Premises used: FractionalIdeal.dual_eq_dual_mul_dual, FractionRing
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
⊢ IsIntegral K x

Tactic:
have hKx : IsIntegral K x := Algebra.IsIntegral.isIntegral x
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
⊢ pb.gen = x

Tactic:
simp [pb]
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
⊢ pb.gen = x

Tactic:
have pbgen : pb.gen = x := by simp [pb]
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
⊢ LinearMap.BilinForm.Nondegenerate (traceForm K L)

Tactic:
have hnondeg : (traceForm K L).Nondegenerate := traceForm_nondegenerate K L