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
A : Finset G
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
⊢ A⁻¹ * (A⁻¹ * A) <• a ⊆ A⁻¹ * (A⁻¹ * A * A)
have grw : A⁻¹ * (A⁻¹ * A * A) ⊆ A⁻¹ * (A⁻¹ * A * A)
Tactic: grw [op_smul_finset_subset_mul (by simpa)]
-- 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
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
⊢ A⁻¹ * (A⁻¹ * A * A) = A⁻¹ * A
have rw : A⁻¹ * (A * A⁻¹ * A) = A * A⁻¹
Tactic: rw [← mul_inv_eq_inv_mul_of_doubling_lt_two <| weaken_doubling 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
⊢ A⁻¹ * (A * A⁻¹ * A) = A * A⁻¹
have simp_rw : (↑A⁻¹ : Set G) * ((↑A : Set G) * (↑A⁻¹ : Set G) * (↑A : Set G)) = (↑A : Set G) * (↑A⁻¹ : Set G)
Tactic: simp_rw [← coe_inj, coe_mul]
-- 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
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
⊢ (↑A⁻¹ : Set G) * ((↑A : Set G) * (↑A⁻¹ : Set G) * (↑A : Set G)) = (↑A : Set G) * (↑A⁻¹ : Set G)
have rw : (↑A⁻¹ : Set G) * ((↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G))) = (↑A : Set G) * (↑A⁻¹ : Set G)
Tactic: rw [mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ← mul_assoc,
          ← invMulSubgroup_eq_inv_mul _ h, ← invMulSubgroup_eq_mul_inv _ 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
rw : (↑A⁻¹ : Set G) * ((↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G))) = (↑A : Set G) * (↑A⁻¹ : Set G)
⊢ (↑A⁻¹ : Set G) * ((↑A : Set G) * (↑A⁻¹ : Set G) * (↑A : Set G)) = (↑A : Set G) * (↑A⁻¹ : Set G)
have rw₁ : (↑A⁻¹ : Set G) * ((↑A : Set G) * (↑(A.invMulSubgroup h) : Set G)) = (↑A : Set G) * (↑A⁻¹ : Set G)
Tactic: rw [mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ← mul_assoc,
          ← invMulSubgroup_eq_inv_mul _ h, ← invMulSubgroup_eq_mul_inv _ 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
rw : (↑A⁻¹ : Set G) * ((↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G))) = (↑A : Set G) * (↑A⁻¹ : Set G)
rw₁ : (↑A⁻¹ : Set G) * ((↑A : Set G) * (↑(A.invMulSubgroup h) : Set G)) = (↑A : Set G) * (↑A⁻¹ : Set G)
⊢ (↑A⁻¹ : Set G) * ((↑A : Set G) * (↑A⁻¹ : Set G) * (↑A : Set G)) = (↑A : Set G) * (↑A⁻¹ : Set G)
have rw₂ : (↑A⁻¹ : Set G) * (↑A : Set G) * (↑(A.invMulSubgroup h) : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)
Tactic: rw [mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ← mul_assoc,
          ← invMulSubgroup_eq_inv_mul _ h, ← invMulSubgroup_eq_mul_inv _ 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
rw : (↑A⁻¹ : Set G) * ((↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G))) = (↑A : Set G) * (↑A⁻¹ : Set G)
rw₁ : (↑A⁻¹ : Set G) * ((↑A : Set G) * (↑(A.invMulSubgroup h) : Set G)) = (↑A : Set G) * (↑A⁻¹ : Set G)
rw₂ : (↑A⁻¹ : Set G) * (↑A : Set G) * (↑(A.invMulSubgroup h) : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)
⊢ (↑A⁻¹ : Set G) * ((↑A : Set G) * (↑A⁻¹ : Set G) * (↑A : Set G)) = (↑A : Set G) * (↑A⁻¹ : Set G)
have rw₃ : (↑(A.invMulSubgroup h) : Set G) * (↑(A.invMulSubgroup h) : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)
Tactic: rw [mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ← mul_assoc,
          ← invMulSubgroup_eq_inv_mul _ h, ← invMulSubgroup_eq_mul_inv _ 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
rw : (↑A⁻¹ : Set G) * ((↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G))) = (↑A : Set G) * (↑A⁻¹ : Set G)
rw₁ : (↑A⁻¹ : Set G) * ((↑A : Set G) * (↑(A.invMulSubgroup h) : Set G)) = (↑A : Set G) * (↑A⁻¹ : Set G)
rw₂ : (↑A⁻¹ : Set G) * (↑A : Set G) * (↑(A.invMulSubgroup h) : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)
rw₃ : (↑(A.invMulSubgroup h) : Set G) * (↑(A.invMulSubgroup h) : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)
⊢ (↑A⁻¹ : Set G) * ((↑A : Set G) * (↑A⁻¹ : Set G) * (↑A : Set G)) = (↑A : Set G) * (↑A⁻¹ : Set G)
have rw₄ : (↑(A.invMulSubgroup h) : Set G) * (↑(A.invMulSubgroup h) : Set G) = (↑(A.invMulSubgroup h) : Set G)
Tactic: rw [mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ← mul_assoc,
          ← invMulSubgroup_eq_inv_mul _ h, ← invMulSubgroup_eq_mul_inv _ 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
rw : (↑A⁻¹ : Set G) * ((↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G))) = (↑A : Set G) * (↑A⁻¹ : Set G)
rw₁ : (↑A⁻¹ : Set G) * ((↑A : Set G) * (↑(A.invMulSubgroup h) : Set G)) = (↑A : Set G) * (↑A⁻¹ : Set G)
rw₂ : (↑A⁻¹ : Set G) * (↑A : Set G) * (↑(A.invMulSubgroup h) : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)
rw₃ : (↑(A.invMulSubgroup h) : Set G) * (↑(A.invMulSubgroup h) : 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⁻¹ : Set G) * ((↑A : Set G) * (↑A⁻¹ : Set G) * (↑A : Set G)) = (↑A : Set G) * (↑A⁻¹ : Set G)
have rw₅ : (↑(A.invMulSubgroup h) : Set G) = (↑(A.invMulSubgroup h) : Set G)
Tactic: rw [mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ← mul_assoc,
          ← invMulSubgroup_eq_inv_mul _ h, ← invMulSubgroup_eq_mul_inv _ 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
⊢ a⁻¹ •> ((A⁻¹ * A) <• a) ⊆ A⁻¹ * A
have a₁ : A⁻¹ * (A⁻¹ * A) <• a ⊆ A⁻¹ * (A⁻¹ * A * A)
Tactic: calc
      a⁻¹ •> ((A⁻¹ * A) <• a) ⊆ A⁻¹ * (A⁻¹ * A) <• a := smul_finset_subset_mul (by simpa)
      _ ⊆ A⁻¹ * ((A⁻¹ * A) * A) := by grw [op_smul_finset_subset_mul (by simpa)]
      _ = A⁻¹ * A := by
        rw [← mul_inv_eq_inv_mul_of_doubling_lt_two <| weaken_doubling h]
        simp_rw [← coe_inj, coe_mul]
        rw [mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ← mul_assoc,
          ← invMulSubgroup_eq_inv_mul _ h, ← invMulSubgroup_eq_mul_inv _ 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
a₁ : A⁻¹ * (A⁻¹ * A) <• a ⊆ A⁻¹ * (A⁻¹ * A * A)
⊢ a⁻¹ •> ((A⁻¹ * A) <• a) ⊆ A⁻¹ * A
have a₂ : A⁻¹ * (A⁻¹ * A * A) = A⁻¹ * A
Tactic: calc
      a⁻¹ •> ((A⁻¹ * A) <• a) ⊆ A⁻¹ * (A⁻¹ * A) <• a := smul_finset_subset_mul (by simpa)
      _ ⊆ A⁻¹ * ((A⁻¹ * A) * A) := by grw [op_smul_finset_subset_mul (by simpa)]
      _ = A⁻¹ * A := by
        rw [← mul_inv_eq_inv_mul_of_doubling_lt_two <| weaken_doubling h]
        simp_rw [← coe_inj, coe_mul]
        rw [mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ← mul_assoc,
          ← invMulSubgroup_eq_inv_mul _ h, ← invMulSubgroup_eq_mul_inv _ 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) : ℚ)
H : Subgroup G := A.invMulSubgroup h
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H),
    (↑(Fintype.card.{u_1} ↥H) : ℚ) < 3 / 2 * (↑(#A) : ℚ) ∧
      ∀ a ∈ A, (↑A : Set G) ⊆ a •> (↑H : Set G) ∧ a •> (↑H : Set G) = (↑H : Set G) <• a
have refine_1 : (↑(Fintype.card.{u_1} ↥H) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
Tactic: refine ⟨H, inferInstance, ?_, fun 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) : ℚ)
H : Subgroup G := A.invMulSubgroup h
refine_1 : (↑(Fintype.card.{u_1} ↥H) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H),
    (↑(Fintype.card.{u_1} ↥H) : ℚ) < 3 / 2 * (↑(#A) : ℚ) ∧
      ∀ a ∈ A, (↑A : Set G) ⊆ a •> (↑H : Set G) ∧ a •> (↑H : Set G) = (↑H : Set G) <• a
have refine_2 : ∀ (a : G) (ha : a ∈ A), (↑A : Set G) ⊆ a •> (↑H : Set G)
Tactic: refine ⟨H, inferInstance, ?_, fun 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) : ℚ)
H : Subgroup G := A.invMulSubgroup h
refine_1 : (↑(Fintype.card.{u_1} ↥H) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
refine_2 : ∀ (a : G) (ha : a ∈ A), (↑A : Set G) ⊆ a •> (↑H : Set G)
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H),
    (↑(Fintype.card.{u_1} ↥H) : ℚ) < 3 / 2 * (↑(#A) : ℚ) ∧
      ∀ a ∈ A, (↑A : Set G) ⊆ a •> (↑H : Set G) ∧ a •> (↑H : Set G) = (↑H : Set G) <• a
have refine_3 : ∀ (a : G) (ha : a ∈ A), a •> (↑H : Set G) = (↑H : Set G) <• a
Tactic: refine ⟨H, inferInstance, ?_, fun 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) : ℚ)
H : Subgroup G := A.invMulSubgroup h
⊢ (↑(Fintype.card.{u_1} ↥H) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
have refine_1 : (↑(Nat.card.{u_1} ↥(A⁻¹ * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
Tactic: simp only [invMulSubgroup, ← coe_mul, Subgroup.mem_mk, Submonoid.mem_mk, Subsemigroup.mem_mk,
      mem_coe, ← Nat.card_eq_fintype_card, 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) : ℚ)
H : Subgroup G := A.invMulSubgroup h
⊢ (↑(Nat.card.{u_1} ↥(A⁻¹ * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
have refine_1 : (↑(#(A⁻¹ * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
Tactic: rwa [Nat.card_eq_finsetCard, card_inv_mul_of_doubling_lt_three_halves 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) : ℚ)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ (↑A : Set G) ⊆ a •> (↑H : Set G)
have refine_2 : (↑A : Set G) ⊆ a •> ((↑A⁻¹ : Set G) * (↑A : Set G))
Tactic: rw [invMulSubgroup_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
c : Set G
x : G
hc : c ∈ orbit Gᵐᵒᵖ (↑H : Set G)
⊢ x ∈ c ↔ (↑H : Set G) <• x = c
have refine : ∀ (hx : x ∈ c), (↑H : Set G) <• x = c
Tactic: refine ⟨fun hx => ?_, fun hx =>
    by simp only [← hx, mem_rightCoset_iff, mul_inv_cancel, SetLike.mem_coe, one_mem]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
c : Set G
x : G
hc : c ∈ orbit Gᵐᵒᵖ (↑H : Set G)
hx : x ∈ c
⊢ (↑H : Set G) <• x = c
have obtain : ∀ (a : G) (hx : Membership.mem (γ := Set G) ((fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }) x),
  (↑H : Set G) <• x = (fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }
Tactic: obtain ⟨⟨a⟩, rfl⟩ := hc
Cleared hypotheses: c, hc, hx
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x a : G
hx : Membership.mem (γ := Set G) ((fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }) x
⊢ (↑H : Set G) <• x = (fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }
have change : (↑H : Set G) <• x = (↑H : Set G) <• a
Tactic: change _ = _ <• _
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x a : G
hx : Membership.mem (γ := Set G) ((fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }) x
⊢ (↑H : Set G) <• x = (↑H : Set G) <• a
have ha : x * a⁻¹ ∈ H
Tactic: rw [eq_comm, smul_eq_iff_eq_inv_smul, ← op_inv, op_smul_op_smul, rightCoset_mem_rightCoset]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x a : G
hx : Membership.mem (γ := Set G) ((fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }) x
⊢ x * a⁻¹ ∈ H
have ha : x <• a⁻¹ ∈ H
Tactic: rwa [← op_smul_eq_mul, op_inv, ← SetLike.mem_coe, ← Set.mem_smul_set_iff_inv_smul_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x a : G
hx : Membership.mem (γ := Set G) ((fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }) x
ha : x <• a⁻¹ ∈ H
⊢ x * a⁻¹ ∈ H
have ha₁ : (op a)⁻¹ •> x ∈ H
Tactic: rwa [← op_smul_eq_mul, op_inv, ← SetLike.mem_coe, ← Set.mem_smul_set_iff_inv_smul_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x a : G
hx : Membership.mem (γ := Set G) ((fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }) x
ha : x <• a⁻¹ ∈ H
ha₁ : (op a)⁻¹ •> x ∈ H
⊢ x * a⁻¹ ∈ H
have ha₂ : (op a)⁻¹ •> x ∈ (↑H : Set G)
Tactic: rwa [← op_smul_eq_mul, op_inv, ← SetLike.mem_coe, ← Set.mem_smul_set_iff_inv_smul_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x a : G
hx : Membership.mem (γ := Set G) ((fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }) x
ha : x <• a⁻¹ ∈ H
ha₁ : (op a)⁻¹ •> x ∈ H
ha₂ : (op a)⁻¹ •> x ∈ (↑H : Set G)
⊢ x * a⁻¹ ∈ H
have ha₃ : x ∈ (↑H : Set G) <• a
Tactic: rwa [← op_smul_eq_mul, op_inv, ← SetLike.mem_coe, ← Set.mem_smul_set_iff_inv_smul_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A : Finset 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)
have 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)
Tactic: obtain ⟨Z, hZA, hZinj, hHZA⟩ :=
    ((A : Set G).surjOn_image ((H : Set G) <• ·)).exists_subset_injOn_image_eq
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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 ⊆ 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)
have 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)
Tactic: lift Z to Finset G using A.finite_toSet.subset hZA
Cleared hypotheses: Z, hZA, hZinj, hHZA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
have refine : (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑A : Set G)
Tactic: refine ⟨Z, mod_cast hZA, ?_, hZinj⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
have rw : Fintype.card.{u_1} ↥H * #Z = #(↑H : Set G).toFinset * #Z
Tactic: rw [card_mul_iff.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ Fintype.card.{u_1} ↥H * #Z = #((↑H : Set G).toFinset * Z)
have rw₁ : Set.InjOn (β := G) (fun (p : G × G) ↦ p.1 * p.2) ((↑(↑H : Set G).toFinset : Set G) ×ˢ (↑Z : Set G))
Tactic: rw [card_mul_iff.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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₁, z₁) = (h₂, z₂)
have hh₃ : h₁ ∈ H
Tactic: simp only [Set.coe_toFinset, SetLike.mem_coe] at *
Cleared hypotheses: hh₁, hz₁, hh₂, hz₂
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ (h₁, z₁) = (h₂, z₂)
have hz₃ : z₁ ∈ Z
Tactic: simp only [Set.coe_toFinset, SetLike.mem_coe] at *
Cleared hypotheses: hh₁, hz₁, hh₂, hz₂
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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₁, z₁) = (h₂, z₂)
have hh₄ : h₂ ∈ H
Tactic: simp only [Set.coe_toFinset, SetLike.mem_coe] at *
Cleared hypotheses: hh₁, hz₁, hh₂, hz₂
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ (h₁, z₁) = (h₂, z₂)
have hz₄ : z₂ ∈ Z
Tactic: simp only [Set.coe_toFinset, SetLike.mem_coe] at *
Cleared hypotheses: hh₁, hz₁, hh₂, hz₂
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ (h₁, z₁) = (h₂, z₂)
have obtain : ∀ (h : h₁ * z₁ = h₂ * z₁) (hz₂ : z₁ ∈ 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₁
Cleared hypotheses: z₂, h, hz₂
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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) : ℝ)
⊢ ∃ (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)
have K_pos : 0 < K
Tactic: have K_pos : 0 < K := by positivity
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
have linarith : φ - K ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 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
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
⊢ 0 < φ - K
have linarith₂ : φ - K ≤ 0 → K - φ + (φ - K - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ ∃ (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)
have hKφ' : 0 < φ - K
Tactic: have hKφ' : 0 < φ - K := by linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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 - ψ
have linarith : K - ψ ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith [Real.goldenConj_neg]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ 0 < K - ψ
have linarith₂ : K - ψ ≤ 0 → -1 + (1 - K) + (K - ψ - 0) + (ψ - 0) = 0
Tactic: linarith [Real.goldenConj_neg]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ ∃ (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)
have hKψ' : 0 < K - ψ
Tactic: have hKψ' : 0 < K - ψ := by linarith [Real.goldenConj_neg]