mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
⊢ f.uncurryRight.curryRight = f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
⊢ f.curryRight.uncurryRight = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
ha' : ↑n ≤ {b}ᶜ.encard
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = ↑n
this : s.Finite
⊢ this.toFinset ∈ powersetCard α n

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
x y : M i
⊢ (f (update m i (x + y) p)) (p.removeNth (update m i (x + y))) =
    (f (update m i x p)) (p.removeNth (update m i x)) + (f (update m i y p)) (p.removeNth (update m i y))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
ha' : ↑n ≤ {b}ᶜ.encard
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = ↑n
this : s.Finite
⊢ a ∈ ⟨this.toFinset, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
ha' : ↑n ≤ {b}ᶜ.encard
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = ↑n
this : s.Finite
⊢ b ∉ ⟨this.toFinset, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
⊢ ∃ s, a ∈ s ∧ b ∉ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
s t : ↑(powersetCard α n)
⊢ s ≠ t ↔ ∃ a ∈ s, a ∉ t

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
x : R
y : M i
⊢ (f (update m i (x • y) p)) (p.removeNth (update m i (x • y))) = x • (f (update m i y p)) (p.removeNth (update m i y))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : ↑(powersetCard α n)
⊢ Finset.map f ↑s ∈ powersetCard β n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : ↑(powersetCard α n)
b : β
⊢ b ∈ map n f s ↔ b ∈ ⇑f '' ↑s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: V : Type u
K : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hK : Invertible 2
B : BilinForm K V
hB₂ : IsSymm B
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : ↑(powersetCard α n)
⊢ ↑(map n f s) = ⇑f '' ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
⊢ (fun s ↦ ⋯.choose) ((fun a ↦ ⟨{a}, ⋯⟩) a) = a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_8
inst✝ : Fintype ι
v : Basis ι R M
Q : QuadraticMap R M N
w : ι → R
⊢ (Q.basisRepr v) w = Q (∑ i, w i • v i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
s : ↑(powersetCard α 1)
⊢ (fun a ↦ ⟨{a}, ⋯⟩) ((fun s ↦ ⋯.choose) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_2
f : Fin n ↪ β
⊢ Finset.univ ∈ powersetCard (Fin n) n

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
p : Fin (n + 1)
f : MultilinearMap R M M₂
x y : M p
⊢ mk' (fun m ↦ f (p.insertNth (x + y) m)) ⋯ ⋯ =
    mk' (fun m ↦ f (p.insertNth x m)) ⋯ ⋯ + mk' (fun m ↦ f (p.insertNth y m)) ⋯ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: n : ℕ
β : Type u_2
f : Fin n ↪ β
b : β
⊢ b ∈ ofFinEmb n β f ↔ b ∈ range ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: n : ℕ
β : Type u_2
f : Fin n ↪ β
⊢ ↑(ofFinEmb n β f) = range ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: n : ℕ
β : Type u_2
f : Fin n ↪ β
⊢ ↑(ofFinEmb n β f) = Finset.map f Finset.univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: n : ℕ
β : Type u_2
s : Finset β
hs : s ∈ powersetCard β n
⊢ Fintype.card ?m.22 = #?m.25

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: n : ℕ
β : Type u_2
⊢ Surjective (ofFinEmb n β)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
p : Fin (n + 1)
f : MultilinearMap R M M₂
c : R
x : M p
⊢ mk' (fun m ↦ f (p.insertNth (c • x) m)) ⋯ ⋯ = (RingHom.id R) c • mk' (fun m ↦ f (p.insertNth x m)) ⋯ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : ↑(powersetCard α n)
⊢ (↑s)ᶜ ∈ powersetCard α m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
t : ↑(powersetCard α m)
⊢ (↑t)ᶜ ∈ powersetCard α n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : ↑(powersetCard α n)
⊢ (fun t ↦ ⟨(↑t)ᶜ, ⋯⟩) ((fun s ↦ ⟨(↑s)ᶜ, ⋯⟩) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
i : Fin (n + 1)
f : M i →ₗ[R] MultilinearMap R (fun j ↦ M (i.succAbove j)) M₂
⊢ curryMid i (uncurryMid i f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
t : ↑(powersetCard α m)
⊢ (fun s ↦ ⟨(↑s)ᶜ, ⋯⟩) ((fun t ↦ ⟨(↑t)ᶜ, ⋯⟩) t) = t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n m : ℕ
s : ↑(powersetCard α m)
t : ↑(powersetCard α n)
hst : Disjoint ↑s ↑t
⊢ (↑s).disjUnion (↑t) hst ∈ powersetCard α (m + n)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
i : Fin (n + 1)
f : MultilinearMap R M M₂
⊢ LinearMap.uncurryMid i (curryMid i f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Fintype α
⊢ powersetCard α n = ↑(Finset.powersetCard n Finset.univ)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Fintype α
⊢ Fintype ↑(powersetCard α n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Finite α
⊢ Finite ↑(powersetCard α n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
h : 0 < n
inst✝ : Infinite α
a : α
⊢ #{a} ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
h : 0 < n
inst✝ : Infinite α
a : α
s : Finset α
a_mem : {a} ⊆ s
s_card : #s = n
⊢ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
h : 0 < n
inst✝ : Infinite α
a : α
⊢ ∃ s ∈ powersetCard α n, a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: ι : Type u_8
inst✝⁴ : Fintype ι
R : Type u_9
M : Type u_10
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
⊢ basisRepr Q v = weightedSumSquares R fun i ↦ Q (v i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
u : (i : ι) → N (Sum.inl i)
⊢ ∀ [inst : DecidableEq ι'] (m : (i : ι') → N (Sum.inr i)) (i : ι') (x y : N (Sum.inr i)),
    (f fun t ↦ Sum.rec u (update m i (x + y)) t) =
      (f fun t ↦ Sum.rec u (update m i x) t) + f fun t ↦ Sum.rec u (update m i y) t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Infinite α
finite : Finite ↑(powersetCard α n)
this : ⋃₀ (SetLike.coe '' powersetCard α n) = univ
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
u : (i : ι) → N (Sum.inl i)
⊢ ∀ [inst : DecidableEq ι'] (m : (i : ι') → N (Sum.inr i)) (i : ι') (c : R) (x : N (Sum.inr i)),
    (f fun t ↦ Sum.rec u (update m i (c • x)) t) = c • f fun t ↦ Sum.rec u (update m i x) t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Infinite α
⊢ Infinite ↑(powersetCard α n)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁹ : CommSemiring R
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : Module R M'
inst✝³ : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝² : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝¹ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
inst✝ : DecidableEq ι
u : (i : ι) → N (Sum.inl i)
i : ι
x y : N (Sum.inl i)
x✝ : (i : ι') → N (Sum.inr i)
⊢ { toFun := fun v ↦ f fun t ↦ Sum.rec (update u i (x + y)) v t, map_update_add' := ⋯, map_update_smul' := ⋯ } x✝ =
    ({ toFun := fun v ↦ f fun t ↦ Sum.rec (update u i x) v t, map_update_add' := ⋯, map_update_smul' := ⋯ } +
        { toFun := fun v ↦ f fun t ↦ Sum.rec (update u i y) v t, map_update_add' := ⋯, map_update_smul' := ⋯ })
      x✝

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁹ : CommSemiring R
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : Module R M'
inst✝³ : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝² : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝¹ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
inst✝ : DecidableEq ι
u : (i : ι) → N (Sum.inl i)
i : ι
c : R
x : N (Sum.inl i)
x✝ : (i : ι') → N (Sum.inr i)
⊢ { toFun := fun v ↦ f fun t ↦ Sum.rec (update u i (c • x)) v t, map_update_add' := ⋯, map_update_smul' := ⋯ } x✝ =
    (c • { toFun := fun v ↦ f fun t ↦ Sum.rec (update u i x) v t, map_update_add' := ⋯, map_update_smul' := ⋯ }) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.PowersetCard

Goal state before:
pp: n : ℕ
I : Type u_1
inst✝ : LinearOrder I
f : Fin n ↪o I
⊢ (fun s ↦ (↑s).orderEmbOfFin ⋯) ((fun f ↦ ofFinEmb n I f.toEmbedding) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.PowersetCard

Goal state before:
pp: n : ℕ
I : Type u_1
inst✝ : LinearOrder I
s : ↑(powersetCard I n)
⊢ (fun f ↦ ofFinEmb n I f.toEmbedding) ((fun s ↦ (↑s).orderEmbOfFin ⋯) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.PowersetCard

Goal state before:
pp: n : ℕ
I : Type u_1
inst✝ : LinearOrder I
f : Fin n ↪o I
i : I
⊢ i ∈ ofFinEmbEquiv f ↔ i ∈ range ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.PowersetCard

Goal state before:
pp: n : ℕ
I : Type u_1
inst✝ : LinearOrder I
s : ↑(powersetCard I n)
i : I
⊢ i ∈ range ⇑(ofFinEmbEquiv.symm s) ↔ i ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ Nat.card ↑(powersetCard α n) = (Nat.card α).choose n

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
g : MultilinearMap R (fun i ↦ N (Sum.inl i)) (MultilinearMap R (fun i ↦ N (Sum.inr i)) M₂)
⊢ ∀ [inst : DecidableEq (ι ⊕ ι')] (m : (i : ι ⊕ ι') → N i) (i : ι ⊕ ι') (x y : N i),
    ((g fun i_1 ↦ update m i (x + y) (Sum.inl i_1)) fun i' ↦ update m i (x + y) (Sum.inr i')) =
      ((g fun i_1 ↦ update m i x (Sum.inl i_1)) fun i' ↦ update m i x (Sum.inr i')) +
        (g fun i_1 ↦ update m i y (Sum.inl i_1)) fun i' ↦ update m i y (Sum.inr i')

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
h1 : 0 < n
h2 : ↑n < ENat.card α
⊢ Nontrivial ↑(powersetCard α n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
h1 : 0 < n
h2 : n < Nat.card α
⊢ Nontrivial ↑(powersetCard α n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Finite α
⊢ powersetCard α n = ∅ ↔ Nat.card α < n

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
g : MultilinearMap R (fun i ↦ N (Sum.inl i)) (MultilinearMap R (fun i ↦ N (Sum.inr i)) M₂)
⊢ ∀ [inst : DecidableEq (ι ⊕ ι')] (m : (i : ι ⊕ ι') → N i) (i : ι ⊕ ι') (c : R) (x : N i),
    ((g fun i_1 ↦ update m i (c • x) (Sum.inl i_1)) fun i' ↦ update m i (c • x) (Sum.inr i')) =
      c • (g fun i_1 ↦ update m i x (Sum.inl i_1)) fun i' ↦ update m i x (Sum.inr i')

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Finite α
⊢ Nontrivial ↑(powersetCard α n) ↔ 0 < n ∧ n < Nat.card α

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
ι : Type uι
ι' : Type uι'
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
⊢ f.currySum.uncurrySum = f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
⊢ ∀ (x y : MultilinearMap R N M₂), (x + y).currySum = x.currySum + y.currySum

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
⊢ ∀ (m : R) (x : MultilinearMap R N M₂), (m • x).currySum = (RingHom.id R) m • x.currySum

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
x✝ : MultilinearMap R N M₂
⊢ x✝.currySum.uncurrySum = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
x : (n : ℕ) × ↑(powersetCard α n)
⊢ (fun x ↦ ⟨#x, ⟨x, ⋯⟩⟩) ((fun x ↦ ↑x.snd) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
⊢ ((curryFinFinset R M₂ M' hk hl).symm f) (s.piecewise (fun x_1 ↦ x) fun x ↦ y) = (f fun x_1 ↦ x) fun x ↦ y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') M₂
x y : M'
⊢ ((((curryFinFinset R M₂ M' hk hl) f) fun x_1 ↦ x) fun x ↦ y) = f (s.piecewise (fun x_1 ↦ x) fun x ↦ y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
⊢ motive x hx

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (CliffordAlgebra Q)) r) ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) (hy : y ∈ evenOdd Q 0),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
⊢ motive x hx

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
ι : ∀ (v : M), P ((CliffordAlgebra.ι Q) v) ⋯
add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) (hy : y ∈ evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1),
    P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
⊢ P x hx

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : ExteriorAlgebra R M →ₐ[R] A
m : M
⊢ g ((ι R) m) * g ((ι R) m) = 0

Tactic:
by

Goal state after: