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

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

case mpr
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' ∘ₗ f = B.compl₂ g → B.IsAdjointPair B' ⇑f ⇑g
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:
ext

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ : Dual R M
x✝ : M
⊢ (((AlgebraTensorModule.curry (dualTensorHom R M R)) x✝¹) 1) x✝ =
    (((AlgebraTensorModule.curry ↑(TensorProduct.rid R (Dual R M))) x✝¹) 1) x✝
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:
ext

Goal state after:
ι : 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 ι
x✝² : Dual R M
a✝¹ : ι
x✝¹ : N
x✝ : M
a✝ : ι
⊢ ((((AlgebraTensorModule.curry (dualTensorHom R M (ι →₀ N))) x✝² ∘ₗ Finsupp.lsingle a✝¹) x✝¹) x✝) a✝ =
    ((((AlgebraTensorModule.curry
                (finsuppLinearMap R ∘ₗ
                  Finsupp.mapRange.linearMap (dualTensorHom R M N) ∘ₗ ↑(finsuppRight R R (Dual R M) N ι)))
              x✝² ∘ₗ
            Finsupp.lsingle a✝¹)
          x✝¹)
        x✝)
      a✝
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:
simp [h _]

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

Goal state after:
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
x✝¹ x✝ : M₁
⊢ ((F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f) x✝¹) x✝ = (((F ∘ₗ f).compl₁₂ ↑e ↑e) x✝¹) x✝
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)
⊢ compRight R g ∘ₗ compRight R f = LinearMap.id

Tactic:
ext

Goal state after:
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)
x✝¹ : M →ₗ[R] N
x✝ : M
⊢ ((compRight R g ∘ₗ compRight R f) x✝¹) x✝ = (LinearMap.id x✝¹) x✝
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:
ext

Goal state after:
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
x✝¹ x✝ : M₁
⊢ (((B.compl₁₂ ↑e ↑e).compl₂ (e.symm.conj f)) x✝¹) x✝ = (((B.compl₂ f).compl₁₂ ↑e ↑e) x✝¹) x✝
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:
ext

Goal state after:
ι : 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)
x✝¹ : ι → N
x✝ : ι
⊢ (↑(Finsupp.linearEquivFunOnFinite R N ι) ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R N ι).symm) x✝¹ x✝ = LinearMap.id x✝¹ x✝
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:
ext

Goal state after:
ι : 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
x✝ : M
⊢ ((dualTensorHomEquiv R M N) x✝¹) x✝ = ((dualTensorHomEquivOfBasis b) x✝¹) x✝
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.SeparatingLeft ↔ ∀ (x : M₁), B x = 0 → x = 0

Tactic:
constructor

Goal state after:
case mp
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.SeparatingLeft → ∀ (x : M₁), B x = 0 → x = 0

case mpr
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
⊢ (∀ (x : M₁), B x = 0 → x = 0) → B.SeparatingLeft
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
h : ∀ (x : M₁), B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), (B x) y = 0
⊢ B x = 0

Tactic:
ext

Goal state after:
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
h : ∀ (x : M₁), B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), (B x) y = 0
x✝ : M₂
⊢ (B x) x✝ = 0 x✝
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp' : Projective R (M ⧸ p)
hp : ∀ (x : M), x ∈ p
⊢ p = ⊤

Tactic:
ext

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp' : Projective R (M ⧸ p)
hp : ∀ (x : M), x ∈ p
x✝ : M
⊢ x✝ ∈ p ↔ x✝ ∈ ⊤
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
⊢ (B x) y * (B y) x < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
⊢ (B x) y * (B y) x < (B x) x * (B y) y → LinearIndependent R ![x, y]

case mpr
R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
⊢ LinearIndependent R ![x, y] → (B x) y * (B y) x < (B x) x * (B y) y
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator = W

Tactic:
ext

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
x✝ : V
⊢ x✝ ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator ↔ x✝ ∈ W
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
φ : Dual K V
⊢ W.quotAnnihilatorEquiv (Submodule.Quotient.mk φ) = (dualRestrict W) φ

Tactic:
ext

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
φ : Dual K V
x✝ : ↥W
⊢ (W.quotAnnihilatorEquiv (Submodule.Quotient.mk φ)) x✝ = ((dualRestrict W) φ) x✝
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ ψ : ↥W.dualAnnihilator
h : (fun φ ↦ ⇑↑φ) φ = (fun φ ↦ ⇑↑φ) ψ
⊢ φ = ψ

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ ψ : ↥W.dualAnnihilator
h : (fun φ ↦ ⇑↑φ) φ = (fun φ ↦ ⇑↑φ) ψ
x✝ : M
⊢ ↑φ x✝ = ↑ψ x✝
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ (∃ y, W.mkQ.dualMap y = φ) ↔ φ ∈ W.dualAnnihilator

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ (∃ y, W.mkQ.dualMap y = φ) → φ ∈ W.dualAnnihilator

case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ φ ∈ W.dualAnnihilator → ∃ y, W.mkQ.dualMap y = φ
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
⊢ LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap ⋯ ∘ₗ W.dualCopairing = LinearMap.id

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
x✝¹ : ↥W.dualAnnihilator
x✝ : M
⊢ ↑((LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap ⋯ ∘ₗ W.dualCopairing) x✝¹) x✝ = ↑(LinearMap.id x✝¹) x✝
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
h : (B x) x * (B y) y ≤ (B x) y * (B y) x
⊢ ¬LinearIndependent R ![x, y]

Tactic:
exact not_linearIndependent_of_apply_mul_apply_eq B hp x y (le_antisymm
      (apply_mul_apply_le_of_forall_zero_le B hle x y) h)

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
⊢ W.dualCopairing ∘ₗ LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap ⋯ = LinearMap.id

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
x✝¹ : Dual R (M ⧸ W)
x✝ : M
⊢ ((W.dualCopairing ∘ₗ LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap ⋯) x✝¹ ∘ₗ W.mkQ) x✝ =
    (LinearMap.id x✝¹ ∘ₗ W.mkQ) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Injective ⇑(Hom.hom f)
⊢ f ≫ g = 0

Tactic:
ext

Goal state after:
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Injective ⇑(Hom.hom f)
x✝ : ↑M
⊢ (Hom.hom (f ≫ g)) x✝ = (Hom.hom 0) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Surjective ⇑(Hom.hom g)
⊢ f ≫ g = 0

Tactic:
ext

Goal state after:
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Surjective ⇑(Hom.hom g)
x✝ : ↑M
⊢ (Hom.hom (f ≫ g)) x✝ = (Hom.hom 0) x✝
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ Submodule.dualPairing W = ↑W.quotAnnihilatorEquiv

Tactic:
ext

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
x✝¹ : Dual K V₁
x✝ : ↥W
⊢ ((Submodule.dualPairing W ∘ₗ (dualAnnihilator W).mkQ) x✝¹) x✝ =
    ((↑W.quotAnnihilatorEquiv ∘ₗ (dualAnnihilator W).mkQ) x✝¹) x✝
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (Submodule.dualPairing W).Nondegenerate

Tactic:
constructor

Goal state after:
case left
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (Submodule.dualPairing W).SeparatingLeft

case right
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (Submodule.dualPairing W).SeparatingRight
Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks

Goal state before:
pp: C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ ∀ (s : PullbackCone f g),
    equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ ≫ e ≫ π₁ = s.fst

Tactic:
simp [π₁, e]

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

Goal state before:
pp: C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = s.fst
h₂ : m ≫ e ≫ π₂ = s.snd
⊢ m = equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯

Tactic:
ext

Goal state after:
case h₁
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := ⋯
π₂ : X ⨯ Y ⟶ Y := ⋯
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := ⋯
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = s.fst
h₂ : m ≫ e ≫ π₂ = s.snd
⊢ (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.fst =
    (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ ≫
        equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
      prod.fst

case h₂
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := ⋯
π₂ : X ⨯ Y ⟶ Y := ⋯
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := ⋯
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = s.fst
h₂ : m ≫ e ≫ π₂ = s.snd
⊢ (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.snd =
    (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ ≫
        equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
      prod.snd
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (dualCopairing W).Nondegenerate

Tactic:
constructor

Goal state after:
case left
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (dualCopairing W).SeparatingLeft

case right
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (dualCopairing W).SeparatingRight
Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks

Goal state before:
pp: C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
m : coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt
h₁ : (ι₁ ≫ c) ≫ m = s.inl
h₂ : (ι₂ ≫ c) ≫ m = s.inr
⊢ m = coequalizer.desc (coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)) ⋯

Tactic:
ext

Goal state after:
case h₁
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := ⋯
ι₂ : Z ⟶ Y ⨿ Z := ⋯
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := ⋯
s : PushoutCocone f g
m : coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt
h₁ : (ι₁ ≫ c) ≫ m = s.inl
h₂ : (ι₂ ≫ c) ≫ m = s.inr
⊢ coprod.inl ≫ coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫ m =
    coprod.inl ≫
      coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫
        coequalizer.desc (coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)) ⋯

case h₂
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := ⋯
ι₂ : Z ⟶ Y ⨿ Z := ⋯
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := ⋯
s : PushoutCocone f g
m : coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt
h₁ : (ι₁ ≫ c) ≫ m = s.inl
h₂ : (ι₂ ≫ c) ≫ m = s.inr
⊢ coprod.inr ≫ coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫ m =
    coprod.inr ≫
      coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫
        coequalizer.desc (coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)) ⋯
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: ι : Type u_1
α : Type u_2
F : Type u_3
inst✝¹ : Finite ι
inst✝ : Field F
f : ι → α → F
⊢ {x | ∀ f_1 ∈ Set.range (⇑↑(Finsupp.llift F F F ι) ∘ flip f), f_1 x = 0} = ↑(Finsupp.linearCombination F f).ker

Tactic:
ext

Goal state after:
ι : Type u_1
α : Type u_2
F : Type u_3
inst✝¹ : Finite ι
inst✝ : Field F
f : ι → α → F
x✝ : ι →₀ F
⊢ x✝ ∈ {x | ∀ f_1 ∈ Set.range (⇑↑(Finsupp.llift F F F ι) ∘ flip f), f_1 x = 0} ↔
    x✝ ∈ ↑(Finsupp.linearCombination F f).ker
Module: Mathlib.CategoryTheory.Abelian.Images

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
P Q : C
f : P ⟶ Q
inst✝³ : HasCokernel f
inst✝² : HasKernel f
inst✝¹ : HasKernel (cokernel.π f)
inst✝ : HasCokernel (kernel.ι f)
⊢ kernel.ι f ≫ kernel.lift (cokernel.π f) f ⋯ = 0

Tactic:
ext

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
P Q : C
f : P ⟶ Q
inst✝³ : HasCokernel f
inst✝² : HasKernel f
inst✝¹ : HasKernel (cokernel.π f)
inst✝ : HasCokernel (kernel.ι f)
⊢ (kernel.ι f ≫ kernel.lift (cokernel.π f) f ⋯) ≫ equalizer.ι (cokernel.π f) 0 = 0 ≫ equalizer.ι (cokernel.π f) 0
Module: Mathlib.CategoryTheory.Abelian.Images

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
P Q : C
f : P ⟶ Q
inst✝³ : HasCokernel f
inst✝² : HasKernel f
inst✝¹ : HasKernel (cokernel.π f)
inst✝ : HasCokernel (kernel.ι f)
⊢ cokernel.desc (kernel.ι f) f ⋯ ≫ cokernel.π f = 0

Tactic:
ext

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
P Q : C
f : P ⟶ Q
inst✝³ : HasCokernel f
inst✝² : HasKernel f
inst✝¹ : HasKernel (cokernel.π f)
inst✝ : HasCokernel (kernel.ι f)
⊢ coequalizer.π (kernel.ι f) 0 ≫ cokernel.desc (kernel.ι f) f ⋯ ≫ cokernel.π f = coequalizer.π (kernel.ι f) 0 ≫ 0