awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
have refine_2 : ∀ (u : Finset α) (hus : u ⊆ s) (hcard : #u = (mulRothNumber : (a : Finset α) → ℕ) s) (hu : ThreeGPFree (↑u : Set α)),
  LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
Tactic: obtain ⟨u, hus, hcard, hu⟩ := mulRothNumber_spec s
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
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 α)
have rw : ThreeGPFree (α := α) ((⇑(mulLeftEmbedding a) : (a : α) → α) '' (↑u : Set α))
Tactic: rw [coe_map]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (hypothesis)
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 α)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
have h : ThreeGPFree (↑(map (mulLeftEmbedding a) u) : Set α)
Tactic: have h : ThreeGPFree (u.map <| mulLeftEmbedding a : Set α) := by rw [coe_map]; exact hu.smul_set
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
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 α)
⊢ LE.le (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
have h₁ : (mulRothNumber : (a : Finset α) → ℕ) s = #(map (mulLeftEmbedding a) u)
Tactic: convert! h.le_mulRothNumber (map_subset_map.2 hus) using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
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 α)
⊢ (mulRothNumber : (a : Finset α) → ℕ) s = #(map (mulLeftEmbedding a) u)
have h₁ : (mulRothNumber : (a : Finset α) → ℕ) s = #u
Tactic: rw [card_map, hcard]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
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
⊢ (mulRothNumber : (a : Finset α) → ℕ) s = #(map (mulLeftEmbedding a) u)
have h₂ : Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
Tactic: rw [card_map, hcard]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : CancelCommMonoid α
s : Finset α
a : α
⊢ Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulRightEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
have rw : Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulLeftEmbedding a) s) : ℕ)
  ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
Tactic: rw [← mulLeftEmbedding_eq_mulRightEmbedding, mulRothNumber_map_mul_left s a]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
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 : ℕ)
⊢ Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) (map (mulRightEmbedding a) s) : ℕ)
    ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
have rw₁ : Eq (α := ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ) ((mulRothNumber : (a : Finset α) → ℕ) s : ℕ)
Tactic: rw [← mulLeftEmbedding_eq_mulRightEmbedding, mulRothNumber_map_mul_left s a]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
M N : ℕ
⊢ (rothNumberNat : (a : ℕ) → ℕ) (M + N) ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((rothNumberNat : (a : ℕ) → ℕ) M : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) N : ℕ)
have simp_rw : (addRothNumber : (a : Finset ℕ) → ℕ) (range (M + N)) ≤
  HAdd.hAdd (α := ℕ) (β := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (range M) : ℕ)
    ((addRothNumber : (a : Finset ℕ) → ℕ) (range N) : ℕ)
Tactic: simp_rw [rothNumberNat_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
M N : ℕ
⊢ (addRothNumber : (a : Finset ℕ) → ℕ) (range (M + N)) ≤
    HAdd.hAdd (α := ℕ) (β := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (range M) : ℕ)
      ((addRothNumber : (a : Finset ℕ) → ℕ) (range N) : ℕ)
have 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)) : ℕ)
Tactic: rw [range_add_eq_union, ← addRothNumber_map_add_left (range N) M]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
a b : ℕ
⊢ Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)
have inl : ∀ (h : b ≤ a),
  Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)
Tactic: obtain h | h := le_total b a
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
a b : ℕ
inl :
  ∀ (h : b ≤ a),
    Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)
⊢ Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)
have inr : ∀ (h : a ≤ b),
  Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)
Tactic: obtain h | h := le_total b a
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
a b : ℕ
h : b ≤ a
⊢ Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)
have inl : Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) 0 : ℕ)
Tactic: rw [Nat.sub_eq_zero_of_le h, Ico_eq_empty_of_le h, rothNumberNat_zero, addRothNumber_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
a b : ℕ
h : b ≤ a
inl : Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) 0 : ℕ)
⊢ Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)
have inl₁ : Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) ∅ : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) 0 : ℕ)
Tactic: rw [Nat.sub_eq_zero_of_le h, Ico_eq_empty_of_le h, rothNumberNat_zero, addRothNumber_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
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 : ℕ)
⊢ Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)
have inl₂ : Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) ∅ : ℕ) (0 : ℕ)
Tactic: rw [Nat.sub_eq_zero_of_le h, Ico_eq_empty_of_le h, rothNumberNat_zero, addRothNumber_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
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 : ℕ)
⊢ Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)
have inl₃ : Eq (α := ℕ) 0 0
Tactic: rw [Nat.sub_eq_zero_of_le h, Ico_eq_empty_of_le h, rothNumberNat_zero, addRothNumber_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
a b : ℕ
h : a ≤ b
⊢ Eq (α := ℕ) ((addRothNumber : (a : Finset ℕ) → ℕ) (Ico a b) : ℕ) ((rothNumberNat : (a : ℕ) → ℕ) (b - a) : ℕ)
have h₁ : Ico a b = map (addLeftEmbedding a) (range (b - a))
Tactic: convert! addRothNumber_map_add_left _ a
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
a b : ℕ
h : a ≤ b
⊢ Ico a b = map (addLeftEmbedding a) (range (b - a))
have h₁ : Ico a b = image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 (b - a))
Tactic: rw [range_eq_Ico, map_eq_image]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
a b : ℕ
h : a ≤ b
⊢ Ico a b = image (⇑(addLeftEmbedding a) : (a : ℕ) → ℕ) (Ico 0 (b - a))
have h₁ : b = a + (b - a)
Tactic: convert! (image_add_left_Ico 0 (b - a) _).symm
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
k n : ℕ
hkn : k ≤ n
⊢ LE.le (α := ℕ) ((addRothNumber : (a : Finset (Fin n.succ)) → ℕ) (Iio (↑k : Fin n.succ)) : ℕ)
    ((rothNumberNat : (a : ℕ) → ℕ) k : ℕ)
have suffices : Set.BijOn Nat.cast (↑(range k) : Set ℕ) (↑(Iio (↑k : Fin n.succ)) : Set (Fin n.succ))
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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
k n : ℕ
hkn : k ≤ n
⊢ (↑(range k) : Set ℕ) ⊆ Set.Iio n.succ
have simp : k ≤ n + 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
k n : ℕ
hkn : k ≤ n
⊢ Set.BijOn Nat.cast (↑(range k) : Set ℕ) (↑(Iio (↑k : Fin n.succ)) : Set (Fin n.succ))
have refine_1 : Set.MapsTo 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), ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
k n : ℕ
hkn : k ≤ n
refine_1 : Set.MapsTo 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))
have refine_2 : Set.SurjOn 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), ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Defs (goal)
Goal:
k n : ℕ
hkn : k ≤ n
⊢ Set.SurjOn Nat.cast (↑(range k) : Set ℕ) (↑(Iio (↑k : Fin n.succ)) : Set (Fin n.succ))
have refine_2 : ∀ (x : Fin n.succ), (↑x : ℕ) < k → ∃ x_1 < k, (↑x_1 : Fin n.succ) = x
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
A : Set G
K : ℝ
hA : IsApproximateSubgroup K A
⊢ 1 ≤ K
have obtain : ∀ (F : Finset G) (hF : (↑(#F) : ℝ) ≤ K) (hSF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F : Set G) • A), 1 ≤ K
Tactic: obtain ⟨F, hF, hSF⟩ := hA.sq_covBySMul
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
⊢ 1 ≤ K
have grw : LE.le (α := ℝ) 1 (↑(#F) : ℝ)
Tactic: grw [← hF]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
have by_contra! : ∀ (hF : (↑(Finset.card.{u_1} (α := G) ∅) : ℝ) ≤ K) (hSF : HPow.hPow (β := ℕ) A 2 ⊆ (↑∅ : Set G) • A), False
Tactic: by_contra! rfl
Cleared hypotheses: F, hF, hSF
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (hypothesis)
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
⊢ LE.le (α := ℝ) 1 (↑(#F) : ℝ)
have this : F.Nonempty
Tactic: have : F.Nonempty := by by_contra! rfl; simp [hA.nonempty.ne_empty] at hSF
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K (↑A : Set G)
n : ℕ
⊢ (↑(#(A ^ (n + 2))) : ℝ) ≤ K ^ (n + 2 - 1) * (↑(#A) : ℝ)
have 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) : ℝ)
Tactic: obtain ⟨F, hF, hSF⟩ := hA.sq_covBySMul
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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)
⊢ LE.le (α := ℝ) (↑(#(A ^ (n + 2))) : ℝ) (↑(#(F ^ (n + 1) * A)) : ℝ)
have a : A ^ (n + 2) ⊆ F ^ (n + 1) * A
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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)
⊢ HMul.hMul (α := ℝ) (↑(#(F ^ (n + 1))) : ℝ) (↑(#A) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F) : ℝ) (n + 1) * (↑(#A) : ℝ)
have hbc : (↑(#(F ^ (n + 1))) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F) : ℝ) (n + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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)
⊢ HPow.hPow (α := ℝ) (↑(#F) : ℝ) (n + 1) * (↑(#A) : ℝ) ≤ K ^ (n + 1) * (↑(#A) : ℝ)
have ha : LE.le (α := ℝ) 0 (↑(#A) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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) : ℝ)
⊢ HPow.hPow (α := ℝ) (↑(#F) : ℝ) (n + 1) * (↑(#A) : ℝ) ≤ K ^ (n + 1) * (↑(#A) : ℝ)
have hbc : LE.le (α := ℝ) 0 (↑(#F) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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))) : ℝ) ≤ K ^ (n + 2 - 1) * (↑(#A) : ℝ)
have exact : LE.le (α := ℝ) (↑(#(A ^ (n + 2))) : ℝ) (↑(#(F ^ (n + 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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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)) : ℝ)
⊢ (↑(#(A ^ (n + 2))) : ℝ) ≤ K ^ (n + 2 - 1) * (↑(#A) : ℝ)
have exact₁ : HMul.hMul (α := ℝ) (↑(#(F ^ (n + 1))) : ℝ) (↑(#A) : ℝ) ≤ HPow.hPow (α := ℝ) (↑(#F) : ℝ) (n + 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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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) : ℝ)
⊢ (↑(#(A ^ (n + 2))) : ℝ) ≤ K ^ (n + 2 - 1) * (↑(#A) : ℝ)
have exact₂ : HPow.hPow (α := ℝ) (↑(#F) : ℝ) (n + 1) * (↑(#A) : ℝ) ≤ K ^ (n + 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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
⊢ CovBySMul H K (HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2) ((⇑f : (a : G) → H) '' A)
have 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)
Tactic: obtain ⟨F, hF, hAF⟩ := hA.sq_covBySMul
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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)
have refine_1 : (↑(Finset.card.{u_3} (α := H) (Finset.image (⇑f : (a : G) → H) F)) : ℝ) ≤ K
Tactic: refine ⟨F.image f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
refine_1 : (↑(Finset.card.{u_3} (α := H) (Finset.image (⇑f : (a : G) → H) F)) : ℝ) ≤ K
⊢ CovBySMul H K (HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2) ((⇑f : (a : G) → H) '' A)
have refine_2 : HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2 ⊆
  HSMul.hSMul (β := Set H) (↑(Finset.image (⇑f : (a : G) → H) F) : Set H) ((⇑f : (a : G) → H) '' A)
Tactic: refine ⟨F.image f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
⊢ HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2 ⊆
    HSMul.hSMul (β := Set H) (↑(Finset.image (⇑f : (a : G) → H) F) : Set H) ((⇑f : (a : G) → H) '' A)
have refine_2 : Subset.{u_3} (α := Set H) ((⇑f : (a : G) → H) '' HPow.hPow (β := ℕ) A 2) ((⇑f : (a : G) → H) '' ((↑F : Set G) * A))
Tactic: simp only [← Set.image_pow, Finset.coe_image, ← Set.image_mul, smul_eq_mul] at hAF ⊢
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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
⊢ CovBySMul H K (HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2) ((⇑f : (a : G) → H) '' A)
have 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)
Tactic: classical
    obtain ⟨F, hF, hAF⟩ := hA.sq_covBySMul
    refine ⟨F.image f, ?_, ?_⟩
    · calc
        (#(F.image f) : ℝ) ≤ #F := mod_cast F.card_image_le
        _ ≤ K := hF
    · simp only [← Set.image_pow, Finset.coe_image, ← Set.image_mul, smul_eq_mul] at hAF ⊢
      gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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)
have refine_1 : ∀ (F_1 : Finset G) (hF : (↑(#F_1) : ℝ) ≤ K) (hAF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F_1 : Set G) • A),
  (↑(Finset.card.{u_3} (α := H) (Finset.image (⇑f : (a : G) → H) F_1)) : ℝ) ≤ K
Tactic: classical
    obtain ⟨F, hF, hAF⟩ := hA.sq_covBySMul
    refine ⟨F.image f, ?_, ?_⟩
    · calc
        (#(F.image f) : ℝ) ≤ #F := mod_cast F.card_image_le
        _ ≤ K := hF
    · simp only [← Set.image_pow, Finset.coe_image, ← Set.image_mul, smul_eq_mul] at hAF ⊢
      gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
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)
refine_1 :
  ∀ (F_1 : Finset G) (hF : (↑(#F_1) : ℝ) ≤ K) (hAF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F_1 : Set G) • A),
    (↑(Finset.card.{u_3} (α := H) (Finset.image (⇑f : (a : G) → H) F_1)) : ℝ) ≤ K
⊢ CovBySMul H K (HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2) ((⇑f : (a : G) → H) '' A)
have refine_2 : ∀ (F_1 : Finset G) (hF : (↑(#F_1) : ℝ) ≤ K) (hAF : HPow.hPow (β := ℕ) A 2 ⊆ (↑F_1 : Set G) • A),
  HPow.hPow (α := Set H) (β := ℕ) ((⇑f : (a : G) → H) '' A) 2 ⊆
    HSMul.hSMul (β := Set H) (↑(Finset.image (⇑f : (a : G) → H) F_1) : Set H) ((⇑f : (a : G) → H) '' A)
Tactic: classical
    obtain ⟨F, hF, hAF⟩ := hA.sq_covBySMul
    refine ⟨F.image f, ?_, ?_⟩
    · calc
        (#(F.image f) : ℝ) ≤ #F := mod_cast F.card_image_le
        _ ≤ K := hF
    · simp only [← Set.image_pow, Finset.coe_image, ← Set.image_mul, smul_eq_mul] at hAF ⊢
      gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ApproximateSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
⊢ 1 ∈ HPow.hPow (β := ℕ) (↑A : Set G) 2
have rw : HMul.hMul (α := G) 1 1 ∈ (↑A : Set G) * (↑A : Set G)
Tactic: rw [sq, ← one_mul 1]