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

Tactic:
⟨fun h ↦ le_one_of_extendedHom_le_one L B h, fun a ↦ extended_le_one_of_le_one L _ I a⟩

Premises used: FractionalIdeal.le_one_of_extendedHom_le_one, FractionalIdeal.extendedHom._proof_2, FractionalIdeal.extended_le_one_of_le_one, Iff.intro
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
hI : I ≠ 0
⊢ Ne.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) 1 0

Tactic:
simp
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
hI : I ≠ 0
⊢ Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) 1 0

Tactic:
simp
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : 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
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
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
rw₃ : I⁻¹ ≤ 1 ↔ 1 ≤ I
rw₄ : 1⁻¹ ≤ I ↔ 1 ≤ I
rw₅ rw₆ : 1 ≤ I ↔ 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

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]

Premises used: Iff.mpr, FractionalIdeal.inv_le_inv_iff, inv_one, FractionalIdeal.extendedHom_eq_zero_iff, map_inv₀, Iff.not, FractionalIdeal.extendedHom_le_one_iff, FractionalIdeal.inv_le_comm
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
I : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : 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) ∧
      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) ↔
    I = 1
rw₁ :
  I ≤ 1 ∧
      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) ↔
    I = 1
rw₂ : I ≤ 1 ∧ 1 ≤ I ↔ I = 1
rw₃ rw₄ : I = 1 ↔ I = 1
⊢ Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
        FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
      (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) ↔
    I = 1

Tactic:
rw [le_antisymm_iff, extendedHom_le_one_iff, one_le_extendedHom_iff _ _ hI, ← le_antisymm_iff]

Premises used: FractionalIdeal.extendedHom_le_one_iff, le_antisymm_iff, FractionalIdeal.one_le_extendedHom_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
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
I J : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
h :
  Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
pos : ∀ (hI : I = 0), I = J
neg : ∀ (hI : ¬I = 0), I = J
⊢ I = J

Tactic:
by_cases hI : I = 0
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
I J : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
h :
  Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
hI : I = 0
pos :
  ∀
    (h :
      Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) 0 :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : I = 0), I = J
pos₁ :
  ∀
    (h :
      Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) (0 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : I = 0), I = J
pos₂ :
  ∀
    (h :
      Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        (0 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : I = 0), I = J
pos₃ : ∀ (h : J = 0) (hI : I = 0), I = J
pos₄ : ∀ (h : 0 = J) (hI : I = 0), I = J
pos₅ pos₆ pos₇ pos₈ : ∀ (h : I = J) (hI : I = 0), I = J
⊢ I = J

Tactic:
rwa [hI, map_zero, eq_comm, extendedHom_eq_zero_iff L B, eq_comm, ← hI] at h

Premises used: FractionalIdeal.extendedHom_eq_zero_iff, map_zero, eq_comm
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
I J : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
h :
  Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
hI : ¬I = 0
pos : ∀ (hJ : J = 0), I = J
neg : ∀ (hJ : ¬J = 0), I = J
⊢ I = J

Tactic:
by_cases hJ : J = 0
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
I J : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
h :
  Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
hI : ¬I = 0
hJ : J = 0
pos :
  ∀
    (h :
      Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) 0 :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : ¬I = 0) (hJ : J = 0), I = J
pos₁ :
  ∀
    (h :
      Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        (0 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : ¬I = 0) (hJ : J = 0), I = J
pos₂ : ∀ (h : I = 0) (hI : ¬I = 0) (hJ : J = 0), I = J
pos₃ pos₄ pos₅ pos₆ : ∀ (h : I = J) (hI : ¬I = 0) (hJ : J = 0), I = J
⊢ I = J

Tactic:
rwa [hJ, map_zero, extendedHom_eq_zero_iff L B, ← hJ] at h

Premises used: FractionalIdeal.extendedHom_eq_zero_iff, map_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Extended
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : IsDomain A
inst_2 : CommRing B
inst_3 : IsDomain B
inst_4 : Algebra A B
inst_5 : IsTorsionFree A B
inst_6 : Field K
inst_7 : Field L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : IsFractionRing A K
inst_11 : IsFractionRing B L
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A B L
inst_15 : IsScalarTower A K L
inst_16 : Algebra.IsIntegral A B
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
I J : FractionalIdeal.{u_1, u_2} (R := A) A⁰ K
h :
  Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) I : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
    ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
hI : ¬I = 0
hJ : ¬J = 0
neg :
  ∀
    (h :
      HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ 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)
          (((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J)⁻¹ :
            FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) =
        1)
    (hI : ¬I = 0) (hJ : ¬J = 0), I = J
neg₁ :
  ∀
    (h :
      HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ 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)
          ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) J⁻¹ :
            FractionalIdeal.{u_4, u_3} (R := B) B⁰ L) =
        1)
    (hI : ¬I = 0) (hJ : ¬J = 0), I = J
neg₂ :
  ∀
    (h :
      Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        ((extendedHom L B : (a : FractionalIdeal A⁰ K) → FractionalIdeal B⁰ L) (I * J⁻¹) :
          FractionalIdeal.{u_4, u_3} (R := B) B⁰ L)
        (1 : FractionalIdeal.{u_4, u_3} (R := B) B⁰ L))
    (hI : ¬I = 0) (hJ : ¬J = 0), I = J
neg₃ : ∀ (h : I * J⁻¹ = 1) (hI : ¬I = 0) (hJ : ¬J = 0), I = J
neg₄ neg₅ neg₆ neg₇ : ∀ (h : I = J) (hI : ¬I = 0) (hJ : ¬J = 0), I = J
⊢ I = J

Tactic:
rwa [← mul_inv_eq_one₀ ((extendedHom_eq_zero_iff _ _).not.mpr hJ), ← map_inv₀, ← map_mul,
    extendedHom_eq_one_iff _ _ (mul_ne_zero hI (inv_ne_zero hJ)), mul_inv_eq_one₀ hJ] at h

Premises used: map_inv₀, map_mul, FractionalIdeal.extendedHom_eq_one_iff, mul_inv_eq_one₀, inv_ne_zero, mul_ne_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
⊢ I⁻¹ = 1 / I

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
⊢ Eq.{u_3 + 1} (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 0⁻¹ 0

Tactic:
div_zero

Premises used: FractionalIdeal.div_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
J : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
h : J ≠ 0
⊢ J⁻¹ =
    Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑1 : Submodule R₁ K) / (↑J : Submodule R₁ K)) ⋯

Tactic:
div_of_ne_zero h

Premises used: FractionalIdeal.div_of_ne_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
J : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
h : J ≠ 0
simp_rw :
  (↑(Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) ((↑1 : Submodule R₁ K) / (↑J : Submodule R₁ K))
          ⋯) :
      Submodule R₁ K) =
    HDiv.hDiv (α := Submodule R₁ K) (IsLocalization.coeSubmodule K ⊤) (↑J : Submodule R₁ K)
simp_rw₁ :
  (↑(Subtype.mk (p := fun (I : Submodule R₁ K) ↦ IsFractional R₁⁰ I) (1 / (↑J : Submodule R₁ K)) ⋯) : Submodule R₁ K) =
    HDiv.hDiv (α := Submodule R₁ K) (IsLocalization.coeSubmodule K ⊤) (↑J : Submodule R₁ K)
simp_rw₂ :
  1 / (↑J : Submodule R₁ K) = HDiv.hDiv (α := Submodule R₁ K) (IsLocalization.coeSubmodule K ⊤) (↑J : Submodule R₁ K)
⊢ (↑J⁻¹ : Submodule R₁ K) = HDiv.hDiv (α := Submodule R₁ K) (IsLocalization.coeSubmodule K ⊤) (↑J : Submodule R₁ K)

Tactic:
simp_rw [inv_of_ne_zero _ h, coe_one, coe_mk, IsLocalization.coeSubmodule_top]

Premises used: FractionalIdeal.coe_mk, FractionalIdeal.coe_one, IsLocalization.coeSubmodule_top, FractionalIdeal.inv_of_ne_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I ≠ 0
x : K
⊢ x ∈ I⁻¹ ↔ ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1 (x * y)

Tactic:
mem_div_iff_of_ne_zero hI

Premises used: Set.Mem, FractionalIdeal.mem_div_iff_of_ne_zero
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I J : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I ≠ 0
hJ : J ≠ 0
hIJ : I ≤ J
x : K
simp :
  (∀ y ∈ J, Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1 (x * y)) →
    ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1 (x * y)
⊢ x ∈ J⁻¹ → x ∈ I⁻¹

Tactic:
simp only [mem_inv_iff hJ, mem_inv_iff hI]

Premises used: FractionalIdeal.mem_inv_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I J : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I ≠ 0
hJ : J ≠ 0
hIJ : I ≤ J
x : K
⊢ (∀ y ∈ J, Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1 (x * y)) →
    ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1 (x * y)

Tactic:
fun h y hy => h y (hIJ hy)
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I J : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I ≠ 0
hJ : J ≠ 0
hIJ : I ≤ J
x : K
⊢ (∀ y ∈ J, Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1 (x * y)) →
    ∀ y ∈ I, Membership.mem (γ := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) 1 (x * y)

Tactic:
exact fun h y hy => h y (hIJ hy)
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I ≤ 1
⊢ I ≤ I * I⁻¹

Tactic:
le_self_mul_one_div hI

Premises used: Set.Mem, FractionalIdeal.le_self_mul_one_div
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : Ideal R₁
⊢ (↑I : FractionalIdeal R₁⁰ K) ≤
    HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (↑I : FractionalIdeal R₁⁰ K)
      (↑I : FractionalIdeal R₁⁰ K)⁻¹

Tactic:
le_self_mul_inv coeIdeal_le_one

Premises used: FractionalIdeal.coeIdeal_le_one, FractionalIdeal.le_self_mul_inv
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I J : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
h : I * J = 1
⊢ J = I⁻¹

Tactic:
eq_one_div_of_mul_eq_one_right _ _ h

Premises used: FractionalIdeal.eq_one_div_of_mul_eq_one_right
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
h : ∃ (J : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K), I * J = 1
J : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hJ rwa rwa₁ rwa₂ rwa₃ : I * J = 1
⊢ I * I⁻¹ = 1

Tactic:
rwa [← right_inverse_eq K I J hJ]

Premises used: FractionalIdeal.right_inverse_eq
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
⊢ I * I⁻¹ = 1 ↔ IsUnit I

Tactic:
(mul_inv_cancel_iff K).trans isUnit_iff_exists_inv.symm

Premises used: isUnit_iff_exists_inv, FractionalIdeal.mul_inv_cancel_iff, Iff.trans, Iff.symm
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
K' : Type u_5
inst_5 : Field K'
inst_6 : Algebra R₁ K'
inst_7 : IsFractionRing R₁ K'
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
h : K ≃ₐ[R₁] K'
rw : map (↑h : K →ₐ[R₁] K') (1 / I) = (map (↑h : K →ₐ[R₁] K') I)⁻¹
rw₁ : map (↑h : K →ₐ[R₁] K') 1 / map (↑h : K →ₐ[R₁] K') I = (map (↑h : K →ₐ[R₁] K') I)⁻¹
rw₂ : 1 / map (↑h : K →ₐ[R₁] K') I = (map (↑h : K →ₐ[R₁] K') I)⁻¹
rw₃ rw₄ : 1 / map (↑h : K →ₐ[R₁] K') I = 1 / map (↑h : K →ₐ[R₁] K') I
⊢ map (↑h : K →ₐ[R₁] K') I⁻¹ = (map (↑h : K →ₐ[R₁] K') I)⁻¹

Tactic:
rw [inv_eq, FractionalIdeal.map_div, FractionalIdeal.map_one, inv_eq]

Premises used: FractionalIdeal.inv_eq, FractionalIdeal.map_div, FractionalIdeal.map_one
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
x : K
⊢ Eq (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ x)⁻¹ (spanSingleton R₁⁰ x⁻¹)

Tactic:
one_div_spanSingleton x

Premises used: FractionalIdeal.one_div_spanSingleton
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
x y : K
rw :
  HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ y⁻¹) (spanSingleton R₁⁰ x) =
    spanSingleton R₁⁰ (x / y)
rw₁ :
  HMul.hMul (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ x) (spanSingleton R₁⁰ y⁻¹) =
    spanSingleton R₁⁰ (x / y)
rw₂ : Eq (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (x * y⁻¹)) (spanSingleton R₁⁰ (x / y))
rw₃ rw₄ :
  Eq (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ (x * y⁻¹)) (spanSingleton R₁⁰ (x * y⁻¹))
⊢ HDiv.hDiv (α := FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ x) (spanSingleton R₁⁰ y) =
    spanSingleton R₁⁰ (x / y)

Tactic:
rw [div_spanSingleton, mul_comm, spanSingleton_mul_spanSingleton, div_eq_mul_inv]

Premises used: FractionalIdeal.spanSingleton_mul_spanSingleton, div_eq_mul_inv, FractionalIdeal.div_spanSingleton, mul_comm