awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
y : R
hy :
  y ∈
    (↑{ carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
          zero_mem' := ⋯, smul_mem' := ⋯ : Submodule R R } :
      Set R)
eq_y : (Algebra.linearMap R P : (a : R) → P) y = x
⊢ x ∈ J
have mp : Membership.mem (α := P) J ((Algebra.linearMap R P : (a : R) → P) y : P)
Tactic: rwa [← eq_y]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
hx : x ∈ J
⊢ Membership.mem (γ := FractionalIdeal S P)
    ((↑{ carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := ⋯,
            zero_mem' := ⋯, smul_mem' := ⋯ } :
        FractionalIdeal S P) :
      FractionalIdeal S P)
    x
have mp : ∀ (y : R) (hx : Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) y : P)),
  Membership.mem.{u_2, u_2} (α := P) (γ := FractionalIdeal S P)
    ((↑{ carrier := {x : R | Membership.mem (α := P) J ((algebraMap R P : (a : R) → P) x : P)}, add_mem' := sorry,
            zero_mem' := sorry, smul_mem' := sorry } :
        FractionalIdeal S P) :
      FractionalIdeal S P)
    ((algebraMap R P : (a : R) → P) y : P)
Tactic: obtain ⟨y, rfl⟩ := (mem_one_iff S).mp (hJ hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
J : FractionalIdeal S P
I : Ideal R
hI : (↑I : FractionalIdeal S P) = J
⊢ J ≤ 1
have mpr : LE.le.{u_2} (α := FractionalIdeal S P) (↑I : FractionalIdeal S P) 1
Tactic: rw [← hI]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
⊢ 1 ≤ I ↔ 1 ∈ I
have rw : (↑1 : Submodule R P) ≤ (↑I : Submodule R P) ↔ 1 ∈ I
Tactic: rw [← coe_le_coe, coe_one, Submodule.one_le, mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
rw : (↑1 : Submodule R P) ≤ (↑I : Submodule R P) ↔ 1 ∈ I
⊢ 1 ≤ I ↔ 1 ∈ I
have rw₁ : 1 ≤ (↑I : Submodule R P) ↔ 1 ∈ I
Tactic: rw [← coe_le_coe, coe_one, Submodule.one_le, mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
rw : (↑1 : Submodule R P) ≤ (↑I : Submodule R P) ↔ 1 ∈ I
rw₁ : 1 ≤ (↑I : Submodule R P) ↔ 1 ∈ I
⊢ 1 ≤ I ↔ 1 ∈ I
have rw₂ : 1 ∈ (↑I : Submodule R P) ↔ 1 ∈ I
Tactic: rw [← coe_le_coe, coe_one, Submodule.one_le, mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
I : FractionalIdeal S P
rw : (↑1 : Submodule R P) ≤ (↑I : Submodule R P) ↔ 1 ∈ I
rw₁ : 1 ≤ (↑I : Submodule R P) ↔ 1 ∈ I
rw₂ : 1 ∈ (↑I : Submodule R P) ↔ 1 ∈ I
⊢ 1 ≤ I ↔ 1 ∈ I
have rw₃ : 1 ∈ I ↔ 1 ∈ I
Tactic: rw [← coe_le_coe, coe_one, Submodule.one_le, mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) (↑1 : FractionalIdeal S P) 1
have rw : Eq.{u_2 + 1} (α := FractionalIdeal S P) (↑⊤ : FractionalIdeal S P) 1
Tactic: rw [Ideal.one_eq_top, coeIdeal_top]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
rw : Eq.{u_2 + 1} (α := FractionalIdeal S P) (↑⊤ : FractionalIdeal S P) 1
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) (↑1 : FractionalIdeal S P) 1
have rw₁ : Eq.{u_2 + 1} (α := FractionalIdeal S P) 1 1
Tactic: rw [Ideal.one_eq_top, coeIdeal_top]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDomain R
S : Submonoid R
P : Type u_4
inst_2 : Nontrivial P
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : Module.IsTorsionFree R P
hR : IsNoetherianRing R
hS : S ≤ R⁰
I : FractionalIdeal S P
⊢ (↑I : Submodule R P).FG
have this : FG I.num
Tactic: have := hR.noetherian I.num
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Basic (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDomain R
S : Submonoid R
P : Type u_4
inst_2 : Nontrivial P
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : Module.IsTorsionFree R P
hR : IsNoetherianRing R
hS : S ≤ R⁰
I : FractionalIdeal S P
this : FG I.num
⊢ (↑I : Submodule R P).FG
have rw : ∀ (this : Module.Finite R ↥I.num), Module.Finite.{u_3, u_4} R ↥(↑I : Submodule R P)
Tactic: rw [← Module.Finite.iff_fg] at this ⊢
Cleared hypotheses: this
-- 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_1 J I : FractionalIdeal M K
⊢ IsFractional.{u_2, u_4} N (P := L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K)))
have have : ∀ (a : A) (ha : a ∈ M) (frac : ∀ b ∈ (↑I : Submodule A K), IsInteger A (a • b)),
  IsFractional.{u_2, u_4} N (P := L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K)))
Tactic: have ⟨a, ha, frac⟩ := I.isFractional
-- 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_1 J I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ (↑I : Submodule A K), IsInteger A (a • b)
⊢ IsFractional.{u_2, u_4} N (P := L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K)))
have refine : ∀ (b : L)
  (hb : Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) b),
  IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) b)
Tactic: refine ⟨f a, hf ha, fun b hb ↦ ?_⟩
-- 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_1 J I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ (↑I : Submodule A K), IsInteger A (a • b)
b : L
hb : Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) b
⊢ IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) b)
have refine_1 : ∀ (x : L) (hx : Membership.mem (γ := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K)) x),
  IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) x)
Tactic: refine span_induction (fun x hx ↦ ?_) ⟨0, by simp⟩
      (fun x y _ _ hx hy ↦ smul_add (f a) x y ▸ isInteger_add hx hy) (fun b c _ hc ↦ ?_) hb
-- 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_1 J I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ (↑I : Submodule A K), IsInteger A (a • b)
b : L
hb : Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) b
refine_1 :
  ∀ (x : L) (hx : Membership.mem (γ := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K)) x),
    IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) x)
⊢ IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) b)
have refine_2 : ∀ (b : B) (c : L),
  Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) c →
    ∀ (hc : IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) c)),
      IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) (b • c))
Tactic: refine span_induction (fun x hx ↦ ?_) ⟨0, by simp⟩
      (fun x y _ _ hx hy ↦ smul_add (f a) x y ▸ isInteger_add hx hy) (fun b c _ hc ↦ ?_) hb
-- 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_1 J I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ (↑I : Submodule A K), IsInteger A (a • b)
b : L
hb : Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) b
x : L
hx : Membership.mem (γ := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K)) x
⊢ IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) x)
have refine_1 : ∀ (k : K) (kI : k ∈ (↑I : Set K)),
  IsInteger B
    (HSMul.hSMul.{u_2, u_4, u_4} (α := B) (β := L) ((f : (a : A) → B) a : B)
      ((IsLocalization.map L f hf : (a : K) → L) k : L))
Tactic: rcases hx with ⟨k, kI, rfl⟩
Cleared hypotheses: x, 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_1 J I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ (↑I : Submodule A K), IsInteger A (a • b)
b : L
hb : Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) b
k : K
kI : k ∈ (↑I : Set K)
⊢ IsInteger B
    (HSMul.hSMul.{u_2, u_4, u_4} (α := B) (β := L) ((f : (a : A) → B) a : B)
      ((IsLocalization.map L f hf : (a : K) → L) k : L))
have refine_1 : ∀ (c : A) (hc : (algebraMap A K : (a : A) → K) c = a • k),
  IsInteger B
    (HSMul.hSMul.{u_2, u_4, u_4} (α := B) (β := L) ((f : (a : A) → B) a : B)
      ((IsLocalization.map L f hf : (a : K) → L) k : L))
Tactic: obtain ⟨c, hc⟩ := frac k kI
-- 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_1 J I : FractionalIdeal M K
a : A
ha : a ∈ M
frac : ∀ b ∈ (↑I : Submodule A K), IsInteger A (a • b)
b_1 : L
hb : Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) b_1
b : B
c : L
h : Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) c
hc : IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) c)
⊢ IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) (b • c))
have refine_2 : IsInteger B (b • HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) c)
Tactic: rw [← smul_assoc, smul_eq_mul, mul_comm (f a), ← smul_eq_mul, smul_assoc]
-- 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 : FractionalIdeal M K
x : L
⊢ Membership.mem (γ := FractionalIdeal N L) (extended L hf I) x ↔
    Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) x
have mp : Membership.mem (γ := FractionalIdeal N L) (extended L hf I) x →
  Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) x
Tactic: constructor
-- 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 : FractionalIdeal M K
x : L
mp :
  Membership.mem (γ := FractionalIdeal N L) (extended L hf I) x →
    Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) x
⊢ Membership.mem (γ := FractionalIdeal N L) (extended L hf I) x ↔
    Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) x
have mpr : Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) x →
  Membership.mem (γ := FractionalIdeal N L) (extended L hf I) x
Tactic: constructor
-- 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 : FractionalIdeal M K
⊢ Eq (α := Submodule B L) (↑(extended L hf I) : Submodule B L)
    (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K)))
have h : ∀ (x : L),
  Membership.mem (γ := Submodule B L) (↑(extended L hf I) : Submodule B L) x ↔
    Membership.mem (γ := Submodule B L) (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K))) x
Tactic: ext
-- 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
⊢ (↑0 : Set K) = {0}
have h : ∀ (x : K), x ∈ (↑0 : Set K) ↔ Membership.mem (γ := Set K) {0} x
Tactic: ext
-- 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 : FractionalIdeal M K
inst_8 : IsDomain B
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hI : I ≠ 0
hN : 0 ∉ N
⊢ Ne (α := FractionalIdeal N L) (extended L hf I) 0
have simp : ∃ (x : K) (_ : x ∈ I), ¬Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) x : L) (0 : L)
Tactic: simp only [ne_eq, ← coeToSubmodule_inj, coe_extended_eq_span, coe_zero, Submodule.span_eq_bot,
    Set.mem_image, SetLike.mem_coe, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
    not_forall]
-- 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 : FractionalIdeal M K
inst_8 : IsDomain B
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hI : I ≠ 0
hN : 0 ∉ N
⊢ ∃ (x : K) (_ : x ∈ I), ¬Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) x : L) (0 : L)
have obtain : ∀ (x : K) (hx₁ : x ∈ I) (hx₂ : x ≠ 0),
  ∃ (x : K) (_ : x ∈ I), ¬Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) x : L) (0 : L)
Tactic: obtain ⟨x, hx₁, hx₂⟩ : ∃ x ∈ I, x ≠ 0 := by simpa [ne_eq, eq_zero_iff] using hI
-- 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 : FractionalIdeal M K
inst_8 : IsDomain B
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hI : I ≠ 0
hN : 0 ∉ N
x : K
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ ∃ (x : K) (_ : x ∈ I), ¬Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) x : L) (0 : L)
have refine : ¬Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) x : L) (0 : L)
Tactic: refine ⟨x, 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 : FractionalIdeal M K
inst_8 : IsDomain B
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hN : 0 ∉ N
⊢ Eq (α := FractionalIdeal N L) (extended L hf I) 0 ↔ I = 0
have refine : Eq (α := FractionalIdeal N L) (extended L hf I) 0 → I = 0
Tactic: refine ⟨?_, fun h ↦ h ▸ extended_zero _ _⟩
-- 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 : FractionalIdeal M K
inst_8 : IsDomain B
hf' : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hN : 0 ∉ N
⊢ Eq (α := FractionalIdeal N L) (extended L hf I) 0 → I = 0
have contrapose! : I ≠ 0 → Ne (α := FractionalIdeal N L) (extended L hf I) 0
Tactic: contrapose!
-- 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
⊢ Eq (α := FractionalIdeal N L) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1) 1
have refine_1 : ∀ (x : L),
  Membership.mem (γ := Submodule B L) ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) 1) x →
    Membership.mem (γ := Submodule B L)
      ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1)) x
Tactic: refine coeToSubmodule_injective <| Submodule.ext fun x ↦ ⟨fun hx ↦ span_induction
    ?_ (zero_mem _) (fun y z _ _ hy hz ↦ add_mem hy hz) (fun b y _ hy ↦ smul_mem _ b 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
refine_1 :
  ∀ (x : L),
    Membership.mem (γ := Submodule B L) ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) 1) x →
      Membership.mem (γ := Submodule B L)
        ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1)) x
⊢ Eq (α := FractionalIdeal N L) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1) 1
have refine_2 : ∀ (x : L)
  (hx :
    Membership.mem (γ := Submodule B L)
      ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1)) x)
  (x : L) (h : Membership.mem (γ := Set L) ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑1 : Set K)) x),
  Membership.mem (γ := Submodule B L) ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) 1) x
Tactic: refine coeToSubmodule_injective <| Submodule.ext fun x ↦ ⟨fun hx ↦ span_induction
    ?_ (zero_mem _) (fun y z _ _ hy hz ↦ add_mem hy hz) (fun b y _ hy ↦ smul_mem _ b 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
b : B
left : b ∈ (↑⊤ : Set B)
⊢ Membership.mem.{u_4, u_4} (α := L) (γ := Submodule B L)
    ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1))
    ((Algebra.linearMap B L : (a : B) → L) b : L)
have refine_1 : Membership.mem (γ := Submodule B L)
  ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1))
  (HSMul.hSMul (β := L) b 1)
Tactic: rw [Algebra.linearMap_apply, Algebra.algebraMap_eq_smul_one]
-- 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
x : L
hx :
  Membership.mem (γ := Submodule B L)
    ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1)) x
a : A
ha : a ∈ (↑⊤ : Set A)
⊢ Eq.{u_4 + 1} (α := L) ((Algebra.linearMap 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) ((Algebra.linearMap A K : (a : A) → K) a : K) : L)
Tactic: rw [Algebra.linearMap_apply, Algebra.linearMap_apply, map_eq]