awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
K' : Type u_5
inst_5 : Field K'
inst_6 : Algebra R₁ K'
inst_7 : IsFractionRing R₁ K'
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : K ≃ₐ[R₁] K'
⊢ map (↑h : K →ₐ[R₁] K') (I / J) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') J
have pos : ∀ (H : J = 0), map (↑h : K →ₐ[R₁] K') (I / J) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') J
Tactic: by_cases H : J = 0
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
K' : Type u_5
inst_5 : Field K'
inst_6 : Algebra R₁ K'
inst_7 : IsFractionRing R₁ K'
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : K ≃ₐ[R₁] K'
pos : ∀ (H : J = 0), map (↑h : K →ₐ[R₁] K') (I / J) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') J
⊢ map (↑h : K →ₐ[R₁] K') (I / J) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') J
have neg : ∀ (H : ¬J = 0), map (↑h : K →ₐ[R₁] K') (I / J) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') J
Tactic: by_cases H : J = 0
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
K' : Type u_5
inst_5 : Field K'
inst_6 : Algebra R₁ K'
inst_7 : IsFractionRing R₁ K'
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : K ≃ₐ[R₁] K'
H : J = 0
⊢ map (↑h : K →ₐ[R₁] K') (I / J) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') J
have pos : map (↑h : K →ₐ[R₁] K') (I / 0) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') 0
Tactic: rw [H, div_zero, FractionalIdeal.map_zero, div_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
K' : Type u_5
inst_5 : Field K'
inst_6 : Algebra R₁ K'
inst_7 : IsFractionRing R₁ K'
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : K ≃ₐ[R₁] K'
H : J = 0
pos : map (↑h : K →ₐ[R₁] K') (I / 0) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') 0
⊢ map (↑h : K →ₐ[R₁] K') (I / J) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') J
have pos₁ : map (↑h : K →ₐ[R₁] K') 0 = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') 0
Tactic: rw [H, div_zero, FractionalIdeal.map_zero, div_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
K' : Type u_5
inst_5 : Field K'
inst_6 : Algebra R₁ K'
inst_7 : IsFractionRing R₁ K'
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : K ≃ₐ[R₁] K'
H : J = 0
pos : map (↑h : K →ₐ[R₁] K') (I / 0) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') 0
pos₁ : map (↑h : K →ₐ[R₁] K') 0 = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') 0
⊢ map (↑h : K →ₐ[R₁] K') (I / J) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') J
have pos₂ : 0 = map (↑h : K →ₐ[R₁] K') I / 0
Tactic: rw [H, div_zero, FractionalIdeal.map_zero, div_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
K' : Type u_5
inst_5 : Field K'
inst_6 : Algebra R₁ K'
inst_7 : IsFractionRing R₁ K'
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : K ≃ₐ[R₁] K'
H : J = 0
pos : map (↑h : K →ₐ[R₁] K') (I / 0) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') 0
pos₁ : map (↑h : K →ₐ[R₁] K') 0 = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') 0
pos₂ : 0 = map (↑h : K →ₐ[R₁] K') I / 0
⊢ map (↑h : K →ₐ[R₁] K') (I / J) = map (↑h : K →ₐ[R₁] K') I / map (↑h : K →ₐ[R₁] K') J
have pos₃ : Eq.{u_5 + 1} (α := FractionalIdeal.{u_3, u_5} (R := R₁) R₁⁰ K') 0 0
Tactic: rw [H, div_zero, FractionalIdeal.map_zero, div_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
K' : Type u_5
inst_5 : Field K'
inst_6 : Algebra R₁ K'
inst_7 : IsFractionRing R₁ K'
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : K ≃ₐ[R₁] K'
⊢ map (↑h : K →ₐ[R₁] K') (1 / I) = 1 / map (↑h : K →ₐ[R₁] K') I
have rw : map (↑h : K →ₐ[R₁] K') 1 / map (↑h : K →ₐ[R₁] K') I = 1 / map (↑h : K →ₐ[R₁] K') I
Tactic: rw [FractionalIdeal.map_div, FractionalIdeal.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
K' : Type u_5
inst_5 : Field K'
inst_6 : Algebra R₁ K'
inst_7 : IsFractionRing R₁ K'
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : K ≃ₐ[R₁] K'
rw : map (↑h : K →ₐ[R₁] K') 1 / map (↑h : K →ₐ[R₁] K') I = 1 / map (↑h : K →ₐ[R₁] K') I
⊢ map (↑h : K →ₐ[R₁] K') (1 / I) = 1 / map (↑h : K →ₐ[R₁] K') I
have rw₁ : 1 / map (↑h : K →ₐ[R₁] K') I = 1 / map (↑h : K →ₐ[R₁] K') I
Tactic: rw [FractionalIdeal.map_div, FractionalIdeal.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
⊢ I = 0 ∨ I = 1
have rw : ¬I = 0 → I = 1
Tactic: rw [or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
⊢ I = 1
have simp_rw : ∀ (x : L), x ∈ I ↔ ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = x
Tactic: simp_rw [@SetLike.ext_iff _ _ _ I 1, mem_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
x : L
⊢ x ∈ I ↔ ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = x
have mp : x ∈ I → ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
x : L
mp : x ∈ I → ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = x
⊢ x ∈ I ↔ ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = x
have mpr : (∃ (x' : K), (algebraMap K L : (a : K) → L) x' = x) → x ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
x : L
x_mem : x ∈ I
⊢ ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = x
have mp : ∀ (n : K) (d : ↥(K⁰ : Submonoid K)) (x_mem : mk' L n d ∈ I), ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = mk' L n d
Tactic: obtain ⟨n, d, rfl⟩ := IsLocalization.exists_mk'_eq K⁰ x
Cleared hypotheses: x, x_mem
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
n : K
d : ↥(K⁰ : Submonoid K)
x_mem : mk' L n d ∈ I
⊢ ∃ (x' : K), (algebraMap K L : (a : K) → L) x' = mk' L n d
have mp : (algebraMap K L : (a : K) → L) (n / (↑d : K)) = mk' L n d
Tactic: refine ⟨n / d, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
n : K
d : ↥(K⁰ : Submonoid K)
x_mem : mk' L n d ∈ I
⊢ (algebraMap K L : (a : K) → L) (n / (↑d : K)) = mk' L n d
have mp : HDiv.hDiv (α := L) (β := L) ((algebraMap K L : (a : K) → L) n : L) ((algebraMap K L : (a : K) → L) (↑d : K) : L) =
  mk' L n d
Tactic: rw [map_div₀, IsFractionRing.mk'_eq_div]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
n : K
d : ↥(K⁰ : Submonoid K)
x_mem : mk' L n d ∈ I
mp :
  HDiv.hDiv (α := L) (β := L) ((algebraMap K L : (a : K) → L) n : L) ((algebraMap K L : (a : K) → L) (↑d : K) : L) =
    mk' L n d
⊢ (algebraMap K L : (a : K) → L) (n / (↑d : K)) = mk' L n d
have mp₁ : HDiv.hDiv (α := L) (β := L) ((algebraMap K L : (a : K) → L) n : L) ((algebraMap K L : (a : K) → L) (↑d : K) : L) =
  HDiv.hDiv (α := L) (β := L) ((algebraMap K L : (a : K) → L) n : L) ((algebraMap K L : (a : K) → L) (↑d : K) : L)
Tactic: rw [map_div₀, IsFractionRing.mk'_eq_div]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
x : K
⊢ Membership.mem (α := L) I ((algebraMap K L : (a : K) → L) x : L)
have mpr : ∀ (y : K) (y_ne : y ≠ 0) (y_mem : Membership.mem (α := L) I ((algebraMap K L : (a : K) → L) y : L)),
  Membership.mem (α := L) I ((algebraMap K L : (a : K) → L) x : L)
Tactic: obtain ⟨y, y_ne, y_mem⟩ := exists_ne_zero_mem_isInteger hI
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsFractionRing K L
I : FractionalIdeal.{u_4, u_5} (R := K) K⁰ L
hI : ¬I = 0
x y : K
y_ne : y ≠ 0
y_mem : Membership.mem (α := L) I ((algebraMap K L : (a : K) → L) y : L)
⊢ Membership.mem (α := L) I ((algebraMap K L : (a : K) → L) x : L)
have mpr : HSMul.hSMul (β := L) (x / y) ((algebraMap K L : (a : K) → L) y : L) ∈ I
Tactic: rw [← div_mul_cancel₀ x y_ne, map_mul, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
R₁ : Type u_3
inst_3 : CommRing R₁
K : Type u_4
inst_4 : Field K
inst_5 : Algebra R₁ K
inst_6 : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
⊢ IsFractional R₁⁰ (span R₁ (f '' (↑s : Set ι)))
have obtain : ∀ (a' : ↥(R₁⁰ : Submonoid R₁)) (ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)),
  IsFractional R₁⁰ (span R₁ (f '' (↑s : Set ι)))
Tactic: obtain ⟨a', ha'⟩ := IsLocalization.exist_integer_multiples R₁⁰ s f
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
R₁ : Type u_3
inst_3 : CommRing R₁
K : Type u_4
inst_4 : Field K
inst_5 : Algebra R₁ K
inst_6 : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
⊢ IsFractional R₁⁰ (span R₁ (f '' (↑s : Set ι)))
have refine_1 : ∀ (x : K) (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x) (x : K)
  (h : x ∈ f '' (↑s : Set ι)), IsInteger R₁ ((↑a' : R₁) • x)
Tactic: refine ⟨a', a'.2, fun x hx => Submodule.span_induction ?_ ?_ ?_ ?_ hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
R₁ : Type u_3
inst_3 : CommRing R₁
K : Type u_4
inst_4 : Field K
inst_5 : Algebra R₁ K
inst_6 : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
refine_1 :
  ∀ (x : K) (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x) (x : K)
    (h : x ∈ f '' (↑s : Set ι)), IsInteger R₁ ((↑a' : R₁) • x)
⊢ IsFractional R₁⁰ (span R₁ (f '' (↑s : Set ι)))
have refine_2 : ∀ (x : K) (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x),
  IsInteger R₁ (HSMul.hSMul (β := K) (↑a' : R₁) 0)
Tactic: refine ⟨a', a'.2, fun x hx => Submodule.span_induction ?_ ?_ ?_ ?_ hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
R₁ : Type u_3
inst_3 : CommRing R₁
K : Type u_4
inst_4 : Field K
inst_5 : Algebra R₁ K
inst_6 : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
refine_1 :
  ∀ (x : K) (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x) (x : K)
    (h : x ∈ f '' (↑s : Set ι)), IsInteger R₁ ((↑a' : R₁) • x)
refine_2 :
  ∀ (x : K) (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x),
    IsInteger R₁ (HSMul.hSMul (β := K) (↑a' : R₁) 0)
⊢ IsFractional R₁⁰ (span R₁ (f '' (↑s : Set ι)))
have refine_3 : ∀ (x : K) (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x) (x y : K)
  (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x)
  (hy : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) y),
  IsInteger R₁ ((↑a' : R₁) • x) → IsInteger R₁ ((↑a' : R₁) • y) → IsInteger R₁ ((↑a' : R₁) • (x + y))
Tactic: refine ⟨a', a'.2, fun x hx => Submodule.span_induction ?_ ?_ ?_ ?_ hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
R₁ : Type u_3
inst_3 : CommRing R₁
K : Type u_4
inst_4 : Field K
inst_5 : Algebra R₁ K
inst_6 : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
refine_1 :
  ∀ (x : K) (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x) (x : K)
    (h : x ∈ f '' (↑s : Set ι)), IsInteger R₁ ((↑a' : R₁) • x)
refine_2 :
  ∀ (x : K) (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x),
    IsInteger R₁ (HSMul.hSMul (β := K) (↑a' : R₁) 0)
refine_3 :
  ∀ (x : K) (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x) (x y : K)
    (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x)
    (hy : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) y),
    IsInteger R₁ ((↑a' : R₁) • x) → IsInteger R₁ ((↑a' : R₁) • y) → IsInteger R₁ ((↑a' : R₁) • (x + y))
⊢ IsFractional R₁⁰ (span R₁ (f '' (↑s : Set ι)))
have refine_4 : ∀ (x : K) (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x) (a : R₁) (x : K)
  (hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x),
  IsInteger R₁ ((↑a' : R₁) • x) → IsInteger R₁ ((↑a' : R₁) • a • x)
Tactic: refine ⟨a', a'.2, fun x hx => Submodule.span_induction ?_ ?_ ?_ ?_ hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
R₁ : Type u_3
inst_3 : CommRing R₁
K : Type u_4
inst_4 : Field K
inst_5 : Algebra R₁ K
inst_6 : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
x : K
hx : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
⊢ IsInteger R₁ (HSMul.hSMul (β := K) (↑a' : R₁) 0)
have refine_2 : IsInteger.{u_3, u_4} R₁ (S := K) 0
Tactic: rw [smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
R₁ : Type u_3
inst_3 : CommRing R₁
K : Type u_4
inst_4 : Field K
inst_5 : Algebra R₁ K
inst_6 : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
x_1 : K
hx_1 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x_1
x y : K
hx_2 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
hy_1 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) y
hx : IsInteger R₁ ((↑a' : R₁) • x)
hy : IsInteger R₁ ((↑a' : R₁) • y)
⊢ IsInteger R₁ ((↑a' : R₁) • (x + y))
have refine_3 : IsInteger R₁ ((↑a' : R₁) • x + (↑a' : R₁) • y)
Tactic: rw [smul_add]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
R₁ : Type u_3
inst_3 : CommRing R₁
K : Type u_4
inst_4 : Field K
inst_5 : Algebra R₁ K
inst_6 : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥(R₁⁰ : Submonoid R₁)
ha' : ∀ i ∈ s, IsInteger R₁ ((↑a' : R₁) • f i)
x_1 : K
hx_1 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x_1
c : R₁
x : K
hx_2 : Membership.mem (γ := Submodule R₁ K) (span R₁ (f '' (↑s : Set ι))) x
hx : IsInteger R₁ ((↑a' : R₁) • x)
⊢ IsInteger R₁ ((↑a' : R₁) • c • x)
have refine_4 : IsInteger R₁ (c • (↑a' : R₁) • x)
Tactic: rw [smul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x : P
⊢ Eq (α := Submodule R P) (↑(spanSingleton S x) : Submodule R P) (R ∙ x)
have rw : Eq (α := Submodule R P) (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ x) sorry) : Submodule R P)
  (R ∙ x)
Tactic: rw [spanSingleton]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y : P
⊢ Membership.mem (γ := FractionalIdeal S P) (spanSingleton S y) x ↔ ∃ (z : R), z • y = x
have rw : Membership.mem (γ := FractionalIdeal S P) (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ y) sorry) x ↔
  ∃ (z : R), z • y = x
Tactic: rw [spanSingleton]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
I : FractionalIdeal S P
⊢ HMul.hMul (α := FractionalIdeal S P)
      (spanSingleton S ((algebraMap R P : (a : R) → P) (↑I.den : R)) : FractionalIdeal S P) I =
    (↑I.num : FractionalIdeal S P)
have a : Eq.{u_2 + 1} (α := Submodule R P)
  ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P))
    (HMul.hMul (α := FractionalIdeal S P)
      (spanSingleton S ((algebraMap R P : (a : R) → P) (↑I.den : R)) : FractionalIdeal S P) I))
  ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P)) (↑I.num : FractionalIdeal S P))
Tactic: apply coeToSubmodule_injective
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
I : FractionalIdeal S P
⊢ (↑(HMul.hMul (α := FractionalIdeal S P)
          (spanSingleton S ((algebraMap R P : (a : R) → P) (↑I.den : R)) : FractionalIdeal S P) I) :
      Submodule R P) =
    (↑(↑I.num : FractionalIdeal S P) : Submodule R P)
have a : HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) (↑I : Submodule R P) =
  (↑(↑I.num : FractionalIdeal S P) : Submodule R P)
Tactic: rw [coe_mul, ← smul_eq_mul, coe_spanSingleton, smul_eq_mul, Submodule.span_singleton_mul]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
I : FractionalIdeal S P
⊢ HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) (↑I : Submodule R P) =
    (↑(↑I.num : FractionalIdeal S P) : Submodule R P)
have h : HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) (↑I : Submodule R P) =
  I.den • (↑I : Submodule R P)
Tactic: convert! I.den_mul_self_eq_num using 1
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
I : FractionalIdeal S P
⊢ HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) (↑I : Submodule R P) =
    I.den • (↑I : Submodule R P)
have h : ∀ (x : P),
  x ∈ HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) (↑I : Submodule R P) ↔
    x ∈ I.den • (↑I : Submodule R P)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
I : FractionalIdeal S P
x : P
⊢ x ∈ HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) (↑I : Submodule R P) ↔
    x ∈ I.den • (↑I : Submodule R P)
have h : (∃ b ∈ (↑I : Submodule R P), HSMul.hSMul (α := P) ((algebraMap R P : (a : R) → P) (↑I.den : R) : P) b = x) ↔
  ∃ b ∈ (↑I : Submodule R P), I.den • b = x
Tactic: rw [mem_smul_pointwise_iff_exists, mem_smul_pointwise_iff_exists]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x : P
I : FractionalIdeal S P
⊢ spanSingleton S x ≤ I ↔ x ∈ I
have rw : (↑(spanSingleton S x) : Submodule R P) ≤ (↑I : Submodule R P) ↔ x ∈ I
Tactic: rw [← coe_le_coe, coe_spanSingleton, Submodule.span_singleton_le_iff_mem, mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x : P
I : FractionalIdeal S P
rw : (↑(spanSingleton S x) : Submodule R P) ≤ (↑I : Submodule R P) ↔ x ∈ I
⊢ spanSingleton S x ≤ I ↔ x ∈ I
have rw₁ : R ∙ x ≤ (↑I : Submodule R P) ↔ x ∈ I
Tactic: rw [← coe_le_coe, coe_spanSingleton, Submodule.span_singleton_le_iff_mem, mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x : P
I : FractionalIdeal S P
rw : (↑(spanSingleton S x) : Submodule R P) ≤ (↑I : Submodule R P) ↔ x ∈ I
rw₁ : R ∙ x ≤ (↑I : Submodule R P) ↔ x ∈ I
⊢ spanSingleton S x ≤ I ↔ x ∈ I
have rw₂ : x ∈ (↑I : Submodule R P) ↔ x ∈ I
Tactic: rw [← coe_le_coe, coe_spanSingleton, Submodule.span_singleton_le_iff_mem, mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x : P
I : FractionalIdeal S P
rw : (↑(spanSingleton S x) : Submodule R P) ≤ (↑I : Submodule R P) ↔ x ∈ I
rw₁ : R ∙ x ≤ (↑I : Submodule R P) ↔ x ∈ I
rw₂ : x ∈ (↑I : Submodule R P) ↔ x ∈ I
⊢ spanSingleton S x ≤ I ↔ x ∈ I
have rw₃ : x ∈ I ↔ x ∈ I
Tactic: rw [← coe_le_coe, coe_spanSingleton, Submodule.span_singleton_le_iff_mem, mem_coe]