awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : (↑A : Set ℕ) ⊆ Set.Iio n
hAε : ε * (↑n : ℝ) ≤ (↑(#A) : ℝ)
hA : ThreeAPFree (Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ)))
this_1 : (↑A : Set ℕ) = Set.image (α := Fin (2 * n).succ) Fin.val (Nat.cast '' (↑A : Set ℕ))
this_2 : IsAddFreimanIso (α := Fin (2 * n + 1)) 2 (Set.Iio (↑n : Fin (2 * n + 1))) (Set.Iio n) Fin.val
this : ThreeAPFree (↑(image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A) : Set (Fin (2 * n + 1)))
_ : ε / 3 * (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) = ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)
_₁ : ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) ≤ ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ))
_₂ : ε / 3 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + (↑n : ℝ)) = ε * (↑n : ℝ)
⊢ ε / 3 * (↑(Fintype.card (Fin (2 * n + 1))) : ℝ) ≤
    (↑(Finset.card (α := Fin (2 * n + 1)) (image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A)) : ℝ)
have _₃ : Eq (α := ℝ) (↑(#A) : ℝ) (↑(Finset.card (α := Fin (2 * n + 1)) (image (fun (x : ℕ) ↦ (↑x : Fin (2 * n + 1))) A)) : ℝ)
Tactic: calc
    _ = ε / 3 * (2 * n + 1) := by simp
    _ ≤ ε / 3 * (2 * n + n) := by gcongr; simp; unfold cornersTheoremBound at hG; lia
    _ = ε * n := by ring
    _ ≤ #A := hAε
    _ = _ := by
      rw [card_image_of_injOn]
      exact (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono <| hAn.trans <| by
        simp; lia
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (N : ℕ) ↦ (↑((rothNumberNat : (a : ℕ) → ℕ) N) : ℝ)) fun (N : ℕ) ↦ (↑N : ℝ)
have simp : ∀ ⦃c : ℝ⦄, 0 < c → ∃ (a : ℕ), ∀ b ≥ a, (↑((rothNumberNat : (a : ℕ) → ℕ) b) : ℝ) ≤ c * (↑b : ℝ)
Tactic: simp only [isLittleO_iff, eventually_atTop, RCLike.norm_natCast]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∃ (a : ℕ), ∀ b ≥ a, (↑((rothNumberNat : (a : ℕ) → ℕ) b) : ℝ) ≤ c * (↑b : ℝ)
have refine : ∀ (ε : ℝ) (hε : 0 < ε) (n : ℕ) (hn : n ≥ cornersTheoremBound (ε / 3)),
  (↑((rothNumberNat : (a : ℕ) → ℕ) n) : ℝ) ≤ ε * (↑n : ℝ)
Tactic: refine fun ε hε ↦ ⟨cornersTheoremBound (ε / 3), fun n hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
ε : ℝ
hε : 0 < ε
n : ℕ
hn : n ≥ cornersTheoremBound (ε / 3)
⊢ (↑((rothNumberNat : (a : ℕ) → ℕ) n) : ℝ) ≤ ε * (↑n : ℝ)
have obtain : ∀ (A : Finset ℕ) (hs₁ : A ⊆ range n) (hs₂ : #A = (rothNumberNat : (a : ℕ) → ℕ) n) (hs₃ : ThreeAPFree (↑A : Set ℕ)),
  (↑((rothNumberNat : (a : ℕ) → ℕ) n) : ℝ) ≤ ε * (↑n : ℝ)
Tactic: obtain ⟨A, hs₁, hs₂, hs₃⟩ := rothNumberNat_spec n
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Corner.Roth (goal)
Goal:
ε : ℝ
hε : 0 < ε
n : ℕ
hn : n ≥ cornersTheoremBound (ε / 3)
A : Finset ℕ
hs₁ : A ⊆ range n
hs₂ : #A = (rothNumberNat : (a : ℕ) → ℕ) n
hs₃ : ThreeAPFree (↑A : Set ℕ)
⊢ (↑((rothNumberNat : (a : ℕ) → ℕ) n) : ℝ) ≤ ε * (↑n : ℝ)
have rw : ¬ε * (↑n : ℝ) < (↑(#A) : ℝ)
Tactic: rw [← hs₂, ← not_lt]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CovBySMul (hypothesis)
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
hAB : CovBySMul M K A B
hBC : CovBySMul N L B C
⊢ CovBySMul N (K * L) A C
have this : 0 ≤ K
Tactic: have := hAB.nonneg
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CovBySMul (goal)
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
hAB : CovBySMul M K A B
hBC : CovBySMul N L B C
this : 0 ≤ K
⊢ CovBySMul N (K * L) A C
have obtain : ∀ (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B), CovBySMul N (K * L) A C
Tactic: obtain ⟨F₁, hF₁, hFAB⟩ := hAB
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CovBySMul (goal)
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
hBC : CovBySMul N L B C
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
⊢ CovBySMul N (K * L) A C
have obtain : ∀ (F₂ : Finset N) (hF₂ : (↑(#F₂) : ℝ) ≤ L) (hFBC : B ⊆ (↑F₂ : Set N) • C), CovBySMul N (K * L) A C
Tactic: obtain ⟨F₂, hF₂, hFBC⟩ := hBC
Cleared hypotheses: hBC
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CovBySMul (goal)
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
⊢ CovBySMul N (K * L) A C
have refine_1 : (↑(#(F₁ • F₂)) : ℝ) ≤ K * L
Tactic: refine ⟨F₁ • F₂, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CovBySMul (goal)
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
refine_1 : (↑(#(F₁ • F₂)) : ℝ) ≤ K * L
⊢ CovBySMul N (K * L) A C
have refine_2 : A ⊆ (↑(F₁ • F₂) : Set N) • C
Tactic: refine ⟨F₁ • F₂, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CovBySMul (goal)
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
⊢ HMul.hMul (α := ℝ) (↑(#F₁) : ℝ) (↑(#F₂) : ℝ) ≤ K * L
have c0 : LE.le (α := ℝ) 0 (↑(#F₂) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CovBySMul (goal)
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
⊢ (↑(#(F₁ • F₂)) : ℝ) ≤ K * L
have mod_cast : HMul.hMul (α := ℝ) (↑(#F₁) : ℝ) (↑(#F₂) : ℝ) ≤ K * L
Tactic: calc
      (#(F₁ • F₂) : ℝ) ≤ #F₁ * #F₂ := mod_cast Finset.card_smul_le
      _ ≤ K * L := by gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CovBySMul (goal)
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
⊢ A ⊆ (↑(F₁ • F₂) : Set N) • C
have A₁ : (↑F₁ : Set M) • B ⊆ (↑F₁ : Set M) • (↑F₂ : Set N) • C
Tactic: calc
      A ⊆ (F₁ : Set M) • B := hFAB
      _ ⊆ (F₁ : Set M) • (F₂ : Set N) • C := by gcongr
      _ = (↑(F₁ • F₂) : Set N) • C := by simp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CovBySMul (goal)
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
this : 0 ≤ K
F₁ : Finset M
hF₁ : (↑(#F₁) : ℝ) ≤ K
hFAB : A ⊆ (↑F₁ : Set M) • B
F₂ : Finset N
hF₂ : (↑(#F₂) : ℝ) ≤ L
hFBC : B ⊆ (↑F₂ : Set N) • C
A₁ : (↑F₁ : Set M) • B ⊆ (↑F₁ : Set M) • (↑F₂ : Set N) • C
⊢ A ⊆ (↑(F₁ • F₂) : Set N) • C
have A₂ : (↑F₁ : Set M) • (↑F₂ : Set N) • C = (↑(F₁ • F₂) : Set N) • C
Tactic: calc
      A ⊆ (F₁ : Set M) • B := hFAB
      _ ⊆ (F₁ : Set M) • (F₂ : Set N) • C := by gcongr
      _ = (↑(F₁ • F₂) : Set N) • C := by simp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CovBySMul (goal)
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
hAB : CovBySMul M K A B
hBC : CovBySMul N L B C
⊢ CovBySMul N (K * L) A C
have have : ∀ (this : 0 ≤ K), CovBySMul N (K * L) A C
Tactic: classical
  have := hAB.nonneg
  obtain ⟨F₁, hF₁, hFAB⟩ := hAB
  obtain ⟨F₂, hF₂, hFBC⟩ := hBC
  refine ⟨F₁ • F₂, ?_, ?_⟩
  · calc
      (#(F₁ • F₂) : ℝ) ≤ #F₁ * #F₂ := mod_cast Finset.card_smul_le
      _ ≤ K * L := by gcongr
  · calc
      A ⊆ (F₁ : Set M) • B := hFAB
      _ ⊆ (F₁ : Set M) • (F₂ : Set N) • C := by gcongr
      _ = (↑(F₁ • F₂) : Set N) • C := by simp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CovBySMul (goal)
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
hAB : CovBySMul M K A B
hBC : CovBySMul N L B C
have have₁ have₂ : ∀ (this : 0 ≤ K), CovBySMul N (K * L) A C
⊢ CovBySMul N (K * L) A C
have have₃ : ∀ (this : 0 ≤ K) (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B), CovBySMul N (K * L) A C
Tactic: classical
  have := hAB.nonneg
  obtain ⟨F₁, hF₁, hFAB⟩ := hAB
  obtain ⟨F₂, hF₂, hFBC⟩ := hBC
  refine ⟨F₁ • F₂, ?_, ?_⟩
  · calc
      (#(F₁ • F₂) : ℝ) ≤ #F₁ * #F₂ := mod_cast Finset.card_smul_le
      _ ≤ K * L := by gcongr
  · calc
      A ⊆ (F₁ : Set M) • B := hFAB
      _ ⊆ (F₁ : Set M) • (F₂ : Set N) • C := by gcongr
      _ = (↑(F₁ • F₂) : Set N) • C := by simp
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CovBySMul (goal)
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
hAB : CovBySMul M K A B
hBC : CovBySMul N L B C
have have₁ have₂ : ∀ (this : 0 ≤ K), CovBySMul N (K * L) A C
have₃ :
  ∀ (this : 0 ≤ K) (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B), CovBySMul N (K * L) A C
⊢ CovBySMul N (K * L) A C
have have₄ : ∀ (this : 0 ≤ K) (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B) (F₂ : Finset N)
  (hF₂ : (↑(#F₂) : ℝ) ≤ L) (hFBC : B ⊆ (↑F₂ : Set N) • C), CovBySMul N (K * L) A C
Tactic: classical
  have := hAB.nonneg
  obtain ⟨F₁, hF₁, hFAB⟩ := hAB
  obtain ⟨F₂, hF₂, hFBC⟩ := hBC
  refine ⟨F₁ • F₂, ?_, ?_⟩
  · calc
      (#(F₁ • F₂) : ℝ) ≤ #F₁ * #F₂ := mod_cast Finset.card_smul_le
      _ ≤ K * L := by gcongr
  · calc
      A ⊆ (F₁ : Set M) • B := hFAB
      _ ⊆ (F₁ : Set M) • (F₂ : Set N) • C := by gcongr
      _ = (↑(F₁ • F₂) : Set N) • C := by simp
Cleared hypotheses: hAB, hBC
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CovBySMul (goal)
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
hAB : CovBySMul M K A B
hBC : CovBySMul N L B C
have have₁ have₂ : ∀ (this : 0 ≤ K), CovBySMul N (K * L) A C
have₃ :
  ∀ (this : 0 ≤ K) (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B), CovBySMul N (K * L) A C
have₄ :
  ∀ (this : 0 ≤ K) (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B) (F₂ : Finset N)
    (hF₂ : (↑(#F₂) : ℝ) ≤ L) (hFBC : B ⊆ (↑F₂ : Set N) • C), CovBySMul N (K * L) A C
⊢ CovBySMul N (K * L) A C
have refine_1 : ∀ (this : 0 ≤ K) (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B) (F₂ : Finset N)
  (hF₂ : (↑(#F₂) : ℝ) ≤ L) (hFBC : B ⊆ (↑F₂ : Set N) • C), (↑(#(F₁ • F₂)) : ℝ) ≤ K * L
Tactic: classical
  have := hAB.nonneg
  obtain ⟨F₁, hF₁, hFAB⟩ := hAB
  obtain ⟨F₂, hF₂, hFBC⟩ := hBC
  refine ⟨F₁ • F₂, ?_, ?_⟩
  · calc
      (#(F₁ • F₂) : ℝ) ≤ #F₁ * #F₂ := mod_cast Finset.card_smul_le
      _ ≤ K * L := by gcongr
  · calc
      A ⊆ (F₁ : Set M) • B := hFAB
      _ ⊆ (F₁ : Set M) • (F₂ : Set N) • C := by gcongr
      _ = (↑(F₁ • F₂) : Set N) • C := by simp
Cleared hypotheses: hAB, hBC
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CovBySMul (goal)
Goal:
M : Type u_1
N : Type u_2
X : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M X
inst_3 : MulAction N X
K L : ℝ
A B C : Set X
inst_4 : SMul M N
inst_5 : IsScalarTower M N X
hAB : CovBySMul M K A B
hBC : CovBySMul N L B C
have have₁ have₂ : ∀ (this : 0 ≤ K), CovBySMul N (K * L) A C
have₃ :
  ∀ (this : 0 ≤ K) (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B), CovBySMul N (K * L) A C
have₄ :
  ∀ (this : 0 ≤ K) (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B) (F₂ : Finset N)
    (hF₂ : (↑(#F₂) : ℝ) ≤ L) (hFBC : B ⊆ (↑F₂ : Set N) • C), CovBySMul N (K * L) A C
refine_1 :
  ∀ (this : 0 ≤ K) (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B) (F₂ : Finset N)
    (hF₂ : (↑(#F₂) : ℝ) ≤ L) (hFBC : B ⊆ (↑F₂ : Set N) • C), (↑(#(F₁ • F₂)) : ℝ) ≤ K * L
⊢ CovBySMul N (K * L) A C
have refine_2 : ∀ (this : 0 ≤ K) (F₁ : Finset M) (hF₁ : (↑(#F₁) : ℝ) ≤ K) (hFAB : A ⊆ (↑F₁ : Set M) • B) (F₂ : Finset N)
  (hF₂ : (↑(#F₂) : ℝ) ≤ L) (hFBC : B ⊆ (↑F₂ : Set N) • C), A ⊆ (↑(F₁ • F₂) : Set N) • C
Tactic: classical
  have := hAB.nonneg
  obtain ⟨F₁, hF₁, hFAB⟩ := hAB
  obtain ⟨F₂, hF₂, hFBC⟩ := hBC
  refine ⟨F₁ • F₂, ?_, ?_⟩
  · calc
      (#(F₁ • F₂) : ℝ) ≤ #F₁ * #F₂ := mod_cast Finset.card_smul_le
      _ ≤ K * L := by gcongr
  · calc
      A ⊆ (F₁ : Set M) • B := hFAB
      _ ⊆ (F₁ : Set M) • (F₂ : Set N) • C := by gcongr
      _ = (↑(F₁ • F₂) : Set N) • C := by simp
Cleared hypotheses: hAB, hBC
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
⊢ ¬MulDissociated s ↔
    ∃ (t : Finset α) (u : Finset α),
      (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
have refine : (∃ (t : Finset α),
    (↑t : Set α) ⊆ s ∧ ∃ (u : Finset α), (↑u : Set α) ⊆ s ∧ t ≠ u ∧ Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)) →
  ∃ (t : Finset α) (u : Finset α),
    (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
Tactic: refine not_mulDissociated.trans
    ⟨?_, fun ⟨t, u, ht, hu, _, htune, htusum⟩ ↦ ⟨t, ht, u, hu, htune, htusum⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
t : Finset α
ht : (↑t : Set α) ⊆ s
u : Finset α
hu : (↑u : Set α) ⊆ s
htu : t ≠ u
h : Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)
⊢ ∃ (t : Finset α) (u : Finset α),
    (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
have refine_1 : (↑(t \ u) : Set α) ⊆ s
Tactic: refine ⟨t \ u, u \ t, ?_, ?_, disjoint_sdiff_sdiff, sdiff_ne_sdiff_iff.2 htu,
    Finset.prod_sdiff_eq_prod_sdiff_iff.2 h⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
t : Finset α
ht : (↑t : Set α) ⊆ s
u : Finset α
hu : (↑u : Set α) ⊆ s
htu : t ≠ u
h : Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)
refine_1 : (↑(t \ u) : Set α) ⊆ s
⊢ ∃ (t : Finset α) (u : Finset α),
    (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
have refine_2 : (↑(u \ t) : Set α) ⊆ s
Tactic: refine ⟨t \ u, u \ t, ?_, ?_, disjoint_sdiff_sdiff, sdiff_ne_sdiff_iff.2 htu,
    Finset.prod_sdiff_eq_prod_sdiff_iff.2 h⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
t : Finset α
ht : (↑t : Set α) ⊆ s
u : Finset α
hu : (↑u : Set α) ⊆ s
htu : t ≠ u
h : Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)
⊢ (↑(t \ u) : Set α) ⊆ s
have refine_1 : (↑t : Set α) \ (↑u : Set α) ⊆ s
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
t : Finset α
ht : (↑t : Set α) ⊆ s
u : Finset α
hu : (↑u : Set α) ⊆ s
htu : t ≠ u
h : Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)
⊢ (↑(u \ t) : Set α) ⊆ s
have refine_2 : (↑u : Set α) \ (↑t : Set α) ⊆ s
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
⊢ ¬MulDissociated s ↔
    ∃ (t : Finset α) (u : Finset α),
      (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
have refine : (∃ (t : Finset α),
    (↑t : Set α) ⊆ s ∧ ∃ (u : Finset α), (↑u : Set α) ⊆ s ∧ t ≠ u ∧ Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)) →
  ∃ (t : Finset α) (u : Finset α),
    (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
Tactic: classical
  refine not_mulDissociated.trans
    ⟨?_, fun ⟨t, u, ht, hu, _, htune, htusum⟩ ↦ ⟨t, ht, u, hu, htune, htusum⟩⟩
  rintro ⟨t, ht, u, hu, htu, h⟩
  refine ⟨t \ u, u \ t, ?_, ?_, disjoint_sdiff_sdiff, sdiff_ne_sdiff_iff.2 htu,
    Finset.prod_sdiff_eq_prod_sdiff_iff.2 h⟩ <;> push_cast <;> exact diff_subset.trans ‹_›
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
refine :
  (∃ (t : Finset α),
      (↑t : Set α) ⊆ s ∧ ∃ (u : Finset α), (↑u : Set α) ⊆ s ∧ t ≠ u ∧ Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)) →
    ∃ (t : Finset α) (u : Finset α),
      (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
⊢ ¬MulDissociated s ↔
    ∃ (t : Finset α) (u : Finset α),
      (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
have refine₁ : ∀ (t : Finset α) (ht : (↑t : Set α) ⊆ s) (u : Finset α) (hu : (↑u : Set α) ⊆ s) (htu : t ≠ u)
  (h : Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)),
  ∃ (t : Finset α) (u : Finset α),
    (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
Tactic: classical
  refine not_mulDissociated.trans
    ⟨?_, fun ⟨t, u, ht, hu, _, htune, htusum⟩ ↦ ⟨t, ht, u, hu, htune, htusum⟩⟩
  rintro ⟨t, ht, u, hu, htu, h⟩
  refine ⟨t \ u, u \ t, ?_, ?_, disjoint_sdiff_sdiff, sdiff_ne_sdiff_iff.2 htu,
    Finset.prod_sdiff_eq_prod_sdiff_iff.2 h⟩ <;> push_cast <;> exact diff_subset.trans ‹_›
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
a : α
ha : a ∈ s
b : α
⊢ Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (-1 : ℤ) ∨
    Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (0 : ℤ) ∨
      Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (1 : ℤ)
have inl : Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 a : ℤ) (-1 : ℤ) ∨
  Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 a : ℤ) (0 : ℤ) ∨
    Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 a : ℤ) (1 : ℤ)
Tactic: obtain rfl | hab := eq_or_ne a b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
a : α
ha : a ∈ s
b : α
inl :
  Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 a : ℤ) (-1 : ℤ) ∨
    Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 a : ℤ) (0 : ℤ) ∨
      Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 a : ℤ) (1 : ℤ)
⊢ Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (-1 : ℤ) ∨
    Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (0 : ℤ) ∨
      Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (1 : ℤ)
have inr : ∀ (hab : a ≠ b),
  Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (-1 : ℤ) ∨
    Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (0 : ℤ) ∨
      Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (1 : ℤ)
Tactic: obtain rfl | hab := eq_or_ne a b
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
⊢ HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1
have pos : a ∈ t →
  HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1
Tactic: by_cases a ∈ t
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
pos :
  a ∈ t →
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
        HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1
⊢ HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1
have neg : a ∉ t →
  HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1
Tactic: by_cases a ∈ t
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h : a ∈ t
⊢ HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1
have pos : a ∈ u →
  HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1
Tactic: by_cases a ∈ u