awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A⁻¹ * A
⊢ #(A⁻¹ * A) < 2 * #A
have this : 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) < HPow.hPow (α := ℚ) (β := ℕ) (↑(#A) : ℚ) 2
Tactic: have : ((1 / 2 : ℚ) * #A) * #(A⁻¹ * A) < (#A : ℚ) ^ 2 := by
    rw [← Nat.cast_pow, sq, ← card_product, card_eq_sum_card_fiberwise h₂, Nat.cast_sum]
    refine (sum_lt_sum_of_nonempty (by simp [h₀]) h₁).trans_eq' ?_
    simp only [sum_const, nsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A⁻¹ * A
this : 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) < HPow.hPow (α := ℚ) (β := ℕ) (↑(#A) : ℚ) 2
⊢ #(A⁻¹ * A) < 2 * #A
have rw : (↑(#(A⁻¹ * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
Tactic: rw [← Nat.cast_lt (α := ℚ), Nat.cast_mul, Nat.cast_two]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A⁻¹ * A
this : 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) < HPow.hPow (α := ℚ) (β := ℕ) (↑(#A) : ℚ) 2
⊢ (↑(#(A⁻¹ * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have nlinarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 1 = 1
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A⁻¹ * A
this : 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) < HPow.hPow (α := ℚ) (β := ℕ) (↑(#A) : ℚ) 2
nlinarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 1 = 1
⊢ (↑(#(A⁻¹ * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have nlinarith₁ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → 2 / 2 = 1
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A⁻¹ * A
this : 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) < HPow.hPow (α := ℚ) (β := ℕ) (↑(#A) : ℚ) 2
nlinarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 1 = 1
nlinarith₁ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → 2 / 2 = 1
⊢ (↑(#(A⁻¹ * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have nlinarith₂ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 2 = 2
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A⁻¹ * A
this : 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) < HPow.hPow (α := ℚ) (β := ℕ) (↑(#A) : ℚ) 2
nlinarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 1 = 1
nlinarith₁ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → 2 / 2 = 1
nlinarith₂ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 2 = 2
⊢ (↑(#(A⁻¹ * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have nlinarith₃ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 2 1 = 2
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A⁻¹ * A
this : 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) < HPow.hPow (α := ℚ) (β := ℕ) (↑(#A) : ℚ) 2
nlinarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 1 = 1
nlinarith₁ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → 2 / 2 = 1
nlinarith₂ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 2 = 2
nlinarith₃ nlinarith₄ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 2 1 = 2
⊢ (↑(#(A⁻¹ * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have nlinarith₅ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → 2 * HPow.hPow (α := ℚ) (β := ℕ) 1 2 = 2
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A⁻¹ * A
this : 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) < HPow.hPow (α := ℚ) (β := ℕ) (↑(#A) : ℚ) 2
nlinarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 1 = 1
nlinarith₁ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → 2 / 2 = 1
nlinarith₂ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 2 = 2
nlinarith₃ nlinarith₄ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 2 1 = 2
nlinarith₅ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → 2 * HPow.hPow (α := ℚ) (β := ℕ) 1 2 = 2
⊢ (↑(#(A⁻¹ * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have nlinarith₆ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → GT.gt (α := ℚ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A⁻¹ * A
this : 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) < HPow.hPow (α := ℚ) (β := ℕ) (↑(#A) : ℚ) 2
nlinarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 1 = 1
nlinarith₁ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → 2 / 2 = 1
nlinarith₂ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 2 = 2
nlinarith₃ nlinarith₄ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 2 1 = 2
nlinarith₅ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → 2 * HPow.hPow (α := ℚ) (β := ℕ) 1 2 = 2
nlinarith₆ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → GT.gt (α := ℚ) 2 0
nlinarith₇ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → 2 / 2 = 1
nlinarith₈ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 2 = 2
nlinarith₉ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 2 1 = 2
nlinarith₁₀ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → GT.gt (α := ℚ) 2 0
⊢ (↑(#(A⁻¹ * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have nlinarith₁₁ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) →
  HMul.hMul (α := ℚ) 1 1 * HMul.hMul (α := ℚ) 1 (↑(#A) : ℚ) * HMul.hMul (α := ℚ) 1 (↑(#(A⁻¹ * A)) : ℚ) -
        2 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℚ) 1 (↑(#A) : ℚ)) 2 +
      (0 -
        HSub.hSub (α := ℚ) 0 (↑(#A) : ℚ) *
          (HMul.hMul (α := ℚ) 1 2 * HMul.hMul (α := ℚ) 1 (↑(#A) : ℚ) - HMul.hMul (α := ℚ) 1 (↑(#(A⁻¹ * A)) : ℚ))) =
    0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
ha : a ∈ A
⊢ A ⊆ a •> (A⁻¹ * A)
have rw : A ⊆ a •> A⁻¹ * A
Tactic: rw [← smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
⊢ A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
have rw : (↑(A⁻¹ * A * (A⁻¹ * A)) : Set G) = (↑(A⁻¹ * A) : Set G)
Tactic: rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
rw : (↑(A⁻¹ * A * (A⁻¹ * A)) : Set G) = (↑(A⁻¹ * A) : Set G)
⊢ A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
have rw₁ : (↑(A⁻¹ * A) : Set G) * (↑(A⁻¹ * A) : Set G) = (↑(A⁻¹ * A) : Set G)
Tactic: rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
rw : (↑(A⁻¹ * A * (A⁻¹ * A)) : Set G) = (↑(A⁻¹ * A) : Set G)
rw₁ : (↑(A⁻¹ * A) : Set G) * (↑(A⁻¹ * A) : Set G) = (↑(A⁻¹ * A) : Set G)
⊢ A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
have rw₂ : (↑A⁻¹ : Set G) * (↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G)) = (↑A⁻¹ : Set G) * (↑A : Set G)
Tactic: rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
rw : (↑(A⁻¹ * A * (A⁻¹ * A)) : Set G) = (↑(A⁻¹ * A) : Set G)
rw₁ : (↑(A⁻¹ * A) : Set G) * (↑(A⁻¹ * A) : Set G) = (↑(A⁻¹ * A) : Set G)
rw₂ : (↑A⁻¹ : Set G) * (↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G)) = (↑A⁻¹ : Set G) * (↑A : Set G)
⊢ A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
have rw₃ : (↑(A.invMulSubgroup h) : Set G) * (↑(A.invMulSubgroup h) : Set G) = (↑(A.invMulSubgroup h) : Set G)
Tactic: rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
rw : (↑(A⁻¹ * A * (A⁻¹ * A)) : Set G) = (↑(A⁻¹ * A) : Set G)
rw₁ : (↑(A⁻¹ * A) : Set G) * (↑(A⁻¹ * A) : Set G) = (↑(A⁻¹ * A) : Set G)
rw₂ : (↑A⁻¹ : Set G) * (↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G)) = (↑A⁻¹ : Set G) * (↑A : Set G)
rw₃ : (↑(A.invMulSubgroup h) : Set G) * (↑(A.invMulSubgroup h) : Set G) = (↑(A.invMulSubgroup h) : Set G)
⊢ A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
have rw₄ : (↑(A.invMulSubgroup h) : Set G) = (↑(A.invMulSubgroup h) : Set G)
Tactic: rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
⊢ A * A ⊆ a •> ((A⁻¹ * A) <• a)
have h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
Tactic: have h₁ : (A⁻¹ * A) * (A⁻¹ * A) = A⁻¹ * A := by
    rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
have rw : a •> ((A⁻¹ * A) <• a) = (a •> (A⁻¹ * A) * (A⁻¹ * A)) <• a
Tactic: rw [mul_smul_comm, smul_mul_assoc, h₁, smul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
rw : a •> ((A⁻¹ * A) <• a) = (a •> (A⁻¹ * A) * (A⁻¹ * A)) <• a
⊢ a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
have rw₁ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A * (A⁻¹ * A)) <• a
Tactic: rw [mul_smul_comm, smul_mul_assoc, h₁, smul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
rw : a •> ((A⁻¹ * A) <• a) = (a •> (A⁻¹ * A) * (A⁻¹ * A)) <• a
rw₁ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A * (A⁻¹ * A)) <• a
⊢ a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
have rw₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) <• a
Tactic: rw [mul_smul_comm, smul_mul_assoc, h₁, smul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
rw : a •> ((A⁻¹ * A) <• a) = (a •> (A⁻¹ * A) * (A⁻¹ * A)) <• a
rw₁ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A * (A⁻¹ * A)) <• a
rw₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) <• a
⊢ a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
have rw₃ : a •> (A⁻¹ * A) <• a = a •> (A⁻¹ * A) <• a
Tactic: rw [mul_smul_comm, smul_mul_assoc, h₁, smul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ A * A ⊆ a •> ((A⁻¹ * A) <• a)
have h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
Tactic: have h₂ : a • op a • (A⁻¹ * A) = (a • (A⁻¹ * A)) * (op a • (A⁻¹ * A)) := by
    rw [mul_smul_comm, smul_mul_assoc, h₁, smul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
⊢ A * A ⊆ a •> ((A⁻¹ * A) <• a)
have rw : A * A ⊆ a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
⊢ A * A ⊆ a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
have refine : A ⊆ (A⁻¹ * A) <• a
Tactic: refine mul_subset_mul (A_subset_aH a ha) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
⊢ A ⊆ (A⁻¹ * A) <• a
have rw : A ⊆ A * A⁻¹ <• a
Tactic: rw [← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h), ← mul_smul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z : G
hz : z ∈ a •> ((A⁻¹ * A) <• a)
⊢ z ∈ A * A
have hz₁ : ∃ (a_1 : G), (∃ a ∈ A, ∃ z ∈ A, a⁻¹ * z = a_1) ∧ a * (a_1 * a) = z
Tactic: simp only [mem_smul_finset, smul_eq_mul_unop, unop_op, smul_eq_mul, mem_mul, mem_inv,
    exists_exists_and_eq_and] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z : G
hz : ∃ (a_1 : G), (∃ a ∈ A, ∃ z ∈ A, a⁻¹ * z = a_1) ∧ a * (a_1 * a) = z
⊢ z ∈ A * A
have obtain : ∀ (b : G) (hb : b ∈ A) (c : G) (hc : c ∈ A) (hz : a * (b⁻¹ * c * a) = z), z ∈ A * A
Tactic: obtain ⟨d, ⟨b, hb, c, hc, rfl⟩, hz⟩ := hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
⊢ A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
have rw : (↑(A⁻¹ * A * (A⁻¹ * A)) : Set G) = (↑(A⁻¹ * A) : Set G)
Tactic: rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
rw : (↑(A⁻¹ * A * (A⁻¹ * A)) : Set G) = (↑(A⁻¹ * A) : Set G)
⊢ A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
have rw₁ : (↑(A⁻¹ * A) : Set G) * (↑(A⁻¹ * A) : Set G) = (↑(A⁻¹ * A) : Set G)
Tactic: rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
rw : (↑(A⁻¹ * A * (A⁻¹ * A)) : Set G) = (↑(A⁻¹ * A) : Set G)
rw₁ : (↑(A⁻¹ * A) : Set G) * (↑(A⁻¹ * A) : Set G) = (↑(A⁻¹ * A) : Set G)
⊢ A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
have rw₂ : (↑A⁻¹ : Set G) * (↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G)) = (↑A⁻¹ : Set G) * (↑A : Set G)
Tactic: rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
rw : (↑(A⁻¹ * A * (A⁻¹ * A)) : Set G) = (↑(A⁻¹ * A) : Set G)
rw₁ : (↑(A⁻¹ * A) : Set G) * (↑(A⁻¹ * A) : Set G) = (↑(A⁻¹ * A) : Set G)
rw₂ : (↑A⁻¹ : Set G) * (↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G)) = (↑A⁻¹ : Set G) * (↑A : Set G)
⊢ A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
have rw₃ : (↑(A.invMulSubgroup h) : Set G) * (↑(A.invMulSubgroup h) : Set G) = (↑(A.invMulSubgroup h) : Set G)
Tactic: rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
rw : (↑(A⁻¹ * A * (A⁻¹ * A)) : Set G) = (↑(A⁻¹ * A) : Set G)
rw₁ : (↑(A⁻¹ * A) : Set G) * (↑(A⁻¹ * A) : Set G) = (↑(A⁻¹ * A) : Set G)
rw₂ : (↑A⁻¹ : Set G) * (↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G)) = (↑A⁻¹ : Set G) * (↑A : Set G)
rw₃ : (↑(A.invMulSubgroup h) : Set G) * (↑(A.invMulSubgroup h) : Set G) = (↑(A.invMulSubgroup h) : Set G)
⊢ A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
have rw₄ : (↑(A.invMulSubgroup h) : Set G) = (↑(A.invMulSubgroup h) : Set G)
Tactic: rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
⊢ z ∈ A * A
have this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
Tactic: have : (A⁻¹ * A) * (A⁻¹ * A) = A⁻¹ * A := by
    rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ l = A
have rw : (z * a⁻¹)⁻¹ •> A ⊆ A⁻¹ * A * (A⁻¹ * A)
Tactic: rw [inter_eq_left, ← this, subset_smul_finset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ (z * a⁻¹)⁻¹ •> A ⊆ A⁻¹ * A * (A⁻¹ * A)
have simp : (a * a⁻¹ * c⁻¹ * b * a⁻¹) •> A ⊆ A⁻¹ * A * A⁻¹ * A
Tactic: simp only [← hz, mul_inv_rev, inv_inv, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ (a * a⁻¹ * c⁻¹ * b * a⁻¹) •> A ⊆ A⁻¹ * A * A⁻¹ * A
have refine : a * a⁻¹ * c⁻¹ * b * a⁻¹ ∈ A⁻¹ * A * A⁻¹
Tactic: refine smul_finset_subset_mul ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ z ∈ A * A
have hl : l = A
Tactic: have hl : l = A := by
    rw [inter_eq_left, ← this, subset_smul_finset_iff]
    simp only [← hz, mul_inv_rev, inv_inv, ← mul_assoc]
    refine smul_finset_subset_mul ?_
    simp [mul_mem_mul, ha, hb, hc]