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
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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
rw : dual A K 1 * I⁻¹ * I = dual A K 1
rw₁ : dual A K 1 * (I⁻¹ * I) = dual A K 1
rw₂ : HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) 1 = dual A K 1
⊢ dual A K I * I = dual A K 1
have rw₃ : Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) (dual A K 1)
Tactic: rw [dual_eq_mul_inv, mul_assoc, inv_mul_cancel₀ hI, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
⊢ I * dual A K I = dual A K 1
have rw : dual A K I * I = dual A K 1
Tactic: rw [mul_comm, dual_mul_self A K hI]
-- 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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
rw : dual A K I * I = dual A K 1
⊢ I * dual A K I = dual A K 1
have rw₁ : Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) (dual A K 1)
Tactic: rw [mul_comm, dual_mul_self A K hI]
-- 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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
⊢ dual A K I⁻¹ = dual A K 1 * I
have rw : dual A K 1 * I⁻¹⁻¹ = dual A K 1 * I
Tactic: rw [dual_eq_mul_inv, inv_inv]
-- 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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
rw : dual A K 1 * I⁻¹⁻¹ = dual A K 1 * I
⊢ dual A K I⁻¹ = dual A K 1 * I
have rw₁ : dual A K 1 * I = dual A K 1 * I
Tactic: rw [dual_eq_mul_inv, inv_inv]
-- 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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
⊢ dual A K (dual A K I) = I
have rw : Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) 0
Tactic: rw [dual_eq_mul_inv, dual_eq_mul_inv A K (I := I), mul_inv, inv_inv, ← mul_assoc, mul_inv_cancel₀,
    one_mul]
-- 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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 1) 0
have rw : Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 0
Tactic: rw [dual_ne_zero_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 : 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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hJ : J ≠ 0
⊢ dual A K I ≤ dual A K J ↔ J ≤ I
have nth_rewrite : dual A K I ≤ dual A K J ↔ J ≤ dual A K (dual A K I)
Tactic: nth_rewrite 2 [← dual_dual A K I]
-- 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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hJ : J ≠ 0
⊢ dual A K I ≤ dual A K J ↔ J ≤ dual A K (dual A K I)
have rw : dual A K I * J ≤ dual A K 1 ↔ J ≤ dual A K (dual A K I)
Tactic: rw [le_dual_iff A K hJ, le_dual_iff A K (I := J) (by rwa [dual_ne_zero_iff]), mul_comm]
-- 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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hJ : J ≠ 0
rw : dual A K I * J ≤ dual A K 1 ↔ J ≤ dual A K (dual A K I)
⊢ dual A K I ≤ dual A K J ↔ J ≤ dual A K (dual A K I)
have rw₁ : dual A K I * J ≤ dual A K 1 ↔ J * dual A K I ≤ dual A K 1
Tactic: rw [le_dual_iff A K hJ, le_dual_iff A K (I := J) (by rwa [dual_ne_zero_iff]), mul_comm]
-- 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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hJ : J ≠ 0
rw : dual A K I * J ≤ dual A K 1 ↔ J ≤ dual A K (dual A K I)
rw₁ : dual A K I * J ≤ dual A K 1 ↔ J * dual A K I ≤ dual A K 1
⊢ dual A K I ≤ dual A K J ↔ J ≤ dual A K (dual A K I)
have rw₂ : J * dual A K I ≤ dual A K 1 ↔ J * dual A K I ≤ dual A K 1
Tactic: rw [le_dual_iff A K hJ, le_dual_iff A K (I := J) (by rwa [dual_ne_zero_iff]), mul_comm]
-- 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_5
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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
x : M
hx : Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual A K 1) x
⊢ Membership.mem.{u, u} (α := L) (γ := FractionalIdeal.{u_5, u} (R := B) B⁰ L) (dual A K 1)
    ((Algebra.trace L M : (a : M) → L) x : L)
have simp : ∀
  (hx :
    ∀ (a : C),
      ∃ (x_1 : A),
        Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
          ((Algebra.trace K M : (a : M) → K) (a • x) : K))
  (a : B),
  ∃ (x_1 : A),
    Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
      ((Algebra.trace K M : (a : M) → K) (a • x) : K)
Tactic: simp only [ne_eq, one_ne_zero, not_false_eq_true, mem_dual, mem_one_iff, traceForm_apply,
    RingHom.mem_range, forall_exists_index, forall_apply_eq_imp_iff,
    mul_comm _ (algebraMap _ _ _), ← Algebra.smul_def, ← LinearMap.map_smul_of_tower,
    Algebra.trace_trace] at hx ⊢
Cleared hypotheses: hx
-- 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_5
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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
x : L
hx : Membership.mem (γ := FractionalIdeal.{u_5, u} (R := B) B⁰ L) (dual A K 1) x
y : M
hy : Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual B L 1) y
⊢ Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (dual A K 1) (x • y)
have simp : ∀
  (hx :
    ∀ (a : B),
      ∃ (x_1 : A),
        Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
          ((Algebra.trace K L : (a : L) → K) (a • x) : K))
  (hy :
    ∀ (a : C),
      ∃ (x : B),
        Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) x : L)
          ((Algebra.trace L M : (a : M) → L) (a • y) : L))
  (a : C),
  ∃ (x_1 : A),
    Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
      ((Algebra.trace K M : (a : M) → K) (a • x • y) : K)
Tactic: simp only [ne_eq, one_ne_zero, not_false_eq_true, mem_dual, mem_one_iff, traceForm_apply,
    RingHom.mem_range, forall_exists_index, forall_apply_eq_imp_iff, mul_comm _ (algebraMap _ _ _),
    ← Algebra.smul_def] at hx hy ⊢
Cleared hypotheses: hx, 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_5
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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
x : L
y : M
hx :
  ∀ (a : B),
    ∃ (x_1 : A),
      Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
        ((Algebra.trace K L : (a : L) → K) (a • x) : K)
hy :
  ∀ (a : C),
    ∃ (x : B),
      Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) x : L)
        ((Algebra.trace L M : (a : M) → L) (a • y) : L)
c : C
⊢ ∃ (x_1 : A),
    Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
      ((Algebra.trace K M : (a : M) → K) (c • x • y) : K)
have obtain : ∀ (b : B)
  (hb :
    Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) b : L)
      ((Algebra.trace L M : (a : M) → L) (c • y) : L)),
  ∃ (x_1 : A),
    Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
      ((Algebra.trace K M : (a : M) → K) (c • x • y) : K)
Tactic: obtain ⟨b, hb⟩ := hy c
-- 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_5
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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
x : L
y : M
hx :
  ∀ (a : B),
    ∃ (x_1 : A),
      Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
        ((Algebra.trace K L : (a : L) → K) (a • x) : K)
hy :
  ∀ (a : C),
    ∃ (x : B),
      Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) x : L)
        ((Algebra.trace L M : (a : M) → L) (a • y) : L)
c : C
b : B
hb :
  Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) b : L) ((Algebra.trace L M : (a : M) → L) (c • y) : L)
⊢ ∃ (x_1 : A),
    Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
      ((Algebra.trace K M : (a : M) → K) (c • x • y) : K)
have obtain : ∀ (a : A)
  (ha :
    Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) a : K)
      ((Algebra.trace K L : (a : L) → K) (b • x) : K)),
  ∃ (x_1 : A),
    Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
      ((Algebra.trace K M : (a : M) → K) (c • x • y) : K)
Tactic: obtain ⟨a, ha⟩ := hx 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_5
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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
x : L
y : M
hx :
  ∀ (a : B),
    ∃ (x_1 : A),
      Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
        ((Algebra.trace K L : (a : L) → K) (a • x) : K)
hy :
  ∀ (a : C),
    ∃ (x : B),
      Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) x : L)
        ((Algebra.trace L M : (a : M) → L) (a • y) : L)
c : C
b : B
hb :
  Eq.{u + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) b : L) ((Algebra.trace L M : (a : M) → L) (c • y) : L)
a : A
ha :
  Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) a : K)
    ((Algebra.trace K L : (a : L) → K) (b • x) : K)
⊢ ∃ (x_1 : A),
    Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
      ((Algebra.trace K M : (a : M) → K) (c • x • y) : K)
have h : Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) a : K)
  ((Algebra.trace K M : (a : M) → K) (c • x • y) : K)
Tactic: use a
-- 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_5
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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
inst_41 : IsTorsionFree B C
⊢ dual A K 1 =
    HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (β := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M)
      (dual B L 1)
      ((extendedHom M C : (a : FractionalIdeal B⁰ L) → FractionalIdeal C⁰ M) (dual A K 1) :
        FractionalIdeal.{u_3, u_4} (R := C) C⁰ M)
have this : IsLocalization (algebraMapSubmonoid.{u_5, u_3} (R := B) C B⁰) M
Tactic: have := IsIntegralClosure.isLocalization B L M C
-- 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_5
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 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
C : Type u_3
M : Type u_4
inst_19 : CommRing C
inst_20 : IsDedekindDomain C
inst_21 : Field M
inst_22 : Algebra C M
inst_23 : IsFractionRing C M
inst_24 : Algebra A C
inst_25 : Algebra B C
inst_26 : Algebra A M
inst_27 : Algebra B M
inst_28 : Algebra K M
inst_29 : Algebra L M
inst_30 : IsScalarTower A C M
inst_31 : IsScalarTower A K M
inst_32 : IsScalarTower B C M
inst_33 : IsScalarTower B L M
inst_34 : IsScalarTower K L M
inst_35 : IsIntegralClosure C A M
inst_36 : FiniteDimensional K M
inst_37 : FiniteDimensional L M
inst_38 : Algebra.IsSeparable K M
inst_39 : IsIntegralClosure C B M
inst_40 : Algebra.IsSeparable L M
inst_41 : IsTorsionFree B C
this : IsLocalization (algebraMapSubmonoid.{u_5, u_3} (R := B) C B⁰) M
⊢ dual A K 1 =
    HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M) (β := FractionalIdeal.{u_3, u_4} (R := C) C⁰ M)
      (dual B L 1)
      ((extendedHom M C : (a : FractionalIdeal B⁰ L) → FractionalIdeal C⁰ M) (dual A K 1) :
        FractionalIdeal.{u_3, u_4} (R := C) C⁰ M)
have h : LE.le (α := Submonoid B) B⁰ (Submonoid.comap (F := B →+* C) (algebraMap B C) C⁰)
Tactic: have h : B⁰ ≤ Submonoid.comap (algebraMap B C) C⁰ :=
    nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _ <| FaithfulSMul.algebraMap_injective _ _