-- Mathlib/Data/Matroid/IndepAxioms.lean
theorem _root_.Matroid.existsMaximalSubsetProperty_of_bdd {P : Set α → Prop}
    (hP : ∃ (n : ℕ), ∀ Y, P Y → Y.encard ≤ n) (X : Set α) : ExistsMaximalSubsetProperty P X

Proof state:
case intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
⊢ ExistsMaximalSubsetProperty P X

Tactic:
rintro I hI hIX

Result:
case intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K => P K ∧ K ⊆ X) J

Proof state:
case h.intro.intro.intro.intro.intro.intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ n₀, Y.encard = ↑n₀ ∧ n₀ ≤ n
Y : Set α
hY : P Y
n₀ : ℕ
heq : Y.encard = ↑n₀
hle : n₀ ≤ n
⊢ Y.ncard ≤ n

Tactic:
rwa [ncard_def, heq, ENat.toNat_coe]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' : ∀ a' ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, Y.ncard ≤ a'.ncard → Y.ncard = a'.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
K : Set α
x✝ : (fun K => P K ∧ K ⊆ X) K
hYK : Y ≤ K
hPK : P K
hKX : K ⊆ X
hKfin : K.Finite
⊢ K.ncard ≤ Y.ncard

Tactic:
rw [hY' K ⟨hPK, hIY.trans hYK, hKX⟩ (ncard_le_ncard hYK hKfin)]

Result:
no goals

Proof state:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
⊢ ∃ x, ∀ y ∈ ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ x

Tactic:
simp_rw [ENat.le_coe_iff] at hP

Result:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ n₀, Y.encard = ↑n₀ ∧ n₀ ≤ n
⊢ ∃ x, ∀ y ∈ ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ x

Proof state:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ n₀, Y.encard = ↑n₀ ∧ n₀ ≤ n
⊢ ∃ x, ∀ y ∈ ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ x

Tactic:
use n

Result:
case h
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ n₀, Y.encard = ↑n₀ ∧ n₀ ≤ n
⊢ ∀ y ∈ ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ n

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' : ∀ a' ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, Y.ncard ≤ a'.ncard → Y.ncard = a'.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
K : Set α
x✝ : (fun K => P K ∧ K ⊆ X) K
hYK : Y ≤ K
hPK : P K
hKX : K ⊆ X
hKfin : K.Finite
⊢ K ≤ Y

Tactic:
refine (eq_of_subset_of_ncard_le hYK ?_ hKfin).symm.subset

Result:
case intro.intro.intro.intro.intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' : ∀ a' ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, Y.ncard ≤ a'.ncard → Y.ncard = a'.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
K : Set α
x✝ : (fun K => P K ∧ K ⊆ X) K
hYK : Y ≤ K
hPK : P K
hKX : K ⊆ X
hKfin : K.Finite
⊢ K.ncard ≤ Y.ncard

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' : ∀ a' ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, Y.ncard ≤ a'.ncard → Y.ncard = a'.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
K : Set α
x✝ : (fun K => P K ∧ K ⊆ X) K
hYK : Y ≤ K
hPK : P K
hKX : K ⊆ X
⊢ K ≤ Y

Tactic:
have hKfin : K.Finite := finite_of_encard_le_coe (hP K hPK)

Result:
case intro.intro.intro.intro.intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' : ∀ a' ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, Y.ncard ≤ a'.ncard → Y.ncard = a'.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
K : Set α
x✝ : (fun K => P K ∧ K ⊆ X) K
hYK : Y ≤ K
hPK : P K
hKX : K ⊆ X
hKfin : K.Finite
⊢ K ≤ Y

Proof state:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
⊢ (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite

Tactic:
rw [finite_iff_bddAbove, bddAbove_def]

Result:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
⊢ ∃ x, ∀ y ∈ ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ x

Proof state:
case h
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ n₀, Y.encard = ↑n₀ ∧ n₀ ≤ n
⊢ ∀ y ∈ ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ n

Tactic:
rintro x ⟨Y, ⟨hY,-,-⟩, rfl⟩

Result:
case h.intro.intro.intro.intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ n₀, Y.encard = ↑n₀ ∧ n₀ ≤ n
Y : Set α
hY : P Y
⊢ Y.ncard ≤ n

Proof state:
case intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K => P K ∧ K ⊆ X) J

Tactic:
have hfin : Set.Finite (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}) := by
  rw [finite_iff_bddAbove, bddAbove_def]
  simp_rw [ENat.le_coe_iff] at hP
  use n
  rintro x ⟨Y, ⟨hY,-,-⟩, rfl⟩
  obtain ⟨n₀, heq, hle⟩ := hP Y hY
  rwa [ncard_def, heq, ENat.toNat_coe]

Result:
case intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K => P K ∧ K ⊆ X) J

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' : ∀ a' ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, Y.ncard ≤ a'.ncard → Y.ncard = a'.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K => P K ∧ K ⊆ X) J

Tactic:
refine ⟨Y, hIY, ⟨hY, hYX⟩, fun K ⟨hPK, hKX⟩ hYK ↦ ?_⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' : ∀ a' ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, Y.ncard ≤ a'.ncard → Y.ncard = a'.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
K : Set α
x✝ : (fun K => P K ∧ K ⊆ X) K
hYK : Y ≤ K
hPK : P K
hKX : K ⊆ X
⊢ K ≤ Y

Proof state:
case h.intro.intro.intro.intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ n₀, Y.encard = ↑n₀ ∧ n₀ ≤ n
Y : Set α
hY : P Y
⊢ Y.ncard ≤ n

Tactic:
obtain ⟨n₀, heq, hle⟩ := hP Y hY

Result:
case h.intro.intro.intro.intro.intro.intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ n₀, Y.encard = ↑n₀ ∧ n₀ ≤ n
Y : Set α
hY : P Y
n₀ : ℕ
heq : Y.encard = ↑n₀
hle : n₀ ≤ n
⊢ Y.ncard ≤ n

Proof state:
α : Type u_1
P : Set α → Prop
hP : ∃ n, ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
X : Set α
⊢ ExistsMaximalSubsetProperty P X

Tactic:
obtain ⟨n, hP⟩ := hP

Result:
case intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
⊢ ExistsMaximalSubsetProperty P X