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
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))
⊢ Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)

Tactic:
have : Algebra.IsSeparable (FractionRing A) (FractionRing B) :=
    Algebra.IsSeparable.of_equiv_equiv _ _ H
-- 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_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)
⊢ FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing B)

Tactic:
have : FiniteDimensional (FractionRing A) (FractionRing B) := Module.Finite.of_equiv_equiv _ _ H
-- 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_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)
⊢ Algebra.IsIntegral A B

Tactic:
have : Algebra.IsIntegral A B := IsIntegralClosure.isIntegral_algebra _ L
-- 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_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
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)
⊢ 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:
simp only [AlgEquiv.toLinearEquiv_toLinearMap, Submodule.map_comp]

Premises used: Submodule.map_comp, AlgEquiv.toLinearEquiv_toLinearMap
-- 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_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
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)
⊢ 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:
rw [← coeSubmodule, coeSubmodule_differentIdeal_fractionRing _ _,
    Submodule.map_div, AlgEquiv.toLinearMap, ← AlgEquiv.toAlgHom_toLinearMap, Submodule.map_one]

Premises used: coeSubmodule_differentIdeal_fractionRing, AlgEquiv.toAlgHom_toLinearMap, AlgEquiv.toLinearMap, Submodule.map_one, IsLocalization.coeSubmodule, Submodule.map_div
-- 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_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
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)
⊢ 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:
congr 1
-- 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_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)

Tactic:
(map_equiv_traceDual A K _).trans ?_

Premises used: AlgHom.toLinearMap, map_equiv_traceDual, Eq.trans
-- 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_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
e_a :
  Eq (α := Submodule B L) (traceDual A K (Submodule.map (AlgEquiv.toLinearMap (FractionRing.algEquiv B L)) 1))
    (traceDual A K 1)
⊢ 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:
refine (map_equiv_traceDual A K _).trans ?_

Premises used: map_equiv_traceDual, Eq.trans
-- 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_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
e_a : Eq (α := Submodule B L) (Submodule.map (AlgEquiv.toLinearMap (FractionRing.algEquiv B L)) 1) 1
⊢ Eq (α := Submodule B L) (traceDual A K (Submodule.map (AlgEquiv.toLinearMap (FractionRing.algEquiv B L)) 1))
    (traceDual A K 1)

Tactic:
congr 1
-- 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_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
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
⊢ Eq (α := Submodule B L) (Submodule.map (AlgEquiv.toLinearMap (FractionRing.algEquiv B L)) 1) 1

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_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
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:
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
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)⁻¹)
⊢ Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑(differentIdeal A B) : FractionalIdeal B⁰ L)
    (FractionalIdeal.dual A K 1)⁻¹

Tactic:
apply FractionalIdeal.coeToSubmodule_injective

Premises used: FractionalIdeal.coeToSubmodule_injective
-- 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} (α := 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:
simp only [FractionalIdeal.coe_div
    (FractionalIdeal.dual_ne_zero _ _ (@one_ne_zero (FractionalIdeal B⁰ L) _ _ _)),
    FractionalIdeal.coe_coeIdeal, coeSubmodule_differentIdeal A K, inv_eq_one_div,
    FractionalIdeal.coe_dual_one, FractionalIdeal.coe_one]

Premises used: FractionalIdeal.coe_coeIdeal, coeSubmodule_differentIdeal, FractionalIdeal.coe_dual_one, inv_eq_one_div, FractionalIdeal.coe_one, FractionalIdeal.dual_ne_zero, one_ne_zero, 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 : 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
rw : ¬Eq.{u_3 + 1} (α := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1)⁻¹ (↑⊥ : FractionalIdeal B⁰ L)
⊢ Ne (α := Ideal B) (differentIdeal A B) ⊥

Tactic:
rw [ne_eq, ← FractionalIdeal.coeIdeal_inj (K := L), coeIdeal_differentIdeal (K := K)]

Premises used: FractionalIdeal.coeIdeal_inj, coeIdeal_differentIdeal, ne_eq
-- 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 : 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
⊢ ¬Eq.{u_3 + 1} (α := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1)⁻¹ (↑⊥ : FractionalIdeal B⁰ 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
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (FractionalIdeal.dual A K 1) 0

Tactic:
simp