-- Mathlib/Combinatorics/Additive/CauchyDavenport.lean
/-- The **Cauchy-Davenport Theorem** for linearly ordered cancellative semigroups. The size of
`s * t` is lower-bounded by `|s| + |t| - 1`. -/
@[to_additive
"The **Cauchy-Davenport theorem** for linearly ordered additive cancellative semigroups. The size of
`s + t` is lower-bounded by `|s| + |t| - 1`."]
lemma cauchy_davenport_mul_of_linearOrder_isCancelMul [LinearOrder α] [Semigroup α] [IsCancelMul α]
    [MulLeftMono α] [MulRightMono α]
    {s t : Finset α} (hs : s.Nonempty) (ht : t.Nonempty) : #s + #t - 1 ≤ #(s * t)

Proof state:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : Semigroup α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this : s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
⊢ #s + #t - 1 ≤ #(s * t)

Tactic:
rw [← card_singleton_mul (s.max' hs) t, ← card_mul_singleton s (t.min' ht),
  ← card_union_add_card_inter, ← card_singleton _, ← this, Nat.add_sub_cancel]

Result:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : Semigroup α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this : s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
⊢ #(s * {t.min' ht} ∪ {s.max' hs} * t) ≤ #(s * t)

Proof state:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : Semigroup α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}

Tactic:
refine eq_singleton_iff_unique_mem.2 ⟨mem_inter.2 ⟨mul_mem_mul (max'_mem _ _) <|
  mem_singleton_self _, mul_mem_mul (mem_singleton_self _) <| min'_mem _ _⟩, ?_⟩

Result:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : Semigroup α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ x ∈ s * {t.min' ht} ∩ ({s.max' hs} * t), x = s.max' hs * t.min' ht

Proof state:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : Semigroup α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this : s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
⊢ #(s * {t.min' ht} ∪ {s.max' hs} * t) ≤ #(s * t)

Tactic:
exact card_mono (union_subset (mul_subset_mul_left <| singleton_subset_iff.2 <| min'_mem _ _) <|
  mul_subset_mul_right <| singleton_subset_iff.2 <| max'_mem _ _)

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : Semigroup α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ a ∈ s, ∀ x ∈ t, s.max' hs * x = a * t.min' ht → a = s.max' hs

Tactic:
exact fun a' ha' b' hb' h ↦ (le_max' _ _ ha').eq_of_not_lt fun ha ↦
  ((mul_lt_mul_right' ha _).trans_eq' h).not_le <| mul_le_mul_left' (min'_le _ _ hb') _

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : Semigroup α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ #s + #t - 1 ≤ #(s * t)

Tactic:
suffices s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht} by
  rw [← card_singleton_mul (s.max' hs) t, ← card_mul_singleton s (t.min' ht),
    ← card_union_add_card_inter, ← card_singleton _, ← this, Nat.add_sub_cancel]
  exact card_mono (union_subset (mul_subset_mul_left <| singleton_subset_iff.2 <| min'_mem _ _) <|
    mul_subset_mul_right <| singleton_subset_iff.2 <| max'_mem _ _)

Result:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : Semigroup α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}

Proof state:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : Semigroup α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ x ∈ s * {t.min' ht} ∩ ({s.max' hs} * t), x = s.max' hs * t.min' ht

Tactic:
simp only [mem_inter, and_imp, mem_mul, mem_singleton, exists_and_left, exists_eq_left,
  forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mul_left_inj]

Result:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : Semigroup α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ ∀ a ∈ s, ∀ x ∈ t, s.max' hs * x = a * t.min' ht → a = s.max' hs