-- Mathlib/Combinatorics/Additive/CauchyDavenport.lean
/-- A generalisation of the **Cauchy-Davenport theorem** to arbitrary groups. The size of `s * t` is
lower-bounded by `|s| + |t| - 1` unless this quantity is greater than the size of the smallest
subgroup. -/
@[to_additive "A generalisation of the **Cauchy-Davenport theorem** to arbitrary groups. The size of
`s + t` is lower-bounded by `|s| + |t| - 1` unless this quantity is greater than the size of the
smallest subgroup."]
lemma cauchy_davenport_minOrder_mul (hs : s.Nonempty) (ht : t.Nonempty) :
    min (minOrder α) ↑(#s + #t - 1) ≤ #(s * t)

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
⊢ op (b⁻¹ * a) • b = a

Tactic:
simp

Result:
no goals

Proof state:
case intro.mk.intro.inr.inr.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

Tactic:
replace aux2 := card_mono <| mulETransformRight.fst_mul_snd_subset g (s, t)

Result:
case intro.mk.intro.inr.inr.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

Proof state:
case refine_1
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : (fun x => x ∈ a⁻¹ • ↑s) c
⊢ (fun x => x ∈ a⁻¹ • ↑s) (c * g)

Tactic:
rw [← hsg, coe_smul_finset, smul_comm]

Result:
case refine_1
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : (fun x => x ∈ a⁻¹ • ↑s) c
⊢ (fun x => x ∈ op g • a⁻¹ • ↑s) (c * g)

Proof state:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
x : Finset α × Finset α
hs : x.1.Nonempty
ht : x.2.Nonempty
⊢ ∀ y ∈ {x | x.1.Nonempty ∧ x.2.Nonempty},
    (∀ z ∈ {x | x.1.Nonempty ∧ x.2.Nonempty},
        DevosMulRel z y → (fun x => minOrder α ⊓ ↑(#x.1 + #x.2 - 1) ≤ ↑(#(x.1 * x.2))) z) →
      (fun x => minOrder α ⊓ ↑(#x.1 + #x.2 - 1) ≤ ↑(#(x.1 * x.2))) y

Tactic:
clear! x

Result:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
⊢ ∀ y ∈ {x | x.1.Nonempty ∧ x.2.Nonempty},
    (∀ z ∈ {x | x.1.Nonempty ∧ x.2.Nonempty},
        DevosMulRel z y → (fun x => minOrder α ⊓ ↑(#x.1 + #x.2 - 1) ≤ ↑(#(x.1 * x.2))) z) →
      (fun x => minOrder α ⊓ ↑(#x.1 + #x.2 - 1) ≤ ↑(#(x.1 * x.2))) y

Proof state:
case intro.mk.intro.inl
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hts : #t < #s
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

Tactic:
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])

Result:
no goals

Proof state:
case intro.mk.intro
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

Tactic:
obtain hts | hst := lt_or_le #t #s

Result:
case intro.mk.intro.inl
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hts : #t < #s
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

case intro.mk.intro.inr
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

Proof state:
case refine_2
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : (fun x => x ∈ a⁻¹ • ↑s) c
⊢ c * g⁻¹ ∈ a⁻¹ • ↑s

Tactic:
rwa [← op_smul_eq_mul, op_inv, ← Set.mem_smul_set_iff_inv_smul_mem, smul_comm,
  ← coe_smul_finset, hsg]

Result:
no goals

Proof state:
case intro.mk.intro.inr.inr.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s ≠ s
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

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

Result:
case intro.mk.intro.inr.inr.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1