awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
x_1 : K
h :
  (∃ (b : K), Membership.mem (γ := Submodule R K) (↑(spanSingleton R⁰ x) : Submodule R K) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₁ :
  (∃ (b : K), Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₂ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₃ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (Algebra.linearMap R K : (a : R) → K) y = x_1
h₄ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
h₅ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ (↑d : R) • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
h₆ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ (↑d : R) • b = x_1) ↔
    ∃ (y : R), (∃ (a : R), a * r = y) ∧ (algebraMap R K : (a : R) → K) y = x_1
h₇ : (∃ (a : R), (↑d : R) • a • x = x_1) ↔ ∃ (a : R), (algebraMap R K : (a : R) → K) (a * r) = x_1
⊢ x_1 ∈ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
have h₈ : (∃ (a : R), (↑d : R) • a • x = x_1) ↔
  ∃ (a : R),
    HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) ((algebraMap R K : (a : R) → K) r : K) = x_1
Tactic: simp_rw [Submodule.mem_smul_pointwise_iff_exists, mem_coe, mem_spanSingleton, Submodule.mem_map,
      Algebra.linearMap_apply, Submonoid.smul_def, Ideal.mem_span_singleton', exists_exists_eq_and,
      map_mul, hr, ← Algebra.smul_def, smul_comm (d : R)]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
x_1 : K
h :
  (∃ (b : K), Membership.mem (γ := Submodule R K) (↑(spanSingleton R⁰ x) : Submodule R K) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₁ :
  (∃ (b : K), Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₂ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₃ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (Algebra.linearMap R K : (a : R) → K) y = x_1
h₄ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
h₅ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ (↑d : R) • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
h₆ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ (↑d : R) • b = x_1) ↔
    ∃ (y : R), (∃ (a : R), a * r = y) ∧ (algebraMap R K : (a : R) → K) y = x_1
h₇ : (∃ (a : R), (↑d : R) • a • x = x_1) ↔ ∃ (a : R), (algebraMap R K : (a : R) → K) (a * r) = x_1
h₈ :
  (∃ (a : R), (↑d : R) • a • x = x_1) ↔
    ∃ (a : R),
      HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) ((algebraMap R K : (a : R) → K) r : K) = x_1
⊢ x_1 ∈ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
have h₉ : (∃ (a : R), (↑d : R) • a • x = x_1) ↔
  ∃ (a : R), HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) a : K) ((↑d : R) • x) = x_1
Tactic: simp_rw [Submodule.mem_smul_pointwise_iff_exists, mem_coe, mem_spanSingleton, Submodule.mem_map,
      Algebra.linearMap_apply, Submonoid.smul_def, Ideal.mem_span_singleton', exists_exists_eq_and,
      map_mul, hr, ← Algebra.smul_def, smul_comm (d : R)]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
x_1 : K
h :
  (∃ (b : K), Membership.mem (γ := Submodule R K) (↑(spanSingleton R⁰ x) : Submodule R K) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₁ :
  (∃ (b : K), Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x) b ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₂ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
h₃ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (Algebra.linearMap R K : (a : R) → K) y = x_1
h₄ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ d • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
h₅ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ (↑d : R) • b = x_1) ↔
    ∃ (y : R), Membership.mem (γ := Submodule R R) (Ideal.span {r}) y ∧ (algebraMap R K : (a : R) → K) y = x_1
h₆ :
  (∃ (b : K), (∃ (z : R), z • x = b) ∧ (↑d : R) • b = x_1) ↔
    ∃ (y : R), (∃ (a : R), a * r = y) ∧ (algebraMap R K : (a : R) → K) y = x_1
h₇ : (∃ (a : R), (↑d : R) • a • x = x_1) ↔ ∃ (a : R), (algebraMap R K : (a : R) → K) (a * r) = x_1
h₈ :
  (∃ (a : R), (↑d : R) • a • x = x_1) ↔
    ∃ (a : R),
      HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) ((algebraMap R K : (a : R) → K) r : K) = x_1
h₉ :
  (∃ (a : R), (↑d : R) • a • x = x_1) ↔
    ∃ (a : R), HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) a : K) ((↑d : R) • x) = x_1
⊢ x_1 ∈ HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) ↔
    Membership.mem (γ := Submodule R K) (Submodule.map (Algebra.linearMap R K) (Ideal.span {r})) x_1
have h₁₀ : (∃ (a : R), (↑d : R) • a • x = x_1) ↔ ∃ (a : R), a • (↑d : R) • x = x_1
Tactic: simp_rw [Submodule.mem_smul_pointwise_iff_exists, mem_coe, mem_spanSingleton, Submodule.mem_map,
      Algebra.linearMap_apply, Submonoid.smul_def, Ideal.mem_span_singleton', exists_exists_eq_and,
      map_mul, hr, ← Algebra.smul_def, smul_comm (d : R)]
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
⊢ IsInteger R (a • b)
have obtain : ∀ (b' : P) (b'_mem : b' ∈ I) (hb' : (g.toLinearMap : (a : P) → P') b' = b), IsInteger R (a • b)
Tactic: obtain ⟨b', b'_mem, hb'⟩ := Submodule.mem_map.mp hb
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
b' : P
b'_mem : b' ∈ I
hb' : (g.toLinearMap : (a : P) → P') b' = b
⊢ IsInteger R (a • b)
have hb'₁ : (g : (a : P) → P') b' = b
Tactic: rw [AlgHom.toLinearMap_apply] at hb'
Cleared hypotheses: hb'
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
b' : P
b'_mem : b' ∈ I
hb' : (g : (a : P) → P') b' = b
⊢ IsInteger R (a • b)
have obtain : ∀ (x : R) (hx : (algebraMap R P : (a : R) → P) x = a • b'), IsInteger R (a • b)
Tactic: obtain ⟨x, hx⟩ := hI b' b'_mem
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
b' : P
b'_mem : b' ∈ I
hb' : (g : (a : P) → P') b' = b
x : R
hx : (algebraMap R P : (a : R) → P) x = a • b'
⊢ IsInteger R (a • b)
have h : (algebraMap R P' : (a : R) → P') x = a • b
Tactic: use x
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
b' : P
b'_mem : b' ∈ I
hb' : (g : (a : P) → P') b' = b
x : R
hx : (algebraMap R P : (a : R) → P) x = a • b'
⊢ (algebraMap R P' : (a : R) → P') x = a • b
have h : (g : (a : P) → P') ((algebraMap R P : (a : R) → P) x : P) = a • b
Tactic: rw [← g.commutes, hx, map_smul, hb']
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
b' : P
b'_mem : b' ∈ I
hb' : (g : (a : P) → P') b' = b
x : R
hx : (algebraMap R P : (a : R) → P) x = a • b'
h : (g : (a : P) → P') ((algebraMap R P : (a : R) → P) x : P) = a • b
⊢ (algebraMap R P' : (a : R) → P') x = a • b
have h₁ : (g : (a : P) → P') (a • b') = a • b
Tactic: rw [← g.commutes, hx, map_smul, hb']
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
b' : P
b'_mem : b' ∈ I
hb' : (g : (a : P) → P') b' = b
x : R
hx : (algebraMap R P : (a : R) → P) x = a • b'
h : (g : (a : P) → P') ((algebraMap R P : (a : R) → P) x : P) = a • b
h₁ : (g : (a : P) → P') (a • b') = a • b
⊢ (algebraMap R P' : (a : R) → P') x = a • b
have h₂ : HSMul.hSMul (β := P') a ((g : (a : P) → P') b' : P') = a • b
Tactic: rw [← g.commutes, hx, map_smul, hb']
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ b ∈ I, IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map g.toLinearMap I
b' : P
b'_mem : b' ∈ I
hb' : (g : (a : P) → P') b' = b
x : R
hx : (algebraMap R P : (a : R) → P) x = a • b'
h : (g : (a : P) → P') ((algebraMap R P : (a : R) → P) x : P) = a • b
h₁ : (g : (a : P) → P') (a • b') = a • b
h₂ : HSMul.hSMul (β := P') a ((g : (a : P) → P') b' : P') = a • b
⊢ (algebraMap R P' : (a : R) → P') x = a • b
have h₃ : a • b = a • b
Tactic: rw [← g.commutes, hx, map_smul, hb']
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
⊢ Eq (α := FractionalIdeal S P') (map g (↑I : FractionalIdeal S P)) (↑I : FractionalIdeal S P')
have a : ∀ (x : P'),
  Membership.mem (γ := FractionalIdeal S P') (map g (↑I : FractionalIdeal S P)) x ↔
    Membership.mem (γ := FractionalIdeal S P') (↑I : FractionalIdeal S P') x
Tactic: ext x
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ map g (I * J) = map g I * map g J
have simp : map g (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) ((↑I : Submodule R P) * (↑J : Submodule R P)) sorry) =
  Subtype.mk (p := fun (I : Submodule R P') ↦ IsFractional S I)
    ((↑(map g I) : Submodule R P') * (↑(map g J) : Submodule R P')) sorry
Tactic: simp only [mul_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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
I : FractionalIdeal S P
g : P ≃ₐ[R] P'
⊢ map (↑g.symm : P' →ₐ[R] P) (map (↑g : P →ₐ[R] P') I) = I
have rw : map ((↑g.symm : P' →ₐ[R] P).comp (↑g : P →ₐ[R] P')) I = I
Tactic: rw [← map_comp, g.symm_comp, map_id]
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
I : FractionalIdeal S P
g : P ≃ₐ[R] P'
rw : map ((↑g.symm : P' →ₐ[R] P).comp (↑g : P →ₐ[R] P')) I = I
⊢ map (↑g.symm : P' →ₐ[R] P) (map (↑g : P →ₐ[R] P') I) = I
have rw₁ : map (AlgHom.id R P) I = I
Tactic: rw [← map_comp, g.symm_comp, map_id]
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
I : FractionalIdeal S P
g : P ≃ₐ[R] P'
rw : map ((↑g.symm : P' →ₐ[R] P).comp (↑g : P →ₐ[R] P')) I = I
rw₁ : map (AlgHom.id R P) I = I
⊢ map (↑g.symm : P' →ₐ[R] P) (map (↑g : P →ₐ[R] P') I) = I
have rw₂ : I = I
Tactic: rw [← map_comp, g.symm_comp, map_id]
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
I : FractionalIdeal S P'
g : P ≃ₐ[R] P'
⊢ map (↑g : P →ₐ[R] P') (map (↑g.symm : P' →ₐ[R] P) I) = I
have rw : map ((↑g : P →ₐ[R] P').comp (↑g.symm : P' →ₐ[R] P)) I = I
Tactic: rw [← map_comp, g.comp_symm, map_id]
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
I : FractionalIdeal S P'
g : P ≃ₐ[R] P'
rw : map ((↑g : P →ₐ[R] P').comp (↑g.symm : P' →ₐ[R] P)) I = I
⊢ map (↑g : P →ₐ[R] P') (map (↑g.symm : P' →ₐ[R] P) I) = I
have rw₁ : map (AlgHom.id R P') I = I
Tactic: rw [← map_comp, g.comp_symm, map_id]
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
I : FractionalIdeal S P'
g : P ≃ₐ[R] P'
rw : map ((↑g : P →ₐ[R] P').comp (↑g.symm : P' →ₐ[R] P)) I = I
rw₁ : map (AlgHom.id R P') I = I
⊢ map (↑g : P →ₐ[R] P') (map (↑g.symm : P' →ₐ[R] P) I) = I
have rw₂ : I = I
Tactic: rw [← map_comp, g.comp_symm, map_id]
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I_1 J : FractionalIdeal S P
g_1 : P →ₐ[R] P'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P
⊢ map (↑g.symm : P' →ₐ[R] P) (map (↑g : P →ₐ[R] P') I) = I
have rw : map ((↑g.symm : P' →ₐ[R] P).comp (↑g : P →ₐ[R] P')) I = I
Tactic: rw [← map_comp, AlgEquiv.symm_comp, map_id]
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I_1 J : FractionalIdeal S P
g_1 : P →ₐ[R] P'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P
rw : map ((↑g.symm : P' →ₐ[R] P).comp (↑g : P →ₐ[R] P')) I = I
⊢ map (↑g.symm : P' →ₐ[R] P) (map (↑g : P →ₐ[R] P') I) = I
have rw₁ : map (AlgHom.id R P) I = I
Tactic: rw [← map_comp, AlgEquiv.symm_comp, map_id]
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I_1 J : FractionalIdeal S P
g_1 : P →ₐ[R] P'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P
rw : map ((↑g.symm : P' →ₐ[R] P).comp (↑g : P →ₐ[R] P')) I = I
rw₁ : map (AlgHom.id R P) I = I
⊢ map (↑g.symm : P' →ₐ[R] P) (map (↑g : P →ₐ[R] P') I) = I
have rw₂ : I = I
Tactic: rw [← map_comp, AlgEquiv.symm_comp, map_id]
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I_1 J : FractionalIdeal S P
g_1 : P →ₐ[R] P'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P'
⊢ map (↑g : P →ₐ[R] P') (map (↑g.symm : P' →ₐ[R] P) I) = I
have rw : map ((↑g : P →ₐ[R] P').comp (↑g.symm : P' →ₐ[R] P)) I = I
Tactic: rw [← map_comp, AlgEquiv.comp_symm, map_id]
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I_1 J : FractionalIdeal S P
g_1 : P →ₐ[R] P'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P'
rw : map ((↑g : P →ₐ[R] P').comp (↑g.symm : P' →ₐ[R] P)) I = I
⊢ map (↑g : P →ₐ[R] P') (map (↑g.symm : P' →ₐ[R] P) I) = I
have rw₁ : map (AlgHom.id R P') I = I
Tactic: rw [← map_comp, AlgEquiv.comp_symm, map_id]
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I_1 J : FractionalIdeal S P
g_1 : P →ₐ[R] P'
g : P ≃ₐ[R] P'
I : FractionalIdeal S P'
rw : map ((↑g : P →ₐ[R] P').comp (↑g.symm : P' →ₐ[R] P)) I = I
rw₁ : map (AlgHom.id R P') I = I
⊢ map (↑g : P →ₐ[R] P') (map (↑g.symm : P' →ₐ[R] P) I) = I
have rw₂ : I = I
Tactic: rw [← map_comp, AlgEquiv.comp_symm, map_id]
-- 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
s : Set P
h_1 : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s, IsInteger R (a • b)
x : P
hb : Membership.mem (γ := Submodule R P) (span R s) x
⊢ IsInteger R (HSMul.hSMul (β := P) a 0)
have rw : IsInteger.{u_1, u_2} R (S := P) 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
s : Set P
h_1 : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s, IsInteger R (a • b)
x_1 : P
hb : Membership.mem (γ := Submodule R P) (span R s) x_1
x y : P
h_2 : Membership.mem (γ := Submodule R P) (span R s) x
h_3 : Membership.mem (γ := Submodule R P) (span R s) y
hx : IsInteger R (a • x)
hy : IsInteger R (a • y)
⊢ IsInteger R (a • (x + y))
have rw : IsInteger R (a • x + a • 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
s_1 : Set P
h_1 : ∃ a ∈ S, ∀ b ∈ s_1, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s_1, IsInteger R (a • b)
x_1 : P
hb : Membership.mem (γ := Submodule R P) (span R s_1) x_1
s : R
x : P
h_2 : Membership.mem (γ := Submodule R P) (span R s_1) x
hx : IsInteger R (a • x)
⊢ IsInteger R (a • s • x)
have rw : IsInteger R (s • a • 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
I : Submodule R P
hI : I.FG
⊢ IsFractional S I
have rcases : ∀ (I : Finset P), IsFractional S (span R (↑I : Set P))
Tactic: rcases hI with ⟨I, rfl⟩
Cleared hypotheses: I, hI
-- 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 : Finset P
⊢ IsFractional S (span R (↑I : Set P))
have rcases : ∀ (s : R) (hs1 : s ∈ S) (hs : ∀ a ∈ I, IsInteger R ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) s hs1) : R) • a)),
  IsFractional S (span R (↑I : Set P))
Tactic: rcases exist_integer_multiples_of_finset S I with ⟨⟨s, hs1⟩, hs⟩
-- 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 : Finset P
s : R
hs1 : s ∈ S
hs : ∀ a ∈ I, IsInteger R ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) s hs1) : R) • a)
⊢ IsFractional S (span R (↑I : Set P))
have rw : ∃ a ∈ S, ∀ b ∈ (↑I : Set P), IsInteger R (a • b)
Tactic: rw [isFractional_span_iff]