awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
A : Finset G
hA : t + 1 ≤ #A
κ₁ : κ + 1 = (κ + 1) / ((κ + 1) / (1 - K)) * ((κ + 1) / (1 - K))
κ₂ : (κ + 1) / ((κ + 1) / (1 - K)) * ((κ + 1) / (1 - K)) < (κ + 1) / ((κ + 1) / (1 - K)) * HAdd.hAdd (α := ℝ) (↑t : ℝ) 1
κ₃ : (κ + 1) / ((κ + 1) / (1 - K)) * HAdd.hAdd (α := ℝ) (↑t : ℝ) 1 = (1 - K) * HAdd.hAdd (α := ℝ) (↑t : ℝ) 1
⊢ κ + 1 < ex A
have κ₄ : (1 - K) * HAdd.hAdd (α := ℝ) (↑t : ℝ) 1 ≤ (1 - K) * (↑(#A) : ℝ)
Tactic: calc
          κ + 1
      _ = (κ + 1) / ((κ + 1) / (1 - K)) * ((κ + 1) / (1 - K)) := by field
      _ < (κ + 1) / ((κ + 1) / (1 - K)) * (t + 1) := by gcongr; exact Nat.lt_floor_add_one _
      _ = (1 - K) * (t + 1) := by field
      _ ≤ (1 - K) * #A      := by norm_cast; gcongr
      _ ≤ ex A              := mul_card_le_expansion hS
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
⊢ False
have largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
Tactic: have largeA {A : Finset G} (hA : t < #A) : κ + 1 < ex A := by
    rw [Nat.lt_iff_add_one_le] at hA
    calc
          κ + 1
      _ = (κ + 1) / ((κ + 1) / (1 - K)) * ((κ + 1) / (1 - K)) := by field
      _ < (κ + 1) / ((κ + 1) / (1 - K)) * (t + 1) := by gcongr; exact Nat.lt_floor_add_one _
      _ = (1 - K) * (t + 1) := by field
      _ ≤ (1 - K) * #A      := by norm_cast; gcongr
      _ ≤ ex A              := mul_card_le_expansion hS
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ ex A ∈ M
have rw : ex A ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) ∧ κ < ex A
Tactic: rw [mem_filter]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ ex A ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) ∧ κ < ex A
have refine_1 : Membership.mem (γ := Finset ℝ) (map Nat.castEmbedding (Icc (#S) (t * #S))) (↑(#(A * S)) : ℝ)
Tactic: refine ⟨sub_mem_sub ?_ ?_, (connectivity_le_expansion hK.le hS hA).lt_of_ne' <| H _ hA⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
refine_1 : Membership.mem (γ := Finset ℝ) (map Nat.castEmbedding (Icc (#S) (t * #S))) (↑(#(A * S)) : ℝ)
⊢ ex A ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) ∧ κ < ex A
have refine_2 : K * (↑(#A) : ℝ) ∈ K •> map Nat.castEmbedding (Icc 1 t)
Tactic: refine ⟨sub_mem_sub ?_ ?_, (connectivity_le_expansion hK.le hS hA).lt_of_ne' <| H _ hA⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ Membership.mem (γ := Finset ℝ) (map Nat.castEmbedding (Icc (#S) (t * #S))) (↑(#(A * S)) : ℝ)
have refine_1 : #(A * S) ∈ Icc (#S) (t * #S)
Tactic: apply mem_map_of_mem
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ #(A * S) ≤ t * #S
have grw : #A * #S ≤ t * #S
Tactic: grw [card_mul_le, hAt]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
grw : #A * #S ≤ t * #S
⊢ #(A * S) ≤ t * #S
have grw₁ : t * #S ≤ t * #S
Tactic: grw [card_mul_le, hAt]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ K * (↑(#A) : ℝ) ∈ K •> map Nat.castEmbedding (Icc 1 t)
have refine_2 : Membership.mem (γ := Finset ℝ) (map Nat.castEmbedding (Icc 1 t)) (↑(#A) : ℝ)
Tactic: apply smul_mem_smul_finset
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ Membership.mem (γ := Finset ℝ) (map Nat.castEmbedding (Icc 1 t)) (↑(#A) : ℝ)
have refine_2 : #A ∈ Icc 1 t
Tactic: apply mem_map_of_mem
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
⊢ False
have smallA : ∀ {A : Finset G} (hA : A.Nonempty) (hAt : #A ≤ t), ex A ∈ M
Tactic: have smallA {A : Finset G} (hA : A.Nonempty) (hAt : #A ≤ t) : ex A ∈ M := by
    rw [mem_filter]
    refine ⟨sub_mem_sub ?_ ?_, (connectivity_le_expansion hK.le hS hA).lt_of_ne' <| H _ hA⟩
    · apply mem_map_of_mem
      exact mem_Icc.2 ⟨card_le_card_mul_left hA, by grw [card_mul_le, hAt]⟩
    · apply smul_mem_smul_finset
      apply mem_map_of_mem
      exact mem_Icc.2 ⟨Nat.one_le_iff_ne_zero.mpr hA.card_ne_zero, hAt⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
smallA : ∀ {A : Finset G} (hA : A.Nonempty) (hAt : #A ≤ t), ex A ∈ M
⊢ False
have this : (M ∪ {κ + 1}).Nonempty
Tactic: have : (M ∪ {κ + 1}).Nonempty := by simp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
smallA : ∀ {A : Finset G} (hA : A.Nonempty) (hAt : #A ≤ t), ex A ∈ M
this : (M ∪ {κ + 1}).Nonempty
k : ℝ := (M ∪ {κ + 1}).min' this
⊢ False
have this₁ : κ < k
Tactic: have : κ < k := by simp [k, M]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
smallA : ∀ {A : Finset G} (hA : A.Nonempty) (hAt : #A ≤ t), ex A ∈ M
this_1 : (M ∪ {κ + 1}).Nonempty
k : ℝ := (M ∪ {κ + 1}).min' this_1
this : κ < k
⊢ False
have obtain : ∀ (A : Finset G) (hA : A.Nonempty) (hAk : expansion K S A < k), False
Tactic: obtain ⟨A, hA, hAk⟩ := (connectivity_lt_iff hK.le hS).mp this
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
smallA : ∀ {A : Finset G} (hA : A.Nonempty) (hAt : #A ≤ t), ex A ∈ M
this_1 : (M ∪ {κ + 1}).Nonempty
k : ℝ := (M ∪ {κ + 1}).min' this_1
this : κ < k
A : Finset G
hA : A.Nonempty
hAk : expansion K S A < k
⊢ False
have this₁ : ex A ≤ κ + 1
Tactic: have : ex A ≤ κ + 1 := hAk.le.trans <| min'_le _ _ (by simp)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G} (hA : t < #A), κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
smallA : ∀ {A : Finset G} (hA : A.Nonempty) (hAt : #A ≤ t), ex A ∈ M
this_1 : (M ∪ {κ + 1}).Nonempty
k : ℝ := (M ∪ {κ + 1}).min' this_1
this_2 : κ < k
A : Finset G
hA : A.Nonempty
hAk : expansion K S A < k
this : ex A ≤ κ + 1
⊢ False
have this₁ : #A ≤ t
Tactic: have := not_lt.mp (mt largeA this.not_gt)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
⊢ 0 < connectivity K S
have obtain : ∀ (A : Finset G) (hA : A.Nonempty) (hSA : IsFragment K S A), 0 < connectivity K S
Tactic: obtain ⟨A, hA, hSA⟩ := exists_nonempty_isFragment hK hS
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A S : Finset G
hK : K < 1
hS : S.Nonempty
hA : IsFragment K S A
⊢ A.Nonempty
have by_contra! : ∀ (hA : IsFragment K S ∅), False
Tactic: by_contra! rfl
Cleared hypotheses: A, hA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H), IsAtom K S (↑H : Set G).toFinset
have obtain : ∀ (N : Finset G) (hN : IsAtom K S N), ∃ (H : Subgroup G) (x : Fintype ↥H), IsAtom K S (↑H : Set G).toFinset
Tactic: obtain ⟨N, hN⟩ := exists_isAtom hK hS
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H), IsAtom K S (↑H : Set G).toFinset
have obtain : ∀ (n : G) (hn : n ∈ N), ∃ (H : Subgroup G) (x : Fintype ↥H), IsAtom K S (↑H : Set G).toFinset
Tactic: obtain ⟨n, hn⟩ := IsAtom.nonempty hK hS hN
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H), IsAtom K S (↑H : Set G).toFinset
have one_mem_carrier : 1 ∈ n⁻¹ •> N
Tactic: have one_mem_carrier : 1 ∈ n⁻¹ •> N := by simpa [mem_inv_smul_finset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
x : G
⊢ x ∈ x •> n⁻¹ •> N
have one_mem_carrier₁ : x •> 1 ∈ x •> n⁻¹ •> N
Tactic: apply smul_mem_smul_finset (a := x) at one_mem_carrier
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H), IsAtom K S (↑H : Set G).toFinset
have self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
Tactic: have self_mem_smul_carrier (x : G) : x ∈ x • n⁻¹ • N := by
    apply smul_mem_smul_finset (a := x) at one_mem_carrier
    simpa only [smul_eq_mul, mul_one] using one_mem_carrier
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a b : G
ha : a ∈ n⁻¹ •> (↑N : Set G)
hb : b ∈ n⁻¹ •> (↑N : Set G)
⊢ a * b ∈ n⁻¹ •> (↑N : Set G)
have rw : ∀ (ha : a ∈ n⁻¹ •> N) (hb : b ∈ n⁻¹ •> N), a * b ∈ n⁻¹ •> N
Tactic: rw [← coe_smul_finset, mem_coe] at *
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a b : G
ha : a ∈ n⁻¹ •> N
hb : b ∈ n⁻¹ •> N
⊢ a * b ∈ n⁻¹ •> N
have hb₁ : a •> b ∈ a •> n⁻¹ •> N
Tactic: apply smul_mem_smul_finset (a := a) at hb
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a b : G
ha : a ∈ n⁻¹ •> N
hb_1 : b ∈ n⁻¹ •> N
hb : a •> b ∈ a •> n⁻¹ •> N
⊢ a * b ∈ n⁻¹ •> N
have hb₁ : a * b ∈ a •> n⁻¹ •> N
Tactic: rw [smul_eq_mul] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a b : G
ha : a ∈ n⁻¹ •> N
hb_1 : b ∈ n⁻¹ •> N
hb : a * b ∈ a •> n⁻¹ •> N
⊢ a * b ∈ n⁻¹ •> N
have this : (n⁻¹ •> N ∩ a •> n⁻¹ •> N).Nonempty
Tactic: have : (n⁻¹ •> N ∩ a •> n⁻¹ •> N).Nonempty := ⟨a, by
        simpa only [mem_inter] using ⟨ha, self_mem_smul_carrier a⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a : G
ha : a ∈ n⁻¹ •> (↑N : Set G)
⊢ a⁻¹ ∈ n⁻¹ •> (↑N : Set G)
have rw : ∀ (ha : a ∈ n⁻¹ •> N), a⁻¹ ∈ n⁻¹ •> N
Tactic: rw [← coe_smul_finset, mem_coe] at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a : G
ha : a ∈ n⁻¹ •> N
⊢ a⁻¹ ∈ n⁻¹ •> N
have ha₁ : a⁻¹ •> a ∈ a⁻¹ •> n⁻¹ •> N
Tactic: apply smul_mem_smul_finset (a := a⁻¹) at ha
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a : G
ha_1 : a ∈ n⁻¹ •> N
ha : a⁻¹ •> a ∈ a⁻¹ •> n⁻¹ •> N
⊢ a⁻¹ ∈ n⁻¹ •> N
have ha₁ : 1 ∈ a⁻¹ •> n⁻¹ •> N
Tactic: rw [smul_eq_mul, inv_mul_cancel] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a : G
ha_1 : a ∈ n⁻¹ •> N
ha : 1 ∈ a⁻¹ •> n⁻¹ •> N
⊢ a⁻¹ ∈ n⁻¹ •> N
have this : (n⁻¹ •> N ∩ a⁻¹ •> n⁻¹ •> N).Nonempty
Tactic: have : (n⁻¹ •> N ∩ a⁻¹ •> n⁻¹ •> N).Nonempty := ⟨1, by simpa using ⟨one_mem_carrier, ha⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
H : Subgroup G := { carrier := n⁻¹ •> (↑N : Set G), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H), IsAtom K S (↑H : Set G).toFinset
have refine_1 : ∀ (a : G), a ∈ n⁻¹ •> N ↔ a ∈ (↑H : Set G)
Tactic: refine ⟨H, Fintype.ofFinset (n⁻¹ •> N) fun a => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
H : Subgroup G := { carrier := n⁻¹ •> (↑N : Set G), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
refine_1 : ∀ (a : G), a ∈ n⁻¹ •> N ↔ a ∈ (↑H : Set G)
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H), IsAtom K S (↑H : Set G).toFinset
have refine_2 : IsAtom K S (↑H : Set G).toFinset
Tactic: refine ⟨H, Fintype.ofFinset (n⁻¹ •> N) fun a => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
hA : ∃ (A : Finset G), #S ≤ #A ∧ (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
K : ℝ := 1 - ε / 2
⊢ 1 - ε / 2 < 1
have linarith : 1 ≤ 1 - ε / 2 → 2 / 2 = 1
Tactic: linarith [hε₀]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
hA : ∃ (A : Finset G), #S ≤ #A ∧ (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
K : ℝ := 1 - ε / 2
linarith : 1 ≤ 1 - ε / 2 → 2 / 2 = 1
⊢ 1 - ε / 2 < 1
have linarith₁ : 1 ≤ 1 - ε / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [hε₀]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
hA : ∃ (A : Finset G), #S ≤ #A ∧ (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
K : ℝ := 1 - ε / 2
linarith : 1 ≤ 1 - ε / 2 → 2 / 2 = 1
linarith₁ : 1 ≤ 1 - ε / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 - ε / 2 < 1
have linarith₂ : 1 ≤ 1 - ε / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [hε₀]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
hA : ∃ (A : Finset G), #S ≤ #A ∧ (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
K : ℝ := 1 - ε / 2
linarith : 1 ≤ 1 - ε / 2 → 2 / 2 = 1
linarith₁ : 1 ≤ 1 - ε / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 ≤ 1 - ε / 2 → GT.gt (α := ℝ) 2 0
⊢ 1 - ε / 2 < 1
have linarith₃ : 1 ≤ 1 - ε / 2 → 0 - ε + (HMul.hMul (α := ℝ) 2 1 - (HMul.hMul (α := ℝ) 2 1 - 1 * ε)) = 0
Tactic: linarith [hε₀]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
hA : ∃ (A : Finset G), #S ≤ #A ∧ (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
K : ℝ := 1 - ε / 2
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G),
    (↑(Fintype.card.{u_1} ↥H) : ℝ) ≤ (2 / ε - 1) * (↑(#S) : ℝ) ∧
      (↑(#Z) : ℝ) ≤ 2 / ε - 1 ∧ (↑S : Set G) ⊆ (↑H : Set G) * (↑Z : Set G)
have hK : K < 1
Tactic: have hK : K < 1 := by unfold K; linarith [hε₀]