Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ min (minOrder α) ↑(#s + #t - 1) ≤ ↑(#(s * t))

Tactic:
by
  -- Set up the induction on `x := (s, t)` along the `DevosMulRel` relation.
  set x := (s, t) with hx
  clear_value x
  simp only [Prod.ext_iff] at hx
  obtain ⟨rfl, rfl⟩ := hx
  refine wellFoundedOn_devosMulRel.induction (P := fun x : Finset α × Finset α ↦
    min (minOrder α) ↑(#x.1 + #x.2 - 1) ≤ #(x.1 * x.2)) ⟨hs, ht⟩ ?_
  clear! x
  rintro ⟨s, t⟩ ⟨hs, ht⟩ ih
  simp only [min_le_iff, tsub_le_iff_right, Prod.forall, Set.mem_ofPred_eq, and_imp,
    Nat.cast_le] at *
  -- If `#t < #s`, we're done by the induction hypothesis on `(t⁻¹, s⁻¹)`.
  obtain hts | hst := lt_or_ge #t #s
  · simpa only [← mul_inv_rev, add_comm, card_inv] using
      ih _ _ ht.inv hs.inv
        (devosMulRel_iff.2 <| Or.inr <| Or.inr <| by
          simpa only [← mul_inv_rev, add_comm, card_inv, true_and])
  -- If `s` is a singleton, then the result is trivial.
  obtain ⟨a, rfl⟩ | ⟨a, ha, b, hb, hab⟩ := hs.exists_eq_singleton_or_nontrivial
  · simp [add_comm]
  -- Else, we have `a, b ∈ s` distinct. So `g := b⁻¹ * a` is a non-identity element such that `s`
  -- intersects its right translate by `g`.
  obtain ⟨g, hg, hgs⟩ : ∃ g : α, g ≠ 1 ∧ (s ∩ op g • s).Nonempty :=
    ⟨b⁻¹ * a, inv_mul_eq_one.not.2 hab.symm, _,
      mem_inter.2 ⟨ha, mem_smul_finset.2 ⟨_, hb, by simp⟩⟩⟩
  -- If `s` is equal to its right translate by `g`, then it contains a nontrivial subgroup, namely
  -- the subgroup generated by `g`. So `s * t` has size at least the size of a nontrivial subgroup,
  -- as wanted.
  obtain hsg | hsg := eq_or_ne (op g • s) s
  · have hS : (zpowers g : Set α) ⊆ a⁻¹ • (s : Set α) := by
      refine forall_mem_zpowers.2 <| @zpow_induction_right _ _ _ (· ∈ a⁻¹ • (s : Set α))
        ⟨_, ha, inv_mul_cancel _⟩ (fun c hc ↦ ?_) fun c hc ↦ ?_
      · rw [← hsg, coe_smul_finset, smul_comm]
        exact Set.smul_mem_smul_set hc
      · rwa [← op_smul_eq_mul, op_inv, ← Set.mem_smul_set_iff_inv_smul_mem, smul_comm,
          ← coe_smul_finset, hsg]
    refine Or.inl ((minOrder_le_natCard (zpowers_ne_bot.2 hg) <|
      s.finite_toSet.smul_set.subset hS).trans <| WithTop.coe_le_coe.2 <|
        ((Nat.card_mono s.finite_toSet.smul_set hS).trans_eq <| ?_).trans <|
          card_le_card_mul_right ht)
    rw [← coe_smul_finset]
    simp [-coe_smul_finset]
  -- Else, we can transform `s`, `t` to `s'`, `t'` and `s''`, `t''`, such that one of `(s', t')` and
  -- `(s'', t'')` is strictly smaller than `(s, t)` according to `DevosMulRel`.
  replace hsg : #(s ∩ op g • s) < #s := card_lt_card ⟨inter_subset_left, fun h ↦
    hsg <| eq_of_superset_of_card_ge (h.trans inter_subset_right) (card_smul_finset _ _).le⟩
  replace aux1 := card_mono <| mulETransformLeft.fst_mul_snd_subset g (s, t)
  replace aux2 := card_mono <| mulETransformRight.fst_mul_snd_subset g (s, t)
  -- If the left translate of `t` by `g⁻¹` is disjoint from `t`, then we're easily done.
  obtain hgt | hgt := disjoint_or_nonempty_inter t (g⁻¹ • t)
  · rw [← card_smul_finset g⁻¹ t]
    right
    grw [hst, ← card_union_of_disjoint hgt]
    exact (card_le_card_mul_left hgs).trans (le_add_of_le_left aux1)
  -- Else, we're done by induction on either `(s', t')` or `(s'', t'')` depending on whether
  -- `|s| + |t| ≤ |s'| + |t'|` or `|s| + |t| < |s''| + |t''|`. One of those two inequalities must
  -- hold since `2 * (|s| + |t|) = |s'| + |t'| + |s''| + |t''|`.
  obtain hstg | hstg := le_or_lt_of_add_le_add (MulETransform.card g (s, t)).ge
  · exact (ih _ _ hgs (hgt.mono inter_subset_union) <| devosMulRel_of_le_of_le aux1 hstg hsg).imp
      (WithTop.coe_le_coe.2 aux1).trans' fun h ↦ hstg.trans <| h.trans <| add_le_add_left aux1 _
  · exact (ih _ _ (hgs.mono inter_subset_union) hgt <| devosMulRel_of_le aux2 hstg).imp
      (WithTop.coe_le_coe.2 aux2).trans' fun h ↦
        hstg.le.trans <| h.trans <| add_le_add_left aux2 _

Goal state after: