awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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
this_1 :
  Eq (α := B →ₗ[B] L)
    ((↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L) ∘ₗ
      Algebra.linearMap B (FractionRing B))
    (Algebra.linearMap B L)
H :
  Eq (α := RingHom.{u_2, u_3} K (FractionRing B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing A) (FractionRing B))
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv A K))) : K →+* FractionRing A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv B L))) : L →+* FractionRing B) (algebraMap K L))
this_2 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
this : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
⊢ Submodule.map
      ((↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L) ∘ₗ
        Algebra.linearMap B (FractionRing B))
      (differentIdeal A B) =
    HDiv.hDiv (α := Submodule B L) 1 (traceDual A K 1)
have this₁ : Algebra.IsIntegral A B
Tactic: have : Algebra.IsIntegral A B := IsIntegralClosure.isIntegral_algebra _ L
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
this_1 :
  Eq (α := B →ₗ[B] L)
    ((↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L) ∘ₗ
      Algebra.linearMap B (FractionRing B))
    (Algebra.linearMap B L)
H :
  Eq (α := RingHom.{u_2, u_3} K (FractionRing B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing A) (FractionRing B))
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv A K))) : K →+* FractionRing A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv B L))) : L →+* FractionRing B) (algebraMap K L))
this_2 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
this_3 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
this : Algebra.IsIntegral A B
⊢ Submodule.map
      ((↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L) ∘ₗ
        Algebra.linearMap B (FractionRing B))
      (differentIdeal A B) =
    HDiv.hDiv (α := Submodule B L) 1 (traceDual A K 1)
have simp : Submodule.map (AlgEquiv.toLinearMap (FractionRing.algEquiv B L))
    (Submodule.map (Algebra.linearMap B (FractionRing B)) (differentIdeal A B)) =
  HDiv.hDiv (α := Submodule B L) 1 (traceDual A K 1)
Tactic: simp only [AlgEquiv.toLinearEquiv_toLinearMap, Submodule.map_comp]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
this_1 :
  Eq (α := B →ₗ[B] L)
    ((↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L) ∘ₗ
      Algebra.linearMap B (FractionRing B))
    (Algebra.linearMap B L)
H :
  Eq (α := RingHom.{u_2, u_3} K (FractionRing B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing A) (FractionRing B))
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv A K))) : K →+* FractionRing A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv B L))) : L →+* FractionRing B) (algebraMap K L))
this_2 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
this_3 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
this : Algebra.IsIntegral A B
⊢ Submodule.map (AlgEquiv.toLinearMap (FractionRing.algEquiv B L))
      (Submodule.map (Algebra.linearMap B (FractionRing B)) (differentIdeal A B)) =
    HDiv.hDiv (α := Submodule B L) 1 (traceDual A K 1)
have rw : HDiv.hDiv (α := Submodule B L) 1
    (Submodule.map (AlgHom.toLinearMap (↑(FractionRing.algEquiv B L) : FractionRing B →ₐ[B] L))
      (traceDual A (FractionRing A) 1)) =
  HDiv.hDiv (α := Submodule B L) 1 (traceDual A K 1)
Tactic: rw [← coeSubmodule, coeSubmodule_differentIdeal_fractionRing _ _,
    Submodule.map_div, AlgEquiv.toLinearMap, ← AlgEquiv.toAlgHom_toLinearMap, Submodule.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
this_1 :
  Eq (α := B →ₗ[B] L)
    ((↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L) ∘ₗ
      Algebra.linearMap B (FractionRing B))
    (Algebra.linearMap B L)
H :
  Eq (α := RingHom.{u_2, u_3} K (FractionRing B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing A) (FractionRing B))
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv A K))) : K →+* FractionRing A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv B L))) : L →+* FractionRing B) (algebraMap K L))
this_2 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
this_3 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
this : Algebra.IsIntegral A B
⊢ HDiv.hDiv (α := Submodule B L) 1
      (Submodule.map (AlgHom.toLinearMap (↑(FractionRing.algEquiv B L) : FractionRing B →ₐ[B] L))
        (traceDual A (FractionRing A) 1)) =
    HDiv.hDiv (α := Submodule B L) 1 (traceDual A K 1)
have e_a : Eq (α := Submodule B L)
  (Submodule.map (AlgHom.toLinearMap (↑(FractionRing.algEquiv B L) : FractionRing B →ₐ[B] L))
    (traceDual A (FractionRing A) 1))
  (traceDual A K 1)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
this_1 :
  Eq (α := B →ₗ[B] L)
    ((↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L) ∘ₗ
      Algebra.linearMap B (FractionRing B))
    (Algebra.linearMap B L)
H :
  Eq (α := RingHom.{u_2, u_3} K (FractionRing B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing A) (FractionRing B))
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv A K))) : K →+* FractionRing A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv B L))) : L →+* FractionRing B) (algebraMap K L))
this_2 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
this_3 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
this : Algebra.IsIntegral A B
⊢ Eq (α := Submodule B L)
    (Submodule.map (AlgHom.toLinearMap (↑(FractionRing.algEquiv B L) : FractionRing B →ₐ[B] L))
      (traceDual A (FractionRing A) 1))
    (traceDual A K 1)
have e_a : Eq (α := Submodule B L) (traceDual A K (Submodule.map (AlgEquiv.toLinearMap (FractionRing.algEquiv B L)) 1))
  (traceDual A K 1)
Tactic: refine (map_equiv_traceDual A K _).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
this_1 :
  Eq (α := B →ₗ[B] L)
    ((↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L) ∘ₗ
      Algebra.linearMap B (FractionRing B))
    (Algebra.linearMap B L)
H :
  Eq (α := RingHom.{u_2, u_3} K (FractionRing B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing A) (FractionRing B))
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv A K))) : K →+* FractionRing A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv B L))) : L →+* FractionRing B) (algebraMap K L))
this_2 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
this_3 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
this : Algebra.IsIntegral A B
⊢ Eq (α := Submodule B L) (traceDual A K (Submodule.map (AlgEquiv.toLinearMap (FractionRing.algEquiv B L)) 1))
    (traceDual A K 1)
have e_a : Eq (α := Submodule B L) (Submodule.map (AlgEquiv.toLinearMap (FractionRing.algEquiv B L)) 1) 1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
this_1 :
  Eq (α := B →ₗ[B] L)
    ((↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L) ∘ₗ
      Algebra.linearMap B (FractionRing B))
    (Algebra.linearMap B L)
H :
  Eq (α := RingHom.{u_2, u_3} K (FractionRing B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing A) (FractionRing B))
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv A K))) : K →+* FractionRing A))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv B L))) : L →+* FractionRing B) (algebraMap K L))
this_2 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
this_3 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
this : Algebra.IsIntegral A B
⊢ Eq (α := Submodule B L) (Submodule.map (AlgEquiv.toLinearMap (FractionRing.algEquiv B L)) 1) 1
have e_a : ∀ (x : L),
  Membership.mem (γ := Submodule B L) (Submodule.map (AlgEquiv.toLinearMap (FractionRing.algEquiv B L)) 1) x ↔
    Membership.mem (γ := Submodule B L) 1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
⊢ Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑(differentIdeal A B) : FractionalIdeal B⁰ L)
    (FractionalIdeal.dual A K 1)⁻¹
have a : Eq.{u + 1} (α := Submodule B L)
  ((fun (I : FractionalIdeal.{u_3, u} (R := B) B⁰ L) ↦ (↑I : Submodule B L))
    (↑(differentIdeal A B) : FractionalIdeal B⁰ L))
  ((fun (I : FractionalIdeal.{u_3, u} (R := B) B⁰ L) ↦ (↑I : Submodule B L)) (FractionalIdeal.dual A K 1)⁻¹)
Tactic: apply FractionalIdeal.coeToSubmodule_injective
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
B : Type u_3
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
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
⊢ Ne (α := Ideal B) (differentIdeal A B) ⊥
have rw : ¬Eq.{u_3 + 1} (α := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1)⁻¹ (↑⊥ : FractionalIdeal B⁰ L)
Tactic: rw [ne_eq, ← FractionalIdeal.coeIdeal_inj (K := L), coeIdeal_differentIdeal (K := K)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
⊢ (↑(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
have 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
Tactic: rw [coeIdeal_differentIdeal A K L B, FractionalIdeal.inv_le_comm (by simp) hI,
    ← FractionalIdeal.coe_le_coe, FractionalIdeal.coe_dual_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
have 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
Tactic: refine le_traceDual_iff_map_le_one.trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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)
⊢ differentIdeal A C =
    HMul.hMul (α := Ideal C) (differentIdeal B C) (Ideal.map (F := B →+* C) (algebraMap B C) (differentIdeal A B))
have this : 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) _ _
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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)
⊢ differentIdeal A C =
    HMul.hMul (α := Ideal C) (differentIdeal B C) (Ideal.map (F := B →+* C) (algebraMap B C) (differentIdeal A B))
have this₁ : 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)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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)
⊢ differentIdeal A C =
    HMul.hMul (α := Ideal C) (differentIdeal B C) (Ideal.map (F := B →+* C) (algebraMap B C) (differentIdeal A B))
have this₁ : FiniteDimensional.{u_1, u_4} (FractionRing A) (FractionRing B)
Tactic: haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰