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

Goal state before:
pp: K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
⊢ LinearIndependent K₁ v

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
⊢ (dualTensorHom R N P) (g ⊗ₜ[R] p) ∘ₗ (dualTensorHom R M N) (f ⊗ₜ[R] n) = g n • (dualTensorHom R M P) (f ⊗ₜ[R] p)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
p : Submodule R₁ M₁
x✝¹ x✝ : ↥p
⊢ ((B.domRestrict₁₂ p p) x✝¹) x✝ = 0 → ((B.domRestrict₁₂ p p) x✝) x✝¹ = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
⊢ B.flip.ker = B.ker

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
h : B.ker = ⊥
⊢ B.flip.ker = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
⊢ B.ker = ⊥ ↔ B.flip.ker = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
x y : M
H1 : (B x) y = 0
⊢ (B y) x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
p : Submodule R M
x✝¹ x✝ : ↥p
⊢ I (((B.domRestrict₁₂ p p) x✝¹) x✝) = ((B.domRestrict₁₂ p p) x✝) x✝¹

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B C : M →ₛₗ[I] M →ₗ[R] R
hB : B.IsSymm
hC : C.IsSymm
x y : M
⊢ I (((B + C) x) y) = ((B + C) y) x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_20
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
B : LinearMap.BilinMap R M N
⊢ (∀ (x y : M), (B x) y = (B y) x) ↔ B = flip B

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i : n
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) = Matrix.single i j 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring R₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst✝ : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
⊢ (B a) a + (B a) b + (B a) c = (B a) c + (B b) c + (B c) c

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring R₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst✝ : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
⊢ (B a) b = (B b) c

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : 1 ∈ (dualTensorHom R M M).range
s : Finset (Dual R M × M)
eq : (dualTensorHom R M M) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) = 1
f : (↥s → R) →ₗ[R] M := Fintype.linearCombination R fun x ↦ (↑x).2
⊢ (f ∘ₗ pi fun x ↦ (↑x).1) = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x y : M₁
⊢ -(B x) y = (B y) x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : 1 ∈ (dualTensorHom R M M).range
⊢ Module.Finite R M ∧ Projective R M

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
⊢ B.IsRefl

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
b : Basis ι R M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ dualTensorHom R M N ∘ₗ ∑ i, (TensorProduct.mk R (Dual R M) N) (b.dualBasis i) ∘ₗ applyₗ (b i) = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
b : Basis ι R M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ (∑ i, (TensorProduct.mk R (Dual R M) N) (b.dualBasis i) ∘ₗ applyₗ (b i)) ∘ₗ dualTensorHom R M N = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
b : Basis ι R M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Dual R M ⊗[R] N
⊢ (dualTensorHomEquivOfBasis b).symm ((dualTensorHom R M N) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
b : Basis ι R M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : M →ₗ[R] N
⊢ (dualTensorHom R M N) ((dualTensorHomEquivOfBasis b).symm x) = x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I : R₁ →+* R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
⊢ B.IsAlt ↔ B = -B.flip

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
⊢ B.IsAdjointPair B' ⇑f ⇑g ↔ B' ∘ₗ f = B.compl₂ g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
x✝¹ : M
x✝ : M₁
⊢ (B' (0 x✝¹)) x✝ = (B x✝¹) (0 x✝)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
⊢ Function.Bijective ⇑(dualTensorHom R M N)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ dualTensorHom R M R = ↑(TensorProduct.rid R (Dual R M))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Function.Bijective ⇑(dualTensorHom R M R)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B' ((f + f') x)) x✝ = (B x) ((g + g') x✝)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : DecidableEq ι
⊢ dualTensorHom R M (ι →₀ N) =
    finsuppLinearMap R ∘ₗ Finsupp.mapRange.linearMap (dualTensorHom R M N) ∘ₗ ↑(finsuppRight R R (Dual R M) N ι)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : Module R M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] M₃
f : M → M₁
g : M₁ → M
f' : M₁ → M₂
g' : M₂ → M₁
h : B.IsAdjointPair B' f g
h' : B'.IsAdjointPair B'' f' g'
x✝¹ : M
x✝ : M₂
⊢ (B'' ((f' ∘ f) x✝¹)) x✝ = (B x✝¹) ((g ∘ g') x✝)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B' ((f - f') x)) x✝ = (B x) ((g - g') x✝)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
fin : Finite ι ∨ Module.Finite R M
h : Function.Bijective ⇑(dualTensorHom R M N)
⊢ Function.Bijective ⇑(dualTensorHom R M (ι →₀ N))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F =
    pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f : M → M₁
g : M₁ → M
c : R
h : B.IsAdjointPair B' f g
x✝¹ : M
x✝ : M₁
⊢ (B' ((c • f) x✝¹)) x✝ = (B x✝¹) ((c • g) x✝)

Tactic:
by

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

Goal state before:
pp: R : Type u_20
M : Type u_21
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
f : M ≃ M
hf : IsAdjointPair B B ⇑f ⇑f.symm
x y : M
⊢ (B (f x)) (f y) = (B x) y

Tactic:
by

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

Goal state before:
pp: R : Type u_20
M : Type u_21
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
f : M ≃ M
hf : IsOrthogonal B ⇑f
x y : M
⊢ (B (f x)) y = (B x) (f.symm y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F ≫ F.map WalkingParallelPairHom.left =
    pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      F.map WalkingParallelPairHom.right

Tactic:
convert!
          (eq_whisker pullback.condition Limits.prod.snd :
            (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.one) = _) using
          1

Goal state after:
case e'_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F ≫ F.map WalkingParallelPairHom.left =
    (pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left)) ≫
      prod.snd

case e'_3
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      F.map WalkingParallelPairHom.right =
    (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      prod.snd
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B x) x + (B (f x)) (f y) + ((B (f x)) (f y) + (B y) y) = (B x) x + (B x) y + ((B x) y + (B y) y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

Tactic:
simp only [add_assoc, add_right_inj] at this

Goal state after:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B (f x)) (f y) + ((B (f x)) (f y) + (B y) y) = (B x) y + ((B x) y + (B y) y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
g : P →ₗ[R] N
comp_eq_id : g ∘ₗ f = LinearMap.id
h : Function.Bijective ⇑(dualTensorHom R M P)
⊢ Function.Injective (⇑(compRight R f) ∘ ⇑(dualTensorHom R M N))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F ≫ F.map WalkingParallelPairHom.left = pullbackFst F ≫ F.map WalkingParallelPairHom.right

Tactic:
by

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

Goal state before:
pp: R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
⊢ IsOrthogonal B ⇑f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
⊢ F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f = (F ∘ₗ f).compl₁₂ ↑e ↑e

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
g : P →ₗ[R] N
comp_eq_id : g ∘ₗ f = LinearMap.id
h : Function.Bijective ⇑(dualTensorHom R M P)
⊢ Function.Surjective (⇑(dualTensorHom R M N) ∘ ⇑(lTensor (Dual R M) g))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
hₗ : F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f = (F ∘ₗ f).compl₁₂ ↑e ↑e
⊢ (B.compl₁₂ ↑e ↑e).compl₂ (e.symm.conj f) = (B.compl₂ f).compl₁₂ ↑e ↑e

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ ∀ (s : Cone F) (j : WalkingParallelPair),
    pullback.lift (s.π.app WalkingParallelPair.zero) (s.π.app WalkingParallelPair.zero) ⋯ ≫ (equalizerCone F).π.app j =
      s.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Finite ι
h : Function.Bijective ⇑(dualTensorHom R M N)
⊢ ↑(Finsupp.linearEquivFunOnFinite R N ι) ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R N ι).symm = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
b : Basis ι R M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ have this := ⋯;
  have this_1 := ⋯;
  dualTensorHomEquiv R M N = dualTensorHomEquivOfBasis b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
⊢ B.IsPairSelfAdjoint F ⇑f ↔ (B.compl₁₂ ↑e ↑e).IsPairSelfAdjoint (F.compl₁₂ ↑e ↑e) ⇑(e.symm.conj f)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
f : End R M
⊢ f ∈ B.skewAdjointSubmodule ↔ B.IsSkewAdjoint ⇑f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : B.SeparatingLeft
⊢ ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B).SeparatingLeft

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B).SeparatingLeft
⊢ B.SeparatingLeft

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ B.flip.SeparatingLeft ↔ B.SeparatingRight

Tactic:
by

Goal state after: