awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : 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 : Set α)
b : α
hb : b ∈ (↑s : Set α)
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 : Disjoint t (g⁻¹ • t)
inr : minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #(g⁻¹ • t) ≤ #(s * t) + 1
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1

Tactic:
rw [← card_smul_finset g⁻¹ t]

Premises used: Inv.inv, Finset.card_smul_finset
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : 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 : Set α)
b : α
hb : b ∈ (↑s : Set α)
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 : Disjoint t (g⁻¹ • t)
inr : #s + #(g⁻¹ • t) ≤ #(s * t) + 1
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #(g⁻¹ • t) ≤ #(s * t) + 1

Tactic:
right
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : 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 : Set α)
b : α
hb : b ∈ (↑s : Set α)
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 : Disjoint t (g⁻¹ • t)
inr : #(t ∪ g⁻¹ • t) ≤ #(s * t) + 1
⊢ #s + #(g⁻¹ • t) ≤ #(s * t) + 1

Tactic:
grw [hst, ← card_union_of_disjoint hgt]

Premises used: Finset.card_union_of_disjoint
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : 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 : Set α)
b : α
hb : b ∈ (↑s : Set α)
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 : Disjoint t (g⁻¹ • t)
⊢ #(t ∪ g⁻¹ • t) ≤ #(s * t) + 1

Tactic:
(card_le_card_mul_left hgs).trans (le_add_of_le_left aux1)

Premises used: le_add_of_le_left, LE.le.trans, Finset.card_le_card_mul_left
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : 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 : Set α)
b : α
hb : b ∈ (↑s : Set α)
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 : Disjoint t (g⁻¹ • t)
⊢ #(t ∪ g⁻¹ • t) ≤ #(s * t) + 1

Tactic:
exact (card_le_card_mul_left hgs).trans (le_add_of_le_left aux1)

Premises used: le_add_of_le_left, LE.le.trans, Finset.card_le_card_mul_left
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : 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 : Set α)
b : α
hb : b ∈ (↑s : Set α)
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
inr :
  ∀ (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
inr₁ :
  ∀ (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
⊢ 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

Premises used: Eq.ge, Prod.mk, Finset.MulETransform.card, le_or_lt_of_add_le_add
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : 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 : Set α)
b : α
hb : b ∈ (↑s : Set α)
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

Tactic:
(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 _

Premises used: Iff.mpr, _private.0.devosMulRel_of_le_of_le, Finset.inter_subset_union, LE.le.trans, WithTop.coe_le_coe, Or.imp, Finset.Nonempty.mono, LE.le.trans'
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : 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 : Set α)
b : α
hb : b ∈ (↑s : Set α)
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

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

Premises used: Iff.mpr, _private.0.devosMulRel_of_le_of_le, Finset.inter_subset_union, LE.le.trans, WithTop.coe_le_coe, Or.imp, Finset.Nonempty.mono, LE.le.trans'
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : 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 : Set α)
b : α
hb : b ∈ (↑s : Set α)
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

Tactic:
(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 _

Premises used: Iff.mpr, LT.lt.le, Finset.inter_subset_union, _private.0.devosMulRel_of_le, LE.le.trans, WithTop.coe_le_coe, Or.imp, Finset.Nonempty.mono, LE.le.trans'
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : 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 : Set α)
b : α
hb : b ∈ (↑s : Set α)
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

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

Premises used: Iff.mpr, LT.lt.le, Finset.inter_subset_union, _private.0.devosMulRel_of_le, LE.le.trans, WithTop.coe_le_coe, Or.imp, Finset.Nonempty.mono, LE.le.trans'
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
inst_2 : IsMulTorsionFree G
s t : Finset G
hs : s.Nonempty
ht : t.Nonempty
⊢ #s + #t - 1 ≤ #(s * t)

Tactic:
simpa only [Monoid.minOrder_eq_top, min_eq_right, le_top, Nat.cast_le]
    using cauchy_davenport_minOrder_mul hs ht

Premises used: min_eq_right, le_top, Nat.cast_le, cauchy_davenport_minOrder_mul, Monoid.minOrder_eq_top
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
p : ℕ
hp : Nat.Prime p
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
⊢ min p (#s + #t - 1) ≤ #(s + t)

Tactic:
simpa only [ZMod.minOrder_of_prime hp, min_le_iff, Nat.cast_le]
    using cauchy_davenport_minOrder_add hs ht

Premises used: ZMod.minOrder_of_prime, min_le_iff, cauchy_davenport_minOrder_add, Nat.cast_le
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Mul α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : 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}
rw : #(s * {t.min' ht} ∪ {s.max' hs} * t) ≤ #(s * t)
⊢ #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]

Premises used: Finset.min', Finset.max', Finset.card_union_add_card_inter, Nat.add_sub_cancel, Finset.card_mul_singleton, Finset.card_singleton_mul, Finset.card_singleton
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Mul α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : 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:
card_mono (union_subset (mul_subset_mul_left <| singleton_subset_iff.2 <| min'_mem _ _) <|
      mul_subset_mul_right <| singleton_subset_iff.2 <| max'_mem _ _)

Premises used: Iff.mpr, Finset.union_subset, Finset.mul_subset_mul_left, Finset.max'_mem, Finset.min'_mem, Finset.singleton_subset_iff, Finset.mul_subset_mul_right, Finset.card_mono
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Mul α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : 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 _ _)

Premises used: Iff.mpr, Finset.union_subset, Finset.mul_subset_mul_left, Finset.max'_mem, Finset.min'_mem, Finset.singleton_subset_iff, Finset.mul_subset_mul_right, Finset.card_mono
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Mul α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
suffices : s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
⊢ #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 _ _)
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Mul α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : 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:
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 _ _⟩, ?_⟩

Premises used: Iff.mpr, Finset.mem_singleton_self, Finset.max'_mem, Finset.min'_mem, Finset.eq_singleton_iff_unique_mem, And.intro, Finset.mem_inter, Finset.mul_mem_mul
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Mul α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
refine : ∀ x ∈ s * {t.min' ht} ∩ ({s.max' hs} * t), x = s.max' hs * t.min' ht
⊢ 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 _ _⟩, ?_⟩

Premises used: Iff.mpr, Finset.mem_singleton_self, Finset.max'_mem, Finset.min'_mem, Finset.eq_singleton_iff_unique_mem, And.intro, Finset.mem_inter, Finset.mul_mem_mul
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Mul α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
simp : ∀ a ∈ s, ∀ x ∈ t, s.max' hs * x = a * t.min' ht → a = s.max' hs
⊢ ∀ 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_eq_left,
    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mul_left_inj]

Premises used: Finset.mem_singleton, and_imp, mul_left_inj, forall_exists_index, exists_eq_left, Finset.mem_inter, forall_apply_eq_imp_iff₂, Finset.mem_mul
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Mul α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : 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:
fun a' ha' b' hb' h ↦ (le_max' _ _ ha').eq_of_not_lt fun ha ↦
    (lt_of_eq_of_lt h (mul_lt_mul_left ha _)).not_ge <| mul_le_mul_right (min'_le _ _ hb') _

Premises used: Finset.min', Finset.min'_le, mul_le_mul_right, Finset.max', LE.le.eq_of_not_lt, lt_of_eq_of_lt, Finset.le_max', mul_lt_mul_left, Exists.intro, LT.lt.not_ge
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Mul α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : 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 ↦
    (lt_of_eq_of_lt h (mul_lt_mul_left ha _)).not_ge <| mul_le_mul_right (min'_le _ _ hb') _

Premises used: Finset.min', Finset.min'_le, mul_le_mul_right, Finset.max', LE.le.eq_of_not_lt, lt_of_eq_of_lt, Finset.le_max', mul_lt_mul_left, Exists.intro, LT.lt.not_ge
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x y : G
⊢ Set.MapsTo (fun (z : G) ↦ (x⁻¹ * z, z⁻¹ * y)) (↑(x •> A ∩ y •> B) : Set G)
    (↑({ab ∈ A ×ˢ B⁻¹ | ab.1 * ab.2 = x⁻¹ * y}) : Set (G × G))

Tactic:
simp +contextual [Set.MapsTo, Set.mem_smul_set_iff_inv_smul_mem, mul_assoc]

Premises used: mul_assoc, Set.MapsTo, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x y : G
simp : ∀ (a b : G), a ∈ A → b⁻¹ ∈ B → a * b = x⁻¹ * y → y⁻¹ * (x * a) ∈ B
⊢ Set.MapsTo (fun (ab' : G × G) ↦ x •> ab'.1) (↑({ab ∈ A ×ˢ B⁻¹ | ab.1 * ab.2 = x⁻¹ * y}) : Set (G × G))
    (↑(x •> A ∩ y •> B) : Set G)

Tactic:
simp +contextual [Set.MapsTo, Set.mem_smul_set_iff_inv_smul_mem]

Premises used: Set.MapsTo, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x y : G
⊢ ∀ (a b : G), a ∈ A → b⁻¹ ∈ B → a * b = x⁻¹ * y → y⁻¹ * (x * a) ∈ B

Tactic:
simp +contextual [← eq_mul_inv_iff_mul_eq, mul_assoc]

Premises used: mul_assoc, eq_mul_inv_iff_mul_eq
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x y : G
⊢ Set.LeftInvOn (fun (ab' : G × G) ↦ x •> ab'.1) (fun (z : G) ↦ (x⁻¹ * z, z⁻¹ * y)) (↑(x •> A ∩ y •> B) : Set G)

Tactic:
simp [Set.LeftInvOn]

Premises used: Set.LeftInvOn
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x y : G
⊢ Set.RightInvOn (fun (ab' : G × G) ↦ x •> ab'.1) (fun (z : G) ↦ (x⁻¹ * z, z⁻¹ * y))
    (↑({ab ∈ A ×ˢ B⁻¹ | ab.1 * ab.2 = x⁻¹ * y}) : Set (G × G))

Tactic:
simp +contextual [Set.LeftInvOn, ← eq_mul_inv_iff_mul_eq, mul_assoc]

Premises used: Set.LeftInvOn, mul_assoc, eq_mul_inv_iff_mul_eq
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ #(A ∩ x •> B) = A.convolution B⁻¹ x

Tactic:
simpa using card_smul_inter_smul _ _ 1 x

Premises used: Finset.card_smul_inter_smul, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ #(x •> A ∩ B) = A.convolution B⁻¹ x⁻¹

Tactic:
simpa using card_smul_inter_smul _ _ x 1

Premises used: Finset.card_smul_inter_smul, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ #(A ∩ x •> B⁻¹) = A.convolution B x

Tactic:
simp [card_inter_smul]

Premises used: Finset.card_inter_smul
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ #({ab ∈ A ×ˢ B | ab.1 * ab.2 = x}) = A.convolution B x

Tactic:
rfl

Premises used: Finset.convolution, rfl
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ ∀ (i : G × G),
    i ∈ {ab ∈ A ×ˢ B | ab.1 / ab.2 = x} ↔
      Membership.mem (α := G × G) ({ab ∈ A ×ˢ B⁻¹ | ab.1 * ab.2 = x})
        (((Equiv.refl G).prodCongr (Equiv.inv G) : (a : G × G) → G × G) i : G × G)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ Set.MapsTo (fun (ab : G × G) ↦ (ab.1, ab.2⁻¹)) (↑({ab ∈ A ×ˢ B | ab.1 * ab.2⁻¹ = x}) : Set (G × G))
    (↑({ab ∈ A ×ˢ B⁻¹ | ab.1 * ab.2 = x}) : Set (G × G))

Tactic:
simp [Set.MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ Set.MapsTo (fun (ab : G × G) ↦ (ab.1, ab.2⁻¹)) (↑({ab ∈ A ×ˢ B⁻¹ | ab.1 * ab.2 = x}) : Set (G × G))
    (↑({ab ∈ A ×ˢ B | ab.1 * ab.2⁻¹ = x}) : Set (G × G))

Tactic:
simp [Set.MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ Set.LeftInvOn (fun (ab : G × G) ↦ (ab.1, ab.2⁻¹)) (fun (ab : G × G) ↦ (ab.1, ab.2⁻¹))
    (↑({ab ∈ A ×ˢ B | ab.1 * ab.2⁻¹ = x}) : Set (G × G))

Tactic:
simp [Set.LeftInvOn]

Premises used: Set.LeftInvOn
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ Set.RightInvOn (fun (ab : G × G) ↦ (ab.1, ab.2⁻¹)) (fun (ab : G × G) ↦ (ab.1, ab.2⁻¹))
    (↑({ab ∈ A ×ˢ B⁻¹ | ab.1 * ab.2 = x}) : Set (G × G))

Tactic:
simp [Set.LeftInvOn]

Premises used: Set.LeftInvOn
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ 0 < A.convolution B x ↔ x ∈ A * B

Tactic:
aesop (add simp [convolution, Finset.Nonempty, mem_mul])

Premises used: Finset.convolution, Finset.Nonempty, Finset.mem_mul
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
this : A.convolution B x ≠ 0 ↔ 0 < A.convolution B x
⊢ A.convolution B x ≠ 0 ↔ x ∈ A * B

Tactic:
simp [this]
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
suffices : A.convolution B x ≠ 0 ↔ 0 < A.convolution B x
⊢ A.convolution B x ≠ 0 ↔ x ∈ A * B

Tactic:
suffices A.convolution B x ≠ 0 ↔ 0 < A.convolution B x by simp [this]
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B x ≠ 0 ↔ 0 < A.convolution B x

Tactic:
lia
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B x = 0 ↔ x ∉ A * B

Tactic:
simp [← convolution_ne_zero]

Premises used: Finset.convolution_ne_zero
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
rw : #(A ∩ x •> B⁻¹) ≤ #A
⊢ A.convolution B x ≤ #A

Tactic:
rw [← inv_inv B, ← card_inter_smul]

Premises used: inv_inv, Finset.card_inter_smul
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ #(A ∩ x •> B⁻¹) ≤ #A

Tactic:
card_le_card inter_subset_left

Premises used: Finset.card_le_card, Finset.inter_subset_left
-- Module: Mathlib.Combinatorics.Additive.Convolution
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
x : G
⊢ #(A ∩ x •> B⁻¹) ≤ #A

Tactic:
exact card_le_card inter_subset_left

Premises used: Finset.card_le_card, Finset.inter_subset_left