awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
refine_1 :
  (∀ (x : ↥S),
      IsUnit.{u_3} (M := Module.End R Aₛ)
        ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
refine_2 :
  ∀ (x : Aₛ),
    (∃ (x_1 : Prod.{u_2, u_1} A ↥S),
        x_1.2 • x = (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x_1.1) ↔
      ∃ (x_1 : A × ↥(Algebra.algebraMapSubmonoid A S)),
        HMul.hMul (β := Aₛ) x ((algebraMap A Aₛ : (a : A) → Aₛ) (↑x_1.2 : A) : Aₛ) =
          (algebraMap A Aₛ : (a : A) → Aₛ) x_1.1
⊢ ((∀ (x : ↥S),
        IsUnit.{u_3} (M := Module.End R Aₛ)
          ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ∧
      (∀ (y : Aₛ),
          ∃ (x : Prod.{u_2, u_1} A ↥S),
            x.2 • y = (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x.1) ∧
        ∀ {x₁ x₂ : A},
          Eq.{u_3 + 1} (α := Aₛ) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x₁ : Aₛ)
              ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x₂ : Aₛ) →
            ∃ (c : ↥S), c • x₁ = c • x₂) ↔
    (∀ (y : ↥(Algebra.algebraMapSubmonoid A S)),
        IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)) ∧
      (∀ (z : Aₛ),
          ∃ (x : A × ↥(Algebra.algebraMapSubmonoid A S)),
            HMul.hMul (β := Aₛ) z ((algebraMap A Aₛ : (a : A) → Aₛ) (↑x.2 : A) : Aₛ) =
              (algebraMap A Aₛ : (a : A) → Aₛ) x.1) ∧
        ∀ {x y : A},
          Eq.{u_3 + 1} (α := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x : Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) y : Aₛ) →
            ∃ (c : ↥(Algebra.algebraMapSubmonoid A S)), (↑c : A) * x = (↑c : A) * y
have refine_3 : ∀ (x x_1 : A),
  (Eq.{u_3 + 1} (α := Aₛ) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x : Aₛ)
        ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x_1 : Aₛ) →
      ∃ (c : ↥S), c • x = c • x_1) ↔
    Eq.{u_3 + 1} (α := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x : Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x_1 : Aₛ) →
      ∃ (c : ↥(Algebra.algebraMapSubmonoid A S)), (↑c : A) * x = (↑c : A) * x_1
Tactic: refine and_congr ?_ (and_congr (forall_congr' fun _ ↦ ?_) (forall₂_congr fun _ _ ↦ ?_))
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
⊢ (∀ (x : ↥S),
      IsUnit.{u_3} (M := Module.End R Aₛ)
        ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
have refine_1 : (∀ (x : ↥S),
    IsUnit (M := Module.End R Aₛ)
      ((Algebra.lmul R Aₛ : (a : Aₛ) → Module.End R Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ) :
        Module.End R Aₛ)) ↔
  ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
Tactic: simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall,
      Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map,
      Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
refine_1 :
  (∀ (x : ↥S),
      IsUnit (M := Module.End R Aₛ)
        ((Algebra.lmul R Aₛ : (a : Aₛ) → Module.End R Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ) :
          Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
⊢ (∀ (x : ↥S),
      IsUnit.{u_3} (M := Module.End R Aₛ)
        ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
have refine_1₁ : (∀ (x : ↥S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ)) ↔
  ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
Tactic: simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall,
      Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map,
      Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
refine_1 :
  (∀ (x : ↥S),
      IsUnit (M := Module.End R Aₛ)
        ((Algebra.lmul R Aₛ : (a : Aₛ) → Module.End R Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ) :
          Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
refine_1₁ :
  (∀ (x : ↥S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
⊢ (∀ (x : ↥S),
      IsUnit.{u_3} (M := Module.End R Aₛ)
        ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
have refine_1₂ : (∀ (a : R) (b : a ∈ S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
  ∀ (a : A) (b : Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) a),
    IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
Tactic: simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall,
      Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map,
      Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
refine_1 :
  (∀ (x : ↥S),
      IsUnit (M := Module.End R Aₛ)
        ((Algebra.lmul R Aₛ : (a : Aₛ) → Module.End R Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ) :
          Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
refine_1₁ :
  (∀ (x : ↥S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
refine_1₂ :
  (∀ (a : R) (b : a ∈ S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ (a : A) (b : Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) a),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
⊢ (∀ (x : ↥S),
      IsUnit.{u_3} (M := Module.End R Aₛ)
        ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
have refine_1₃ : (∀ (a : R) (b : a ∈ S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
  ∀ (a : A) (b : Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) S) a),
    IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
Tactic: simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall,
      Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map,
      Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
refine_1 :
  (∀ (x : ↥S),
      IsUnit (M := Module.End R Aₛ)
        ((Algebra.lmul R Aₛ : (a : Aₛ) → Module.End R Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ) :
          Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
refine_1₁ :
  (∀ (x : ↥S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
refine_1₂ :
  (∀ (a : R) (b : a ∈ S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ (a : A) (b : Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) a),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
refine_1₃ :
  (∀ (a : R) (b : a ∈ S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ (a : A) (b : Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) S) a),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
⊢ (∀ (x : ↥S),
      IsUnit.{u_3} (M := Module.End R Aₛ)
        ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
have refine_1₄ : (∀ (a : R) (b : a ∈ (↑S : Set R)), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
  ∀ (a : A) (b : a ∈ (↑(Submonoid.map (F := R →+* A) (algebraMap R A) S) : Set A)),
    IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
Tactic: simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall,
      Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map,
      Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
refine_1 :
  (∀ (x : ↥S),
      IsUnit (M := Module.End R Aₛ)
        ((Algebra.lmul R Aₛ : (a : Aₛ) → Module.End R Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ) :
          Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
refine_1₁ :
  (∀ (x : ↥S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
refine_1₂ :
  (∀ (a : R) (b : a ∈ S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ (a : A) (b : Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) a),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
refine_1₃ :
  (∀ (a : R) (b : a ∈ S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ (a : A) (b : Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) S) a),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
refine_1₄ :
  (∀ (a : R) (b : a ∈ (↑S : Set R)), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ (a : A) (b : a ∈ (↑(Submonoid.map (F := R →+* A) (algebraMap R A) S) : Set A)),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
⊢ (∀ (x : ↥S),
      IsUnit.{u_3} (M := Module.End R Aₛ)
        ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
have refine_1₅ : (∀ (a : R) (b : a ∈ (↑S : Set R)), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
  ∀ (a : A) (b : Membership.mem (γ := Set A) ((⇑(algebraMap R A) : (a : R) → A) '' (↑S : Set R)) a),
    IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
Tactic: simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall,
      Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map,
      Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
refine_1 :
  (∀ (x : ↥S),
      IsUnit (M := Module.End R Aₛ)
        ((Algebra.lmul R Aₛ : (a : Aₛ) → Module.End R Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ) :
          Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
refine_1₁ :
  (∀ (x : ↥S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) (↑x : R) : Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
refine_1₂ :
  (∀ (a : R) (b : a ∈ S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ (a : A) (b : Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) a),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
refine_1₃ :
  (∀ (a : R) (b : a ∈ S), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ (a : A) (b : Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) S) a),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
refine_1₄ :
  (∀ (a : R) (b : a ∈ (↑S : Set R)), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ (a : A) (b : a ∈ (↑(Submonoid.map (F := R →+* A) (algebraMap R A) S) : Set A)),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
refine_1₅ :
  (∀ (a : R) (b : a ∈ (↑S : Set R)), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
    ∀ (a : A) (b : Membership.mem (γ := Set A) ((⇑(algebraMap R A) : (a : R) → A) '' (↑S : Set R)) a),
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) a : Aₛ)
⊢ (∀ (x : ↥S),
      IsUnit.{u_3} (M := Module.End R Aₛ)
        ((algebraMap R (Module.End R Aₛ) : (a : R) → Module.End R Aₛ) (↑x : R) : Module.End R Aₛ)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) (↑y : A) : Aₛ)
have refine_1₆ : (∀ (a : R) (b : a ∈ (↑S : Set R)), IsUnit.{u_3} (M := Aₛ) ((algebraMap R Aₛ : (a : R) → Aₛ) a : Aₛ)) ↔
  ∀ ⦃x : R⦄,
    x ∈ (↑S : Set R) →
      IsUnit.{u_3} (M := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) ((algebraMap R A : (a : R) → A) x : A) : Aₛ)
Tactic: simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall,
      Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map,
      Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
x : Aₛ
⊢ (∃ (x_1 : Prod.{u_2, u_1} A ↥S),
      x_1.2 • x = (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x_1.1) ↔
    ∃ (x_1 : A × ↥(Algebra.algebraMapSubmonoid A S)),
      HMul.hMul (β := Aₛ) x ((algebraMap A Aₛ : (a : A) → Aₛ) (↑x_1.2 : A) : Aₛ) =
        (algebraMap A Aₛ : (a : A) → Aₛ) x_1.1
have refine_2 : (∃ (a : A) (a_1 : R) (b : a_1 ∈ S),
    Subtype.mk (p := fun (a : R) ↦ a ∈ S) a_1 b • x =
      (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) a) ↔
  ∃ (a : A) (a_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) S) a_1),
    HMul.hMul (β := Aₛ) x ((algebraMap A Aₛ : (a : A) → Aₛ) a_1 : Aₛ) = (algebraMap A Aₛ : (a : A) → Aₛ) a
Tactic: simp_rw [Prod.exists, Subtype.exists, Algebra.algebraMapSubmonoid]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
x x_1 : A
⊢ (Eq.{u_3 + 1} (α := Aₛ) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x : Aₛ)
        ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x_1 : Aₛ) →
      ∃ (c : ↥S), c • x = c • x_1) ↔
    Eq.{u_3 + 1} (α := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x : Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x_1 : Aₛ) →
      ∃ (c : ↥(Algebra.algebraMapSubmonoid A S)), (↑c : A) * x = (↑c : A) * x_1
have refine_3 : (Eq.{u_3 + 1} (α := Aₛ) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x : Aₛ)
      ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x_1 : Aₛ) →
    ∃ (a : R) (b : a ∈ S),
      Subtype.mk (p := fun (a : R) ↦ a ∈ S) a b • x = Subtype.mk (p := fun (a : R) ↦ a ∈ S) a b • x_1) ↔
  Eq.{u_3 + 1} (α := Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x : Aₛ) ((algebraMap A Aₛ : (a : A) → Aₛ) x_1 : Aₛ) →
    ∃ (a : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) S) a),
      a * x = a * x_1
Tactic: simp_rw [Subtype.exists, Algebra.algebraMapSubmonoid]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
⊢ IsLocalizedModule S (Algebra.linearMap R A) ↔ IsLocalization S A
have h : S = Algebra.algebraMapSubmonoid R S
Tactic: convert! isLocalizedModule_iff_isLocalization (S := S) (A := R) (Aₛ := A)
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommSemiring Aₛ
inst_4 : Algebra A Aₛ
inst_5 : Algebra R Aₛ
inst_6 : IsScalarTower R A Aₛ
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
x : A
s : ↥S
⊢ mk' (M := Algebra.algebraMapSubmonoid A S) Aₛ x
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) x)
        ((algebraMap R A : (a : R) → A) (↑s : R)) ⋯) =
    IsLocalizedModule.mk' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ)) x s
have rw : HSMul.hSMul.{u_2, u_3, u_3} (α := A) ((algebraMap R A : (a : R) → A) (↑s : R) : A)
    (mk' (M := Algebra.algebraMapSubmonoid A S) Aₛ x
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) x)
        ((algebraMap R A : (a : R) → A) (↑s : R)) sorry)) =
  (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ) : (a : A) → Aₛ) x
Tactic: rw [← IsLocalizedModule.smul_inj (IsScalarTower.toAlgHom R A Aₛ).toLinearMap s,
    IsLocalizedModule.mk'_cancel', Submonoid.smul_def, ← algebraMap_smul A]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.IsLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
x : R
s : ↥S
⊢ mk' A x s = IsLocalizedModule.mk' (Algebra.linearMap R A) x s
have rw : s • mk' A x s = (Algebra.linearMap R A : (a : R) → A) x
Tactic: rw [← IsLocalizedModule.smul_inj (Algebra.linearMap R A) s, IsLocalizedModule.mk'_cancel']
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x y : N
h : Membership.mem (γ := Set N) {x : N | ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x} x
h_1 : Membership.mem (γ := Set N) {x : N | ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x} y
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
n : M
hn : n ∈ M'
t : ↥p
hy : IsLocalizedModule.mk' f n t = y
⊢ IsLocalizedModule.mk' f (t • m + s • n) (s * t) = x + y
have rw : IsLocalizedModule.mk' f (t • m + s • n) (s * t) = IsLocalizedModule.mk' f m s + y
Tactic: rw [← hx, ← hy, IsLocalizedModule.mk'_add_mk']
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x y : N
h : Membership.mem (γ := Set N) {x : N | ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x} x
h_1 : Membership.mem (γ := Set N) {x : N | ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x} y
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
n : M
hn : n ∈ M'
t : ↥p
hy : IsLocalizedModule.mk' f n t = y
rw : IsLocalizedModule.mk' f (t • m + s • n) (s * t) = IsLocalizedModule.mk' f m s + y
⊢ IsLocalizedModule.mk' f (t • m + s • n) (s * t) = x + y
have rw₁ : IsLocalizedModule.mk' f (t • m + s • n) (s * t) = IsLocalizedModule.mk' f m s + IsLocalizedModule.mk' f n t
Tactic: rw [← hx, ← hy, IsLocalizedModule.mk'_add_mk']
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x y : N
h : Membership.mem (γ := Set N) {x : N | ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x} x
h_1 : Membership.mem (γ := Set N) {x : N | ∃ m ∈ M', ∃ (s : ↥p), IsLocalizedModule.mk' f m s = x} y
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
n : M
hn : n ∈ M'
t : ↥p
hy : IsLocalizedModule.mk' f n t = y
rw : IsLocalizedModule.mk' f (t • m + s • n) (s * t) = IsLocalizedModule.mk' f m s + y
rw₁ : IsLocalizedModule.mk' f (t • m + s • n) (s * t) = IsLocalizedModule.mk' f m s + IsLocalizedModule.mk' f n t
⊢ IsLocalizedModule.mk' f (t • m + s • n) (s * t) = x + y
have rw₂ : IsLocalizedModule.mk' f (t • m + s • n) (s * t) = IsLocalizedModule.mk' f (t • m + s • n) (s * t)
Tactic: rw [← hx, ← hy, IsLocalizedModule.mk'_add_mk']