awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : CommRing Sₘ
inst_6 : Algebra S Sₘ
M : Submonoid R
inst_7 : IsLocalization M Rₘ
inst_8 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra Rₘ Sₘ
inst_10 : Algebra R Sₘ
inst_11 : IsScalarTower R Rₘ Sₘ
inst_12 : IsScalarTower R S Sₘ
inst_13 : Free R S
inst_14 : Module.Finite R S
a : S
h : Subsingleton R
this : Subsingleton Rₘ
⊢ Eq.{u_3 + 1} (α := Rₘ) ((norm Rₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((norm R : (a : S) → R) a : R) : Rₘ)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : CommRing Sₘ
inst_6 : Algebra S Sₘ
M : Submonoid R
inst_7 : IsLocalization M Rₘ
inst_8 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra Rₘ Sₘ
inst_10 : Algebra R Sₘ
inst_11 : IsScalarTower R Rₘ Sₘ
inst_12 : IsScalarTower R S Sₘ
inst_13 : Free R S
inst_14 : Module.Finite R S
a : S
b : R
hM : M ≤ R⁰
⊢ (norm R : (a : S) → R) a = b ↔
    Eq.{u_3 + 1} (α := Rₘ) ((norm Rₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) b : Rₘ)

Tactic:
⟨fun h ↦ h.symm ▸ Algebra.norm_localization _ M _, fun h ↦
    IsLocalization.injective Rₘ hM <| h.symm ▸ (Algebra.norm_localization R M a).symm⟩

Premises used: Algebra.norm_localization, IsLocalization.injective, Eq.rec, Iff.intro, Eq.symm
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : CommRing Sₘ
inst_6 : Algebra S Sₘ
M : Submonoid R
inst_7 : IsLocalization M Rₘ
inst_8 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra Rₘ Sₘ
inst_10 : Algebra R Sₘ
inst_11 : IsScalarTower R Rₘ Sₘ
inst_12 : IsScalarTower R S Sₘ
inst_13 : Free R S
inst_14 : Module.Finite R S
a : S
inl :
  Subsingleton R →
    Eq.{u_3 + 1} (α := Rₘ) ((trace Rₘ Sₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((trace R S : (a : S) → R) a : R) : Rₘ)
inr :
  Nontrivial R →
    Eq.{u_3 + 1} (α := Rₘ) ((trace Rₘ Sₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((trace R S : (a : S) → R) a : R) : Rₘ)
⊢ Eq.{u_3 + 1} (α := Rₘ) ((trace Rₘ Sₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((trace R S : (a : S) → R) a : R) : Rₘ)

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : CommRing Sₘ
inst_6 : Algebra S Sₘ
M : Submonoid R
inst_7 : IsLocalization M Rₘ
inst_8 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra Rₘ Sₘ
inst_10 : Algebra R Sₘ
inst_11 : IsScalarTower R Rₘ Sₘ
inst_12 : IsScalarTower R S Sₘ
inst_13 : Free R S
inst_14 : Module.Finite R S
a : S
h : Subsingleton R
this : Subsingleton Rₘ
⊢ Eq.{u_3 + 1} (α := Rₘ) ((trace Rₘ Sₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((trace R S : (a : S) → R) a : R) : Rₘ)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : CommRing Sₘ
inst_6 : Algebra S Sₘ
M : Submonoid R
inst_7 : IsLocalization M Rₘ
inst_8 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra Rₘ Sₘ
inst_10 : Algebra R Sₘ
inst_11 : IsScalarTower R Rₘ Sₘ
inst_12 : IsScalarTower R S Sₘ
inst_13 : Free R S
inst_14 : Module.Finite R S
a : S
h : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
this : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
inr :
  Eq.{u_3 + 1} (α := Rₘ)
    (Matrix.trace.{u_2, u_3} (n := Free.ChooseBasisIndex R S)
        ((RingHom.mapMatrix (algebraMap R Rₘ) :
            (a : Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) →
              Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
          ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) a)) :
      Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ)
        (Matrix.trace.{u_2, u_1} (n := Free.ChooseBasisIndex R S)
          ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) a)) :
      Rₘ)
⊢ Eq.{u_3 + 1} (α := Rₘ) ((trace Rₘ Sₘ : (a : Sₘ) → Rₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) a : Sₘ) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) ((trace R S : (a : S) → R) a : R) : Rₘ)

Tactic:
rw [Algebra.trace_eq_matrix_trace (b.localizationLocalization Rₘ M Sₘ),
    Algebra.trace_eq_matrix_trace b, ← Algebra.map_leftMulMatrix_localization]

Premises used: Algebra.map_leftMulMatrix_localization, Module.Basis.localizationLocalization, Algebra.trace_eq_matrix_trace
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : CommRing Sₘ
inst_6 : Algebra S Sₘ
M : Submonoid R
inst_7 : IsLocalization M Rₘ
inst_8 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra Rₘ Sₘ
inst_10 : Algebra R Sₘ
inst_11 : IsScalarTower R Rₘ Sₘ
inst_12 : IsScalarTower R S Sₘ
inst_13 : Free R S
inst_14 : Module.Finite R S
a : S
h : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
this : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ Eq.{u_3 + 1} (α := Rₘ)
    (Matrix.trace.{u_2, u_3} (n := Free.ChooseBasisIndex R S)
        ((RingHom.mapMatrix (algebraMap R Rₘ) :
            (a : Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) →
              Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
          ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) a)) :
      Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ)
        (Matrix.trace.{u_2, u_1} (n := Free.ChooseBasisIndex R S)
          ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) a)) :
      Rₘ)

Tactic:
(AddMonoidHom.map_trace (algebraMap R Rₘ).toAddMonoidHom _).symm

Premises used: Algebra.algebraMap, AddMonoidHom.map_trace, RingHom.toAddMonoidHom, Matrix.map, Eq.symm
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
inst_5 : CommRing Sₘ
inst_6 : Algebra S Sₘ
M : Submonoid R
inst_7 : IsLocalization M Rₘ
inst_8 : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst_9 : Algebra Rₘ Sₘ
inst_10 : Algebra R Sₘ
inst_11 : IsScalarTower R Rₘ Sₘ
inst_12 : IsScalarTower R S Sₘ
inst_13 : Free R S
inst_14 : Module.Finite R S
a : S
h : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
this : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ Eq.{u_3 + 1} (α := Rₘ)
    (Matrix.trace.{u_2, u_3} (n := Free.ChooseBasisIndex R S)
        ((RingHom.mapMatrix (algebraMap R Rₘ) :
            (a : Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) →
              Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) Rₘ)
          ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) a)) :
      Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ)
        (Matrix.trace.{u_2, u_1} (n := Free.ChooseBasisIndex R S)
          ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) a)) :
      Rₘ)

Tactic:
exact (AddMonoidHom.map_trace (algebraMap R Rₘ).toAddMonoidHom _).symm

Premises used: Algebra.algebraMap, AddMonoidHom.map_trace, RingHom.toAddMonoidHom, Eq.symm
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
M : Submonoid R
inst_5 : IsLocalization M Rₘ
Sₘ : Type u_5
inst_6 : CommRing Sₘ
inst_7 : Algebra S Sₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : Algebra R Sₘ
inst_10 : IsScalarTower R Rₘ Sₘ
inst_11 : IsScalarTower R S Sₘ
inst_12 : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst_13 : Fintype ι
inst_14 : DecidableEq ι
b : Basis ι R S
⊢ Module.Finite R S

Tactic:
have : Module.Finite R S := Module.Finite.of_basis b
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
M : Submonoid R
inst_5 : IsLocalization M Rₘ
Sₘ : Type u_5
inst_6 : CommRing Sₘ
inst_7 : Algebra S Sₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : Algebra R Sₘ
inst_10 : IsScalarTower R Rₘ Sₘ
inst_11 : IsScalarTower R S Sₘ
inst_12 : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst_13 : Fintype ι
inst_14 : DecidableEq ι
b : Basis ι R S
this : Module.Finite R S
⊢ Free R S

Tactic:
have : Module.Free R S := Module.Free.of_basis b
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
M : Submonoid R
inst_5 : IsLocalization M Rₘ
Sₘ : Type u_5
inst_6 : CommRing Sₘ
inst_7 : Algebra S Sₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : Algebra R Sₘ
inst_10 : IsScalarTower R Rₘ Sₘ
inst_11 : IsScalarTower R S Sₘ
inst_12 : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst_13 : Fintype ι
inst_14 : DecidableEq ι
b : Basis ι R S
this_1 : Module.Finite R S
this : Free R S
a :
  ∀ (i j : ι),
    traceMatrix.{u_3, u_5, u_6} Rₘ (B := Sₘ)
        (⇑(Basis.localizationLocalization.{u_1, u_3, u_2, u_5, u_6} Rₘ M (A := S) Sₘ b) : (a : ι) → Sₘ) i j =
      (RingHom.mapMatrix (algebraMap R Rₘ) : (a : Matrix ι ι R) → Matrix ι ι Rₘ)
        (traceMatrix.{u_1, u_2, u_6} R (B := S) (⇑b : (a : ι) → S)) i j
⊢ Eq (α := Matrix ι ι Rₘ)
    (traceMatrix.{u_3, u_5, u_6} Rₘ (B := Sₘ)
      (⇑(Basis.localizationLocalization.{u_1, u_3, u_2, u_5, u_6} Rₘ M (A := S) Sₘ b) : (a : ι) → Sₘ))
    ((RingHom.mapMatrix (algebraMap R Rₘ) : (a : Matrix ι ι R) → Matrix ι ι Rₘ)
      (traceMatrix.{u_1, u_2, u_6} R (B := S) (⇑b : (a : ι) → S)))

Tactic:
ext i j : 2
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
M : Submonoid R
inst_5 : IsLocalization M Rₘ
Sₘ : Type u_5
inst_6 : CommRing Sₘ
inst_7 : Algebra S Sₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : Algebra R Sₘ
inst_10 : IsScalarTower R Rₘ Sₘ
inst_11 : IsScalarTower R S Sₘ
inst_12 : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst_13 : Fintype ι
inst_14 : DecidableEq ι
b : Basis ι R S
this_1 : Module.Finite R S
this : Free R S
i j : ι
a :
  Eq.{u_3 + 1} (α := Rₘ)
    ((trace Rₘ Sₘ : (a : Sₘ) → Rₘ)
        ((algebraMap S Sₘ : (a : S) → Sₘ)
            (HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) i : S) ((b : (a : ι) → S) j : S)) :
          Sₘ) :
      Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ)
        ((trace R S : (a : S) → R) (HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) i : S) ((b : (a : ι) → S) j : S)) :
          R) :
      Rₘ)
⊢ traceMatrix.{u_3, u_5, u_6} Rₘ (B := Sₘ)
      (⇑(Basis.localizationLocalization.{u_1, u_3, u_2, u_5, u_6} Rₘ M (A := S) Sₘ b) : (a : ι) → Sₘ) i j =
    (RingHom.mapMatrix (algebraMap R Rₘ) : (a : Matrix ι ι R) → Matrix ι ι Rₘ)
      (traceMatrix.{u_1, u_2, u_6} R (B := S) (⇑b : (a : ι) → S)) i j

Tactic:
simp_rw [RingHom.mapMatrix_apply, Matrix.map_apply, traceMatrix_apply, traceForm_apply,
    Basis.localizationLocalization_apply, ← map_mul]

Premises used: RingHom.mapMatrix_apply, Algebra.traceMatrix_apply, Algebra.traceForm_apply, Module.Basis.localizationLocalization_apply, Matrix.map_apply, map_mul
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
M : Submonoid R
inst_5 : IsLocalization M Rₘ
Sₘ : Type u_5
inst_6 : CommRing Sₘ
inst_7 : Algebra S Sₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : Algebra R Sₘ
inst_10 : IsScalarTower R Rₘ Sₘ
inst_11 : IsScalarTower R S Sₘ
inst_12 : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst_13 : Fintype ι
inst_14 : DecidableEq ι
b : Basis ι R S
this_1 : Module.Finite R S
this : Free R S
i j : ι
⊢ Eq.{u_3 + 1} (α := Rₘ)
    ((trace Rₘ Sₘ : (a : Sₘ) → Rₘ)
        ((algebraMap S Sₘ : (a : S) → Sₘ)
            (HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) i : S) ((b : (a : ι) → S) j : S)) :
          Sₘ) :
      Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ)
        ((trace R S : (a : S) → R) (HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) i : S) ((b : (a : ι) → S) j : S)) :
          R) :
      Rₘ)

Tactic:
Algebra.trace_localization R M _

Premises used: Algebra.trace_localization
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
M : Submonoid R
inst_5 : IsLocalization M Rₘ
Sₘ : Type u_5
inst_6 : CommRing Sₘ
inst_7 : Algebra S Sₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : Algebra R Sₘ
inst_10 : IsScalarTower R Rₘ Sₘ
inst_11 : IsScalarTower R S Sₘ
inst_12 : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst_13 : Fintype ι
inst_14 : DecidableEq ι
b : Basis ι R S
this_1 : Module.Finite R S
this : Free R S
i j : ι
⊢ Eq.{u_3 + 1} (α := Rₘ)
    ((trace Rₘ Sₘ : (a : Sₘ) → Rₘ)
        ((algebraMap S Sₘ : (a : S) → Sₘ)
            (HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) i : S) ((b : (a : ι) → S) j : S)) :
          Sₘ) :
      Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ)
        ((trace R S : (a : S) → R) (HMul.hMul (α := S) (β := S) ((b : (a : ι) → S) i : S) ((b : (a : ι) → S) j : S)) :
          R) :
      Rₘ)

Tactic:
exact Algebra.trace_localization R M _

Premises used: Algebra.trace_localization
-- Module: Mathlib.RingTheory.Localization.NormTrace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Rₘ : Type u_3
inst_3 : CommRing Rₘ
inst_4 : Algebra R Rₘ
M : Submonoid R
inst_5 : IsLocalization M Rₘ
Sₘ : Type u_5
inst_6 : CommRing Sₘ
inst_7 : Algebra S Sₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : Algebra R Sₘ
inst_10 : IsScalarTower R Rₘ Sₘ
inst_11 : IsScalarTower R S Sₘ
inst_12 : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst_13 : Fintype ι
inst_14 : DecidableEq ι
b : Basis ι R S
rw :
  Matrix.det.{u_3, u_6} (n := ι)
      (traceMatrix.{u_3, u_5, u_6} Rₘ (B := Sₘ)
        (⇑(Basis.localizationLocalization.{u_1, u_3, u_2, u_5, u_6} Rₘ M (A := S) Sₘ b) : (a : ι) → Sₘ)) =
    (algebraMap R Rₘ : (a : R) → Rₘ) (discr.{u_1, u_2, u_6} (ι := ι) R (B := S) (⇑b : (a : ι) → S))
rw₁ :
  Matrix.det.{u_3, u_6} (n := ι)
      (traceMatrix.{u_3, u_5, u_6} Rₘ (B := Sₘ)
        (⇑(Basis.localizationLocalization.{u_1, u_3, u_2, u_5, u_6} Rₘ M (A := S) Sₘ b) : (a : ι) → Sₘ)) =
    (algebraMap R Rₘ : (a : R) → Rₘ)
      (Matrix.det.{u_1, u_6} (n := ι) (traceMatrix.{u_1, u_2, u_6} R (B := S) (⇑b : (a : ι) → S)))
rw₂ :
  Matrix.det.{u_3, u_6} (n := ι)
      (traceMatrix.{u_3, u_5, u_6} Rₘ (B := Sₘ)
        (⇑(Basis.localizationLocalization.{u_1, u_3, u_2, u_5, u_6} Rₘ M (A := S) Sₘ b) : (a : ι) → Sₘ)) =
    Matrix.det.{u_3, u_6} (n := ι)
      ((RingHom.mapMatrix (algebraMap R Rₘ) : (a : Matrix ι ι R) → Matrix ι ι Rₘ)
        (traceMatrix.{u_1, u_2, u_6} R (B := S) (⇑b : (a : ι) → S)))
rw₃ rw₄ :
  Eq.{u_3 + 1} (α := Rₘ)
    (Matrix.det.{u_3, u_6} (n := ι)
      ((RingHom.mapMatrix (algebraMap R Rₘ) : (a : Matrix ι ι R) → Matrix ι ι Rₘ)
        (traceMatrix.{u_1, u_2, u_6} R (B := S) (⇑b : (a : ι) → S))))
    (Matrix.det.{u_3, u_6} (n := ι)
      ((RingHom.mapMatrix (algebraMap R Rₘ) : (a : Matrix ι ι R) → Matrix ι ι Rₘ)
        (traceMatrix.{u_1, u_2, u_6} R (B := S) (⇑b : (a : ι) → S))))
⊢ discr.{u_3, u_5, u_6} (ι := ι) Rₘ (B := Sₘ)
      (⇑(Basis.localizationLocalization.{u_1, u_3, u_2, u_5, u_6} Rₘ M (A := S) Sₘ b) : (a : ι) → Sₘ) =
    (algebraMap R Rₘ : (a : R) → Rₘ) (discr.{u_1, u_2, u_6} (ι := ι) R (B := S) (⇑b : (a : ι) → S))

Tactic:
rw [Algebra.discr_def, Algebra.discr_def, RingHom.map_det,
    Algebra.traceMatrix_localizationLocalization]

Premises used: Algebra.traceMatrix_localizationLocalization, RingHom.map_det, Algebra.discr_def
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
obtain :
  ∀ (b : A) (b_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b) (a : A)
    (hab :
      (algebraMap A K : (a : A) → K) a =
        (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b
                b_nonzero) :
            A) •
          x),
    ∃ (a : A) (b : ↥(nonZeroDivisors A)), IsRelPrime a (↑b : A) ∧ mk' K a b = x
⊢ ∃ (a : A) (b : ↥(nonZeroDivisors A)), IsRelPrime a (↑b : A) ∧ mk' K a b = x

Tactic:
obtain ⟨⟨b, b_nonzero⟩, a, hab⟩ := exists_integer_multiple (nonZeroDivisors A) x

Premises used: nonZeroDivisors, IsLocalization.exists_integer_multiple
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
b : A
b_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
a : A
hab :
  (algebraMap A K : (a : A) → K) a =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b
            b_nonzero) :
        A) •
      x
obtain :
  ∀ (a' b' c' : A) (no_factor : IsRelPrime a' b')
    (b_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) (c' * b'))
    (hab :
      (algebraMap A K : (a : A) → K) (c' * a') =
        (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x)
                (c' * b') b_nonzero) :
            A) •
          x),
    ∃ (a : A) (b : ↥(nonZeroDivisors A)), IsRelPrime a (↑b : A) ∧ mk' K a b = x
⊢ ∃ (a : A) (b : ↥(nonZeroDivisors A)), IsRelPrime a (↑b : A) ∧ mk' K a b = x

Tactic:
obtain ⟨a', b', c', no_factor, rfl, rfl⟩ :=
    UniqueFactorizationMonoid.exists_reduced_factors' a b
      (mem_nonZeroDivisors_iff_ne_zero.mp b_nonzero)

Premises used: Iff.mp, mem_nonZeroDivisors_iff_ne_zero, rfl, UniqueFactorizationMonoid.exists_reduced_factors'
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) (c' * b')
hab :
  (algebraMap A K : (a : A) → K) (c' * a') =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) (c' * b')
            b_nonzero) :
        A) •
      x
⊢ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) c'

Tactic:
obtain ⟨_, b'_nonzero⟩ := mul_mem_nonZeroDivisors.mp b_nonzero

Premises used: Iff.mp, mul_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) (c' * b')
hab :
  (algebraMap A K : (a : A) → K) (c' * a') =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) (c' * b')
            b_nonzero) :
        A) •
      x
left : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) c'
⊢ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b'

Tactic:
obtain ⟨_, b'_nonzero⟩ := mul_mem_nonZeroDivisors.mp b_nonzero

Premises used: Iff.mp, mul_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) (c' * b')
hab :
  (algebraMap A K : (a : A) → K) (c' * a') =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) (c' * b')
            b_nonzero) :
        A) •
      x
left : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) c'
b'_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b'
⊢ ∃ (a : A) (b : ↥(nonZeroDivisors A)), IsRelPrime a (↑b : A) ∧ mk' K a b = x

Tactic:
⟨a', ⟨b', b'_nonzero⟩, no_factor, ?_⟩

Premises used: Subtype.mk, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) (c' * b')
hab :
  (algebraMap A K : (a : A) → K) (c' * a') =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) (c' * b')
            b_nonzero) :
        A) •
      x
left : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) c'
b'_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b'
refine :
  mk' K a' (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero) = x
⊢ ∃ (a : A) (b : ↥(nonZeroDivisors A)), IsRelPrime a (↑b : A) ∧ mk' K a b = x

Tactic:
refine ⟨a', ⟨b', b'_nonzero⟩, no_factor, ?_⟩
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) (c' * b')
hab :
  (algebraMap A K : (a : A) → K) (c' * a') =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) (c' * b')
            b_nonzero) :
        A) •
      x
left : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) c'
b'_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b'
⊢ mk' K a' (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero) = x

Tactic:
mul_left_cancel₀ (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors b_nonzero) ?_

Premises used: mul_left_cancel₀, IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors