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₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
neg : HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J * spanSingleton R₁⁰ d ≤ J
neg₁ :
  HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * (J * spanSingleton R₁⁰ d) ≤ J
neg₂ :
  J * (HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * spanSingleton R₁⁰ d) ≤ J
neg₃ : J * HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d⁻¹) (spanSingleton R₁⁰ d) ≤ J
neg₄ : J * spanSingleton R₁⁰ (d⁻¹ * d) ≤ J
neg₅ : J * spanSingleton R₁⁰ 1 ≤ J
⊢ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J ≤ J / spanSingleton R₁⁰ d
have neg₆ : J * 1 ≤ J
Tactic: rw [le_div_iff_mul_le h_spand, mul_assoc, mul_left_comm, one_div_spanSingleton,
      spanSingleton_mul_spanSingleton, inv_mul_cancel₀ hd, spanSingleton_one, mul_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₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
neg : HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J * spanSingleton R₁⁰ d ≤ J
neg₁ :
  HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * (J * spanSingleton R₁⁰ d) ≤ J
neg₂ :
  J * (HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * spanSingleton R₁⁰ d) ≤ J
neg₃ : J * HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d⁻¹) (spanSingleton R₁⁰ d) ≤ J
neg₄ : J * spanSingleton R₁⁰ (d⁻¹ * d) ≤ J
neg₅ : J * spanSingleton R₁⁰ 1 ≤ J
neg₆ : J * 1 ≤ J
⊢ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J ≤ J / spanSingleton R₁⁰ d
have neg₇ : J ≤ J
Tactic: rw [le_div_iff_mul_le h_spand, mul_assoc, mul_left_comm, one_div_spanSingleton,
      spanSingleton_mul_spanSingleton, inv_mul_cancel₀ hd, spanSingleton_one, mul_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₁
I : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
⊢ ∃ (a : R₁) (aI : Ideal R₁),
    a ≠ 0 ∧
      I =
        HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          ((↑aI : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
have obtain : ∀ (a_inv : R₁) (nonzero : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv)
  (ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)),
  ∃ (a : R₁) (aI : Ideal R₁),
    a ≠ 0 ∧
      I =
        HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          ((↑aI : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
Tactic: obtain ⟨a_inv, nonzero, ha⟩ := I.isFractional
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
⊢ ∃ (a : R₁) (aI : Ideal R₁),
    a ≠ 0 ∧
      I =
        HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          ((↑aI : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
have nonzero₁ : a_inv ≠ 0
Tactic: have nonzero := mem_nonZeroDivisors_iff_ne_zero.mp nonzero
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
⊢ ∃ (a : R₁) (aI : Ideal R₁),
    a ≠ 0 ∧
      I =
        HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          ((↑aI : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
have map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
Tactic: have map_a_nonzero : algebraMap R₁ K a_inv ≠ 0 :=
    mt IsFractionRing.to_map_eq_zero_iff.mp nonzero
-- 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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
⊢ ∃ (a : R₁) (aI : Ideal R₁),
    a ≠ 0 ∧
      I =
        HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          ((↑aI : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
have refine_1 : ∀ x ∈ I,
  ∃ (y' : K),
    Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (↑(comap (Algebra.linearMap R₁ K)
              (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                      FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                    I) :
                Submodule R₁ K)) :
          FractionalIdeal R₁⁰ K)
        y' ∧
      x = HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K) y'
Tactic: refine
    ⟨a_inv,
      Submodule.comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ (algebraMap R₁ K a_inv) * I),
      nonzero, ext fun x => Iff.trans ⟨?_, ?_⟩ mem_singleton_mul.symm⟩
-- 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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
refine_1 :
  ∀ x ∈ I,
    ∃ (y' : K),
      Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          (↑(comap (Algebra.linearMap R₁ K)
                (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                        FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                      I) :
                  Submodule R₁ K)) :
            FractionalIdeal R₁⁰ K)
          y' ∧
        x = HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K) y'
⊢ ∃ (a : R₁) (aI : Ideal R₁),
    a ≠ 0 ∧
      I =
        HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a)⁻¹ : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          ((↑aI : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
have refine_2 : ∀ (x : K),
  (∃ (y' : K),
      Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
          (↑(comap (Algebra.linearMap R₁ K)
                (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                        FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                      I) :
                  Submodule R₁ K)) :
            FractionalIdeal R₁⁰ K)
          y' ∧
        x = HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K) y') →
    x ∈ I
Tactic: refine
    ⟨a_inv,
      Submodule.comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ (algebraMap R₁ K a_inv) * I),
      nonzero, ext fun x => Iff.trans ⟨?_, ?_⟩ mem_singleton_mul.symm⟩
-- 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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
x : K
hx : x ∈ I
⊢ ∃ (y' : K),
    Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (↑(comap (Algebra.linearMap R₁ K)
              (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                      FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                    I) :
                Submodule R₁ K)) :
          FractionalIdeal R₁⁰ K)
        y' ∧
      x = HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K) y'
have refine_1 : ∀ (x' : R₁) (hx' : (algebraMap R₁ K : (a : R₁) → K) x' = a_inv • x),
  ∃ (y' : K),
    Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (↑(comap (Algebra.linearMap R₁ K)
              (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                      FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                    I) :
                Submodule R₁ K)) :
          FractionalIdeal R₁⁰ K)
        y' ∧
      x = HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K) y'
Tactic: obtain ⟨x', hx'⟩ := ha x hx
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K : (a : R₁) → K) x' = a_inv • x
⊢ ∃ (y' : K),
    Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (↑(comap (Algebra.linearMap R₁ K)
              (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                      FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                    I) :
                Submodule R₁ K)) :
          FractionalIdeal R₁⁰ K)
        y' ∧
      x = HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K) y'
have hx'₁ : (algebraMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) x
Tactic: rw [Algebra.smul_def] at hx'
Cleared hypotheses: hx'
-- 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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) x
⊢ ∃ (y' : K),
    Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (↑(comap (Algebra.linearMap R₁ K)
              (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                      FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                    I) :
                Submodule R₁ K)) :
          FractionalIdeal R₁⁰ K)
        y' ∧
      x = HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K) y'
have refine_1 : ∃ y' ∈ I,
  (Algebra.linearMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y'
Tactic: refine ⟨algebraMap R₁ K x', (mem_coeIdeal _).mpr ⟨x', mem_singleton_mul.mpr ?_, rfl⟩, ?_⟩
-- 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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) x
refine_1 :
  ∃ y' ∈ I,
    (Algebra.linearMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y'
⊢ ∃ (y' : K),
    Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (↑(comap (Algebra.linearMap R₁ K)
              (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                      FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                    I) :
                Submodule R₁ K)) :
          FractionalIdeal R₁⁰ K)
        y' ∧
      x = HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K) y'
have refine_1₁ : x =
  HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K) ((algebraMap R₁ K : (a : R₁) → K) x' : K)
Tactic: refine ⟨algebraMap R₁ K x', (mem_coeIdeal _).mpr ⟨x', mem_singleton_mul.mpr ?_, rfl⟩, ?_⟩
-- 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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) x
⊢ x =
    HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) x' : K)
have refine_1 : x =
  HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
    (HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) x)
Tactic: rw [hx', ← mul_assoc, inv_mul_cancel₀ map_a_nonzero, one_mul]
-- 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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) x
refine_1 :
  x =
    HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      (HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) x)
⊢ x =
    HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) x' : K)
have refine_1₁ : x =
  HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) *
    x
Tactic: rw [hx', ← mul_assoc, inv_mul_cancel₀ map_a_nonzero, one_mul]
-- 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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) x
refine_1 :
  x =
    HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      (HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) x)
refine_1₁ :
  x =
    HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
        ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) *
      x
⊢ x =
    HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) x' : K)
have refine_1₂ : x = 1 * x
Tactic: rw [hx', ← mul_assoc, inv_mul_cancel₀ map_a_nonzero, one_mul]
-- 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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
x : K
hx : x ∈ I
x' : R₁
hx' : (algebraMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) x
refine_1 :
  x =
    HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      (HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) x)
refine_1₁ :
  x =
    HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
        ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) *
      x
refine_1₂ : x = 1 * x
⊢ x =
    HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) x' : K)
have refine_1₃ : x = x
Tactic: rw [hx', ← mul_assoc, inv_mul_cancel₀ map_a_nonzero, one_mul]
-- 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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
y : K
hy :
  Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (↑(comap (Algebra.linearMap R₁ K)
          (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                  FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                I) :
            Submodule R₁ K)) :
      FractionalIdeal R₁⁰ K)
    y
⊢ HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K) y ∈ I
have refine_2 : ∀ (x' : R₁)
  (hx' :
    x' ∈
      comap (Algebra.linearMap R₁ K)
        (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
              (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
              I) :
          Submodule R₁ K))
  (hy :
    Membership.mem.{u_4, u_4} (α := K) (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
      (↑(comap (Algebra.linearMap R₁ K)
            (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                  (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                    FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                  I) :
              Submodule R₁ K)) :
        FractionalIdeal R₁⁰ K)
      ((algebraMap R₁ K : (a : R₁) → K) x' : K)),
  HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) x' : K) ∈
    I
Tactic: obtain ⟨x', hx', rfl⟩ := (mem_coeIdeal _).mp hy
Cleared hypotheses: y, hy
-- 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 : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
a_inv : R₁
nonzero_1 : Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) a_inv
ha : ∀ b ∈ (↑I : Submodule R₁ K), IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : Ne.{u_4 + 1} (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) (0 : K)
x' : R₁
hx' :
  x' ∈
    comap (Algebra.linearMap R₁ K)
      (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
            I) :
        Submodule R₁ K)
hy :
  Membership.mem.{u_4, u_4} (α := K) (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (↑(comap (Algebra.linearMap R₁ K)
          (↑(HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) a_inv) :
                  FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
                I) :
            Submodule R₁ K)) :
      FractionalIdeal R₁⁰ K)
    ((algebraMap R₁ K : (a : R₁) → K) x' : K)
⊢ HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) x' : K) ∈
    I
have refine_2 : ∀ (y' : K) (hy' : y' ∈ I)
  (hx' :
    (Algebra.linearMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y'),
  HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) x' : K) ∈
    I
Tactic: obtain ⟨y', hy', hx'⟩ := mem_singleton_mul.mp hx'