awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ (↑ℤ⁰ : Set ℤ)
h :
  HMul.hMul (β := K) x
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          ((↑(a,
                    Subtype.mk (p := fun (x : 𝓞 K) ↦
                      Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
                      ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯).2 :
              𝓞 K) :
            𝓞 K) :
        K) =
    (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((a,
            Subtype.mk (p := fun (x : 𝓞 K) ↦
              Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
              ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯) :
          𝓞 K × ↥(Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰)).1
⊢ (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : 𝓞 K) * a ∈
    (↑I : FractionalIdeal (𝓞 K)⁰ K).num

Tactic:
exact Ideal.mul_mem_right _ _ I.1.num.absNorm_mem

Premises used: Units.val, FractionalIdeal.num, Ideal.absNorm_mem, Ideal.mul_mem_right
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ (↑ℤ⁰ : Set ℤ)
h :
  HMul.hMul (β := K) x
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          ((↑(a,
                    Subtype.mk (p := fun (x : 𝓞 K) ↦
                      Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
                      ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯).2 :
              𝓞 K) :
            𝓞 K) :
        K) =
    (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((a,
            Subtype.mk (p := fun (x : 𝓞 K) ↦
              Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
              ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯) :
          𝓞 K × ↥(Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰)).1
refine_1 :
  HMul.hMul (α := K) (β := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : 𝓞 K) :
        K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) =
    HMul.hMul (α := K) (β := K)
      ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
refine_1₁ refine_1₂ :
  HMul.hMul (α := K) (β := K) ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) =
    HMul.hMul (α := K) (β := K)
      ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : 𝓞 K) * a) =
    HMul.hMul (α := K) (β := K)
      ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)

Tactic:
rw [map_mul, map_natCast]

Premises used: map_mul, map_natCast
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ (↑ℤ⁰ : Set ℤ)
h :
  HMul.hMul (β := K) x
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          ((↑(a,
                    Subtype.mk (p := fun (x : 𝓞 K) ↦
                      Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
                      ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯).2 :
              𝓞 K) :
            𝓞 K) :
        K) =
    (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((a,
            Subtype.mk (p := fun (x : 𝓞 K) ↦
              Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
              ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯) :
          𝓞 K × ↥(Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰)).1
⊢ Membership.mem (γ := Submonoid ℤ) ℤ⁰
    (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ))

Tactic:
Submonoid.mul_mem _ hd (mem_nonZeroDivisors_of_ne_zero ?_)

Premises used: Submonoid.mul_mem, Set.Mem, mem_nonZeroDivisors_of_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ (↑ℤ⁰ : Set ℤ)
h :
  HMul.hMul (β := K) x
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          ((↑(a,
                    Subtype.mk (p := fun (x : 𝓞 K) ↦
                      Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
                      ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯).2 :
              𝓞 K) :
            𝓞 K) :
        K) =
    (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((a,
            Subtype.mk (p := fun (x : 𝓞 K) ↦
              Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
              ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯) :
          𝓞 K × ↥(Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰)).1
refine_2 : Ne (α := ℤ) (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ) 0
⊢ Membership.mem (γ := Submonoid ℤ) ℤ⁰
    (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ))

Tactic:
refine Submonoid.mul_mem _ hd (mem_nonZeroDivisors_of_ne_zero ?_)

Premises used: Submonoid.mul_mem, mem_nonZeroDivisors_of_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ (↑ℤ⁰ : Set ℤ)
h :
  HMul.hMul (β := K) x
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          ((↑(a,
                    Subtype.mk (p := fun (x : 𝓞 K) ↦
                      Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
                      ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯).2 :
              𝓞 K) :
            𝓞 K) :
        K) =
    (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((a,
            Subtype.mk (p := fun (x : 𝓞 K) ↦
              Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
              ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯) :
          𝓞 K × ↥(Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰)).1
refine_2 : ¬(↑I : FractionalIdeal (𝓞 K)⁰ K).num = ⊥
⊢ Ne (α := ℤ) (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ) 0

Tactic:
rw [Nat.cast_ne_zero, ne_eq, Ideal.absNorm_eq_zero_iff]

Premises used: ne_eq, Ideal.absNorm_eq_zero_iff, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ (↑ℤ⁰ : Set ℤ)
h :
  HMul.hMul (β := K) x
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          ((↑(a,
                    Subtype.mk (p := fun (x : 𝓞 K) ↦
                      Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
                      ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯).2 :
              𝓞 K) :
            𝓞 K) :
        K) =
    (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((a,
            Subtype.mk (p := fun (x : 𝓞 K) ↦
              Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
              ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯) :
          𝓞 K × ↥(Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰)).1
⊢ ¬(↑I : FractionalIdeal (𝓞 K)⁰ K).num = ⊥

Tactic:
FractionalIdeal.num_eq_zero_iff.not.mpr <| Units.ne_zero I

Premises used: Iff.mpr, Units.ne_zero, Iff.not, FractionalIdeal.num_eq_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ (↑ℤ⁰ : Set ℤ)
h :
  HMul.hMul (β := K) x
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          ((↑(a,
                    Subtype.mk (p := fun (x : 𝓞 K) ↦
                      Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
                      ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯).2 :
              𝓞 K) :
            𝓞 K) :
        K) =
    (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((a,
            Subtype.mk (p := fun (x : 𝓞 K) ↦
              Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
              ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯) :
          𝓞 K × ↥(Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰)).1
⊢ ¬(↑I : FractionalIdeal (𝓞 K)⁰ K).num = ⊥

Tactic:
exact FractionalIdeal.num_eq_zero_iff.not.mpr <| Units.ne_zero I

Premises used: Iff.mpr, Units.ne_zero, Iff.not, FractionalIdeal.num_eq_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ (↑ℤ⁰ : Set ℤ)
h :
  HMul.hMul (β := K) x
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          ((↑(a,
                    Subtype.mk (p := fun (x : 𝓞 K) ↦
                      Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
                      ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯).2 :
              𝓞 K) :
            𝓞 K) :
        K) =
    (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((a,
            Subtype.mk (p := fun (x : 𝓞 K) ↦
              Membership.mem (γ := Submonoid (𝓞 K)) (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x)
              ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d) ⋯) :
          𝓞 K × ↥(Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰)).1
refine_3 :
  Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) ℤ⁰ x)
        (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ)) ⋯ •
      x =
    HMul.hMul (α := K) (β := K)
      ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
⊢ (Subtype.mk (p := fun (x : K) ↦ x ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (HMul.hMul (α := K) (β := K)
              ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) : K)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))
            ⋯,
          Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) ℤ⁰ x)
            (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ)) ⋯).2 •
      x =
    ((↑ℤ :
            {S M M₂ : Type u_1} →
              [inst : Semiring ℤ] →
                [inst_2 : Semiring S] →
                  [inst_3 : AddCommMonoid M] →
                    [inst_4 : AddCommMonoid M₂] →
                      [inst_5 : Module ℤ M] →
                        [inst_6 : Module ℤ M₂] →
                          [inst_7 : Module S M] →
                            [inst_8 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
          (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K).subtype :
        (a : ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
      (Subtype.mk (p := fun (x : K) ↦ x ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (HMul.hMul (α := K) (β := K)
              ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) : K)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))
            ⋯,
          Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) ℤ⁰ x)
            (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ)) ⋯).1

Tactic:
simp_rw [LinearMap.coe_restrictScalars, Submodule.coe_subtype] at h ⊢

Premises used: LinearMap.coe_restrictScalars, Submodule.coe_subtype
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ (↑ℤ⁰ : Set ℤ)
h :
  HMul.hMul (β := K) x ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d : 𝓞 K) : K) =
    (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a
refine_3 :
  Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) ℤ⁰ x)
        (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ)) ⋯ •
      x =
    (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) *
      HMul.hMul (β := K) x ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d : 𝓞 K) : K)
⊢ Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) ℤ⁰ x)
        (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ)) ⋯ •
      x =
    HMul.hMul (α := K) (β := K)
      ((↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)

Tactic:
rw [← h]
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ (↑ℤ⁰ : Set ℤ)
h :
  HMul.hMul (β := K) x ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d : 𝓞 K) : K) =
    (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a
refine_3 :
  HMul.hMul (α := K) (↑d : K) (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) * x =
    (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) * (x * (↑d : K))
⊢ Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) ℤ⁰ x)
        (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ)) ⋯ •
      x =
    (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) *
      HMul.hMul (β := K) x ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d : 𝓞 K) : K)

Tactic:
simp only [Submonoid.mk_smul, zsmul_eq_mul, Int.cast_mul, Int.cast_natCast, algebraMap_int_eq,
        eq_intCast, map_intCast]

Premises used: Int.cast_natCast, zsmul_eq_mul, map_intCast, Submonoid.mk_smul, eq_intCast, Int.cast_mul, algebraMap_int_eq
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ (↑ℤ⁰ : Set ℤ)
h :
  HMul.hMul (β := K) x ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((algebraMap ℤ (𝓞 K) : (a : ℤ) → 𝓞 K) d : 𝓞 K) : K) =
    (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a
⊢ HMul.hMul (α := K) (↑d : K) (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) * x =
    (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : K) * (x * (↑d : K))

Tactic:
ring
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x₁ x₂ : ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)
h :
  Eq (α := K)
    (((↑ℤ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℤ] →
                  [inst_2 : Semiring S] →
                    [inst_3 : AddCommMonoid M] →
                      [inst_4 : AddCommMonoid M₂] →
                        [inst_5 : Module ℤ M] →
                          [inst_6 : Module ℤ M₂] →
                            [inst_7 : Module S M] →
                              [inst_8 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K).subtype :
          (a : ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
        x₁ :
      K)
    (((↑ℤ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℤ] →
                  [inst_2 : Semiring S] →
                    [inst_3 : AddCommMonoid M] →
                      [inst_4 : AddCommMonoid M₂] →
                        [inst_5 : Module ℤ M] →
                          [inst_6 : Module ℤ M₂] →
                            [inst_7 : Module S M] →
                              [inst_8 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K).subtype :
          (a : ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
        x₂ :
      K)
rwa : x₁ = HSMul.hSMul (α := ↥ℤ⁰) 1 x₂
rwa₁ : x₁ = x₂
rwa₂ rwa₃ rwa₄ rwa₅ :
  Eq (α := K)
    (((↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K).subtype :
          (a : ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
        x₁ :
      K)
    (((↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K).subtype :
          (a : ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
        x₂ :
      K)
⊢ HSMul.hSMul (α := ↥ℤ⁰) 1 x₁ = HSMul.hSMul (α := ↥ℤ⁰) 1 x₂

Tactic:
rwa [one_smul, one_smul, ← (Submodule.injective_subtype I.1.coeToSubmodule).eq_iff]

Premises used: Units.val, Function.Injective.eq_iff, one_smul, Submodule.injective_subtype, FractionalIdeal.coeToSubmodule
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
i : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)
⊢ Eq (α := K)
    (((basisOfFractionalIdeal K I :
            Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
          (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)
        i :
      K)
    ((↑(((fractionalIdealBasis K (↑I : FractionalIdeal (𝓞 K)⁰ K) :
                Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℤ
                  ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) :
              (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) →
                ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            i) :
        K) :
      K)

Tactic:
(fractionalIdealBasis K I.1).ofIsLocalizedModule_apply ℚ ℤ⁰ _ i

Premises used: Units.val, Rat, nonZeroDivisors, NumberField.fractionalIdealBasis, Module.Basis.ofIsLocalizedModule_apply, Int
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : K
rw :
  Membership.mem (γ := Submodule ℤ K)
      (LinearMap.range
        ((↑ℤ :
            {S M M₂ : Type u_1} →
              [inst : Semiring ℤ] →
                [inst_2 : Semiring S] →
                  [inst_3 : AddCommMonoid M] →
                    [inst_4 : AddCommMonoid M₂] →
                      [inst_5 : Module ℤ M] →
                        [inst_6 : Module ℤ M₂] →
                          [inst_7 : Module S M] →
                            [inst_8 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
          (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K).subtype))
      x ↔
    x ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K)
⊢ Membership.mem (γ := Submodule ℤ K)
      (Submodule.span ℤ
        (Set.range (ι := Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(basisOfFractionalIdeal K I :
                Basis (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℚ K) :
            (a : Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → K)))
      x ↔
    x ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K)

Tactic:
rw [basisOfFractionalIdeal, (fractionalIdealBasis K I.1).ofIsLocalizedModule_span ℚ ℤ⁰ _]

Premises used: Units.val, Rat, nonZeroDivisors, NumberField.fractionalIdealBasis, Int, Module.Basis.ofIsLocalizedModule_span, NumberField.basisOfFractionalIdeal
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : K
⊢ Membership.mem (γ := Submodule ℤ K)
      (LinearMap.range
        ((↑ℤ :
            {S M M₂ : Type u_1} →
              [inst : Semiring ℤ] →
                [inst_2 : Semiring S] →
                  [inst_3 : AddCommMonoid M] →
                    [inst_4 : AddCommMonoid M₂] →
                      [inst_5 : Module ℤ M] →
                        [inst_6 : Module ℤ M₂] →
                          [inst_7 : Module S M] →
                            [inst_8 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
          (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K).subtype))
      x ↔
    x ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
rw :
  Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) =
    finrank.{0, u_1} ℤ (𝓞 K)
rw₁ : Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) = finrank ℚ K
rw₂ rw₃ :
  Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) =
    Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
⊢ finrank.{0, u_1} ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) = finrank.{0, u_1} ℤ (𝓞 K)

Tactic:
rw [finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank,
    finrank_eq_card_basis (basisOfFractionalIdeal K I)]

Premises used: Module.finrank_eq_card_basis, NumberField.RingOfIntegers.rank, Module.finrank_eq_card_chooseBasisIndex, NumberField.basisOfFractionalIdeal
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)
rw :
  Eq (α := ℚ)
    (|((Basis.det.{0, u_1, u_1} (R := ℚ) (M := K) (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (integralBasis K) :
              K [⋀^Free.ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℚ] ℚ) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K) → K) → ℚ)
          (⇑(Basis.reindex (basisOfFractionalIdeal K I) e.symm : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)| :
      ℚ)
    (|((Basis.det.{0, u_1, u_1} (R := ℚ) (M := K) (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
                (Basis.localizationLocalization ℚ ℤ⁰ K (RingOfIntegers.basis K)) :
              K [⋀^Free.ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℚ] ℚ) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K) → K) → ℚ)
          (Function.comp (β := ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (Subtype.val (p := fun (x : K) ↦ x ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))
            (⇑(Basis.reindex (fractionalIdealBasis K (↑I : FractionalIdeal (𝓞 K)⁰ K)) e.symm) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))| :
      ℚ)
⊢ Eq (α := ℚ)
    (|((Basis.det.{0, u_1, u_1} (R := ℚ) (M := K) (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (integralBasis K) :
              K [⋀^Free.ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℚ] ℚ) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K) → K) → ℚ)
          (⇑(Basis.reindex (basisOfFractionalIdeal K I) e.symm : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)| :
      ℚ)
    ((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑I : FractionalIdeal (𝓞 K)⁰ K) : ℚ)

Tactic:
rw [← FractionalIdeal.abs_det_basis_change (RingOfIntegers.basis K) I.1
    ((fractionalIdealBasis K I.1).reindex e.symm)]

Premises used: Units.val, NumberField.fractionalIdealBasis, NumberField.RingOfIntegers.basis, Module.Basis.reindex, FractionalIdeal.abs_det_basis_change, Equiv.symm