awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)
rw :
  HDiv.hDiv (α := Submodule B (FractionRing B)) 1 (traceDual A (FractionRing A) 1) ≤
    LinearMap.range (Algebra.linearMap B (FractionRing B))
⊢ coeSubmodule (FractionRing B) (differentIdeal A B) =
    HDiv.hDiv (α := Submodule B (FractionRing B)) 1 (traceDual A (FractionRing A) 1)

Tactic:
rw [coeSubmodule, differentIdeal, Submodule.map_comap_eq, inf_eq_right]

Premises used: Submodule.map_comap_eq, differentIdeal, inf_eq_right, IsLocalization.coeSubmodule
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)
⊢ LE.le.{u_3} (α := FractionalIdeal (R := B) B⁰ (FractionRing B)) (FractionalIdeal.dual A (FractionRing A) 1)⁻¹ 1

Tactic:
have := FractionalIdeal.dual_inv_le (A := A) (K := FractionRing A)
    (1 : FractionalIdeal B⁰ (FractionRing B))
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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 : LE.le.{u_3} (α := FractionalIdeal (R := B) B⁰ (FractionRing B)) (FractionalIdeal.dual A (FractionRing A) 1)⁻¹ 1
⊢ 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))

Tactic:
have : _ ≤ ((1 : FractionalIdeal B⁰ (FractionRing B)) : Submodule B (FractionRing B)) := this
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
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
⊢ HDiv.hDiv (α := Submodule B (FractionRing B)) 1 (traceDual A (FractionRing A) 1) ≤
    LinearMap.range (Algebra.linearMap B (FractionRing B))

Tactic:
rw [← one_div, FractionalIdeal.coe_div (FractionalIdeal.dual_ne_zero _ _ _),
    FractionalIdeal.coe_dual] at this

Premises used: FractionalIdeal.coe_dual, FractionalIdeal.dual_ne_zero, one_div, FractionalIdeal.coe_div
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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 :
  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))

Tactic:
simpa only [FractionalIdeal.coe_one, Submodule.one_eq_range] using this

Premises used: FractionalIdeal.coe_one, Submodule.one_eq_range
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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 :
  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:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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 :
  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:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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 :
  (↑(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:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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 :
  (↑(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:
exact one_ne_zero

Premises used: one_ne_zero
-- 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
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)
⊢ 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:
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 : 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} (α := 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:
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
⊢ 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
-- 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
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)
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)
⊢ coeSubmodule L (differentIdeal A B) = HDiv.hDiv (α := Submodule B L) 1 (traceDual A K 1)

Tactic:
rw [coeSubmodule, ← this]

Premises used: IsLocalization.coeSubmodule
-- 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
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_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))
⊢ 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:
apply IsLocalization.ringHom_ext A⁰

Premises used: nonZeroDivisors, IsLocalization.ringHom_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 : 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 :
  ∀ (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)
⊢ 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:
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 : 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 A L : (a : A) → L) x) :
      FractionRing B)
⊢ 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:
simp only [RingHom.coe_comp, RingHom.coe_coe,
      AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes,
      ← IsScalarTower.algebraMap_apply]

Premises used: RingHom.coe_coe, AlgEquiv.commutes, AlgEquiv.coe_ringEquiv, RingHom.coe_comp, Function.comp_apply, IsScalarTower.algebraMap_apply
-- 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
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)
h₂ 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)
⊢ 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:
rw [IsScalarTower.algebraMap_apply A B L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

Premises used: AlgEquiv.commutes, IsScalarTower.algebraMap_apply
-- 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
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))

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]