awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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 : 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)) : ℝ)
⊢ z •> w ∈ S
have this₁ : LT.lt (α := ℝ) 0 (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
Tactic: have : (0 : ℝ) < #((z⁻¹ •> A) ∩ (w •> A)) := by
      have : (#((A ∩ z⁻¹ •> A) ∩ (A ∩ w •> A)) : ℝ) ≤ #(z⁻¹ •> A ∩ w •> A) := by
        gcongr <;> exact inter_subset_right
      have : (#((A ∩ z⁻¹ •> A) ∪ (A ∩ w •> A)) : ℝ) ≤ #A := by
        gcongr; exact union_subset inter_subset_left inter_subset_left
      have :
          (#((A ∩ z⁻¹ •> A) ∩ (A ∩ w •> A)) + #((A ∩ z⁻¹ •> A) ∪ (A ∩ w •> A)) : ℝ) =
            #(A ∩ z⁻¹ •> A) + #(A ∩ w •> A) := mod_cast card_inter_add_card_union ..
      linarith
-- 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
hS : S.Nonempty
⊢ (1 - K) * (↑(#A) : ℝ) ≤ expansion K S A
have rw : (↑(#A) : ℝ) - K * (↑(#A) : ℝ) ≤ (↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ)
Tactic: rw [one_sub_mul, expansion]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A S : Finset G
hS : S.Nonempty
⊢ (↑(#A) : ℝ) - K * (↑(#A) : ℝ) ≤ (↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ)
have this : #A ≤ #(A * S)
Tactic: have := card_le_card_mul_right hS (s := A)
-- 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
⊢ 0 ≤ expansion K S A
have 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
Tactic: nlinarith [mul_card_le_expansion (K := K) hS (A := A)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ 0 < expansion K S A
have this : LT.lt (α := ℝ) 0 (↑(#A) : ℝ)
Tactic: have : (0 : ℝ) < #A := by simp [hA]
-- 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 : A.Nonempty
this : LT.lt (α := ℝ) 0 (↑(#A) : ℝ)
⊢ 0 < expansion K S A
have 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
Tactic: nlinarith [mul_card_le_expansion (K := K) hS (A := A)]
-- 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 : 0 < expansion K S A
⊢ A.Nonempty
have by_contra! : ∀ (hA : 0 < expansion K S ∅), False
Tactic: by_contra! rfl
Cleared hypotheses: A, hA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B S : Finset G
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
have this : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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) : ℝ)
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
have this₁ : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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) : ℝ)
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
have this₁ : 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)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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))) : ℝ)
have grw : LE.le (α := ℝ) (↑(#(A * S ∩ (B * S))) : ℝ) (↑(#(A * S ∩ (B * S))) : ℝ)
Tactic: grw [inter_mul_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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)) : ℝ)
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
have this₁ : LE.le (α := ℝ) (↑(#(A ∩ B * S)) : ℝ) (↑(#(A * S ∩ (B * S))) : ℝ)
Tactic: have : (#((A ∩ B) * S) : ℝ) ≤ #(A * S ∩ (B * S)) := by grw [inter_mul_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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))) : ℝ)
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
have simp_rw : (↑(#(A ∩ B * S)) : ℝ) - K * (↑(#(A ∩ B)) : ℝ) + ((↑(#(A * S ∪ B * S)) : ℝ) - K * (↑(#(A ∪ B)) : ℝ)) ≤
  (↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ) + ((↑(#(B * S)) : ℝ) - K * (↑(#B) : ℝ))
Tactic: simp_rw [expansion, union_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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))) : ℝ)
⊢ (↑(#(A ∩ B * S)) : ℝ) - K * (↑(#(A ∩ B)) : ℝ) + ((↑(#(A * S ∪ B * S)) : ℝ) - K * (↑(#(A ∪ B)) : ℝ)) ≤
    (↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ) + ((↑(#(B * S)) : ℝ) - K * (↑(#B) : ℝ))
have 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
Tactic: nlinarith
-- 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
r : ℝ
⊢ r ≤ connectivity K S ↔ ∀ ⦃A : Finset G⦄, A.Nonempty → r ≤ expansion K S A
have this : Nonempty.{max 1 (u_1 + 1)} { A : Finset G // A.Nonempty }
Tactic: have : Nonempty {A : Finset G // A.Nonempty} := ⟨{1}, 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
r : ℝ
⊢ connectivity K S < r ↔ ∃ (A : Finset G), A.Nonempty ∧ expansion K S A < r
have this : Nonempty.{max 1 (u_1 + 1)} { A : Finset G // A.Nonempty }
Tactic: have : Nonempty {A : Finset G // A.Nonempty} := ⟨{1}, 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 : ℝ
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) = connectivity K S
have this : 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)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ expansion K S (A ∩ B) = connectivity K S
have this₁ : connectivity K S ≤ expansion K S (A ∩ B)
Tactic: have := connectivity_le_expansion hK hS hAB
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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)
⊢ expansion K S (A ∩ B) = connectivity K S
have this₁ : connectivity K S ≤ expansion K S (A ∪ B)
Tactic: have := connectivity_le_expansion hK hS <| hAB.mono inter_subset_union
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
⊢ expansion K S (A ∩ B) = connectivity K S
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ expansion K S (A ∩ B) = connectivity K S
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ A = B
have hAB₁ : IsFragment K S (A ∩ B)
Tactic: replace hAB := hA.isFragment.inter hK hS hB.isFragment hAB
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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 ∩ B) ≤ #A
have grw : #A ≤ #A
Tactic: grw [inter_subset_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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 = B
have hA₁ : #A ≤ #(A ∩ B)
Tactic: replace hA := hA.2 hAB <| by grw [inter_subset_left]
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
⊢ #(A ∩ B) ≤ #B
have grw : #B ≤ #B
Tactic: grw [inter_subset_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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)
⊢ A = B
have hB₁ : #B ≤ #(A ∩ B)
Tactic: replace hB := hB.2 hAB <| by grw [inter_subset_right]
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 : ℝ
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
have hA₁ : A ∩ B = A
Tactic: replace hA := eq_of_subset_of_card_le inter_subset_left 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 : ℝ
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
have hB₁ : A ∩ B = B
Tactic: replace hB := eq_of_subset_of_card_le inter_subset_right hB
Cleared hypotheses: hB
-- 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
⊢ ∃ (A : Finset G), A.Nonempty ∧ IsFragment K S A
have by_contra! : ∀ (H : ∀ (A : Finset G) (_ : A.Nonempty), ¬IsFragment K S A), False
Tactic: by_contra! H
-- 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
⊢ 0 < κ + 1
have linarith : κ + 1 ≤ 0 → -1 + (κ + 1 - 0) + (0 - connectivity K S) = 0
Tactic: linarith [connectivity_nonneg hK.le 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
⊢ False
have κ_add_one_pos : 0 < κ + 1
Tactic: have κ_add_one_pos : 0 < κ + 1 := by linarith [connectivity_nonneg hK.le 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
⊢ 0 < 1 - K
have linarith : 1 - K ≤ 0 → K - 1 + (1 - K - 0) = 0
Tactic: linarith
-- 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
⊢ False
have one_sub_K_pos : 0 < 1 - K
Tactic: have one_sub_K_pos : 0 < 1 - K := by linarith
-- 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)⌋₊
A : Finset G
hA : t < #A
⊢ κ + 1 < ex A
have hA₁ : t + 1 ≤ #A
Tactic: rw [Nat.lt_iff_add_one_le] at hA
Cleared hypotheses: 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)⌋₊
A : Finset G
hA : t + 1 ≤ #A
⊢ (κ + 1) / ((κ + 1) / (1 - K)) * ((κ + 1) / (1 - K)) < (κ + 1) / ((κ + 1) / (1 - K)) * HAdd.hAdd (α := ℝ) (↑t : ℝ) 1
have hbc : (κ + 1) / (1 - K) < HAdd.hAdd (α := ℝ) (↑t : ℝ) 1
Tactic: gcongr
-- 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 - K) * HAdd.hAdd (α := ℝ) (↑t : ℝ) 1 ≤ (1 - K) * (↑(#A) : ℝ)
have norm_cast : (1 - K) * (↑(t + 1) : ℝ) ≤ (1 - K) * (↑(#A) : ℝ)
Tactic: norm_cast
-- 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 - K) * (↑(t + 1) : ℝ) ≤ (1 - K) * (↑(#A) : ℝ)
have ha : 0 ≤ 1 - K
Tactic: gcongr
-- 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 < ex A
have κ₁ : κ + 1 = (κ + 1) / ((κ + 1) / (1 - K)) * ((κ + 1) / (1 - K))
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 (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 < ex A
have κ₂ : (κ + 1) / ((κ + 1) / (1 - K)) * ((κ + 1) / (1 - K)) < (κ + 1) / ((κ + 1) / (1 - K)) * HAdd.hAdd (α := ℝ) (↑t : ℝ) 1
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 (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 < ex A
have κ₃ : (κ + 1) / ((κ + 1) / (1 - K)) * HAdd.hAdd (α := ℝ) (↑t : ℝ) 1 = (1 - K) * HAdd.hAdd (α := ℝ) (↑t : ℝ) 1
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