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

Premises used: HMul.hMul, HSub.hSub, sub_le_iff_le_add, HDiv.hDiv, Set.toFinset, Nat.cast, sub_mul, SetLike.coe, Finset.card, OfNat.ofNat, one_mul, rfl, mul_le_mul_iff_right₀