awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
S_1 : Submonoid R_1
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R_1 P
R₁ : Type u_3
inst_3 : CommRing R₁
K_1 : Type u_4
inst_4 : Field K_1
inst_5 : Algebra R₁ K_1
inst_6 : IsFractionRing R₁ K_1
inst_7 : IsDomain R₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst_8 : CommRing R
inst_9 : IsDomain R
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : CommRing K
inst_13 : CommRing L
inst_14 : Algebra R K
inst_15 : Algebra S L
inst_16 : IsFractionRing R K
inst_17 : IsFractionRing S L
f : R ≃+* S
I J : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
⊢ Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L)
      ((↑I : Submodule R K) * (↑J : Submodule R K)) ≤
    HMul.hMul (α := Submodule S L)
      (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K))
      (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑J : Submodule R K))
have a : ∀ m ∈ I,
  ∀ n ∈ J,
    HMul.hMul (α := L) (β := L) ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) m : L)
        ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) n : L) ∈
      HMul.hMul (α := Submodule S L)
        (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K))
        (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑J : Submodule R K))
Tactic: simp only [map_le_iff_le_comap, Submodule.mul_le, mem_coe, mem_comap,
          semilinearEquivOfRingEquiv_apply, map_mul, mem_map_equiv,
          semilinearEquivOfRingEquiv_symm_apply, LinearEquiv.coe_coe]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
S_1 : Submonoid R_1
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R_1 P
R₁ : Type u_3
inst_3 : CommRing R₁
K_1 : Type u_4
inst_4 : Field K_1
inst_5 : Algebra R₁ K_1
inst_6 : IsFractionRing R₁ K_1
inst_7 : IsDomain R₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst_8 : CommRing R
inst_9 : IsDomain R
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : CommRing K
inst_13 : CommRing L
inst_14 : Algebra R K
inst_15 : Algebra S L
inst_16 : IsFractionRing R K
inst_17 : IsFractionRing S L
f : R ≃+* S
I J : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
⊢ HMul.hMul (α := Submodule S L)
      (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K))
      (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑J : Submodule R K)) ≤
    Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L)
      ((↑I : Submodule R K) * (↑J : Submodule R K))
have a : ∀ (m : L),
  Membership.mem (α := K) I ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) m : K) →
    ∀ (n : L),
      Membership.mem (α := K) J ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) n : K) →
        HMul.hMul (α := K) (β := K) ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) m : K)
            ((RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f) : (a : L) → K) n : K) ∈
          (↑I : Submodule R K) * (↑J : Submodule R K)
Tactic: simp only [map_le_iff_le_comap, Submodule.mul_le, mem_coe, mem_comap,
          semilinearEquivOfRingEquiv_apply, map_mul, mem_map_equiv,
          semilinearEquivOfRingEquiv_symm_apply, LinearEquiv.coe_coe]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
S_1 : Submonoid R_1
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R_1 P
R₁ : Type u_3
inst_3 : CommRing R₁
K_1 : Type u_4
inst_4 : Field K_1
inst_5 : Algebra R₁ K_1
inst_6 : IsFractionRing R₁ K_1
inst_7 : IsDomain R₁
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst_8 : CommRing R
inst_9 : IsDomain R
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : CommRing K
inst_13 : CommRing L
inst_14 : Algebra R K
inst_15 : Algebra S L
inst_16 : IsFractionRing R K
inst_17 : IsFractionRing S L
f : R ≃+* S
I J : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
⊢ Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
      (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑(I + J) : Submodule R K)) ⋯ =
    HAdd.hAdd (α := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
      (Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
        (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K)) ⋯)
      (Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
        (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑J : Submodule R K)) ⋯)
have a : ∀ (x : L),
  Membership.mem (γ := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
      (Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
        (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑(I + J) : Submodule R K)) sorry)
      x ↔
    x ∈
      HAdd.hAdd (α := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
        (Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
          (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑I : Submodule R K)) sorry)
        (Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
          (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (↑J : Submodule R K)) sorry)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
T : Type u_9
inst_10 : CommRing T
inst_11 : IsDomain T
M : Type u_10
inst_12 : CommRing M
inst_13 : Algebra T M
inst_14 : IsFractionRing T M
f : R ≃+* S
g : S ≃+* T
⊢ Eq (α := RingEquiv.{u_7, u_10} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K) (FractionalIdeal.{u_9, u_10} (R := T) T⁰ M))
    (ringEquivOfRingEquiv K M (f.trans g))
    (RingEquiv.trans (S := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L) (ringEquivOfRingEquiv K L f)
      (ringEquivOfRingEquiv L M g))
have this : RingHomCompTriple (↑f : R →+* S) (↑g : S →+* T) (↑(f.trans g) : R →+* T)
Tactic: have : RingHomCompTriple f (g : S →+* T) (f.trans g : R →+* T) := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
T : Type u_9
inst_10 : CommRing T
inst_11 : IsDomain T
M : Type u_10
inst_12 : CommRing M
inst_13 : Algebra T M
inst_14 : IsFractionRing T M
f : R ≃+* S
g : S ≃+* T
this : RingHomCompTriple (↑f : R →+* S) (↑g : S →+* T) (↑(f.trans g) : R →+* T)
⊢ Eq (α := RingEquiv.{u_7, u_10} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K) (FractionalIdeal.{u_9, u_10} (R := T) T⁰ M))
    (ringEquivOfRingEquiv K M (f.trans g))
    (RingEquiv.trans (S := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L) (ringEquivOfRingEquiv K L f)
      (ringEquivOfRingEquiv L M g))
have h : ∀ (I : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K),
  Eq.{u_10 + 1} (α := FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)
    (((ringEquivOfRingEquiv K M (f.trans g) :
            RingEquiv.{u_7, u_10} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
              (FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)) :
          (a : FractionalIdeal R⁰ K) → FractionalIdeal T⁰ M)
        I :
      FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)
    (((RingEquiv.trans (S := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L) (ringEquivOfRingEquiv K L f)
              (ringEquivOfRingEquiv L M g) :
            RingEquiv.{u_7, u_10} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
              (FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)) :
          (a : FractionalIdeal R⁰ K) → FractionalIdeal T⁰ M)
        I :
      FractionalIdeal.{u_9, u_10} (R := T) T⁰ M)
Tactic: ext1 I
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
K : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
⊢ Eq (α := FractionalIdeal.{u_5, u_7} (R := R) R⁰ K ≃+* FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
    (ringEquivOfRingEquiv K K (RingEquiv.refl R)) (RingEquiv.refl (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K))
have h : ∀ (I : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K) (x : K),
  Membership.mem (γ := FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
      ((ringEquivOfRingEquiv K K (RingEquiv.refl R) : (a : FractionalIdeal R⁰ K) → FractionalIdeal R⁰ K) I :
        FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
      x ↔
    Membership.mem (γ := FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
      ((RingEquiv.refl (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K) : (a : FractionalIdeal R⁰ K) → FractionalIdeal R⁰ K)
          I :
        FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
      x
Tactic: ext I x
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
K : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
I : FractionalIdeal.{u_5, u_7} (R := R) R⁰ K
x : K
⊢ Membership.mem (γ := FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
      ((ringEquivOfRingEquiv K K (RingEquiv.refl R) : (a : FractionalIdeal R⁰ K) → FractionalIdeal R⁰ K) I :
        FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
      x ↔
    Membership.mem (γ := FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
      ((RingEquiv.refl (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K) : (a : FractionalIdeal R⁰ K) → FractionalIdeal R⁰ K)
          I :
        FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
      x
have h : Membership.mem (γ := Submodule R K)
    (↑(Subtype.mk (p := fun (I : Submodule R K) ↦ IsFractional R⁰ I)
          (Submodule.map (↑(semilinearEquivOfRingEquiv K K (RingEquiv.refl R)) : K →ₗ[R] K) (↑I : Submodule R K)) sorry) :
      Submodule R K)
    x ↔
  x ∈ (↑I : Submodule R K)
Tactic: simp only [ringEquivOfRingEquiv_apply, RingEquiv.coe_ringHom_refl, RingEquiv.symm_refl,
    val_eq_coe, RingEquiv.refl_apply, ← mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
x : K
⊢ Eq.{u_8 + 1} (α := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
    (((ringEquivOfRingEquiv K L f :
            RingEquiv.{u_7, u_8} (FractionalIdeal.{u_5, u_7} (R := R) R⁰ K)
              (FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)) :
          (a : FractionalIdeal R⁰ K) → FractionalIdeal S⁰ L)
        (spanSingleton R⁰ x) :
      FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
    (spanSingleton S⁰ ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) x) :
      FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
have simp : Eq (α := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
  (Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
    (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (R ∙ x)) sorry)
  (spanSingleton S⁰ ((IsLocalization.map L (↑f : R →+* S) sorry : (a : K) → L) x))
Tactic: simp only [ringEquivOfRingEquiv, val_eq_coe, RingEquiv.symm_symm, RingEquiv.coe_mk,
    Equiv.coe_fn_mk, coe_spanSingleton, IsFractionRing.ringEquivOfRingEquiv_apply]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
x : K
⊢ Eq (α := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
    (Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
      (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (R ∙ x)) ⋯)
    (spanSingleton S⁰ ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x))
have rw : ∀ (x_1 : L),
  Membership.mem (γ := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
      (Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
        (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (R ∙ x)) sorry)
      x_1 ↔
    Membership.mem (γ := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
      (spanSingleton S⁰ ((IsLocalization.map L (↑f : R →+* S) sorry : (a : K) → L) x) :
        FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
      x_1
Tactic: rw [SetLike.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
x : K
y : L
⊢ Membership.mem (γ := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
      (Subtype.mk (p := fun (I : Submodule S L) ↦ IsFractional S⁰ I)
        (Submodule.map (↑(semilinearEquivOfRingEquiv K L f) : K →ₛₗ[(↑f : R →+* S)] L) (R ∙ x)) ⋯)
      y ↔
    Membership.mem (γ := FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
      (spanSingleton S⁰ ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x) :
        FractionalIdeal.{u_6, u_8} (R := S) S⁰ L)
      y
have simp : (∃ (a : R), (semilinearEquivOfRingEquiv K L f : (a : K) → L) (a • x) = y) ↔
  ∃ (a : S), HSMul.hSMul (β := L) a ((IsLocalization.map L (↑f : R →+* S) sorry : (a : K) → L) x : L) = y
Tactic: simp only [← FractionalIdeal.mem_coe, coe_mk, mem_map_equiv, coe_spanSingleton,
    Submodule.mem_span_singleton, (semilinearEquivOfRingEquiv K L f).eq_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
x : K
y : L
⊢ (∃ (a : R), (semilinearEquivOfRingEquiv K L f : (a : K) → L) (a • x) = y) ↔
    ∃ (a : S), HSMul.hSMul (β := L) a ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L) = y
have mp : (∃ (a : R), (semilinearEquivOfRingEquiv K L f : (a : K) → L) (a • x) = y) →
  ∃ (a : S), HSMul.hSMul (β := L) a ((IsLocalization.map L (↑f : R →+* S) sorry : (a : K) → L) x : L) = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
x : K
y : L
mp :
  (∃ (a : R), (semilinearEquivOfRingEquiv K L f : (a : K) → L) (a • x) = y) →
    ∃ (a : S), HSMul.hSMul (β := L) a ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L) = y
⊢ (∃ (a : R), (semilinearEquivOfRingEquiv K L f : (a : K) → L) (a • x) = y) ↔
    ∃ (a : S), HSMul.hSMul (β := L) a ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L) = y
have mpr : (∃ (a : S), HSMul.hSMul (β := L) a ((IsLocalization.map L (↑f : R →+* S) sorry : (a : K) → L) x : L) = y) →
  ∃ (a : R), (semilinearEquivOfRingEquiv K L f : (a : K) → L) (a • x) = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
x : K
r : R
⊢ ∃ (a : S),
    HSMul.hSMul (β := L) a ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L) =
      (semilinearEquivOfRingEquiv K L f : (a : K) → L) (r • x)
have h : HSMul.hSMul.{u_6, u_8, u_8} (α := S) (β := L) ((f : (a : R) → S) r : S)
    ((IsLocalization.map L (↑f : R →+* S) sorry : (a : K) → L) x : L) =
  (semilinearEquivOfRingEquiv K L f : (a : K) → L) (r • x)
Tactic: use f r
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : CommRing K
inst_5 : CommRing L
inst_6 : Algebra R K
inst_7 : Algebra S L
inst_8 : IsFractionRing R K
inst_9 : IsFractionRing S L
f : R ≃+* S
x : K
s : S
⊢ ∃ (a : R),
    (semilinearEquivOfRingEquiv K L f : (a : K) → L) (a • x) =
      HSMul.hSMul (β := L) s ((IsLocalization.map L (↑f : R →+* S) ⋯ : (a : K) → L) x : L)
have h : (semilinearEquivOfRingEquiv K L f : (a : K) → L)
    (HSMul.hSMul.{u_5, u_7, u_7} (α := R) ((f.symm : (a : S) → R) s : R) x) =
  HSMul.hSMul (β := L) s ((IsLocalization.map L (↑f : R →+* S) sorry : (a : K) → L) x : L)
Tactic: use f.symm s
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
a : α
m : Multiset α
⊢ FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) (a ::ₘ m)) =
    HMul.hMul (β := FreeAbelianGroup (Multiplicative (Multiset α))) (of a)
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
have rw : FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) ({a} + m)) =
  HMul.hMul (β := FreeAbelianGroup (Multiplicative (Multiset α))) (of a)
    (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
      FreeAbelianGroup (Multiplicative (Multiset α)))
Tactic: rw [← Multiset.singleton_add, ofAdd_add,
    of, FreeAbelianGroup.of_mul_of]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
a : α
m : Multiset α
rw :
  FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) ({a} + m)) =
    HMul.hMul (β := FreeAbelianGroup (Multiplicative (Multiset α))) (of a)
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
⊢ FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) (a ::ₘ m)) =
    HMul.hMul (β := FreeAbelianGroup (Multiplicative (Multiset α))) (of a)
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
have rw₁ : FreeAbelianGroup.of
    (HMul.hMul (α := Multiplicative (Multiset α)) (β := Multiplicative (Multiset α))
      ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) {a} : Multiplicative (Multiset α))
      ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m : Multiplicative (Multiset α))) =
  HMul.hMul (β := FreeAbelianGroup (Multiplicative (Multiset α))) (of a)
    (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
      FreeAbelianGroup (Multiplicative (Multiset α)))
Tactic: rw [← Multiset.singleton_add, ofAdd_add,
    of, FreeAbelianGroup.of_mul_of]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
a : α
m : Multiset α
rw :
  FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) ({a} + m)) =
    HMul.hMul (β := FreeAbelianGroup (Multiplicative (Multiset α))) (of a)
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
rw₁ :
  FreeAbelianGroup.of
      (HMul.hMul (α := Multiplicative (Multiset α)) (β := Multiplicative (Multiset α))
        ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) {a} : Multiplicative (Multiset α))
        ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m : Multiplicative (Multiset α))) =
    HMul.hMul (β := FreeAbelianGroup (Multiplicative (Multiset α))) (of a)
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
⊢ FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) (a ::ₘ m)) =
    HMul.hMul (β := FreeAbelianGroup (Multiplicative (Multiset α))) (of a)
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
have rw₂ : FreeAbelianGroup.of
    (HMul.hMul (α := Multiplicative (Multiset α)) (β := Multiplicative (Multiset α))
      ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) {a} : Multiplicative (Multiset α))
      ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m : Multiplicative (Multiset α))) =
  HMul.hMul (α := FreeAbelianGroup (Multiplicative (Multiset α))) (β := FreeAbelianGroup (Multiplicative (Multiset α)))
    (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) {a}) :
      FreeAbelianGroup (Multiplicative (Multiset α)))
    (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
      FreeAbelianGroup (Multiplicative (Multiset α)))
Tactic: rw [← Multiset.singleton_add, ofAdd_add,
    of, FreeAbelianGroup.of_mul_of]