-- Mathlib/Order/Partition/Finpartition.lean
theorem card_mono {a : α} {P Q : Finpartition a} (h : P ≤ Q) : #Q.parts ≤ #P.parts

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
⊢ #Q.parts ≤ #P.parts

Tactic:
rw [← card_attach]

Result:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
⊢ #Q.parts.attach ≤ #P.parts

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h✝ : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
b : { x // x ∈ Q.parts }
x✝¹ : b ∈ ↑Q.parts.attach
c : { x // x ∈ Q.parts }
x✝ : c ∈ ↑Q.parts.attach
h : (fun b => f ↑b ⋯) b = (fun b => f ↑b ⋯) c
⊢ b = c

Tactic:
exact
  Subtype.coe_injective
    (Q.disjoint.elim b.2 c.2 fun H ↦
      P.ne_bot (hP _ b.2) <| disjoint_self.1 <| H.mono (hf _ b.2) <| h.le.trans <| hf _ c.2)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
⊢ #Q.parts.attach ≤ #P.parts

Tactic:
refine card_le_card_of_injOn (fun b ↦ f _ b.2) (fun b _ ↦ hP _ b.2) fun b _ c _ h ↦ ?_

Result:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h✝ : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
b : { x // x ∈ Q.parts }
x✝¹ : b ∈ ↑Q.parts.attach
c : { x // x ∈ Q.parts }
x✝ : c ∈ ↑Q.parts.attach
h : (fun b => f ↑b ⋯) b = (fun b => f ↑b ⋯) c
⊢ b = c

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
⊢ #Q.parts ≤ #P.parts

Tactic:
classical
  have : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b := fun b ↦ exists_le_of_le h
  choose f hP hf using this
  rw [← card_attach]
  refine card_le_card_of_injOn (fun b ↦ f _ b.2) (fun b _ ↦ hP _ b.2) fun b _ c _ h ↦ ?_
  exact
    Subtype.coe_injective
      (Q.disjoint.elim b.2 c.2 fun H ↦
        P.ne_bot (hP _ b.2) <| disjoint_self.1 <| H.mono (hf _ b.2) <| h.le.trans <| hf _ c.2)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
⊢ #Q.parts ≤ #P.parts

Tactic:
have : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b := fun b ↦ exists_le_of_le h

Result:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
this : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b
⊢ #Q.parts ≤ #P.parts

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
this : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b
⊢ #Q.parts ≤ #P.parts

Tactic:
choose f hP hf using this

Result:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
⊢ #Q.parts ≤ #P.parts