awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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)
⊢ (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)
have 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)
Tactic: rw [map_mul, map_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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) : ℤ))
have refine_2 : Ne (α := ℤ) (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ) 0
Tactic: refine Submonoid.mul_mem _ hd (mem_nonZeroDivisors_of_ne_zero ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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
⊢ Ne (α := ℤ) (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ) 0
have refine_2 : ¬(↑I : FractionalIdeal (𝓞 K)⁰ K).num = ⊥
Tactic: rw [Nat.cast_ne_zero, ne_eq, Ideal.absNorm_eq_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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
⊢ (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
have refine_3 : Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) ℤ⁰ x)
      (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ)) sorry •
    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: simp_rw [LinearMap.coe_restrictScalars, Submodule.coe_subtype] at h ⊢
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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
⊢ 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)
have refine_3 : Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) ℤ⁰ x)
      (d * (↑((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : FractionalIdeal (𝓞 K)⁰ K).num) : ℤ)) sorry •
    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: rw [← h]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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
⊢ 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)
have 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))
Tactic: simp only [Submonoid.mk_smul, zsmul_eq_mul, Int.cast_mul, Int.cast_natCast, algebraMap_int_eq,
        eq_intCast, map_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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)
⊢ HSMul.hSMul (α := ↥ℤ⁰) 1 x₁ = HSMul.hSMul (α := ↥ℤ⁰) 1 x₂
have rwa : x₁ = HSMul.hSMul (α := ↥ℤ⁰) 1 x₂
Tactic: rwa [one_smul, one_smul, ← (Submodule.injective_subtype I.1.coeToSubmodule).eq_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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₂
⊢ HSMul.hSMul (α := ↥ℤ⁰) 1 x₁ = HSMul.hSMul (α := ↥ℤ⁰) 1 x₂
have rwa₁ : x₁ = x₂
Tactic: rwa [one_smul, one_smul, ← (Submodule.injective_subtype I.1.coeToSubmodule).eq_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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₂
⊢ HSMul.hSMul (α := ↥ℤ⁰) 1 x₁ = HSMul.hSMul (α := ↥ℤ⁰) 1 x₂
have 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)
Tactic: rwa [one_smul, one_smul, ← (Submodule.injective_subtype I.1.coeToSubmodule).eq_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : 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)
have 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)
Tactic: rw [basisOfFractionalIdeal, (fractionalIdealBasis K I.1).ofIsLocalizedModule_span ℚ ℤ⁰ _]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ finrank.{0, u_1} ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) = finrank.{0, u_1} ℤ (𝓞 K)
have rw : Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥(↑(↑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)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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)
⊢ finrank.{0, u_1} ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) = finrank.{0, u_1} ℤ (𝓞 K)
have rw₁ : Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) = finrank ℚ K
Tactic: rw [finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank,
    finrank_eq_card_basis (basisOfFractionalIdeal K I)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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
⊢ finrank.{0, u_1} ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K) = finrank.{0, u_1} ℤ (𝓞 K)
have 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))
Tactic: rw [finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank,
    finrank_eq_card_basis (basisOfFractionalIdeal K I)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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)
⊢ 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) : ℚ)
have 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)))| :
    ℚ)
Tactic: rw [← FractionalIdeal.abs_det_basis_change (RingOfIntegers.basis K) I.1
    ((fractionalIdealBasis K I.1).reindex e.symm)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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)
⊢ 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)))| :
      ℚ)
have e_a : Eq (α := Free.ChooseBasisIndex ℤ (𝓞 K) → K)
  (⇑(Basis.reindex (basisOfFractionalIdeal K I) e.symm : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ 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)))
Tactic: congr