mathlib-initiative/mathlib-tactics huggingface dataset:
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

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

Goal state after:
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

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
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem.mem_mul.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ (GradedMonoid.mk (1 + ↑i) (GradedMonoid.GMul.mul ⟨(ι Q) w✝, ⋯⟩ ⟨x, ⋯⟩)).fst =
    (GradedMonoid.mk ↑i.succ ⟨(ι Q) w✝ * x, ⋯⟩).fst

pp: case mem.mem_mul.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ ↑(GradedMonoid.mk (1 + ↑i) (GradedMonoid.GMul.mul ⟨(ι Q) w✝, ⋯⟩ ⟨x, ⋯⟩)).snd =
    ↑(GradedMonoid.mk ↑i.succ ⟨(ι Q) w✝ * x, ⋯⟩).snd

Tactic:
<;>

Goal state after:
case mem.mem_mul.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ (GradedMonoid.mk (1 + ↑i) (GradedMonoid.GMul.mul ⟨(ι Q) w✝, ⋯⟩ ⟨x, ⋯⟩)).fst =
    (GradedMonoid.mk ↑i.succ ⟨(ι Q) w✝ * x, ⋯⟩).fst

case mem.mem_mul.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ ↑(GradedMonoid.mk (1 + ↑i) (GradedMonoid.GMul.mul ⟨(ι Q) w✝, ⋯⟩ ⟨x, ⋯⟩)).snd =
    ↑(GradedMonoid.mk ↑i.succ ⟨(ι Q) w✝ * x, ⋯⟩).snd
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: case zero
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₂
f : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
x y : M 0
⊢ (f (update m 0 (x + y) 0)) (tail (update m 0 (x + y))) =
    (f (update m 0 x 0)) (tail (update m 0 x)) + (f (update m 0 y 0)) (tail (update m 0 y))

pp: case succ
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₂
f : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
i✝ : Fin n
x y : M i✝.succ
⊢ (f (update m i✝.succ (x + y) 0)) (tail (update m i✝.succ (x + y))) =
    (f (update m i✝.succ x 0)) (tail (update m i✝.succ x)) + (f (update m i✝.succ y 0)) (tail (update m i✝.succ y))

Tactic:
<;>

Goal state after:
case zero
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₂
f : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
x y : M 0
⊢ (f (update m 0 (x + y) 0)) (tail (update m 0 (x + y))) =
    (f (update m 0 x 0)) (tail (update m 0 x)) + (f (update m 0 y 0)) (tail (update m 0 y))

case succ
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₂
f : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
i✝ : Fin n
x y : M i✝.succ
⊢ (f (update m i✝.succ (x + y) 0)) (tail (update m i✝.succ (x + y))) =
    (f (update m i✝.succ x 0)) (tail (update m i✝.succ x)) + (f (update m i✝.succ y 0)) (tail (update m i✝.succ y))
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: case zero
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₂
f : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
c : R
x : M 0
⊢ (f (update m 0 (c • x) 0)) (tail (update m 0 (c • x))) = c • (f (update m 0 x 0)) (tail (update m 0 x))

pp: case succ
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₂
f : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
c : R
i✝ : Fin n
x : M i✝.succ
⊢ (f (update m i✝.succ (c • x) 0)) (tail (update m i✝.succ (c • x))) =
    c • (f (update m i✝.succ x 0)) (tail (update m i✝.succ x))

Tactic:
<;>

Goal state after:
case zero
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₂
f : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
c : R
x : M 0
⊢ (f (update m 0 (c • x) 0)) (tail (update m 0 (c • x))) = c • (f (update m 0 x 0)) (tail (update m 0 x))

case succ
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₂
f : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
c : R
i✝ : Fin n
x : M i✝.succ
⊢ (f (update m i✝.succ (c • x) 0)) (tail (update m i✝.succ (c • x))) =
    c • (f (update m i✝.succ x 0)) (tail (update m i✝.succ x))
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: case last
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₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n.succ) → M i
x y : M (last n)
⊢ (f (init (update m (last n) (x + y)))) (update m (last n) (x + y) (last n)) =
    (f (init (update m (last n) x))) (update m (last n) x (last n)) +
      (f (init (update m (last n) y))) (update m (last n) y (last n))

pp: case cast
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₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n.succ) → M i
i✝ : Fin n
x y : M i✝.castSucc
⊢ (f (init (update m i✝.castSucc (x + y)))) (update m i✝.castSucc (x + y) (last n)) =
    (f (init (update m i✝.castSucc x))) (update m i✝.castSucc x (last n)) +
      (f (init (update m i✝.castSucc y))) (update m i✝.castSucc y (last n))

Tactic:
<;>

Goal state after:
case last
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₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n.succ) → M i
x y : M (last n)
⊢ (f (init (update m (last n) (x + y)))) (update m (last n) (x + y) (last n)) =
    (f (init (update m (last n) x))) (update m (last n) x (last n)) +
      (f (init (update m (last n) y))) (update m (last n) y (last n))

case cast
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₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n.succ) → M i
i✝ : Fin n
x y : M i✝.castSucc
⊢ (f (init (update m i✝.castSucc (x + y)))) (update m i✝.castSucc (x + y) (last n)) =
    (f (init (update m i✝.castSucc x))) (update m i✝.castSucc x (last n)) +
      (f (init (update m i✝.castSucc y))) (update m i✝.castSucc y (last n))
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: case last
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₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n.succ) → M i
c : R
x : M (last n)
⊢ (f (init (update m (last n) (c • x)))) (update m (last n) (c • x) (last n)) =
    c • (f (init (update m (last n) x))) (update m (last n) x (last n))

pp: case cast
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₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n.succ) → M i
c : R
i✝ : Fin n
x : M i✝.castSucc
⊢ (f (init (update m i✝.castSucc (c • x)))) (update m i✝.castSucc (c • x) (last n)) =
    c • (f (init (update m i✝.castSucc x))) (update m i✝.castSucc x (last n))

Tactic:
<;>

Goal state after:
case last
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₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n.succ) → M i
c : R
x : M (last n)
⊢ (f (init (update m (last n) (c • x)))) (update m (last n) (c • x) (last n)) =
    c • (f (init (update m (last n) x))) (update m (last n) x (last n))

case cast
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₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n.succ) → M i
c : R
i✝ : Fin n
x : M i✝.castSucc
⊢ (f (init (update m i✝.castSucc (c • x)))) (update m i✝.castSucc (c • x) (last n)) =
    c • (f (init (update m i✝.castSucc x))) (update m i✝.castSucc x (last n))
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))

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

Goal state after:
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))

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))
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))

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

Goal state after:
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))

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))
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : ↑n < ENat.card α
val✝ : Fintype α
this : (Nat.card α).choose n ≤ 1
⊢ False

Tactic:
rw [Nat.le_one_iff_eq_zero_or_eq_one] at this

Goal state after:
case inl
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : ↑n < ENat.card α
val✝ : Fintype α
this : (Nat.card α).choose n = 0 ∨ (Nat.card α).choose n = 1
⊢ False
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✝)

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

Goal state after:
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✝)

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✝)
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

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

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

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
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case hij.hab
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
i : I
his : i ∈ ↑s
hit : i ∈ ↑t
j : Fin m
hj : (ofFinEmbEquiv.symm s) j = i
k : Fin n
hk : (ofFinEmbEquiv.symm t) k = i
⊢ ↑(Fin.castAdd n j) < m

pp: case hij.hbc
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
i : I
his : i ∈ ↑s
hit : i ∈ ↑t
j : Fin m
hj : (ofFinEmbEquiv.symm s) j = i
k : Fin n
hk : (ofFinEmbEquiv.symm t) k = i
⊢ m ≤ ↑(Fin.natAdd m k)

Tactic:
<;>

Goal state after:
case hij.hab
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
i : I
his : i ∈ ↑s
hit : i ∈ ↑t
j : Fin m
hj : (ofFinEmbEquiv.symm s) j = i
k : Fin n
hk : (ofFinEmbEquiv.symm t) k = i
⊢ ↑(Fin.castAdd n j) < m

case hij.hbc
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
i : I
his : i ∈ ↑s
hit : i ∈ ↑t
j : Fin m
hj : (ofFinEmbEquiv.symm s) j = i
k : Fin n
hk : (ofFinEmbEquiv.symm t) k = i
⊢ m ≤ ↑(Fin.natAdd m k)