awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ (x : { w : InfinitePlace K // w ≠ w₀ }),
    Eq (α := logSpace K)
      ((↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K))
              (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                    (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                  x :
                Fin (rank K))) :
          logSpace K) :
        logSpace K)
      ((Basis.reindex (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) equivFinRank :
            (a : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K)
          x :
        logSpace K)
⊢ LinearIndependent ℝ (M := { w : InfinitePlace K // w ≠ w₀ } → ℝ) fun (x : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K))
          (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
              x :
            Fin (rank K))) :
      logSpace K)

Tactic:
convert! (((basisUnitLattice K).ofZLatticeBasis ℝ _).reindex equivFinRank).linearIndependent

Premises used: NumberField.Units.basisUnitLattice, Real, Module.Basis.ofZLatticeBasis, NumberField.mixedEmbedding.fundamentalCone.equivFinRank, Module.Basis.linearIndependent, Module.Basis.reindex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w ≠ w₀ }
⊢ Eq (α := logSpace K)
    ((↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K))
            (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                  (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                x :
              Fin (rank K))) :
        logSpace K) :
      logSpace K)
    ((Basis.reindex (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) equivFinRank :
          (a : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K)
        x :
      logSpace K)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
h :
  Membership.mem (γ := Submodule ℝ (realSpace K))
    (Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)))
    (completeFamily K w₀)
⊢ Eq (α := ℝ) (∑ w : InfinitePlace K, completeFamily K w₀ w) 0

Tactic:
have := sum_eq_zero_of_mem_span_completeFamily h
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
h :
  Membership.mem (γ := Submodule ℝ (realSpace K))
    (Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)))
    (completeFamily K w₀)
this : Eq (α := ℝ) (∑ w : InfinitePlace K, completeFamily K w₀ w) 0
⊢ finrank ℚ K = 0

Tactic:
rw [completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq, Nat.cast_eq_zero] at this

Premises used: NumberField.InfinitePlace.sum_mult_eq, NumberField.mixedEmbedding.fundamentalCone.completeFamily, dif_pos, Nat.cast_sum, Nat.cast_eq_zero, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
h :
  Membership.mem (γ := Submodule ℝ (realSpace K))
    (Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)))
    (completeFamily K w₀)
this : finrank ℚ K = 0
⊢ False

Tactic:
Module.finrank_pos.ne' this

Premises used: LT.lt.ne', Module.finrank_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
h :
  Membership.mem (γ := Submodule ℝ (realSpace K))
    (Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K)))
    (completeFamily K w₀)
this : finrank ℚ K = 0
⊢ False

Tactic:
exact Module.finrank_pos.ne' this

Premises used: LT.lt.ne', Module.finrank_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
⊢ completeFamily K w₀ ∉
    Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K))

Tactic:
have h₂ : completeFamily K w₀ ∉ Submodule.span ℝ
      (Set.range (fun w : {w // w ≠ w₀} ↦ completeFamily K w.1)) := by
    intro h
    have := sum_eq_zero_of_mem_span_completeFamily h
    rw [completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq, Nat.cast_eq_zero] at this
    exact Module.finrank_pos.ne' this
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
h₂ :
  completeFamily K w₀ ∉
    Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K))
rw :
  LinearIndependent (ι := { b : InfinitePlace K // b ≠ w₀ }) ℝ (M := realSpace K)
      ((completeFamily K ∘
          (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K)) ∘
        some) ∧
    Function.comp (α := Option { b : InfinitePlace K // b ≠ w₀ }) (completeFamily K)
        (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K) none ∉
      Submodule.span ℝ
        (Set.range (ι := { b : InfinitePlace K // b ≠ w₀ })
          ((completeFamily K ∘
              (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K)) ∘
            some))
⊢ LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)

Tactic:
rw [← linearIndependent_equiv (Equiv.optionSubtypeNe w₀), linearIndependent_option]

Premises used: linearIndependent_option, NumberField.Units.dirichletUnitTheorem.w₀, linearIndependent_equiv, Equiv.optionSubtypeNe
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
h₂ :
  completeFamily K w₀ ∉
    Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K))
⊢ LinearIndependent (ι := { b : InfinitePlace K // b ≠ w₀ }) ℝ (M := realSpace K)
      ((completeFamily K ∘
          (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K)) ∘
        some) ∧
    Function.comp (α := Option { b : InfinitePlace K // b ≠ w₀ }) (completeFamily K)
        (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K) none ∉
      Submodule.span ℝ
        (Set.range (ι := { b : InfinitePlace K // b ≠ w₀ })
          ((completeFamily K ∘
              (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K)) ∘
            some))

Tactic:
⟨h₁, h₂⟩

Premises used: And.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h₁ :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
h₂ :
  completeFamily K w₀ ∉
    Submodule.span ℝ (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K))
⊢ LinearIndependent (ι := { b : InfinitePlace K // b ≠ w₀ }) ℝ (M := realSpace K)
      ((completeFamily K ∘
          (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K)) ∘
        some) ∧
    Function.comp (α := Option { b : InfinitePlace K // b ≠ w₀ }) (completeFamily K)
        (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K) none ∉
      Submodule.span ℝ
        (Set.range (ι := { b : InfinitePlace K // b ≠ w₀ })
          ((completeFamily K ∘
              (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K)) ∘
            some))

Tactic:
exact ⟨h₁, h₂⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Eq (α := realSpace K)
    ((basisOfLinearIndependentOfCardEqFinrank (b := completeFamily K) ⋯ ⋯ : (a : InfinitePlace K) → realSpace K) w₀ :
      realSpace K)
    fun (w : InfinitePlace K) ↦ ((↑w.mult : ℝ) : ℝ)
rw₁ : Eq (α := realSpace K) (completeFamily K w₀) fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
rw₂ :
  Eq.{u_1 + 1} (α := realSpace K)
    (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
    else
      (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces
          ((mixedEmbedding K : (a : K) → mixedSpace K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              (↑(fundSystem K
                    (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                        (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w₀ hi))) :
                𝓞 K)))))
    fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
rw₃ rw₄ :
  Eq.{u_1 + 1} (α := realSpace K) (fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)) fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
⊢ Eq (α := realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀ : realSpace K)
    fun (w : InfinitePlace K) ↦ ((↑w.mult : ℝ) : ℝ)

Tactic:
rw [completeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, completeFamily, dif_pos rfl]

Premises used: NumberField.mixedEmbedding.fundamentalCone.completeFamily, dif_pos, coe_basisOfLinearIndependentOfCardEqFinrank, rfl, NumberField.mixedEmbedding.fundamentalCone.completeBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ (x : InfinitePlace K),
    (↑expMap : realSpace K → realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀) x = Real.exp 1
⊢ Eq.{u_1 + 1} (α := realSpace K)
    ((↑expMap : realSpace K → realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀))
    fun (x : InfinitePlace K) ↦ Real.exp 1

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h :
  Real.exp (HMul.hMul (α := ℝ) (↑x.mult : ℝ)⁻¹ ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀ x)) =
    Real.exp 1
h₁ : Real.exp (HMul.hMul (α := ℝ) (↑x.mult : ℝ)⁻¹ (↑x.mult : ℝ)) = Real.exp 1
⊢ (↑expMap : realSpace K → realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w₀) x = Real.exp 1

Tactic:
simp_rw [expMap_apply, completeBasis_apply_of_eq, inv_mul_cancel₀ mult_coe_ne_zero]

Premises used: NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_eq, NumberField.InfinitePlace.mult_coe_ne_zero, NumberField.mixedEmbedding.fundamentalCone.expMap_apply, inv_mul_cancel₀
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i : { w : InfinitePlace K // w ≠ w₀ }
⊢ Membership.mem (γ := Set (realSpace K)) (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv expMap))
    (normAtAllPlaces
      ((mixedEmbedding K : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (↑(fundSystem K
                (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                    (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                  i)) :
            𝓞 K))))

Tactic:
simp [expMap_target, pos_at_place]

Premises used: NumberField.Units.pos_at_place, NumberField.mixedEmbedding.fundamentalCone.expMap_target
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i : { w : InfinitePlace K // w ≠ w₀ }
rw :
  Eq.{u_1 + 1} (α := realSpace K)
    ((↑expMap : realSpace K → realSpace K)
      ((↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
        (normAtAllPlaces
          ((mixedEmbedding K : (a : K) → mixedSpace K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              (↑(fundSystem K
                    (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                        (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                      i)) :
                𝓞 K))))))
    (normAtAllPlaces
      ((mixedEmbedding K : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (↑(fundSystem K
                (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                    (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                  i)) :
            𝓞 K))))
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := realSpace K)
    (normAtAllPlaces
      ((mixedEmbedding K : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (↑(fundSystem K
                (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                    (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                  i)) :
            𝓞 K))))
    (normAtAllPlaces
      ((mixedEmbedding K : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (↑(fundSystem K
                (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                    (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                  i)) :
            𝓞 K))))
⊢ Eq.{u_1 + 1} (α := realSpace K)
    ((↑expMap : realSpace K → realSpace K)
      ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K)))
    (normAtAllPlaces
      ((mixedEmbedding K : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (↑(fundSystem K
                (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                    (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                  i)) :
            𝓞 K))))

Tactic:
rw [completeBasis_apply_of_ne, expMap.right_inv (by simp [expMap_target, pos_at_place])]

Premises used: NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, NumberField.mixedEmbedding.fundamentalCone.expMap, OpenPartialHomeomorph.right_inv
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Eq (α := ℝ)
    |Matrix.det.{0, u_1} (n := InfinitePlace K)
        (Matrix.transpose
          ((LinearMap.toMatrix (completeBasis K) (completeBasis K) :
              (a : realSpace K →ₗ[ℝ] realSpace K) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
            (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
                  (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
              (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ)))|
    |Matrix.det (n := InfinitePlace K)
        ((Matrix.of : (a : InfinitePlace K → InfinitePlace K → ℝ) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
            fun (i w : InfinitePlace K) ↦
            if h : i = w₀ then (↑w.mult : ℝ)
            else
              (↑w.mult : ℝ) *
                Real.log
                  ((w : (a : K) → ℝ)
                    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                        (↑(fundSystem K
                              (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                                  (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                                (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) i h))) :
                          𝓞 K) :
                      K)) :
          Matrix (InfinitePlace K) (InfinitePlace K) ℝ)|
⊢ |ContinuousLinearMap.det (M := InfinitePlace K → ℝ)
        (↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) : (InfinitePlace K → ℝ) →L[ℝ] realSpace K)| =
    (↑(finrank ℚ K) : ℝ) * regulator K

Tactic:
rw [ContinuousLinearMap.det, ← LinearMap.det_toMatrix (completeBasis K), ← Matrix.det_transpose,
    regulator_eq_regOfFamily_fundSystem, finrank_mul_regOfFamily_eq_det _ w₀ equivFinRank.symm]

Premises used: Matrix.det_transpose, NumberField.Units.finrank_mul_regOfFamily_eq_det, NumberField.mixedEmbedding.fundamentalCone.equivFinRank, ContinuousLinearMap.det, NumberField.Units.dirichletUnitTheorem.w₀, NumberField.Units.regulator_eq_regOfFamily_fundSystem, Equiv.symm, LinearMap.det_toMatrix, NumberField.mixedEmbedding.fundamentalCone.completeBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
e_a :
  ∀ (w i : InfinitePlace K),
    Eq (α := ℝ)
      (Matrix.transpose
          ((LinearMap.toMatrix (completeBasis K) (completeBasis K) :
              (a : realSpace K →ₗ[ℝ] realSpace K) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
            (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
                  (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
              (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ))
          w i :
        ℝ)
      ((Matrix.of : (a : InfinitePlace K → InfinitePlace K → ℝ) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
          (fun (i w : InfinitePlace K) ↦
            if h : i = w₀ then (↑w.mult : ℝ)
            else
              (↑w.mult : ℝ) *
                Real.log
                  ((w : (a : K) → ℝ)
                    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                        (↑(fundSystem K
                              (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                                  (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                                (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) i h))) :
                          𝓞 K) :
                      K)))
          w i :
        ℝ)
⊢ Eq (α := ℝ)
    |Matrix.det.{0, u_1} (n := InfinitePlace K)
        (Matrix.transpose
          ((LinearMap.toMatrix (completeBasis K) (completeBasis K) :
              (a : realSpace K →ₗ[ℝ] realSpace K) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
            (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
                  (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
              (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ)))|
    |Matrix.det (n := InfinitePlace K)
        ((Matrix.of : (a : InfinitePlace K → InfinitePlace K → ℝ) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
            fun (i w : InfinitePlace K) ↦
            if h : i = w₀ then (↑w.mult : ℝ)
            else
              (↑w.mult : ℝ) *
                Real.log
                  ((w : (a : K) → ℝ)
                    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                        (↑(fundSystem K
                              (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                                  (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                                (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) i h))) :
                          𝓞 K) :
                      K)) :
          Matrix (InfinitePlace K) (InfinitePlace K) ℝ)|

Tactic:
congr 2 with w i
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w i : InfinitePlace K
e_a :
  Eq (α := ℝ) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w i)
    (if h : w = w₀ then (↑i.mult : ℝ)
    else
      (↑i.mult : ℝ) *
        Real.log
          ((i : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                (↑(fundSystem K
                      (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                          (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w h))) :
                  𝓞 K) :
              K)))
⊢ Eq (α := ℝ)
    (Matrix.transpose
        ((LinearMap.toMatrix (completeBasis K) (completeBasis K) :
            (a : realSpace K →ₗ[ℝ] realSpace K) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
          (↑(↑(ContinuousLinearEquiv.symm (Basis.equivFunL (completeBasis K))) :
                (InfinitePlace K → ℝ) →L[ℝ] realSpace K) :
            (InfinitePlace K → ℝ) →ₗ[ℝ] InfinitePlace K → ℝ))
        w i :
      ℝ)
    ((Matrix.of : (a : InfinitePlace K → InfinitePlace K → ℝ) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
        (fun (i w : InfinitePlace K) ↦
          if h : i = w₀ then (↑w.mult : ℝ)
          else
            (↑w.mult : ℝ) *
              Real.log
                ((w : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K
                            (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                              (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) i h))) :
                        𝓞 K) :
                    K)))
        w i :
      ℝ)

Tactic:
rw [Matrix.transpose_apply, LinearMap.toMatrix_apply, Matrix.of_apply, ← Basis.equivFunL_apply,
    ContinuousLinearMap.coe_coe, ContinuousLinearEquiv.coe_apply,
    (completeBasis K).equivFunL.apply_symm_apply]

Premises used: ContinuousLinearEquiv.apply_symm_apply, Module.Basis.equivFunL, ContinuousLinearMap.coe_coe, Module.Basis.equivFunL_apply, Matrix.of_apply, ContinuousLinearEquiv.coe_apply, Matrix.transpose_apply, LinearMap.toMatrix_apply, NumberField.mixedEmbedding.fundamentalCone.completeBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w i : InfinitePlace K
pos : ∀ (hw : w = w₀), Eq (α := ℝ) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w i) (↑i.mult : ℝ)
neg :
  ∀ (hw : ¬w = w₀),
    (completeBasis K : (a : InfinitePlace K) → realSpace K) w i =
      (↑i.mult : ℝ) *
        Real.log
          ((i : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                (↑(fundSystem K
                      (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                          (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w hw))) :
                  𝓞 K) :
              K))
⊢ Eq (α := ℝ) ((completeBasis K : (a : InfinitePlace K) → realSpace K) w i)
    (if h : w = w₀ then (↑i.mult : ℝ)
    else
      (↑i.mult : ℝ) *
        Real.log
          ((i : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                (↑(fundSystem K
                      (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                          (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w h))) :
                  𝓞 K) :
              K)))

Tactic:
split_ifs with hw