awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
rw :
  HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((↑d : R) • x)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₁ :
  HDiv.hDiv (α := ℚ) (β := ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) (HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) x)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
⊢ HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) r : K)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
have rw₂ : HDiv.hDiv (β := ℚ)
    |HMul.hMul (α := ℚ) (β := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K) : ℚ)
        ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ)|
    (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
  |(Algebra.norm ℚ : (a : K) → ℚ) x|
Tactic: rw [hr, Algebra.smul_def, map_mul, abs_mul, mul_div_assoc, mul_div_cancel₀ _ (by
      rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]
      exact nonZeroDivisors.coe_ne_zero _)]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
rw :
  HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((↑d : R) • x)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₁ :
  HDiv.hDiv (α := ℚ) (β := ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) (HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) x)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₂ :
  HDiv.hDiv (β := ℚ)
      |HMul.hMul (α := ℚ) (β := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K) : ℚ)
          ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ)|
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
⊢ HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) r : K)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
have rw₃ : HDiv.hDiv (β := ℚ)
    (HMul.hMul (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ))
    (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
  |(Algebra.norm ℚ : (a : K) → ℚ) x|
Tactic: rw [hr, Algebra.smul_def, map_mul, abs_mul, mul_div_assoc, mul_div_cancel₀ _ (by
      rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]
      exact nonZeroDivisors.coe_ne_zero _)]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
rw :
  HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((↑d : R) • x)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₁ :
  HDiv.hDiv (α := ℚ) (β := ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) (HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) x)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₂ :
  HDiv.hDiv (β := ℚ)
      |HMul.hMul (α := ℚ) (β := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K) : ℚ)
          ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ)|
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₃ :
  HDiv.hDiv (β := ℚ)
      (HMul.hMul (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ)
        (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ))
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
⊢ HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) r : K)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
have rw₄ : HMul.hMul (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ)
    (HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ)) =
  |(Algebra.norm ℚ : (a : K) → ℚ) x|
Tactic: rw [hr, Algebra.smul_def, map_mul, abs_mul, mul_div_assoc, mul_div_cancel₀ _ (by
      rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]
      exact nonZeroDivisors.coe_ne_zero _)]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
rw :
  HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((↑d : R) • x)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₁ :
  HDiv.hDiv (α := ℚ) (β := ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) (HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) x)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₂ :
  HDiv.hDiv (β := ℚ)
      |HMul.hMul (α := ℚ) (β := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K) : ℚ)
          ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ)|
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₃ :
  HDiv.hDiv (β := ℚ)
      (HMul.hMul (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ)
        (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ))
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
rw₄ :
  HMul.hMul (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ)
      (HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ)
        (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ)) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
⊢ HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) r : K)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
have rw₅ : Eq (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ)
Tactic: rw [hr, Algebra.smul_def, map_mul, abs_mul, mul_div_assoc, mul_div_cancel₀ _ (by
      rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]
      exact nonZeroDivisors.coe_ne_zero _)]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
⊢ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) =
    Submodule.map (Algebra.linearMap R K) (Ideal.span {r})
have h : ∀ (x_1 : K),
  x_1 ∈ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
x_1 : K
⊢ x_1 ∈ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
have h : (∃ (b : K), Membership.mem (γ := Submodule R K) (↑(spanSingleton R⁰ x) : Submodule R K) b ∧ d • b = x_1) ↔
  Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
Tactic: simp_rw [Submodule.mem_smul_pointwise_iff_exists, mem_coe, mem_spanSingleton, Submodule.mem_map,
      Algebra.linearMap_apply, Submonoid.smul_def, Ideal.mem_span_singleton', exists_exists_eq_and,
      map_mul, hr, ← Algebra.smul_def, smul_comm (d : R)]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
x_1 : K
h :
  (∃ (b : K), Membership.mem (γ := Submodule R K) (↑(spanSingleton R⁰ x) : Submodule R K) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
⊢ x_1 ∈ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
have h₁ : (∃ (b : K), Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x) b ∧ d • b = x_1) ↔
  Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
Tactic: simp_rw [Submodule.mem_smul_pointwise_iff_exists, mem_coe, mem_spanSingleton, Submodule.mem_map,
      Algebra.linearMap_apply, Submonoid.smul_def, Ideal.mem_span_singleton', exists_exists_eq_and,
      map_mul, hr, ← Algebra.smul_def, smul_comm (d : R)]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
x_1 : K
h :
  (∃ (b : K), Membership.mem (γ := Submodule R K) (↑(spanSingleton R⁰ x) : Submodule R K) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₁ :
  (∃ (b : K), Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
⊢ x_1 ∈ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
have h₂ : (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
  Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
Tactic: simp_rw [Submodule.mem_smul_pointwise_iff_exists, mem_coe, mem_spanSingleton, Submodule.mem_map,
      Algebra.linearMap_apply, Submonoid.smul_def, Ideal.mem_span_singleton', exists_exists_eq_and,
      map_mul, hr, ← Algebra.smul_def, smul_comm (d : R)]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
x_1 : K
h :
  (∃ (b : K), Membership.mem (γ := Submodule R K) (↑(spanSingleton R⁰ x) : Submodule R K) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₁ :
  (∃ (b : K), Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₂ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
⊢ x_1 ∈ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
have h₃ : (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
  ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (Algebra.linearMap R K : (a : R) → K) y = x_1
Tactic: simp_rw [Submodule.mem_smul_pointwise_iff_exists, mem_coe, mem_spanSingleton, Submodule.mem_map,
      Algebra.linearMap_apply, Submonoid.smul_def, Ideal.mem_span_singleton', exists_exists_eq_and,
      map_mul, hr, ← Algebra.smul_def, smul_comm (d : R)]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
x_1 : K
h :
  (∃ (b : K), Membership.mem (γ := Submodule R K) (↑(spanSingleton R⁰ x) : Submodule R K) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₁ :
  (∃ (b : K), Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₂ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₃ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (Algebra.linearMap R K : (a : R) → K) y = x_1
⊢ x_1 ∈ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
have h₄ : (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
  ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
Tactic: simp_rw [Submodule.mem_smul_pointwise_iff_exists, mem_coe, mem_spanSingleton, Submodule.mem_map,
      Algebra.linearMap_apply, Submonoid.smul_def, Ideal.mem_span_singleton', exists_exists_eq_and,
      map_mul, hr, ← Algebra.smul_def, smul_comm (d : R)]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
x_1 : K
h :
  (∃ (b : K), Membership.mem (γ := Submodule R K) (↑(spanSingleton R⁰ x) : Submodule R K) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₁ :
  (∃ (b : K), Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₂ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₃ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (Algebra.linearMap R K : (a : R) → K) y = x_1
h₄ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
⊢ x_1 ∈ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
have h₅ : (∃ (b : K), (∃ (z : R), z • x = b) ∧ (↑d : R) • b = x_1) ↔
  ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
Tactic: simp_rw [Submodule.mem_smul_pointwise_iff_exists, mem_coe, mem_spanSingleton, Submodule.mem_map,
      Algebra.linearMap_apply, Submonoid.smul_def, Ideal.mem_span_singleton', exists_exists_eq_and,
      map_mul, hr, ← Algebra.smul_def, smul_comm (d : R)]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
x_1 : K
h :
  (∃ (b : K), Membership.mem (γ := Submodule R K) (↑(spanSingleton R⁰ x) : Submodule R K) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₁ :
  (∃ (b : K), Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₂ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₃ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (Algebra.linearMap R K : (a : R) → K) y = x_1
h₄ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
h₅ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ (↑d : R) • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
⊢ x_1 ∈ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
have h₆ : (∃ (b : K), (∃ (z : R), z • x = b) ∧ (↑d : R) • b = x_1) ↔
  ∃ (y : R), (∃ (a : R), a * r = y) ∧ (algebraMap R K : (a : R) → K) y = x_1
Tactic: simp_rw [Submodule.mem_smul_pointwise_iff_exists, mem_coe, mem_spanSingleton, Submodule.mem_map,
      Algebra.linearMap_apply, Submonoid.smul_def, Ideal.mem_span_singleton', exists_exists_eq_and,
      map_mul, hr, ← Algebra.smul_def, smul_comm (d : R)]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
x_1 : K
h :
  (∃ (b : K), Membership.mem (γ := Submodule R K) (↑(spanSingleton R⁰ x) : Submodule R K) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₁ :
  (∃ (b : K), Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₂ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₃ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (Algebra.linearMap R K : (a : R) → K) y = x_1
h₄ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
h₅ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ (↑d : R) • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
h₆ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ (↑d : R) • b = x_1) ↔
    ∃ (y : R), (∃ (a : R), a * r = y) ∧ (algebraMap R K : (a : R) → K) y = x_1
⊢ x_1 ∈ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
have h₇ : (∃ (a : R), (↑d : R) • a • x = x_1) ↔ ∃ (a : R), (algebraMap R K : (a : R) → K) (a * r) = x_1
Tactic: simp_rw [Submodule.mem_smul_pointwise_iff_exists, mem_coe, mem_spanSingleton, Submodule.mem_map,
      Algebra.linearMap_apply, Submonoid.smul_def, Ideal.mem_span_singleton', exists_exists_eq_and,
      map_mul, hr, ← Algebra.smul_def, smul_comm (d : R)]