-- 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 k✝ : Fin m
h : ¬f k✝ ≤ a
i : Fin m
hij : ¬i < k✝
hia : f i ≤ a
⊢ f k✝ ≤ a

Tactic:
exact (h_sorted (le_of_not_lt hij)).trans hia

Result:
no goals

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 }
⊢ False

Tactic:
apply hw.ne'

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 }
⊢ 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 { i // f i ≤ a } ≤ m

Tactic:
conv_rhs => rw [← Fintype.card_fin m]

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 { i // f i ≤ a } ≤ Fintype.card (Fin m)

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 { i // f i ≤ a } ≤ Fintype.card (Fin m)

Tactic:
exact Fintype.card_subtype_le _

Result:
no goals

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 ∉ Finset.Iio k✝ → i ∉ Finset.filter (fun x => f x ≤ a) Finset.univ

Tactic:
simp_rw [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_Iio]

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 < k✝ → ¬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
⊢ ∀ (k : Fin m), ↑k < Fintype.card { i // f i ≤ a } → f k ≤ a

Tactic:
intro _ 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 : ↑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
⊢ Fintype.card { i // f i ≤ a } ≤ ↑k✝

Tactic:
rw [← Fin.card_Iio, Fintype.card_subtype]

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
⊢ (Finset.filter (fun x => f x ≤ a) Finset.univ).card ≤ (Finset.Iio k✝).card

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
⊢ False

Tactic:
let p : Fin m → Prop := fun x ↦ f x ≤ 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
⊢ 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 }
q' : { i // f i ≤ a } → Prop := fun x => q ↑x
⊢ False

Tactic:
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⟩⟩

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 }
⊢ 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 }
q' : { i // f i ≤ a } → Prop := fun x => q ↑x
hw : 0 < Fintype.card { j // ¬q' j }
⊢ Fintype.card { j // ¬q' j } = 0

Tactic:
have he := Fintype.card_congr <| Equiv.sumCompl <| q'

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 }
⊢ Fintype.card { j // ¬q' j } = 0