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_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
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))
⊢ IsInteger B (HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) x)

Tactic:
rcases hx with ⟨k, kI, rfl⟩

Premises used: rfl
-- 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_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)
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))
⊢ 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
-- 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_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)
c : A
hc : (algebraMap A K : (a : A) → K) c = a • k
⊢ (algebraMap B L : (a : B) → L) ((f : (a : A) → B) c : 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:
simp [← IsLocalization.map_smul, ← hc]

Premises used: IsLocalization.map_smul
-- 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_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)
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:
exact ⟨f c, by simp [← IsLocalization.map_smul, ← hc]⟩
-- 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_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)
refine_2 : IsInteger B (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:
rw [← smul_assoc, smul_eq_mul, mul_comm (f a), ← smul_eq_mul, smul_assoc]

Premises used: smul_assoc, mul_comm, smul_eq_mul, 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_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 (b • HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) c)

Tactic:
isInteger_smul hc

Premises used: IsLocalization.isInteger_smul
-- 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_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 (b • HSMul.hSMul.{u_2, u_4, u_4} (α := B) ((f : (a : A) → B) a : B) c)

Tactic:
exact isInteger_smul hc

Premises used: IsLocalization.isInteger_smul
-- 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 : 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
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
⊢ 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
-- 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 : FractionalIdeal M K
x : L
hx : 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:
simpa
-- 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 : FractionalIdeal M K
x : L
mp mp₁ :
  ∀ (hx : 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

Tactic:
{ intro hx; simpa }
-- 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 : FractionalIdeal M K
x : L
hx : 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:
simpa
-- 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 : FractionalIdeal M K
x : L
mpr mpr₁ :
  ∀
    (hx :
      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 →
    Membership.mem (γ := FractionalIdeal N L) (extended L hf I) x

Tactic:
{ intro hx; simpa }
-- 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 : FractionalIdeal M K
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
⊢ Eq (α := Submodule B L) (↑(extended L hf I) : Submodule B L)
    (span B ((⇑(IsLocalization.map L f hf) : (a : K) → L) '' (↑I : Set K)))

Tactic:
ext
-- 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 : FractionalIdeal M K
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:
simp [mem_coe, mem_extended_iff]

Premises used: FractionalIdeal.mem_coe, FractionalIdeal.mem_extended_iff
-- 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
h : ∀ (x : K), x ∈ (↑0 : Set K) ↔ Membership.mem (γ := Set K) {0} x
⊢ (↑0 : Set K) = {0}

Tactic:
ext
-- 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
x : K
⊢ x ∈ (↑0 : Set K) ↔ Membership.mem (γ := Set K) {0} x

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
this : (↑0 : Set K) = {0}
⊢ Eq.{u_4 + 1} (α := 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 0))
    ((fun (I : FractionalIdeal N L) ↦ (↑I : Submodule B L)) 0)

Tactic:
simp [this]
-- 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 : 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
simp : ∃ (x : K) (_ : x ∈ I), ¬Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) x : L) (0 : L)
⊢ Ne (α := FractionalIdeal N L) (extended L hf I) 0

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]

Premises used: and_imp, Submodule.span_eq_bot, Set.mem_image, forall_exists_index, FractionalIdeal.coeToSubmodule_inj, ne_eq, SetLike.mem_coe, Classical.not_forall, forall_apply_eq_imp_iff₂, FractionalIdeal.coe_zero, 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 : 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 ∈ I, x ≠ 0

Tactic:
simpa [ne_eq, eq_zero_iff] using hI

Premises used: FractionalIdeal.eq_zero_iff, ne_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 : 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
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)
⊢ ∃ (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
-- 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 : 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)

Tactic:
⟨x, hx₁, ?_⟩

Premises used: Exists.intro
-- 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 : 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
refine : ¬Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) x : L) (0 : L)
⊢ ∃ (x : K) (_ : x ∈ I), ¬Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) x : L) (0 : L)

Tactic:
refine ⟨x, hx₁, ?_⟩
-- 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 : 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
⊢ ¬Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) x : L) (0 : L)

Tactic:
(map_ne_zero_iff _ (IsLocalization.map_injective_of_injective' _ _ _ _ hN hf')).mpr hx₂

Premises used: Iff.mpr, IsLocalization.map_injective_of_injective', map_ne_zero_iff
-- 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 : 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
⊢ ¬Eq.{u_4 + 1} (α := L) ((IsLocalization.map L f hf : (a : K) → L) x : L) (0 : L)

Tactic:
exact (map_ne_zero_iff _ (IsLocalization.map_injective_of_injective' _ _ _ _ hN hf')).mpr hx₂

Premises used: Iff.mpr, IsLocalization.map_injective_of_injective', map_ne_zero_iff
-- 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 : 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

Tactic:
⟨?_, fun h ↦ h ▸ extended_zero _ _⟩

Premises used: Eq.rec, FractionalIdeal.extended_zero, Iff.intro, Eq.symm
-- 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 : 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
refine : Eq (α := FractionalIdeal N L) (extended L hf I) 0 → I = 0
⊢ Eq (α := FractionalIdeal N L) (extended L hf I) 0 ↔ I = 0

Tactic:
refine ⟨?_, fun h ↦ h ▸ extended_zero _ _⟩
-- 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 : 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
contrapose! : I ≠ 0 → Ne (α := FractionalIdeal N L) (extended L hf I) 0
⊢ Eq (α := FractionalIdeal N L) (extended L hf I) 0 → I = 0

Tactic:
contrapose!
-- 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 : 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
⊢ I ≠ 0 → Ne (α := FractionalIdeal N L) (extended L hf I) 0

Tactic:
fun h ↦ extended_ne_zero L hf hf' h hN

Premises used: FractionalIdeal.extended_ne_zero
-- 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 : 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
⊢ I ≠ 0 → Ne (α := FractionalIdeal N L) (extended L hf I) 0

Tactic:
exact fun h ↦ extended_ne_zero L hf hf' h hN

Premises used: FractionalIdeal.extended_ne_zero
-- 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
⊢ Eq (α := FractionalIdeal N L) (extended.{u_1, u_2, u_3, u_4} (K := K) L hf 1) 1

Tactic:
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, ?_⟩

Premises used: Submodule.span_induction, Iff.intro, FractionalIdeal.coeToSubmodule_injective, Submodule.ext