awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
this : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
c : ↥M
eq₃ : (↑c : R) * (x * z') = (↑c : R) * (y * z')
refine_2 :
  ∀ (eq₃ : (↑c : R) * (z' * x) = (↑c : R) * (y * z')),
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * x =
      (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * y
refine_2₁ :
  ∀ (eq₃ : (↑c : R) * (z' * x) = (↑c : R) * (z' * y)),
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * x =
      (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * y
refine_2₂ :
  ∀ (eq₃ : (↑c : R) * z' * x = (↑c : R) * (z' * y)),
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * x =
      (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * y
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * x =
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * y
have refine_2₃ : ∀ (eq₃ : (↑c : R) * z' * x = (↑c : R) * z' * y),
  (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') sorry) : R) * x =
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') sorry) : R) * y
Tactic: rwa [mul_comm _ z', mul_comm _ z', ← mul_assoc, ← mul_assoc] at eq₃
Cleared hypotheses: eq₃
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
⊢ ∃ (c : ↥(localizationLocalizationSubmodule M N)), (↑c : R) * x = (↑c : R) * y
have suffices : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
Tactic: suffices (algebraMap R S) (x * z' : R) = (algebraMap R S) (y * z') by
    obtain ⟨c, eq₃ : ↑c * (x * z') = ↑c * (y * z')⟩ := (IsLocalization.eq_iff_exists M S).mp this
    refine ⟨⟨c * z', ?_⟩, ?_⟩
    · rw [mem_localizationLocalizationSubmodule]
      refine ⟨z, c * s, ?_⟩
      rw [map_mul, ← eq₂, Submonoid.coe_mul, map_mul, mul_left_comm]
    · rwa [mul_comm _ z', mul_comm _ z', ← mul_assoc, ← mul_assoc] at eq₃
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
have rw : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
  (algebraMap R S : (a : R) → S) (y * z')
Tactic: rw [map_mul, map_mul, ← eq₂, ← mul_assoc, ← mul_assoc, mul_comm _ (z : S), eq₁,
    mul_comm _ (z : S)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
rw :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    (algebraMap R S : (a : R) → S) (y * z')
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
have rw₁ : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) y : S) ((algebraMap R S : (a : R) → S) z' : S)
Tactic: rw [map_mul, map_mul, ← eq₂, ← mul_assoc, ← mul_assoc, mul_comm _ (z : S), eq₁,
    mul_comm _ (z : S)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
rw :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    (algebraMap R S : (a : R) → S) (y * z')
rw₁ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) y : S) ((algebraMap R S : (a : R) → S) z' : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
have rw₂ : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S)
    (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S)
    (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S))
Tactic: rw [map_mul, map_mul, ← eq₂, ← mul_assoc, ← mul_assoc, mul_comm _ (z : S), eq₁,
    mul_comm _ (z : S)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
rw :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    (algebraMap R S : (a : R) → S) (y * z')
rw₁ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) y : S) ((algebraMap R S : (a : R) → S) z' : S)
rw₂ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S))
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
have rw₃ : HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (↑z : S))
    ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S)
    (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S))
Tactic: rw [map_mul, map_mul, ← eq₂, ← mul_assoc, ← mul_assoc, mul_comm _ (z : S), eq₁,
    mul_comm _ (z : S)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
rw :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    (algebraMap R S : (a : R) → S) (y * z')
rw₁ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) y : S) ((algebraMap R S : (a : R) → S) z' : S)
rw₂ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S))
rw₃ :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S))
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
have rw₄ : HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (↑z : S))
    ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑z : S))
    ((algebraMap R S : (a : R) → S) (↑s : R) : S)
Tactic: rw [map_mul, map_mul, ← eq₂, ← mul_assoc, ← mul_assoc, mul_comm _ (z : S), eq₁,
    mul_comm _ (z : S)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
rw :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    (algebraMap R S : (a : R) → S) (y * z')
rw₁ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) y : S) ((algebraMap R S : (a : R) → S) z' : S)
rw₂ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S))
rw₃ :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S))
rw₄ :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
have rw₅ : HMul.hMul (β := S) (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S))
    ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑z : S))
    ((algebraMap R S : (a : R) → S) (↑s : R) : S)
Tactic: rw [map_mul, map_mul, ← eq₂, ← mul_assoc, ← mul_assoc, mul_comm _ (z : S), eq₁,
    mul_comm _ (z : S)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
rw :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    (algebraMap R S : (a : R) → S) (y * z')
rw₁ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) y : S) ((algebraMap R S : (a : R) → S) z' : S)
rw₂ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S))
rw₃ :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S))
rw₄ :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S)
rw₅ :
  HMul.hMul (β := S) (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
have rw₆ : HMul.hMul (β := S) (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S))
    ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑z : S))
    ((algebraMap R S : (a : R) → S) (↑s : R) : S)
Tactic: rw [map_mul, map_mul, ← eq₂, ← mul_assoc, ← mul_assoc, mul_comm _ (z : S), eq₁,
    mul_comm _ (z : S)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
rw :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    (algebraMap R S : (a : R) → S) (y * z')
rw₁ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) y : S) ((algebraMap R S : (a : R) → S) z' : S)
rw₂ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S))
rw₃ :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S))
rw₄ :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S)
rw₅ :
  HMul.hMul (β := S) (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S)
rw₆ :
  HMul.hMul (β := S) (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
have rw₇ : HMul.hMul (β := S) (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S))
    ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
  HMul.hMul (β := S) (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S))
    ((algebraMap R S : (a : R) → S) (↑s : R) : S)
Tactic: rw [map_mul, map_mul, ← eq₂, ← mul_assoc, ← mul_assoc, mul_comm _ (z : S), eq₁,
    mul_comm _ (z : S)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ IsLocalization (Submonoid.comap (F := R →+* S) (algebraMap R S) N) T
have h : Submonoid.comap (F := R →+* S) (algebraMap R S) N = localizationLocalizationSubmodule M N
Tactic: convert! localization_localization_isLocalization M N T using 1
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ Eq (α := Submonoid R) (Submonoid.comap (F := R →+* S) (algebraMap R S) N)
    (Submonoid.comap (F := R →+* S) (algebraMap R S) (N ⊔ Submonoid.map (F := R →+* S) (algebraMap R S) M))
have h : N = N ⊔ Submonoid.map (F := R →+* S) (algebraMap R S) M
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ N = N ⊔ Submonoid.map (F := R →+* S) (algebraMap R S) M
have h : N ⊔ Submonoid.map (F := R →+* S) (algebraMap R S) M = N
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ N ⊔ Submonoid.map (F := R →+* S) (algebraMap R S) M = N
have h : Submonoid.map (F := R →+* S) (algebraMap R S) M ≤ N
Tactic: rw [sup_eq_left]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
p : Ideal S
Hp : p.IsPrime
inst_8 : IsLocalization.AtPrime T p
⊢ IsLocalization.AtPrime T (Ideal.comap (F := R →+* S) (algebraMap R S) p)
have apply : ∀ (x : S), IsUnit x → x ∈ p.primeCompl
Tactic: apply localization_localization_isLocalization_of_has_all_units M p.primeCompl T
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
x : Ideal R
H : x.IsPrime
inst_5 : IsDomain R
a : R
ha : a ∈ x.primeCompl
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) a
have rw : a ≠ 0
Tactic: rw [mem_nonZeroDivisors_iff_ne_zero]