awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
a :
  ∀ (y : K) (hy : y ∈ (↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K)),
    Membership.mem (α := L)
      (↑(span B
            (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)))) :
        Set L)
      ((IsLocalization.map L f hf : (a : K) → L) y : L)
⊢ Membership.mem (α := L)
    (↑(span B
          (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)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) x : L)
have a₁ : ∀ (y z : K),
  Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) y →
    Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) z →
      ∀
        (hy :
          Membership.mem (α := L)
            (↑(span B
                  (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)))) :
              Set L)
            ((IsLocalization.map L f hf : (a : K) → L) y : L))
        (hz :
          Membership.mem (α := L)
            (↑(span B
                  (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)))) :
              Set L)
            ((IsLocalization.map L f hf : (a : K) → L) z : L)),
        Membership.mem (α := L)
          (↑(span B
                (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)))) :
            Set L)
          ((IsLocalization.map L f hf : (a : K) → L) (y + z) : L)
Tactic: refine span_induction (fun y hy ↦ ?_) (by simp) (fun y z _ _ hy hz ↦ ?_)
      (fun a y _ hy ↦ ?_) hx
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
y : K
hy : y ∈ (↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K)
⊢ Membership.mem (α := L)
    (↑(span B
          (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)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) y : L)
have a : ∀ (i : K) (hi : i ∈ (↑(↑I : Submodule A K) : Set K)) (j : K) (hj : j ∈ (↑(↑J : Submodule A K) : Set K))
  (hy : i * j ∈ (↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K)),
  Membership.mem (α := L)
    (↑(span B
          (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)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) (i * j) : L)
Tactic: rcases Set.mem_mul.mp hy with ⟨i, hi, j, hj, rfl⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
x : K
hx : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) x
a : A
y : K
h : Membership.mem (γ := Submodule A K) (span A ((↑(↑I : Submodule A K) : Set K) * (↑(↑J : Submodule A K) : Set K))) y
hy :
  Membership.mem (α := L)
    (↑(span B
          (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)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) y : L)
⊢ Membership.mem (α := L)
    (↑(span B
          (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)))) :
      Set L)
    ((IsLocalization.map L f hf : (a : K) → L) (a • y) : L)
have a₁ : HSMul.hSMul.{u_2, u_4, u_4} (α := B) (β := L) ((f : (a : A) → B) a : B)
    ((IsLocalization.map L f hf : (a : K) → L) y : L) ∈
  (↑(span B
        (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)))) :
    Set L)
Tactic: rw [Algebra.smul_def, map_mul, map_eq, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
x : L
h :
  x ∈
    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))
⊢ x ∈ (↑(span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑(I * J) : Set K))) : Set L)
have a : ∀ (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: rcases Set.mem_mul.mp h with ⟨y, ⟨i, hi, rfl⟩, z, ⟨j, hj, rfl⟩, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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 (α := 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)
have 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))))
Tactic: rw [Ideal.map, Ideal.span, ← coeToSubmodule_inj, Ideal.submodule_span_eq, coe_coeIdeal,
    IsLocalization.coeSubmodule_span, coe_extended_eq_span]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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))))
have 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)
Tactic: refine Submodule.span_eq_span ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
⊢ 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))))
have 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)
Tactic: refine Submodule.span_eq_span ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Algebra.linearMap_apply, IsLocalization.map_eq hf a]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Algebra.linearMap_apply, IsLocalization.map_eq hf a]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
    (↑((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)))
have rw : Eq.{u_3 + 1} (α := Submodule B L) (span B ((⇑(IsLocalization.map L (algebraMap A B) sorry) : (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) sorry) :
        (a : K) → L) ''
      (↑I : Set K)))
Tactic: rw [extendedHom'_apply, coe_extended_eq_span,
    IsLocalization.algebraMap_eq_map_map_submonoid A⁰ B K L]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
⊢ I ≤ 1
have 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)
Tactic: contrapose hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
⊢ ¬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)
have 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
Tactic: rw [SetLike.not_le_iff_exists] at hI ⊢
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨x, hx₁, hx₂⟩ := hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
have 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)
Tactic: refine ⟨algebraMap K L x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
⊢ ∃ (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
have refine_2 : ((algebraMap K L : (a : K) → L) x : L) ∉ 1
Tactic: refine ⟨algebraMap K L x, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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
⊢ ((algebraMap K L : (a : K) → L) x : L) ∉ 1
have 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
Tactic: contrapose hx₂
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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)
⊢ Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) 1 x
have refine_2 : ∀ (hx₂ : IsIntegral.{u_4, u_3} B (A := L) ((algebraMap K L : (a : K) → L) x : L)), IsIntegral A x
Tactic: rw [mem_one_iff, ← IsIntegrallyClosed.isIntegral_iff] at hx₂ ⊢
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
hI : I ≠ 0
⊢ LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (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) ↔
    1 ≤ I
have rw : 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) ↔
  1 ≤ I
Tactic: rw [← inv_le_inv_iff ((extendedHom_eq_zero_iff _ _).not.mpr hI) (by simp), inv_one, ← map_inv₀,
    extendedHom_le_one_iff, inv_le_comm hI (by simp), inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Extended (goal)
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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
hI : I ≠ 0
rw :
  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) ↔
    1 ≤ I
⊢ LE.le.{u_3} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (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) ↔
    1 ≤ I
have rw₁ : 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) ↔
  1 ≤ I
Tactic: rw [← inv_le_inv_iff ((extendedHom_eq_zero_iff _ _).not.mpr hI) (by simp), inv_one, ← map_inv₀,
    extendedHom_le_one_iff, inv_le_comm hI (by simp), inv_one]