awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
i : K
hi : i ∈ (↑I : Set K)
j : K
hj : j ∈ (↑J : Set K)
h :
  HMul.hMul (α := L) (β := L) ((IsLocalization.map L f hf : (a : K) → L) i : L)
      ((IsLocalization.map L f hf : (a : K) → L) j : L) ∈
    HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
      ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K))
⊢ (IsLocalization.map L f hf : (a : K) → L) (i * j) =
    HMul.hMul (α := L) (β := L) ((IsLocalization.map L f hf : (a : K) → L) i : L)
      ((IsLocalization.map L f hf : (a : K) → L) j : L)

Tactic:
simp
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
i : K
hi : i ∈ (↑I : Set K)
j : K
hj : j ∈ (↑J : Set K)
h :
  HMul.hMul (α := L) (β := L) ((IsLocalization.map L f hf : (a : K) → L) i : L)
      ((IsLocalization.map L f hf : (a : K) → L) j : L) ∈
    HMul.hMul (α := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))
      ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑J : Set K))
⊢ HMul.hMul (α := L) (β := L) ((IsLocalization.map L f hf : (a : K) → L) i : L)
      ((IsLocalization.map L f hf : (a : K) → L) j : L) ∈
    (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(I * J) : Set K))) : Set L)

Tactic:
exact Submodule.subset_span ⟨i * j, mul_mem_mul hi hj, by simp⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I₀ : Ideal A
rw :
  Eq.{u_4 + 1} (α := Submodule B L)
    (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(↑I₀ : FractionalIdeal M K) : Set K)))
    (span B (Set.image.{u_2, u_4} (α := B) (⇑(algebraMap B L) : (a : B) → L) ((⇑f : (a : A) → B) '' (↑I₀ : Set A))))
⊢ Eq (α := FractionalIdeal N L) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf (↑I₀ : FractionalIdeal M K))
    (↑(Ideal.map f I₀) : FractionalIdeal N L)

Tactic:
rw [Ideal.map, Ideal.span, ← coeToSubmodule_inj, Ideal.submodule_span_eq, coe_coeIdeal,
    IsLocalization.coeSubmodule_span, coe_extended_eq_span]

Premises used: IsLocalization.coeSubmodule_span, FractionalIdeal.coe_coeIdeal, Ideal.submodule_span_eq, FractionalIdeal.coeToSubmodule_inj, Ideal.map, Ideal.span, FractionalIdeal.coe_extended_eq_span
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I₀ : Ideal A
⊢ Eq.{u_4 + 1} (α := Submodule B L)
    (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(↑I₀ : FractionalIdeal M K) : Set K)))
    (span B (Set.image.{u_2, u_4} (α := B) (⇑(algebraMap B L) : (a : B) → L) ((⇑f : (a : A) → B) '' (↑I₀ : Set A))))

Tactic:
Submodule.span_eq_span ?_ ?_

Premises used: Submodule.span_eq_span
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I₀ : Ideal A
refine_1 :
  (⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(↑I₀ : FractionalIdeal M K) : Set K) ⊆
    (↑(span B (Set.image.{u_2, u_4} (α := B) (⇑(algebraMap B L) : (a : B) → L) ((⇑f : (a : A) → B) '' (↑I₀ : Set A)))) :
      Set L)
refine_2 :
  Set.image.{u_2, u_4} (α := B) (⇑(algebraMap B L) : (a : B) → L) ((⇑f : (a : A) → B) '' (↑I₀ : Set A)) ⊆
    (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(↑I₀ : FractionalIdeal M K) : Set K))) : Set L)
⊢ Eq.{u_4 + 1} (α := Submodule B L)
    (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(↑I₀ : FractionalIdeal M K) : Set K)))
    (span B (Set.image.{u_2, u_4} (α := B) (⇑(algebraMap B L) : (a : B) → L) ((⇑f : (a : A) → B) '' (↑I₀ : Set A))))

Tactic:
refine Submodule.span_eq_span ?_ ?_

Premises used: Submodule.span_eq_span
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I₀ : Ideal A
a : A
ha : a ∈ (↑I₀ : Set A)
rw :
  Eq.{u_4 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((f : (a : A) → B) a : B) : L)
    ((IsLocalization.map L f hf : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
rw₁ rw₂ :
  Eq.{u_4 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((f : (a : A) → B) a : B) : L)
    ((algebraMap B L : (a : B) → L) ((f : (a : A) → B) a : B) : L)
⊢ Eq.{u_4 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((f : (a : A) → B) a : B) : L)
    ((IsLocalization.map L f hf : (a : K) → L) ((Algebra.linearMap A K : (a : A) → K) a : K) : L)

Tactic:
rw [Algebra.linearMap_apply, IsLocalization.map_eq hf a]

Premises used: Algebra.linearMap_apply, IsLocalization.map_eq
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I₀ : Ideal A
a : A
ha : a ∈ (↑I₀ : Set A)
⊢ Membership.mem (α := L)
    (↑(span B (Set.image.{u_2, u_4} (α := B) (⇑(algebraMap B L) : (a : B) → L) ((⇑f : (a : A) → B) '' (↑I₀ : Set A)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) ((Algebra.linearMap A K : (a : A) → K) a : K) : L)

Tactic:
exact Submodule.subset_span
      ⟨f a, Set.mem_image_of_mem f ha, by rw [Algebra.linearMap_apply, IsLocalization.map_eq hf a]⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I₀ : Ideal A
a : A
ha : a ∈ (↑I₀ : Set A)
⊢ Membership.mem (α := L)
    (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(↑I₀ : FractionalIdeal M K) : Set K))) : Set L)
    ((algebraMap B L : (a : B) → L) ((f : (a : A) → B) a : B) : L)

Tactic:
Submodule.subset_span
      ⟨algebraMap A K a, mem_coeIdeal_of_mem M ha, IsLocalization.map_eq hf a⟩

Premises used: Algebra.algebraMap, IsLocalization.map_eq, FractionalIdeal.mem_coeIdeal_of_mem, And.intro, Exists.intro, Submodule.subset_span, DFunLike.coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst_2 : CommRing K
inst_3 : Algebra A K
inst_4 : IsLocalization M K
L : Type u_4
N : Submonoid B
inst_5 : CommRing L
inst_6 : Algebra B L
inst_7 : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I₀ : Ideal A
a : A
ha : a ∈ (↑I₀ : Set A)
⊢ Membership.mem (α := L)
    (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(↑I₀ : FractionalIdeal M K) : Set K))) : Set L)
    ((algebraMap B L : (a : B) → L) ((f : (a : A) → B) a : B) : L)

Tactic:
exact Submodule.subset_span
      ⟨algebraMap A K a, mem_coeIdeal_of_mem M ha, IsLocalization.map_eq hf a⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
⊢ Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (0 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    I = 0

Tactic:
extended_eq_zero_iff _ _ (FaithfulSMul.algebraMap_injective _ _) zero_notMem_nonZeroDivisors

Premises used: FractionalIdeal.extended, FaithfulSMul.algebraMap_injective, zero_notMem_nonZeroDivisors, FractionalIdeal.extended_eq_zero_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : Ideal A
⊢ Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) (↑I : FractionalIdeal A⁰ K) :
      FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((↑(Ideal.map (F := A →+* B) (algebraMap A B) I) : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) :
      FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)

Tactic:
extended_coeIdeal_eq_map L _ I

Premises used: FractionalIdeal.extended_coeIdeal_eq_map, FractionalIdeal.extended
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
rw :
  Eq.{u_3 + 1} (α := Submodule B L)
    (span B ((⇑(IsLocalization.map L (algebraMap A B) ⋯) : (a : K) → L) '' (↑I : Set K)))
    (span B
      ((⇑(IsLocalization.map (M := A⁰) (T := Algebra.algebraMapSubmonoid.{u_1, u_4} (R := A) B A⁰) L (algebraMap A B)
              ⋯) :
          (a : K) → L) ''
        (↑I : Set K)))
⊢ Eq.{u_3 + 1} (α := Submodule B L)
    (↑((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I) : Submodule B L)
    (span B ((⇑(algebraMap K L) : (a : K) → L) '' (↑I : Set K)))

Tactic:
rw [extendedHom'_apply, coe_extended_eq_span,
    IsLocalization.algebraMap_eq_map_map_submonoid A⁰ B K L]

Premises used: FractionalIdeal.extendedHom'_apply, nonZeroDivisors, FractionalIdeal.coe_extended_eq_span, IsLocalization.algebraMap_eq_map_map_submonoid
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
⊢ Eq.{u_3 + 1} (α := Submodule B L)
    (span B ((⇑(IsLocalization.map L (algebraMap A B) ⋯) : (a : K) → L) '' (↑I : Set K)))
    (span B
      ((⇑(IsLocalization.map (M := A⁰) (T := Algebra.algebraMapSubmonoid.{u_1, u_4} (R := A) B A⁰) L (algebraMap A B)
              ⋯) :
          (a : K) → L) ''
        (↑I : Set K)))

Tactic:
rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsIntegrallyClosed A
inst_18 : IsIntegrallyClosed B
hI :
  LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
contrapose :
  ∀ (hI : ¬I ≤ 1),
    ¬LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
⊢ I ≤ 1

Tactic:
contrapose hI
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsIntegrallyClosed A
inst_18 : IsIntegrallyClosed B
hI : ¬I ≤ 1
rw :
  ∀ (hI : ∃ x ∈ I, x ∉ 1),
    ∃ (x : L),
      Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
          ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
            FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
          x ∧
        x ∉ 1
⊢ ¬LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)

Tactic:
rw [SetLike.not_le_iff_exists] at hI ⊢

Premises used: SetLike.not_le_iff_exists
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsIntegrallyClosed A
inst_18 : IsIntegrallyClosed B
hI : ∃ x ∈ I, x ∉ 1
obtain :
  ∀ (x : K) (hx₁ : x ∈ I) (hx₂ : x ∉ 1),
    ∃ (x : L),
      Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
          ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
            FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
          x ∧
        x ∉ 1
⊢ ∃ (x : L),
    Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        x ∧
      x ∉ 1

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := hI
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsIntegrallyClosed A
inst_18 : IsIntegrallyClosed B
x : K
hx₁ : x ∈ I
hx₂ : x ∉ 1
⊢ ∃ (x : L),
    Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        x ∧
      x ∉ 1

Tactic:
⟨algebraMap K L x, ?_, ?_⟩

Premises used: Algebra.algebraMap, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsIntegrallyClosed A
inst_18 : IsIntegrallyClosed B
x : K
hx₁ : x ∈ I
hx₂ : x ∉ 1
refine_1 :
  Membership.mem.{u_3, u_3} (α := L) (γ := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((algebraMap K L : (a : K) → L) x : L)
refine_2 : ((algebraMap K L : (a : K) → L) x : L) ∉ 1
⊢ ∃ (x : L),
    Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        x ∧
      x ∉ 1

Tactic:
refine ⟨algebraMap K L x, ?_, ?_⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsIntegrallyClosed A
inst_18 : IsIntegrallyClosed B
x : K
hx₁ : x ∈ I
hx₂ : x ∉ 1
⊢ Membership.mem.{u_3, u_3} (α := L) (γ := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((algebraMap K L : (a : K) → L) x : L)

Tactic:
simpa [← FractionalIdeal.mem_coe, IsLocalization.algebraMap_eq_map_map_submonoid A⁰ B K L]
      using subset_span <| Set.mem_image_of_mem _ hx₁

Premises used: nonZeroDivisors, Set.mem_image_of_mem, FractionalIdeal.mem_coe, Submodule.subset_span, IsLocalization.algebraMap_eq_map_map_submonoid
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsIntegrallyClosed A
inst_18 : IsIntegrallyClosed B
x : K
hx₁ : x ∈ I
hx₂ : x ∉ 1
refine_2 :
  ∀
    (hx₂ :
      Membership.mem.{u_3, u_3} (α := L) (γ := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) 1
        ((algebraMap K L : (a : K) → L) x : L)),
    Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) 1 x
⊢ ((algebraMap K L : (a : K) → L) x : L) ∉ 1

Tactic:
contrapose hx₂
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsIntegrallyClosed A
inst_18 : IsIntegrallyClosed B
x : K
hx₁ : x ∈ I
hx₂ :
  Membership.mem.{u_3, u_3} (α := L) (γ := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) 1
    ((algebraMap K L : (a : K) → L) x : L)
refine_2 : ∀ (hx₂ : IsIntegral.{u_4, u_3} B (A := L) ((algebraMap K L : (a : K) → L) x : L)), IsIntegral A x
⊢ Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) 1 x

Tactic:
rw [mem_one_iff, ← IsIntegrallyClosed.isIntegral_iff] at hx₂ ⊢

Premises used: IsIntegrallyClosed.isIntegral_iff, FractionalIdeal.mem_one_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsIntegrallyClosed A
inst_18 : IsIntegrallyClosed B
x : K
hx₁ : x ∈ I
hx₂ : IsIntegral.{u_4, u_3} B (A := L) ((algebraMap K L : (a : K) → L) x : L)
⊢ IsIntegral A x

Tactic:
IsIntegral.tower_bot_of_field <| isIntegral_trans _ hx₂

Premises used: isIntegral_trans, IsIntegral.tower_bot_of_field
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsIntegrallyClosed A
inst_18 : IsIntegrallyClosed B
x : K
hx₁ : x ∈ I
hx₂ : IsIntegral.{u_4, u_3} B (A := L) ((algebraMap K L : (a : K) → L) x : L)
⊢ IsIntegral A x

Tactic:
exact IsIntegral.tower_bot_of_field <| isIntegral_trans _ hx₂

Premises used: isIntegral_trans, IsIntegral.tower_bot_of_field