mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case mk.mk
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q Q' : QuadraticMap R M N
toFun✝¹ : M → N
toFun_smul✝¹ : ∀ (a : R) (x : M), toFun✝¹ (a • x) = (a * a) • toFun✝¹ x
exists_companion'✝¹ : ∃ B, ∀ (x y : M), toFun✝¹ (x + y) = toFun✝¹ x + toFun✝¹ y + (B x) y
toFun✝ : M → N
toFun_smul✝ : ∀ (a : R) (x : M), toFun✝ (a • x) = (a * a) • toFun✝ x
exists_companion'✝ : ∃ B, ∀ (x y : M), toFun✝ (x + y) = toFun✝ x + toFun✝ y + (B x) y
h :
  { toFun := toFun✝¹, toFun_smul := toFun_smul✝¹, exists_companion' := exists_companion'✝¹ }.toFun =
    { toFun := toFun✝, toFun_smul := toFun_smul✝, exists_companion' := exists_companion'✝ }.toFun
⊢ { toFun := toFun✝¹, toFun_smul := toFun_smul✝¹, exists_companion' := exists_companion'✝¹ } =
    { toFun := toFun✝, toFun_smul := toFun_smul✝, exists_companion' := exists_companion'✝ }

Tactic:
;

Goal state after:
case mk.mk
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q Q' : QuadraticMap R M N
toFun✝¹ : M → N
toFun_smul✝¹ : ∀ (a : R) (x : M), toFun✝¹ (a • x) = (a * a) • toFun✝¹ x
exists_companion'✝¹ : ∃ B, ∀ (x y : M), toFun✝¹ (x + y) = toFun✝¹ x + toFun✝¹ y + (B x) y
toFun✝ : M → N
toFun_smul✝ : ∀ (a : R) (x : M), toFun✝ (a • x) = (a * a) • toFun✝ x
exists_companion'✝ : ∃ B, ∀ (x y : M), toFun✝ (x + y) = toFun✝ x + toFun✝ y + (B x) y
h :
  { toFun := toFun✝¹, toFun_smul := toFun_smul✝¹, exists_companion' := exists_companion'✝¹ }.toFun =
    { toFun := toFun✝, toFun_smul := toFun_smul✝, exists_companion' := exists_companion'✝ }.toFun
⊢ { toFun := toFun✝¹, toFun_smul := toFun_smul✝¹, exists_companion' := exists_companion'✝¹ } =
    { toFun := toFun✝, toFun_smul := toFun_smul✝, exists_companion' := exists_companion'✝ }
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
i j : ι
r : R
x : A i
y : A j
⊢ { toFun := fun b ↦ GradedMonoid.GMul.mul (r • x) b, map_add' := ⋯, map_smul' := ⋯ } y =
    ((RingHom.id R) r • { toFun := fun b ↦ GradedMonoid.GMul.mul x b, map_add' := ⋯, map_smul' := ⋯ }) y

Tactic:
by
    injection smul_assoc r (GradedMonoid.mk _ x) (GradedMonoid.mk _ y)

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i), (mulHom A) ((of A i) y) = (mulHom A).flip ((of A i) y)

Tactic:
;

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i), (mulHom A) ((of A i) y) = (mulHom A).flip ((of A i) y)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ (mulHom A) ((of A ai) ax) = (mulHom A).flip ((of A ai) ax)

Tactic:
;

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ (mulHom A) ((of A ai) ax) = (mulHom A).flip ((of A ai) ax)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ ∀ (i : ι) (y : A i), ((mulHom A) ((of A ai) ax)) ((of A i) y) = ((mulHom A).flip ((of A ai) ax)) ((of A i) y)

Tactic:
;

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ ∀ (i : ι) (y : A i), ((mulHom A) ((of A ai) ax)) ((of A i) y) = ((mulHom A).flip ((of A ai) ax)) ((of A i) y)
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i j : ι
hxi : x ∈ ℳ i
hxj : x ∈ ℳ j
hx : i ≠ j
⊢ x = 0

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i j : ι
hxi : x ∈ ℳ i
hxj : x ∈ ℳ j
hx : i ≠ j
⊢ x = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case mk
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
ι : Type u_8
Q : QuadraticMap R M N
g : ι → M
l : ι → R
p : Sym2 ι
fst✝ snd✝ : ι
⊢ polarSym2 (⇑Q) (Sym2.map (l • g) (Quot.mk (Sym2.Rel ι) (fst✝, snd✝))) =
    (Sym2.map l (Quot.mk (Sym2.Rel ι) (fst✝, snd✝))).mul •
      polarSym2 (⇑Q) (Sym2.map g (Quot.mk (Sym2.Rel ι) (fst✝, snd✝)))

Tactic:
;

Goal state after:
case mk
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
ι : Type u_8
Q : QuadraticMap R M N
g : ι → M
l : ι → R
p : Sym2 ι
fst✝ snd✝ : ι
⊢ polarSym2 (⇑Q) (Sym2.map (l • g) (Quot.mk (Sym2.Rel ι) (fst✝, snd✝))) =
    (Sym2.map l (Quot.mk (Sym2.Rel ι) (fst✝, snd✝))).mul •
      polarSym2 (⇑Q) (Sym2.map g (Quot.mk (Sym2.Rel ι) (fst✝, snd✝)))
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
i : ι
⊢ A i →+ R

Tactic:
;

Goal state after:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
i : ι
⊢ A i →+ R
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x y : M
⊢ (⋯.choose x) y = (Q.polarBilin x) y

Tactic:
rw [polarBilin_apply_apply, polar, Q.exists_companion.choose_spec, sub_sub,
      add_sub_cancel_left]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
Q : QuadraticMap R N P
f : M →ₗ[R] N
B : BilinMap R N P
h : ∀ (x y : N), Q (x + y) = Q x + Q y + (B x) y
x y : M
⊢ Q (f x + f y) = Q (f x) + Q (f y) + ((LinearMap.compl₁₂ B f f) x) y

Tactic:
;

Goal state after:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
Q : QuadraticMap R N P
f : M →ₗ[R] N
B : BilinMap R N P
h : ∀ (x y : N), Q (x + y) = Q x + Q y + (B x) y
x y : M
⊢ Q (f x + f y) = Q (f x) + Q (f y) + ((LinearMap.compl₁₂ B f f) x) y
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: case neg.inl
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
h' : i ≠ 0
⊢ 0 = ↑(((decompose 𝒜) c) 0) * ↑(((decompose 𝒜) c') 0)

Tactic:
simp only [decompose_of_mem_ne 𝒜 hc h', zero_mul]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : ↥(𝒜 0)
⊢ ↑((projZeroRingHom' 𝒜) ↑a) = ↑a

Tactic:
;

Goal state after:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : ↥(𝒜 0)
⊢ ↑((projZeroRingHom' 𝒜) ↑a) = ↑a
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ∑ i ∈ DFinsupp.support r,
      ↑((DFinsupp.sum r' fun x aj ↦ (of (fun i ↦ ↥(A i)) (i + x)) (GradedMonoid.GMul.mul (r i) aj)) n) =
    DFinsupp.sum r fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0

Tactic:
;

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ∑ i ∈ DFinsupp.support r,
      ↑((DFinsupp.sum r' fun x aj ↦ (of (fun i ↦ ↥(A i)) (i + x)) (GradedMonoid.GMul.mul (r i) aj)) n) =
    DFinsupp.sum r fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case e_f
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ (fun i ↦ ↑((DFinsupp.sum r' fun x aj ↦ (of (fun i ↦ ↥(A i)) (i + x)) (GradedMonoid.GMul.mul (r i) aj)) n)) = fun i ↦
    (fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0) i (r i)

Tactic:
;

Goal state after:
case e_f
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ (fun i ↦ ↑((DFinsupp.sum r' fun x aj ↦ (of (fun i ↦ ↥(A i)) (i + x)) (GradedMonoid.GMul.mul (r i) aj)) n)) = fun i ↦
    (fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0) i (r i)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case e_f
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝ : ι
⊢ ∑ i ∈ DFinsupp.support r', ↑(((of (fun i ↦ ↥(A i)) (x✝ + i)) (GradedMonoid.GMul.mul (r x✝) (r' i))) n) =
    (fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0) x✝ (r x✝)

Tactic:
;

Goal state after:
case e_f
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝ : ι
⊢ ∑ i ∈ DFinsupp.support r', ↑(((of (fun i ↦ ↥(A i)) (x✝ + i)) (GradedMonoid.GMul.mul (r x✝) (r' i))) n) =
    (fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0) x✝ (r x✝)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case e_f.e_f
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝ : ι
⊢ (fun i ↦ ↑(((of (fun i ↦ ↥(A i)) (x✝ + i)) (GradedMonoid.GMul.mul (r x✝) (r' i))) n)) = fun i ↦
    (fun j rj ↦ if x✝ + j = n then ↑(r x✝) * ↑rj else 0) i (r' i)

Tactic:
;

Goal state after:
case e_f.e_f
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝ : ι
⊢ (fun i ↦ ↑(((of (fun i ↦ ↥(A i)) (x✝ + i)) (GradedMonoid.GMul.mul (r x✝) (r' i))) n)) = fun i ↦
    (fun j rj ↦ if x✝ + j = n then ↑(r x✝) * ↑rj else 0) i (r' i)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ↑((r * r') n) = DFinsupp.sum r fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0

Tactic:
rw [mul_eq_dfinsuppSum]
  iterate 2 rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]; congr; ext
  dsimp only
  split_ifs with h
  · subst h
    rw [of_eq_same]
    rfl
  · rw [of_eq_of_ne _ _ _ (Ne.symm h)]
    rfl

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

Goal state after:
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✝
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ ↑((r * (of (fun i ↦ ↥(A i)) i) r') n) = 0

Tactic:
by
  classical
    rw [coe_mul_apply_eq_dfinsuppSum, DFinsupp.sum_comm]
    apply (DFinsupp.sum_single_index _).trans
    swap
    · simp_rw [ZeroMemClass.coe_zero, mul_zero, ite_self]
      exact DFinsupp.sum_zero
    · rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]
      exact fun x _ H => h ((self_le_add_left i x).trans_eq H)

Goal state after:
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case cons
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : SetLike.GradedMonoid A
inst✝ : CanonicallyOrderedAdd ι
m : ι
head : ⨁ (i : ι), ↥(A i)
tail : List (⨁ (i : ι), ↥(A i))
ih : (∀ x ∈ tail, ∀ k < m, x k = 0) → ∀ ⦃n : ι⦄, n < tail.length • m → tail.prod n = 0
n : ι
hn : n < (tail.length + 1) • m
hl : (∀ k < m, head k = 0) ∧ ∀ a ∈ tail, ∀ k < m, a k = 0
⊢ n < m + tail.length • m

Tactic:
simpa [add_smul, add_comm m] using hn

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

Goal state before:
pp: case mem.algebraMap
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 : ℕ
r : R
⊢ (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) 0) (DirectSum.GAlgebra.toFun r) =
    (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑0) ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩

Tactic:
;

Goal state after:
case mem.algebraMap
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 : ℕ
r : R
⊢ (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) 0) (DirectSum.GAlgebra.toFun r) =
    (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑0) ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ ⟨0, ⋯⟩ = 0

Tactic:
;

Goal state after:
case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ ⟨0, ⋯⟩ = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' x y : CliffordAlgebra Q
hx : x ∈ ⨆ i, (ι Q).range ^ ↑i
hy : y ∈ ⨆ i, (ι Q).range ^ ↑i
ihx : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨x, hx⟩
ihy : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) y = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨y, hy⟩
⊢ (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') (⟨x, hx⟩ + ⟨y, hy⟩) = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨x + y, ⋯⟩

Tactic:
;

Goal state after:
case add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' x y : CliffordAlgebra Q
hx : x ∈ ⨆ i, (ι Q).range ^ ↑i
hy : y ∈ ⨆ i, (ι Q).range ^ ↑i
ihx : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨x, hx⟩
ihy : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) y = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨y, hy⟩
⊢ (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') (⟨x, hx⟩ + ⟨y, hy⟩) = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨x + y, ⋯⟩
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
x✝ : (i : Fin n) → M (p.succAbove i)
⊢ (mk' (fun m ↦ f (p.insertNth (x + y) m)) ⋯ ⋯) x✝ =
    (mk' (fun m ↦ f (p.insertNth x m)) ⋯ ⋯ + mk' (fun m ↦ f (p.insertNth y m)) ⋯ ⋯) x✝

Tactic:
;

Goal state after:
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
x✝ : (i : Fin n) → M (p.succAbove i)
⊢ (mk' (fun m ↦ f (p.insertNth (x + y) m)) ⋯ ⋯) x✝ =
    (mk' (fun m ↦ f (p.insertNth x m)) ⋯ ⋯ + mk' (fun m ↦ f (p.insertNth y m)) ⋯ ⋯) x✝
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
x✝ : (i : Fin n) → M (p.succAbove i)
⊢ (mk' (fun m ↦ f (p.insertNth (c • x) m)) ⋯ ⋯) x✝ = ((RingHom.id R) c • mk' (fun m ↦ f (p.insertNth x m)) ⋯ ⋯) x✝

Tactic:
;

Goal state after:
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
x✝ : (i : Fin n) → M (p.succAbove i)
⊢ (mk' (fun m ↦ f (p.insertNth (c • x) m)) ⋯ ⋯) x✝ = ((RingHom.id R) c • mk' (fun m ↦ f (p.insertNth x m)) ⋯ ⋯) x✝
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)
⊢ Fintype.card α - n = m

Tactic:
;

Goal state after:
α : Type u_1
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : ↑(powersetCard α n)
⊢ Fintype.card α - n = m
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)
⊢ Fintype.card α - m = n

Tactic:
;

Goal state after:
α : Type u_1
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
t : ↑(powersetCard α m)
⊢ Fintype.card α - m = n
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:
;

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

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

Goal state after:
α : Type u_1
n : ℕ
inst✝ : Fintype α
x✝ : Finset α
⊢ x✝ ∈ powersetCard α n ↔ x✝ ∈ ↑(Finset.powersetCard n Finset.univ)
Module: Mathlib.Data.Set.PowersetCard

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

Tactic:
;

Goal state after:
α : Type u_1
n : ℕ
h : 0 < n
inst✝ : Infinite α
a : α
⊢ 1 ≤ n