awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
x_mul_mem :
  ∀ (b : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)
p : A[X]
hy :
  Membership.mem (α := K) (γ := Submodule A K)
    ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) (AlgHom.range (Polynomial.aeval x)) :
      Submodule A K)
    ((Polynomial.aeval x : (a : A[X]) → K) p : K)
i : ℕ
ih : Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) (x ^ i)
neg : Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) (x * x ^ i)
⊢ Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) (x ^ (i + 1))

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
x_mul_mem :
  ∀ (b : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)
p : A[X]
hy :
  Membership.mem (α := K) (γ := Submodule A K)
    ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) (AlgHom.range (Polynomial.aeval x)) :
      Submodule A K)
    ((Polynomial.aeval x : (a : A[X]) → K) p : K)
i : ℕ
ih : Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) (x ^ i)
⊢ Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) (x * x ^ i)

Tactic:
x_mul_mem _ ih

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
x_mul_mem :
  ∀ (b : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)
p : A[X]
hy :
  Membership.mem (α := K) (γ := Submodule A K)
    ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) (AlgHom.range (Polynomial.aeval x)) :
      Submodule A K)
    ((Polynomial.aeval x : (a : A[X]) → K) p : K)
i : ℕ
ih : Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) (x ^ i)
⊢ Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) (x * x ^ i)

Tactic:
exact x_mul_mem _ ih
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 :
  ¬HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ =
      0
x : K
hx :
  x ∈
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)
        (↑I : FractionalIdeal A⁰ K)⁻¹)⁻¹
x_mul_mem :
  ∀ (b : K),
    Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ b →
      Membership.mem (γ := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (↑I : FractionalIdeal A⁰ K)⁻¹ (x * b)
p : A[X]
hy :
  Membership.mem (α := K) (γ := Submodule A K)
    ((Subalgebra.toSubmodule : (a : Subalgebra A K) → Submodule A K) (AlgHom.range (Polynomial.aeval x)) :
      Submodule A K)
    ((Polynomial.aeval x : (a : A[X]) → K) p : K)
i : ℕ
neg : Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) (HPow.hPow (β := ℕ) x 0)
neg₁ :
  ∀ (i : ℕ) (ih : Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) (x ^ i)),
    Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) (x ^ (i + 1))
⊢ Membership.mem (γ := Submodule A K) (↑(↑I : FractionalIdeal A⁰ K)⁻¹ : Submodule A K) (x ^ i)

Tactic:
induction i with
  | zero => rw [pow_zero]; exact one_mem_inv_coe_ideal hI0
  | succ i ih => rw [pow_succ']; exact x_mul_mem _ ih

Premises used: FractionalIdeal.one_mem_inv_coe_ideal, pow_zero, pow_succ'
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : IsDedekindDomain A
I_1 : Ideal A
I : FractionalIdeal (R := A) A⁰ (FractionRing A)
hI : I ≠ ⊥
obtain :
  ∀ (a : A) (J : Ideal A) (ha : a ≠ 0)
    (hJ :
      I =
        HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β :=
          FractionalIdeal (R := A) A⁰ (FractionRing A))
          (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a)⁻¹ :
            FractionalIdeal (R := A) A⁰ (FractionRing A))
          ((↑J : FractionalIdeal (R := A) A⁰ (FractionRing A)) : FractionalIdeal (R := A) A⁰ (FractionRing A))),
    I * I⁻¹ = 1
⊢ I * I⁻¹ = 1

Tactic:
obtain ⟨a, J, ha, hJ⟩ := exists_eq_spanSingleton_mul (K := FractionRing A) I

Premises used: FractionalIdeal.exists_eq_spanSingleton_mul
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : IsDedekindDomain A
I_1 : Ideal A
I : FractionalIdeal (R := A) A⁰ (FractionRing A)
hI : I ≠ ⊥
a : A
J : Ideal A
ha : a ≠ 0
hJ :
  I =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a)⁻¹ :
        FractionalIdeal (R := A) A⁰ (FractionRing A))
      ((↑J : FractionalIdeal (R := A) A⁰ (FractionRing A)) : FractionalIdeal (R := A) A⁰ (FractionRing A))
h₂ :
  I *
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
        (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a) :
          FractionalIdeal (R := A) A⁰ (FractionRing A))
        ((↑J : FractionalIdeal A⁰ (FractionRing A))⁻¹ : FractionalIdeal (R := A) A⁰ (FractionRing A)) =
    1
rw : ∃ (J : FractionalIdeal (R := A) A⁰ (FractionRing A)), I * J = 1
⊢ I * I⁻¹ = 1

Tactic:
rw [mul_inv_cancel_iff]

Premises used: FractionalIdeal.mul_inv_cancel_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : IsDedekindDomain A
I_1 : Ideal A
I : FractionalIdeal (R := A) A⁰ (FractionRing A)
hI : I ≠ ⊥
a : A
J : Ideal A
ha : a ≠ 0
hJ :
  I =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a)⁻¹ :
        FractionalIdeal (R := A) A⁰ (FractionRing A))
      ((↑J : FractionalIdeal (R := A) A⁰ (FractionRing A)) : FractionalIdeal (R := A) A⁰ (FractionRing A))
h₂ :
  I *
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
        (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a) :
          FractionalIdeal (R := A) A⁰ (FractionRing A))
        ((↑J : FractionalIdeal A⁰ (FractionRing A))⁻¹ : FractionalIdeal (R := A) A⁰ (FractionRing A)) =
    1
⊢ ∃ (J : FractionalIdeal (R := A) A⁰ (FractionRing A)), I * J = 1

Tactic:
⟨spanSingleton A⁰ (algebraMap _ _ a) * (J : FractionalIdeal A⁰ _)⁻¹, h₂⟩

Premises used: FractionalIdeal.spanSingleton, HMul.hMul, Algebra.algebraMap, nonZeroDivisors, Inv.inv, Exists.intro, FractionalIdeal.coeIdeal, DFunLike.coe
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : IsDedekindDomain A
I_1 : Ideal A
I : FractionalIdeal (R := A) A⁰ (FractionRing A)
hI : I ≠ ⊥
a : A
J : Ideal A
ha : a ≠ 0
hJ :
  I =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a)⁻¹ :
        FractionalIdeal (R := A) A⁰ (FractionRing A))
      ((↑J : FractionalIdeal (R := A) A⁰ (FractionRing A)) : FractionalIdeal (R := A) A⁰ (FractionRing A))
h₂ :
  I *
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
        (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a) :
          FractionalIdeal (R := A) A⁰ (FractionRing A))
        ((↑J : FractionalIdeal A⁰ (FractionRing A))⁻¹ : FractionalIdeal (R := A) A⁰ (FractionRing A)) =
    1
⊢ ∃ (J : FractionalIdeal (R := A) A⁰ (FractionRing A)), I * J = 1

Tactic:
exact ⟨spanSingleton A⁰ (algebraMap _ _ a) * (J : FractionalIdeal A⁰ _)⁻¹, h₂⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : IsDedekindDomain A
I_1 : Ideal A
I : FractionalIdeal (R := A) A⁰ (FractionRing A)
hI : I ≠ ⊥
a : A
J : Ideal A
ha : a ≠ 0
hJ :
  I =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a)⁻¹ :
        FractionalIdeal (R := A) A⁰ (FractionRing A))
      ((↑J : FractionalIdeal (R := A) A⁰ (FractionRing A)) : FractionalIdeal (R := A) A⁰ (FractionRing A))
suffices :
  I *
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
        (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a) :
          FractionalIdeal (R := A) A⁰ (FractionRing A))
        ((↑J : FractionalIdeal A⁰ (FractionRing A))⁻¹ : FractionalIdeal (R := A) A⁰ (FractionRing A)) =
    1
⊢ I * I⁻¹ = 1

Tactic:
suffices h₂ : I * (spanSingleton A⁰ (algebraMap _ _ a) * (J : FractionalIdeal A⁰ _)⁻¹) = 1 by
      rw [mul_inv_cancel_iff]
      exact ⟨spanSingleton A⁰ (algebraMap _ _ a) * (J : FractionalIdeal A⁰ _)⁻¹, h₂⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : IsDedekindDomain A
I_1 : Ideal A
I : FractionalIdeal (R := A) A⁰ (FractionRing A)
hI : I ≠ ⊥
a : A
J : Ideal A
ha : a ≠ 0
hJ :
  I =
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a)⁻¹ :
        FractionalIdeal (R := A) A⁰ (FractionRing A))
      ((↑J : FractionalIdeal (R := A) A⁰ (FractionRing A)) : FractionalIdeal (R := A) A⁰ (FractionRing A))
subst :
  ∀
    (hI :
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
          (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a)⁻¹ :
            FractionalIdeal (R := A) A⁰ (FractionRing A))
          ((↑J : FractionalIdeal (R := A) A⁰ (FractionRing A)) : FractionalIdeal (R := A) A⁰ (FractionRing A)) ≠
        ⊥),
    HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
          (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a)⁻¹ :
            FractionalIdeal (R := A) A⁰ (FractionRing A))
          ((↑J : FractionalIdeal (R := A) A⁰ (FractionRing A)) : FractionalIdeal (R := A) A⁰ (FractionRing A)) *
        HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β :=
          FractionalIdeal (R := A) A⁰ (FractionRing A))
          (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a) :
            FractionalIdeal (R := A) A⁰ (FractionRing A))
          ((↑J : FractionalIdeal A⁰ (FractionRing A))⁻¹ : FractionalIdeal (R := A) A⁰ (FractionRing A)) =
      1
⊢ I *
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
        (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a) :
          FractionalIdeal (R := A) A⁰ (FractionRing A))
        ((↑J : FractionalIdeal A⁰ (FractionRing A))⁻¹ : FractionalIdeal (R := A) A⁰ (FractionRing A)) =
    1

Tactic:
subst hJ
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : IsDedekindDomain A
I : Ideal A
a : A
J : Ideal A
ha : a ≠ 0
hI :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a)⁻¹ :
        FractionalIdeal (R := A) A⁰ (FractionRing A))
      ((↑J : FractionalIdeal (R := A) A⁰ (FractionRing A)) : FractionalIdeal (R := A) A⁰ (FractionRing A)) ≠
    ⊥
rw :
  Ne (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a : FractionRing A)
    (0 : FractionRing A)
hI0 : J ≠ ⊥
⊢ HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
        (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a)⁻¹ :
          FractionalIdeal (R := A) A⁰ (FractionRing A))
        ((↑J : FractionalIdeal (R := A) A⁰ (FractionRing A)) : FractionalIdeal (R := A) A⁰ (FractionRing A)) *
      HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
        (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a) :
          FractionalIdeal (R := A) A⁰ (FractionRing A))
        ((↑J : FractionalIdeal A⁰ (FractionRing A))⁻¹ : FractionalIdeal (R := A) A⁰ (FractionRing A)) =
    1

Tactic:
rw [mul_assoc, mul_left_comm (J : FractionalIdeal A⁰ _), coe_ideal_mul_inv, mul_one,
      spanSingleton_mul_spanSingleton, inv_mul_cancel₀, spanSingleton_one]

Premises used: FractionalIdeal.spanSingleton_mul_spanSingleton, mul_assoc, mul_left_comm, FractionalIdeal.coe_ideal_mul_inv, FractionalIdeal.spanSingleton_one, mul_one, FractionalIdeal.coeIdeal, inv_mul_cancel₀
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : IsDedekindDomain A
I : Ideal A
a : A
J : Ideal A
ha : a ≠ 0
hI :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a)⁻¹ :
        FractionalIdeal (R := A) A⁰ (FractionRing A))
      ((↑J : FractionalIdeal (R := A) A⁰ (FractionRing A)) : FractionalIdeal (R := A) A⁰ (FractionRing A)) ≠
    ⊥
⊢ Ne (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a : FractionRing A)
    (0 : FractionRing A)

Tactic:
mt ((injective_iff_map_eq_zero (algebraMap A _)).mp (IsFractionRing.injective A _) _) ha

Premises used: Algebra.algebraMap, IsFractionRing.injective, mt, injective_iff_map_eq_zero, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : IsDedekindDomain A
I : Ideal A
a : A
J : Ideal A
ha : a ≠ 0
hI :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a)⁻¹ :
        FractionalIdeal (R := A) A⁰ (FractionRing A))
      ((↑J : FractionalIdeal (R := A) A⁰ (FractionRing A)) : FractionalIdeal (R := A) A⁰ (FractionRing A)) ≠
    ⊥
⊢ Ne (α := FractionRing A) ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a : FractionRing A)
    (0 : FractionRing A)

Tactic:
exact mt ((injective_iff_map_eq_zero (algebraMap A _)).mp (IsFractionRing.injective A _) _) ha

Premises used: Algebra.algebraMap, IsFractionRing.injective, mt, injective_iff_map_eq_zero, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : IsDedekindDomain A
I : Ideal A
a : A
J : Ideal A
ha : a ≠ 0
hI :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a)⁻¹ :
        FractionalIdeal (R := A) A⁰ (FractionRing A))
      ((↑J : FractionalIdeal (R := A) A⁰ (FractionRing A)) : FractionalIdeal (R := A) A⁰ (FractionRing A)) ≠
    ⊥
⊢ J ≠ ⊥

Tactic:
coeIdeal_ne_zero.mp (right_ne_zero_of_mul hI)

Premises used: right_ne_zero_of_mul, Iff.mp, FractionalIdeal.coeIdeal_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : IsDedekindDomain A
I : Ideal A
a : A
J : Ideal A
ha : a ≠ 0
hI :
  HMul.hMul (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) (β := FractionalIdeal (R := A) A⁰ (FractionRing A))
      (spanSingleton A⁰ ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) a)⁻¹ :
        FractionalIdeal (R := A) A⁰ (FractionRing A))
      ((↑J : FractionalIdeal (R := A) A⁰ (FractionRing A)) : FractionalIdeal (R := A) A⁰ (FractionRing A)) ≠
    ⊥
⊢ J ≠ ⊥

Tactic:
exact coeIdeal_ne_zero.mp (right_ne_zero_of_mul hI)

Premises used: right_ne_zero_of_mul, Iff.mp, FractionalIdeal.coeIdeal_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : IsDedekindDomain A
I : Ideal A
⊢ PosMulStrictMono.{u_3} (FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)

Tactic:
PosMulMono.toPosMulStrictMono

Premises used: PosMulMono.toPosMulStrictMono
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : IsDedekindDomain A
I : Ideal A
⊢ MulPosStrictMono.{u_3} (FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)

Tactic:
MulPosMono.toMulPosStrictMono

Premises used: MulPosMono.toMulPosStrictMono
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K_1 : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K_1
inst_3 : Algebra A K_1
inst_4 : IsFractionRing A K_1
inst_5 : IsDedekindDomain A
I_1 : Ideal A
I : { x : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1 // 0 < x }
J K : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1
hJK :
  (fun (x1 x2 : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1) ↦ x1 ≤ x2)
    ((fun (x : { x : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1 // 0 < x })
          (y : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1) ↦
        (↑x : FractionalIdeal A⁰ K_1) * y)
      I J)
    ((fun (x : { x : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1 // 0 < x })
          (y : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1) ↦
        (↑x : FractionalIdeal A⁰ K_1) * y)
      I K)
⊢ (fun (x1 x2 : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1) ↦ x1 ≤ x2) J K

Tactic:
simpa [I.2.ne'] using mul_right_mono (a := I.1⁻¹) hJK

Premises used: mul_right_mono, LT.lt.ne', Subtype.property
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K_1 : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K_1
inst_3 : Algebra A K_1
inst_4 : IsFractionRing A K_1
inst_5 : IsDedekindDomain A
I_1 : Ideal A
I : { x : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1 // 0 < x }
J K : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1
hJK :
  (fun (x1 x2 : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1) ↦ x1 ≤ x2)
    ((fun (x : { x : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1 // 0 < x })
          (y : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1) ↦
        y * (↑x : FractionalIdeal A⁰ K_1))
      I J)
    ((fun (x : { x : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1 // 0 < x })
          (y : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1) ↦
        y * (↑x : FractionalIdeal A⁰ K_1))
      I K)
⊢ (fun (x1 x2 : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K_1) ↦ x1 ≤ x2) J K

Tactic:
simpa [I.2.ne'] using mul_left_mono (a := I.1⁻¹) hJK

Premises used: mul_left_mono, LT.lt.ne', Subtype.property
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hI : I ≠ 0
⊢ StrictMono (β := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) fun (x : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦ x * I

Tactic:
fun _J _K hJK ↦ mul_lt_mul_of_pos_right hJK <| pos_iff_ne_zero.2 hI

Premises used: Iff.mpr, StrictMono, mul_lt_mul_of_pos_right, pos_iff_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDedekindDomain A
I : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
hI : I ≠ 0
⊢ StrictMono (β := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) fun (x : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦ I * x

Tactic:
fun _J _K hJK ↦ mul_lt_mul_of_pos_left hJK <| pos_iff_ne_zero.2 hI

Premises used: Iff.mpr, StrictMono, mul_lt_mul_of_pos_left, pos_iff_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Goal:
R : Type u_1
A : Type u_2
K_1 : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K_1
inst_3 : Algebra A K_1
inst_4 : IsFractionRing A K_1
inst_5 : IsDedekindDomain A
I_1 : Ideal A
I : { x : Ideal A // 0 < x }
J K : Ideal A
e :
  (fun (x1 x2 : Ideal A) ↦ x1 ≤ x2) ((fun (x : { x : Ideal A // 0 < x }) (y : Ideal A) ↦ (↑x : Ideal A) * y) I J)
    ((fun (x : { x : Ideal A // 0 < x }) (y : Ideal A) ↦ (↑x : Ideal A) * y) I K)
⊢ LT.lt (α := FractionalIdeal (R := A) A⁰ (FractionRing A)) 0 (↑(↑I : Ideal A) : FractionalIdeal A⁰ (FractionRing A))

Tactic:
simpa [pos_iff_ne_zero] using I.2.ne'

Premises used: LT.lt.ne', pos_iff_ne_zero, Subtype.property