mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case refine_3
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ ∑ i ∈ Finset.map { toFun := Subtype.val, inj' := ⋯ } {a_1 | ↑x a_1 ≠ 0}, a i = 0

Tactic:
·

Goal state after:
case refine_3
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ ∑ i ∈ Finset.map { toFun := Subtype.val, inj' := ⋯ } {a_1 | ↑x a_1 ≠ 0}, a i = 0
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case bit.false
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i ↦ 2 ^ i) ∘ fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i
⊢ (map (fun i ↦ 2 ^ i) (bit false n).bitIndices).sum = bit false n

pp: case bit.true
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i ↦ 2 ^ i) ∘ fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i
⊢ (map (fun i ↦ 2 ^ i) (bit true n).bitIndices).sum = bit true n

Tactic:
·

Goal state after:
case bit.false
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i ↦ 2 ^ i) ∘ fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i
⊢ (map (fun i ↦ 2 ^ i) (bit false n).bitIndices).sum = bit false n
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case refine_1
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ (map (fun x ↦ x - (a + 1)) L).SortedLT

pp: case refine_2
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ L = map (fun x ↦ x + a + 1) (map (fun x ↦ x - (a + 1)) L)

Tactic:
·

Goal state after:
case refine_1
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ (map (fun x ↦ x - (a + 1)) L).SortedLT
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case refine_1
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ #(ℬ.biUnion fun x ↦ x) = m * n

pp: case refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ↑(m * n) ∣ ∑ i ∈ ℬ.biUnion fun x ↦ x, a i

Tactic:
·

Goal state after:
case refine_1
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ #(ℬ.biUnion fun x ↦ x) = m * n
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ∀ i ∈ ℬ, ↑n ∣ ∑ i ∈ i, a i

pp: case refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ↑n ∣ ∑ x ∈ ℬ, ∑ i ∈ x, a i

pp: case refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ (↑ℬ).PairwiseDisjoint fun x ↦ x

Tactic:
·

Goal state after:
case refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ∀ i ∈ ℬ, ↑n ∣ ∑ i ∈ i, a i
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ↑n ∣ ∑ x ∈ ℬ, ∑ i ∈ x, a i

pp: case refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ (↑ℬ).PairwiseDisjoint fun x ↦ x

Tactic:
·

Goal state after:
case refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ↑n ∣ ∑ x ∈ ℬ, ∑ i ∈ x, a i
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ (↑ℬ).PairwiseDisjoint fun x ↦ x

Tactic:
·

Goal state after:
case refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ (↑ℬ).PairwiseDisjoint fun x ↦ x
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : toColex s ≤ toColex t
htu : toColex t ≤ toColex u
has : a ∈ s
hat : a ∉ t
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b
c : α
hct : c ∈ ofColex (toColex t)
hcs : c ∉ ofColex (toColex s)
hbc : b ≤ c
hcu : c ∈ u
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : toColex s ≤ toColex t
htu : toColex t ≤ toColex u
has : a ∈ s
hat : a ∉ t
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b
c : α
hct : c ∈ ofColex (toColex t)
hcs : c ∉ ofColex (toColex s)
hbc : b ≤ c
hcu : c ∉ u
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
s t u : Finset α
a : α
hst : toColex s ≤ toColex t
htu : toColex t ≤ toColex u
has : a ∈ s
hat : a ∉ t
s' : Finset α := {b ∈ s | b ∉ t ∧ a ≤ b}
b : α
hb : b ∈ s ∧ b ∉ t ∧ a ≤ b
hbmax : ∀ ⦃y : α⦄, y ∈ s → y ∉ t → a ≤ y → b ≤ y → y ≤ b
c : α
hct : c ∈ ofColex (toColex t)
hcs : c ∉ ofColex (toColex s)
hbc : b ≤ c
hcu : c ∈ u
⊢ ∃ b ∈ u, b ∉ s ∧ a ≤ b
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b

Tactic:
by_cases hat : a ∈ ofColex t

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∈ ofColex t
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b

case neg
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∉ ofColex t
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∈ ofColex t
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∉ ofColex t
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∈ ofColex t
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H1
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (m₁ m₂ n : Fin 3 → R),
    ![(m₁ + m₂) 1 * n 2 - (m₁ + m₂) 2 * n 1, (m₁ + m₂) 2 * n 0 - (m₁ + m₂) 0 * n 2,
        (m₁ + m₂) 0 * n 1 - (m₁ + m₂) 1 * n 0] =
      ![m₁ 1 * n 2 - m₁ 2 * n 1, m₁ 2 * n 0 - m₁ 0 * n 2, m₁ 0 * n 1 - m₁ 1 * n 0] +
        ![m₂ 1 * n 2 - m₂ 2 * n 1, m₂ 2 * n 0 - m₂ 0 * n 2, m₂ 0 * n 1 - m₂ 1 * n 0]

pp: case H2
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![(c • m) 1 * n 2 - (c • m) 2 * n 1, (c • m) 2 * n 0 - (c • m) 0 * n 2, (c • m) 0 * n 1 - (c • m) 1 * n 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]

pp: case H3
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (m n₁ n₂ : Fin 3 → R),
    ![m 1 * (n₁ + n₂) 2 - m 2 * (n₁ + n₂) 1, m 2 * (n₁ + n₂) 0 - m 0 * (n₁ + n₂) 2,
        m 0 * (n₁ + n₂) 1 - m 1 * (n₁ + n₂) 0] =
      ![m 1 * n₁ 2 - m 2 * n₁ 1, m 2 * n₁ 0 - m 0 * n₁ 2, m 0 * n₁ 1 - m 1 * n₁ 0] +
        ![m 1 * n₂ 2 - m 2 * n₂ 1, m 2 * n₂ 0 - m 0 * n₂ 2, m 0 * n₂ 1 - m 1 * n₂ 0]

pp: case H4
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]

Tactic:
·

Goal state after:
case H1
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (m₁ m₂ n : Fin 3 → R),
    ![(m₁ + m₂) 1 * n 2 - (m₁ + m₂) 2 * n 1, (m₁ + m₂) 2 * n 0 - (m₁ + m₂) 0 * n 2,
        (m₁ + m₂) 0 * n 1 - (m₁ + m₂) 1 * n 0] =
      ![m₁ 1 * n 2 - m₁ 2 * n 1, m₁ 2 * n 0 - m₁ 0 * n 2, m₁ 0 * n 1 - m₁ 1 * n 0] +
        ![m₂ 1 * n 2 - m₂ 2 * n 1, m₂ 2 * n 0 - m₂ 0 * n 2, m₂ 0 * n 1 - m₂ 1 * n 0]
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b✝ : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∈ ofColex t
b : α
hbu : b ∈ ofColex u
hbt : b ∉ ofColex t
hab : a ≤ b
hbs : b ∈ ofColex s
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b✝ : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∈ ofColex t
b : α
hbu : b ∈ ofColex u
hbt : b ∉ ofColex t
hab : a ≤ b
hbs : b ∉ ofColex s
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b✝ : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∈ ofColex t
b : α
hbu : b ∈ ofColex u
hbt : b ∉ ofColex t
hab : a ≤ b
hbs : b ∈ ofColex s
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H2
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![(c • m) 1 * n 2 - (c • m) 2 * n 1, (c • m) 2 * n 0 - (c • m) 0 * n 2, (c • m) 0 * n 1 - (c • m) 1 * n 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]

pp: case H3
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (m n₁ n₂ : Fin 3 → R),
    ![m 1 * (n₁ + n₂) 2 - m 2 * (n₁ + n₂) 1, m 2 * (n₁ + n₂) 0 - m 0 * (n₁ + n₂) 2,
        m 0 * (n₁ + n₂) 1 - m 1 * (n₁ + n₂) 0] =
      ![m 1 * n₁ 2 - m 2 * n₁ 1, m 2 * n₁ 0 - m 0 * n₁ 2, m 0 * n₁ 1 - m 1 * n₁ 0] +
        ![m 1 * n₂ 2 - m 2 * n₂ 1, m 2 * n₂ 0 - m 0 * n₂ 2, m 0 * n₂ 1 - m 1 * n₂ 0]

pp: case H4
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]

Tactic:
·

Goal state after:
case H2
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![(c • m) 1 * n 2 - (c • m) 2 * n 1, (c • m) 2 * n 0 - (c • m) 0 * n 2, (c • m) 0 * n 1 - (c • m) 1 * n 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H3
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (m n₁ n₂ : Fin 3 → R),
    ![m 1 * (n₁ + n₂) 2 - m 2 * (n₁ + n₂) 1, m 2 * (n₁ + n₂) 0 - m 0 * (n₁ + n₂) 2,
        m 0 * (n₁ + n₂) 1 - m 1 * (n₁ + n₂) 0] =
      ![m 1 * n₁ 2 - m 2 * n₁ 1, m 2 * n₁ 0 - m 0 * n₁ 2, m 0 * n₁ 1 - m 1 * n₁ 0] +
        ![m 1 * n₂ 2 - m 2 * n₂ 1, m 2 * n₂ 0 - m 0 * n₂ 2, m 0 * n₂ 1 - m 1 * n₂ 0]

pp: case H4
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]

Tactic:
·

Goal state after:
case H3
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (m n₁ n₂ : Fin 3 → R),
    ![m 1 * (n₁ + n₂) 2 - m 2 * (n₁ + n₂) 1, m 2 * (n₁ + n₂) 0 - m 0 * (n₁ + n₂) 2,
        m 0 * (n₁ + n₂) 1 - m 1 * (n₁ + n₂) 0] =
      ![m 1 * n₁ 2 - m 2 * n₁ 1, m 2 * n₁ 0 - m 0 * n₁ 2, m 0 * n₁ 1 - m 1 * n₁ 0] +
        ![m 1 * n₂ 2 - m 2 * n₂ 1, m 2 * n₂ 0 - m 0 * n₂ 2, m 0 * n₂ 1 - m 1 * n₂ 0]
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b✝ : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∈ ofColex t
b : α
hbu : b ∈ ofColex u
hbt : b ∉ ofColex t
hab : a ≤ b
hbs : b ∉ ofColex s
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b✝ : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∈ ofColex t
b : α
hbu : b ∈ ofColex u
hbt : b ∉ ofColex t
hab : a ≤ b
hbs : b ∉ ofColex s
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H4
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]

Tactic:
·

Goal state after:
case H4
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∉ ofColex t
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∉ ofColex t
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∈ t
⊢ b ≤ a

pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b ≤ a

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∈ t
⊢ b ≤ a
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b ≤ a

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b ≤ a
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∈ t
⊢ b < a

pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b < a

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∈ t
⊢ b < a
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b < a

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b < a