awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
h : u ∈ t.powerset
simp_rw :
  Eq (α := ℂ)
    (𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
    (𝔼 i : G,
      HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)))
        ((HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) i : ℂ))
simp_rw₁ :
  Eq (α := ℂ)
    (𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
    (𝔼 i : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
        HMul.hMul (α := ℂ) (β := ℂ) ((∑ ψ ∈ u, ψ : (a : G) → ℂ) i : ℂ) ((∑ ψ ∈ t \ u, ψ : (a : G) → ℂ) (-i) : ℂ))
simp_rw₂ :
  Eq (α := ℂ)
    (𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
    (𝔼 i : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
        HMul.hMul (α := ℂ) (∏ i_1 ∈ u, (i_1 : (a : G) → ℂ) i) (∏ i_1 ∈ t \ u, (i_1 : (a : G) → ℂ) (-i)))
⊢ 𝔼 a : G,
      HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
        (∏ ψ ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)) =
    HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
      𝔼 a : G, (HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) a
have simp_rw₃ : Eq (α := ℂ)
  (𝔼 a : G,
    HMul.hMul (α := ℂ) (∏ ψ ∈ u, HMul.hMul (β := ℂ) (d ψ) ((ψ : (a : G) → ℂ) a : ℂ))
      (∏ ψ ∈ t \ u,
        HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ) : ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ψ : (a : G) → ℂ) a : ℂ) : ℂ)))
  (𝔼 i : G,
    HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ i_1 ∈ u, (i_1 : (a : G) → ℂ) i) *
      HMul.hMul (α := ℂ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) (∏ i_1 ∈ t \ u, (i_1 : (a : G) → ℂ) (-i)))
Tactic: simp_rw [mul_expect, AddChar.sub_apply, AddChar.sum_apply, mul_mul_mul_comm,
          ← prod_mul_distrib, AddChar.map_neg_eq_conj]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
h : u ∈ t.powerset
⊢ Eq (α := ℂ)
    (𝔼 i : G,
      HMul.hMul (α := ℂ) (∏ i_1 ∈ u, HMul.hMul (β := ℂ) (d i_1) ((i_1 : (a : G) → ℂ) i : ℂ))
        (∏ i_1 ∈ t \ u,
          HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d i_1) : ℂ)
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((i_1 : (a : G) → ℂ) i : ℂ) : ℂ)))
    0
have 𝔼 : HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
    𝔼 a : G, (HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) a =
  0
Tactic: calc
    𝔼 a, (∏ ψ ∈ u, d ψ * ψ a) * ∏ ψ ∈ t \ u, conj (d ψ) * conj (ψ a)
      = ((∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, conj (d ψ)) * 𝔼 a, (∑ ψ ∈ u, ψ - ∑ ψ ∈ t \ u, ψ) a := by
        simp_rw [mul_expect, AddChar.sub_apply, AddChar.sum_apply, mul_mul_mul_comm,
          ← prod_mul_distrib, AddChar.map_neg_eq_conj]
    _ = 0 := ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Randomisation (goal)
Goal:
G : Type u_1
inst : Fintype G
inst_1 : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated.{u_1} (α := AddChar G ℂ) {ψ : AddChar G ℂ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
h : u ∈ t.powerset
⊢ HMul.hMul (α := ℂ) (∏ ψ ∈ u, d ψ) (∏ ψ ∈ t \ u, (starRingEnd ℂ : (a : ℂ) → ℂ) (d ψ)) *
      𝔼 a : G, (HSub.hSub (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ) : (a : G) → ℂ) a =
    0
have rw : ((∀ a ∈ u, d a ≠ 0) ∧ ∀ a ∈ t \ u, Ne (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (d a) : ℂ) (0 : ℂ)) →
  Ne (α := AddChar G ℂ) (∑ ψ ∈ u, ψ) (∑ ψ ∈ t \ u, ψ)
Tactic: rw [mul_eq_zero, AddChar.expect_eq_zero_iff_ne_zero, sub_ne_zero, or_iff_not_imp_left, ← Ne,
    mul_ne_zero_iff, prod_ne_zero_iff, prod_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
⊢ ∃ F ⊆ A, (↑(#F) : ℝ) ≤ K ∧ A ⊆ F * (B / B)
have haveI : ∀ (this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)),
  ∃ F ⊆ A, (↑(#F) : ℝ) ≤ K ∧ A ⊆ F * (B / B)
Tactic: haveI : ∀ F, Decidable ((F : Set G).PairwiseDisjoint (· • B)) := fun F ↦ Classical.dec _
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
⊢ ∃ F ⊆ A, (↑(#F) : ℝ) ≤ K ∧ A ⊆ F * (B / B)
have obtain : ∀ (F : Finset G) (hFmax : Maximal (fun (x : Finset G) ↦ x ∈ C) F), ∃ F ⊆ A, (↑(#F) : ℝ) ≤ K ∧ A ⊆ F * (B / B)
Tactic: obtain ⟨F, hFmax⟩ := C.exists_maximal <| filter_nonempty_iff.2
    ⟨∅, empty_mem_powerset _, by simp [coe_empty]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (hypothesis)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ∈ C) F
⊢ ∃ F ⊆ A, (↑(#F) : ℝ) ≤ K ∧ A ⊆ F * (B / B)
have hFmax₁ : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
Tactic: simp only [C, mem_filter, mem_powerset] at hFmax
Cleared hypotheses: hFmax
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (hypothesis)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
⊢ ∃ F ⊆ A, (↑(#F) : ℝ) ≤ K ∧ A ⊆ F * (B / B)
have hFA : F ⊆ A
Tactic: obtain ⟨hFA, hF⟩ := hFmax.1
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (hypothesis)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
⊢ ∃ F ⊆ A, (↑(#F) : ℝ) ≤ K ∧ A ⊆ F * (B / B)
have hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
Tactic: obtain ⟨hFA, hF⟩ := hFmax.1
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
⊢ ∃ F ⊆ A, (↑(#F) : ℝ) ≤ K ∧ A ⊆ F * (B / B)
have refine_1 : HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) ≤ K * (↑(#B) : ℝ)
Tactic: refine ⟨F, hFA, le_of_mul_le_mul_right ?_ (by positivity : (0 : ℝ) < #B), fun a ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
refine_1 : HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) ≤ K * (↑(#B) : ℝ)
⊢ ∃ F ⊆ A, (↑(#F) : ℝ) ≤ K ∧ A ⊆ F * (B / B)
have refine_2 : ∀ (a : G) (ha : a ∈ A), a ∈ F * (B / B)
Tactic: refine ⟨F, hFA, le_of_mul_le_mul_right ?_ (by positivity : (0 : ℝ) < #B), fun a ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
⊢ HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) = (↑(#(F * B)) : ℝ)
have rw : HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) = (↑(#F * #B) : ℝ)
Tactic: rw [card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hF, Nat.cast_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
rw : HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) = (↑(#F * #B) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) = (↑(#(F * B)) : ℝ)
have rw₁ : HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) = HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ)
Tactic: rw [card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hF, Nat.cast_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
⊢ HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) ≤ K * (↑(#B) : ℝ)
have rw : HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) = (↑(#(F * B)) : ℝ)
Tactic: calc
      (#F * #B : ℝ) = #(F * B) := by
        rw [card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hF, Nat.cast_mul]
      _ ≤ #(A * B) := by gcongr
      _ ≤ K * #B := hK
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
rw : HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) = (↑(#(F * B)) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#F) : ℝ) (↑(#B) : ℝ) ≤ K * (↑(#B) : ℝ)
have rw₁ : LE.le (α := ℝ) (↑(#(F * B)) : ℝ) (↑(#(A * B)) : ℝ)
Tactic: calc
      (#F * #B : ℝ) = #(F * B) := by
        rw [card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hF, Nat.cast_mul]
      _ ≤ #(A * B) := by gcongr
      _ ≤ K * #B := hK
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
⊢ a ∈ F * (B / B)
have pos : ∀ (hau : a ∈ F), a ∈ F * (B / B)
Tactic: by_cases hau : a ∈ F
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
pos : ∀ (hau : a ∈ F), a ∈ F * (B / B)
⊢ a ∈ F * (B / B)
have neg : ∀ (hau : a ∉ F), a ∈ F * (B / B)
Tactic: by_cases hau : a ∈ F
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
⊢ a ∈ F * (B / B)
have pos : ∀ (H : ∀ b ∈ F, Disjoint (a • B) (b • B)), a ∈ F * (B / B)
Tactic: by_cases! H : ∀ b ∈ F, Disjoint (a • B) (b • B)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
pos : ∀ (H : ∀ b ∈ F, Disjoint (a • B) (b • B)), a ∈ F * (B / B)
⊢ a ∈ F * (B / B)
have neg : ∀ (H : ∃ b ∈ F, ¬Disjoint (a • B) (b • B)), a ∈ F * (B / B)
Tactic: by_cases! H : ∀ b ∈ F, Disjoint (a • B) (b • B)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ a ∈ F * (B / B)
have pos : insert a F ⊆ A ∧ (↑(insert a F) : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
Tactic: refine (hFmax.not_gt ?_ <| ssubset_insert hau).elim
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ insert a F ⊆ A ∧ (↑(insert a F) : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
have pos : (a ∈ A ∧ F ⊆ A) ∧ (insert a (↑F : Set G)).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
Tactic: rw [insert_subset_iff, coe_insert]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (hypothesis)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∃ b ∈ F, ¬Disjoint (a • B) (b • B)
⊢ a ∈ F * (B / B)
have H₁ : ∃ b ∈ F, ∃ (a_1 : G), a⁻¹ • a_1 ∈ B ∧ b⁻¹ • a_1 ∈ B
Tactic: simp_rw [not_disjoint_iff, ← inv_smul_mem_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
inst_1 : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : (↑(#(A * B)) : ℝ) ≤ K * (↑(#B) : ℝ)
this : (F : Set G) → Decidable (F.PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B}
F : Finset G
hFmax : Maximal (fun (x : Finset G) ↦ x ⊆ A ∧ (↑x : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B) F
hFA : F ⊆ A
hF : (↑F : Set G).PairwiseDisjoint (α := Finset G) fun (x : G) ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∃ b ∈ F, ∃ (a_1 : G), a⁻¹ • a_1 ∈ B ∧ b⁻¹ • a_1 ∈ B
⊢ a ∈ F * (B / B)
have neg : ∀ (b : G) (hb : b ∈ F) (c : G) (hc₁ : a⁻¹ • c ∈ B) (hc₂ : b⁻¹ • c ∈ B), a ∈ F * (B / B)
Tactic: obtain ⟨b, hb, c, hc₁, hc₂⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
A B : Set G
hA : A.Finite
hB : B.Finite
hB₀ : B.Nonempty
hK : (↑(Nat.card.{u_1} (↑(A * B) : Type u_1)) : ℝ) ≤ K * (↑(Nat.card.{u_1} (↑B : Type u_1)) : ℝ)
⊢ ∃ F ⊆ A, (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ A ⊆ F * (B / B) ∧ F.Finite
have lift : ∀ (A : Finset G)
  (hK : (↑(Nat.card.{u_1} (↑((↑A : Set G) * B) : Type u_1)) : ℝ) ≤ K * (↑(Nat.card.{u_1} (↑B : Type u_1)) : ℝ)),
  ∃ F ⊆ (↑A : Set G), (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * (B / B) ∧ F.Finite
Tactic: lift A to Finset G using hA
Cleared hypotheses: A, hA, hK
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
B : Set G
hB : B.Finite
hB₀ : B.Nonempty
A : Finset G
hK : (↑(Nat.card.{u_1} (↑((↑A : Set G) * B) : Type u_1)) : ℝ) ≤ K * (↑(Nat.card.{u_1} (↑B : Type u_1)) : ℝ)
⊢ ∃ F ⊆ (↑A : Set G), (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * (B / B) ∧ F.Finite
have lift : ∀ (B : Finset G) (hB₀ : (↑B : Set G).Nonempty)
  (hK :
    (↑(Nat.card.{u_1} (↑((↑A : Set G) * (↑B : Set G)) : Type u_1)) : ℝ) ≤
      K * (↑(Nat.card.{u_1} (↑(↑B : Set G) : Type u_1)) : ℝ)),
  ∃ F ⊆ (↑A : Set G),
    (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * ((↑B : Set G) / (↑B : Set G)) ∧ F.Finite
Tactic: lift B to Finset G using hB
Cleared hypotheses: B, hB, hB₀, hK
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B : Set G).Nonempty
hK :
  (↑(Nat.card.{u_1} (↑((↑A : Set G) * (↑B : Set G)) : Type u_1)) : ℝ) ≤
    K * (↑(Nat.card.{u_1} (↑(↑B : Set G) : Type u_1)) : ℝ)
⊢ ∃ F ⊆ (↑A : Set G),
    (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * ((↑B : Set G) / (↑B : Set G)) ∧ F.Finite
have obtain : ∀ (F : Finset G) (hFA : F ⊆ A) (hF : (↑F.card : ℝ) ≤ K) (hAF : A ⊆ F * (B / B)),
  ∃ F ⊆ (↑A : Set G),
    (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * ((↑B : Set G) / (↑B : Set G)) ∧ F.Finite
Tactic: obtain ⟨F, hFA, hF, hAF⟩ := Finset.ruzsa_covering_mul hB₀ (by simpa [← Finset.coe_mul] using hK)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B : Set G).Nonempty
hK :
  (↑(Nat.card.{u_1} (↑((↑A : Set G) * (↑B : Set G)) : Type u_1)) : ℝ) ≤
    K * (↑(Nat.card.{u_1} (↑(↑B : Set G) : Type u_1)) : ℝ)
F : Finset G
hFA : F ⊆ A
hF : (↑F.card : ℝ) ≤ K
hAF : A ⊆ F * (B / B)
⊢ (↑F : Set G) ⊆ (↑A : Set G) ∧
    (↑(Nat.card.{u_1} (↑(↑F : Set G) : Type u_1)) : ℝ) ≤ K ∧
      (↑A : Set G) ⊆ (↑F : Set G) * ((↑B : Set G) / (↑B : Set G)) ∧ (↑F : Set G).Finite
have norm_cast : F ≤ A ∧ (↑(Nat.card.{u_1} ↥F) : ℝ) ≤ K ∧ A ≤ F * (B / B) ∧ (↑F : Set G).Finite
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.RuzsaCovering (goal)
Goal:
G : Type u_1
inst : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B : Set G).Nonempty
hK :
  (↑(Nat.card.{u_1} (↑((↑A : Set G) * (↑B : Set G)) : Type u_1)) : ℝ) ≤
    K * (↑(Nat.card.{u_1} (↑(↑B : Set G) : Type u_1)) : ℝ)
⊢ ∃ F ⊆ (↑A : Set G),
    (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * ((↑B : Set G) / (↑B : Set G)) ∧ F.Finite
have obtain : ∀ (F : Finset G) (hFA : F ⊆ A) (hF : (↑F.card : ℝ) ≤ K) (hAF : A ⊆ F * (B / B)),
  ∃ F ⊆ (↑A : Set G),
    (↑(Nat.card.{u_1} (↑F : Type u_1)) : ℝ) ≤ K ∧ (↑A : Set G) ⊆ F * ((↑B : Set G) / (↑B : Set G)) ∧ F.Finite
Tactic: classical
  obtain ⟨F, hFA, hF, hAF⟩ := Finset.ruzsa_covering_mul hB₀ (by simpa [← Finset.coe_mul] using hK)
  exact ⟨F, by norm_cast; simp [*]⟩