awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Algebra.IsIntegral A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
inst_9 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
this_1 : LE.le.{u_3} (α := FractionalIdeal (R := B) B⁰ (FractionRing B)) (FractionalIdeal.dual A (FractionRing A) 1)⁻¹ 1
this :
  LE.le.{u_3} (α := Submodule B (FractionRing B))
    ((↑(FractionalIdeal.dual A (FractionRing A) 1)⁻¹ : Submodule B (FractionRing B)) : Submodule B (FractionRing B))
    (↑1 : Submodule B (FractionRing B))
rw :
  ∀
    (this :
      HDiv.hDiv (α := Submodule B (FractionRing B)) (↑1 : Submodule B (FractionRing B))
          (traceDual A (FractionRing A) (↑1 : Submodule B (FractionRing B))) ≤
        (↑1 : Submodule B (FractionRing B))),
    HDiv.hDiv (α := Submodule B (FractionRing B)) 1 (traceDual A (FractionRing A) 1) ≤
      LinearMap.range (Algebra.linearMap B (FractionRing B))
⊢ HDiv.hDiv (α := Submodule B (FractionRing B)) 1 (traceDual A (FractionRing A) 1) ≤
    LinearMap.range (Algebra.linearMap B (FractionRing B))
have hI : ∀
  (this :
    HDiv.hDiv (α := Submodule B (FractionRing B)) (↑1 : Submodule B (FractionRing B))
        (↑(FractionalIdeal.dual A (FractionRing A) 1) : Submodule B (FractionRing B)) ≤
      (↑1 : Submodule B (FractionRing B))),
  Ne.{u_3 + 1} (α := FractionalIdeal (R := B) B⁰ (FractionRing B)) 1 0
Tactic: rw [← one_div, FractionalIdeal.coe_div (FractionalIdeal.dual_ne_zero _ _ _),
    FractionalIdeal.coe_dual] at this
Cleared hypotheses: this
-- 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 : Algebra.IsIntegral A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
inst_9 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
this_1 : LE.le.{u_3} (α := FractionalIdeal (R := B) B⁰ (FractionRing B)) (FractionalIdeal.dual A (FractionRing A) 1)⁻¹ 1
this :
  LE.le.{u_3} (α := Submodule B (FractionRing B))
    ((↑(FractionalIdeal.dual A (FractionRing A) 1)⁻¹ : Submodule B (FractionRing B)) : Submodule B (FractionRing B))
    (↑1 : Submodule B (FractionRing B))
rw :
  ∀
    (this :
      HDiv.hDiv (α := Submodule B (FractionRing B)) (↑1 : Submodule B (FractionRing B))
          (traceDual A (FractionRing A) (↑1 : Submodule B (FractionRing B))) ≤
        (↑1 : Submodule B (FractionRing B))),
    HDiv.hDiv (α := Submodule B (FractionRing B)) 1 (traceDual A (FractionRing A) 1) ≤
      LinearMap.range (Algebra.linearMap B (FractionRing B))
hI :
  ∀
    (this :
      HDiv.hDiv (α := Submodule B (FractionRing B)) (↑1 : Submodule B (FractionRing B))
          (↑(FractionalIdeal.dual A (FractionRing A) 1) : Submodule B (FractionRing B)) ≤
        (↑1 : Submodule B (FractionRing B))),
    Ne.{u_3 + 1} (α := FractionalIdeal (R := B) B⁰ (FractionRing B)) 1 0
⊢ HDiv.hDiv (α := Submodule B (FractionRing B)) 1 (traceDual A (FractionRing A) 1) ≤
    LinearMap.range (Algebra.linearMap B (FractionRing B))
have rw₁ : ∀
  (this :
    (↑(HDiv.hDiv (α := FractionalIdeal (R := B) B⁰ (FractionRing B)) 1 (FractionalIdeal.dual A (FractionRing A) 1)) :
        Submodule B (FractionRing B)) ≤
      (↑1 : Submodule B (FractionRing B))),
  Ne.{u_3 + 1} (α := FractionalIdeal (R := B) B⁰ (FractionRing B)) 1 0
Tactic: rw [← one_div, FractionalIdeal.coe_div (FractionalIdeal.dual_ne_zero _ _ _),
    FractionalIdeal.coe_dual] at this
Cleared hypotheses: this
-- 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 (α := B →ₗ[B] L)
    ((↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L) ∘ₗ
      Algebra.linearMap B (FractionRing B))
    (Algebra.linearMap B L)
have h : Eq.{u + 1} (α := L)
  (((↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L) ∘ₗ
          Algebra.linearMap B (FractionRing B) :
        (a : B) → L)
      1 :
    L)
  ((Algebra.linearMap B L : (a : B) → L) 1 : L)
Tactic: ext
-- 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
⊢ coeSubmodule L (differentIdeal A B) = HDiv.hDiv (α := Submodule B L) 1 (traceDual A K 1)
have this : 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)
Tactic: have : (FractionRing.algEquiv B L).toLinearEquiv.comp (Algebra.linearMap B (FractionRing B)) =
    Algebra.linearMap B L := by ext; simp
-- 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 :
  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)
⊢ coeSubmodule L (differentIdeal A B) = HDiv.hDiv (α := Submodule B L) 1 (traceDual A K 1)
have rw : 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)
Tactic: rw [coeSubmodule, ← this]
-- 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 :
  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)
⊢ 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))
have h : Eq (α := RingHom.{u_1, u_3} A (FractionRing B))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing A) (FractionRing B))
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv A K))) : K →+* FractionRing A))
    (algebraMap A K))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv B L))) : L →+* FractionRing B) (algebraMap K L))
    (algebraMap A K))
Tactic: apply IsLocalization.ringHom_ext A⁰
-- 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 :
  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)
⊢ Eq (α := RingHom.{u_1, u_3} A (FractionRing B))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing A) (FractionRing B))
        (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv A K))) : K →+* FractionRing A))
      (algebraMap A K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv B L))) : L →+* FractionRing B) (algebraMap K L))
      (algebraMap A K))
have h : ∀ (x : A),
  Eq.{u_3 + 1} (α := FractionRing B)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing A) (FractionRing B))
              (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv A K))) : K →+* FractionRing A))
            (algebraMap A K) :
          (a : A) → FractionRing B)
        x :
      FractionRing B)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv B L))) : L →+* FractionRing B)
                (algebraMap K L))
              (algebraMap A K) :
            RingHom.{u_1, u_3} A (FractionRing B)) :
          (a : A) → FractionRing B)
        x :
      FractionRing B)
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
this :
  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)
x : A
⊢ Eq.{u_3 + 1} (α := FractionRing B)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (FractionRing A) (FractionRing B))
              (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv A K))) : K →+* FractionRing A))
            (algebraMap A K) :
          (a : A) → FractionRing B)
        x :
      FractionRing B)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv B L))) : L →+* FractionRing B)
                (algebraMap K L))
              (algebraMap A K) :
            RingHom.{u_1, u_3} A (FractionRing B)) :
          (a : A) → FractionRing B)
        x :
      FractionRing B)
have h : Eq.{u_3 + 1} (α := FractionRing B) ((algebraMap A (FractionRing B) : (a : A) → FractionRing B) x : FractionRing B)
  (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B)
      ((algebraMap A L : (a : A) → L) x) :
    FractionRing B)
Tactic: simp only [RingHom.coe_comp, RingHom.coe_coe,
      AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes,
      ← IsScalarTower.algebraMap_apply]
-- 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 :
  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)
x : A
⊢ Eq.{u_3 + 1} (α := FractionRing B) ((algebraMap A (FractionRing B) : (a : A) → FractionRing B) x : FractionRing B)
    (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B)
        ((algebraMap A L : (a : A) → L) x) :
      FractionRing B)
have h : Eq.{u_3 + 1} (α := FractionRing B) ((algebraMap A (FractionRing B) : (a : A) → FractionRing B) x : FractionRing B)
  (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) x : B)) :
    FractionRing B)
Tactic: rw [IsScalarTower.algebraMap_apply A B L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
-- 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 :
  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)
x : A
h :
  Eq.{u_3 + 1} (α := FractionRing B) ((algebraMap A (FractionRing B) : (a : A) → FractionRing B) x : FractionRing B)
    (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B)
        ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) x : B)) :
      FractionRing B)
⊢ Eq.{u_3 + 1} (α := FractionRing B) ((algebraMap A (FractionRing B) : (a : A) → FractionRing B) x : FractionRing B)
    (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B)
        ((algebraMap A L : (a : A) → L) x) :
      FractionRing B)
have h₁ : Eq.{u_3 + 1} (α := FractionRing B) ((algebraMap A (FractionRing B) : (a : A) → FractionRing B) x : FractionRing B)
  ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) ((algebraMap A B : (a : A) → B) x) : FractionRing B)
Tactic: rw [IsScalarTower.algebraMap_apply A B L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
-- 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 :
  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)
x : A
h :
  Eq.{u_3 + 1} (α := FractionRing B) ((algebraMap A (FractionRing B) : (a : A) → FractionRing B) x : FractionRing B)
    (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B)
        ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) x : B)) :
      FractionRing B)
h₁ :
  Eq.{u_3 + 1} (α := FractionRing B) ((algebraMap A (FractionRing B) : (a : A) → FractionRing B) x : FractionRing B)
    ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) ((algebraMap A B : (a : A) → B) x) : FractionRing B)
⊢ Eq.{u_3 + 1} (α := FractionRing B) ((algebraMap A (FractionRing B) : (a : A) → FractionRing B) x : FractionRing B)
    (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B)
        ((algebraMap A L : (a : A) → L) x) :
      FractionRing B)
have h₂ : Eq.{u_3 + 1} (α := FractionRing B) ((algebraMap A (FractionRing B) : (a : A) → FractionRing B) x : FractionRing B)
  ((algebraMap A (FractionRing B) : (a : A) → FractionRing B) x : FractionRing B)
Tactic: rw [IsScalarTower.algebraMap_apply A B L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
-- 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 :
  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)
⊢ 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 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))
Tactic: have H : RingHom.comp (algebraMap (FractionRing A) (FractionRing B))
      ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
        RingHom.comp ↑(FractionRing.algEquiv B L).symm.toRingEquiv (algebraMap K L) := by
    apply IsLocalization.ringHom_ext A⁰
    ext
    simp only [RingHom.coe_comp, RingHom.coe_coe,
      AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes,
      ← IsScalarTower.algebraMap_apply]
    rw [IsScalarTower.algebraMap_apply A B L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
-- 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 :
  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))
⊢ 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.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
Tactic: have : Algebra.IsSeparable (FractionRing A) (FractionRing B) :=
    Algebra.IsSeparable.of_equiv_equiv _ _ H
-- 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 : Algebra.IsSeparable.{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₁ : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)
Tactic: have : FiniteDimensional (FractionRing A) (FractionRing B) := Module.Finite.of_equiv_equiv _ _ H