awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A : Finset G
obtain :
  ∀ (Z : Set G) (hZA : Z ⊆ (↑A : Set G)) (hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) Z)
    (hHZA :
      Eq (α := Set (Set G)) ((fun (x : G) ↦ (↑H : Set G) <• x) '' Z)
        ((fun (x : G) ↦ (↑H : Set G) <• x) '' (↑A : Set G))),
    ∃ Z ⊆ A,
      (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑A : Set G) ∧
        Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
⊢ ∃ Z ⊆ A,
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑A : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)

Tactic:
obtain ⟨Z, hZA, hZinj, hHZA⟩ :=
    ((A : Set G).surjOn_image ((H : Set G) <• ·)).exists_subset_injOn_image_eq

Premises used: Set.surjOn_image, Set.SurjOn.exists_subset_injOn_image_eq, SetLike.coe, HSMul.hSMul, MulOpposite.op
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A : Finset G
Z : Set G
hZA : Z ⊆ (↑A : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) Z
hHZA :
  Eq (α := Set (Set G)) ((fun (x : G) ↦ (↑H : Set G) <• x) '' Z) ((fun (x : G) ↦ (↑H : Set G) <• x) '' (↑A : Set G))
⊢ Z.Finite

Tactic:
A.finite_toSet.subset hZA

Premises used: Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A : Finset G
Z : Set G
hZA : Z ⊆ (↑A : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) Z
hHZA :
  Eq (α := Set (Set G)) ((fun (x : G) ↦ (↑H : Set G) <• x) '' Z) ((fun (x : G) ↦ (↑H : Set G) <• x) '' (↑A : Set G))
lift :
  ∀ (Z : Finset G) (hZA : (↑Z : Set G) ⊆ (↑A : Set G))
    (hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G))
    (hHZA :
      Eq (α := Set (Set G)) ((fun (x : G) ↦ (↑H : Set G) <• x) '' (↑Z : Set G))
        ((fun (x : G) ↦ (↑H : Set G) <• x) '' (↑A : Set G))),
    ∃ Z ⊆ A,
      (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑A : Set G) ∧
        Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
⊢ ∃ Z ⊆ A,
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑A : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)

Tactic:
lift Z to Finset G using A.finite_toSet.subset hZA

Premises used: Finset, Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A Z : Finset G
hZA : (↑Z : Set G) ⊆ (↑A : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
hHZA :
  Eq (α := Set (Set G)) ((fun (x : G) ↦ (↑H : Set G) <• x) '' (↑Z : Set G))
    ((fun (x : G) ↦ (↑H : Set G) <• x) '' (↑A : Set G))
⊢ ∃ Z ⊆ A,
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑A : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)

Tactic:
⟨Z, mod_cast hZA, ?_, hZinj⟩

Premises used: SetLike.coe_subset_coe._simp_1, cast, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A Z : Finset G
hZA : (↑Z : Set G) ⊆ (↑A : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
hHZA :
  Eq (α := Set (Set G)) ((fun (x : G) ↦ (↑H : Set G) <• x) '' (↑Z : Set G))
    ((fun (x : G) ↦ (↑H : Set G) <• x) '' (↑A : Set G))
refine : (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑A : Set G)
⊢ ∃ Z ⊆ A,
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑A : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)

Tactic:
refine ⟨Z, mod_cast hZA, ?_, hZinj⟩
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A Z : Finset G
hZA : (↑Z : Set G) ⊆ (↑A : Set G)
hZinj : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
hHZA :
  Eq (α := Set (Set G)) ((fun (x : G) ↦ (↑H : Set G) <• x) '' (↑Z : Set G))
    ((fun (x : G) ↦ (↑H : Set G) <• x) '' (↑A : Set G))
⊢ (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑A : Set G)

Tactic:
simpa [-SetLike.mem_coe, Set.iUnion_op_smul_set] using congr(Set.sUnion $hHZA)

Premises used: Set.iUnion_op_smul_set, SetLike.mem_coe
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
rw : Fintype.card.{u_1} ↥H * #Z = #(↑H : Set G).toFinset * #Z
rw₁ : Set.InjOn (β := G) (fun (p : G × G) ↦ p.1 * p.2) ((↑(↑H : Set G).toFinset : Set G) ×ˢ (↑Z : Set G))
⊢ Fintype.card.{u_1} ↥H * #Z = #((↑H : Set G).toFinset * Z)

Tactic:
rw [card_mul_iff.2]

Premises used: Iff.mpr, Finset.card_mul_iff
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
⊢ Fintype.card.{u_1} ↥H * #Z = #(↑H : Set G).toFinset * #Z

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
h₁ z₁ : G
hh₁ : (h₁, z₁).1 ∈ (↑(↑H : Set G).toFinset : Set G)
hz₁ : (h₁, z₁).2 ∈ (↑Z : Set G)
h₂ z₂ : G
hh₂ : (h₂, z₂).1 ∈ (↑(↑H : Set G).toFinset : Set G)
hz₂ : (h₂, z₂).2 ∈ (↑Z : Set G)
h : Eq.{u_1 + 1} (α := G) ((fun (p : G × G) ↦ p.1 * p.2) (h₁, z₁)) ((fun (p : G × G) ↦ p.1 * p.2) (h₂, z₂))
⊢ h₁ ∈ H

Tactic:
simp only [Set.coe_toFinset, SetLike.mem_coe] at *

Premises used: SetLike.mem_coe, Set.coe_toFinset
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
h₁ z₁ : G
hh₁ : (h₁, z₁).1 ∈ (↑(↑H : Set G).toFinset : Set G)
hz₁ : (h₁, z₁).2 ∈ (↑Z : Set G)
h₂ z₂ : G
hh₂ : (h₂, z₂).1 ∈ (↑(↑H : Set G).toFinset : Set G)
hz₂ : (h₂, z₂).2 ∈ (↑Z : Set G)
h : Eq.{u_1 + 1} (α := G) ((fun (p : G × G) ↦ p.1 * p.2) (h₁, z₁)) ((fun (p : G × G) ↦ p.1 * p.2) (h₂, z₂))
hh₃ : h₁ ∈ H
⊢ z₁ ∈ Z

Tactic:
simp only [Set.coe_toFinset, SetLike.mem_coe] at *

Premises used: SetLike.mem_coe, Set.coe_toFinset
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
h₁ z₁ : G
hh₁ : (h₁, z₁).1 ∈ (↑(↑H : Set G).toFinset : Set G)
hz₁ : (h₁, z₁).2 ∈ (↑Z : Set G)
h₂ z₂ : G
hh₂ : (h₂, z₂).1 ∈ (↑(↑H : Set G).toFinset : Set G)
hz₂ : (h₂, z₂).2 ∈ (↑Z : Set G)
h : Eq.{u_1 + 1} (α := G) ((fun (p : G × G) ↦ p.1 * p.2) (h₁, z₁)) ((fun (p : G × G) ↦ p.1 * p.2) (h₂, z₂))
hh₃ : h₁ ∈ H
hz₃ : z₁ ∈ Z
⊢ h₂ ∈ H

Tactic:
simp only [Set.coe_toFinset, SetLike.mem_coe] at *

Premises used: SetLike.mem_coe, Set.coe_toFinset
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
h₁ z₁ : G
hh₁ : (h₁, z₁).1 ∈ (↑(↑H : Set G).toFinset : Set G)
hz₁ : (h₁, z₁).2 ∈ (↑Z : Set G)
h₂ z₂ : G
hh₂ : (h₂, z₂).1 ∈ (↑(↑H : Set G).toFinset : Set G)
hz₂ : (h₂, z₂).2 ∈ (↑Z : Set G)
h : Eq.{u_1 + 1} (α := G) ((fun (p : G × G) ↦ p.1 * p.2) (h₁, z₁)) ((fun (p : G × G) ↦ p.1 * p.2) (h₂, z₂))
hh₃ : h₁ ∈ H
hz₃ : z₁ ∈ Z
hh₄ : h₂ ∈ H
⊢ z₂ ∈ Z

Tactic:
simp only [Set.coe_toFinset, SetLike.mem_coe] at *

Premises used: SetLike.mem_coe, Set.coe_toFinset
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
h₁ z₁ h₂ z₂ : G
h : h₁ * z₁ = h₂ * z₂
hh₁ : h₁ ∈ H
hz₁ : z₁ ∈ Z
hh₂ : h₂ ∈ H
hz₂ : z₂ ∈ Z
⊢ z₂ * z₁⁻¹ ∈ H

Tactic:
simpa [eq_inv_mul_iff_mul_eq.2 h, mul_assoc] using mul_mem (inv_mem hh₂) hh₁

Premises used: Iff.mpr, mul_assoc, eq_inv_mul_iff_mul_eq, InvMemClass.inv_mem, MulMemClass.mul_mem
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
h₁ z₁ h₂ z₂ : G
h : h₁ * z₁ = h₂ * z₂
hh₁ : h₁ ∈ H
hz₁ : z₁ ∈ Z
hh₂ : h₂ ∈ H
hz₂ : z₂ ∈ Z
obtain : ∀ (h : h₁ * z₁ = h₂ * z₁) (hz₂ : z₁ ∈ Z), (h₁, z₁) = (h₂, z₁)
⊢ (h₁, z₁) = (h₂, z₂)

Tactic:
obtain rfl := hZ hz₁ hz₂ <| (rightCoset_eq_iff _).2 <| by
    simpa [eq_inv_mul_iff_mul_eq.2 h, mul_assoc] using mul_mem (inv_mem hh₂) hh₁

Premises used: Iff.mpr, rightCoset_eq_iff, rfl
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : Fintype ↥H
Z : Finset G
hZ : Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
h₁ z₁ h₂ : G
hh₁ : h₁ ∈ H
hz₁ : z₁ ∈ Z
hh₂ : h₂ ∈ H
h : h₁ * z₁ = h₂ * z₁
hz₂ : z₁ ∈ Z
⊢ (h₁, z₁) = (h₂, z₁)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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) : ℝ)
⊢ 0 < K

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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) : ℝ)
⊢ 0 < K

Tactic:
have K_pos : 0 < K := by positivity
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 : 0 < K
⊢ 0 < K

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 : 0 < K
⊢ 0 < K

Tactic:
have hK₀ : 0 < K := by positivity
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
linarith linarith₁ : φ - K ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₂ : φ - K ≤ 0 → K - φ + (φ - K - 0) = 0
⊢ 0 < φ - K

Tactic:
linarith
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ 0 < φ - K

Tactic:
have hKφ' : 0 < φ - K := by linarith
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
linarith linarith₁ : K - ψ ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₂ : K - ψ ≤ 0 → -1 + (1 - K) + (K - ψ - 0) + (ψ - 0) = 0
⊢ 0 < K - ψ

Tactic:
linarith [Real.goldenConj_neg]

Premises used: Real.goldenConj_neg
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ 0 < K - ψ

Tactic:
have hKψ' : 0 < K - ψ := by linarith [Real.goldenConj_neg]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 - ψ
linarith linarith₁ : 2 - K ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₂ : 2 - K ≤ 0 → K - φ + (2 - K - 0) + (φ - 2) = 0
⊢ 0 < 2 - K

Tactic:
linarith [Real.goldenRatio_lt_two]

Premises used: Real.goldenRatio_lt_two
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 - ψ
⊢ 0 < 2 - K

Tactic:
have hK₂' : 0 < 2 - K := by linarith [Real.goldenRatio_lt_two]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ 0 < K * (2 - K) / ((φ - K) * (K - ψ))

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ 0 < K * (2 - K) / ((φ - K) * (K - ψ))

Tactic:
have const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ)) := by positivity
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 - ψ))
inl :
  ∀ (hA₁ : (↑(#(HMul.hMul (α := Finset G) ∅⁻¹ ∅)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ))
    (hA₂ : (↑(#(HMul.hMul (α := Finset G) ∅ ∅⁻¹)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)),
    ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G),
      (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ (↑H : Set G) * (↑Z : Set G) = (↑∅ : Set G) * (↑∅⁻¹ : Set G)
inr :
  ∀ (A_nonempty : A.Nonempty),
    ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G),
      (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ (↑H : Set G) * (↑Z : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G),
    (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ (↑H : Set G) * (↑Z : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)

Tactic:
obtain rfl | A_nonempty := A.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
hK₁ : 1 < K
hKφ : K < φ
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
hA₁ : (↑(#(HMul.hMul (α := Finset G) ∅⁻¹ ∅)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)
hA₂ : (↑(#(HMul.hMul (α := Finset G) ∅ ∅⁻¹)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)
simp : 0 ≤ (2 - K) * K / ((φ - K) * (K - ψ))
⊢ (↑(card.{u_1} (α := G) ∅) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧
    (↑⊥ : Set G) * (↑∅ : Set G) = (↑∅ : Set G) * (↑∅⁻¹ : Set G)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
hK₁ : 1 < K
hKφ : K < φ
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
hA₁ : (↑(#(HMul.hMul (α := Finset G) ∅⁻¹ ∅)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)
hA₂ : (↑(#(HMul.hMul (α := Finset G) ∅ ∅⁻¹)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)
⊢ 0 ≤ (2 - K) * K / ((φ - K) * (K - ψ))

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
hK₁ : 1 < K
hKφ : K < φ
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
hA₁ : (↑(#(HMul.hMul (α := Finset G) ∅⁻¹ ∅)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)
hA₂ : (↑(#(HMul.hMul (α := Finset G) ∅ ∅⁻¹)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G),
    (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ (↑H : Set G) * (↑Z : Set G) = (↑∅ : Set G) * (↑∅⁻¹ : Set G)

Tactic:
exact ⟨⊥, inferInstance, ∅, by simp; positivity⟩
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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

Tactic:
simpa [S]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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

Tactic:
have S_nonempty : S.Nonempty := by simpa [S]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ (↑S : Set G).Nonempty

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ Finite.{u_1 + 1} ↥H

Tactic:
simpa [H] using stabilizer_finite (by simpa) S.finite_toSet

Premises used: MulAction.stabilizer_finite, Finset.finite_toSet
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ Finite.{u_1 + 1} ↥H

Tactic:
have : Finite H := by simpa [H] using stabilizer_finite (by simpa) S.finite_toSet
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
inr :
  ∀ (val : Fintype ↥H),
    ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G),
      (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ (↑H : Set G) * (↑Z : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G),
    (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ (↑H : Set G) * (↑Z : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)

Tactic:
cases nonempty_fintype H

Premises used: Membership.mem, Subtype, nonempty_fintype
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 : Set G) * (↑S : Set G) = (↑S : Set G)

Tactic:
simp [H, ← stabilizer_coe_finset]

Premises used: MulAction.stabilizer_coe_finset
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 : Set G) * (↑S : Set G) = (↑S : Set G)

Tactic:
have H_mul_S : (H : Set G) * S = S := by simp [H, ← stabilizer_coe_finset]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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)
inr :
  ∀ (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 : Subgroup G) (x : Fintype ↥H) (Z : Finset G),
      (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ (↑H : Set G) * (↑Z : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G),
    (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ (↑H : Set G) * (↑Z : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)

Tactic:
obtain ⟨Z, hZ⟩ := exists_subset_mul_eq_mul_injOn H S

Premises used: _private.0.Finset.exists_subset_mul_eq_mul_injOn
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 : Set G) * (↑Z : Set G) = (↑S : Set G)

Tactic:
simp [hZ.2.1, H_mul_S]

Premises used: And.right, And.left