awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
⊢ 2 ≤ ringKrullDim ℕ

Tactic:
le_iSup_of_le ⟨2, ![⊥, ⟨_, (span_singleton_prime two_ne_zero).mpr <| Nat.prime_iff.mp
      Nat.prime_two⟩, ⟨_, (maximalIdeal.isMaximal ℕ).isPrime⟩], fun i ↦ ?_⟩ le_rfl

Premises used: Iff.mpr, PrimeSpectrum.mk, le_rfl, Nat.prime_iff, Bot.bot, Ideal.IsMaximal.isPrime, Order.krullDim, Nat.prime_two, two_ne_zero, IsLocalRing.maximalIdeal.isMaximal, le_iSup_of_le, Nat, Matrix.vecEmpty, Iff.mp, ringKrullDim, Ideal.span_singleton_prime, OfNat.ofNat, Matrix.vecCons, RelSeries.mk
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
refine_2 :
  ∀ (i : Fin 2),
    Membership.mem (γ := SetRel (PrimeSpectrum ℕ) (PrimeSpectrum ℕ))
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b}
      (![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
            { asIdeal := maximalIdeal ℕ, isPrime := ⋯ : PrimeSpectrum ℕ }]
          i.castSucc,
        ![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
            { asIdeal := maximalIdeal ℕ, isPrime := ⋯ : PrimeSpectrum ℕ }]
          i.succ)
⊢ 2 ≤ ringKrullDim ℕ

Tactic:
refine le_iSup_of_le ⟨2, ![⊥, ⟨_, (span_singleton_prime two_ne_zero).mpr <| Nat.prime_iff.mp
      Nat.prime_two⟩, ⟨_, (maximalIdeal.isMaximal ℕ).isPrime⟩], fun i ↦ ?_⟩ le_rfl

Premises used: le_rfl, le_iSup_of_le
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
i : Fin 2
refine_2 :
  Membership.mem (γ := SetRel (PrimeSpectrum ℕ) (PrimeSpectrum ℕ))
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b}
    (![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := maximalIdeal ℕ, isPrime := ⋯ : PrimeSpectrum ℕ }]
        (Fin.castSucc ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))),
      ![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := maximalIdeal ℕ, isPrime := ⋯ : PrimeSpectrum ℕ }]
        (Fin.succ ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))))
refine_2₁ :
  Membership.mem (γ := SetRel (PrimeSpectrum ℕ) (PrimeSpectrum ℕ))
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b}
    (![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := maximalIdeal ℕ, isPrime := ⋯ : PrimeSpectrum ℕ }]
        (Fin.castSucc ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))),
      ![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := maximalIdeal ℕ, isPrime := ⋯ : PrimeSpectrum ℕ }]
        (Fin.succ ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))))
⊢ Membership.mem (γ := SetRel (PrimeSpectrum ℕ) (PrimeSpectrum ℕ))
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b}
    (![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := maximalIdeal ℕ, isPrime := ⋯ : PrimeSpectrum ℕ }]
        i.castSucc,
      ![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := maximalIdeal ℕ, isPrime := ⋯ : PrimeSpectrum ℕ }]
        i.succ)

Tactic:
fin_cases i
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
⊢ Membership.mem (γ := SetRel (PrimeSpectrum ℕ) (PrimeSpectrum ℕ))
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b}
    (![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := maximalIdeal ℕ, isPrime := ⋯ : PrimeSpectrum ℕ }]
        (Fin.castSucc ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))),
      ![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := maximalIdeal ℕ, isPrime := ⋯ : PrimeSpectrum ℕ }]
        (Fin.succ ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))))

Tactic:
bot_lt_iff_ne_bot.mpr (Ideal.span_singleton_eq_bot.not.mpr two_ne_zero)

Premises used: Iff.mpr, Ideal.span_singleton_eq_bot, Set.Mem, setOf, bot_lt_iff_ne_bot, Iff.not, two_ne_zero
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
⊢ Membership.mem (γ := SetRel (PrimeSpectrum ℕ) (PrimeSpectrum ℕ))
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b}
    (![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := maximalIdeal ℕ, isPrime := ⋯ : PrimeSpectrum ℕ }]
        (Fin.castSucc ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))),
      ![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := maximalIdeal ℕ, isPrime := ⋯ : PrimeSpectrum ℕ }]
        (Fin.succ ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))))

Tactic:
exact bot_lt_iff_ne_bot.mpr (Ideal.span_singleton_eq_bot.not.mpr two_ne_zero)

Premises used: Iff.mpr, Ideal.span_singleton_eq_bot, bot_lt_iff_ne_bot, Iff.not, two_ne_zero
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
refine_2 :
  Membership.mem (γ := SetRel (PrimeSpectrum ℕ) (PrimeSpectrum ℕ)) {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ | x.1 < x.2}
    (![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := span {2, 3}, isPrime := ⋯ : PrimeSpectrum ℕ }]
        (Fin.castSucc (⟨1, ⋯⟩ : Fin 2)),
      ![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := span {2, 3}, isPrime := ⋯ : PrimeSpectrum ℕ }]
        (Fin.succ (⟨1, ⋯⟩ : Fin 2)))
⊢ Membership.mem (γ := SetRel (PrimeSpectrum ℕ) (PrimeSpectrum ℕ))
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b}
    (![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := maximalIdeal ℕ, isPrime := ⋯ : PrimeSpectrum ℕ }]
        (Fin.castSucc ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))),
      ![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := maximalIdeal ℕ, isPrime := ⋯ : PrimeSpectrum ℕ }]
        (Fin.succ ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))))

Tactic:
simp_rw [Nat.maximalIdeal_eq_span_two_three]

Premises used: Nat.maximalIdeal_eq_span_two_three
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
⊢ Subset (α := Set ℕ) {2} {2, 3}

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
⊢ Membership.mem (γ := Set ℕ) {2, 3} 3

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
⊢ ¬Dvd.dvd (α := ℕ) 2 3

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
⊢ Membership.mem (γ := SetRel (PrimeSpectrum ℕ) (PrimeSpectrum ℕ)) {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ | x.1 < x.2}
    (![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := span {2, 3}, isPrime := ⋯ : PrimeSpectrum ℕ }]
        (Fin.castSucc (⟨1, ⋯⟩ : Fin 2)),
      ![⊥, { asIdeal := span {2}, isPrime := ⋯ : PrimeSpectrum ℕ },
          { asIdeal := span {2, 3}, isPrime := ⋯ : PrimeSpectrum ℕ }]
        (Fin.succ (⟨1, ⋯⟩ : Fin 2)))

Tactic:
exact SetLike.lt_iff_le_and_exists.mpr ⟨Ideal.span_mono (by simp),
        3, Ideal.subset_span (by simp), Ideal.mem_span_singleton.not.mpr <| by simp⟩

Premises used: Iff.mpr, SetLike.lt_iff_le_and_exists, Ideal.subset_span, Iff.not, And.intro, Exists.intro, Ideal.span_mono, Ideal.mem_span_singleton, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
a : α
inst : Monoid α
⊢ a ∈ nonunits α ↔ ¬IsUnit a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, nonunits, Not
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
a b : α
inst : CommMonoid α
⊢ b ∈ nonunits α → a * b ∈ nonunits α

Tactic:
mt isUnit_of_mul_isUnit_right

Premises used: Set.Mem, setOf, nonunits, mt, isUnit_of_mul_isUnit_right, Not
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
a b : α
inst : CommMonoid α
⊢ a ∈ nonunits α → a * b ∈ nonunits α

Tactic:
mt isUnit_of_mul_isUnit_left

Premises used: Set.Mem, setOf, nonunits, mt, isUnit_of_mul_isUnit_left, Not
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
inst : MonoidWithZero α
⊢ 0 ∈ nonunits α ↔ Ne.{u_2 + 1} (α := α) 0 1

Tactic:
not_congr isUnit_zero_iff

Premises used: Set.Mem, setOf, nonunits, isUnit_zero_iff, Not, not_congr
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
inst : Monoid α
⊢ 1 ∉ nonunits α

Tactic:
not_not_intro isUnit_one

Premises used: Set.Mem, setOf, nonunits, not_not_intro, isUnit_one, Not
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Monoid α
inst_1 : Monoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
inst_4 : IsLocalHom.{u_2, u_3, u_1} (R := α) (S := β) f
a : α
⊢ Membership.mem (α := β) (nonunits β) ((f : (a : α) → β) a : β) ↔ a ∈ nonunits α

Tactic:
⟨fun h ha => h <| ha.map f, fun h ha => h <| ha.of_map⟩

Premises used: IsUnit.of_map, Iff.intro, IsUnit.map
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
inst : Semiring α
I : Ideal α
h : I ≠ ⊤
⊢ (↑I : Set α) ⊆ nonunits α

Tactic:
fun _x hx hu => h <| I.eq_top_of_isUnit_mem hx hu

Premises used: Set.Mem, setOf, Ideal.eq_top_of_isUnit_mem, nonunits, Set.Subset, Not
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
a : α
inst : CommSemiring α
h : a ∈ nonunits α
H : Eq (α := Ideal α) (Ideal.span {a}) ⊤
⊢ IsUnit a

Tactic:
rw [Ideal.span_singleton_eq_top] at H

Premises used: Ideal.span_singleton_eq_top
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
a : α
inst : CommSemiring α
h : a ∈ nonunits α
H : IsUnit a
⊢ False

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
a : α
inst : CommSemiring α
h : a ∈ nonunits α
⊢ Ne (α := Ideal α) (Ideal.span {a}) ⊤

Tactic:
have : Ideal.span ({a} : Set α) ≠ ⊤ := by
    intro H
    rw [Ideal.span_singleton_eq_top] at H
    contradiction
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
a : α
inst : CommSemiring α
h : a ∈ nonunits α
this : Ne (α := Ideal α) (Ideal.span {a}) ⊤
rcases : ∀ (I : Ideal α) (Imax : I.IsMaximal) (H : Ideal.span {a} ≤ I), ∃ (I : Ideal α), I.IsMaximal ∧ a ∈ I
⊢ ∃ (I : Ideal α), I.IsMaximal ∧ a ∈ I

Tactic:
rcases Ideal.exists_le_maximal _ this with ⟨I, Imax, H⟩

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
a : α
inst : CommSemiring α
h : a ∈ nonunits α
this : Ne (α := Ideal α) (Ideal.span {a}) ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
right : a ∈ I
⊢ ∃ (I : Ideal α), I.IsMaximal ∧ a ∈ I

Tactic:
use I, Imax
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
a : α
inst : CommSemiring α
h : a ∈ nonunits α
this : Ne (α := Ideal α) (Ideal.span {a}) ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
right : Membership.mem (γ := Submodule α α) (Ideal.span {a}) a
⊢ a ∈ I

Tactic:
apply H
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
a : α
inst : CommSemiring α
h : a ∈ nonunits α
this : Ne (α := Ideal α) (Ideal.span {a}) ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
right : Membership.mem (γ := Set α) {a} a
⊢ Membership.mem (γ := Submodule α α) (Ideal.span {a}) a

Tactic:
apply Ideal.subset_span

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
a : α
inst : CommSemiring α
h : a ∈ nonunits α
this : Ne (α := Ideal α) (Ideal.span {a}) ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
⊢ Membership.mem (γ := Set α) {a} a

Tactic:
Set.mem_singleton a

Premises used: Set.mem_singleton
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
a : α
inst : CommSemiring α
h : a ∈ nonunits α
this : Ne (α := Ideal α) (Ideal.span {a}) ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
⊢ Membership.mem (γ := Set α) {a} a

Tactic:
exact Set.mem_singleton a

Premises used: Set.mem_singleton
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
C : Type u_4
inst : SetLike C α
inst_1 : DivisionMonoid α
inst_2 : SubmonoidClass C α
S : C
a : ↥S
ha : IsUnit a
obtain : ∀ (u : (↥S)ˣ), (↑(↑u : ↥S) : α)⁻¹ ∈ S
⊢ (↑a : α)⁻¹ ∈ S

Tactic:
obtain ⟨u, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
C : Type u_4
inst : SetLike C α
inst_1 : DivisionMonoid α
inst_2 : SubmonoidClass C α
S : C
u : (↥S)ˣ
⊢ (↑(↑u⁻¹ : ↥S) : α) ∈ S

Tactic:
u⁻¹.1.2

Premises used: Units.val, Inv.inv, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
C : Type u_4
inst : SetLike C α
inst_1 : DivisionMonoid α
inst_2 : SubmonoidClass C α
S : C
u : (↥S)ˣ
h : (↑(↑u : ↥S) : α)⁻¹ = (↑(↑u⁻¹ : ↥S) : α)
⊢ (↑(↑u : ↥S) : α)⁻¹ ∈ S

Tactic:
convert! u⁻¹.1.2

Premises used: Units.val, Inv.inv, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
C : Type u_4
inst : SetLike C α
inst_1 : DivisionMonoid α
inst_2 : SubmonoidClass C α
S : C
u : (↥S)ˣ
⊢ (↑(↑u : ↥S) : α)⁻¹ = (↑(↑u⁻¹ : ↥S) : α)

Tactic:
(map_inv ((subtype <| ofClass S).comp <| Units.coeHom S) u).symm

Premises used: Units.coeHom, map_inv, Submonoid.ofClass, Membership.mem, Subtype, MonoidHom.comp, Submonoid.subtype, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
C : Type u_4
inst : SetLike C α
inst_1 : DivisionMonoid α
inst_2 : SubmonoidClass C α
S : C
u : (↥S)ˣ
⊢ (↑(↑u : ↥S) : α)⁻¹ = (↑(↑u⁻¹ : ↥S) : α)

Tactic:
exact (map_inv ((subtype <| ofClass S).comp <| Units.coeHom S) u).symm

Premises used: Units.coeHom, map_inv, Submonoid.ofClass, Membership.mem, Subtype, MonoidHom.comp, Submonoid.subtype, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
C : Type u_4
inst : SetLike C α
inst_1 : Group α
inst_2 : SubmonoidClass C α
S : C
a : ↥S
rw : ¬IsUnit a ↔ (↑a : α)⁻¹ ∉ S
rw₁ rw₂ : (↑a : α)⁻¹ ∉ S ↔ (↑a : α)⁻¹ ∉ S
⊢ Membership.mem (γ := Set ↥S) (nonunits ↥S) a ↔ (↑a : α)⁻¹ ∉ S

Tactic:
rw [mem_nonunits_iff, isUnit_iff]

Premises used: mem_nonunits_iff, Submonoid.isUnit_iff
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
C : Type u_4
inst : SetLike C α
inst_1 : GroupWithZero α
inst_2 : SubmonoidClass C α
S : C
a : ↥S
ha : (↑a : α) ≠ 0
rw : (↑a : α) ≠ 0 ∧ (↑a : α)⁻¹ ∈ S ↔ (↑a : α)⁻¹ ∈ S
rw₁ rw₂ : (↑a : α)⁻¹ ∈ S ↔ (↑a : α)⁻¹ ∈ S
⊢ IsUnit a ↔ (↑a : α)⁻¹ ∈ S

Tactic:
rw [isUnit_iff_and, and_iff_right ha]

Premises used: Submonoid.isUnit_iff_and, and_iff_right
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
C : Type u_4
inst : SetLike C α
inst_1 : GroupWithZero α
inst_2 : SubmonoidClass C α
S : C
a : ↥S
rw : ¬IsUnit a ↔ (↑a : α) = 0 ∨ (↑a : α)⁻¹ ∉ S
rw₁ : ¬((↑a : α) ≠ 0 ∧ (↑a : α)⁻¹ ∈ S) ↔ (↑a : α) = 0 ∨ (↑a : α)⁻¹ ∉ S
rw₂ : ¬(↑a : α) ≠ 0 ∨ (↑a : α)⁻¹ ∉ S ↔ (↑a : α) = 0 ∨ (↑a : α)⁻¹ ∉ S
rw₃ : ¬¬(↑a : α) = 0 ∨ (↑a : α)⁻¹ ∉ S ↔ (↑a : α) = 0 ∨ (↑a : α)⁻¹ ∉ S
rw₄ rw₅ : (↑a : α) = 0 ∨ (↑a : α)⁻¹ ∉ S ↔ (↑a : α) = 0 ∨ (↑a : α)⁻¹ ∉ S
⊢ Membership.mem (γ := Set ↥S) (nonunits ↥S) a ↔ (↑a : α) = 0 ∨ (↑a : α)⁻¹ ∉ S

Tactic:
rw [mem_nonunits_iff, isUnit_iff_and, not_and_or, Ne, not_not]

Premises used: Submonoid.isUnit_iff_and, Classical.not_not, mem_nonunits_iff, Ne, not_and_or
-- Module: Mathlib.RingTheory.Ideal.Nonunits
Goal:
α : Type u_2
C : Type u_4
inst : SetLike C α
inst_1 : GroupWithZero α
inst_2 : SubmonoidClass C α
S : C
a : ↥S
ha : (↑a : α) ≠ 0
rw : (↑a : α) = 0 ∨ (↑a : α)⁻¹ ∉ S ↔ (↑a : α)⁻¹ ∉ S
rw₁ rw₂ : (↑a : α)⁻¹ ∉ S ↔ (↑a : α)⁻¹ ∉ S
⊢ Membership.mem (γ := Set ↥S) (nonunits ↥S) a ↔ (↑a : α)⁻¹ ∉ S

Tactic:
rw [mem_nonunits_iff_or, or_iff_right ha]

Premises used: Submonoid.mem_nonunits_iff_or, or_iff_right
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
⊢ S.cardQuot = Nat.card.{u_2} (M ⧸ S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Infinite M
⊢ cardQuot.{u_1, u_2} (R := R) (M := M) ⊥ = 0

Tactic:
AddSubgroup.index_bot.trans Nat.card_eq_zero_of_infinite

Premises used: Nat.card_eq_zero_of_infinite, Submodule.cardQuot, Eq.trans, AddSubgroup.index_bot
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ cardQuot.{u_1, u_2} (R := R) (M := M) ⊤ = 1

Tactic:
AddSubgroup.index_top

Premises used: Submodule.cardQuot, AddSubgroup.index_top
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
P : Submodule R M
⊢ P.toAddSubgroup = ⊤ ↔ P = ⊤

Tactic:
simp [SetLike.ext_iff]

Premises used: SetLike.ext_iff
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
I J : Ideal S
coprime : IsCoprime I J
rw : Nat.card.{u_1} (S ⧸ I * J) = cardQuot.{u_1, u_1} (R := S) (M := S) I * cardQuot.{u_1, u_1} (R := S) (M := S) J
rw₁ : Nat.card.{u_1} (S ⧸ I * J) = Nat.card.{u_1} (S ⧸ I) * cardQuot.{u_1, u_1} (R := S) (M := S) J
rw₂ : Nat.card.{u_1} (S ⧸ I * J) = Nat.card.{u_1} (S ⧸ I) * Nat.card.{u_1} (S ⧸ J)
rw₃ : Nat.card.{u_1} ((S ⧸ I) × S ⧸ J) = Nat.card.{u_1} (S ⧸ I) * Nat.card.{u_1} (S ⧸ J)
rw₄ rw₅ : Nat.card.{u_1} (S ⧸ I) * Nat.card.{u_1} (S ⧸ J) = Nat.card.{u_1} (S ⧸ I) * Nat.card.{u_1} (S ⧸ J)
⊢ cardQuot.{u_1, u_1} (R := S) (M := S) (I * J) =
    cardQuot.{u_1, u_1} (R := S) (M := S) I * cardQuot.{u_1, u_1} (R := S) (M := S) J

Tactic:
rw [cardQuot_apply, cardQuot_apply, cardQuot_apply,
    Nat.card_congr (Ideal.quotientMulEquivQuotientProd I J coprime).toEquiv,
    Nat.card_prod]

Premises used: RingEquiv.toEquiv, Ideal.quotientMulEquivQuotientProd, Nat.card_congr, Nat.card_prod, Submodule.cardQuot_apply
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
simp : a * (d - d') ∈ P ^ (i + 1)
⊢ a * d - a * d' ∈ P ^ (i + 1)

Tactic:
simp only [← mul_sub]

Premises used: mul_sub
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ a * (d - d') ∈ P ^ (i + 1)

Tactic:
Ideal.mul_mem_mul a_mem h

Premises used: Set.Mem, Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ a * (d - d') ∈ P ^ (i + 1)

Tactic:
exact Ideal.mul_mem_mul a_mem h

Premises used: Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ a * d - a * d' ∈ P ^ (i + 1)

Tactic:
have : a * d - a * d' ∈ P ^ (i + 1) := by
    simp only [← mul_sub]
    exact Ideal.mul_mem_mul a_mem h
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
this : a * d - a * d' ∈ P ^ (i + 1)
⊢ a * d - a * d' + (e - e') ∈ P ^ (i + 1)

Tactic:
Ideal.add_mem _ this (Ideal.sub_mem _ e_mem e'_mem)

Premises used: Ideal.add_mem, Ideal.sub_mem
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
this : a * d - a * d' ∈ P ^ (i + 1)
h₁ : a * d + e - (a * d' + e') = a * d - a * d' + (e - e')
⊢ a * d + e - (a * d' + e') ∈ P ^ (i + 1)

Tactic:
convert! Ideal.add_mem _ this (Ideal.sub_mem _ e_mem e'_mem) using 1

Premises used: Ideal.add_mem, Ideal.sub_mem
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
this : a * d - a * d' ∈ P ^ (i + 1)
⊢ a * d + e - (a * d' + e') = a * d - a * d' + (e - e')

Tactic:
ring
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ P ^ i
eq_b : P ^ i = span {a} ⊔ P ^ (i + 1)
⊢ c ∈ span {a} ⊔ P ^ (i + 1)

Tactic:
rw [eq_b] at c_mem
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ P ^ i
eq_b : P ^ i = span {a} ⊔ P ^ (i + 1)
c_mem₁ : c ∈ span {a} ⊔ P ^ (i + 1)
⊢ P ^ i = span {a} ⊔ P ^ (i + 1)

Tactic:
rw [eq_b] at c_mem
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ span {a} ⊔ P ^ (i + 1)
eq_b : P ^ i = span {a} ⊔ P ^ (i + 1)
simp : ∃ (d : S), ∃ e ∈ P ^ (i + 1), d * a + e = c
⊢ ∃ (d : S), ∃ e ∈ P ^ (i + 1), a * d + e = c

Tactic:
simp only [mul_comm a]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ span {a} ⊔ P ^ (i + 1)
eq_b : P ^ i = span {a} ⊔ P ^ (i + 1)
⊢ ∃ (d : S), ∃ e ∈ P ^ (i + 1), d * a + e = c

Tactic:
Ideal.mem_span_singleton_sup.mp c_mem

Premises used: Ideal.mem_span_singleton_sup, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ span {a} ⊔ P ^ (i + 1)
eq_b : P ^ i = span {a} ⊔ P ^ (i + 1)
⊢ ∃ (d : S), ∃ e ∈ P ^ (i + 1), d * a + e = c

Tactic:
exact Ideal.mem_span_singleton_sup.mp c_mem

Premises used: Ideal.mem_span_singleton_sup, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ P ^ i
suffices : P ^ i = span {a} ⊔ P ^ (i + 1)
⊢ ∃ (d : S), ∃ e ∈ P ^ (i + 1), a * d + e = c

Tactic:
suffices eq_b : P ^ i = Ideal.span {a} ⊔ P ^ (i + 1) by
    rw [eq_b] at c_mem
    simp only [mul_comm a]
    exact Ideal.mem_span_singleton_sup.mp c_mem
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ P ^ i
⊢ P ^ i = span {a} ⊔ P ^ (i + 1)

Tactic:
(Ideal.eq_prime_pow_of_succ_lt_of_le hP (lt_of_le_of_ne le_sup_right ?_)
    (sup_le (Ideal.span_le.mpr (Set.singleton_subset_iff.mpr a_mem))
      (Ideal.pow_succ_lt_pow hP i).le)).symm

Premises used: Ideal.span_le, Iff.mpr, Set.singleton_subset_iff, Ideal.pow_succ_lt_pow, Ideal.eq_prime_pow_of_succ_lt_of_le, LT.lt.le, le_sup_right, sup_le, Eq.symm, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ P ^ i
refine : P ^ (i + 1) ≠ span {a} ⊔ P ^ (i + 1)
⊢ P ^ i = span {a} ⊔ P ^ (i + 1)

Tactic:
refine (Ideal.eq_prime_pow_of_succ_lt_of_le hP (lt_of_le_of_ne le_sup_right ?_)
    (sup_le (Ideal.span_le.mpr (Set.singleton_subset_iff.mpr a_mem))
      (Ideal.pow_succ_lt_pow hP i).le)).symm

Premises used: Ideal.span_le, Iff.mpr, Set.singleton_subset_iff, Ideal.pow_succ_lt_pow, Ideal.eq_prime_pow_of_succ_lt_of_le, LT.lt.le, le_sup_right, sup_le, Eq.symm, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a c : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
c_mem : c ∈ P ^ i
contrapose : ∀ (this : P ^ (i + 1) = span {a} ⊔ P ^ (i + 1)), a ∈ P ^ (i + 1)
⊢ P ^ (i + 1) ≠ span {a} ⊔ P ^ (i + 1)

Tactic:
contrapose a_notMem with this