-- Mathlib/Data/Fin/Tuple/Sort.lean
theorem lt_card_le_iff_apply_le_of_monotone [PartialOrder α] [DecidableRel (α := α) LE.le]
    {m : ℕ} (f : Fin m → α) (a : α) (h_sorted : Monotone f) (j : Fin m) :
    j < Fintype.card {i // f i ≤ a} ↔ f j ≤ a

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
⊢ ↑j < Fintype.card { i // f i ≤ a } ↔ f j ≤ a

Tactic:
suffices h1 : ∀ k : Fin m, (k < Fintype.card {i // f i ≤ a}) → f k ≤ a by
  refine ⟨h1 j, fun h ↦ ?_⟩
  by_contra! hc
  let p : Fin m → Prop := fun x ↦ f x ≤ a
  let q : Fin m → Prop := fun x ↦ x < Fintype.card {i // f i ≤ a}
  let q' : {i // f i ≤ a} → Prop := fun x ↦ q x
  have hw : 0 < Fintype.card {j : {x : Fin m // f x ≤ a} // ¬ q' j} :=
    Fintype.card_pos_iff.2 ⟨⟨⟨j, h⟩, not_lt.2 hc⟩⟩
  apply hw.ne'
  have he := Fintype.card_congr <| Equiv.sumCompl <| q'
  have h4 := (Fintype.card_congr (@Equiv.subtypeSubtypeEquivSubtype _ p q (h1 _)))
  have h_le : Fintype.card { i // f i ≤ a } ≤ m := by
    conv_rhs => rw [← Fintype.card_fin m]
    exact Fintype.card_subtype_le _
  rwa [Fintype.card_sum, h4, Fintype.card_fin_lt_of_le h_le, add_right_eq_self] at he

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
⊢ ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j k✝ : Fin m
h : ¬f k✝ ≤ a
i : Fin m
hij : ¬i < k✝
hia : f i ≤ a
⊢ False

Tactic:
apply h

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j k✝ : Fin m
h : ¬f k✝ ≤ a
i : Fin m
hij : ¬i < k✝
hia : f i ≤ a
⊢ f k✝ ≤ a

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j k✝ : Fin m
h : ¬f k✝ ≤ a
⊢ (Finset.filter (fun x => f x ≤ a) Finset.univ).card ≤ (Finset.Iio k✝).card

Tactic:
refine Finset.card_mono (fun i => Function.mtr ?_)

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j k✝ : Fin m
h : ¬f k✝ ≤ a
i : Fin m
⊢ i ∉ Finset.Iio k✝ → i ∉ Finset.filter (fun x => f x ≤ a) Finset.univ

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
h1 : ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a
⊢ ↑j < Fintype.card { i // f i ≤ a } ↔ f j ≤ a

Tactic:
refine ⟨h1 j, fun h ↦ ?_⟩

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
h1 : ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a
h : f j ≤ a
⊢ ↑j < Fintype.card { i // f i ≤ a }

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
h1 : ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a
h : f j ≤ a
hc : Fintype.card { i // f i ≤ a } ≤ ↑j
p : Fin m → Prop := fun x => f x ≤ a
q : Fin m → Prop := fun x => ↑x < Fintype.card { i // f i ≤ a }
q' : { i // f i ≤ a } → Prop := fun x => q ↑x
hw : 0 < Fintype.card { j // ¬q' j }
he : Fintype.card ({ a // q' a } ⊕ { a // ¬q' a }) = Fintype.card { i // f i ≤ a }
⊢ Fintype.card { j // ¬q' j } = 0

Tactic:
have h4 := (Fintype.card_congr (@Equiv.subtypeSubtypeEquivSubtype _ p q (h1 _)))

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
h1 : ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a
h : f j ≤ a
hc : Fintype.card { i // f i ≤ a } ≤ ↑j
p : Fin m → Prop := fun x => f x ≤ a
q : Fin m → Prop := fun x => ↑x < Fintype.card { i // f i ≤ a }
q' : { i // f i ≤ a } → Prop := fun x => q ↑x
hw : 0 < Fintype.card { j // ¬q' j }
he : Fintype.card ({ a // q' a } ⊕ { a // ¬q' a }) = Fintype.card { i // f i ≤ a }
h4 : Fintype.card { x // q ↑x } = Fintype.card (Subtype q)
⊢ Fintype.card { j // ¬q' j } = 0

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
h1 : ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a
h : f j ≤ a
hc : Fintype.card { i // f i ≤ a } ≤ ↑j
p : Fin m → Prop := fun x => f x ≤ a
q : Fin m → Prop := fun x => ↑x < Fintype.card { i // f i ≤ a }
q' : { i // f i ≤ a } → Prop := fun x => q ↑x
hw : 0 < Fintype.card { j // ¬q' j }
he : Fintype.card ({ a // q' a } ⊕ { a // ¬q' a }) = Fintype.card { i // f i ≤ a }
h4 : Fintype.card { x // q ↑x } = Fintype.card (Subtype q)
⊢ Fintype.card { j // ¬q' j } = 0

Tactic:
have h_le : Fintype.card { i // f i ≤ a } ≤ m := by
  conv_rhs => rw [← Fintype.card_fin m]
  exact Fintype.card_subtype_le _

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
h1 : ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a
h : f j ≤ a
hc : Fintype.card { i // f i ≤ a } ≤ ↑j
p : Fin m → Prop := fun x => f x ≤ a
q : Fin m → Prop := fun x => ↑x < Fintype.card { i // f i ≤ a }
q' : { i // f i ≤ a } → Prop := fun x => q ↑x
hw : 0 < Fintype.card { j // ¬q' j }
he : Fintype.card ({ a // q' a } ⊕ { a // ¬q' a }) = Fintype.card { i // f i ≤ a }
h4 : Fintype.card { x // q ↑x } = Fintype.card (Subtype q)
h_le : Fintype.card { i // f i ≤ a } ≤ m
⊢ Fintype.card { j // ¬q' j } = 0

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j k✝ : Fin m
h : ¬f k✝ ≤ a
i : Fin m
⊢ ¬i < k✝ → ¬f i ≤ a

Tactic:
intro hij hia

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j k✝ : Fin m
h : ¬f k✝ ≤ a
i : Fin m
hij : ¬i < k✝
hia : f i ≤ a
⊢ False

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j k✝ : Fin m
h : ↑k✝ < Fintype.card { i // f i ≤ a }
⊢ f k✝ ≤ a

Tactic:
contrapose! h

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j k✝ : Fin m
h : ¬f k✝ ≤ a
⊢ Fintype.card { i // f i ≤ a } ≤ ↑k✝

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
h1 : ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a
h : f j ≤ a
hc : Fintype.card { i // f i ≤ a } ≤ ↑j
p : Fin m → Prop := fun x => f x ≤ a
⊢ False

Tactic:
let q : Fin m → Prop := fun x ↦ x < Fintype.card {i // f i ≤ a}

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
h1 : ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a
h : f j ≤ a
hc : Fintype.card { i // f i ≤ a } ≤ ↑j
p : Fin m → Prop := fun x => f x ≤ a
q : Fin m → Prop := fun x => ↑x < Fintype.card { i // f i ≤ a }
⊢ False

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
h1 : ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a
h : f j ≤ a
hc : Fintype.card { i // f i ≤ a } ≤ ↑j
p : Fin m → Prop := fun x => f x ≤ a
q : Fin m → Prop := fun x => ↑x < Fintype.card { i // f i ≤ a }
⊢ False

Tactic:
let q' : {i // f i ≤ a} → Prop := fun x ↦ q x

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableRel LE.le
m : ℕ
f : Fin m → α
a : α
h_sorted : Monotone f
j : Fin m
h1 : ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a
h : f j ≤ a
hc : Fintype.card { i // f i ≤ a } ≤ ↑j
p : Fin m → Prop := fun x => f x ≤ a
q : Fin m → Prop := fun x => ↑x < Fintype.card { i // f i ≤ a }
q' : { i // f i ≤ a } → Prop := fun x => q ↑x
⊢ False