awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
norm_cast : (1 - K) * (↑(t + 1) : ℝ) ≤ (1 - K) * (↑(#A) : ℝ)
⊢ (1 - K) * HAdd.hAdd (α := ℝ) (↑t : ℝ) 1 ≤ (1 - K) * (↑(#A) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
ha : 0 ≤ 1 - K
⊢ (1 - K) * (↑(t + 1) : ℝ) ≤ (1 - K) * (↑(#A) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 - K) * (↑(#A) : ℝ) ≤ ex A

Tactic:
mul_card_le_expansion hS

Premises used: _private.0.Finset.mul_card_le_expansion
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 - K) * HAdd.hAdd (α := ℝ) (↑t : ℝ) 1 ≤ (1 - K) * (↑(#A) : ℝ)
⊢ κ + 1 < ex 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

Premises used: HSub.hSub, HDiv.hDiv, _private.0.Finset.mul_card_le_expansion, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 < #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
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
rw : ex A ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) ∧ κ < ex A
⊢ ex A ∈ M

Tactic:
rw [mem_filter]

Premises used: Finset.mem_filter
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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

Tactic:
⟨sub_mem_sub ?_ ?_, (connectivity_le_expansion hK.le hS hA).lt_of_ne' <| H _ hA⟩

Premises used: Finset.sub_mem_sub, LT.lt.le, And.intro, LE.le.lt_of_ne', _private.0.Finset.connectivity_le_expansion
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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)) : ℝ)
refine_2 : K * (↑(#A) : ℝ) ∈ K •> map Nat.castEmbedding (Icc 1 t)
⊢ ex A ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) ∧ κ < ex A

Tactic:
refine ⟨sub_mem_sub ?_ ?_, (connectivity_le_expansion hK.le hS hA).lt_of_ne' <| H _ hA⟩
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 : #(A * S) ∈ Icc (#S) (t * #S)
⊢ Membership.mem (γ := Finset ℝ) (map Nat.castEmbedding (Icc (#S) (t * #S))) (↑(#(A * S)) : ℝ)

Tactic:
apply mem_map_of_mem

Premises used: Finset.mem_map_of_mem
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
grw₁ grw₂ : t * #S ≤ t * #S
⊢ #(A * S) ≤ t * #S

Tactic:
grw [card_mul_le, hAt]

Premises used: Finset.card_mul_le
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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) ∈ Icc (#S) (t * #S)

Tactic:
exact mem_Icc.2 ⟨card_le_card_mul_left hA, by grw [card_mul_le, hAt]⟩

Premises used: Iff.mpr, Finset.mem_Icc, And.intro, Finset.card_le_card_mul_left
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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_2 : Membership.mem (γ := Finset ℝ) (map Nat.castEmbedding (Icc 1 t)) (↑(#A) : ℝ)
⊢ K * (↑(#A) : ℝ) ∈ K •> map Nat.castEmbedding (Icc 1 t)

Tactic:
apply smul_mem_smul_finset

Premises used: Finset.smul_mem_smul_finset
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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_2 : #A ∈ Icc 1 t
⊢ Membership.mem (γ := Finset ℝ) (map Nat.castEmbedding (Icc 1 t)) (↑(#A) : ℝ)

Tactic:
apply mem_map_of_mem

Premises used: Finset.mem_map_of_mem
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 ∈ Icc 1 t

Tactic:
mem_Icc.2 ⟨Nat.one_le_iff_ne_zero.mpr hA.card_ne_zero, hAt⟩

Premises used: Iff.mpr, Finset.mem_Icc, And.intro, Finset.Nonempty.card_ne_zero, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 ∈ Icc 1 t

Tactic:
exact mem_Icc.2 ⟨Nat.one_le_iff_ne_zero.mpr hA.card_ne_zero, hAt⟩

Premises used: Iff.mpr, Finset.mem_Icc, And.intro, Finset.Nonempty.card_ne_zero, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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

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⟩
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ (M ∪ {κ + 1}).Nonempty

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ (M ∪ {κ + 1}).Nonempty

Tactic:
have : (M ∪ {κ + 1}).Nonempty := by simp
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ κ < k

Tactic:
simp [k, M]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ κ < k

Tactic:
have : κ < k := by simp [k, M]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
obtain : ∀ (A : Finset G) (hA : A.Nonempty) (hAk : expansion K S A < k), False
⊢ False

Tactic:
obtain ⟨A, hA, hAk⟩ := (connectivity_lt_iff hK.le hS).mp this

Premises used: LT.lt.le, _private.0.Finset.connectivity_lt_iff, Iff.mp
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ κ + 1 ∈ M ∪ {κ + 1}

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ ex A ≤ κ + 1

Tactic:
have : ex A ≤ κ + 1 := hAk.le.trans <| min'_le _ _ (by simp)
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ #A ≤ t

Tactic:
have := not_lt.mp (mt largeA this.not_gt)
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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_3 : ex A ≤ κ + 1
this : #A ≤ t
⊢ False

Tactic:
hAk.not_ge <| min'_le (M ∪ {κ + 1}) _ <| subset_union_left <| smallA hA this

Premises used: Finset.min'_le, Finset.subset_union_left, HAdd.hAdd, Union.union, LT.lt.not_ge, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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_3 : ex A ≤ κ + 1
this : #A ≤ t
⊢ False

Tactic:
exact hAk.not_ge <| min'_le (M ∪ {κ + 1}) _ <| subset_union_left <| smallA hA this

Premises used: Finset.min'_le, Finset.subset_union_left, HAdd.hAdd, Union.union, LT.lt.not_ge, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
⊢ ∃ (A : Finset G), IsFragment K S A

Tactic:
let ⟨A, _, hA⟩ := exists_nonempty_isFragment hK hS; ⟨A, hA⟩

Premises used: _private.0.Finset.IsFragment, Exists, _private.0.Finset.exists_nonempty_isFragment, _private.0.Finset.exists_isFragment.match_1, Exists.intro
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
⊢ ∃ (A : Finset G), IsAtom K S A

Tactic:
exists_minimalFor_of_wellFoundedLT _ _ <| exists_isFragment hK hS

Premises used: exists_minimalFor_of_wellFoundedLT, _private.0.Finset.exists_isFragment, _private.0.Finset.IsAtom
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
obtain : ∀ (A : Finset G) (hA : A.Nonempty) (hSA : IsFragment K S A), 0 < connectivity K S
⊢ 0 < connectivity K S

Tactic:
obtain ⟨A, hA, hSA⟩ := exists_nonempty_isFragment hK hS

Premises used: _private.0.Finset.exists_nonempty_isFragment
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
A : Finset G
hA : A.Nonempty
hSA : IsFragment K S A
⊢ 0 < connectivity K S

Tactic:
(expansion_pos hK hS hA).trans_eq hSA

Premises used: LT.lt.trans_eq, _private.0.Finset.expansion_pos
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
A : Finset G
hA : A.Nonempty
hSA : IsFragment K S A
⊢ 0 < connectivity K S

Tactic:
exact (expansion_pos hK hS hA).trans_eq hSA

Premises used: LT.lt.trans_eq, _private.0.Finset.expansion_pos
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
⊢ ¬IsFragment K S ∅

Tactic:
simp [IsFragment, (connectivity_pos hK hS).ne]

Premises used: _private.0.Finset.IsFragment, _private.0.Finset.connectivity_pos, LT.lt.ne
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
by_contra! : ∀ (hA : IsFragment K S ∅), False
⊢ A.Nonempty

Tactic:
by_contra! rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
hA : IsFragment K S ∅
⊢ False

Tactic:
simp [*, not_isFragment_empty hK hS] at hA

Premises used: _private.0.Finset.not_isFragment_empty
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A S : Finset G
hK : K < 1
hS : S.Nonempty
hA : IsAtom K S A
⊢ A.Nonempty

Tactic:
hA.isFragment.nonempty hK hS

Premises used: _private.0.Finset.IsFragment.nonempty, _private.0.Finset.IsAtom.isFragment
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
obtain : ∀ (N : Finset G) (hN : IsAtom K S N), ∃ (H : Subgroup G) (x : Fintype ↥H), IsAtom K S (↑H : Set G).toFinset
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H), IsAtom K S (↑H : Set G).toFinset

Tactic:
obtain ⟨N, hN⟩ := exists_isAtom hK hS

Premises used: _private.0.Finset.exists_isAtom