-- Mathlib/RingTheory/ChainOfDivisors.lean
theorem card_subset_divisors_le_length_of_chain {q : Associates M} {n : ℕ}
    {c : Fin (n + 1) → Associates M} (h₂ : ∀ {r}, r ≤ q ↔ ∃ i, r = c i) {m : Finset (Associates M)}
    (hm : ∀ r, r ∈ m → r ≤ q) : m.card ≤ n + 1

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
r : Associates M
hr : r ≤ q
⊢ r ∈ Finset.image c Finset.univ

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

Result:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, 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

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
mem_image : ∀ r ≤ q, r ∈ Finset.image c Finset.univ
⊢ m.card ≤ n + 1

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

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, 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.univ.card

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
⊢ 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

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
⊢ ∀ r ≤ q, r ∈ Finset.image c Finset.univ

Tactic:
intro r hr

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
r : Associates M
hr : r ≤ q
⊢ r ∈ Finset.image c Finset.univ

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, 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.univ.card

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

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
⊢ m.card ≤ n + 1

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⟩

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
m : Finset (Associates M)
hm : ∀ r ∈ m, r ≤ q
mem_image : ∀ r ≤ q, r ∈ Finset.image c Finset.univ
⊢ m.card ≤ n + 1

Proof state:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, 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⟩

Result:
no goals