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

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
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : CliffordAlgebra Q →ₐ[R] A
m : M
⊢ g ((ι Q) m) * g ((ι Q) m) = (algebraMap R A) (Q m)

Tactic:
by
  rw [← map_mul, ι_sq_scalar, AlgHom.commutes]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
i j : Fin 2
⊢ ↑(diag2 a ha) i j = !![a, 0; 0, a⁻¹] i j

Tactic:
fin_cases i <;> fin_cases j <;> simp [diag2n_coe]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
⊢ (((toLinearMap₂' T) M) v) w = v ⬝ᵥ M *ᵥ w

Tactic:
simp_rw [Matrix.toLinearMap₂'_apply, dotProduct, Matrix.mulVec, dotProduct]
  refine Finset.sum_congr rfl fun _ _ => ?_
  rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun _ _ => ?_
  rw [smul_eq_mul, smul_eq_mul, mul_comm (w _), ← mul_assoc]

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
Q : QuadraticMap R M N
x : M
⊢ (2 * 2) • Q x = 4 • Q x

Tactic:
← Nat.cast_smul_eq_nsmul R

Goal state after:
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
Q : QuadraticMap R M N
x : M
⊢ (2 * 2) • Q x = ↑4 • Q x
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 j : ι
⊢ ∀ (ai : A i) (aj : A j),
    ((↑F).comp (of A (i + j))) (GradedMonoid.GMul.mul ai aj) = ((↑F).comp (of A i)) ai * ((↑F).comp (of A j)) aj

Tactic:
ai

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 j : ι
ai : A i
⊢ ∀ (aj : A j),
    ((↑F).comp (of A (i + j))) (GradedMonoid.GMul.mul ai aj) = ((↑F).comp (of A i)) ai * ((↑F).comp (of A j)) aj
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ (b₁.toMatrix ⇑c₁)ᵀ * (toMatrix₂ b₁ b₂) B * b₂.toMatrix ⇑c₂ = (toMatrix₂ c₁ c₂) B

Tactic:
← LinearMap.toMatrix_id_eq_basis_toMatrix

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ ((toMatrix c₁ b₁) id)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix c₂ b₂) id = (toMatrix₂ c₁ c₂) B
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddLeftCancelMonoid ι
inst✝ : GradedRing 𝒜
b : A
a : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) ↑a * (decompose 𝒜) b) (i + j)) = ↑a * ↑(((decompose 𝒜) b) j)

Tactic:
decompose_coe,

Goal state after:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddLeftCancelMonoid ι
inst✝ : GradedRing 𝒜
b : A
a : ↥(𝒜 i)
⊢ ↑(((of (fun i ↦ ↥(𝒜 i)) i) a * (decompose 𝒜) b) (i + j)) = ↑a * ↑(((decompose 𝒜) b) j)
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : ↥(𝒜 j)
⊢ ↑(((decompose 𝒜) a * (decompose 𝒜) ↑b) (i + j)) = ↑(((decompose 𝒜) a) i) * ↑b

Tactic:
decompose_coe,

Goal state after:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : ↥(𝒜 j)
⊢ ↑(((decompose 𝒜) a * (of (fun i ↦ ↥(𝒜 i)) j) b) (i + j)) = ↑(((decompose 𝒜) a) i) * ↑b
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
j : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
b : A
a : ↥(𝒜 0)
⊢ ↑(((decompose 𝒜) ↑a * (decompose 𝒜) b) j) = ↑a * ↑(((decompose 𝒜) b) j)

Tactic:
decompose_coe,

Goal state after:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
j : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
b : A
a : ↥(𝒜 0)
⊢ ↑(((of (fun i ↦ ↥(𝒜 i)) 0) a * (decompose 𝒜) b) j) = ↑a * ↑(((decompose 𝒜) b) j)
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : ↥(𝒜 0)
⊢ ↑(((decompose 𝒜) a * (decompose 𝒜) ↑b) i) = ↑(((decompose 𝒜) a) i) * ↑b

Tactic:
decompose_coe,

Goal state after:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : ↥(𝒜 0)
⊢ ↑(((decompose 𝒜) a * (of (fun i ↦ ↥(𝒜 i)) 0) b) i) = ↑(((decompose 𝒜) a) i) * ↑b
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 𝒜
b : A
n i : ι
h : ¬i ≤ n
a : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) ↑a * (decompose 𝒜) b) n) = 0

Tactic:
decompose_coe,

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 𝒜
b : A
n i : ι
h : ¬i ≤ n
a : ↥(𝒜 i)
⊢ ↑(((of (fun i ↦ ↥(𝒜 i)) i) a * (decompose 𝒜) b) n) = 0
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 : A
n i : ι
h : ¬i ≤ n
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) a * (decompose 𝒜) ↑b) n) = 0

Tactic:
decompose_coe,

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 : A
n i : ι
h : ¬i ≤ n
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) a * (of (fun i ↦ ↥(𝒜 i)) i) b) n) = 0
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 𝒜
b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
h : i ≤ n
a : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) ↑a * (decompose 𝒜) b) n) = ↑a * ↑(((decompose 𝒜) b) (n - i))

Tactic:
decompose_coe,

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 𝒜
b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
h : i ≤ n
a : ↥(𝒜 i)
⊢ ↑(((of (fun i ↦ ↥(𝒜 i)) i) a * (decompose 𝒜) b) n) = ↑a * ↑(((decompose 𝒜) b) (n - i))
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 : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
h : i ≤ n
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) a * (decompose 𝒜) ↑b) n) = ↑(((decompose 𝒜) a) (n - i)) * ↑b

Tactic:
decompose_coe,

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 : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
h : i ≤ n
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) a * (of (fun i ↦ ↥(𝒜 i)) i) b) n) = ↑(((decompose 𝒜) a) (n - i)) * ↑b
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 𝒜
b : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
a : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) ↑a * (decompose 𝒜) b) n) = if i ≤ n then ↑a * ↑(((decompose 𝒜) b) (n - i)) else 0

Tactic:
decompose_coe,

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 𝒜
b : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
a : ↥(𝒜 i)
⊢ ↑(((of (fun i ↦ ↥(𝒜 i)) i) a * (decompose 𝒜) b) n) = if i ≤ n then ↑a * ↑(((decompose 𝒜) b) (n - i)) else 0
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 : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) a * (decompose 𝒜) ↑b) n) = if i ≤ n then ↑(((decompose 𝒜) a) (n - i)) * ↑b else 0

Tactic:
decompose_coe,

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 : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) a * (of (fun i ↦ ↥(𝒜 i)) i) b) n) = if i ≤ n then ↑(((decompose 𝒜) a) (n - i)) * ↑b else 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case pos
ι : 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)
x✝¹ x✝ : ι
⊢ ↑(((of (fun i ↦ ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) (x✝¹ + x✝)) = ↑(r x✝¹) * ↑(r' x✝)

Tactic:
of_eq_same

Goal state after:
case pos
ι : 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)
x✝¹ x✝ : ι
⊢ ↑(GradedMonoid.GMul.mul (r x✝¹) (r' x✝)) = ↑(r x✝¹) * ↑(r' x✝)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
f g : M →ₗ[R] R
⊢ associated (linMulLin f g) = ⅟2 • ((mul R R).compl₁₂ f g + (mul R R).compl₁₂ g f)

Tactic:
by
  ext
  simp only [associated_apply, linMulLin_apply, map_add, smul_add, LinearMap.add_apply,
    LinearMap.smul_apply, compl₁₂_apply, mul_apply', smul_eq_mul, invOf_smul_eq_iff]
  simp only [Module.End.smul_def, Module.End.ofNat_apply, nsmul_eq_mul, Nat.cast_ofNat,
    mul_invOf_cancel_left']
  ring_nf

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticMap R M R
hB : Q.Anisotropic
x : M
hx : ∀ (y : M), ((associated' Q) x) y = 0
⊢ Q x = 0

Tactic:
rw [← hx x]
  exact (associated_eq_self_apply _ _ x).symm

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₂
f : MultilinearMap R M M₂
c : R
x : M 0
⊢ mk' (fun m ↦ f (Fin.cons (c • x) m)) ⋯ ⋯ = (RingHom.id R) c • mk' (fun m ↦ f (Fin.cons x m)) ⋯ ⋯

Tactic:
by
    ext m
    exact cons_smul f m c x

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 (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n) → M i.castSucc
x : M (last n)
⊢ (f.uncurryRight.curryRight m) x = (f m) x

Tactic:
simp only [snoc_last, MultilinearMap.curryRight_apply, MultilinearMap.uncurryRight_apply]

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₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n) → M i.castSucc
x : M (last n)
⊢ (f (init (snoc m x))) x = (f m) x
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
⊢ Finite α

Tactic:
rw [← Set.finite_univ_iff, ← this]

Goal state after:
α : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Infinite α
finite : Finite ↑(powersetCard α n)
this : ⋃₀ (SetLike.coe '' powersetCard α n) = univ
⊢ (⋃₀ (SetLike.coe '' powersetCard α n)).Finite
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case e_6
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)
h : Disjoint ↑s ↑t
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) i =
    ((v ∘ ⇑(ofFinEmbEquiv.symm (disjUnion h))) ∘
        ⇑(finSumFinEquiv.symm.trans
            ((↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t))).trans
              ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h).trans ↑(orderIsoOfFin (disjUnion h)).symm))))
      i

Tactic:
change _ = v (e (e.symm _))

Goal state after:
case e_6
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)
h : Disjoint ↑s ↑t
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) i =
    v
      ↑(e
          (e.symm
            ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
              (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t)) (finSumFinEquiv.symm i)))))
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
⊢ IsConnected C ↔ Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})

Tactic:
by
  refine ⟨fun _ => ⟨colimitConstPUnitIsoPUnit.{w} C⟩, fun ⟨h⟩ => ?_⟩
  have : Nonempty C := nonempty_of_nonempty_colimit <| Nonempty.map h.inv inferInstance
  refine zigzag_isConnected <| fun c d => ?_
  refine zigzag_of_eqvGen_colimitTypeRel _ (constPUnitFunctor C) ⟨c, PUnit.unit⟩ ⟨d, PUnit.unit⟩ ?_
  exact colimit_eq <| h.toEquiv.injective rfl

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ ∀ {c : Cᵒᵖ} (s s' : op d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t

Tactic:
· intro c s s'
    obtain ⟨c', t, ht⟩ := h₂ s.unop s'.unop
    exact ⟨op c', Quiver.Hom.op t, Quiver.Hom.unop_inj ht⟩

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
⊢ ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : d ⟶ (Pi.eval I s).obj c),
    ∃ c' t, s_1 ≫ (Pi.eval I s).map t = s' ≫ (Pi.eval I s).map t

Tactic:
intro d c f g

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
d : I s
c : (i : α) → I i
f g : d ⟶ (Pi.eval I s).obj c
⊢ ∃ c' t, f ≫ (Pi.eval I s).map t = g ≫ (Pi.eval I s).map t
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
⊢ ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : (Pi.eval I s).obj c ⟶ d),
    ∃ c' t, (Pi.eval I s).map t ≫ s_1 = (Pi.eval I s).map t ≫ s'

Tactic:
intro d c f g

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
d : I s
c : (i : α) → I i
f g : (Pi.eval I s).obj c ⟶ d
⊢ ∃ c' t, (Pi.eval I s).map t ≫ f = (Pi.eval I s).map t ≫ g
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ M.ιFreeYonedaCoproduct m ≫ M.fromFreeYonedaCoproduct = m.fromFreeYoneda

Tactic:
by
  apply Sigma.ι_desc

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitCurrySwapCompLimIsoLimitCurryCompLim G).inv ≫
      limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j =
    limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k

Tactic:
simp [limitCurrySwapCompLimIsoLimitCurryCompLim]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : F.PartialRightAdjointSource
⊢ F.partialRightAdjointHomEquiv (F.partialRightAdjointMap (𝟙 X)) =
    F.partialRightAdjointHomEquiv (𝟙 (F.partialRightAdjointObj X))

Tactic:
simp [partialRightAdjointHomEquiv_map]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ pullbackObjIsDefined φ M

Tactic:
apply leftAdjointObjIsDefined_of_isColimit
    M.isColimitFreeYonedaCoproductsCokernelCofork

Goal state after:
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ ∀ (j : WalkingParallelPair), (pushforward φ).leftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj j)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y✝ : ι → C
f : (i : ι) → Y✝ i ⟶ X
Y : C
i : ι
⊢ f i = eqToHom ⋯ ≫ f i

Tactic:
by simp only [eqToHom_refl, id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
g : Z ⟶ X
hg : ofArrows Y f g
⊢ ∃ i, ∃ (h : Y i = Z), g = eqToHom ⋯ ≫ f i

Tactic:
by
  obtain ⟨i⟩ := hg
  exact ⟨i, rfl, by simp only [eqToHom_refl, id_comp]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
⊢ (FamilyOfElements.restrict ⋯ x).sieveExtend = x

Tactic:
funext _ _ h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : (generate R).arrows x✝
⊢ (FamilyOfElements.restrict ⋯ x).sieveExtend x✝ h = x x✝ h
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ Z
f₂ : Z₂ ⟶ Z
h₁ : Presieve.functorPullback F T f₁
h₂ : Presieve.functorPullback F T f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ F.map g₁ ≫ F.map f₁ = F.map g₂ ≫ F.map f₂

Tactic:
by simp only [← F.map_comp, eq]

Goal state after: