awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hx : x ≠ 0
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A x * num A x⁻¹) : K)
      ((algebraMap A K : (a : A) → K) ((↑(den A x) : A) * (↑(den A x⁻¹) : A)) : K) =
    1

Tactic:
simp [mul_div_mul_comm, hx]

Premises used: mul_div_mul_comm
-- 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
hx : x ≠ 0
⊢ Associated (num A x⁻¹⁻¹) (↑(den A x⁻¹) : A)

Tactic:
have : Associated (num A x⁻¹⁻¹ : A) (den A x⁻¹) :=
    (associated_den_num_inv x⁻¹ (inv_ne_zero hx)).symm
-- 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
hx : x ≠ 0
this : Associated (num A x⁻¹⁻¹) (↑(den A x⁻¹) : A)
⊢ Associated (num A x) (↑(den A x⁻¹) : A)

Tactic:
rw [inv_inv] at this

Premises used: inv_inv
-- 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
hx : x ≠ 0
this : Associated (num A x) (↑(den A x⁻¹) : A)
⊢ Associated (num A x) (↑(den A x⁻¹) : A)

Tactic:
this
-- 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
hx : x ≠ 0
this : Associated (num A x) (↑(den A x⁻¹) : A)
⊢ Associated (num A x) (↑(den A x⁻¹) : A)

Tactic:
exact this
-- 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
n : A
d : ↥(nonZeroDivisors A)
pr : IsRelPrime n (↑d : A)
h : mk' K n d = x
⊢ n * (↑(den A x) : A) = num A x * (↑d : A)

Tactic:
rw [← IsFractionRing.mk'_num_den A x, IsLocalization.mk'_eq_iff_eq',
    (FaithfulSMul.algebraMap_injective _ _).eq_iff] at h

Premises used: Function.Injective.eq_iff, IsFractionRing.mk'_num_den, FaithfulSMul.algebraMap_injective, IsLocalization.mk'_eq_iff_eq'
-- 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
n : A
d : ↥(nonZeroDivisors A)
pr : IsRelPrime n (↑d : A)
h : n * (↑(den A x) : A) = num A x * (↑d : A)
⊢ Associated (num A x) n ∧ Associated (↑(den A x) : A) (↑d : A)

Tactic:
⟨associated_of_dvd_dvd
      ((num_den_reduced A x).dvd_of_dvd_mul_right <| h ▸ dvd_mul_right _ _)
      (pr.dvd_of_dvd_mul_right <| h ▸ dvd_mul_right _ _),
    associated_of_dvd_dvd
      ((num_den_reduced A x).symm.dvd_of_dvd_mul_left <| h ▸ dvd_mul_left _ _)
      (pr.symm.dvd_of_dvd_mul_left <| h ▸ dvd_mul_left _ _)⟩

Premises used: IsRelPrime.dvd_of_dvd_mul_right, associated_of_dvd_dvd, Eq.rec, IsRelPrime.symm, dvd_mul_left, And.intro, IsRelPrime.dvd_of_dvd_mul_left, dvd_mul_right, IsFractionRing.num_den_reduced, Eq.symm
-- 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
n : A
d : ↥(nonZeroDivisors A)
pr : IsRelPrime n (↑d : A)
h : n * (↑(den A x) : A) = num A x * (↑d : A)
⊢ Associated (num A x) n ∧ Associated (↑(den A x) : A) (↑d : A)

Tactic:
refine ⟨associated_of_dvd_dvd
      ((num_den_reduced A x).dvd_of_dvd_mul_right <| h ▸ dvd_mul_right _ _)
      (pr.dvd_of_dvd_mul_right <| h ▸ dvd_mul_right _ _),
    associated_of_dvd_dvd
      ((num_den_reduced A x).symm.dvd_of_dvd_mul_left <| h ▸ dvd_mul_left _ _)
      (pr.symm.dvd_of_dvd_mul_left <| h ▸ dvd_mul_left _ _)⟩
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
M : (i : ι) → Submonoid (R i)
inst_3 : ∀ (i : ι), IsLocalization.{u_2, u_3} (M i) (S i)
z : (i : ι) → S i
choose :
  ∀ (rm : (i : ι) → R i × ↥(M i))
    (h :
      ∀ (i : ι),
        HMul.hMul (β := S i) (z i) ((algebraMap (R i) (S i) : (a : R i) → S i) (↑(rm i).2 : R i) : S i) =
          (algebraMap (R i) (S i) : (a : R i) → S i) (rm i).1),
    ∃ (x : ((i : ι) → R i) × ↥(Submonoid.pi (M := R) Set.univ M)),
      HMul.hMul (β := (i : ι) → S i) z
          ((algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) (↑x.2 : (i : ι) → R i) :
            (i : ι) → S i) =
        (algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) x.1
⊢ ∃ (x : ((i : ι) → R i) × ↥(Submonoid.pi (M := R) Set.univ M)),
    HMul.hMul (β := (i : ι) → S i) z
        ((algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) (↑x.2 : (i : ι) → R i) :
          (i : ι) → S i) =
      (algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) x.1

Tactic:
choose rm h using fun i ↦ surj (M := M i) (z i)

Premises used: IsLocalization.surj
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
M : (i : ι) → Submonoid (R i)
inst_3 : ∀ (i : ι), IsLocalization.{u_2, u_3} (M i) (S i)
z : (i : ι) → S i
rm : (i : ι) → R i × ↥(M i)
h :
  ∀ (i : ι),
    HMul.hMul (β := S i) (z i) ((algebraMap (R i) (S i) : (a : R i) → S i) (↑(rm i).2 : R i) : S i) =
      (algebraMap (R i) (S i) : (a : R i) → S i) (rm i).1
⊢ ∃ (x : ((i : ι) → R i) × ↥(Submonoid.pi (M := R) Set.univ M)),
    HMul.hMul (β := (i : ι) → S i) z
        ((algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) (↑x.2 : (i : ι) → R i) :
          (i : ι) → S i) =
      (algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) x.1

Tactic:
⟨(fun i ↦ (rm i).1, ⟨_, fun i _ ↦ (rm i).2.2⟩), funext h⟩

Premises used: Prod.mk, Prod.fst, Subtype.mk, funext, Exists.intro, Prod.snd, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
M : (i : ι) → Submonoid (R i)
inst_3 : ∀ (i : ι), IsLocalization.{u_2, u_3} (M i) (S i)
z : (i : ι) → S i
rm : (i : ι) → R i × ↥(M i)
h :
  ∀ (i : ι),
    HMul.hMul (β := S i) (z i) ((algebraMap (R i) (S i) : (a : R i) → S i) (↑(rm i).2 : R i) : S i) =
      (algebraMap (R i) (S i) : (a : R i) → S i) (rm i).1
⊢ ∃ (x : ((i : ι) → R i) × ↥(Submonoid.pi (M := R) Set.univ M)),
    HMul.hMul (β := (i : ι) → S i) z
        ((algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) (↑x.2 : (i : ι) → R i) :
          (i : ι) → S i) =
      (algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) x.1

Tactic:
exact ⟨(fun i ↦ (rm i).1, ⟨_, fun i _ ↦ (rm i).2.2⟩), funext h⟩
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
M : (i : ι) → Submonoid (R i)
inst_3 : ∀ (i : ι), IsLocalization.{u_2, u_3} (M i) (S i)
x y : (i : ι) → R i
eq :
  Eq (α := (i : ι) → S i)
    ((algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) x : (i : ι) → S i)
    ((algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) y : (i : ι) → S i)
choose :
  ∀ (c : (i : ι) → ↥(M i))
    (hc :
      ∀ (i : ι),
        HMul.hMul (β := R i) (↑(c i) : R i)
            (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) x : R i) =
          HMul.hMul (β := R i) (↑(c i) : R i)
            (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) y : R i)),
    ∃ (c : ↥(Submonoid.pi (M := R) Set.univ M)), (↑c : (i : ι) → R i) * x = (↑c : (i : ι) → R i) * y
⊢ ∃ (c : ↥(Submonoid.pi (M := R) Set.univ M)), (↑c : (i : ι) → R i) * x = (↑c : (i : ι) → R i) * y

Tactic:
choose c hc using fun i ↦ exists_of_eq (M := M i) (congr_fun eq i)

Premises used: congr_fun, IsLocalization.exists_of_eq
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
M : (i : ι) → Submonoid (R i)
inst_3 : ∀ (i : ι), IsLocalization.{u_2, u_3} (M i) (S i)
x y : (i : ι) → R i
eq :
  Eq (α := (i : ι) → S i)
    ((algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) x : (i : ι) → S i)
    ((algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) y : (i : ι) → S i)
c : (i : ι) → ↥(M i)
hc :
  ∀ (i : ι),
    HMul.hMul (β := R i) (↑(c i) : R i)
        (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) x : R i) =
      HMul.hMul (β := R i) (↑(c i) : R i)
        (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) y : R i)
⊢ ∃ (c : ↥(Submonoid.pi (M := R) Set.univ M)), (↑c : (i : ι) → R i) * x = (↑c : (i : ι) → R i) * y

Tactic:
⟨⟨_, fun i _ ↦ (c i).2⟩, funext hc⟩

Premises used: Subtype.mk, funext, Exists.intro, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
M : (i : ι) → Submonoid (R i)
inst_3 : ∀ (i : ι), IsLocalization.{u_2, u_3} (M i) (S i)
x y : (i : ι) → R i
eq :
  Eq (α := (i : ι) → S i)
    ((algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) x : (i : ι) → S i)
    ((algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) y : (i : ι) → S i)
c : (i : ι) → ↥(M i)
hc :
  ∀ (i : ι),
    HMul.hMul (β := R i) (↑(c i) : R i)
        (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) x : R i) =
      HMul.hMul (β := R i) (↑(c i) : R i)
        (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) y : R i)
⊢ ∃ (c : ↥(Submonoid.pi (M := R) Set.univ M)), (↑c : (i : ι) → R i) * x = (↑c : (i : ι) → R i) * y

Tactic:
exact ⟨⟨_, fun i _ ↦ (c i).2⟩, funext hc⟩
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst_1 : CommSemiring S'
inst_2 : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst_3 : Finite ι
n : (i : ι) → R i
hn :
  Membership.mem (γ := Submonoid ((i : ι) → R i))
    (Submonoid.pi (M := R) Set.univ fun (i : ι) ↦ Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) n
choose :
  ∀ (m : (i : ι) → Membership.mem (γ := Set ι) Set.univ i → (i : ι) → R i)
    (mem : ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), m i a ∈ (↑M : Set ((i : ι) → R i)))
    (eq :
      ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i),
        (Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) (m i a) = n i),
    ∃ m ∈ M, n ∣ m
⊢ ∃ m ∈ M, n ∣ m

Tactic:
choose m mem eq using hn
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst_1 : CommSemiring S'
inst_2 : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst_3 : Finite ι
n : (i : ι) → R i
m : (i : ι) → Membership.mem (γ := Set ι) Set.univ i → (i : ι) → R i
mem : ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), m i a ∈ (↑M : Set ((i : ι) → R i))
eq :
  ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), (Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) (m i a) = n i
have : ∀ (this : Fintype ι), ∃ m ∈ M, n ∣ m
⊢ ∃ m ∈ M, n ∣ m

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst_1 : CommSemiring S'
inst_2 : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst_3 : Finite ι
n : (i : ι) → R i
m : (i : ι) → Membership.mem (γ := Set ι) Set.univ i → (i : ι) → R i
mem : ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), m i a ∈ (↑M : Set ((i : ι) → R i))
eq :
  ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), (Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) (m i a) = n i
this : Fintype ι
⊢ ∃ m ∈ M, n ∣ m

Tactic:
⟨∏ i, m i ⟨⟩, prod_mem fun i _ ↦ mem i _, pi_dvd_iff.mpr fun i ↦ ?_⟩

Premises used: Iff.mpr, Finset.univ, pi_dvd_iff, Finset.prod, And.intro, Exists.intro, prod_mem, True.intro
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst_1 : CommSemiring S'
inst_2 : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst_3 : Finite ι
n : (i : ι) → R i
m : (i : ι) → Membership.mem (γ := Set ι) Set.univ i → (i : ι) → R i
mem : ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), m i a ∈ (↑M : Set ((i : ι) → R i))
eq :
  ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), (Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) (m i a) = n i
this : Fintype ι
refine : ∀ (i : ι), n i ∣ (∏ i : ι, m i True.intro) i
⊢ ∃ m ∈ M, n ∣ m

Tactic:
refine ⟨∏ i, m i ⟨⟩, prod_mem fun i _ ↦ mem i _, pi_dvd_iff.mpr fun i ↦ ?_⟩
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst_1 : CommSemiring S'
inst_2 : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst_3 : Finite ι
n : (i : ι) → R i
m : (i : ι) → Membership.mem (γ := Set ι) Set.univ i → (i : ι) → R i
mem : ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), m i a ∈ (↑M : Set ((i : ι) → R i))
eq :
  ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), (Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) (m i a) = n i
this : Fintype ι
i : ι
rw : n i ∣ ∏ c : ι, m c True.intro i
⊢ n i ∣ (∏ i : ι, m i True.intro) i

Tactic:
rw [Fintype.prod_apply]

Premises used: Fintype.prod_apply
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst_1 : CommSemiring S'
inst_2 : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst_3 : Finite ι
n : (i : ι) → R i
m : (i : ι) → Membership.mem (γ := Set ι) Set.univ i → (i : ι) → R i
mem : ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), m i a ∈ (↑M : Set ((i : ι) → R i))
eq :
  ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), (Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) (m i a) = n i
this : Fintype ι
i : ι
⊢ n i ∣ ∏ c : ι, m c True.intro i

Tactic:
(eq i ⟨⟩).symm.dvd.trans (Finset.dvd_prod_of_mem _ <| Finset.mem_univ _)

Premises used: Finset.mem_univ, Finset.dvd_prod_of_mem, Eq.dvd, Eq.symm, Dvd.dvd.trans, True.intro
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst_1 : CommSemiring S'
inst_2 : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst_3 : Finite ι
n : (i : ι) → R i
m : (i : ι) → Membership.mem (γ := Set ι) Set.univ i → (i : ι) → R i
mem : ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), m i a ∈ (↑M : Set ((i : ι) → R i))
eq :
  ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), (Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) (m i a) = n i
this : Fintype ι
i : ι
⊢ n i ∣ ∏ c : ι, m c True.intro i

Tactic:
exact (eq i ⟨⟩).symm.dvd.trans (Finset.dvd_prod_of_mem _ <| Finset.mem_univ _)
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst_3 :
  ∀ (i : ι), IsLocalization.{u_2, u_3} (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) (S i)
y : ↥M
⊢ IsUnit (M := (i : ι) → S i)
    ((Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i) :
          (a : (i : ι) → R i) → (i : ι) → S i)
        (↑y : (i : ι) → R i) :
      (i : ι) → S i)

Tactic:
Pi.isUnit_iff.mpr fun i ↦ map_units _ (⟨y.1 i, y, y.2, rfl⟩ : M.map (Pi.evalRingHom R i))

Premises used: Iff.mpr, Pi.isUnit_iff, Subtype.mk, And.intro, Exists.intro, IsLocalization.map_units, Subtype.val, rfl, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
S' : Type u_4
inst_3 : CommSemiring S'
inst_4 : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst_5 :
  ∀ (i : ι), IsLocalization.{u_2, u_3} (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) (S i)
inst_6 : IsLocalization (R := (i : ι) → R i) M S'
inst_7 : Finite ι
⊢ Function.Bijective (α := S') (β := (i : ι) → S i)
    (⇑(lift (R := (i : ι) → R i) (M := M) (g :=
          Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i)) ⋯) :
      (a : S') → (i : ι) → S i)

Tactic:
have := (iff_map_piEvalRingHom R (Π i, S i) M).mpr inferInstance
  (ringEquivOfRingEquiv (M := M) (T := M) _ _ (.refl _) <|
    Submonoid.map_equiv_eq_comap_symm _ _).bijective

Premises used: Iff.mpr, RingEquiv.refl, RingEquiv.toMulEquiv, inferInstance, IsLocalization.iff_map_piEvalRingHom, IsLocalization.ringEquivOfRingEquiv, Submonoid.map_equiv_eq_comap_symm, RingEquiv.bijective
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst_3 :
  ∀ (i : ι), IsLocalization.{u_2, u_3} (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) (S i)
inst_4 : ∀ (i : ι), Ring.KrullDimLE.{u_2} 0 (R i)
inst_5 : ∀ (i : ι), IsLocalRing.{u_2} (R i)
apply :
  ∀ (i : ι),
    Surjective.{u_2 + 1, u_3 + 1} (α := R i) (β := S i)
      (↑(↑(algebraMap (R i) (S i)) : R i →* S i) : OneHom (R i) (S i)).1
⊢ Surjective (α := (i : ι) → R i) (β := (i : ι) → S i)
    (⇑(Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i)) :
      (a : (i : ι) → R i) → (i : ι) → S i)

Tactic:
apply Surjective.piMap (fun i ↦ ?_)

Premises used: Function.Surjective.piMap
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst_3 :
  ∀ (i : ι), IsLocalization.{u_2, u_3} (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) (S i)
inst_4 : ∀ (i : ι), Ring.KrullDimLE.{u_2} 0 (R i)
inst_5 : ∀ (i : ι), IsLocalRing.{u_2} (R i)
i : ι
pos :
  ∀
    (h₀ :
      Membership.mem (γ := Submonoid (R i)) (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) 0),
    Surjective.{u_2 + 1, u_3 + 1} (α := R i) (β := S i)
      (↑(↑(algebraMap (R i) (S i)) : R i →* S i) : OneHom (R i) (S i)).1
neg :
  ∀ (h₀ : 0 ∉ Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M),
    Surjective.{u_2 + 1, u_3 + 1} (α := R i) (β := S i)
      (↑(↑(algebraMap (R i) (S i)) : R i →* S i) : OneHom (R i) (S i)).1
⊢ Surjective.{u_2 + 1, u_3 + 1} (α := R i) (β := S i) (↑(↑(algebraMap (R i) (S i)) : R i →* S i) : OneHom (R i) (S i)).1

Tactic:
by_cases h₀ : (0 : R i) ∈ (M.map (Pi.evalRingHom R i))

Premises used: Submonoid.map, Pi.evalRingHom, OfNat.ofNat
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst_3 :
  ∀ (i : ι), IsLocalization.{u_2, u_3} (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) (S i)
inst_4 : ∀ (i : ι), Ring.KrullDimLE.{u_2} 0 (R i)
inst_5 : ∀ (i : ι), IsLocalRing.{u_2} (R i)
i : ι
h₀ : Membership.mem (γ := Submonoid (R i)) (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) 0
pos :
  ∀ (this : Unique (S i)),
    Surjective.{u_2 + 1, u_3 + 1} (α := R i) (β := S i)
      (↑(↑(algebraMap (R i) (S i)) : R i →* S i) : OneHom (R i) (S i)).1
⊢ Surjective.{u_2 + 1, u_3 + 1} (α := R i) (β := S i) (↑(↑(algebraMap (R i) (S i)) : R i →* S i) : OneHom (R i) (S i)).1

Tactic:
have := uniqueOfZeroMem h₀ (S := (S i))
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst_3 :
  ∀ (i : ι), IsLocalization.{u_2, u_3} (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) (S i)
inst_4 : ∀ (i : ι), Ring.KrullDimLE.{u_2} 0 (R i)
inst_5 : ∀ (i : ι), IsLocalRing.{u_2} (R i)
i : ι
h₀ : Membership.mem (γ := Submonoid (R i)) (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) 0
this : Unique (S i)
⊢ Surjective.{u_2 + 1, u_3 + 1} (α := R i) (β := S i) (↑(↑(algebraMap (R i) (S i)) : R i →* S i) : OneHom (R i) (S i)).1

Tactic:
surjective_to_subsingleton (algebraMap (R i) (S i))

Premises used: Algebra.algebraMap, Function.surjective_to_subsingleton, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst_3 :
  ∀ (i : ι), IsLocalization.{u_2, u_3} (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) (S i)
inst_4 : ∀ (i : ι), Ring.KrullDimLE.{u_2} 0 (R i)
inst_5 : ∀ (i : ι), IsLocalRing.{u_2} (R i)
i : ι
h₀ : Membership.mem (γ := Submonoid (R i)) (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) 0
this : Unique (S i)
⊢ Surjective.{u_2 + 1, u_3 + 1} (α := R i) (β := S i) (↑(↑(algebraMap (R i) (S i)) : R i →* S i) : OneHom (R i) (S i)).1

Tactic:
exact surjective_to_subsingleton (algebraMap (R i) (S i))

Premises used: Algebra.algebraMap, Function.surjective_to_subsingleton, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst_3 :
  ∀ (i : ι), IsLocalization.{u_2, u_3} (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) (S i)
inst_4 : ∀ (i : ι), Ring.KrullDimLE.{u_2} 0 (R i)
inst_5 : ∀ (i : ι), IsLocalRing.{u_2} (R i)
i : ι
h₀ : 0 ∉ Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M
⊢ LE.le (α := Submonoid (R i)) (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M)
    (IsUnit.submonoid (R i))

Tactic:
simpa