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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
⊢ (1 - K) * (↑(#((↑H : Set G).toFinset * S)) : ℝ) ≤ (1 - K) * ((2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ))
have hab : (1 - K) * (↑(#((↑H : Set G).toFinset * S)) : ℝ) ≤ (1 - ε / 2) * (↑(#(↑H : Set G).toFinset) : ℝ)
Tactic: suffices (1 - K) * #(Set.toFinset H * S) ≤ (1 - ε / 2) * #(H : Set G).toFinset by
      apply le_of_le_of_eq this; simp [K]; 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) : ℝ)
⊢ (1 - K) * (↑(#((↑H : Set G).toFinset * S)) : ℝ) ≤ (1 - ε / 2) * (↑(#(↑H : Set G).toFinset) : ℝ)
have hab : (↑(#((↑H : Set G).toFinset * S)) : ℝ) ≤
  (1 - ε / 2) * (↑(#(↑H : Set G).toFinset) : ℝ) + K * (↑(#((↑H : Set G).toFinset * S)) : ℝ)
Tactic: rw [sub_mul, one_mul, sub_le_iff_le_add]
-- 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) : ℝ)
⊢ K * (↑(#(↑H : Set G).toFinset) : ℝ) + ex (↑H : Set G).toFinset ≤
    K * (↑(#(↑H : Set G).toFinset) : ℝ) + (1 - ε / 2) * (↑(#((↑H : Set G).toFinset * S)) : ℝ)
have grw : K * (↑(#(↑H : Set G).toFinset) : ℝ) + (1 - ε / 2) * (↑(#S) : ℝ) ≤
  K * (↑(#(↑H : Set G).toFinset) : ℝ) + (1 - ε / 2) * (↑(#((↑H : Set G).toFinset * S)) : ℝ)
Tactic: grw [calc₁]
-- 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) : ℝ)
⊢ K * (↑(#(↑H : Set G).toFinset) : ℝ) + (1 - ε / 2) * (↑(#S) : ℝ) ≤
    K * (↑(#(↑H : Set G).toFinset) : ℝ) + (1 - ε / 2) * (↑(#((↑H : Set G).toFinset * S)) : ℝ)
have bc : 0 ≤ 1 - ε / 2
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) : ℝ)
bc : 0 ≤ 1 - ε / 2
⊢ K * (↑(#(↑H : Set G).toFinset) : ℝ) + (1 - ε / 2) * (↑(#S) : ℝ) ≤
    K * (↑(#(↑H : Set G).toFinset) : ℝ) + (1 - ε / 2) * (↑(#((↑H : Set G).toFinset * S)) : ℝ)
have bc₁ : S ⊆ (↑H : Set G).toFinset * S
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 - ε / 2
have linarith : 1 - ε / 2 < 0 → 2 / 2 = 1
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
linarith : 1 - ε / 2 < 0 → 2 / 2 = 1
⊢ 0 ≤ 1 - ε / 2
have linarith₁ : 1 - ε / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
linarith : 1 - ε / 2 < 0 → 2 / 2 = 1
linarith₁ : 1 - ε / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ 1 - ε / 2
have linarith₂ : 1 - ε / 2 < 0 → GT.gt (α := ℝ) 2 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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 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 → 2 / 2 = 1
linarith₄ : 1 - ε / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ 1 - ε / 2
have linarith₅ : 1 - ε / 2 < 0 → HMul.hMul (α := ℝ) 2 1 = 2
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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 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 → 2 / 2 = 1
linarith₄ : 1 - ε / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 1 - ε / 2 < 0 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₆ : 1 - ε / 2 < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ 1 - ε / 2
have linarith₇ : 1 - ε / 2 < 0 → -1 + (ε - 1) + (HMul.hMul (α := ℝ) 2 1 - 1 * ε - HMul.hMul (α := ℝ) 2 0) = 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) : ℝ)
calc₁ : ex (↑H : Set G).toFinset ≤ (1 - ε / 2) * (↑(#S) : ℝ)
⊢ (↑(#((↑H : Set G).toFinset * S)) : ℝ) ≤
    (1 - ε / 2) * (↑(#(↑H : Set G).toFinset) : ℝ) + K * (↑(#((↑H : Set G).toFinset * S)) : ℝ)
have H₁ : (↑(#((↑H : Set G).toFinset * S)) : ℝ) =
  K * (↑(#(↑H : Set G).toFinset) : ℝ) + ((↑(#((↑H : Set G).toFinset * S)) : ℝ) - K * (↑(#(↑H : Set G).toFinset) : ℝ))
Tactic: calc
          (#(Set.toFinset H * S) : ℝ)
      _ = K * #(H : Set G).toFinset + (#(Set.toFinset H * S) - K * #(H : Set G).toFinset) := by ring
      _ = K * #(H : Set G).toFinset + ex (Set.toFinset H)                 := rfl
      _ ≤ K * #(H : Set G).toFinset + (1 - ε / 2) * #(Set.toFinset H * S) := by
        grw [calc₁]
        gcongr
        · linarith
        · simp only [Set.mem_toFinset, SetLike.mem_coe, H.one_mem, subset_mul_right]
-- 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₁ :
  (↑(#((↑H : Set G).toFinset * S)) : ℝ) =
    K * (↑(#(↑H : Set G).toFinset) : ℝ) + ((↑(#((↑H : Set G).toFinset * S)) : ℝ) - K * (↑(#(↑H : Set G).toFinset) : ℝ))
⊢ (↑(#((↑H : Set G).toFinset * S)) : ℝ) ≤
    (1 - ε / 2) * (↑(#(↑H : Set G).toFinset) : ℝ) + K * (↑(#((↑H : Set G).toFinset * S)) : ℝ)
have H₂ : K * (↑(#(↑H : Set G).toFinset) : ℝ) + ex (↑H : Set G).toFinset ≤
  K * (↑(#(↑H : Set G).toFinset) : ℝ) + (1 - ε / 2) * (↑(#((↑H : Set G).toFinset * S)) : ℝ)
Tactic: calc
          (#(Set.toFinset H * S) : ℝ)
      _ = K * #(H : Set G).toFinset + (#(Set.toFinset H * S) - K * #(H : Set G).toFinset) := by ring
      _ = K * #(H : Set G).toFinset + ex (Set.toFinset H)                 := rfl
      _ ≤ K * #(H : Set G).toFinset + (1 - ε / 2) * #(Set.toFinset H * S) := by
        grw [calc₁]
        gcongr
        · linarith
        · simp only [Set.mem_toFinset, SetLike.mem_coe, H.one_mem, subset_mul_right]
-- 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 case : (↑(#Z) : ℝ) = HMul.hMul (α := ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) (↑(#Z) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ)
Tactic: case cardZ =>
    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
    gcongr
    -- Finally, to show `#(HS) ≤ (2 / ε - 1) * #H`, we multiply both sides by `1 - K = ε / 2` and
    -- show `#(HS) = K * #H + ex H ≤ K * #H + (1 - ε / 2) * #S ≤ K * #H + (1 - ε / 2) * #(HS)`,
    -- where we used `calc₁` again.
    rw [← mul_le_mul_iff_right₀ (show 0 < 1 - K by linarith [hK])]
    suffices (1 - K) * #(Set.toFinset H * S) ≤ (1 - ε / 2) * #(H : Set G).toFinset by
      apply le_of_le_of_eq this; simp [K]; field
    rw [sub_mul, one_mul, sub_le_iff_le_add]
    calc
          (#(Set.toFinset H * S) : ℝ)
      _ = K * #(H : Set G).toFinset + (#(Set.toFinset H * S) - K * #(H : Set G).toFinset) := by ring
      _ = K * #(H : Set G).toFinset + ex (Set.toFinset H)                 := rfl
      _ ≤ K * #(H : Set G).toFinset + (1 - ε / 2) * #(Set.toFinset H * S) := by
        grw [calc₁]
        gcongr
        · linarith
        · simp only [Set.mem_toFinset, SetLike.mem_coe, H.one_mem, subset_mul_right]
-- 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) : ℝ)
case : (↑(#Z) : ℝ) = HMul.hMul (α := ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) (↑(#Z) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ)
⊢ (↑(#Z) : ℝ) ≤ 2 / ε - 1
have case₁ : HMul.hMul (α := ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) (↑(#Z) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ) =
  HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * Z)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ)
Tactic: case cardZ =>
    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
    gcongr
    -- Finally, to show `#(HS) ≤ (2 / ε - 1) * #H`, we multiply both sides by `1 - K = ε / 2` and
    -- show `#(HS) = K * #H + ex H ≤ K * #H + (1 - ε / 2) * #S ≤ K * #H + (1 - ε / 2) * #(HS)`,
    -- where we used `calc₁` again.
    rw [← mul_le_mul_iff_right₀ (show 0 < 1 - K by linarith [hK])]
    suffices (1 - K) * #(Set.toFinset H * S) ≤ (1 - ε / 2) * #(H : Set G).toFinset by
      apply le_of_le_of_eq this; simp [K]; field
    rw [sub_mul, one_mul, sub_le_iff_le_add]
    calc
          (#(Set.toFinset H * S) : ℝ)
      _ = K * #(H : Set G).toFinset + (#(Set.toFinset H * S) - K * #(H : Set G).toFinset) := by ring
      _ = K * #(H : Set G).toFinset + ex (Set.toFinset H)                 := rfl
      _ ≤ K * #(H : Set G).toFinset + (1 - ε / 2) * #(Set.toFinset H * S) := by
        grw [calc₁]
        gcongr
        · linarith
        · simp only [Set.mem_toFinset, SetLike.mem_coe, H.one_mem, subset_mul_right]
-- 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) : ℝ)
case : (↑(#Z) : ℝ) = HMul.hMul (α := ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) (↑(#Z) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ)
case₁ :
  HMul.hMul (α := ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) (↑(#Z) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * Z)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ)
⊢ (↑(#Z) : ℝ) ≤ 2 / ε - 1
have case₂ : HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * Z)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) =
  HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * S)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ)
Tactic: case cardZ =>
    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
    gcongr
    -- Finally, to show `#(HS) ≤ (2 / ε - 1) * #H`, we multiply both sides by `1 - K = ε / 2` and
    -- show `#(HS) = K * #H + ex H ≤ K * #H + (1 - ε / 2) * #S ≤ K * #H + (1 - ε / 2) * #(HS)`,
    -- where we used `calc₁` again.
    rw [← mul_le_mul_iff_right₀ (show 0 < 1 - K by linarith [hK])]
    suffices (1 - K) * #(Set.toFinset H * S) ≤ (1 - ε / 2) * #(H : Set G).toFinset by
      apply le_of_le_of_eq this; simp [K]; field
    rw [sub_mul, one_mul, sub_le_iff_le_add]
    calc
          (#(Set.toFinset H * S) : ℝ)
      _ = K * #(H : Set G).toFinset + (#(Set.toFinset H * S) - K * #(H : Set G).toFinset) := by ring
      _ = K * #(H : Set G).toFinset + ex (Set.toFinset H)                 := rfl
      _ ≤ K * #(H : Set G).toFinset + (1 - ε / 2) * #(Set.toFinset H * S) := by
        grw [calc₁]
        gcongr
        · linarith
        · simp only [Set.mem_toFinset, SetLike.mem_coe, H.one_mem, subset_mul_right]
-- 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) : ℝ)
case : (↑(#Z) : ℝ) = HMul.hMul (α := ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) (↑(#Z) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ)
case₁ :
  HMul.hMul (α := ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) (↑(#Z) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * Z)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ)
case₂ :
  HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * Z)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑(#((↑H : Set G).toFinset * S)) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ)
⊢ (↑(#Z) : ℝ) ≤ 2 / ε - 1
have case₃ : (2 / ε - 1) * (↑(#(↑H : Set G).toFinset) : ℝ) / (↑(#(↑H : Set G).toFinset) : ℝ) = 2 / ε - 1
Tactic: case cardZ =>
    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
    gcongr
    -- Finally, to show `#(HS) ≤ (2 / ε - 1) * #H`, we multiply both sides by `1 - K = ε / 2` and
    -- show `#(HS) = K * #H + ex H ≤ K * #H + (1 - ε / 2) * #S ≤ K * #H + (1 - ε / 2) * #(HS)`,
    -- where we used `calc₁` again.
    rw [← mul_le_mul_iff_right₀ (show 0 < 1 - K by linarith [hK])]
    suffices (1 - K) * #(Set.toFinset H * S) ≤ (1 - ε / 2) * #(H : Set G).toFinset by
      apply le_of_le_of_eq this; simp [K]; field
    rw [sub_mul, one_mul, sub_le_iff_le_add]
    calc
          (#(Set.toFinset H * S) : ℝ)
      _ = K * #(H : Set G).toFinset + (#(Set.toFinset H * S) - K * #(H : Set G).toFinset) := by ring
      _ = K * #(H : Set G).toFinset + ex (Set.toFinset H)                 := rfl
      _ ≤ K * #(H : Set G).toFinset + (1 - ε / 2) * #(Set.toFinset H * S) := by
        grw [calc₁]
        gcongr
        · linarith
        · simp only [Set.mem_toFinset, SetLike.mem_coe, H.one_mem, subset_mul_right]