awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
P'' : Type u_5
inst_7 : CommRing P''
inst_8 : Algebra R P''
inst_9 : IsLocalization S P''
I : FractionalIdeal S P
a :
  ∀ (x : P''),
    Membership.mem (γ := FractionalIdeal S P'')
        (((canonicalEquiv S P' P'' : RingEquiv.{u_3, u_5} (FractionalIdeal S P') (FractionalIdeal S P'')) :
              (a : FractionalIdeal S P') → FractionalIdeal S P'')
            (((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
                (a : FractionalIdeal S P) → FractionalIdeal S P')
              I) :
          FractionalIdeal S P'')
        x ↔
      Membership.mem (γ := FractionalIdeal S P'')
        (((canonicalEquiv S P P'' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P'')) :
              (a : FractionalIdeal S P) → FractionalIdeal S P'')
            I :
          FractionalIdeal S P'')
        x
⊢ Eq.{u_5 + 1} (α := FractionalIdeal S P'')
    (((canonicalEquiv S P' P'' : RingEquiv.{u_3, u_5} (FractionalIdeal S P') (FractionalIdeal S P'')) :
          (a : FractionalIdeal S P') → FractionalIdeal S P'')
        (((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
            (a : FractionalIdeal S P) → FractionalIdeal S P')
          I) :
      FractionalIdeal S P'')
    (((canonicalEquiv S P P'' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P'')) :
          (a : FractionalIdeal S P) → FractionalIdeal S P'')
        I :
      FractionalIdeal S P'')

Tactic:
ext
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
P'' : Type u_5
inst_7 : CommRing P''
inst_8 : Algebra R P''
inst_9 : IsLocalization S P''
I : FractionalIdeal S P
x : P''
⊢ Membership.mem (γ := FractionalIdeal S P'')
      (((canonicalEquiv S P' P'' : RingEquiv.{u_3, u_5} (FractionalIdeal S P') (FractionalIdeal S P'')) :
            (a : FractionalIdeal S P') → FractionalIdeal S P'')
          (((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
              (a : FractionalIdeal S P) → FractionalIdeal S P')
            I) :
        FractionalIdeal S P'')
      x ↔
    Membership.mem (γ := FractionalIdeal S P'')
      (((canonicalEquiv S P P'' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P'')) :
            (a : FractionalIdeal S P) → FractionalIdeal S P'')
          I :
        FractionalIdeal S P'')
      x

Tactic:
simp [IsLocalization.map_map]

Premises used: IsLocalization.map_map
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
P'' : Type u_5
inst_7 : CommRing P''
inst_8 : Algebra R P''
inst_9 : IsLocalization S P''
⊢ Eq (α := RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P''))
    (RingEquiv.trans (S := FractionalIdeal S P') (canonicalEquiv S P P') (canonicalEquiv S P' P''))
    (canonicalEquiv S P P'')

Tactic:
RingEquiv.ext (canonicalEquiv_canonicalEquiv S P P' P'')

Premises used: FractionalIdeal.canonicalEquiv_canonicalEquiv, RingEquiv.ext
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
I : Ideal R
a :
  ∀ (x : P'),
    Membership.mem (γ := FractionalIdeal S P')
        (((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
              (a : FractionalIdeal S P) → FractionalIdeal S P')
            (↑I : FractionalIdeal S P) :
          FractionalIdeal S P')
        x ↔
      Membership.mem (γ := FractionalIdeal S P') (↑I : FractionalIdeal S P') x
⊢ Eq.{u_3 + 1} (α := FractionalIdeal S P')
    (((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
          (a : FractionalIdeal S P) → FractionalIdeal S P')
        (↑I : FractionalIdeal S P) :
      FractionalIdeal S P')
    ((↑I : FractionalIdeal S P') : FractionalIdeal S P')

Tactic:
ext
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
I : Ideal R
x : P'
⊢ Membership.mem (γ := FractionalIdeal S P')
      (((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
            (a : FractionalIdeal S P) → FractionalIdeal S P')
          (↑I : FractionalIdeal S P) :
        FractionalIdeal S P')
      x ↔
    Membership.mem (γ := FractionalIdeal S P') (↑I : FractionalIdeal S P') x

Tactic:
simp [IsLocalization.map_eq]

Premises used: IsLocalization.map_eq
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
rw :
  Eq (α := FractionalIdeal S P ≃+* FractionalIdeal S P)
    (RingEquiv.trans (S := FractionalIdeal S P) (canonicalEquiv S P P) (canonicalEquiv S P P))
    (RingEquiv.refl (FractionalIdeal S P))
⊢ Eq (α := FractionalIdeal S P ≃+* FractionalIdeal S P) (canonicalEquiv S P P) (RingEquiv.refl (FractionalIdeal S P))

Tactic:
rw [← canonicalEquiv_trans_canonicalEquiv S P P]

Premises used: FractionalIdeal.canonicalEquiv_trans_canonicalEquiv
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
⊢ Eq (α := FractionalIdeal S P ≃+* FractionalIdeal S P)
    (RingEquiv.trans (S := FractionalIdeal S P) (RingEquiv.symm (canonicalEquiv S P P)) (canonicalEquiv S P P))
    (RingEquiv.refl (FractionalIdeal S P))

Tactic:
(canonicalEquiv S P P).symm_trans_self

Premises used: FractionalIdeal.canonicalEquiv, RingEquiv.symm_trans_self
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
h : Eq (α := FractionalIdeal S P ≃+* FractionalIdeal S P) (canonicalEquiv S P P) (RingEquiv.symm (canonicalEquiv S P P))
⊢ Eq (α := FractionalIdeal S P ≃+* FractionalIdeal S P)
    (RingEquiv.trans (S := FractionalIdeal S P) (canonicalEquiv S P P) (canonicalEquiv S P P))
    (RingEquiv.refl (FractionalIdeal S P))

Tactic:
convert! (canonicalEquiv S P P).symm_trans_self

Premises used: FractionalIdeal.canonicalEquiv, RingEquiv.symm_trans_self
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
⊢ Eq (α := FractionalIdeal S P ≃+* FractionalIdeal S P) (canonicalEquiv S P P) (RingEquiv.symm (canonicalEquiv S P P))

Tactic:
(canonicalEquiv_symm S P P).symm

Premises used: FractionalIdeal.canonicalEquiv_symm, Eq.symm
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
⊢ Eq (α := FractionalIdeal S P ≃+* FractionalIdeal S P) (canonicalEquiv S P P) (RingEquiv.symm (canonicalEquiv S P P))

Tactic:
exact (canonicalEquiv_symm S P P).symm

Premises used: FractionalIdeal.canonicalEquiv_symm, Eq.symm
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
⊢ ⊥ < I

Tactic:
simpa only using bot_lt_iff_ne_bot.mpr hI

Premises used: Iff.mpr, bot_lt_iff_ne_bot
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
obtain :
  ∀ (y : K) (y_mem : y ∈ I) (y_notMem : y ∉ ⊥),
    ∃ (x : R), x ≠ 0 ∧ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
⊢ ∃ (x : R), x ≠ 0 ∧ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)

Tactic:
obtain ⟨y : K, y_mem, y_notMem⟩ :=
    SetLike.exists_of_lt (by simpa only using bot_lt_iff_ne_bot.mpr hI)

Premises used: SetLike.exists_of_lt
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
⊢ y ≠ 0

Tactic:
simpa using y_notMem
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
⊢ y ≠ 0

Tactic:
have y_ne_zero : y ≠ 0 := by simpa using y_notMem
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
obtain :
  ∀ (z : ↥(R⁰ : Submonoid R)) (x : R) (hx : (algebraMap R K : (a : R) → K) x = (↑z : R) • y),
    ∃ (x : R), x ≠ 0 ∧ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
⊢ ∃ (x : R), x ≠ 0 ∧ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)

Tactic:
obtain ⟨z, ⟨x, hx⟩⟩ := exists_integer_multiple R⁰ y

Premises used: nonZeroDivisors, IsLocalization.exists_integer_multiple
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥(R⁰ : Submonoid R)
x : R
hx : (algebraMap R K : (a : R) → K) x = (↑z : R) • y
⊢ ∃ (x : R), x ≠ 0 ∧ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)

Tactic:
⟨x, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥(R⁰ : Submonoid R)
x : R
hx : (algebraMap R K : (a : R) → K) x = (↑z : R) • y
refine_1 : x ≠ 0
refine_2 : Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
⊢ ∃ (x : R), x ≠ 0 ∧ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)

Tactic:
refine ⟨x, ?_, ?_⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥(R⁰ : Submonoid R)
x : R
hx : (algebraMap R K : (a : R) → K) x = (↑z : R) • y
refine_1 : ¬HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑z : R) : K) y = 0
⊢ x ≠ 0

Tactic:
rw [Ne, ← @IsFractionRing.to_map_eq_zero_iff R _ K, hx, Algebra.smul_def]

Premises used: IsFractionRing.to_map_eq_zero_iff, Ne, Algebra.smul_def
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥(R⁰ : Submonoid R)
x : R
hx : (algebraMap R K : (a : R) → K) x = (↑z : R) • y
⊢ ¬HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑z : R) : K) y = 0

Tactic:
mul_ne_zero (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors z.2) y_ne_zero

Premises used: IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors, mul_ne_zero, Subtype.property
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥(R⁰ : Submonoid R)
x : R
hx : (algebraMap R K : (a : R) → K) x = (↑z : R) • y
⊢ ¬HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑z : R) : K) y = 0

Tactic:
exact mul_ne_zero (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors z.2) y_ne_zero

Premises used: IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors, mul_ne_zero, Subtype.property
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥(R⁰ : Submonoid R)
x : R
hx : (algebraMap R K : (a : R) → K) x = (↑z : R) • y
refine_2 : (↑z : R) • y ∈ I
⊢ Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)

Tactic:
rw [hx]
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥(R⁰ : Submonoid R)
x : R
hx : (algebraMap R K : (a : R) → K) x = (↑z : R) • y
⊢ (↑z : R) • y ∈ I

Tactic:
smul_mem _ _ y_mem

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
inst_4 : Nontrivial R
hI : I ≠ 0
y : K
y_mem : y ∈ I
y_notMem : y ∉ ⊥
y_ne_zero : y ≠ 0
z : ↥(R⁰ : Submonoid R)
x : R
hx : (algebraMap R K : (a : R) → K) x = (↑z : R) • y
⊢ (↑z : R) • y ∈ I

Tactic:
exact smul_mem _ _ y_mem

Premises used: Submodule.smul_mem
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
K' : Type u_4
inst_1 : Field K
inst_2 : Field K'
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : Algebra R K'
inst_6 : IsFractionRing R K'
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
h : K →ₐ[R] K'
inst_7 : Nontrivial R
hI : I ≠ 0
obtain :
  ∀ (x : R) (x_ne_zero : x ≠ 0) (hx : Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)), map h I ≠ 0
⊢ map h I ≠ 0

Tactic:
obtain ⟨x, x_ne_zero, hx⟩ := exists_ne_zero_mem_isInteger hI

Premises used: FractionalIdeal.exists_ne_zero_mem_isInteger
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
K' : Type u_4
inst_1 : Field K
inst_2 : Field K'
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : Algebra R K'
inst_6 : IsFractionRing R K'
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
h : K →ₐ[R] K'
inst_7 : Nontrivial R
hI : I ≠ 0
x : R
x_ne_zero : x ≠ 0
hx : Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
contrapose : ∀ (map_eq_zero : map h I = 0), x = 0
⊢ map h I ≠ 0

Tactic:
contrapose x_ne_zero with map_eq_zero

Premises used: map_eq_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
K' : Type u_4
inst_1 : Field K
inst_2 : Field K'
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : Algebra R K'
inst_6 : IsFractionRing R K'
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
h : K →ₐ[R] K'
inst_7 : Nontrivial R
hI : I ≠ 0
x : R
hx : Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
map_eq_zero : map h I = 0
⊢ x = 0

Tactic:
IsFractionRing.to_map_eq_zero_iff.mp (eq_zero_iff.mp map_eq_zero _ (mem_map.mpr ?_))

Premises used: Iff.mpr, FractionalIdeal.eq_zero_iff, FractionalIdeal.mem_map, IsFractionRing.to_map_eq_zero_iff, Iff.mp
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
K' : Type u_4
inst_1 : Field K
inst_2 : Field K'
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : Algebra R K'
inst_6 : IsFractionRing R K'
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
h : K →ₐ[R] K'
inst_7 : Nontrivial R
hI : I ≠ 0
x : R
hx : Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
map_eq_zero : map h I = 0
refine : ∃ x_1 ∈ I, Eq.{u_4 + 1} (α := K') ((h : (a : K) → K') x_1 : K') ((algebraMap R K' : (a : R) → K') x : K')
⊢ x = 0

Tactic:
refine IsFractionRing.to_map_eq_zero_iff.mp (eq_zero_iff.mp map_eq_zero _ (mem_map.mpr ?_))

Premises used: Iff.mpr, FractionalIdeal.eq_zero_iff, FractionalIdeal.mem_map, IsFractionRing.to_map_eq_zero_iff, Iff.mp
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
K' : Type u_4
inst_1 : Field K
inst_2 : Field K'
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : Algebra R K'
inst_6 : IsFractionRing R K'
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
h : K →ₐ[R] K'
inst_7 : Nontrivial R
hI : I ≠ 0
x : R
hx : Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
map_eq_zero : map h I = 0
⊢ ∃ x_1 ∈ I, Eq.{u_4 + 1} (α := K') ((h : (a : K) → K') x_1 : K') ((algebraMap R K' : (a : R) → K') x : K')

Tactic:
⟨algebraMap R K x, hx, h.commutes x⟩

Premises used: Algebra.algebraMap, And.intro, AlgHom.commutes, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
K' : Type u_4
inst_1 : Field K
inst_2 : Field K'
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : Algebra R K'
inst_6 : IsFractionRing R K'
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
h : K →ₐ[R] K'
inst_7 : Nontrivial R
hI : I ≠ 0
x : R
hx : Membership.mem (α := K) I ((algebraMap R K : (a : R) → K) x : K)
map_eq_zero : map h I = 0
⊢ ∃ x_1 ∈ I, Eq.{u_4 + 1} (α := K') ((h : (a : K) → K') x_1 : K') ((algebraMap R K' : (a : R) → K') x : K')

Tactic:
exact ⟨algebraMap R K x, hx, h.commutes x⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
K' : Type u_4
inst_1 : Field K
inst_2 : Field K'
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : Algebra R K'
inst_6 : IsFractionRing R K'
I : FractionalIdeal.{u_1, u_3} (R := R) R⁰ K
h : K →ₐ[R] K'
inst_7 : Nontrivial R
⊢ map h I = 0 ↔ I = 0

Tactic:
⟨not_imp_not.mp (map_ne_zero _), fun hI => hI.symm ▸ FractionalIdeal.map_zero h⟩

Premises used: Eq.rec, FractionalIdeal.map_ne_zero, Iff.intro, Iff.mp, Eq.symm, not_imp_not, FractionalIdeal.map_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (β := FractionalIdeal.{u_1, u_3} (R := R) R⁰ K) fun (I : Ideal R) ↦
    (↑I : FractionalIdeal R⁰ K)

Tactic:
coeIdeal_injective' le_rfl

Premises used: le_rfl, FractionalIdeal.coeIdeal_injective'
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I J : Ideal R
⊢ Eq.{u_3 + 1} (α := FractionalIdeal.{u_1, u_3} (R := R) R⁰ K) (↑I : FractionalIdeal R⁰ K) (↑J : FractionalIdeal R⁰ K) ↔
    I = J

Tactic:
coeIdeal_inj' le_rfl

Premises used: le_rfl, FractionalIdeal.coeIdeal_inj'
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : Ideal R
⊢ Eq.{u_3 + 1} (α := FractionalIdeal.{u_1, u_3} (R := R) R⁰ K) (↑I : FractionalIdeal R⁰ K) 0 ↔ I = ⊥

Tactic:
coeIdeal_eq_zero' le_rfl

Premises used: le_rfl, FractionalIdeal.coeIdeal_eq_zero'
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : Ideal R
⊢ Ne.{u_3 + 1} (α := FractionalIdeal.{u_1, u_3} (R := R) R⁰ K) (↑I : FractionalIdeal R⁰ K) 0 ↔ I ≠ ⊥

Tactic:
coeIdeal_ne_zero' le_rfl

Premises used: le_rfl, FractionalIdeal.coeIdeal_ne_zero'
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : Ideal R
⊢ Eq.{u_3 + 1} (α := FractionalIdeal.{u_1, u_3} (R := R) R⁰ K) (↑I : FractionalIdeal R⁰ K) 1 ↔ I = 1

Tactic:
simpa only [Ideal.one_eq_top] using coeIdeal_inj

Premises used: Ideal.one_eq_top, FractionalIdeal.coeIdeal_inj
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : Ideal R
⊢ Ne.{u_3 + 1} (α := FractionalIdeal.{u_1, u_3} (R := R) R⁰ K) (↑I : FractionalIdeal R⁰ K) 1 ↔ I ≠ 1

Tactic:
not_iff_not.mpr coeIdeal_eq_one

Premises used: not_iff_not, Iff.mpr, FractionalIdeal.coeIdeal_eq_one
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
R₁ : Type u_3
inst_3 : CommRing R₁
K : Type u_4
inst_4 : Field K
inst_5 : Algebra R₁ K
h : Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 1
rw :
  Membership.mem.{u_4, u_4} (α := K) (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0
    ((algebraMap R₁ K : (a : R₁) → K) 1 : K)
⊢ Membership.mem (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 1

Tactic:
rw [← (algebraMap R₁ K).map_one]

Premises used: Algebra.algebraMap, RingHom.map_one
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
R₁ : Type u_3
inst_3 : CommRing R₁
K : Type u_4
inst_4 : Field K
inst_5 : Algebra R₁ K
h : Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 1
⊢ Membership.mem.{u_4, u_4} (α := K) (γ := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0
    ((algebraMap R₁ K : (a : R₁) → K) 1 : K)

Tactic:
simpa only [h] using coe_mem_one R₁⁰ 1

Premises used: FractionalIdeal.coe_mem_one, nonZeroDivisors, OfNat.ofNat
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I = 0
⊢ I * J = 1

Tactic:
h
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I = 0
h₁ : 0 = I * J
⊢ Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 0 1

Tactic:
convert! h
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
I J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
h : I * J = 1
hI : I = 0
⊢ 0 = I * J

Tactic:
simp [hI]