mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
⊢ G.map (coequalizer.π f g) ≫
      (PreservesCoequalizer.iso G f g).inv ≫
        colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) ≫ coequalizer.desc h wh =
    q ≫ h

Tactic:
by

Goal state after:
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
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
x : M
⊢ B x = 0 → x = 0 ↔ (B x = 0 ↔ 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✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
⊢ Nondegenerate B ↔ ∀ (x : M), (B x) x = 0 ↔ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f✝ g✝ : X ⟶ Y
h : Y ⟶ Z
w : f✝ ≫ h = g✝ ≫ h
inst✝³ : HasCoequalizer f✝ g✝
inst✝² : HasCoequalizer (G.map f✝) (G.map g✝)
inst✝¹ : PreservesColimit (parallelPair f✝ g✝) G
f g : X ⟶ Y
inst✝ : HasSplitCoequalizer f g
⊢ PreservesColimit (parallelPair f g) G

Tactic:
by

Goal state after:
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
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
x : M
⊢ (B x) x = 0 ∧ x ≠ 0 ∨ (B x) x ≠ 0 ∧ x = 0 → x ≠ 0 ∧ (B x) x ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f✝ g✝ : X ⟶ Y
h : Y ⟶ Z
w : f✝ ≫ h = g✝ ≫ h
inst✝³ : HasCoequalizer f✝ g✝
inst✝² : HasCoequalizer (G.map f✝) (G.map g✝)
inst✝¹ : PreservesColimit (parallelPair f✝ g✝) G
f g : X ⟶ Y
inst✝ : HasSplitEqualizer f g
⊢ PreservesLimit (parallelPair f g) G

Tactic:
by

Goal state after:
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
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
⊢ Nondegenerate B ↔ ∀ (x : M), x ≠ 0 → 0 < (B x) x

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f ↦ F.obj f.fst.2
s t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), s ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.1 } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), t ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.2 }
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
⊢ q.pt ⟶ (buildLimit s t hs ht i).pt

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f ↦ F.obj f.fst.2
s✝ t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), s✝ ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.1 } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), t ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.2 }
i : Fork s✝ t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
s : Cone F
j : J
⊢ hi.lift (Fork.ofι (t₁.lift (Fan.mk s.1 fun j ↦ s.π.app j)) ⋯) ≫ (buildLimit s✝ t hs ht i).π.app j = s.π.app j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f ↦ F.obj f.fst.2
s t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), s ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.1 } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), t ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.2 }
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
m : q.pt ⟶ (buildLimit s t hs ht i).pt
w : ∀ (j : J), m ≫ (buildLimit s t hs ht i).π.app j = q.π.app j
j : Discrete J
⊢ (m ≫ i.ι) ≫ c₁.π.app j = (hi.lift (Fork.ofι (t₁.lift (Fan.mk q.1 fun j ↦ q.π.app j)) ⋯) ≫ i.ι) ≫ c₁.π.app j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : HasLimit (Discrete.functor F.obj)
inst✝¹ : HasLimit (Discrete.functor fun f ↦ F.obj f.fst.2)
inst✝ : HasEqualizers C
⊢ ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    (Pi.lift fun f ↦ limit.π (Discrete.functor F.obj) { as := f.fst.1 } ≫ F.map f.snd) ≫
        (limit.cone (Discrete.functor fun f ↦ F.obj f.fst.2)).π.app { as := f } =
      (limit.cone (Discrete.functor F.obj)).π.app { as := f.fst.1 } ≫ F.map f.snd

Tactic:
by

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

Goal state before:
pp: ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
⊢ K ∈ span 𝕜 (Set.range L)

Tactic:
by

Goal state after:
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
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
⊢ (domRestrict₁₂ B W W).Nondegenerate ↔ Disjoint W (ker B)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : HasLimit (Discrete.functor F.obj)
inst✝¹ : HasLimit (Discrete.functor fun f ↦ F.obj f.fst.2)
inst✝ : HasEqualizers C
⊢ ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    (Pi.lift fun f ↦ limit.π (Discrete.functor F.obj) { as := f.fst.2 }) ≫
        (limit.cone (Discrete.functor fun f ↦ F.obj f.fst.2)).π.app { as := f } =
      (limit.cone (Discrete.functor F.obj)).π.app { as := f.fst.2 }

Tactic:
by

Goal state after:
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 z : M
⊢ 0 ≤ (B z) z

Tactic:
by

Goal state after:
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
⊢ (dualAnnihilator W).dualCoannihilator = W

Tactic:
by

Goal state after:
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
v : V
⊢ (∀ φ ∈ dualAnnihilator W, φ v = 0) ↔ v ∈ W

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ (limit.cone (Discrete.functor fun f ↦ K.obj f.fst.2)).π.app { as := f } =
      (limit.cone (Discrete.functor K.obj)).π.app { as := f.fst.1 } ≫ K.map f.snd

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    t ≫ (limit.cone (Discrete.functor fun f ↦ K.obj f.fst.2)).π.app { as := f } =
      (limit.cone (Discrete.functor K.obj)).π.app { as := f.fst.2 }

Tactic:
by

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

Goal state after:
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
⊢ dualRestrict W ∘ₗ W.dualLift = 1

Tactic:
by

Goal state after:
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
x : Dual K ↥W
⊢ (dualRestrict W) (W.dualLift x) = x

Tactic:
by

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

Goal state after:
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
inst✝ : FiniteDimensional K V
⊢ FiniteDimensional K (Dual K V)

Tactic:
by

Goal state after:
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
⊢ finrank K (Dual K V) = finrank K V

Tactic:
by

Goal state after:
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
inst✝ : FiniteDimensional K V
W : Subspace K V
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V) W

Tactic:
by

Goal state after:
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
inst✝ : FiniteDimensional K V
W : Subspace K V
⊢ finrank K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V

Tactic:
by

Goal state after:
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
inst✝ : FiniteDimensional K V
Φ : Subspace K (Dual K V)
⊢ finrank K ↥(dualCoannihilator Φ) = finrank K ↥(dualAnnihilator Φ)

Tactic:
by

Goal state after:
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
inst✝ : FiniteDimensional K V
W : Subspace K (Dual K V)
⊢ finrank K ↥W + finrank K ↥(dualCoannihilator W) = finrank K V

Tactic:
by

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 ≤ W.dualAnnihilator.subtype.flip.ker

Tactic:
by

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.dualAnnihilator
h : (fun φ ↦ ⇑↑φ) φ = (fun φ ↦ ⇑↑φ) ψ
⊢ φ = ψ

Tactic:
by

Goal state after:
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
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this : r * r * s * s * ((B x) x * (B y) y) = r * r * s * s * ((B x) y * (B y) x)
⊢ r * r * s * s ≠ 0

Tactic:
by

Goal state after:
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
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this : (B (r • x)) (r • x) * (B (s • y)) (s • y) = (B (r • x)) (s • y) * (B (s • y)) (r • x)
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
by

Goal state after:
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
⊢ W.mkQ.dualMap.range = W.dualAnnihilator

Tactic:
by

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
⊢ LinearMap.codRestrict W.dualAnnihilator W.mkQ.dualMap ⋯ ∘ₗ W.dualCopairing = LinearMap.id

Tactic:
by

Goal state after:
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
⊢ (B x) y * (B y) x < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]

Tactic:
by

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

Goal state after:
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
⊢ W.dualAnnihilator = ⊥ ↔ Subsingleton (Dual R (M ⧸ W))

Tactic:
by

Goal state after:
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
hB : IsSymm B
x y : M
⊢ (B x) y ^ 2 < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]

Tactic:
by

Goal state after:
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
inst✝ : Projective R (M ⧸ W)
⊢ W.dualAnnihilator = ⊥ ↔ W = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.FGModuleCat.Colimits

Goal state before:
pp: J✝ : Type
inst✝⁴ : SmallCategory J✝
inst✝³ : FinCategory J✝
k : Type u
inst✝² : Ring k
J : Type
inst✝¹ : Finite J
Z : J → ModuleCat k
inst✝ : ∀ (j : J), Module.Finite k ↑(Z j)
⊢ Module.Finite k ↑(∐ fun j ↦ Z j)

Tactic:
by

Goal state after:
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
inst✝ : Projective R M
⊢ W.dualAnnihilator = ⊤ ↔ W = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.FGModuleCat.Colimits

Goal state before:
pp: J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
k : Type u
inst✝ : Ring k
F : J ⥤ FGModuleCat k
⊢ ModuleCat.isFG k (colimit (F ⋙ forget₂ (FGModuleCat k) (ModuleCat k)))

Tactic:
by

Goal state after:
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 (Dual R M)
⊢ W.quotDualCoannihilatorToDual.Nondegenerate

Tactic:
by

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'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f.range.subtype.dualMap
⊢ Function.Surjective ⇑f.rangeRestrict

Tactic:
by

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'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f.range.subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : f.rangeRestrict.dualMap.range = f.rangeRestrict.ker.dualAnnihilator
⊢ f.dualMap.range = (f.range.subtype ∘ₗ f.rangeRestrict).dualMap.range

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f : M ⟶ N
⊢ ↟(Hom.hom f).ker.subtype ≫ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f : M ⟶ N
s : Fork f 0
c : ↑s.1
⊢ (Hom.hom f) ((Hom.hom s.ι) c) = 0

Tactic:
by

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'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f.range.subtype.dualMap
⊢ f.dualMap.range = f.ker.dualAnnihilator

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f : M ⟶ N
s : Fork f 0
m : s.pt ⟶ (kernelCone f).pt
h : m ≫ Fork.ι (kernelCone f) = s.ι
x : ↑s.pt
⊢ ↑((Hom.hom m) x) = ↑((Hom.hom (↟(LinearMap.codRestrict (Hom.hom f).ker (Hom.hom s.ι) ⋯))) x)

Tactic:
by

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

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
this : finrank K ↥(LinearMap.range f) = 1
⊢ finrank K ↥(LinearMap.ker f) + 1 = finrank K V₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.FGModuleCat.Limits

Goal state before:
pp: J✝ : Type
inst✝⁴ : SmallCategory J✝
inst✝³ : FinCategory J✝
k : Type u
inst✝² : Ring k
J : Type
inst✝¹ : Finite J
Z : J → ModuleCat k
inst✝ : ∀ (j : J), Module.Finite k ↑(Z j)
⊢ Module.Finite k ↑(ModuleCat.of k ((j : J) → ↑(Z j)))

Tactic:
by

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
⊢ finrank K ↥(LinearMap.ker f) + 1 = finrank K V₁

Tactic:
by

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
⊢ finrank K ↥(LinearMap.ker f ⊔ p) = finrank K ↥(LinearMap.ker f) + finrank K ↥p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.FGModuleCat.Limits

Goal state before:
pp: J : Type
inst✝³ : SmallCategory J
inst✝² : FinCategory J
k : Type u
inst✝¹ : Ring k
inst✝ : IsNoetherianRing k
F : J ⥤ FGModuleCat k
⊢ ModuleCat.isFG k (limit (F ⋙ forget₂ (FGModuleCat k) (ModuleCat k)))

Tactic:
by

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
⊢ IsCompl (LinearMap.ker f) p

Tactic:
by

Goal state after:
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)
⊢ IsLimit (KernelFork.ofι f ⋯)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
⊢ p ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f : M ⟶ N
s : Cofork f 0
m : (cokernelCocone f).pt ⟶ s.pt
h : Cofork.π (cokernelCocone f) ≫ m = s.π
⊢ m = ↟((Hom.hom f).range.liftQ (Hom.hom s.π) ⋯)

Tactic:
by

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

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
t : K
hfy : f (t • x) = 0
hpy : t • x ∈ p
⊢ t = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
⊢ Disjoint (LinearMap.ker f) p

Tactic:
by

Goal state after: