awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
x : K
hx : x * d ∈ (↑J : Submodule R₁ K)
h_xd : x = d⁻¹ * (x * d)
⊢ d⁻¹ * (x * d) ∈ (↑(spanSingleton R₁⁰ d⁻¹) : Submodule R₁ K) * (↑J : Submodule R₁ K)

Tactic:
exact Submodule.mul_mem_mul (mem_spanSingleton_self R₁⁰ _) hx

Premises used: Submodule.mul_mem_mul, nonZeroDivisors, FractionalIdeal.mem_spanSingleton_self
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
neg₇ neg₈ : J ≤ J
⊢ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J ≤ J / spanSingleton R₁⁰ d

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]

Premises used: FractionalIdeal.le_div_iff_mul_le, FractionalIdeal.spanSingleton_mul_spanSingleton, mul_assoc, FractionalIdeal.one_div_spanSingleton, mul_left_comm, FractionalIdeal.spanSingleton_one, mul_one, inv_mul_cancel₀
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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)
⊢ ∃ (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

Premises used: FractionalIdeal.isFractional
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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_inv ≠ 0

Tactic:
have nonzero := mem_nonZeroDivisors_iff_ne_zero.mp nonzero
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
⊢ 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
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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)

Tactic:
⟨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⟩

Premises used: FractionalIdeal.spanSingleton, HMul.hMul, Algebra.algebraMap, nonZeroDivisors, Algebra.linearMap, FractionalIdeal.coeToSubmodule, Submodule.comap, And.intro, FractionalIdeal.mem_singleton_mul, Iff.intro, FractionalIdeal.ext, Exists.intro, Iff.trans, DFunLike.coe, Iff.symm
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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'
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
⊢ ∃ (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:
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⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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'
⊢ ∃ (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
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
⊢ (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'

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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'

Tactic:
⟨algebraMap R₁ K x', (mem_coeIdeal _).mpr ⟨x', mem_singleton_mul.mpr ?_, rfl⟩, ?_⟩

Premises used: Iff.mpr, Algebra.algebraMap, FractionalIdeal.mem_coeIdeal, And.intro, FractionalIdeal.mem_singleton_mul, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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'
refine_1₁ :
  x =
    HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) 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'

Tactic:
refine ⟨algebraMap R₁ K x', (mem_coeIdeal _).mpr ⟨x', mem_singleton_mul.mpr ?_, rfl⟩, ?_⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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' ∈ I,
    (Algebra.linearMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y'

Tactic:
⟨x, hx, hx'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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' ∈ I,
    (Algebra.linearMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y'

Tactic:
exact ⟨x, hx, hx'⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
refine_1₃ refine_1₄ : x = x
⊢ x =
    HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) x' : K)

Tactic:
rw [hx', ← mul_assoc, inv_mul_cancel₀ map_a_nonzero, one_mul]

Premises used: mul_assoc, inv_mul_cancel₀, one_mul
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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
⊢ HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K) y ∈ I

Tactic:
obtain ⟨x', hx', rfl⟩ := (mem_coeIdeal _).mp hy

Premises used: FractionalIdeal.mem_coeIdeal, Iff.mp, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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)
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
⊢ 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'

Premises used: FractionalIdeal.mem_singleton_mul, Iff.mp
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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'_1 :
  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)
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'
⊢ (algebraMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y'

Tactic:
rw [Algebra.linearMap_apply] at hx'

Premises used: Algebra.linearMap_apply
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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'_1 :
  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)
y' : K
hy' : y' ∈ I
hx' : (algebraMap R₁ K : (a : R₁) → K) x' = HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y'
refine_2 :
  HMul.hMul (α := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      (HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) y') ∈
    I
refine_2₁ :
  HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
        ((algebraMap R₁ K : (a : R₁) → K) a_inv : K) *
      y' ∈
    I
refine_2₂ : 1 * y' ∈ I
refine_2₃ refine_2₄ refine_2₅ refine_2₆ : y' ∈ I
⊢ HMul.hMul (α := K) (β := K) (((algebraMap R₁ K : (a : R₁) → K) a_inv)⁻¹ : K)
      ((algebraMap R₁ K : (a : R₁) → K) x' : K) ∈
    I

Tactic:
rwa [hx', ← mul_assoc, inv_mul_cancel₀ map_a_nonzero, one_mul]

Premises used: mul_assoc, inv_mul_cancel₀, one_mul