awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
⊢ ThreeGPFree (α := α) ((⇑(mulLeftEmbedding a) : (a : α) → α) '' (↑u : Set α))

Tactic:
hu.smul_set

Premises used: ThreeGPFree.smul_set
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
⊢ ThreeGPFree (α := α) ((⇑(mulLeftEmbedding a) : (a : α) → α) '' (↑u : Set α))

Tactic:
exact hu.smul_set

Premises used: ThreeGPFree.smul_set
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
⊢ ThreeGPFree (↑(map (mulLeftEmbedding a) u) : Set α)

Tactic:
have h : ThreeGPFree (u.map <| mulLeftEmbedding a : Set α) := by rw [coe_map]; exact hu.smul_set
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
h : ThreeGPFree (↑(map (mulLeftEmbedding a) u) : Set α)
⊢ #(map (mulLeftEmbedding a) u) ≤ (mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s)

Tactic:
h.le_mulRothNumber (map_subset_map.2 hus)

Premises used: Iff.mpr, ThreeGPFree.le_mulRothNumber, Finset.map_subset_map
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
h : ThreeGPFree (↑(map (mulLeftEmbedding a) u) : Set α)
h₁ : (mulRothNumber : (a : Finset α) → ℕ) s = #(map (mulLeftEmbedding a) u)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)

Tactic:
convert! h.le_mulRothNumber (map_subset_map.2 hus) using 1

Premises used: Iff.mpr, ThreeGPFree.le_mulRothNumber, Finset.map_subset_map
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
u : Finset α
hus : u ⊆ s
hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) s
hu : ThreeGPFree (↑u : Set α)
h : ThreeGPFree (↑(map (mulLeftEmbedding a) u) : Set α)
h₁ : (mulRothNumber : (a : Finset α) → ℕ) s = #u
h₂ h₃ : Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
⊢ (mulRothNumber : (a : Finset α) → ℕ) s = #(map (mulLeftEmbedding a) u)

Tactic:
rw [card_map, hcard]

Premises used: Finset.card_map
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
rw :
  Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
rw₁ rw₂ : Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
⊢ Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulRightEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)

Tactic:
rw [← mulLeftEmbedding_eq_mulRightEmbedding, mulRothNumber_map_mul_left s a]

Premises used: mulRothNumber_map_mul_left, mulLeftEmbedding_eq_mulRightEmbedding
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (range n) : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
N : ℕ
⊢ (rothNumberNat : (a : ℕ) → ℕ) N ≤ N

Tactic:
(addRothNumber_le _).trans (card_range _).le

Premises used: Finset.card_range, Eq.le, addRothNumber_le, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
n : ℕ
⊢ ∃ t ⊆ range n, #t = (rothNumberNat : (a : ℕ) → ℕ) n ∧ ThreeAPFree (↑t : Set ℕ)

Tactic:
addRothNumber_spec _

Premises used: addRothNumber_spec
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
k n : ℕ
s : Finset ℕ
hs : ThreeAPFree (↑s : Set ℕ)
hsn : ∀ x ∈ s, x < n
hsk : #s = k
⊢ k ≤ (rothNumberNat : (a : ℕ) → ℕ) n

Tactic:
hsk.ge.trans <| hs.le_addRothNumber fun x hx => mem_range.2 <| hsn x hx

Premises used: Iff.mpr, Eq.ge, Finset.mem_range, ThreeAPFree.le_addRothNumber, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
M N : ℕ
simp_rw :
  (addRothNumber : (a : Finset ℕ) → ℕ) (range (M + N)) ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (range M) : ℕ)
      ((addRothNumber : (a : Finset ℕ) → ℕ) (range N) : ℕ)
⊢ (rothNumberNat : (a : ℕ) → ℕ) (M + N) ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((rothNumberNat : (a : ℕ) → ℕ) M : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) N : ℕ)

Tactic:
simp_rw [rothNumberNat_def]

Premises used: rothNumberNat_def
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
M N : ℕ
rw :
  (addRothNumber : (a : Finset ℕ) → ℕ) (range M ∪ map (addLeftEmbedding M) (range N)) ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (range M) : ℕ)
      ((addRothNumber : (a : Finset ℕ) → ℕ) (map (addLeftEmbedding M) (range N)) : ℕ)
⊢ (addRothNumber : (a : Finset ℕ) → ℕ) (range (M + N)) ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (range M) : ℕ)
      ((addRothNumber : (a : Finset ℕ) → ℕ) (range N) : ℕ)

Tactic:
rw [range_add_eq_union, ← addRothNumber_map_add_left (range N) M]

Premises used: Finset.range, addRothNumber_map_add_left, Finset.range_add_eq_union
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
M N : ℕ
⊢ (addRothNumber : (a : Finset ℕ) → ℕ) (range M ∪ map (addLeftEmbedding M) (range N)) ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (range M) : ℕ)
      ((addRothNumber : (a : Finset ℕ) → ℕ) (map (addLeftEmbedding M) (range N)) : ℕ)

Tactic:
addRothNumber_union_le _ _

Premises used: Set.Mem, setOf, addRothNumber_union_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
M N : ℕ
⊢ (addRothNumber : (a : Finset ℕ) → ℕ) (range M ∪ map (addLeftEmbedding M) (range N)) ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (range M) : ℕ)
      ((addRothNumber : (a : Finset ℕ) → ℕ) (map (addLeftEmbedding M) (range N)) : ℕ)

Tactic:
exact addRothNumber_union_le _ _

Premises used: addRothNumber_union_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
⊢ Eq (α := ℕ) ((rothNumberNat : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)

Tactic:
rfl

Premises used: Nat.findGreatest, rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
a b : ℕ
inl :
  ∀ (h : b ≤ a),
    Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)
inr :
  ∀ (h : a ≤ b),
    Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)
⊢ Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)

Tactic:
obtain h | h := le_total b a

Premises used: le_total
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
a b : ℕ
h : b ≤ a
inl : Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) 0 : ℕ)
inl₁ : Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) ∅ : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) 0 : ℕ)
inl₂ : Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) ∅ : ℕ) (0 : ℕ)
inl₃ inl₄ : Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)

Tactic:
rw [Nat.sub_eq_zero_of_le h, Ico_eq_empty_of_le h, rothNumberNat_zero, addRothNumber_empty]

Premises used: rothNumberNat_zero, addRothNumber_empty, Finset.Ico_eq_empty_of_le, Nat.sub_eq_zero_of_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
a b : ℕ
h : a ≤ b
⊢ Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (map (addLeftEmbedding a) (range (b - a))) : ℕ)
    ((addRothNumber : (a : Finset ℕ) → ℕ) (range (b - a)) : ℕ)

Tactic:
addRothNumber_map_add_left _ a

Premises used: addRothNumber_map_add_left
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
a b : ℕ
h : a ≤ b
h₁ : Ico a b = map (addLeftEmbedding a) (range (b - a))
⊢ Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)

Tactic:
convert! addRothNumber_map_add_left _ a

Premises used: addRothNumber_map_add_left
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
a b : ℕ
h : a ≤ b
h₁ : Ico a b = image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 (b - a))
⊢ Ico a b = map (addLeftEmbedding a) (range (b - a))

Tactic:
rw [range_eq_Ico, map_eq_image]

Premises used: Finset.map_eq_image, Finset.range_eq_Ico
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
a b : ℕ
h : a ≤ b
⊢ Ico (a + 0) (a + (b - a)) = image (fun (x : ℕ) ↦ a + x) (Ico 0 (b - a))

Tactic:
(image_add_left_Ico 0 (b - a) _).symm

Premises used: HSub.hSub, OfNat.ofNat, Eq.symm, Finset.image_add_left_Ico
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
a b : ℕ
h : a ≤ b
h₁ : b = a + (b - a)
⊢ Ico a b = image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 (b - a))

Tactic:
convert! (image_add_left_Ico 0 (b - a) _).symm

Premises used: HSub.hSub, OfNat.ofNat, Eq.symm, Finset.image_add_left_Ico
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
a b : ℕ
h : a ≤ b
⊢ b = a + (b - a)

Tactic:
(add_tsub_cancel_of_le h).symm

Premises used: Eq.symm, add_tsub_cancel_of_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
a b : ℕ
h : a ≤ b
⊢ b = a + (b - a)

Tactic:
exact (add_tsub_cancel_of_le h).symm

Premises used: Eq.symm, add_tsub_cancel_of_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
k n : ℕ
hkn : 2 * k ≤ n
⊢ Eq (α := ℕ) ((addRothNumber : (a : Finset (Fin n.succ)) → ℕ) (Iio (↑k : Fin n.succ)) : ℕ)
    ((rothNumberNat : (a : ℕ) → ℕ) k : ℕ)

Tactic:
IsAddFreimanIso.addRothNumber_congr <| mod_cast isAddFreimanIso_Iio two_ne_zero hkn

Premises used: IsAddFreimanIso.addRothNumber_congr
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
k n : ℕ
hkn : k ≤ n
h : Set.BijOn Nat.cast (↑(range k) : Set ℕ) (↑(Iio (↑k : Fin n.succ)) : Set (Fin n.succ))
⊢ LE.le (α := ℕ) ((addRothNumber : (a : Finset (Fin n.succ)) → ℕ) (Iio (↑k : Fin n.succ)) : ℕ)
    ((rothNumberNat : (a : ℕ) → ℕ) k : ℕ)

Tactic:
(AddHomClass.isAddFreimanHom (Nat.castRingHom _) h.mapsTo).addRothNumber_mono h

Premises used: AddHomClass.isAddFreimanHom, Nat.castRingHom, IsAddFreimanHom.addRothNumber_mono, Set.BijOn.mapsTo
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
k n : ℕ
hkn : k ≤ n
h : Set.BijOn Nat.cast (↑(range k) : Set ℕ) (↑(Iio (↑k : Fin n.succ)) : Set (Fin n.succ))
⊢ LE.le (α := ℕ) ((addRothNumber : (a : Finset (Fin n.succ)) → ℕ) (Iio (↑k : Fin n.succ)) : ℕ)
    ((rothNumberNat : (a : ℕ) → ℕ) k : ℕ)

Tactic:
exact (AddHomClass.isAddFreimanHom (Nat.castRingHom _) h.mapsTo).addRothNumber_mono h

Premises used: AddHomClass.isAddFreimanHom, Nat.castRingHom, IsAddFreimanHom.addRothNumber_mono, Set.BijOn.mapsTo
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
k n : ℕ
hkn : k ≤ n
suffices : Set.BijOn Nat.cast (↑(range k) : Set ℕ) (↑(Iio (↑k : Fin n.succ)) : Set (Fin n.succ))
⊢ LE.le (α := ℕ) ((addRothNumber : (a : Finset (Fin n.succ)) → ℕ) (Iio (↑k : Fin n.succ)) : ℕ)
    ((rothNumberNat : (a : ℕ) → ℕ) k : ℕ)

Tactic:
suffices h : Set.BijOn (Nat.cast : ℕ → Fin n.succ) (range k) (Iio k : Finset (Fin n.succ)) by
    exact (AddHomClass.isAddFreimanHom (Nat.castRingHom _) h.mapsTo).addRothNumber_mono h
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
k n : ℕ
hkn : k ≤ n
simp : k ≤ n + 1
⊢ (↑(range k) : Set ℕ) ⊆ Set.Iio n.succ

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
k n : ℕ
hkn : k ≤ n
⊢ k ≤ n + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
k n : ℕ
hkn : k ≤ n
refine_1 : Set.MapsTo Nat.cast (↑(range k) : Set ℕ) (↑(Iio (↑k : Fin n.succ)) : Set (Fin n.succ))
refine_2 : Set.SurjOn Nat.cast (↑(range k) : Set ℕ) (↑(Iio (↑k : Fin n.succ)) : Set (Fin n.succ))
⊢ Set.BijOn Nat.cast (↑(range k) : Set ℕ) (↑(Iio (↑k : Fin n.succ)) : Set (Fin n.succ))

Tactic:
refine ⟨?_, (CharP.natCast_injOn_Iio _ n.succ).mono (by simp; lia), ?_⟩
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
k n : ℕ
hkn : k ≤ n
⊢ Set.MapsTo Nat.cast (↑(range k) : Set ℕ) (↑(Iio (↑k : Fin n.succ)) : Set (Fin n.succ))

Tactic:
simpa using fun x ↦ natCast_strictMono hkn

Premises used: Fin.natCast_strictMono
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
k n : ℕ
hkn : k ≤ n
refine_2 : ∀ (x : Fin n.succ), (↑x : ℕ) < k → ∃ x_1 < k, (↑x_1 : Fin n.succ) = x
⊢ Set.SurjOn Nat.cast (↑(range k) : Set ℕ) (↑(Iio (↑k : Fin n.succ)) : Set (Fin n.succ))

Tactic:
simp only [Set.SurjOn, coe_Iio, Set.subset_def, Set.mem_Iio, Set.mem_image, lt_def,
    val_cast_of_lt, Nat.lt_succ_iff.2 hkn, coe_range]

Premises used: Iff.mpr, Set.mem_Iio, Set.subset_def, Finset.coe_range, Set.SurjOn, Set.mem_image, Fin.lt_def, Nat.lt_succ_iff, Finset.coe_Iio, Fin.val_cast_of_lt
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
k n : ℕ
hkn : k ≤ n
x : Fin n.succ
hx : (↑x : ℕ) < k
⊢ (↑(↑x : ℕ) : Fin n.succ) = x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Defs
Goal:
k n : ℕ
hkn : k ≤ n
⊢ ∀ (x : Fin n.succ), (↑x : ℕ) < k → ∃ x_1 < k, (↑x_1 : Fin n.succ) = x

Tactic:
exact fun x hx ↦ ⟨x, hx, by simp⟩
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
⊢ A.Nonempty

Tactic:
⟨1, hA.one_mem⟩

Premises used: IsApproximateSubgroup.one_mem, Set.Nonempty, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
obtain : ∀ (F : Finset G) (hF : (↑(#F) : ℝ) ≤ K) (hSF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F : Set G) • A), 1 ≤ K
⊢ 1 ≤ K

Tactic:
obtain ⟨F, hF, hSF⟩ := hA.sq_covBySMul

Premises used: IsApproximateSubgroup.sq_covBySMul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hSF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F : Set G) • A
grw : LE.le (α := ℝ) 1 (↑(#F) : ℝ)
⊢ 1 ≤ K

Tactic:
grw [← hF]
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hSF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F : Set G) • A
by_contra! : ∀ (hF : (↑(Finset.card.{u_1} (α := G) ∅) : ℝ) ≤ K) (hSF : HPow.hPow (β := ℕ) A 2 ⊆ (↑∅ : Set G) • A), False
⊢ F.Nonempty

Tactic:
by_contra! rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
hF : (↑(Finset.card.{u_1} (α := G) ∅) : ℝ) ≤ K
hSF : HPow.hPow (β := ℕ) A 2 ⊆ (↑∅ : Set G) • A
⊢ False

Tactic:
simp [hA.nonempty.ne_empty] at hSF

Premises used: Set.Nonempty.ne_empty, IsApproximateSubgroup.nonempty
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hSF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F : Set G) • A
⊢ F.Nonempty

Tactic:
have : F.Nonempty := by by_contra! rfl; simp [hA.nonempty.ne_empty] at hSF
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hSF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F : Set G) • A
this : F.Nonempty
⊢ LE.le (α := ℝ) 1 (↑(#F) : ℝ)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K (↑A : Set G)
⊢ (↑(#(HPow.hPow (β := ℕ) A 0)) : ℝ) ≤ K ^ HSub.hSub (α := ℕ) 0 1 * (↑(#A) : ℝ)

Tactic:
simpa using hA.nonempty

Premises used: IsApproximateSubgroup.nonempty
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K (↑A : Set G)
⊢ (↑(#(HPow.hPow (β := ℕ) A 1)) : ℝ) ≤ K ^ HSub.hSub (α := ℕ) 1 1 * (↑(#A) : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K (↑A : Set G)
n : ℕ
obtain :
  ∀ (F : Finset G) (hF : (↑(#F) : ℝ) ≤ K) (hSF : HPow.hPow (β := ℕ) (↑A : Set G) 2 ⊆ (↑F : Set G) • (↑A : Set G)),
    (↑(#(A ^ (n + 2))) : ℝ) ≤ K ^ (n + 2 - 1) * (↑(#A) : ℝ)
⊢ (↑(#(A ^ (n + 2))) : ℝ) ≤ K ^ (n + 2 - 1) * (↑(#A) : ℝ)

Tactic:
obtain ⟨F, hF, hSF⟩ := hA.sq_covBySMul

Premises used: IsApproximateSubgroup.sq_covBySMul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K (↑A : Set G)
n : ℕ
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hSF : HPow.hPow (β := ℕ) (↑A : Set G) 2 ⊆ (↑F : Set G) • (↑A : Set G)
a : A ^ (n + 2) ⊆ F ^ (n + 1) * A
⊢ LE.le (α := ℝ) (↑(#(A ^ (n + 2))) : ℝ) (↑(#(F ^ (n + 1) * A)) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K (↑A : Set G)
n : ℕ
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hSF : HPow.hPow (β := ℕ) (↑A : Set G) 2 ⊆ (↑F : Set G) • (↑A : Set G)
⊢ n + 2 ≠ 0

Tactic:
lia
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K (↑A : Set G)
n : ℕ
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hSF : HPow.hPow (β := ℕ) (↑A : Set G) 2 ⊆ (↑F : Set G) • (↑A : Set G)
⊢ A ^ (n + 2) ⊆ F ^ (n + 1) * A

Tactic:
exact mod_cast Set.pow_subset_pow_mul_of_sq_subset_mul hSF (by lia)

Premises used: Set.pow_subset_pow_mul_of_sq_subset_mul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K (↑A : Set G)
n : ℕ
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hSF : HPow.hPow (β := ℕ) (↑A : Set G) 2 ⊆ (↑F : Set G) • (↑A : Set G)
⊢ (↑(#(F ^ (n + 1) * A)) : ℝ) ≤ HMul.hMul (α := ℝ) (↑(#(F ^ (n + 1))) : ℝ) (↑(#A) : ℝ)

Tactic:
mod_cast Finset.card_mul_le

Premises used: Nat.cast_mul._simp_1, HMul.hMul, congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, Finset.card_mul_le, HPow.hPow, HAdd.hAdd, Finset.card, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K (↑A : Set G)
n : ℕ
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hSF : HPow.hPow (β := ℕ) (↑A : Set G) 2 ⊆ (↑F : Set G) • (↑A : Set G)
hbc : (↑(#(F ^ (n + 1))) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F) : ℝ) (n + 1)
⊢ HMul.hMul (α := ℝ) (↑(#(F ^ (n + 1))) : ℝ) (↑(#A) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F) : ℝ) (n + 1) * (↑(#A) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K (↑A : Set G)
n : ℕ
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hSF : HPow.hPow (β := ℕ) (↑A : Set G) 2 ⊆ (↑F : Set G) • (↑A : Set G)
⊢ (↑(#(F ^ (n + 1))) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F) : ℝ) (n + 1)

Tactic:
mod_cast Finset.card_pow_le

Premises used: Finset.card_pow_le, congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, HPow.hPow, HAdd.hAdd, Finset.card, OfNat.ofNat, Eq.symm, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K (↑A : Set G)
n : ℕ
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hSF : HPow.hPow (β := ℕ) (↑A : Set G) 2 ⊆ (↑F : Set G) • (↑A : Set G)
⊢ (↑(#(F ^ (n + 1))) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F) : ℝ) (n + 1)

Tactic:
exact mod_cast Finset.card_pow_le

Premises used: Finset.card_pow_le
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K (↑A : Set G)
n : ℕ
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hSF : HPow.hPow (β := ℕ) (↑A : Set G) 2 ⊆ (↑F : Set G) • (↑A : Set G)
ha : LE.le (α := ℝ) 0 (↑(#A) : ℝ)
hbc : LE.le (α := ℝ) 0 (↑(#F) : ℝ)
⊢ HPow.hPow (α := ℝ) (↑(#F) : ℝ) (n + 1) * (↑(#A) : ℝ) ≤ K ^ (n + 1) * (↑(#A) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K (↑A : Set G)
n : ℕ
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hSF : HPow.hPow (β := ℕ) (↑A : Set G) 2 ⊆ (↑F : Set G) • (↑A : Set G)
exact : LE.le (α := ℝ) (↑(#(A ^ (n + 2))) : ℝ) (↑(#(F ^ (n + 1) * A)) : ℝ)
exact₁ : HMul.hMul (α := ℝ) (↑(#(F ^ (n + 1))) : ℝ) (↑(#A) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F) : ℝ) (n + 1) * (↑(#A) : ℝ)
exact₂ : HPow.hPow (α := ℝ) (↑(#F) : ℝ) (n + 1) * (↑(#A) : ℝ) ≤ K ^ (n + 1) * (↑(#A) : ℝ)
⊢ (↑(#(A ^ (n + 2))) : ℝ) ≤ K ^ (n + 2 - 1) * (↑(#A) : ℝ)

Tactic:
calc
      (#(A ^ (n + 2)) : ℝ) ≤ #(F ^ (n + 1) * A) := by
        gcongr; exact mod_cast Set.pow_subset_pow_mul_of_sq_subset_mul hSF (by lia)
      _ ≤ #(F ^ (n + 1)) * #A := mod_cast Finset.card_mul_le
      _ ≤ #F ^ (n + 1) * #A := by gcongr; exact mod_cast Finset.card_pow_le
      _ ≤ K ^ (n + 1) * #A := by gcongr

Premises used: HMul.hMul, Nat.cast, Finset.card_mul_le, HPow.hPow, HAdd.hAdd, Finset.card, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K (↑A : Set G)
⊢ (↑(#(A * A)) : ℝ) ≤ K * (↑(#A) : ℝ)

Tactic:
simpa [sq] using hA.card_pow_le (n := 2)

Premises used: sq, IsApproximateSubgroup.card_pow_le
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
F : Type u_2
H : Type u_3
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
hA : IsApproximateSubgroup K A
⊢ Eq.{u_3 + 1} (α := Set H) ((⇑f : (a : G) → H) '' A)⁻¹ ((⇑f : (a : G) → H) '' A)

Tactic:
simp [← Set.image_inv, hA.inv_eq_self]

Premises used: IsApproximateSubgroup.inv_eq_self, Set.image_inv
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
F : Type u_2
H : Type u_3
inst_1 : Group H
inst_2 : FunLike F G H
inst_3 : MonoidHomClass F G H
f : F
hA : IsApproximateSubgroup K A
obtain :
  ∀ (F_1 : Finset G) (hF : (↑(#F_1) : ℝ) ≤ K) (hAF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F_1 : Set G) • A),
    CovBySMul H K (HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2) ((⇑f : (a : G) → H) '' A)
⊢ CovBySMul H K (HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2) ((⇑f : (a : G) → H) '' A)

Tactic:
obtain ⟨F, hF, hAF⟩ := hA.sq_covBySMul

Premises used: IsApproximateSubgroup.sq_covBySMul
-- Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
F_1 : Type u_2
H : Type u_3
inst_1 : Group H
inst_2 : FunLike F_1 G H
inst_3 : MonoidHomClass F_1 G H
f : F_1
hA : IsApproximateSubgroup K A
F : Finset G
hF : (↑(#F) : ℝ) ≤ K
hAF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F : Set G) • A
⊢ CovBySMul H K (HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2) ((⇑f : (a : G) → H) '' A)

Tactic:
⟨F.image f, ?_, ?_⟩

Premises used: CovBySMul, And.intro, Exists.intro, DFunLike.coe, Finset.image