awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Eq.{u + 1} (α := Submodule B L) ⊤ᵛ
    (if LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1 then ⊤ else ⊥)
have pos : ∀ (h : LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1),
  Eq.{u + 1} (α := Submodule B L) ⊤ᵛ ⊤
Tactic: classical
  split_ifs with h
  · rw [_root_.eq_top_iff]
    exact fun _ _ _ _ ↦ h ⟨_, rfl⟩
  · simp only [SetLike.le_def, restrictScalars_mem, LinearMap.mem_range, mem_one,
      forall_exists_index, forall_apply_eq_imp_iff, not_forall, not_exists] at h
    obtain ⟨b, hb⟩ := h
    simp_rw [eq_bot_iff, SetLike.le_def, mem_bot, mem_traceDual, mem_top, true_implies,
      traceForm_apply, RingHom.mem_range]
    contrapose! hb with hx'
    obtain ⟨c, hc, hc0⟩ := hx'
    simpa [hc0] using hc (c⁻¹ * b)
-- 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
pos :
  ∀ (h : LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1),
    Eq.{u + 1} (α := Submodule B L) ⊤ᵛ ⊤
⊢ Eq.{u + 1} (α := Submodule B L) ⊤ᵛ
    (if LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1 then ⊤ else ⊥)
have neg : ∀ (h : ¬LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1),
  Eq.{u + 1} (α := Submodule B L) ⊤ᵛ ⊥
Tactic: classical
  split_ifs with h
  · rw [_root_.eq_top_iff]
    exact fun _ _ _ _ ↦ h ⟨_, rfl⟩
  · simp only [SetLike.le_def, restrictScalars_mem, LinearMap.mem_range, mem_one,
      forall_exists_index, forall_apply_eq_imp_iff, not_forall, not_exists] at h
    obtain ⟨b, hb⟩ := h
    simp_rw [eq_bot_iff, SetLike.le_def, mem_bot, mem_traceDual, mem_top, true_implies,
      traceForm_apply, RingHom.mem_range]
    contrapose! hb with hx'
    obtain ⟨c, hc, hc0⟩ := hx'
    simpa [hc0] using hc (c⁻¹ * b)
-- 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 : Decidable (IsField A)
⊢ Eq.{u + 1} (α := Submodule B L) ⊤ᵛ (if IsField A then ⊤ else ⊥)
have h : IsField A ↔ LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1
Tactic: convert! traceDual_top'
-- 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 : Decidable (IsField A)
⊢ IsField A ↔ LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1
have h : LE.le.{u_2} (α := Subring K) ⊤ (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K)) ↔
  LE.le.{u_2} (α := Submodule A K) (restrictScalars A (R := K) ⊤) 1
Tactic: rw [← IsFractionRing.surjective_iff_isField (R := A) (K := K),
    LinearMap.range_eq_top.mpr (Algebra.trace_surjective K L),
    ← RingHom.range_eq_top, _root_.eq_top_iff]
-- 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 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
⊢ Eq (α := Submodule B L)
    (Submodule.map (↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L)
      (traceDual A (FractionRing A) I))
    (Submodule.map (↑(↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L) : FractionRing B →ₗ[B] L) I)ᵛ
have rw : Eq (α := Submodule B L)
  (comap (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B)
    (traceDual A (FractionRing A) I))
  (comap (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B) I)ᵛ
Tactic: rw [Submodule.map_equiv_eq_comap_symm, Submodule.map_equiv_eq_comap_symm]
-- 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 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
⊢ Eq (α := Submodule B L)
    (comap (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B)
      (traceDual A (FractionRing A) I))
    (comap (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B) I)ᵛ
have h : ∀ (x : L),
  Membership.mem (γ := Submodule B L)
      (comap (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B)
        (traceDual A (FractionRing A) I))
      x ↔
    Membership.mem (γ := Submodule B L)
      (comap (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B) I)ᵛ
      x
Tactic: ext x
-- 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 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
⊢ Membership.mem (α := FractionRing B)
      (toAddSubmonoid
        (LinearMap.BilinForm.dualSubmodule (S := FractionRing A) (traceForm (FractionRing A) (FractionRing B))
          (Submodule.restrictScalars A I)))
      ((((↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B) :
              L →ₗ[B] FractionRing B) :
            (a : L) → FractionRing B)
          x :
        FractionRing B) ↔
    Membership.mem (γ := AddSubmonoid L)
      (toAddSubmonoid.{u_1, u} (R := A)
        (LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (R := A) (S := K) (M := L) (traceForm K L)
          (Submodule.restrictScalars A
            (comap
              (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B)
              I))))
      x
have h : ∀ (a : FractionRing B),
  Membership.mem (γ := Submodule A (FractionRing B)) (Submodule.restrictScalars A I) a →
      Membership.mem.{u_1, u_1} (α := FractionRing A) (γ := Submodule A (FractionRing A)) 1
        ((((traceForm (FractionRing A) (FractionRing B) :
                    (a : FractionRing B) → FractionRing B →ₗ[FractionRing A] FractionRing A)
                  ((((↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) :
                          L →ₗ[B] FractionRing B) :
                        L →ₗ[B] FractionRing B) :
                      (a : L) → FractionRing B)
                    x) :
                LinearMap.{u_1, u_1, u_3, u_1} (R := FractionRing A) (RingHom.id (FractionRing A)) (FractionRing B)
                  (FractionRing A)) :
              (a : FractionRing B) → FractionRing A)
            a :
          FractionRing A) ↔
    Membership.mem (α := L) (γ := Submodule A L)
        (Submodule.restrictScalars A
          (comap (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B)
            I))
        ((AlgEquiv.toEquiv (FractionRing.algEquiv B L) : (a : FractionRing B) → L) a : L) →
      Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1
        ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K)
            ((AlgEquiv.toEquiv (FractionRing.algEquiv B L) : (a : FractionRing B) → L) a : L) :
          K)
Tactic: apply (FractionRing.algEquiv B L).forall_congr
-- 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 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
⊢ ∀ (a : FractionRing B),
    Membership.mem (γ := Submodule A (FractionRing B)) (Submodule.restrictScalars A I) a →
        Membership.mem.{u_1, u_1} (α := FractionRing A) (γ := Submodule A (FractionRing A)) 1
          ((((traceForm (FractionRing A) (FractionRing B) :
                      (a : FractionRing B) → FractionRing B →ₗ[FractionRing A] FractionRing A)
                    ((((↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) :
                            L →ₗ[B] FractionRing B) :
                          L →ₗ[B] FractionRing B) :
                        (a : L) → FractionRing B)
                      x) :
                  LinearMap.{u_1, u_1, u_3, u_1} (R := FractionRing A) (RingHom.id (FractionRing A)) (FractionRing B)
                    (FractionRing A)) :
                (a : FractionRing B) → FractionRing A)
              a :
            FractionRing A) ↔
      Membership.mem (α := L) (γ := Submodule A L)
          (Submodule.restrictScalars A
            (comap
              (↑(LinearEquiv.symm (↑(FractionRing.algEquiv B L) : FractionRing B ≃ₗ[B] L)) : L →ₗ[B] FractionRing B) I))
          ((AlgEquiv.toEquiv (FractionRing.algEquiv B L) : (a : FractionRing B) → L) a : L) →
        Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1
          ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K)
              ((AlgEquiv.toEquiv (FractionRing.algEquiv B L) : (a : FractionRing B) → L) a : L) :
            K)
have h : ∀ (a : FractionRing B),
  (a ∈ I →
      ∃ (y : A),
        Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y : FractionRing A)
          ((Algebra.trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
              (HMul.hMul (α := FractionRing B)
                (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B) x :
                  FractionRing B)
                a) :
            FractionRing A)) ↔
    a ∈ I →
      ∃ (y : A),
        Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y : K)
          ((Algebra.trace K L : (a : L) → K)
              (HMul.hMul (β := L) x ((FractionRing.algEquiv B L : (a : FractionRing B) → L) a : L)) :
            K)
Tactic: simp only [restrictScalars_mem, LinearEquiv.coe_coe, AlgEquiv.coe_symm_toLinearEquiv,
    traceForm_apply, mem_one, AlgEquiv.toEquiv_eq_coe, EquivLike.coe_coe, mem_comap,
    AlgEquiv.symm_apply_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 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
⊢ ∀ (a : FractionRing B),
    (a ∈ I →
        ∃ (y : A),
          Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y : FractionRing A)
            ((Algebra.trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
                (HMul.hMul (α := FractionRing B)
                  (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B) x :
                    FractionRing B)
                  a) :
              FractionRing A)) ↔
      a ∈ I →
        ∃ (y : A),
          Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y : K)
            ((Algebra.trace K L : (a : L) → K)
                (HMul.hMul (β := L) x ((FractionRing.algEquiv B L : (a : FractionRing B) → L) a : L)) :
              K)
have h : ∀ {y : FractionRing B} (hy : y ∈ I),
  (∃ (y_1 : A),
      Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y_1 : FractionRing A)
        ((Algebra.trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
            (HMul.hMul (α := FractionRing B)
              (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B) x :
                FractionRing B)
              y) :
          FractionRing A)) ↔
    ∃ (y_1 : A),
      Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y_1 : K)
        ((Algebra.trace K L : (a : L) → K)
            (HMul.hMul (β := L) x ((FractionRing.algEquiv B L : (a : FractionRing B) → L) y : L)) :
          K)
Tactic: refine fun {y} ↦ (forall_congr' fun hy ↦ ?_)
-- 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 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
⊢ (∃ (y_1 : A),
      Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y_1 : FractionRing A)
        ((Algebra.trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
            (HMul.hMul (α := FractionRing B)
              (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B) x :
                FractionRing B)
              y) :
          FractionRing A)) ↔
    ∃ (y_1 : A),
      Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y_1 : K)
        ((Algebra.trace K L : (a : L) → K)
            (HMul.hMul (β := L) x ((FractionRing.algEquiv B L : (a : FractionRing B) → L) y : L)) :
          K)
have h : (∃ (y_1 : A),
    Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y_1 : FractionRing A)
      (((RingEquiv.symm (AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : RingEquiv.{u_2, u_1} K (FractionRing A)) :
            (a : K) → FractionRing A)
          ((Algebra.trace K L : (a : L) → K)
            ((AlgEquiv.toRingEquiv (FractionRing.algEquiv B L) : (a : FractionRing B) → L)
                (HMul.hMul (α := FractionRing B)
                  (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B) x :
                    FractionRing B)
                  y) :
              L)) :
        FractionRing A)) ↔
  ∃ (y_1 : A),
    Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y_1 : K)
      ((Algebra.trace K L : (a : L) → K)
          (HMul.hMul (β := L) x ((FractionRing.algEquiv B L : (a : FractionRing B) → L) y : L)) :
        K)
Tactic: rw [Algebra.trace_eq_of_equiv_equiv (FractionRing.algEquiv A K).toRingEquiv
    (FractionRing.algEquiv B L).toRingEquiv]
-- 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 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
h :
  (∃ (y_1 : A),
      Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y_1 : FractionRing A)
        (((RingEquiv.symm (AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) :
                RingEquiv.{u_2, u_1} K (FractionRing A)) :
              (a : K) → FractionRing A)
            ((Algebra.trace K L : (a : L) → K)
              ((AlgEquiv.toRingEquiv (FractionRing.algEquiv B L) : (a : FractionRing B) → L)
                  (HMul.hMul (α := FractionRing B)
                    (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B)
                        x :
                      FractionRing B)
                    y) :
                L)) :
          FractionRing A)) ↔
    ∃ (y_1 : A),
      Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y_1 : K)
        ((Algebra.trace K L : (a : L) → K)
            (HMul.hMul (β := L) x ((FractionRing.algEquiv B L : (a : FractionRing B) → L) y : L)) :
          K)
⊢ (∃ (y_1 : A),
      Eq (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) y_1 : FractionRing A)
        ((Algebra.trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
            (HMul.hMul (α := FractionRing B)
              (((AlgEquiv.symm (FractionRing.algEquiv B L) : L ≃ₐ[B] FractionRing B) : (a : L) → FractionRing B) x :
                FractionRing B)
              y) :
          FractionRing A)) ↔
    ∃ (y_1 : A),
      Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y_1 : K)
        ((Algebra.trace K L : (a : L) → K)
            (HMul.hMul (β := L) x ((FractionRing.algEquiv B L : (a : FractionRing B) → L) y : L)) :
          K)
have h₁ : Eq (α := RingHom.{u_1, u} (FractionRing A) L)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
    (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
    (algebraMap (FractionRing A) (FractionRing B)))
Tactic: rw [Algebra.trace_eq_of_equiv_equiv (FractionRing.algEquiv A K).toRingEquiv
    (FractionRing.algEquiv B L).toRingEquiv]
-- 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 : IsFractionRing A K
inst_12 : IsDomain A
inst_13 : IsFractionRing B L
inst_14 : IsDomain B
inst_15 : FaithfulSMul A B
I : Submodule B (FractionRing B)
x : L
y : FractionRing B
hy : y ∈ I
⊢ Eq (α := RingHom.{u_1, u} (FractionRing A) L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
      (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
      (algebraMap (FractionRing A) (FractionRing B)))
have h : ∀ (x : FractionRing A),
  Eq.{u + 1} (α := L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
            (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K) :
          (a : FractionRing A) → L)
        x :
      L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
            (algebraMap (FractionRing A) (FractionRing B)) :
          (a : FractionRing A) → L)
        x :
      L)
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 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
⊢ LE.le.{u} (α := Submodule B L) 1 1ᵛ
have rw : LE.le (α := Submodule A K)
  (map
    ((↑A :
        {S : Type u_2} →
          {M : Type u} →
            {M₂ : Type u_2} →
              [inst : Semiring A] →
                [inst_15 : Semiring S] →
                  [inst_16 : AddCommMonoid M] →
                    [inst_17 : AddCommMonoid M₂] →
                      [inst_18 : Module A M] →
                        [inst_19 : Module A M₂] →
                          [inst_20 : Module S M] →
                            [inst_21 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
      (Algebra.trace K L))
    (restrictScalars A (LinearMap.range (Algebra.linearMap B L))))
  1
Tactic: rw [le_traceDual_iff_map_le_one, mul_one, one_eq_range]