-- 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:
case intro.mk.intro.inr.inr.intro.intro.intro.intro.intro.intro.inr.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)
hgt : (t ∩ g⁻¹ • t).Nonempty
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

Tactic:
obtain hstg | hstg := le_or_lt_of_add_le_add (MulETransform.card g (s, t)).ge

Result:
case intro.mk.intro.inr.inr.intro.intro.intro.intro.intro.intro.inr.inr.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
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)
hgt : (t ∩ g⁻¹ • t).Nonempty
hstg : #(s, t).1 + #(s, t).2 ≤ #(mulETransformLeft g (s, t)).1 + #(mulETransformLeft g (s, t)).2
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

case intro.mk.intro.inr.inr.intro.intro.intro.intro.intro.intro.inr.inr.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)
hgt : (t ∩ g⁻¹ • t).Nonempty
hstg : #(s, t).1 + #(s, t).2 < #(mulETransformRight g (s, t)).1 + #(mulETransformRight g (s, t)).2
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
x : Finset α × Finset α := (s, t)
hx : x = (s, t)
⊢ minOrder α ⊓ ↑(#s + #t - 1) ≤ ↑(#(s * t))

Tactic:
clear_value x

Result:
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
x : Finset α × Finset α
hx : x = (s, t)
⊢ minOrder α ⊓ ↑(#s + #t - 1) ≤ ↑(#(s * t))

Proof state:
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

Tactic:
rintro ⟨s, t⟩ ⟨hs, ht⟩ ih

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

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

Tactic:
simp [add_comm]

Result:
no goals

Proof state:
case intro.mk.intro.inr.inr.intro.intro.intro.intro.intro.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
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
hS : ↑(zpowers g) ⊆ a⁻¹ • ↑s
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

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

Result:
case intro.mk.intro.inr.inr.intro.intro.intro.intro.intro.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
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
hS : ↑(zpowers g) ⊆ a⁻¹ • ↑s
⊢ Nat.card ↑(a⁻¹ • ↑s) = #s

Proof state:
case intro.mk.intro.inr.inr.intro.intro.intro.intro.intro.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
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
hS : ↑(zpowers g) ⊆ a⁻¹ • ↑s
⊢ Nat.card ↑(a⁻¹ • ↑s) = #s

Tactic:
rw [← coe_smul_finset]

Result:
case intro.mk.intro.inr.inr.intro.intro.intro.intro.intro.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
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
hS : ↑(zpowers g) ⊆ a⁻¹ • ↑s
⊢ Nat.card ↑↑(a⁻¹ • s) = #s