awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : P →ₐ[R] P'
inst_7 : IsLocalization S P
I : (Submodule R P)ˣ
⊢ (↑(HMul.hMul (α := FractionalIdeal S P)
          (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I : Submodule R P) ⋯)
          (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I⁻¹ : Submodule R P) ⋯)) :
      Submodule R P) =
    (↑1 : Submodule R P)
have rw : (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I : Submodule R P) sorry) : Submodule R P) *
    (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I⁻¹ : Submodule R P) sorry) : Submodule R P) =
  1
Tactic: rw [coe_mul, coe_one]
-- 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 : P →ₐ[R] P'
inst_7 : IsLocalization S P
I : (Submodule R P)ˣ
⊢ (↑(HMul.hMul (α := FractionalIdeal S P)
          (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I⁻¹ : Submodule R P) ⋯)
          (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I : Submodule R P) ⋯)) :
      Submodule R P) =
    (↑1 : Submodule R P)
have rw : (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I⁻¹ : Submodule R P) sorry) : Submodule R P) *
    (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I : Submodule R P) sorry) : Submodule R P) =
  1
Tactic: rw [coe_mul, coe_one]
-- 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
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := P) (⇑(algebraMap R P) : (a : R) → P)
I : Ideal R
h : IsUnit.{u_2} (M := FractionalIdeal S P) (↑I : FractionalIdeal S P)
⊢ I.FG
have rw : FG.{u_1, u_2} (M := P) (↑(↑I : FractionalIdeal S P) : Submodule R P)
Tactic: rw [← coeIdeal_fg S inj I]
-- 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 J : FractionalIdeal S P
g : P →ₐ[R] P'
inst_7 : IsLocalization S P
inst_8 : IsLocalization S P'
⊢ Submonoid.map (F := R →* R) (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S
have rw : Submonoid.map (F := R →* R) (MonoidHom.id R) S = S
Tactic: rw [RingEquiv.toMonoidHom_refl, Submonoid.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 J : FractionalIdeal S P
g : P →ₐ[R] P'
inst_7 : IsLocalization S P
inst_8 : IsLocalization S P'
rw : Submonoid.map (F := R →* R) (MonoidHom.id R) S = S
⊢ Submonoid.map (F := R →* R) (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S
have rw₁ : S = S
Tactic: rw [RingEquiv.toMonoidHom_refl, Submonoid.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'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
I : FractionalIdeal S P
x : P'
⊢ Membership.mem (γ := FractionalIdeal S P')
      (((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
            (a : FractionalIdeal S P) → FractionalIdeal S P')
          I :
        FractionalIdeal S P')
      x ↔
    ∃ y ∈ I, (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') y = x
have rw : (∃ x_1 ∈ I,
    ((↑(let __src : P ≃+* P' := ringEquivOfRingEquiv P P' (RingEquiv.refl R) sorry;
              { toEquiv := __src.toEquiv, map_mul' := sorry, map_add' := sorry, commutes' := sorry }) :
            P →ₐ[R] P') :
          (a : P) → P')
        x_1 =
      x) ↔
  ∃ y ∈ I, (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') y = x
Tactic: rw [canonicalEquiv, mapEquiv_apply, mem_map]
-- 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'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
I : FractionalIdeal S P'
x : P
⊢ Membership.mem (γ := FractionalIdeal S P)
      (((RingEquiv.symm (canonicalEquiv S P P') : RingEquiv.{u_3, u_2} (FractionalIdeal S P') (FractionalIdeal S P)) :
            (a : FractionalIdeal S P') → FractionalIdeal S P)
          I :
        FractionalIdeal S P)
      x ↔
    Membership.mem (γ := FractionalIdeal S P)
      (((canonicalEquiv S P' P : RingEquiv.{u_3, u_2} (FractionalIdeal S P') (FractionalIdeal S P)) :
            (a : FractionalIdeal S P') → FractionalIdeal S P)
          I :
        FractionalIdeal S P)
      x
have rw : (∃ x_1 ∈ I,
    ((↑(AlgEquiv.symm
                (let __src : P ≃+* P' := ringEquivOfRingEquiv P P' (RingEquiv.refl R) sorry;
                { toEquiv := __src.toEquiv, map_mul' := sorry, map_add' := sorry, commutes' := sorry })) :
            P' →ₐ[R] P) :
          (a : P') → P)
        x_1 =
      x) ↔
  ∃ y ∈ I, (IsLocalization.map (M := S) (T := S) P (RingHom.id R) sorry : (a : P') → P) y = x
Tactic: rw [mem_canonicalEquiv_apply, canonicalEquiv, mapEquiv_symm, mapEquiv_apply,
        mem_map]
-- 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'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
I : FractionalIdeal S P'
⊢ ((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
        (a : FractionalIdeal S P) → FractionalIdeal S P')
      (((canonicalEquiv S P' P : RingEquiv.{u_3, u_2} (FractionalIdeal S P') (FractionalIdeal S P)) :
          (a : FractionalIdeal S P') → FractionalIdeal S P)
        I) =
    I
have rw : ((RingEquiv.symm (canonicalEquiv S P' P) : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
      (a : FractionalIdeal S P) → FractionalIdeal S P')
    (((canonicalEquiv S P' P : RingEquiv.{u_3, u_2} (FractionalIdeal S P') (FractionalIdeal S P)) :
        (a : FractionalIdeal S P') → FractionalIdeal S P)
      I) =
  I
Tactic: rw [← canonicalEquiv_symm, RingEquiv.symm_apply_apply]
-- 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'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
I : FractionalIdeal S P'
rw :
  ((RingEquiv.symm (canonicalEquiv S P' P) : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
        (a : FractionalIdeal S P) → FractionalIdeal S P')
      (((canonicalEquiv S P' P : RingEquiv.{u_3, u_2} (FractionalIdeal S P') (FractionalIdeal S P)) :
          (a : FractionalIdeal S P') → FractionalIdeal S P)
        I) =
    I
⊢ ((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
        (a : FractionalIdeal S P) → FractionalIdeal S P')
      (((canonicalEquiv S P' P : RingEquiv.{u_3, u_2} (FractionalIdeal S P') (FractionalIdeal S P)) :
          (a : FractionalIdeal S P') → FractionalIdeal S P)
        I) =
    I
have rw₁ : I = I
Tactic: rw [← canonicalEquiv_symm, RingEquiv.symm_apply_apply]
-- 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'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
P'' : Type u_5
inst_7 : CommRing P''
inst_8 : Algebra R P''
inst_9 : IsLocalization S P''
I : FractionalIdeal S P
⊢ Eq.{u_5 + 1} (α := FractionalIdeal S P'')
    (((canonicalEquiv S P' P'' : RingEquiv.{u_3, u_5} (FractionalIdeal S P') (FractionalIdeal S P'')) :
          (a : FractionalIdeal S P') → FractionalIdeal S P'')
        (((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
            (a : FractionalIdeal S P) → FractionalIdeal S P')
          I) :
      FractionalIdeal S P'')
    (((canonicalEquiv S P P'' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P'')) :
          (a : FractionalIdeal S P) → FractionalIdeal S P'')
        I :
      FractionalIdeal S P'')
have a : ∀ (x : P''),
  Membership.mem (γ := FractionalIdeal S P'')
      (((canonicalEquiv S P' P'' : RingEquiv.{u_3, u_5} (FractionalIdeal S P') (FractionalIdeal S P'')) :
            (a : FractionalIdeal S P') → FractionalIdeal S P'')
          (((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
              (a : FractionalIdeal S P) → FractionalIdeal S P')
            I) :
        FractionalIdeal S P'')
      x ↔
    Membership.mem (γ := FractionalIdeal S P'')
      (((canonicalEquiv S P P'' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P'')) :
            (a : FractionalIdeal S P) → FractionalIdeal S P'')
          I :
        FractionalIdeal S P'')
      x
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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
I : Ideal R
⊢ Eq.{u_3 + 1} (α := FractionalIdeal S P')
    (((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
          (a : FractionalIdeal S P) → FractionalIdeal S P')
        (↑I : FractionalIdeal S P) :
      FractionalIdeal S P')
    ((↑I : FractionalIdeal S P') : FractionalIdeal S P')
have a : ∀ (x : P'),
  Membership.mem (γ := FractionalIdeal S P')
      (((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
            (a : FractionalIdeal S P) → FractionalIdeal S P')
          (↑I : FractionalIdeal S P) :
        FractionalIdeal S P')
      x ↔
    Membership.mem (γ := FractionalIdeal S P') (↑I : FractionalIdeal S P') x
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
⊢ Eq (α := FractionalIdeal S P ≃+* FractionalIdeal S P) (canonicalEquiv S P P) (RingEquiv.refl (FractionalIdeal S P))
have rw : Eq (α := FractionalIdeal S P ≃+* FractionalIdeal S P)
  (RingEquiv.trans (S := FractionalIdeal S P) (canonicalEquiv S P P) (canonicalEquiv S P P))
  (RingEquiv.refl (FractionalIdeal S P))
Tactic: rw [← canonicalEquiv_trans_canonicalEquiv S P P]
-- 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
⊢ Eq (α := FractionalIdeal S P ≃+* FractionalIdeal S P)
    (RingEquiv.trans (S := FractionalIdeal S P) (canonicalEquiv S P P) (canonicalEquiv S P P))
    (RingEquiv.refl (FractionalIdeal S P))
have h : Eq (α := FractionalIdeal S P ≃+* FractionalIdeal S P) (canonicalEquiv S P P) (RingEquiv.symm (canonicalEquiv S P P))
Tactic: convert! (canonicalEquiv S P P).symm_trans_self
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
⊢ ∃ (x : R), x ≠ 0 ∧ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
have obtain : ∀ (y : K) (y_mem : y ∈ I) (y_notMem : y ∉ ⊥),
  ∃ (x : R), x ≠ 0 ∧ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
Tactic: obtain ⟨y : K, y_mem, y_notMem⟩ :=
    SetLike.exists_of_lt (by simpa only using bot_lt_iff_ne_bot.mpr hI)
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
⊢ ∃ (x : R), x ≠ 0 ∧ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
have y_ne_zero : y ≠ 0
Tactic: have y_ne_zero : y ≠ 0 := by simpa using y_notMem
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
⊢ ∃ (x : R), x ≠ 0 ∧ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
have obtain : ∀ (z : ↥(R⁰ : Submonoid R)) (x : R) (hx : (algebraMap R K : (a : R) → K) x = (↑z : R) • y),
  ∃ (x : R), x ≠ 0 ∧ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
Tactic: obtain ⟨z, ⟨x, hx⟩⟩ := exists_integer_multiple R⁰ y
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥(R⁰ : Submonoid R)
x : R
hx : (algebraMap R K : (a : R) → K) x = (↑z : R) • y
⊢ ∃ (x : R), x ≠ 0 ∧ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
have refine_1 : x ≠ 0
Tactic: refine ⟨x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥(R⁰ : Submonoid R)
x : R
hx : (algebraMap R K : (a : R) → K) x = (↑z : R) • y
refine_1 : x ≠ 0
⊢ ∃ (x : R), x ≠ 0 ∧ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
have refine_2 : Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
Tactic: refine ⟨x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥(R⁰ : Submonoid R)
x : R
hx : (algebraMap R K : (a : R) → K) x = (↑z : R) • y
⊢ x ≠ 0
have refine_1 : ¬HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑z : R) : K) y = 0
Tactic: rw [Ne, ← @IsFractionRing.to_map_eq_zero_iff R _ K, hx, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥(R⁰ : Submonoid R)
x : R
hx : (algebraMap R K : (a : R) → K) x = (↑z : R) • y
⊢ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
have refine_2 : (↑z : R) • y ∈ I
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
K' : Type u_4
inst_1 : Field K
inst_2 : Field K'
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : Algebra R K'
inst_6 : IsFractionRing R K'
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
h : K →ₐ[R] K'
inst_7 : Nontrivial R
hI : I ≠ 0
⊢ map h I ≠ 0
have obtain : ∀ (x : R) (x_ne_zero : x ≠ 0) (hx : Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)), map h I ≠ 0
Tactic: obtain ⟨x, x_ne_zero, hx⟩ := exists_ne_zero_mem_isInteger hI
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
K' : Type u_4
inst_1 : Field K
inst_2 : Field K'
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : Algebra R K'
inst_6 : IsFractionRing R K'
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
h : K →ₐ[R] K'
inst_7 : Nontrivial R
hI : I ≠ 0
x : R
x_ne_zero : x ≠ 0
hx : Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
⊢ map h I ≠ 0
have contrapose : ∀ (map_eq_zero : map h I = 0), x = 0
Tactic: contrapose x_ne_zero with map_eq_zero
Cleared hypotheses: x_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
K' : Type u_4
inst_1 : Field K
inst_2 : Field K'
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : Algebra R K'
inst_6 : IsFractionRing R K'
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
h : K →ₐ[R] K'
inst_7 : Nontrivial R
hI : I ≠ 0
x : R
hx : Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
map_eq_zero : map h I = 0
⊢ x = 0
have refine : ∃ x_1 ∈ I, Eq.{u_4 + 1} (α := K') ((h : (a : K) → K') x_1 : K') ((algebraMap R K' : (a : R) → K') x : K')
Tactic: refine IsFractionRing.to_map_eq_zero_iff.mp (eq_zero_iff.mp map_eq_zero _ (mem_map.mpr ?_))
-- 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
h : Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 1
⊢ Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 1
have rw : Membership.mem.{u_4, u_4} (α := K) (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0
  ((algebraMap R₁ K : (a : R₁) → K) 1 : K)
Tactic: rw [← (algebraMap R₁ K).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
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I = 0
⊢ Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 1
have h₁ : 0 = I * J
Tactic: convert! h
-- 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₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
⊢ IsFractional R₁⁰ (I / J)
have obtain : ∀ (y : K) (mem_J : y ∈ J) (notMem_zero : y ∉ 0), IsFractional R₁⁰ (I / J)
Tactic: obtain ⟨y, mem_J, notMem_zero⟩ :=
      SetLike.exists_of_lt (show 0 < J by simpa only using bot_lt_iff_ne_bot.mpr h)
-- 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₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
⊢ IsFractional R₁⁰ (I / J)
have obtain : ∀ (y' : R₁) (hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y), IsFractional R₁⁰ (I / J)
Tactic: obtain ⟨y', hy'⟩ := hJ y mem_J
-- 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₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
⊢ IsFractional R₁⁰ (I / J)
have h₁ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) (aI * y') ∧ ∀ b ∈ I / J, IsInteger R₁ ((aI * y') • b)
Tactic: use aI * y'
-- 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₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
⊢ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) (aI * y') ∧ ∀ b ∈ I / J, IsInteger R₁ ((aI * y') • b)
have h₁ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) (aI * y')
Tactic: constructor
-- 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₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
h₁ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) (aI * y')
⊢ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) (aI * y') ∧ ∀ b ∈ I / J, IsInteger R₁ ((aI * y') • b)
have h₂ : ∀ b ∈ I / J, IsInteger R₁ ((aI * y') • b)
Tactic: constructor
-- 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₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
⊢ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) (aI * y')
have apply : y' ≠ 0
Tactic: apply (nonZeroDivisors R₁).mul_mem haI (mem_nonZeroDivisors_iff_ne_zero.mpr _)
-- 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₁
I J : Submodule R₁ K
aI : R₁
haI : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aI
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) aJ
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K : (a : R₁) → K) y' = aJ • y
y'_eq_zero : y' = 0
⊢ HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) aJ : K) y = 0
have rw : aJ • y = 0
Tactic: rw [← Algebra.smul_def, ← hy', y'_eq_zero, map_zero]