internlm/Lean-Github huggingface dataset:
Theorem: ConvexIndependent.subset_of_convexHull_eq_convexHull
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x✝ : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
x : E
hx : x ∈ s
hxextreme : x ∈ extremePoints 𝕜 ((convexHull 𝕜) fun x => x ∈ s.val)
⊢ x ∈ t
Tactic:
erw [h] at hxextreme
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x✝ : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
x : E
hx : x ∈ s
hxextreme : x ∈ extremePoints 𝕜 ((convexHull 𝕜) ↑t)
⊢ x ∈ t
Theorem: ConvexIndependent.subset_of_convexHull_eq_convexHull
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x✝ : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
x : E
hx : x ∈ s
hxextreme : x ∈ extremePoints 𝕜 ((convexHull 𝕜) ↑t)
⊢ x ∈ t
Tactic:
exact_mod_cast extremePoints_convexHull_subset hxextreme
Proof state after:
no goals
Theorem: hasSliceRankLE_zero
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
⊢ HasSliceRankLE 0 f ↔ f = 0
Tactic:
rw [hasSliceRankLE_iff]
Proof state after:
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
⊢ (0 = 0 ∧ f = 0 ∨ ∃ n f_1 i g h, HasSliceRankLE n f_1 ∧ 0 = n + 1 ∧ f = f_1 + fun x => g (x i) * h fun j x_1 => x j) ↔
    f = 0
Theorem: hasSliceRankLE_zero
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
⊢ (0 = 0 ∧ f = 0 ∨ ∃ n f_1 i g h, HasSliceRankLE n f_1 ∧ 0 = n + 1 ∧ f = f_1 + fun x => g (x i) * h fun j x_1 => x j) ↔
    f = 0
Tactic:
simp [@eq_comm _ 0]
Proof state after:
no goals
Theorem: hasSliceRankLE_succ
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
⊢ HasSliceRankLE (n + 1) f ↔ ∃ f' i g h, HasSliceRankLE n f' ∧ f = f' + fun x => g (x i) * h fun j x_1 => x j
Tactic:
rw [hasSliceRankLE_iff]
Proof state after:
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
⊢ (n + 1 = 0 ∧ f = 0 ∨
      ∃ n_1 f_1 i g h, HasSliceRankLE n_1 f_1 ∧ n + 1 = n_1 + 1 ∧ f = f_1 + fun x => g (x i) * h fun j x_1 => x j) ↔
    ∃ f' i g h, HasSliceRankLE n f' ∧ f = f' + fun x => g (x i) * h fun j x_1 => x j
Theorem: hasSliceRankLE_succ
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
⊢ (n + 1 = 0 ∧ f = 0 ∨
      ∃ n_1 f_1 i g h, HasSliceRankLE n_1 f_1 ∧ n + 1 = n_1 + 1 ∧ f = f_1 + fun x => g (x i) * h fun j x_1 => x j) ↔
    ∃ f' i g h, HasSliceRankLE n f' ∧ f = f' + fun x => g (x i) * h fun j x_1 => x j
Tactic:
sorry
Proof state after:
no goals
Theorem: hasSliceRankLE_one
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
⊢ HasSliceRankLE 1 f ↔ ∃ i g h, f = fun x => g (x i) * h fun j x_1 => x j
Tactic:
simp [hasSliceRankLE_succ]
Proof state after:
no goals
Theorem: hasSliceRankLE_iff_exists_sum
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
⊢ HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
Tactic:
induction' n with n ih generalizing f
Proof state after:
case zero
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ f : ((i : ι) → α i) → R
⊢ HasSliceRankLE 0 f ↔ ∃ i g h, f = ∑ k : Fin 0, fun x => g k (x (i k)) * h k fun j x_1 => x j

case succ
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
f : ((i : ι) → α i) → R
⊢ HasSliceRankLE (n + 1) f ↔ ∃ i g h, f = ∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j
Theorem: hasSliceRankLE_iff_exists_sum
Proof state before:
case succ
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
f : ((i : ι) → α i) → R
⊢ HasSliceRankLE (n + 1) f ↔ ∃ i g h, f = ∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j
Tactic:
simp_rw [hasSliceRankLE_succ, ih]
Proof state after:
case succ
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
f : ((i : ι) → α i) → R
⊢ (∃ f' i g h,
      (∃ i g h, f' = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) ∧
        f = f' + fun x => g (x i) * h fun j x_1 => x j) ↔
    ∃ i g h, f = ∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j
Theorem: hasSliceRankLE_iff_exists_sum
Proof state before:
case succ
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
f : ((i : ι) → α i) → R
⊢ (∃ f' i g h,
      (∃ i g h, f' = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) ∧
        f = f' + fun x => g (x i) * h fun j x_1 => x j) ↔
    ∃ i g h, f = ∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j
Tactic:
constructor
Proof state after:
case succ.mp
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
f : ((i : ι) → α i) → R
⊢ (∃ f' i g h,
      (∃ i g h, f' = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) ∧
        f = f' + fun x => g (x i) * h fun j x_1 => x j) →
    ∃ i g h, f = ∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j

case succ.mpr
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
f : ((i : ι) → α i) → R
⊢ (∃ i g h, f = ∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j) →
    ∃ f' i g h,
      (∃ i g h, f' = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) ∧
        f = f' + fun x => g (x i) * h fun j x_1 => x j
Theorem: hasSliceRankLE_iff_exists_sum
Proof state before:
case zero
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ f : ((i : ι) → α i) → R
⊢ HasSliceRankLE 0 f ↔ ∃ i g h, f = ∑ k : Fin 0, fun x => g k (x (i k)) * h k fun j x_1 => x j
Tactic:
simp
Proof state after:
no goals
Theorem: hasSliceRankLE_iff_exists_sum
Proof state before:
case succ.mp
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
f : ((i : ι) → α i) → R
⊢ (∃ f' i g h,
      (∃ i g h, f' = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) ∧
        f = f' + fun x => g (x i) * h fun j x_1 => x j) →
    ∃ i g h, f = ∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j
Tactic:
rintro ⟨f', iₙ, gₙ, hₙ, ⟨i, g, h, rfl⟩, rfl⟩
Proof state after:
case succ.mp.intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
iₙ : ι
gₙ : α iₙ → R
hₙ : ((j : ι) → j ≠ iₙ → α j) → R
i : Fin n → ι
g : (k : Fin n) → α (i k) → R
h : (k : Fin n) → ((j : ι) → j ≠ i k → α j) → R
⊢ ∃ i_1 g_1 h_1,
    ((∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) + fun x => gₙ (x iₙ) * hₙ fun j x_1 => x j) =
      ∑ k : Fin (n + 1), fun x => g_1 k (x (i_1 k)) * h_1 k fun j x_1 => x j
Theorem: hasSliceRankLE_iff_exists_sum
Proof state before:
case succ.mp.intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
iₙ : ι
gₙ : α iₙ → R
hₙ : ((j : ι) → j ≠ iₙ → α j) → R
i : Fin n → ι
g : (k : Fin n) → α (i k) → R
h : (k : Fin n) → ((j : ι) → j ≠ i k → α j) → R
⊢ ∃ i_1 g_1 h_1,
    ((∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) + fun x => gₙ (x iₙ) * hₙ fun j x_1 => x j) =
      ∑ k : Fin (n + 1), fun x => g_1 k (x (i_1 k)) * h_1 k fun j x_1 => x j
Tactic:
refine ⟨Fin.cons iₙ i, Fin.cons gₙ g, Fin.cons hₙ h, ?_⟩
Proof state after:
case succ.mp.intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
iₙ : ι
gₙ : α iₙ → R
hₙ : ((j : ι) → j ≠ iₙ → α j) → R
i : Fin n → ι
g : (k : Fin n) → α (i k) → R
h : (k : Fin n) → ((j : ι) → j ≠ i k → α j) → R
⊢ ((∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) + fun x => gₙ (x iₙ) * hₙ fun j x_1 => x j) =
    ∑ k : Fin (n + 1), fun x => Fin.cons gₙ g k (x (Fin.cons iₙ i k)) * Fin.cons hₙ h k fun j x_1 => x j
Theorem: hasSliceRankLE_iff_exists_sum
Proof state before:
case succ.mp.intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
iₙ : ι
gₙ : α iₙ → R
hₙ : ((j : ι) → j ≠ iₙ → α j) → R
i : Fin n → ι
g : (k : Fin n) → α (i k) → R
h : (k : Fin n) → ((j : ι) → j ≠ i k → α j) → R
⊢ ((∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) + fun x => gₙ (x iₙ) * hₙ fun j x_1 => x j) =
    ∑ k : Fin (n + 1), fun x => Fin.cons gₙ g k (x (Fin.cons iₙ i k)) * Fin.cons hₙ h k fun j x_1 => x j
Tactic:
ext x
Proof state after:
case succ.mp.intro.intro.intro.intro.intro.intro.intro.intro.h
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
iₙ : ι
gₙ : α iₙ → R
hₙ : ((j : ι) → j ≠ iₙ → α j) → R
i : Fin n → ι
g : (k : Fin n) → α (i k) → R
h : (k : Fin n) → ((j : ι) → j ≠ i k → α j) → R
x : (i : ι) → α i
⊢ ((∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) + fun x => gₙ (x iₙ) * hₙ fun j x_1 => x j) x =
    (∑ k : Fin (n + 1), fun x => Fin.cons gₙ g k (x (Fin.cons iₙ i k)) * Fin.cons hₙ h k fun j x_1 => x j) x
Theorem: hasSliceRankLE_iff_exists_sum
Proof state before:
case succ.mp.intro.intro.intro.intro.intro.intro.intro.intro.h
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
iₙ : ι
gₙ : α iₙ → R
hₙ : ((j : ι) → j ≠ iₙ → α j) → R
i : Fin n → ι
g : (k : Fin n) → α (i k) → R
h : (k : Fin n) → ((j : ι) → j ≠ i k → α j) → R
x : (i : ι) → α i
⊢ ((∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) + fun x => gₙ (x iₙ) * hₙ fun j x_1 => x j) x =
    (∑ k : Fin (n + 1), fun x => Fin.cons gₙ g k (x (Fin.cons iₙ i k)) * Fin.cons hₙ h k fun j x_1 => x j) x
Tactic:
simp only [ne_eq, Pi.add_apply, Finset.sum_apply, add_comm (_ * _), Fin.sum_univ_succ,
  Fin.cons_zero, Fin.cons_succ]
Proof state after:
case succ.mp.intro.intro.intro.intro.intro.intro.intro.intro.h
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
iₙ : ι
gₙ : α iₙ → R
hₙ : ((j : ι) → j ≠ iₙ → α j) → R
i : Fin n → ι
g : (k : Fin n) → α (i k) → R
h : (k : Fin n) → ((j : ι) → j ≠ i k → α j) → R
x : (i : ι) → α i
⊢ ((∑ c : Fin n, g c (x (i c)) * h c fun j x_1 => x j) + gₙ (x iₙ) * hₙ fun j x_1 => x j) =
    (∑ x_1 : Fin n, g x_1 (x (Fin.cons iₙ i x_1.succ)) * h x_1 fun j x_2 => x j) +
      gₙ (x (Fin.cons iₙ i 0)) * hₙ fun j x_1 => x j
Theorem: hasSliceRankLE_iff_exists_sum
Proof state before:
case succ.mp.intro.intro.intro.intro.intro.intro.intro.intro.h
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
iₙ : ι
gₙ : α iₙ → R
hₙ : ((j : ι) → j ≠ iₙ → α j) → R
i : Fin n → ι
g : (k : Fin n) → α (i k) → R
h : (k : Fin n) → ((j : ι) → j ≠ i k → α j) → R
x : (i : ι) → α i
⊢ ((∑ c : Fin n, g c (x (i c)) * h c fun j x_1 => x j) + gₙ (x iₙ) * hₙ fun j x_1 => x j) =
    (∑ x_1 : Fin n, g x_1 (x (Fin.cons iₙ i x_1.succ)) * h x_1 fun j x_2 => x j) +
      gₙ (x (Fin.cons iₙ i 0)) * hₙ fun j x_1 => x j
Tactic:
congr
Proof state after:
no goals
Theorem: hasSliceRankLE_iff_exists_sum
Proof state before:
case succ.mpr
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
f : ((i : ι) → α i) → R
⊢ (∃ i g h, f = ∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j) →
    ∃ f' i g h,
      (∃ i g h, f' = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) ∧
        f = f' + fun x => g (x i) * h fun j x_1 => x j
Tactic:
rintro ⟨i, g, h, rfl⟩
Proof state after:
case succ.mpr.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
i : Fin (n + 1) → ι
g : (k : Fin (n + 1)) → α (i k) → R
h : (k : Fin (n + 1)) → ((j : ι) → j ≠ i k → α j) → R
⊢ ∃ f' i_1 g_1 h_1,
    (∃ i g h, f' = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) ∧
      (∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j) =
        f' + fun x => g_1 (x i_1) * h_1 fun j x_1 => x j
Theorem: hasSliceRankLE_iff_exists_sum
Proof state before:
case succ.mpr.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
i : Fin (n + 1) → ι
g : (k : Fin (n + 1)) → α (i k) → R
h : (k : Fin (n + 1)) → ((j : ι) → j ≠ i k → α j) → R
⊢ ∃ f' i_1 g_1 h_1,
    (∃ i g h, f' = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j) ∧
      (∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j) =
        f' + fun x => g_1 (x i_1) * h_1 fun j x_1 => x j
Tactic:
refine ⟨_, i 0, g 0, h 0, ⟨Fin.tail i, Fin.tail g, Fin.tail h, rfl⟩, ?_⟩
Proof state after:
case succ.mpr.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
i : Fin (n + 1) → ι
g : (k : Fin (n + 1)) → α (i k) → R
h : (k : Fin (n + 1)) → ((j : ι) → j ≠ i k → α j) → R
⊢ (∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j) =
    (∑ k : Fin n, fun x => Fin.tail g k (x (Fin.tail i k)) * Fin.tail h k fun j x_1 => x j) + fun x =>
      g 0 (x (i 0)) * h 0 fun j x_1 => x j
Theorem: hasSliceRankLE_iff_exists_sum
Proof state before:
case succ.mpr.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
i : Fin (n + 1) → ι
g : (k : Fin (n + 1)) → α (i k) → R
h : (k : Fin (n + 1)) → ((j : ι) → j ≠ i k → α j) → R
⊢ (∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j) =
    (∑ k : Fin n, fun x => Fin.tail g k (x (Fin.tail i k)) * Fin.tail h k fun j x_1 => x j) + fun x =>
      g 0 (x (i 0)) * h 0 fun j x_1 => x j
Tactic:
ext x
Proof state after:
case succ.mpr.intro.intro.intro.h
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
i : Fin (n + 1) → ι
g : (k : Fin (n + 1)) → α (i k) → R
h : (k : Fin (n + 1)) → ((j : ι) → j ≠ i k → α j) → R
x : (i : ι) → α i
⊢ (∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j) x =
    ((∑ k : Fin n, fun x => Fin.tail g k (x (Fin.tail i k)) * Fin.tail h k fun j x_1 => x j) + fun x =>
        g 0 (x (i 0)) * h 0 fun j x_1 => x j)
      x
Theorem: hasSliceRankLE_iff_exists_sum
Proof state before:
case succ.mpr.intro.intro.intro.h
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
i : Fin (n + 1) → ι
g : (k : Fin (n + 1)) → α (i k) → R
h : (k : Fin (n + 1)) → ((j : ι) → j ≠ i k → α j) → R
x : (i : ι) → α i
⊢ (∑ k : Fin (n + 1), fun x => g k (x (i k)) * h k fun j x_1 => x j) x =
    ((∑ k : Fin n, fun x => Fin.tail g k (x (Fin.tail i k)) * Fin.tail h k fun j x_1 => x j) + fun x =>
        g 0 (x (i 0)) * h 0 fun j x_1 => x j)
      x
Tactic:
simp only [ne_eq, Pi.add_apply, Finset.sum_apply, add_comm (_ * _), Fin.sum_univ_succ,
  Fin.cons_zero, Fin.cons_succ]
Proof state after:
case succ.mpr.intro.intro.intro.h
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
i : Fin (n + 1) → ι
g : (k : Fin (n + 1)) → α (i k) → R
h : (k : Fin (n + 1)) → ((j : ι) → j ≠ i k → α j) → R
x : (i : ι) → α i
⊢ ((∑ i_1 : Fin n, g i_1.succ (x (i i_1.succ)) * h i_1.succ fun j x_1 => x j) + g 0 (x (i 0)) * h 0 fun j x_1 => x j) =
    (∑ c : Fin n, Fin.tail g c (x (Fin.tail i c)) * Fin.tail h c fun j x_1 => x j) +
      g 0 (x (i 0)) * h 0 fun j x_1 => x j
Theorem: hasSliceRankLE_iff_exists_sum
Proof state before:
case succ.mpr.intro.intro.intro.h
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m : ℕ
f₁ f₂ : ((i : ι) → α i) → R
n : ℕ
ih :
  ∀ {f : ((i : ι) → α i) → R},
    HasSliceRankLE n f ↔ ∃ i g h, f = ∑ k : Fin n, fun x => g k (x (i k)) * h k fun j x_1 => x j
i : Fin (n + 1) → ι
g : (k : Fin (n + 1)) → α (i k) → R
h : (k : Fin (n + 1)) → ((j : ι) → j ≠ i k → α j) → R
x : (i : ι) → α i
⊢ ((∑ i_1 : Fin n, g i_1.succ (x (i i_1.succ)) * h i_1.succ fun j x_1 => x j) + g 0 (x (i 0)) * h 0 fun j x_1 => x j) =
    (∑ c : Fin n, Fin.tail g c (x (Fin.tail i c)) * Fin.tail h c fun j x_1 => x j) +
      g 0 (x (i 0)) * h 0 fun j x_1 => x j
Tactic:
congr
Proof state after:
no goals
Theorem: HasSliceRankLE.add
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
h₁ : HasSliceRankLE m f₁
⊢ HasSliceRankLE (m + 0) (f₁ + 0)
Tactic:
simpa
Proof state after:
no goals
Theorem: HasSliceRankLE.add
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : DecidableEq ι
α : ι → Type u_3
inst✝ : Semiring R
m n : ℕ
f f₁ f₂ : ((i : ι) → α i) → R
h₁ : HasSliceRankLE m f₁
n✝ : ℕ
f✝ : ((i : ι) → (fun i => α i) i) → R
i✝ : ι
g : α i✝ → R
h : ((j : ι) → j ≠ i✝ → α j) → R
h₂ : HasSliceRankLE n✝ f✝
⊢ HasSliceRankLE (m + (n✝ + 1)) (f₁ + (f✝ + fun x => g (x i✝) * h fun j x_1 => x j))
Tactic:
simpa [add_assoc] using (h₁.add h₂).succ g h
Proof state after:
no goals
Theorem: hasSliceRankLE_card
Proof state before:
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Fintype (α i)
f : ((i : ι) → α i) → R
⊢ HasSliceRankLE (Fintype.card ((i : ι) → α i)) f
Tactic:
rw [hasSliceRankLE_iff_exists_sum]
Proof state after:
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Fintype (α i)
f : ((i : ι) → α i) → R
⊢ ∃ i g h, f = ∑ k : Fin (Fintype.card ((i : ι) → α i)), fun x => g k (x (i k)) * h k fun j x_1 => x j
Theorem: hasSliceRankLE_card
Proof state before:
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Fintype (α i)
f : ((i : ι) → α i) → R
⊢ ∃ i g h, f = ∑ k : Fin (Fintype.card ((i : ι) → α i)), fun x => g k (x (i k)) * h k fun j x_1 => x j
Tactic:
sorry
Proof state after:
no goals
Theorem: exists_hasSliceRankLE
Proof state before:
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), Finite (α i)
f : ((i : ι) → α i) → R
⊢ ∃ n, HasSliceRankLE n f
Tactic:
cases nonempty_fintype ι
Proof state after:
case intro
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), Finite (α i)
f : ((i : ι) → α i) → R
val✝ : Fintype ι
⊢ ∃ n, HasSliceRankLE n f
Theorem: exists_hasSliceRankLE
Proof state before:
case intro
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), Finite (α i)
f : ((i : ι) → α i) → R
val✝ : Fintype ι
⊢ ∃ n, HasSliceRankLE n f
Tactic:
have (i) := Fintype.ofFinite (α i)
Proof state after:
case intro
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), Finite (α i)
f : ((i : ι) → α i) → R
val✝ : Fintype ι
this : (i : ι) → Fintype (α i)
⊢ ∃ n, HasSliceRankLE n f
Theorem: exists_hasSliceRankLE
Proof state before:
case intro
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), Finite (α i)
f : ((i : ι) → α i) → R
val✝ : Fintype ι
this : (i : ι) → Fintype (α i)
⊢ ∃ n, HasSliceRankLE n f
Tactic:
exact ⟨_, hasSliceRankLE_card _⟩
Proof state after:
no goals