awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  (↑s : R i) *
      HMul.hMul (α := R i) (β := R i)
        ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₂ : (i : ι) → R i))
                ⋯) :
            R i) :
          R i)
        (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₁ : R i) =
    (↑s : R i) *
      HMul.hMul (α := R i) (β := R i)
        ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₁ : (i : ι) → R i))
                ⋯) :
            R i) :
          R i)
        (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₂ : R i)
j : ι
⊢ ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 i (↑s : R i)) ⋯) : (i : ι) → R i) *
        ((↑s₂ : (i : ι) → R i) * r₁))
      j =
    ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 i (↑s : R i)) ⋯) : (i : ι) → R i) *
        ((↑s₁ : (i : ι) → R i) * r₂))
      j
have refine_1 : ∀ (S : Submonoid (R j)),
  let T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) S;
  ∀ (s₁ s₂ : ↥T) (s : ↥S)
    (hs :
      (↑s : R j) *
          HMul.hMul (α := R j) (β := R j)
            ((↑(Subtype.mk (p := fun (x : R j) ↦ x ∈ S)
                    (((Pi.evalRingHom R j : ((i : ι) → R i) →+* R j) : (a : (i : ι) → R i) → R j) (↑s₂ : (i : ι) → R i))
                    sorry) :
                R j) :
              R j)
            (((Pi.evalRingHom R j : ((i : ι) → R i) →+* R j) : (a : (i : ι) → R i) → R j) r₁ : R j) =
        (↑s : R j) *
          HMul.hMul (α := R j) (β := R j)
            ((↑(Subtype.mk (p := fun (x : R j) ↦ x ∈ S)
                    (((Pi.evalRingHom R j : ((i : ι) → R i) →+* R j) : (a : (i : ι) → R i) → R j) (↑s₁ : (i : ι) → R i))
                    sorry) :
                R j) :
              R j)
            (((Pi.evalRingHom R j : ((i : ι) → R i) →+* R j) : (a : (i : ι) → R i) → R j) r₂ : R j)),
    ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 j (↑s : R j)) sorry) : (i : ι) → R i) *
          ((↑s₂ : (i : ι) → R i) * r₁))
        j =
      ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 j (↑s : R j)) sorry) : (i : ι) → R i) *
          ((↑s₁ : (i : ι) → R i) * r₂))
        j
Tactic: obtain rfl | ne := eq_or_ne j i
Cleared hypotheses: i, S, T, s₁, s₂, s, hs
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
x : Localization (M := R i) S
⊢ ∃ (a : Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)),
    (mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S) a = x
have refine_2 : ∀ (r : R i) (s : ↥S),
  ∃ (a : Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)),
    Eq (α := Localization (M := R i) S)
      ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S) a :
        Localization (M := R i) S)
      (mk' (Localization (M := R i) S) r s : Localization (M := R i) S)
Tactic: obtain ⟨r, s, rfl⟩ := exists_mk'_eq S x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
⊢ Bijective (α := Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) (β :=
    Localization (M := R i) S)
    (⇑(mapPiEvalRingHom (R := R) S) : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
have refine_1 : ∀ (x₁ x₂ : Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S))
  (eq :
    Eq.{u_2 + 1} (α := Localization (M := R i) S)
      ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S) x₁ :
        Localization (M := R i) S)
      ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S) x₂ :
        Localization (M := R i) S)),
  x₁ = x₂
Tactic: classical
  refine ⟨fun x₁ x₂ eq ↦ ?_, fun x ↦ ?_⟩
  · obtain ⟨r₁, s₁, rfl⟩ := exists_mk'_eq T x₁
    obtain ⟨r₂, s₂, rfl⟩ := exists_mk'_eq T x₂
    simp_rw [map_mk'] at eq
    rw [IsLocalization.eq] at eq ⊢
    obtain ⟨s, hs⟩ := eq
    refine ⟨⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩, funext fun j ↦ ?_⟩
    obtain rfl | ne := eq_or_ne j i
    · simpa using hs
    · simp [update_of_ne ne]
  · obtain ⟨r, s, rfl⟩ := exists_mk'_eq S x
    exact ⟨mk' (M := T) _ (update 0 i r) ⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩,
      by simp [map_mk']⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
refine_1 :
  ∀ (x₁ x₂ : Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S))
    (eq :
      Eq.{u_2 + 1} (α := Localization (M := R i) S)
        ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
            x₁ :
          Localization (M := R i) S)
        ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
            x₂ :
          Localization (M := R i) S)),
    x₁ = x₂
⊢ Bijective (α := Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) (β :=
    Localization (M := R i) S)
    (⇑(mapPiEvalRingHom (R := R) S) : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
have refine_2 : ∀ (x : Localization (M := R i) S),
  ∃ (a : Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)),
    (mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S) a = x
Tactic: classical
  refine ⟨fun x₁ x₂ eq ↦ ?_, fun x ↦ ?_⟩
  · obtain ⟨r₁, s₁, rfl⟩ := exists_mk'_eq T x₁
    obtain ⟨r₂, s₂, rfl⟩ := exists_mk'_eq T x₂
    simp_rw [map_mk'] at eq
    rw [IsLocalization.eq] at eq ⊢
    obtain ⟨s, hs⟩ := eq
    refine ⟨⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩, funext fun j ↦ ?_⟩
    obtain rfl | ne := eq_or_ne j i
    · simpa using hs
    · simp [update_of_ne ne]
  · obtain ⟨r, s, rfl⟩ := exists_mk'_eq S x
    exact ⟨mk' (M := T) _ (update 0 i r) ⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩,
      by simp [map_mk']⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : Finite R
⊢ Finite S
have this : Surjective.{u_1 + 1, u_2 + 1} (α := R × ↥M) (uncurry (mk' S))
Tactic: have : Function.Surjective (Function.uncurry (mk' (M := M) S)) := fun x ↦ by
    simpa using IsLocalization.exists_mk'_eq M x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
inst_3 : IsLocalization M S
N₁ : Type u_4
N₂ : Type u_5
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₁
inst_7 : Module R N₂
inst_8 : Module S N₁
inst_9 : Module S N₂
inst_10 : IsScalarTower R S N₁
inst_11 : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s : S
s' : N₁
⊢ (f : (a : N₁) → N₂) (s • s') = HSMul.hSMul (β := N₂) s ((f : (a : N₁) → N₂) s' : N₂)
have obtain : ∀ (r : R) (m : ↥M),
  (f : (a : N₁) → N₂) (mk' S r m • s') = HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
Tactic: obtain ⟨r, m, rfl⟩ := exists_mk'_eq M s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
inst_3 : IsLocalization M S
N₁ : Type u_4
N₂ : Type u_5
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₁
inst_7 : Module R N₂
inst_8 : Module S N₁
inst_9 : Module S N₂
inst_10 : IsScalarTower R S N₁
inst_11 : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
⊢ (f : (a : N₁) → N₂) (mk' S r m • s') = HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
have rw : HSMul.hSMul.{u_2, u_5, u_5} (α := S) (β := N₂) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
    ((f : (a : N₁) → N₂) (mk' S r m • s') : N₂) =
  HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
    (HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂))
Tactic: rw [← (map_units S m).smul_left_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
inst_3 : IsLocalization M S
N₁ : Type u_4
N₂ : Type u_5
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₁
inst_7 : Module R N₂
inst_8 : Module S N₁
inst_9 : Module S N₂
inst_10 : IsScalarTower R S N₁
inst_11 : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S) (β := N₂) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      ((f : (a : N₁) → N₂) (mk' S r m • s') : N₂) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      (HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂))
have simp_rw : HSMul.hSMul (β := N₂) (↑m : R) ((f : (a : N₁) → N₂) (mk' S r m • s') : N₂) =
  (↑m : R) • HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
Tactic: simp_rw [algebraMap_smul, ← map_smul, ← smul_assoc, smul_mk'_self, algebraMap_smul, map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
inst_3 : IsLocalization M S
N₁ : Type u_4
N₂ : Type u_5
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₁
inst_7 : Module R N₂
inst_8 : Module S N₁
inst_9 : Module S N₂
inst_10 : IsScalarTower R S N₁
inst_11 : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
simp_rw :
  HSMul.hSMul (β := N₂) (↑m : R) ((f : (a : N₁) → N₂) (mk' S r m • s') : N₂) =
    (↑m : R) • HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S) (β := N₂) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      ((f : (a : N₁) → N₂) (mk' S r m • s') : N₂) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      (HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂))
have simp_rw₁ : (f : (a : N₁) → N₂) ((↑m : R) • mk' S r m • s') =
  (↑m : R) • HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
Tactic: simp_rw [algebraMap_smul, ← map_smul, ← smul_assoc, smul_mk'_self, algebraMap_smul, map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
inst_3 : IsLocalization M S
N₁ : Type u_4
N₂ : Type u_5
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₁
inst_7 : Module R N₂
inst_8 : Module S N₁
inst_9 : Module S N₂
inst_10 : IsScalarTower R S N₁
inst_11 : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
simp_rw :
  HSMul.hSMul (β := N₂) (↑m : R) ((f : (a : N₁) → N₂) (mk' S r m • s') : N₂) =
    (↑m : R) • HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
simp_rw₁ :
  (f : (a : N₁) → N₂) ((↑m : R) • mk' S r m • s') =
    (↑m : R) • HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S) (β := N₂) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      ((f : (a : N₁) → N₂) (mk' S r m • s') : N₂) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      (HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂))
have simp_rw₂ : (f : (a : N₁) → N₂) (((↑m : R) • mk' S r m) • s') =
  HSMul.hSMul (β := N₂) ((↑m : R) • mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
Tactic: simp_rw [algebraMap_smul, ← map_smul, ← smul_assoc, smul_mk'_self, algebraMap_smul, map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
inst_3 : IsLocalization M S
N₁ : Type u_4
N₂ : Type u_5
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₁
inst_7 : Module R N₂
inst_8 : Module S N₁
inst_9 : Module S N₂
inst_10 : IsScalarTower R S N₁
inst_11 : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
simp_rw :
  HSMul.hSMul (β := N₂) (↑m : R) ((f : (a : N₁) → N₂) (mk' S r m • s') : N₂) =
    (↑m : R) • HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
simp_rw₁ :
  (f : (a : N₁) → N₂) ((↑m : R) • mk' S r m • s') =
    (↑m : R) • HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
simp_rw₂ :
  (f : (a : N₁) → N₂) (((↑m : R) • mk' S r m) • s') =
    HSMul.hSMul (β := N₂) ((↑m : R) • mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S) (β := N₂) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      ((f : (a : N₁) → N₂) (mk' S r m • s') : N₂) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      (HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂))
have simp_rw₃ : (f : (a : N₁) → N₂) (HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) r : S) s') =
  HSMul.hSMul.{u_2, u_5, u_5} (α := S) (β := N₂) ((algebraMap R S : (a : R) → S) r : S) ((f : (a : N₁) → N₂) s' : N₂)
Tactic: simp_rw [algebraMap_smul, ← map_smul, ← smul_assoc, smul_mk'_self, algebraMap_smul, map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
inst_3 : IsLocalization M S
N₁ : Type u_4
N₂ : Type u_5
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₁
inst_7 : Module R N₂
inst_8 : Module S N₁
inst_9 : Module S N₂
inst_10 : IsScalarTower R S N₁
inst_11 : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
simp_rw :
  HSMul.hSMul (β := N₂) (↑m : R) ((f : (a : N₁) → N₂) (mk' S r m • s') : N₂) =
    (↑m : R) • HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
simp_rw₁ :
  (f : (a : N₁) → N₂) ((↑m : R) • mk' S r m • s') =
    (↑m : R) • HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
simp_rw₂ :
  (f : (a : N₁) → N₂) (((↑m : R) • mk' S r m) • s') =
    HSMul.hSMul (β := N₂) ((↑m : R) • mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
simp_rw₃ :
  (f : (a : N₁) → N₂) (HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) r : S) s') =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) (β := N₂) ((algebraMap R S : (a : R) → S) r : S) ((f : (a : N₁) → N₂) s' : N₂)
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S) (β := N₂) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      ((f : (a : N₁) → N₂) (mk' S r m • s') : N₂) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      (HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂))
have simp_rw₄ : (f : (a : N₁) → N₂) (r • s') = HSMul.hSMul (β := N₂) r ((f : (a : N₁) → N₂) s' : N₂)
Tactic: simp_rw [algebraMap_smul, ← map_smul, ← smul_assoc, smul_mk'_self, algebraMap_smul, map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
inst_5 : Algebra R P
f g : S →ₐ[R] P
⊢ Eq (α := R →+* P) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : S →+* P) (algebraMap R S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* P) (algebraMap R S))
have rw : Eq (α := R →+* P) (algebraMap R P) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* P) (algebraMap R S))
Tactic: rw [f.comp_algebraMap, g.comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
inst_5 : Algebra R P
f g : S →ₐ[R] P
rw :
  Eq (α := R →+* P) (algebraMap R P)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* P) (algebraMap R S))
⊢ Eq (α := R →+* P) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : S →+* P) (algebraMap R S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* P) (algebraMap R S))
have rw₁ : Eq (α := R →+* P) (algebraMap R P) (algebraMap R P)
Tactic: rw [f.comp_algebraMap, g.comp_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
inst_3 : IsLocalization M S
Q : Type u_4
inst_4 : CommSemiring Q
inst_5 : Algebra R Q
inst_6 : IsLocalization M Q
f : S →+* Q
hf : Eq (α := R →+* Q) (f.comp (algebraMap R S)) (algebraMap R Q)
⊢ f = (↑(algEquiv M S Q) : S →+* Q)
have h : Eq (α := R →+* Q) (f.comp (algebraMap R S))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv M S Q) : S →+* Q) (algebraMap R S))
Tactic: apply IsLocalization.ringHom_ext M
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
inst_3 : IsLocalization M S
Q : Type u_4
inst_4 : CommSemiring Q
inst_5 : Algebra R Q
inst_6 : IsLocalization M Q
f : S →+* Q
hf : Eq (α := R →+* Q) (f.comp (algebraMap R S)) (algebraMap R Q)
⊢ Eq (α := R →+* Q) (f.comp (algebraMap R S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv M S Q) : S →+* Q) (algebraMap R S))
have h : Eq (α := R →+* Q) (algebraMap R Q)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv M S Q) : S →+* Q) (algebraMap R S))
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
inst_3 : IsLocalization M S
Q : Type u_4
inst_4 : CommSemiring Q
inst_5 : Algebra R Q
inst_6 : IsLocalization M Q
f : S →+* Q
hf : Eq (α := R →+* Q) (f.comp (algebraMap R S)) (algebraMap R Q)
⊢ Eq (α := R →+* Q) (algebraMap R Q)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv M S Q) : S →+* Q) (algebraMap R S))
have h : ∀ (x : R),
  Eq.{u_4 + 1} (α := Q) ((algebraMap R Q : (a : R) → Q) x : Q)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv M S Q) : S →+* Q) (algebraMap R S) : (a : R) → Q)
        x :
      Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x : A
⊢ (RingEquiv.toEquiv (ringEquivOfRingEquiv S Q h.toRingEquiv H)).toFun ((algebraMap A S : (a : A) → S) x) =
    (algebraMap A Q : (a : A) → Q) x
have dsimp : Eq.{u_8 + 1} (α := Q) ((map Q (↑h : R →+* P) sorry : (a : S) → Q) ((algebraMap A S : (a : A) → S) x : S) : Q)
  ((algebraMap A Q : (a : A) → Q) x : Q)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x : A
⊢ Eq.{u_8 + 1} (α := Q) ((map Q (↑h : R →+* P) ⋯ : (a : S) → Q) ((algebraMap A S : (a : A) → S) x : S) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
have rw : Eq.{u_8 + 1} (α := Q)
  ((map Q (↑h : R →+* P) sorry : (a : S) → Q) ((algebraMap R S : (a : R) → S) ((algebraMap A R : (a : A) → R) x : R) : S) :
    Q)
  ((algebraMap A Q : (a : A) → Q) x : Q)
Tactic: rw [IsScalarTower.algebraMap_apply A R S, map_eq,
    RingHom.coe_coe, AlgEquiv.commutes, IsScalarTower.algebraMap_apply A P Q]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x : A
rw :
  Eq.{u_8 + 1} (α := Q)
    ((map Q (↑h : R →+* P) ⋯ : (a : S) → Q)
        ((algebraMap R S : (a : R) → S) ((algebraMap A R : (a : A) → R) x : R) : S) :
      Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
⊢ Eq.{u_8 + 1} (α := Q) ((map Q (↑h : R →+* P) ⋯ : (a : S) → Q) ((algebraMap A S : (a : A) → S) x : S) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
have rw₁ : Eq.{u_8 + 1} (α := Q)
  ((algebraMap P Q : (a : P) → Q) (((↑h : R →+* P) : (a : R) → P) ((algebraMap A R : (a : A) → R) x : R) : P) : Q)
  ((algebraMap A Q : (a : A) → Q) x : Q)
Tactic: rw [IsScalarTower.algebraMap_apply A R S, map_eq,
    RingHom.coe_coe, AlgEquiv.commutes, IsScalarTower.algebraMap_apply A P Q]