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
hA : ∃ (A : Finset G), #S ≤ #A ∧ (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
K : ℝ := 1 - ε / 2
hK : K < 1
ex : (A : Finset G) → ℝ := expansion K S
κ : ℝ := connectivity K 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 obtain : ∀ (H : Subgroup G) (w : Fintype ↥H) (hH : IsAtom K S (↑H : Set G).toFinset),
  ∃ (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)
Tactic: obtain ⟨H, _, hH⟩ := exists_subgroup_isAtom hK hS
-- 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
hA : ∃ (A : Finset G), #S ≤ #A ∧ (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
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
⊢ ∃ (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 obtain : ∀ (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)),
  ∃ (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)
Tactic: obtain ⟨Z, hZS, hHZS, hZinj⟩ := exists_subset_mul_eq_mul_injOn H S
-- 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
hA : ∃ (A : Finset G), #S ≤ #A ∧ (↑(#(A * S)) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ)
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)
⊢ ∃ (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 obtain : ∀ (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)
Tactic: obtain ⟨A, hA₁, hA₂⟩ := 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
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) : ℝ)
⊢ (↑(#(A * S)) : ℝ) - K * (↑(#A) : ℝ) ≤ (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ)
have hcd : 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) : ℝ)
⊢ 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) : ℝ)
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) : ℝ)
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) : ℝ)
linarith : 1 - ε / 2 < 0 → 2 / 2 = 1
linarith₁ : 1 - ε / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 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) : ℝ)
⊢ (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) = (1 - ε / 2) * (↑(#S) : ℝ)
have linarith : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) < (1 - ε / 2) * (↑(#S) : ℝ) → 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) : ℝ)
linarith : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) < (1 - ε / 2) * (↑(#S) : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) = (1 - ε / 2) * (↑(#S) : ℝ)
have linarith₁ : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) < (1 - ε / 2) * (↑(#S) : ℝ) → 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) : ℝ)
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
⊢ (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) = (1 - ε / 2) * (↑(#S) : ℝ)
have linarith₃ : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) < (1 - ε / 2) * (↑(#S) : ℝ) → 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) : ℝ)
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
⊢ (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) = (1 - ε / 2) * (↑(#S) : ℝ)
have linarith₇ : (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) < (1 - ε / 2) * (↑(#S) : ℝ) → 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) : ℝ)
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
⊢ (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) = (1 - ε / 2) * (↑(#S) : ℝ)
have 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
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) : ℝ)
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
⊢ (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) = (1 - ε / 2) * (↑(#S) : ℝ)
have linarith₉ : (1 - ε / 2) * (↑(#S) : ℝ) < (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) → 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) : ℝ)
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
⊢ (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) = (1 - ε / 2) * (↑(#S) : ℝ)
have linarith₁₀ : (1 - ε / 2) * (↑(#S) : ℝ) < (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) → 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) : ℝ)
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
⊢ (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) = (1 - ε / 2) * (↑(#S) : ℝ)
have linarith₁₁ : (1 - ε / 2) * (↑(#S) : ℝ) < (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) → 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) : ℝ)
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
⊢ (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) = (1 - ε / 2) * (↑(#S) : ℝ)
have linarith₁₆ : (1 - ε / 2) * (↑(#S) : ℝ) < (2 - ε) * (↑(#S) : ℝ) - (1 - ε / 2) * (↑(#S) : ℝ) → GT.gt (α := ℝ) 2 0
Tactic: linarith