awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1 + 1)), r = c i
j : Fin (n + 1)
hp : Prime (c j.succ)
hp' : c j.succ ∣ r
hi : 1 < j.succ
succ : j.castSucc < j.succ
⊢ DvdNotUnit (c j.castSucc) (c j.succ)

Tactic:
refine Associates.dvdNotUnit_iff_lt.2 (h₁ ?_)

Premises used: Iff.mpr, Associates.dvdNotUnit_iff_lt
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1 + 1)), r = c i
j : Fin (n + 1)
hp : Prime (c j.succ)
hp' : c j.succ ∣ r
hi : 1 < j.succ
⊢ j.castSucc < j.succ

Tactic:
simpa only [Fin.coe_eq_castSucc] using Fin.castSucc_lt_succ

Premises used: Fin.castSucc_lt_succ, Fin.coe_eq_castSucc
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
r : Associates M
hr : r ≤ q
obtain : ∀ (i : Fin (n + 1)) (hi : r = c i), r ∈ Finset.image c Finset.univ
⊢ r ∈ Finset.image c Finset.univ

Tactic:
obtain ⟨i, hi⟩ := h₂.1 hr

Premises used: Iff.mp
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
r : Associates M
hr : r ≤ q
i : Fin (n + 1)
hi : r = c i
⊢ r ∈ Finset.image c Finset.univ

Tactic:
Finset.mem_image.2 ⟨i, Finset.mem_univ _, hi.symm⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_image, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
r : Associates M
hr : r ≤ q
i : Fin (n + 1)
hi : r = c i
⊢ r ∈ Finset.image c Finset.univ

Tactic:
exact Finset.mem_image.2 ⟨i, Finset.mem_univ _, hi.symm⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_image, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
⊢ ∀ r ≤ q, r ∈ Finset.image c Finset.univ

Tactic:
have mem_image : ∀ r : Associates M, r ≤ q → r ∈ Finset.univ.image c := by
      intro r hr
      obtain ⟨i, hi⟩ := h₂.1 hr
      exact Finset.mem_image.2 ⟨i, Finset.mem_univ _, hi.symm⟩
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
mem_image : ∀ r ≤ q, r ∈ Finset.image c Finset.univ
rw : m.card ≤ Finset.card (α := Fin (n + 1)) Finset.univ
⊢ m.card ≤ n + 1

Tactic:
rw [← Finset.card_fin (n + 1)]

Premises used: HAdd.hAdd, Finset.card_fin, OfNat.ofNat
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
mem_image : ∀ r ≤ q, r ∈ Finset.image c Finset.univ
⊢ m.card ≤ Finset.card (α := Fin (n + 1)) Finset.univ

Tactic:
(Finset.card_le_card fun x hx => mem_image x <| hm x hx).trans Finset.card_image_le

Premises used: Finset.card_le_card, Finset.card_image_le, LE.le.trans
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
mem_image : ∀ r ≤ q, r ∈ Finset.image c Finset.univ
⊢ m.card ≤ Finset.card (α := Fin (n + 1)) Finset.univ

Tactic:
exact (Finset.card_le_card fun x hx => mem_image x <| hm x hx).trans Finset.card_image_le

Premises used: Finset.card_le_card, Finset.card_image_le, LE.le.trans
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
have : ∀ r ≤ q, r ∈ Finset.image c Finset.univ
have₁ : ∀ (mem_image : ∀ r ≤ q, r ∈ Finset.image c Finset.univ), m.card ≤ n + 1
have₂ : ∀ r ≤ q, r ∈ Finset.image c Finset.univ
have₃ have₄ : ∀ (mem_image : ∀ r ≤ q, r ∈ Finset.image c Finset.univ), m.card ≤ n + 1
have₅ : ∀ (mem_image : ∀ r ≤ q, r ∈ Finset.image c Finset.univ), m.card ≤ Finset.card (α := Fin (n + 1)) Finset.univ
⊢ m.card ≤ n + 1

Tactic:
classical
    have mem_image : ∀ r : Associates M, r ≤ q → r ∈ Finset.univ.image c := by
      intro r hr
      obtain ⟨i, hi⟩ := h₂.1 hr
      exact Finset.mem_image.2 ⟨i, Finset.mem_univ _, hi.symm⟩
    rw [← Finset.card_fin (n + 1)]
    exact (Finset.card_le_card fun x hx => mem_image x <| hm x hx).trans Finset.card_image_le

Premises used: HAdd.hAdd, Finset.card_fin, OfNat.ofNat
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
a : ∀ b ∈ normalizedFactors r, b = c 1
⊢ normalizedFactors r = Multiset.replicate i (c 1)

Tactic:
apply Multiset.eq_replicate_of_mem

Premises used: Multiset.eq_replicate_of_mem
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
b : Associates M
hb : b ∈ normalizedFactors r
⊢ b = c 1

Tactic:
eq_second_of_chain_of_prime_dvd hn h₁ (@fun r' => h₂) (prime_of_normalized_factor b hb) hr
          (dvd_of_mem_normalizedFactors hb)

Premises used: UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, UniqueFactorizationMonoid.prime_of_normalized_factor, DivisorChain.eq_second_of_chain_of_prime_dvd
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
b : Associates M
hb : b ∈ normalizedFactors r
⊢ b = c 1

Tactic:
refine
        eq_second_of_chain_of_prime_dvd hn h₁ (@fun r' => h₂) (prime_of_normalized_factor b hb) hr
          (dvd_of_mem_normalizedFactors hb)

Premises used: UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, UniqueFactorizationMonoid.prime_of_normalized_factor, DivisorChain.eq_second_of_chain_of_prime_dvd
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
⊢ normalizedFactors r = Multiset.replicate i (c 1)

Tactic:
have hi : normalizedFactors r = Multiset.replicate i (c 1) := by
      apply Multiset.eq_replicate_of_mem
      intro b hb
      refine
        eq_second_of_chain_of_prime_dvd hn h₁ (@fun r' => h₂) (prime_of_normalized_factor b hb) hr
          (dvd_of_mem_normalizedFactors hb)
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
⊢ Associated (normalizedFactors r).prod r

Tactic:
have := UniqueFactorizationMonoid.prod_normalizedFactors (ne_zero_of_dvd_ne_zero hq hr)
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
this : Associated (normalizedFactors r).prod r
⊢ c 1 ^ i = r

Tactic:
rw [associated_iff_eq, hi, Multiset.prod_replicate] at this

Premises used: Multiset.prod_replicate, associated_iff_eq
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
this : c 1 ^ i = r
rw rw₁ : r = r
⊢ r = c 1 ^ i

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
⊢ r = c 1 ^ i

Tactic:
have H : r = c 1 ^ i := by
      have := UniqueFactorizationMonoid.prod_normalizedFactors (ne_zero_of_dvd_ne_zero hq hr)
      rw [associated_iff_eq, hi, Multiset.prod_replicate] at this
      rw [this]
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ ∃ (i : Fin (n + 1)), r = c 1 ^ (↑i : ℕ)

Tactic:
⟨⟨i, ?_⟩, H⟩

Premises used: Fin.mk, Exists.intro
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
refine : i < n + 1
⊢ ∃ (i : Fin (n + 1)), r = c 1 ^ (↑i : ℕ)

Tactic:
refine ⟨⟨i, ?_⟩, H⟩
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
rw : Finset.card (α := Fin (i + 1)) Finset.univ
| i + 1

Tactic:
rw [← Finset.card_fin (i + 1)]

Premises used: HAdd.hAdd, Finset.card_fin, OfNat.ofNat
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
conv_rhs :
  Finset.card.{u_1} (α := Associates M) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) =
    Finset.card (α := Fin (i + 1)) Finset.univ
⊢ Finset.card.{u_1} (α := Associates M) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) = i + 1

Tactic:
conv_rhs => rw [← Finset.card_fin (i + 1)]

Premises used: HAdd.hAdd, Finset.card_fin, OfNat.ofNat
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
zero :
  ∀ (hn : Ne (α := ℕ) 0 0) {c : Fin (HAdd.hAdd (α := ℕ) 0 1) → Associates M} (h₁ : StrictMono c)
    (h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), r = c i)
    (hi : normalizedFactors r = Multiset.replicate i (c 1)) (H : r = c 1 ^ i),
    Finset.card.{u_1} (α := Associates M) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) =
      Finset.card (α := Fin (i + 1)) Finset.univ
succ :
  ∀ (n : ℕ) (hn : n + 1 ≠ 0) {c : Fin (n + 1 + 1) → Associates M} (h₁ : StrictMono c)
    (h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1 + 1)), r = c i)
    (hi : normalizedFactors r = Multiset.replicate i (c 1)) (H : r = c 1 ^ i),
    Finset.card.{u_1} (α := Associates M) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) =
      Finset.card (α := Fin (i + 1)) Finset.univ
⊢ Finset.card.{u_1} (α := Associates M) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) =
    Finset.card (α := Fin (i + 1)) Finset.univ

Tactic:
cases n
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hn : Ne (α := ℕ) 0 0
c : Fin (HAdd.hAdd (α := ℕ) 0 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ Finset.card.{u_1} (α := Associates M) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) =
    Finset.card (α := Fin (i + 1)) Finset.univ

Tactic:
contradiction
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1 + 1)), r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
succ :
  Set.InjOn.{0, u_1} (β := Associates M) (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) (↑Finset.univ : Set (Fin (i + 1)))
⊢ Finset.card.{u_1} (α := Associates M) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) =
    Finset.card (α := Fin (i + 1)) Finset.univ

Tactic:
rw [Finset.card_image_iff]

Premises used: Finset.card_image_iff
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1 + 1)), r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ Set.InjOn.{0, u_1} (β := Associates M) (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) (↑Finset.univ : Set (Fin (i + 1)))

Tactic:
Set.injOn_of_injective (fun m m' h => Fin.ext ?_)

Premises used: Fin.ext, Set.injOn_of_injective
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1 + 1)), r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
succ : ∀ (m m' : Fin (i + 1)) (h : c 1 ^ (↑m : ℕ) = c 1 ^ (↑m' : ℕ)), (↑m : ℕ) = (↑m' : ℕ)
⊢ Set.InjOn.{0, u_1} (β := Associates M) (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) (↑Finset.univ : Set (Fin (i + 1)))

Tactic:
refine Set.injOn_of_injective (fun m m' h => Fin.ext ?_)

Premises used: Fin.ext, Set.injOn_of_injective
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1 + 1)), r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
m m' : Fin (i + 1)
h : c 1 ^ (↑m : ℕ) = c 1 ^ (↑m' : ℕ)
⊢ Ne (α := Fin (n + 1 + 1)) 1 0

Tactic:
simp
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1 + 1)), r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
m m' : Fin (i + 1)
h : c 1 ^ (↑m : ℕ) = c 1 ^ (↑m' : ℕ)
succ : c 1 ≠ 0
⊢ (↑m : ℕ) = (↑m' : ℕ)

Tactic:
refine
        pow_injective_of_not_isUnit (element_of_chain_not_isUnit_of_index_ne_zero (by simp) h₁) ?_ h

Premises used: pow_injective_of_not_isUnit, DivisorChain.element_of_chain_not_isUnit_of_index_ne_zero
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1 + 1)), r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
m m' : Fin (i + 1)
h : c 1 ^ (↑m : ℕ) = c 1 ^ (↑m' : ℕ)
⊢ c 1 ≠ 0

Tactic:
Irreducible.ne_zero (second_of_chain_is_irreducible hn h₁ (@h₂) hq)

Premises used: DivisorChain.second_of_chain_is_irreducible, Irreducible.ne_zero
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1 + 1)), r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
m m' : Fin (i + 1)
h : c 1 ^ (↑m : ℕ) = c 1 ^ (↑m' : ℕ)
⊢ c 1 ≠ 0

Tactic:
exact Irreducible.ne_zero (second_of_chain_is_irreducible hn h₁ (@h₂) hq)

Premises used: DivisorChain.second_of_chain_is_irreducible, Irreducible.ne_zero
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ Finset.card.{u_1} (α := Associates M) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) = i + 1

Tactic:
have : (Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ)).card = i + 1 := by
      conv_rhs => rw [← Finset.card_fin (i + 1)]
      cases n
      · contradiction
      rw [Finset.card_image_iff]
      refine Set.injOn_of_injective (fun m m' h => Fin.ext ?_)
      refine
        pow_injective_of_not_isUnit (element_of_chain_not_isUnit_of_index_ne_zero (by simp) h₁) ?_ h
      exact Irreducible.ne_zero (second_of_chain_is_irreducible hn h₁ (@h₂) hq)
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : Finset.card.{u_1} (α := Associates M) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) = i + 1
H' :
  ∀ (r : Associates M),
    Membership.mem (γ := Finset (Associates M)) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) r →
      r ≤ q
simp : Finset.card.{u_1} (α := Associates M) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) ≤ n + 1
⊢ i < n + 1

Tactic:
simp only [← Nat.succ_le_iff, Nat.succ_eq_add_one, ← this]

Premises used: Nat.succ_eq_add_one, Nat.succ_le_iff
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : Finset.card.{u_1} (α := Associates M) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) = i + 1
H' :
  ∀ (r : Associates M),
    Membership.mem (γ := Finset (Associates M)) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) r →
      r ≤ q
⊢ Finset.card.{u_1} (α := Associates M) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) ≤ n + 1

Tactic:
apply card_subset_divisors_le_length_of_chain (@h₂) H'

Premises used: DivisorChain.card_subset_divisors_le_length_of_chain
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : Finset.card.{u_1} (α := Associates M) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) = i + 1
suffices :
  ∀ (r : Associates M),
    Membership.mem (γ := Finset (Associates M)) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) r →
      r ≤ q
⊢ i < n + 1

Tactic:
suffices H' : ∀ r ∈ Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ), r ≤ q by
      simp only [← Nat.succ_le_iff, Nat.succ_eq_add_one, ← this]
      apply card_subset_divisors_le_length_of_chain (@h₂) H'
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : Finset.card.{u_1} (α := Associates M) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) = i + 1
simp :
  ∀ (r : Associates M),
    (∃ (a : Fin (i + 1)), Membership.mem (γ := Finset (Fin (i + 1))) Finset.univ a ∧ c 1 ^ (↑a : ℕ) = r) → r ≤ q
⊢ ∀ (r : Associates M),
    Membership.mem (γ := Finset (Associates M)) (Finset.image (fun (m : Fin (i + 1)) ↦ c 1 ^ (↑m : ℕ)) Finset.univ) r →
      r ≤ q

Tactic:
simp only [Finset.mem_image]

Premises used: Finset.mem_image