awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
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
⊢ (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) = (1 - ε / 2) * (↑(#S) : ℝ)
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
have ex₁ : (↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ) - (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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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 (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
have ex₂ : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) = (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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G),
    (↑(Fintype.card.{u_1} ↥H) : ℝ) ≤ (2 / ε - 1) * (↑(#S) : ℝ) ∧
      (↑(#Z) : ℝ) ≤ 2 / ε - 1 ∧ (↑S : Set G) ⊆ (↑H : Set G) * (↑Z : Set G)
have calc₁ : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 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)
have refine : (↑(Fintype.card.{u_1} ↥H) : ℝ) ≤ (2 / ε - 1) * (↑(#S) : ℝ)
Tactic: refine ⟨H, inferInstance, Z, ?cardH, ?cardZ, by
    simpa only [hHZS] using Set.subset_mul_right _ H.one_mem⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
refine : (↑(Fintype.card.{u_1} ↥H) : ℝ) ≤ (2 / ε - 1) * (↑(#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)
have refine₁ : (↑(#Z) : ℝ) ≤ 2 / ε - 1
Tactic: refine ⟨H, inferInstance, Z, ?cardH, ?cardZ, by
    simpa only [hHZS] using Set.subset_mul_right _ H.one_mem⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
⊢ (↑(Fintype.card.{u_1} ↥H) : ℝ) ≤ (2 / ε - 1) * (↑(#S) : ℝ)
have rw : ε / 2 * (↑(Fintype.card.{u_1} ↥H) : ℝ) ≤ ε / 2 * ((2 / ε - 1) * (↑(#S) : ℝ))
Tactic: rw [← mul_le_mul_iff_right₀ (a := ε / 2) (by positivity)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
⊢ ε / 2 * (↑(Fintype.card.{u_1} ↥H) : ℝ) ≤ ε / 2 * ((2 / ε - 1) * (↑(#S) : ℝ))
have ε₁ : ε / 2 * (↑(Fintype.card.{u_1} ↥H) : ℝ) = ε / 2 * (↑(#(↑H : Set G).toFinset) : ℝ)
Tactic: calc
            ε / 2 * (Fintype.card H)
        _ = ε / 2 * #(H : Set G).toFinset   := by
          simp only [Set.toFinset_card, SetLike.coe_sort_coe]
        _ = (1 - K) * #(H : Set G).toFinset := by ring
        _ ≤ ex (Set.toFinset H)             := mul_card_le_expansion hS
        _ ≤ (1 - ε / 2) * #S                := calc₁
        _ = ε / 2 * ((2 / ε - 1) * #S)      := by field
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
ε₁ : ε / 2 * (↑(Fintype.card.{u_1} ↥H) : ℝ) = ε / 2 * (↑(#(↑H : Set G).toFinset) : ℝ)
⊢ ε / 2 * (↑(Fintype.card.{u_1} ↥H) : ℝ) ≤ ε / 2 * ((2 / ε - 1) * (↑(#S) : ℝ))
have ε₂ : ε / 2 * (↑(#(↑H : Set G).toFinset) : ℝ) = (1 - K) * (↑(#(↑H : Set G).toFinset) : ℝ)
Tactic: calc
            ε / 2 * (Fintype.card H)
        _ = ε / 2 * #(H : Set G).toFinset   := by
          simp only [Set.toFinset_card, SetLike.coe_sort_coe]
        _ = (1 - K) * #(H : Set G).toFinset := by ring
        _ ≤ ex (Set.toFinset H)             := mul_card_le_expansion hS
        _ ≤ (1 - ε / 2) * #S                := calc₁
        _ = ε / 2 * ((2 / ε - 1) * #S)      := by field
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
ε₁ : ε / 2 * (↑(Fintype.card.{u_1} ↥H) : ℝ) = ε / 2 * (↑(#(↑H : Set G).toFinset) : ℝ)
ε₂ : ε / 2 * (↑(#(↑H : Set G).toFinset) : ℝ) = (1 - K) * (↑(#(↑H : Set G).toFinset) : ℝ)
⊢ ε / 2 * (↑(Fintype.card.{u_1} ↥H) : ℝ) ≤ ε / 2 * ((2 / ε - 1) * (↑(#S) : ℝ))
have ε₃ : (1 - ε / 2) * (↑(#S) : ℝ) = ε / 2 * ((2 / ε - 1) * (↑(#S) : ℝ))
Tactic: calc
            ε / 2 * (Fintype.card H)
        _ = ε / 2 * #(H : Set G).toFinset   := by
          simp only [Set.toFinset_card, SetLike.coe_sort_coe]
        _ = (1 - K) * #(H : Set G).toFinset := by ring
        _ ≤ ex (Set.toFinset H)             := mul_card_le_expansion hS
        _ ≤ (1 - ε / 2) * #S                := calc₁
        _ = ε / 2 * ((2 / ε - 1) * #S)      := by field
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * Z)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * S)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ)
have e_a : (↑H : Set G).toFinset * Z = (↑H : Set G).toFinset * S
Tactic: congr 3
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
⊢ (↑(#Z) : ℝ) ≤ 2 / ε - 1
have _ : HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * S)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) ≤
  (2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ)
Tactic: calc
          (#Z : ℝ)
      _ = #(H : Set G).toFinset * #Z / #(H : Set G).toFinset          := by field
      _ = #(Set.toFinset H * Z) / #(H : Set G).toFinset               := by
        simp [← card_mul_eq_mul_card_of_injOn_opSMul hZinj, Nat.cast_mul]
      _ = #(Set.toFinset H * S) / #(H : Set G).toFinset               := by
        congr 3; simpa using congr(($hHZS).toFinset)
      _ ≤ (2 / ε - 1) * #(H : Set G).toFinset / #(H : Set G).toFinset := ?_
      _ = 2 / ε - 1                                                   := by field
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * S)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) ≤
    (2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ)
have hab : (↑(#((↑H : Set G).toFinset * S)) : ℝ) ≤ (2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
⊢ 0 < 1 - K
have linarith : 1 - K ≤ 0 → 2 / 2 = 1
Tactic: linarith [hK]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
linarith : 1 - K ≤ 0 → 2 / 2 = 1
⊢ 0 < 1 - K
have linarith₁ : 1 - K ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [hK]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
linarith : 1 - K ≤ 0 → 2 / 2 = 1
linarith₁ : 1 - K ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 < 1 - K
have linarith₂ : 1 - K ≤ 0 → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith [hK]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
linarith : 1 - K ≤ 0 → 2 / 2 = 1
linarith₁ : 1 - K ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - K ≤ 0 → HMul.hMul (α := ℝ) 2 1 = 2
⊢ 0 < 1 - K
have linarith₃ : 1 - K ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [hK]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
linarith : 1 - K ≤ 0 → 2 / 2 = 1
linarith₁ : 1 - K ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - K ≤ 0 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 1 - K ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < 1 - K
have linarith₄ : 1 - K ≤ 0 → K - 1 + (1 - K - 0) = 0
Tactic: linarith [hK]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
⊢ (↑(#((↑H : Set G).toFinset * S)) : ℝ) ≤ (2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ)
have hab : (1 - K) * (↑(#((↑H : Set G).toFinset * S)) : ℝ) ≤ (1 - K) * ((2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ))
Tactic: rw [← mul_le_mul_iff_right₀ (show 0 < 1 - K by linarith [hK])]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
this : (1 - K) * (↑(#((↑H : Set G).toFinset * S)) : ℝ) ≤ (1 - ε / 2) * (↑(#(↑H : Set G).toFinset) : ℝ)
⊢ (1 - K) * (↑(#((↑H : Set G).toFinset * S)) : ℝ) ≤ (1 - K) * ((2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ))
have apply : (1 - ε / 2) * (↑(#(↑H : Set G).toFinset) : ℝ) = (1 - K) * ((2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ))
Tactic: apply le_of_le_of_eq this
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
this : (1 - K) * (↑(#((↑H : Set G).toFinset * S)) : ℝ) ≤ (1 - ε / 2) * (↑(#(↑H : Set G).toFinset) : ℝ)
⊢ (1 - ε / 2) * (↑(#(↑H : Set G).toFinset) : ℝ) = (1 - K) * ((2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ))
have simp : (1 - ε / 2) * (↑(Fintype.card.{u_1} ↥H) : ℝ) = ε / 2 * ((2 / ε - 1) * (↑(Fintype.card.{u_1} ↥H) : ℝ))
Tactic: simp [K]