mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (-ι Q) m * (-ι Q) m = (algebraMap R (CliffordAlgebra Q)) (Q m)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ((involute.comp involute).toLinearMap ∘ₗ ι Q) x✝ = ((AlgHom.id R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ unop ((↑(opLinearEquiv R) ∘ₗ ι Q) m * (↑(opLinearEquiv R) ∘ₗ ι Q) m) =
    unop ((algebraMap R (CliffordAlgebra Q)ᵐᵒᵖ) (Q m))

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ((AlgHom.unop (reverseOp.comp (AlgHom.opComm reverseOp))).toLinearMap ∘ₗ ι Q) x✝ =
    ((AlgHom.unop (AlgHom.id R (CliffordAlgebra Q)ᵐᵒᵖ)).toLinearMap ∘ₗ ι Q) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ (((AlgHom.opComm reverseOp).comp reverseOp).toLinearMap ∘ₗ ι Q) x✝ =
    ((AlgHom.id R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q) x✝

Tactic:
simp

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

Goal state before:
pp: case algebraMap
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r✝ : R
⊢ reverse (involute ((algebraMap R (CliffordAlgebra Q)) r✝)) =
    involute (reverse ((algebraMap R (CliffordAlgebra Q)) r✝))

Tactic:
simp

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

Goal state before:
pp: case ι
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ reverse (involute ((ι Q) x✝)) = involute (reverse ((ι Q) x✝))

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ reverse (List.map ⇑(ι Q) []).prod = (List.map ⇑(ι Q) []).reverse.prod

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ involute (List.map ⇑(ι Q) []).prod = (-1) ^ [].length • (List.map ⇑(ι Q) []).prod

Tactic:
simp

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

Goal state before:
pp: case succ.inr
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
⊢ IsOrthoᵢ B (Fin.cons x (Subtype.val ∘ ⇑v'))

Tactic:
intro j

Goal state after:
case succ.inr
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j : Fin (d + 1)
⊢ ∀ ⦃j_1 : Fin (d + 1)⦄, j ≠ j_1 → Function.onFun (fun n m ↦ (B n) m = 0) (Fin.cons x (Subtype.val ∘ ⇑v')) j j_1
Module: Mathlib.LinearAlgebra.Alternating.Curry

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M [⋀^Fin n.succ.succ]→ₗ[R] N
m : M
x✝ : Fin n → M
⊢ Fin.cons m (Fin.cons m x✝) 0 = Fin.cons m (Fin.cons m x✝) 1

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R N
n : ℕ
g : M₂ →ₗ[R] M
f : M [⋀^Fin n.succ]→ₗ[R] N
m : M₂
v : Fin n → M₂
⊢ ((fun x ↦ g) 0) (Fin.cons m v 0) = Fin.cons (g m) (fun i ↦ ((fun x ↦ g) i) (v i)) 0

Tactic:
simp

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

Goal state before:
pp: case succ
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R N
n : ℕ
g : M₂ →ₗ[R] M
f : M [⋀^Fin n.succ]→ₗ[R] N
m : M₂
v : Fin n → M₂
i✝ : Fin n
⊢ ((fun x ↦ g) i✝.succ) (Fin.cons m v i✝.succ) = Fin.cons (g m) (fun i ↦ ((fun x ↦ g) i) (v i)) i✝.succ

Tactic:
simp

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₂
m : (i : Fin n.succ) → M i
⊢ f.curryLeft.uncurryLeft m = f m

Tactic:
simp

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₂
m : (i : Fin n.succ) → M i
⊢ f.curryRight.uncurryRight m = f m

Tactic:
simp

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

Goal state before:
pp: case x
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
x y : M p
⊢ (f (update m p (x + y) p)) (p.removeNth (update m p (x + y))) =
    (f (update m p x p)) (p.removeNth (update m p x)) + (f (update m p y p)) (p.removeNth (update m p y))

Tactic:
simp

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

Goal state before:
pp: case p
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
j✝ : Fin n
x y : M (p.succAbove j✝)
⊢ (f (update m (p.succAbove j✝) (x + y) p)) (p.removeNth (update m (p.succAbove j✝) (x + y))) =
    (f (update m (p.succAbove j✝) x p)) (p.removeNth (update m (p.succAbove j✝) x)) +
      (f (update m (p.succAbove j✝) y p)) (p.removeNth (update m (p.succAbove j✝) y))

Tactic:
simp

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

Goal state before:
pp: case x
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
x : R
y : M p
⊢ (f (update m p (x • y) p)) (p.removeNth (update m p (x • y))) = x • (f (update m p y p)) (p.removeNth (update m p y))

Tactic:
simp

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

Goal state before:
pp: case p
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
x : R
j✝ : Fin n
y : M (p.succAbove j✝)
⊢ (f (update m (p.succAbove j✝) (x • y) p)) (p.removeNth (update m (p.succAbove j✝) (x • y))) =
    x • (f (update m (p.succAbove j✝) y p)) (p.removeNth (update m (p.succAbove j✝) y))

Tactic:
simp

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:
simp

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:
simp

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₂
x✝¹ : M i
x✝ : (i_1 : Fin n) → M (i.succAbove i_1)
⊢ ((curryMid i (uncurryMid i f)) x✝¹) x✝ = (f x✝¹) x✝

Tactic:
simp

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:
simp

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₂
x✝ : (i : Fin n.succ) → M i
⊢ (LinearMap.uncurryMid i (curryMid i f)) x✝ = f x✝

Tactic:
simp

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

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

Tactic:
simp

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)
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ [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:
simp

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)
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ [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:
simp

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)
this : DecidableEq ι' := Classical.decEq ι'
⊢ { 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:
simp

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)
this : DecidableEq ι' := Classical.decEq ι'
⊢ { 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:
simp

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
⊢ ∀ (x : Fin n), f x ∈ ↑((fun f ↦ ofFinEmb n I f.toEmbedding) f)

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inl
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₂)
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
inst✝ : DecidableEq (ι ⊕ ι')
m✝ : (i : ι ⊕ ι') → N i
val✝ : ι
x✝ y✝ : N (Sum.inl val✝)
⊢ ((g fun i ↦ update m✝ (Sum.inl val✝) (x✝ + y✝) (Sum.inl i)) fun i' ↦
      update m✝ (Sum.inl val✝) (x✝ + y✝) (Sum.inr i')) =
    ((g fun i ↦ update m✝ (Sum.inl val✝) x✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inl val✝) x✝ (Sum.inr i')) +
      (g fun i ↦ update m✝ (Sum.inl val✝) y✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inl val✝) y✝ (Sum.inr i')

Tactic:
simp

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

Goal state before:
pp: case inr
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₂)
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
inst✝ : DecidableEq (ι ⊕ ι')
m✝ : (i : ι ⊕ ι') → N i
val✝ : ι'
x✝ y✝ : N (Sum.inr val✝)
⊢ ((g fun i ↦ update m✝ (Sum.inr val✝) (x✝ + y✝) (Sum.inl i)) fun i' ↦
      update m✝ (Sum.inr val✝) (x✝ + y✝) (Sum.inr i')) =
    ((g fun i ↦ update m✝ (Sum.inr val✝) x✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inr val✝) x✝ (Sum.inr i')) +
      (g fun i ↦ update m✝ (Sum.inr val✝) y✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inr val✝) y✝ (Sum.inr i')

Tactic:
simp

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

Goal state before:
pp: case inl
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₂)
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
inst✝ : DecidableEq (ι ⊕ ι')
m✝ : (i : ι ⊕ ι') → N i
val✝ : ι
c✝ : R
x✝ : N (Sum.inl val✝)
⊢ ((g fun i ↦ update m✝ (Sum.inl val✝) (c✝ • x✝) (Sum.inl i)) fun i' ↦
      update m✝ (Sum.inl val✝) (c✝ • x✝) (Sum.inr i')) =
    c✝ • (g fun i ↦ update m✝ (Sum.inl val✝) x✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inl val✝) x✝ (Sum.inr i')

Tactic:
simp

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

Goal state before:
pp: case inr
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₂)
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
inst✝ : DecidableEq (ι ⊕ ι')
m✝ : (i : ι ⊕ ι') → N i
val✝ : ι'
c✝ : R
x✝ : N (Sum.inr val✝)
⊢ ((g fun i ↦ update m✝ (Sum.inr val✝) (c✝ • x✝) (Sum.inl i)) fun i' ↦
      update m✝ (Sum.inr val✝) (c✝ • x✝) (Sum.inr i')) =
    c✝ • (g fun i ↦ update m✝ (Sum.inr val✝) x✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inr val✝) x✝ (Sum.inr i')

Tactic:
simp

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

Goal state before:
pp: case e_6.inl
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₂
x✝ : (i : ι ⊕ ι') → N i
val✝ : ι
⊢ Sum.rec (fun i ↦ x✝ (Sum.inl i)) (fun i' ↦ x✝ (Sum.inr i')) (Sum.inl val✝) = x✝ (Sum.inl val✝)

Tactic:
simp

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

Goal state before:
pp: case e_6.inr
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₂
x✝ : (i : ι ⊕ ι') → N i
val✝ : ι'
⊢ Sum.rec (fun i ↦ x✝ (Sum.inl i)) (fun i' ↦ x✝ (Sum.inr i')) (Sum.inr val✝) = x✝ (Sum.inr val✝)

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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
⊢ ∀ (a : M →ₗ[R] A),
    (∀ (m : M), a m * a m = 0) ↔
      ∀ (m : M), ((Equiv.refl (M →ₗ[R] A)) a) m * ((Equiv.refl (M →ₗ[R] A)) a) m = (algebraMap R A) (0 m)

Tactic:
simp

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
x✝ : M
⊢ 0 x✝ * 0 x✝ = 0

Tactic:
simp

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
m : M
x : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
x✝¹ : ℕ
x✝ : Fin x✝¹ → M
⊢ (((LinearMap.mk₂ R (fun m f i ↦ (f i.succ).curryLeft m) ⋯ ⋯ ⋯ ⋯) m)
        (((LinearMap.mk₂ R (fun m f i ↦ (f i.succ).curryLeft m) ⋯ ⋯ ⋯ ⋯) m) x) x✝¹)
      x✝ =
    ((0 m • x) x✝¹) x✝

Tactic:
simp

Goal state after: