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 : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this_1 : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * (↑(#A) : ℝ) < (↑(#(A ∩ z⁻¹ •> A)) : ℝ)
hrw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(#(A ∩ w •> A)) : ℝ)
this : LT.lt (α := ℝ) 0 (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
⊢ z •> w ∈ S

Tactic:
simpa [S, card_smul_inter_smul, Finset.Nonempty, mem_mul, mem_inv, -mem_inv', and_assoc]
      using this

Premises used: Finset.mem_inv', and_assoc, Finset.Nonempty, Finset.mem_inv, Finset.card_smul_inter_smul, Finset.mem_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S : Finset G
⊢ expansion K S ∅ = 0

Tactic:
simp [expansion]

Premises used: _private.0.Finset.expansion
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A S : Finset G
hS : S.Nonempty
rw : (↑(#A) : ℝ) - K * (↑(#A) : ℝ) ≤ (↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ)
⊢ (1 - K) * (↑(#A) : ℝ) ≤ expansion K S A

Tactic:
rw [one_sub_mul, expansion]

Premises used: one_sub_mul, _private.0.Finset.expansion
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A S : Finset G
hS : S.Nonempty
⊢ #A ≤ #(A * S)

Tactic:
have := card_le_card_mul_right hS (s := A)
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A S : Finset G
hS : S.Nonempty
this : #A ≤ #(A * S)
⊢ (↑(#A) : ℝ) - K * (↑(#A) : ℝ) ≤ (↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ)

Tactic:
gcongr
-- 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
nlinarith :
  expansion K S A < 0 →
    expansion K S A - 0 + ((1 - K) * (↑(#A) : ℝ) - expansion K S A) + (0 - HSub.hSub (α := ℝ) 0 (↑(#A) : ℝ) * (K - 1)) =
      0
⊢ 0 ≤ expansion K S A

Tactic:
nlinarith [mul_card_le_expansion (K := K) hS (A := A)]

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 : ℝ
A S : Finset G
hK : K < 1
hS : S.Nonempty
hA : A.Nonempty
⊢ LT.lt (α := ℝ) 0 (↑(#A) : ℝ)

Tactic:
simp [hA]
-- 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 : A.Nonempty
⊢ LT.lt (α := ℝ) 0 (↑(#A) : ℝ)

Tactic:
have : (0 : ℝ) < #A := by simp [hA]
-- 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 : A.Nonempty
this : LT.lt (α := ℝ) 0 (↑(#A) : ℝ)
nlinarith :
  expansion K S A ≤ 0 →
    expansion K S A - 0 + ((1 - K) * (↑(#A) : ℝ) - expansion K S A) + (0 - (K - 1) * HSub.hSub (α := ℝ) 0 (↑(#A) : ℝ)) =
      0
⊢ 0 < expansion K S A

Tactic:
nlinarith [mul_card_le_expansion (K := K) hS (A := A)]

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 : ℝ
A S : Finset G
hK : K < 1
hS : S.Nonempty
hA : 0 < expansion K S A
by_contra! : ∀ (hA : 0 < expansion 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 : 0 < expansion K S ∅
⊢ False

Tactic:
simp at hA
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
S A : Finset G
a : G
⊢ expansion K S (a •> A) = expansion K S A

Tactic:
simp [expansion, smul_mul_assoc]

Premises used: smul_mul_assoc, _private.0.Finset.expansion
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
⊢ HAdd.hAdd (α := ℝ) (↑(#(A ∩ B)) : ℝ) (↑(#(A ∪ B)) : ℝ) = HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)

Tactic:
have : (#(A ∩ B) + #(A ∪ B) : ℝ) = #A + #B := mod_cast card_inter_add_card_union A B
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
this : HAdd.hAdd (α := ℝ) (↑(#(A ∩ B)) : ℝ) (↑(#(A ∪ B)) : ℝ) = HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)
⊢ K * (↑(#(A ∩ B)) : ℝ) + K * (↑(#(A ∪ B)) : ℝ) = K * (↑(#A) : ℝ) + K * (↑(#B) : ℝ)

Tactic:
simp only [← mul_add, this]

Premises used: mul_add
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
this : HAdd.hAdd (α := ℝ) (↑(#(A ∩ B)) : ℝ) (↑(#(A ∪ B)) : ℝ) = HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)
⊢ K * (↑(#(A ∩ B)) : ℝ) + K * (↑(#(A ∪ B)) : ℝ) = K * (↑(#A) : ℝ) + K * (↑(#B) : ℝ)

Tactic:
have : K * #(A ∩ B) + K * #(A ∪ B) = K * #A + K * #B := by simp only [← mul_add, this]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
this_1 : HAdd.hAdd (α := ℝ) (↑(#(A ∩ B)) : ℝ) (↑(#(A ∪ B)) : ℝ) = HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)
this : K * (↑(#(A ∩ B)) : ℝ) + K * (↑(#(A ∪ B)) : ℝ) = K * (↑(#A) : ℝ) + K * (↑(#B) : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑(#(A * S ∩ (B * S))) : ℝ) (↑(#(A * S ∪ B * S)) : ℝ) =
    HAdd.hAdd (α := ℝ) (↑(#(A * S)) : ℝ) (↑(#(B * S)) : ℝ)

Tactic:
have : (#(A * S ∩ (B * S)) + #(A * S ∪ B * S) : ℝ) = #(A * S) + #(B * S) :=
    mod_cast card_inter_add_card_union (A * S) (B * S)
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
this_1 : HAdd.hAdd (α := ℝ) (↑(#(A ∩ B)) : ℝ) (↑(#(A ∪ B)) : ℝ) = HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)
this_2 : K * (↑(#(A ∩ B)) : ℝ) + K * (↑(#(A ∪ B)) : ℝ) = K * (↑(#A) : ℝ) + K * (↑(#B) : ℝ)
this :
  HAdd.hAdd (α := ℝ) (↑(#(A * S ∩ (B * S))) : ℝ) (↑(#(A * S ∪ B * S)) : ℝ) =
    HAdd.hAdd (α := ℝ) (↑(#(A * S)) : ℝ) (↑(#(B * S)) : ℝ)
grw grw₁ : LE.le (α := ℝ) (↑(#(A * S ∩ (B * S))) : ℝ) (↑(#(A * S ∩ (B * S))) : ℝ)
⊢ LE.le (α := ℝ) (↑(#(A ∩ B * S)) : ℝ) (↑(#(A * S ∩ (B * S))) : ℝ)

Tactic:
grw [inter_mul_subset]

Premises used: Finset.inter_mul_subset
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
this_1 : HAdd.hAdd (α := ℝ) (↑(#(A ∩ B)) : ℝ) (↑(#(A ∪ B)) : ℝ) = HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)
this_2 : K * (↑(#(A ∩ B)) : ℝ) + K * (↑(#(A ∪ B)) : ℝ) = K * (↑(#A) : ℝ) + K * (↑(#B) : ℝ)
this :
  HAdd.hAdd (α := ℝ) (↑(#(A * S ∩ (B * S))) : ℝ) (↑(#(A * S ∪ B * S)) : ℝ) =
    HAdd.hAdd (α := ℝ) (↑(#(A * S)) : ℝ) (↑(#(B * S)) : ℝ)
⊢ LE.le (α := ℝ) (↑(#(A ∩ B * S)) : ℝ) (↑(#(A * S ∩ (B * S))) : ℝ)

Tactic:
have : (#((A ∩ B) * S) : ℝ) ≤ #(A * S ∩ (B * S)) := by grw [inter_mul_subset]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
this_1 : HAdd.hAdd (α := ℝ) (↑(#(A ∩ B)) : ℝ) (↑(#(A ∪ B)) : ℝ) = HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)
this_2 : K * (↑(#(A ∩ B)) : ℝ) + K * (↑(#(A ∪ B)) : ℝ) = K * (↑(#A) : ℝ) + K * (↑(#B) : ℝ)
this_3 :
  HAdd.hAdd (α := ℝ) (↑(#(A * S ∩ (B * S))) : ℝ) (↑(#(A * S ∪ B * S)) : ℝ) =
    HAdd.hAdd (α := ℝ) (↑(#(A * S)) : ℝ) (↑(#(B * S)) : ℝ)
this : LE.le (α := ℝ) (↑(#(A ∩ B * S)) : ℝ) (↑(#(A * S ∩ (B * S))) : ℝ)
simp_rw :
  (↑(#(A ∩ B * S)) : ℝ) - K * (↑(#(A ∩ B)) : ℝ) + ((↑(#(A * S ∪ B * S)) : ℝ) - K * (↑(#(A ∪ B)) : ℝ)) ≤
    (↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ) + ((↑(#(B * S)) : ℝ) - K * (↑(#B) : ℝ))
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B

Tactic:
simp_rw [expansion, union_mul]

Premises used: Finset.union_mul, _private.0.Finset.expansion
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
this_1 : HAdd.hAdd (α := ℝ) (↑(#(A ∩ B)) : ℝ) (↑(#(A ∪ B)) : ℝ) = HAdd.hAdd (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)
this_2 : K * (↑(#(A ∩ B)) : ℝ) + K * (↑(#(A ∪ B)) : ℝ) = K * (↑(#A) : ℝ) + K * (↑(#B) : ℝ)
this_3 :
  HAdd.hAdd (α := ℝ) (↑(#(A * S ∩ (B * S))) : ℝ) (↑(#(A * S ∪ B * S)) : ℝ) =
    HAdd.hAdd (α := ℝ) (↑(#(A * S)) : ℝ) (↑(#(B * S)) : ℝ)
this : LE.le (α := ℝ) (↑(#(A ∩ B * S)) : ℝ) (↑(#(A * S ∩ (B * S))) : ℝ)
nlinarith :
  (↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ) + ((↑(#(B * S)) : ℝ) - K * (↑(#B) : ℝ)) <
      (↑(#(A ∩ B * S)) : ℝ) - K * (↑(#(A ∩ B)) : ℝ) + ((↑(#(A * S ∪ B * S)) : ℝ) - K * (↑(#(A ∪ B)) : ℝ)) →
    -(K * (↑(#(A ∩ B)) : ℝ) + K * (↑(#(A ∪ B)) : ℝ) - (K * (↑(#A) : ℝ) + K * (↑(#B) : ℝ))) +
            (HAdd.hAdd (α := ℝ) (↑(#(A * S ∩ (B * S))) : ℝ) (↑(#(A * S ∪ B * S)) : ℝ) -
              HAdd.hAdd (α := ℝ) (↑(#(A * S)) : ℝ) (↑(#(B * S)) : ℝ)) +
          HSub.hSub (α := ℝ) (↑(#(A ∩ B * S)) : ℝ) (↑(#(A * S ∩ (B * S))) : ℝ) +
        ((↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ) + ((↑(#(B * S)) : ℝ) - K * (↑(#B) : ℝ)) -
          ((↑(#(A ∩ B * S)) : ℝ) - K * (↑(#(A ∩ B)) : ℝ) + ((↑(#(A * S ∪ B * S)) : ℝ) - K * (↑(#(A ∪ B)) : ℝ)))) =
      0
⊢ (↑(#(A ∩ B * S)) : ℝ) - K * (↑(#(A ∩ B)) : ℝ) + ((↑(#(A * S ∪ B * S)) : ℝ) - K * (↑(#(A ∪ B)) : ℝ)) ≤
    (↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ) + ((↑(#(B * S)) : ℝ) - K * (↑(#B) : ℝ))

Tactic:
nlinarith
-- 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
⊢ Membership.mem (γ := Set ℝ)
    (lowerBounds (Set.range fun (A : { A : Finset G // A.Nonempty }) ↦ expansion K S (↑A : Finset G))) 0

Tactic:
simp [lowerBounds, *]

Premises used: lowerBounds
-- 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
r : ℝ
⊢ Finset.Nonempty (α := G) {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
r : ℝ
⊢ Nonempty.{max 1 (u_1 + 1)} { A : Finset G // A.Nonempty }

Tactic:
have : Nonempty {A : Finset G // A.Nonempty} := ⟨{1}, 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
r : ℝ
this : Nonempty.{max 1 (u_1 + 1)} { A : Finset G // A.Nonempty }
⊢ r ≤ connectivity K S ↔ ∀ ⦃A : Finset G⦄, A.Nonempty → r ≤ expansion K S A

Tactic:
simp [connectivity, le_ciInf_iff, bddBelow_expansion, *]

Premises used: _private.0.Finset.bddBelow_expansion, _private.0.Finset.connectivity, le_ciInf_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
r : ℝ
this : Nonempty.{max 1 (u_1 + 1)} { A : Finset G // A.Nonempty }
⊢ connectivity K S < r ↔ ∃ (A : Finset G), A.Nonempty ∧ expansion K S A < r

Tactic:
simp [connectivity, ciInf_lt_iff, bddBelow_expansion, *]

Premises used: _private.0.Finset.bddBelow_expansion, ciInf_lt_iff, _private.0.Finset.connectivity
-- 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 : A.Nonempty
⊢ connectivity K S ≤ expansion K S A

Tactic:
(le_connectivity_iff hK hS).1 le_rfl hA

Premises used: le_rfl, Iff.mp, _private.0.Finset.le_connectivity_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
⊢ 0 ≤ connectivity K S

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A S : Finset G
hA : IsAtom K S A
⊢ IsFragment K S A

Tactic:
hA.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A S : Finset G
a : G
⊢ IsFragment K S (a •> A) ↔ IsFragment K S A

Tactic:
simp [IsFragment]

Premises used: _private.0.Finset.IsFragment
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A S : Finset G
a : G
⊢ IsAtom K S (a •> A) ↔ IsAtom K S A

Tactic:
simp [IsAtom, MinimalFor]

Premises used: _private.0.Finset.IsAtom, MinimalFor
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A S : Finset G
a : G
hA : IsFragment K S A
⊢ IsFragment K S (a •> A)

Tactic:
isFragment_smul_finset.2 hA

Premises used: Iff.mpr, _private.0.Finset.isFragment_smul_finset
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A S : Finset G
a : G
hA : IsAtom K S A
⊢ IsAtom K S (a •> A)

Tactic:
isAtom_smul_finset.2 hA

Premises used: Iff.mpr, _private.0.Finset.isAtom_smul_finset
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hA : expansion K S A = connectivity K S
hB : expansion K S B = connectivity K S
hAB : (A ∩ B).Nonempty
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B

Tactic:
have := expansion_submodularity (S := S) (A := A) (B := B) (K := K)
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hA : expansion K S A = connectivity K S
hB : expansion K S B = connectivity K S
hAB : (A ∩ B).Nonempty
this : expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
⊢ connectivity K S ≤ expansion K S (A ∩ B)

Tactic:
have := connectivity_le_expansion hK hS hAB
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hA : expansion K S A = connectivity K S
hB : expansion K S B = connectivity K S
hAB : (A ∩ B).Nonempty
this_1 : expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
this : connectivity K S ≤ expansion K S (A ∩ B)
⊢ connectivity K S ≤ expansion K S (A ∪ B)

Tactic:
have := connectivity_le_expansion hK hS <| hAB.mono inter_subset_union
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hA : expansion K S A = connectivity K S
hB : expansion K S B = connectivity K S
hAB : (A ∩ B).Nonempty
this_1 : expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
this_2 : connectivity K S ≤ expansion K S (A ∩ B)
this : connectivity K S ≤ expansion K S (A ∪ B)
linarith :
  expansion K S (A ∩ B) < connectivity K S →
    connectivity K S - expansion K S (A ∩ B) + (expansion K S (A ∩ B) - connectivity K S) = 0
linarith₁ :
  connectivity K S < expansion K S (A ∩ B) →
    expansion K S A - connectivity K S + (expansion K S B - connectivity K S) +
            (expansion K S (A ∩ B) + expansion K S (A ∪ B) - (expansion K S A + expansion K S B)) +
          (connectivity K S - expansion K S (A ∪ B)) +
        (connectivity K S - expansion K S (A ∩ B)) =
      0
⊢ expansion K S (A ∩ B) = connectivity K S

Tactic:
linarith
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hA : IsAtom K S A
hB : IsAtom K S B
hAB : (A ∩ B).Nonempty
⊢ IsFragment K S (A ∩ B)

Tactic:
replace hAB := hA.isFragment.inter hK hS hB.isFragment hAB
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hA : IsAtom K S A
hB : IsAtom K S B
hAB : IsFragment K S (A ∩ B)
grw grw₁ : #A ≤ #A
⊢ #(A ∩ B) ≤ #A

Tactic:
grw [inter_subset_left]

Premises used: Finset.inter_subset_left
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hA : IsAtom K S A
hB : IsAtom K S B
hAB : IsFragment K S (A ∩ B)
⊢ #A ≤ #(A ∩ B)

Tactic:
replace hA := hA.2 hAB <| by grw [inter_subset_left]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hB : IsAtom K S B
hAB : IsFragment K S (A ∩ B)
hA : #A ≤ #(A ∩ B)
grw grw₁ : #B ≤ #B
⊢ #(A ∩ B) ≤ #B

Tactic:
grw [inter_subset_right]

Premises used: Finset.inter_subset_right
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hB : IsAtom K S B
hAB : IsFragment K S (A ∩ B)
hA : #A ≤ #(A ∩ B)
⊢ #B ≤ #(A ∩ B)

Tactic:
replace hB := hB.2 hAB <| by grw [inter_subset_right]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hAB : IsFragment K S (A ∩ B)
hA : #A ≤ #(A ∩ B)
hB : #B ≤ #(A ∩ B)
⊢ A ∩ B = A

Tactic:
replace hA := eq_of_subset_of_card_le inter_subset_left hA
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hAB : IsFragment K S (A ∩ B)
hB : #B ≤ #(A ∩ B)
hA : A ∩ B = A
⊢ A ∩ B = B

Tactic:
replace hB := eq_of_subset_of_card_le inter_subset_right hB
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hAB : IsFragment K S (A ∩ B)
hA : A ∩ B = A
hB : A ∩ B = B
⊢ A = B

Tactic:
hA.symm.trans hB

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hAB : IsFragment K S (A ∩ B)
hA : A ∩ B = A
hB : A ∩ B = B
⊢ A = B

Tactic:
exact hA.symm.trans hB

Premises used: Eq.symm, Eq.trans
-- 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
by_contra! : ∀ (H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A), False
⊢ ∃ (A : Finset G), A.Nonempty ∧ IsFragment K S A

Tactic:
by_contra! H
-- 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
linarith : κ + 1 ≤ 0 → -1 + (κ + 1 - 0) + (0 - connectivity K S) = 0
⊢ 0 < κ + 1

Tactic:
linarith [connectivity_nonneg hK.le hS]

Premises used: LT.lt.le, _private.0.Finset.connectivity_nonneg
-- 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
⊢ 0 < κ + 1

Tactic:
have κ_add_one_pos : 0 < κ + 1 := by linarith [connectivity_nonneg hK.le 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
linarith : 1 - K ≤ 0 → K - 1 + (1 - K - 0) = 0
⊢ 0 < 1 - K

Tactic:
linarith
-- 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
⊢ 0 < 1 - K

Tactic:
have one_sub_K_pos : 0 < 1 - K := by linarith
-- 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
⊢ t + 1 ≤ #A

Tactic:
rw [Nat.lt_iff_add_one_le] at hA

Premises used: Nat.lt_iff_add_one_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)⌋₊
A : Finset G
hA : t + 1 ≤ #A
⊢ κ + 1 = (κ + 1) / ((κ + 1) / (1 - K)) * ((κ + 1) / (1 - K))

Tactic:
field
-- 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
hbc : (κ + 1) / (1 - K) < HAdd.hAdd (α := ℝ) (↑t : ℝ) 1
⊢ (κ + 1) / ((κ + 1) / (1 - K)) * ((κ + 1) / (1 - K)) < (κ + 1) / ((κ + 1) / (1 - K)) * HAdd.hAdd (α := ℝ) (↑t : ℝ) 1

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) / (1 - K) < HAdd.hAdd (α := ℝ) (↑t : ℝ) 1

Tactic:
Nat.lt_floor_add_one _

Premises used: Nat.lt_floor_add_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
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 - K) < HAdd.hAdd (α := ℝ) (↑t : ℝ) 1

Tactic:
exact Nat.lt_floor_add_one _

Premises used: Nat.lt_floor_add_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
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 - K)) * HAdd.hAdd (α := ℝ) (↑t : ℝ) 1 = (1 - K) * HAdd.hAdd (α := ℝ) (↑t : ℝ) 1

Tactic:
field