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
N : Finset G
hN : IsAtom K S N
obtain : ∀ (n : G) (hn : n ∈ 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⟩ := IsAtom.nonempty hK hS hN

Premises used: _private.0.Finset.IsAtom.nonempty
-- 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
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
⊢ 1 ∈ n⁻¹ •> N

Tactic:
simpa [mem_inv_smul_finset_iff]

Premises used: Finset.mem_inv_smul_finset_iff
-- 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
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
⊢ 1 ∈ n⁻¹ •> N

Tactic:
have one_mem_carrier : 1 ∈ n⁻¹ •> N := by simpa [mem_inv_smul_finset_iff]
-- 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
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
x : G
⊢ x •> 1 ∈ x •> n⁻¹ •> N

Tactic:
apply smul_mem_smul_finset (a := x) at one_mem_carrier

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
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier_1 : 1 ∈ n⁻¹ •> N
x : G
one_mem_carrier : x •> 1 ∈ x •> n⁻¹ •> N
⊢ x ∈ x •> n⁻¹ •> N

Tactic:
simpa only [smul_eq_mul, mul_one] using one_mem_carrier

Premises used: smul_eq_mul, mul_one
-- 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
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

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
-- 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
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)
rw : ∀ (ha : a ∈ n⁻¹ •> N) (hb : b ∈ n⁻¹ •> N), a * b ∈ n⁻¹ •> N
⊢ a * b ∈ n⁻¹ •> (↑N : Set G)

Tactic:
rw [← coe_smul_finset, mem_coe] at *

Premises used: Finset.coe_smul_finset, Finset.mem_coe
-- 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
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 ∈ a •> n⁻¹ •> N

Tactic:
apply smul_mem_smul_finset (a := a) at hb

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
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 ∈ a •> n⁻¹ •> N

Tactic:
rw [smul_eq_mul] at hb

Premises used: smul_eq_mul
-- 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
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 ∈ n⁻¹ •> N ∩ a •> n⁻¹ •> N

Tactic:
simpa only [mem_inter] using ⟨ha, self_mem_smul_carrier a⟩

Premises used: Finset.mem_inter
-- 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
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
⊢ (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⟩⟩
-- 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
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
this : (n⁻¹ •> N ∩ a •> n⁻¹ •> N).Nonempty
⊢ a * b ∈ n⁻¹ •> N

Tactic:
simpa only [← (hN.smul_finset n⁻¹).eq_of_inter_nonempty hK.le hS
        ((hN.smul_finset n⁻¹).smul_finset a) this] using hb

Premises used: _private.0.Finset.IsAtom.eq_of_inter_nonempty, LT.lt.le, _private.0.Finset.IsAtom.smul_finset, Inv.inv
-- 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
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)
rw : ∀ (ha : a ∈ n⁻¹ •> N), a⁻¹ ∈ n⁻¹ •> N
⊢ a⁻¹ ∈ n⁻¹ •> (↑N : Set G)

Tactic:
rw [← coe_smul_finset, mem_coe] at *

Premises used: Finset.coe_smul_finset, Finset.mem_coe
-- 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
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⁻¹ •> a ∈ a⁻¹ •> n⁻¹ •> N

Tactic:
apply smul_mem_smul_finset (a := a⁻¹) at ha

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
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
⊢ 1 ∈ a⁻¹ •> n⁻¹ •> N

Tactic:
rw [smul_eq_mul, inv_mul_cancel] at ha

Premises used: inv_mul_cancel, smul_eq_mul
-- 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
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
⊢ 1 ∈ n⁻¹ •> N ∩ a⁻¹ •> n⁻¹ •> N

Tactic:
simpa using ⟨one_mem_carrier, 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
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
⊢ (n⁻¹ •> N ∩ a⁻¹ •> n⁻¹ •> N).Nonempty

Tactic:
have : (n⁻¹ •> N ∩ a⁻¹ •> n⁻¹ •> N).Nonempty := ⟨1, by simpa using ⟨one_mem_carrier, 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
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
this : (n⁻¹ •> N ∩ a⁻¹ •> n⁻¹ •> N).Nonempty
⊢ a⁻¹ ∈ n⁻¹ •> N

Tactic:
simpa only [← (hN.smul_finset n⁻¹).eq_of_inter_nonempty hK.le hS
        ((hN.smul_finset n⁻¹).smul_finset a⁻¹) this] using self_mem_smul_carrier a⁻¹

Premises used: _private.0.Finset.IsAtom.eq_of_inter_nonempty, LT.lt.le, _private.0.Finset.IsAtom.smul_finset, Inv.inv
-- 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
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

Tactic:
⟨H, Fintype.ofFinset (n⁻¹ •> N) fun a => ?_, ?_⟩

Premises used: Fintype.ofFinset, Inv.inv, Exists.intro, HSMul.hSMul
-- 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
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)
refine_2 : IsAtom K S (↑H : Set G).toFinset
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H), IsAtom K S (↑H : Set G).toFinset

Tactic:
refine ⟨H, Fintype.ofFinset (n⁻¹ •> N) fun a => ?_, ?_⟩
-- 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
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' := ⋯ }
a : G
⊢ a ∈ n⁻¹ •> N ↔ a ∈ (↑H : Set G)

Tactic:
simpa only [← mem_coe, coe_smul_finset] using H.mem_carrier

Premises used: Finset.coe_smul_finset, Subgroup.mem_carrier, Finset.mem_coe
-- 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
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' := ⋯ }
⊢ IsAtom K S (↑H : Set G).toFinset

Tactic:
simpa [Set.toFinset_smul_set, toFinset_coe, H] using IsAtom.smul_finset n⁻¹ hN

Premises used: Finset.toFinset_coe, _private.0.Finset.IsAtom.smul_finset, Inv.inv, Set.toFinset_smul_set
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
unfold : 1 - ε / 2 < 1
⊢ K < 1

Tactic:
unfold K
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
linarith₃ : 1 ≤ 1 - ε / 2 → 0 - ε + (HMul.hMul (α := ℝ) 2 1 - (HMul.hMul (α := ℝ) 2 1 - 1 * ε)) = 0
⊢ 1 - ε / 2 < 1

Tactic:
linarith [hε₀]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ K < 1

Tactic:
have hK : K < 1 := by unfold K; linarith [hε₀]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
hK : K < 1
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
obtain :
  ∀ (H : Subgroup G) (w : Fintype ↥H) (hH : IsAtom K S (↑H : Set G).toFinset),
    ∃ (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)
⊢ ∃ (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)

Tactic:
obtain ⟨H, _, hH⟩ := exists_subgroup_isAtom hK hS

Premises used: _private.0.Finset.exists_subgroup_isAtom
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
hK : K < 1
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w : Fintype ↥H
hH : IsAtom K S (↑H : Set G).toFinset
obtain :
  ∀ (Z : Finset G) (hZS : Z ⊆ S) (hHZS : (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G))
    (hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)),
    ∃ (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)
⊢ ∃ (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)

Tactic:
obtain ⟨Z, hZS, hHZS, hZinj⟩ := exists_subset_mul_eq_mul_injOn H S

Premises used: _private.0.Finset.exists_subset_mul_eq_mul_injOn
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
hK : K < 1
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w : Fintype ↥H
hH : IsAtom K S (↑H : Set G).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
obtain :
  ∀ (A : Finset G) (hA₁ : #S ≤ #A) (hA₂ : (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)),
    ∃ (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)
⊢ ∃ (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)

Tactic:
obtain ⟨A, hA₁, hA₂⟩ := hA
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w : Fintype ↥H
hH : IsAtom K S (↑H : Set G).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
A : Finset G
hA₁ : #S ≤ #A
hA₂ : (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
⊢ ex (↑H : Set G).toFinset = κ

Tactic:
hH.isFragment

Premises used: _private.0.Finset.IsFragment, _private.0.Finset.IsAtom.isFragment
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w : Fintype ↥H
hH : IsAtom K S (↑H : Set G).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
A : Finset G
hA₁ : #S ≤ #A
hA₂ : (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
⊢ κ ≤ (↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ)

Tactic:
connectivity_le_expansion hK.le hS <| card_pos.mp <| hS.card_pos.trans_le hA₁

Premises used: Finset.Nonempty.card_pos, LT.lt.le, LT.lt.trans_le, Iff.mp, Finset.card_pos, _private.0.Finset.expansion, _private.0.Finset.connectivity_le_expansion
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w : Fintype ↥H
hH : IsAtom K S (↑H : Set G).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
A : Finset G
hA₁ : #S ≤ #A
hA₂ : (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
hcd : 0 ≤ 1 - ε / 2
⊢ (↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w : Fintype ↥H
hH : IsAtom K S (↑H : Set G).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
A : Finset G
hA₁ : #S ≤ #A
hA₂ : (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
linarith : 1 - ε / 2 < 0 → 2 / 2 = 1
linarith₁ : 1 - ε / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - ε / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 - ε / 2 < 0 → -1 + (ε - 1) + (HMul.hMul (α := ℝ) 2 1 - 1 * ε - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 ≤ 1 - ε / 2

Tactic:
linarith
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w : Fintype ↥H
hH : IsAtom K S (↑H : Set G).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
A : Finset G
hA₁ : #S ≤ #A
hA₂ : (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
linarith : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) < (1 - ε / 2) * (↑(#S) : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁ : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) < (1 - ε / 2) * (↑(#S) : ℝ) → 2 / 2 = 1
linarith₂ : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) < (1 - ε / 2) * (↑(#S) : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₃ : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) < (1 - ε / 2) * (↑(#S) : ℝ) → HMul.hMul (α := ℝ) 2 1 = 2
linarith₄ : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) < (1 - ε / 2) * (↑(#S) : ℝ) → 2 / 2 = 1
linarith₅ : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) < (1 - ε / 2) * (↑(#S) : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) < (1 - ε / 2) * (↑(#S) : ℝ) → HMul.hMul (α := ℝ) 2 1 = 2
linarith₇ : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) < (1 - ε / 2) * (↑(#S) : ℝ) → GT.gt (α := ℝ) 2 0
linarith₈ :
  (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) < (1 - ε / 2) * (↑(#S) : ℝ) →
    (HMul.hMul (α := ℝ) 1 2 - 1 * ε) * HMul.hMul (α := ℝ) 2 (↑(#S) : ℝ) -
          (HMul.hMul (α := ℝ) 2 1 - 1 * ε) * HMul.hMul (α := ℝ) 1 (↑(#S) : ℝ) -
        (HMul.hMul (α := ℝ) 2 1 - 1 * ε) * HMul.hMul (α := ℝ) 1 (↑(#S) : ℝ) =
      0
linarith₉ : (1 - ε / 2) * (↑(#S) : ℝ) < (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) → 2 / 2 = 1
linarith₁₀ : (1 - ε / 2) * (↑(#S) : ℝ) < (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : (1 - ε / 2) * (↑(#S) : ℝ) < (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) → HMul.hMul (α := ℝ) 2 1 = 2
linarith₁₂ : (1 - ε / 2) * (↑(#S) : ℝ) < (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₃ : (1 - ε / 2) * (↑(#S) : ℝ) < (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) → 2 / 2 = 1
linarith₁₄ : (1 - ε / 2) * (↑(#S) : ℝ) < (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₅ : (1 - ε / 2) * (↑(#S) : ℝ) < (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) → HMul.hMul (α := ℝ) 2 1 = 2
linarith₁₆ : (1 - ε / 2) * (↑(#S) : ℝ) < (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) → GT.gt (α := ℝ) 2 0
linarith₁₇ :
  (1 - ε / 2) * (↑(#S) : ℝ) < (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) →
    (HMul.hMul (α := ℝ) 2 1 - 1 * ε) * HMul.hMul (α := ℝ) 1 (↑(#S) : ℝ) -
        ((HMul.hMul (α := ℝ) 1 2 - 1 * ε) * HMul.hMul (α := ℝ) 2 (↑(#S) : ℝ) -
          (HMul.hMul (α := ℝ) 2 1 - 1 * ε) * HMul.hMul (α := ℝ) 1 (↑(#S) : ℝ)) =
      0
⊢ (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) = (1 - ε / 2) * (↑(#S) : ℝ)

Tactic:
linarith
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w : Fintype ↥H
hH : IsAtom K S (↑H : Set G).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
A : Finset G
hA₁ : #S ≤ #A
hA₂ : (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
ex₁ : (↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ)
ex₂ : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) = (1 - ε / 2) * (↑(#S) : ℝ)
⊢ ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)

Tactic:
calc
          ex (Set.toFinset H)
      _ = κ                               := hH.isFragment
      _ ≤ #(A * S) - K * #A :=
        connectivity_le_expansion hK.le hS <| card_pos.mp <| hS.card_pos.trans_le hA₁
      _ ≤ (2 - ε) * #S - (1 - ε / 2) * #S := by gcongr; linarith
      _ = (1 - ε / 2) * #S                := by linarith

Premises used: HMul.hMul, HSub.hSub, Finset.Nonempty.card_pos, HDiv.hDiv, LT.lt.le, _private.0.Finset.IsAtom.isFragment, Set.toFinset, SetLike.coe, LT.lt.trans_le, Iff.mp, Finset.card_pos, OfNat.ofNat, _private.0.Finset.connectivity_le_expansion
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
K : ℝ := 1 - ε / 2
hK : K < 1
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w : Fintype ↥H
hH : IsAtom K S (↑H : Set G).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
A : Finset G
hA₁ : #S ≤ #A
hA₂ : (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
⊢ ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)

Tactic:
have calc₁ : ex (Set.toFinset H) ≤ (1 - ε / 2) * #S := by
    calc
          ex (Set.toFinset H)
      _ = κ                               := hH.isFragment
      _ ≤ #(A * S) - K * #A :=
        connectivity_le_expansion hK.le hS <| card_pos.mp <| hS.card_pos.trans_le hA₁
      _ ≤ (2 - ε) * #S - (1 - ε / 2) * #S := by gcongr; linarith
      _ = (1 - ε / 2) * #S                := by linarith