awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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ₘ) ((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ₘ)
have 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ₘ)
Tactic: rw [Algebra.trace_eq_matrix_trace (b.localizationLocalization Rₘ M Sₘ),
    Algebra.trace_eq_matrix_trace b, ← Algebra.map_leftMulMatrix_localization]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (hypothesis)
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
⊢ 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)))
have this : Module.Finite R S
Tactic: have : Module.Finite R S := Module.Finite.of_basis b
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (hypothesis)
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
⊢ 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)))
have this₁ : Free R S
Tactic: have : Module.Free R S := Module.Free.of_basis b
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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
⊢ 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)))
have 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
Tactic: ext i j : 2
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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 : ι
⊢ 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
have 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ₘ)
Tactic: simp_rw [RingHom.mapMatrix_apply, Matrix.map_apply, traceMatrix_apply, traceForm_apply,
    Basis.localizationLocalization_apply, ← map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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
⊢ 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))
have 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))
Tactic: rw [Algebra.discr_def, Algebra.discr_def, RingHom.map_det,
    Algebra.traceMatrix_localizationLocalization]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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))
⊢ 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))
have 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)))
Tactic: rw [Algebra.discr_def, Algebra.discr_def, RingHom.map_det,
    Algebra.traceMatrix_localizationLocalization]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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)))
⊢ 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))
have 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)))
Tactic: rw [Algebra.discr_def, Algebra.discr_def, RingHom.map_det,
    Algebra.traceMatrix_localizationLocalization]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NormTrace (goal)
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)))
⊢ 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))
have 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))))
Tactic: rw [Algebra.discr_def, Algebra.discr_def, RingHom.map_det,
    Algebra.traceMatrix_localizationLocalization]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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 : A) (b : ↥(nonZeroDivisors A)), IsRelPrime a (↑b : A) ∧ mk' K a b = x
have 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
Tactic: obtain ⟨⟨b, b_nonzero⟩, a, hab⟩ := exists_integer_multiple (nonZeroDivisors A) x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
⊢ ∃ (a : A) (b : ↥(nonZeroDivisors A)), IsRelPrime a (↑b : A) ∧ mk' K a b = x
have 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
Tactic: obtain ⟨a', b', c', no_factor, rfl, rfl⟩ :=
    UniqueFactorizationMonoid.exists_reduced_factors' a b
      (mem_nonZeroDivisors_iff_ne_zero.mp b_nonzero)
Cleared hypotheses: b, b_nonzero, a, hab
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (hypothesis)
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
⊢ ∃ (a : A) (b : ↥(nonZeroDivisors A)), IsRelPrime a (↑b : A) ∧ mk' K a b = x
have left : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) c'
Tactic: obtain ⟨_, b'_nonzero⟩ := mul_mem_nonZeroDivisors.mp b_nonzero
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (hypothesis)
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'
⊢ ∃ (a : A) (b : ↥(nonZeroDivisors A)), IsRelPrime a (↑b : A) ∧ mk' K a b = x
have b'_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b'
Tactic: obtain ⟨_, b'_nonzero⟩ := mul_mem_nonZeroDivisors.mp b_nonzero
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
have refine : mk' K a' (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero) = x
Tactic: refine ⟨a', ⟨b', b'_nonzero⟩, no_factor, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
have refine : HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (c' * b') : K)
    (mk' K a' (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero)) =
  HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (c' * b') : K) x
Tactic: refine mul_left_cancel₀ (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors b_nonzero) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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'
⊢ HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (c' * b') : K)
      (mk' K a'
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero)) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (c' * b') : K) x
have simp : ∀
  (hab :
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) a' : K) =
      HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) b' : K) * x),
  HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) b' : K) *
      mk' K a' (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) b' : K) * x
Tactic: simp only [map_mul, Algebra.smul_def] at *
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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')
left : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) c'
b'_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b'
hab :
  HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) a' : K) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) b' : K) * x
⊢ HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) b' : K) *
      mk' K a' (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) b' : K) * x
have rw : HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) b' : K) *
    mk' K a' (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero) =
  HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) a' : K)
Tactic: rw [← hab, mul_assoc, mk'_spec' _ a' ⟨b', b'_nonzero⟩]