awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
refine :
  ∀ (n : ℕ),
    Set.WellFoundedOn.{u_2} (α := Finset α × Finset α)
      ({x : Finset α × Finset α | x.1.Nonempty ∧ x.2.Nonempty} ∩
        Set.preimage (β := ℕ) (fun (x : Finset α × Finset α) ↦ #(x.1 * x.2)) {n})
      ((fun (x1 x2 : ℕ) ↦ x1 > x2) on fun (x : Finset α × Finset α) ↦ #x.1 + #x.2)
⊢ Set.WellFoundedOn.{u_2} (α := Finset α × Finset α) {x : Finset α × Finset α | x.1.Nonempty ∧ x.2.Nonempty} DevosMulRel

Tactic:
refine wellFounded_lt.onFun.wellFoundedOn.prod_lex_of_wellFoundedOn_fiber fun n ↦
    Set.WellFoundedOn.prod_lex_of_wellFoundedOn_fiber ?_ fun n ↦
      wellFounded_lt.onFun.wellFoundedOn

Premises used: WellFounded.wellFoundedOn, wellFounded_lt, WellFounded.onFun, Set.WellFoundedOn.prod_lex_of_wellFoundedOn_fiber
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
n : ℕ
⊢ Set.WellFoundedOn.{u_2} (α := Finset α × Finset α)
    ({x : Finset α × Finset α | x.1.Nonempty ∧ x.2.Nonempty} ∩
      Set.preimage (β := ℕ) (fun (x : Finset α × Finset α) ↦ #(x.1 * x.2)) {n})
    ((fun (x1 x2 : ℕ) ↦ x1 > x2) on fun (x : Finset α × Finset α) ↦ #x.1 + #x.2)

Tactic:
wellFounded_lt.onFun.wellFoundedOn.mono' fun x hx y _ ↦ tsub_lt_tsub_left_of_le <|
    add_le_add ((card_le_card_mul_right hx.1.2).trans_eq hx.2) <|
      (card_le_card_mul_left hx.1.1).trans_eq hx.2

Premises used: LE.le.trans_eq, Set.WellFoundedOn.mono', add_le_add, WellFounded.wellFoundedOn, tsub_lt_tsub_left_of_le, wellFounded_lt, And.right, And.left, Finset.card_le_card_mul_right, WellFounded.onFun, Finset.card_le_card_mul_left
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
n : ℕ
⊢ Set.WellFoundedOn.{u_2} (α := Finset α × Finset α)
    ({x : Finset α × Finset α | x.1.Nonempty ∧ x.2.Nonempty} ∩
      Set.preimage (β := ℕ) (fun (x : Finset α × Finset α) ↦ #(x.1 * x.2)) {n})
    ((fun (x1 x2 : ℕ) ↦ x1 > x2) on fun (x : Finset α × Finset α) ↦ #x.1 + #x.2)

Tactic:
exact wellFounded_lt.onFun.wellFoundedOn.mono' fun x hx y _ ↦ tsub_lt_tsub_left_of_le <|
    add_le_add ((card_le_card_mul_right hx.1.2).trans_eq hx.2) <|
      (card_le_card_mul_left hx.1.1).trans_eq hx.2

Premises used: LE.le.trans_eq, Set.WellFoundedOn.mono', add_le_add, tsub_lt_tsub_left_of_le, Finset.card_le_card_mul_right, 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
⊢ let x := (s, t);
  x = (s, t)

Tactic:
set x := (s, t) with hx

Premises used: Prod.mk
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
x : Finset α × Finset α := (s, t)
hx : x = (s, t)
clear_value : ∀ (x : Finset α × Finset α) (hx : x = (s, t)), min (minOrder α) (↑(#s + #t - 1) : ℕ∞) ≤ (↑(#(s * t)) : ℕ∞)
⊢ min (minOrder α) (↑(#s + #t - 1) : ℕ∞) ≤ (↑(#(s * t)) : ℕ∞)

Tactic:
clear_value x
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
x : Finset α × Finset α
hx : x = (s, t)
⊢ x.1 = s ∧ x.2 = t

Tactic:
simp only [Prod.ext_iff] at hx

Premises used: Prod.ext_iff
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
x : Finset α × Finset α
hx : x.1 = s ∧ x.2 = t
obtain : ∀ (hs : x.1.Nonempty) (ht : x.2.Nonempty), min (minOrder α) (↑(#x.1 + #x.2 - 1) : ℕ∞) ≤ (↑(#(x.1 * x.2)) : ℕ∞)
⊢ min (minOrder α) (↑(#s + #t - 1) : ℕ∞) ≤ (↑(#(s * t)) : ℕ∞)

Tactic:
obtain ⟨rfl, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
x : Finset α × Finset α
hs : x.1.Nonempty
ht : x.2.Nonempty
⊢ min (minOrder α) (↑(#x.1 + #x.2 - 1) : ℕ∞) ≤ (↑(#(x.1 * x.2)) : ℕ∞)

Tactic:
wellFoundedOn_devosMulRel.induction (P := fun x : Finset α × Finset α ↦
    min (minOrder α) ↑(#x.1 + #x.2 - 1) ≤ #(x.1 * x.2)) ⟨hs, ht⟩ ?_

Premises used: And.intro, _private.0.wellFoundedOn_devosMulRel, Set.WellFoundedOn.induction
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
x : Finset α × Finset α
hs : x.1.Nonempty
ht : x.2.Nonempty
refine :
  ∀ (y : Finset α × Finset α),
    Membership.mem (γ := Set (Finset α × Finset α)) {x : Finset α × Finset α | x.1.Nonempty ∧ x.2.Nonempty} y →
      (∀ (z : Finset α × Finset α),
          Membership.mem (γ := Set (Finset α × Finset α)) {x : Finset α × Finset α | x.1.Nonempty ∧ x.2.Nonempty} z →
            DevosMulRel z y →
              (fun (x : Finset α × Finset α) ↦ min (minOrder α) (↑(#x.1 + #x.2 - 1) : ℕ∞) ≤ (↑(#(x.1 * x.2)) : ℕ∞)) z) →
        (fun (x : Finset α × Finset α) ↦ min (minOrder α) (↑(#x.1 + #x.2 - 1) : ℕ∞) ≤ (↑(#(x.1 * x.2)) : ℕ∞)) y
⊢ min (minOrder α) (↑(#x.1 + #x.2 - 1) : ℕ∞) ≤ (↑(#(x.1 * x.2)) : ℕ∞)

Tactic:
refine wellFoundedOn_devosMulRel.induction (P := fun x : Finset α × Finset α ↦
    min (minOrder α) ↑(#x.1 + #x.2 - 1) ≤ #(x.1 * x.2)) ⟨hs, ht⟩ ?_

Premises used: And.intro, _private.0.wellFoundedOn_devosMulRel, Set.WellFoundedOn.induction
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : (s, t).1.Nonempty
ht : (s, t).2.Nonempty
ih :
  ∀ (z : Finset α × Finset α),
    Membership.mem (γ := Set (Finset α × Finset α)) {x : Finset α × Finset α | x.1.Nonempty ∧ x.2.Nonempty} z →
      DevosMulRel z (s, t) →
        (fun (x : Finset α × Finset α) ↦ min (minOrder α) (↑(#x.1 + #x.2 - 1) : ℕ∞) ≤ (↑(#(x.1 * x.2)) : ℕ∞)) z
simp :
  ∀
    (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
⊢ min (minOrder α) (↑(#(s, t).1 + #(s, t).2 - 1) : ℕ∞) ≤ (↑(#((s, t).1 * (s, t).2)) : ℕ∞)

Tactic:
simp only [min_le_iff, tsub_le_iff_right, Prod.forall, Set.mem_setOf_eq, and_imp,
    Nat.cast_le] at *

Premises used: and_imp, min_le_iff, Set.mem_setOf_eq, tsub_le_iff_right, Prod.forall, Nat.cast_le
-- 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
inl : ∀ (hts : #t < #s), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
inr : ∀ (hst : #s ≤ #t), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1

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

Premises used: Finset.card, lt_or_ge
-- 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
hts : #t < #s
⊢ #((t⁻¹, s⁻¹).1 * (t⁻¹, s⁻¹).2) = #((s, t).1 * (s, t).2) ∧
    #(t⁻¹, s⁻¹).1 + #(t⁻¹, s⁻¹).2 = #(s, t).1 + #(s, t).2 ∧ #(t⁻¹, s⁻¹).1 < #(s, t).1

Tactic:
simpa only [← mul_inv_rev, add_comm, card_inv, true_and]

Premises used: Finset.card_inv, add_comm, mul_inv_rev, true_and
-- 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
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])

Premises used: Iff.mpr, Finset.card_inv, _private.0.devosMulRel_iff, add_comm, Finset.Nonempty.inv, mul_inv_rev, Or.inr
-- 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
inr :
  ∀ (a : α) (hs : Finset.Nonempty (α := α) {a})
    (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 : card (α := α) {a} ≤ #t), minOrder α ≤ (↑(#({a} * t)) : ℕ∞) ∨ card (α := α) {a} + #t ≤ #({a} * t) + 1
inr₁ :
  ∀ (a : α) (ha : a ∈ (↑s : Set α)) (b : α) (hb : b ∈ (↑s : Set α)) (hab : a ≠ b),
    minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1

Tactic:
obtain ⟨a, rfl⟩ | ⟨a, ha, b, hb, hab⟩ := hs.exists_eq_singleton_or_nontrivial

Premises used: Finset.Nonempty.exists_eq_singleton_or_nontrivial, rfl
-- Module: Mathlib.Combinatorics.Additive.CauchyDavenport
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
t : Finset α
ht : t.Nonempty
a : α
hs : Finset.Nonempty (α := α) {a}
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 : card (α := α) {a} ≤ #t
⊢ minOrder α ≤ (↑(#({a} * t)) : ℕ∞) ∨ card (α := α) {a} + #t ≤ #({a} * t) + 1

Tactic:
simp [add_comm]

Premises used: add_comm
-- 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
⊢ op (b⁻¹ * a) • b = a

Tactic:
simp
-- 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
inr : ∀ (g : α) (hg : g ≠ 1) (hgs : (s ∩ op g • s).Nonempty), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1

Tactic:
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⟩⟩⟩
-- 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
inr : ∀ (hsg : op g • s = s), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
inr₁ : ∀ (hsg : op g • s ≠ s), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1

Tactic:
obtain hsg | hsg := eq_or_ne (op g • s) s

Premises used: eq_or_ne, HSMul.hSMul, MulOpposite.op
-- 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 : op g • s = s
⊢ (↑(zpowers g) : Set α) ⊆ a⁻¹ • (↑s : Set α)

Tactic:
forall_mem_zpowers.2 <| @zpow_induction_right _ _ _ (· ∈ a⁻¹ • (s : Set α))
        ⟨_, ha, inv_mul_cancel _⟩ (fun c hc ↦ ?_) fun c hc ↦ ?_

Premises used: Iff.mpr, inv_mul_cancel, zpow_induction_right, Set.Subset, And.intro, Exists.intro, Subgroup.forall_mem_zpowers
-- 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 : op g • s = s
refine_1 : ∀ (c : α) (hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c), (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) (c * g)
refine_2 : ∀ (c : α) (hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c), (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) (c * g⁻¹)
⊢ (↑(zpowers g) : Set α) ⊆ a⁻¹ • (↑s : Set α)

Tactic:
refine forall_mem_zpowers.2 <| @zpow_induction_right _ _ _ (· ∈ a⁻¹ • (s : Set α))
        ⟨_, ha, inv_mul_cancel _⟩ (fun c hc ↦ ?_) fun c hc ↦ ?_

Premises used: Iff.mpr, inv_mul_cancel, zpow_induction_right, And.intro, Exists.intro, Subgroup.forall_mem_zpowers
-- 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 : op g • s = s
c : α
hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c
refine_1 : c * g ∈ op g • a⁻¹ • (↑s : Set α)
⊢ c * g ∈ a⁻¹ • (↑s : Set α)

Tactic:
rw [← hsg, coe_smul_finset, smul_comm]

Premises used: Finset.coe_smul_finset, SMulCommClass.smul_comm
-- 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 : op g • s = s
c : α
hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c
⊢ (fun (x : α) ↦ x ∈ op g • a⁻¹ • (↑s : Set α)) (c * g)

Tactic:
Set.smul_mem_smul_set hc

Premises used: Set.Mem, MulOpposite.unop, Set.smul_mem_smul_set
-- 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 : op g • s = s
c : α
hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c
⊢ (fun (x : α) ↦ x ∈ op g • a⁻¹ • (↑s : Set α)) (c * g)

Tactic:
exact Set.smul_mem_smul_set hc

Premises used: Set.smul_mem_smul_set
-- 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 : op g • s = s
c : α
hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c
refine_2 : op g⁻¹ • c ∈ a⁻¹ • (↑s : Set α)
refine_2₁ : (op g)⁻¹ • c ∈ a⁻¹ • (↑s : Set α)
refine_2₂ : c ∈ op g • a⁻¹ • (↑s : Set α)
refine_2₃ : c ∈ a⁻¹ • op g • (↑s : Set α)
refine_2₄ : c ∈ a⁻¹ • (↑(op g • s) : Set α)
refine_2₅ refine_2₆ refine_2₇ refine_2₈ : c ∈ a⁻¹ • (↑s : Set α)
⊢ c * g⁻¹ ∈ a⁻¹ • (↑s : Set α)

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

Premises used: op_smul_eq_mul, Finset.coe_smul_finset, Set.mem_smul_set_iff_inv_smul_mem, SMulCommClass.smul_comm, MulOpposite.op_inv
-- 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 : op g • s = s
⊢ (↑(zpowers g) : Set α) ⊆ a⁻¹ • (↑s : Set α)

Tactic:
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
      · simp only
        rwa [← op_smul_eq_mul, op_inv, ← Set.mem_smul_set_iff_inv_smul_mem, smul_comm,
          ← coe_smul_finset, hsg]
-- 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 : op g • s = s
hS : (↑(zpowers g) : Set α) ⊆ a⁻¹ • (↑s : Set α)
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1

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

Premises used: Iff.mpr, LE.le.trans_eq, Monoid.minOrder_le_natCard, Subgroup.zpowers_ne_bot, Set.Finite.subset, Nat.card_mono, Finset.card_le_card_mul_right, Set.Finite.smul_set, Or.inl, Finset.finite_toSet, LE.le.trans, WithTop.coe_le_coe
-- 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 : op g • s = s
hS : (↑(zpowers g) : Set α) ⊆ a⁻¹ • (↑s : Set α)
inr : Nat.card.{u_2} (↑(a⁻¹ • (↑s : Set α)) : Type u_2) = #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)

Premises used: Iff.mpr, LE.le.trans_eq, Monoid.minOrder_le_natCard, Subgroup.zpowers_ne_bot, Set.Finite.subset, Nat.card_mono, Finset.card_le_card_mul_right, Set.Finite.smul_set, Or.inl, Finset.finite_toSet, LE.le.trans, WithTop.coe_le_coe
-- 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 : op g • s = s
hS : (↑(zpowers g) : Set α) ⊆ a⁻¹ • (↑s : Set α)
inr : Nat.card.{u_2} (↑(↑(a⁻¹ • s) : Set α) : Type u_2) = #s
⊢ Nat.card.{u_2} (↑(a⁻¹ • (↑s : Set α)) : Type u_2) = #s

Tactic:
rw [← coe_smul_finset]

Premises used: Finset.coe_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 : op g • s = s
hS : (↑(zpowers g) : Set α) ⊆ a⁻¹ • (↑s : Set α)
⊢ Nat.card.{u_2} (↑(↑(a⁻¹ • s) : Set α) : Type u_2) = #s

Tactic:
simp [-coe_smul_finset]

Premises used: Finset.coe_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 : op g • s ≠ s
⊢ #(s ∩ op g • s) < #s

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⟩
-- 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
⊢ #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)

Tactic:
replace aux1 := card_mono <| mulETransformLeft.fst_mul_snd_subset g (s, t)
-- 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)
⊢ #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)

Tactic:
replace aux2 := card_mono <| mulETransformRight.fst_mul_snd_subset g (s, t)
-- 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)
inr : ∀ (hgt : Disjoint t (g⁻¹ • t)), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
inr₁ : ∀ (hgt : (t ∩ g⁻¹ • t).Nonempty), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1

Tactic:
obtain hgt | hgt := disjoint_or_nonempty_inter t (g⁻¹ • t)

Premises used: Finset.disjoint_or_nonempty_inter, Inv.inv, HSMul.hSMul