mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝ : LocallySmall.{w, v_1, u_1} C
H₁ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} fun x ↦ Nonempty (F.obj x ≅ Y)
Y : D
⊢ ⊤.map F Y ≤ F.essImage Y

Tactic:
simp [ObjectProperty.map, Functor.essImage]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ (CostructuredArrow.toOver P F X).map (CostructuredArrow.homMk (F.preimage f.left) trivial ⋯) = f

Tactic:
· ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map f.unop.left.op)) ⟨op (unop X).left, yonedaEquiv.toFun (unop X).hom⟩.snd =
    ⟨op (unop Y).left, yonedaEquiv.toFun (unop Y).hom⟩.snd

Tactic:
by simp [yonedaEquiv_naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: case refine_2
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ Type w
inst✝ : EssentiallySmall.{w, v, u} C
P : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} P
hP : ⊤ ≤ P.isoClosure
y : F.Elements
x✝ : ⊤ y
⊢ ObjectProperty.isoClosure (fun x ↦ P x.fst) y

Tactic:
obtain ⟨Z, hZ, ⟨e⟩⟩ := hP y.fst (by simp)
    exact ⟨F.elementsMk Z (F.map e.hom y.snd), hZ,
      ⟨CategoryOfElements.isoMk _ _ e rfl⟩⟩

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

Goal state before:
pp: C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
⊢ IsConnected (StructuredArrow d F)

Tactic:
by
    have : Nonempty (StructuredArrow d F) := by
      have := (I d).inv PUnit.unit
      obtain ⟨j, y, rfl⟩ := Limits.Types.jointly_surjective'.{v, v} this
      exact ⟨StructuredArrow.mk y⟩
    apply zigzag_isConnected
    rintro ⟨⟨⟨⟩⟩, X₁, f₁⟩ ⟨⟨⟨⟩⟩, X₂, f₂⟩
    let y₁ := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁
    let y₂ := colimit.ι (F ⋙ coyoneda.obj (op d)) X₂ f₂
    have e : y₁ = y₂ := by
      apply (I d).toEquiv.injective
      ext
    have t := Types.colimit_eq.{v, v} e
    clear e y₁ y₂
    exact Final.zigzag_of_eqvGen_colimitTypeRel t

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
hf : Surjective ⇑f
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation R B
⊢ (RingHom.ker f.toRingHom).FG

Tactic:
by
  obtain ⟨n, g, hg, _⟩ := FinitePresentation.out (R := R) (A := A)
  convert! (ker_fg_of_mvPolynomial (f.comp g) (hf.comp hg)).map g.toRingHom
  simp_rw [RingHom.ker_eq_comap_bot, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom]
  rw [← Ideal.comap_comap, Ideal.map_comap_of_surjective (g : MvPolynomial (Fin n) R →+* A) hg]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
T : C ⥤ D
inst✝ : T.Initial
S : D ⥤ E
X : E
f : CostructuredArrow S X
⊢ IsConnected (CostructuredArrow (pre T S X) f)

Tactic:
rw [isConnected_iff_of_equivalence (CostructuredArrow.preEquivalence T f)]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
T : C ⥤ D
inst✝ : T.Initial
S : D ⥤ E
X : E
f : CostructuredArrow S X
⊢ IsConnected (CostructuredArrow T f.left)
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂

Tactic:
rw [small_k.w_assoc]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
A B : C
⊢ ∀ (f : A ⟶ B), P f → P.pullbacks f

Tactic:
q

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
A B : C
q : A ⟶ B
⊢ P q → P.pullbacks q
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ (extendFan c₁ c₂).π.app j = s.π.app j
j : Fin n
⊢ m ≫ c₂.snd ≫ c₁.π.app { as := j } = s.π.app { as := j.succ }

Tactic:
← w ⟨j.succ⟩

Goal state after:
case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ (extendFan c₁ c₂).π.app j = s.π.app j
j : Fin n
⊢ m ≫ c₂.snd ≫ c₁.π.app { as := j } = m ≫ (extendFan c₁ c₂).π.app { as := j.succ }
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : ObjectProperty C
inst✝ : Q.IsStableUnderRetracts
h : P ≤ Q
⊢ Q.retractClosure ≤ Q

Tactic:
rw [retractClosure_eq_self]

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

Goal state before:
pp: case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
j : Fin n
⊢ c₁.ι.app { as := j } ≫ c₂.inr ≫ m = s.ι.app { as := j.succ }

Tactic:
← w ⟨j.succ⟩

Goal state after:
case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
j : Fin n
⊢ c₁.ι.app { as := j } ≫ c₂.inr ≫ m = (extendCofan c₁ c₂).ι.app { as := j.succ } ≫ m
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
⊢ (P ⊓ Q).universally = P.universally ⊓ Q.universally

Tactic:
by
  ext X Y f
  change _ ↔ _ ∧ _
  simp_rw [universally, ← forall_and]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ (ConcreteCategory.hom (α.app (op (𝟙_ C)))) η = η

Tactic:
← Category.id_comp η[M.X],

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ (ConcreteCategory.hom (α.app (op (𝟙_ C)))) (𝟙 (𝟙_ C) ≫ η) = η
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommBialgCat R
X✝ Y✝ Z : Type v
inst✝⁵ : CommRing X✝
inst✝⁴ : Bialgebra R X✝
inst✝³ : CommRing Y✝
inst✝² : Bialgebra R Y✝
inst✝¹ : CommRing Z
inst✝ : Bialgebra R Z
X Y : CommBialgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (CommBialgCat R)).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget (CommBialgCat.{u} R)).map f)
    let e : X ≃ₐc[R] Y := { f.hom, i.toEquiv with }
    exact (isoMk e).isIso_hom

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
A B : C
⊢ prodComparison (F ⋙ G) A B = G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B)

Tactic:
unfold prodComparison

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
A B : C
⊢ lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd A B)) =
    G.map (lift (F.map (fst A B)) (F.map (snd A B))) ≫
      lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (F.obj A) (F.obj B)))
Module: Mathlib.RingTheory.Bialgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Semiring C
inst✝² : Bialgebra R C
inst✝¹ : Algebra R A
inst✝ : Algebra R B
h : A →ₐ[R] B
f g : WithConv (C →ₐ[R] A)
⊢ toConv (h.toLinearMap ∘ₗ (toConv f.ofConv.toLinearMap * toConv g.ofConv.toLinearMap).ofConv) =
    toConv (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap

Tactic:
simp [LinearMap.algHom_comp_convMul_distrib, toLinearMap_convMul]

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
⊢ f⁻¹ * f = 1

Tactic:
by
    have H : (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) =
      f.ofConv.comp (lmul' R) := by ext <;> simp
    trans toConv <| ((lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv)).comp
      ((Algebra.TensorProduct.map
      (HopfAlgebra.antipodeAlgHom R A) (.id _ _)).comp (comulAlgHom R A))
    · rw [AlgHom.comp_assoc, ← AlgHom.comp_assoc (Algebra.TensorProduct.map f.ofConv f.ofConv),
        ← Algebra.TensorProduct.map_comp]; rfl
    rw [H, AlgHom.comp_assoc, WithConv.ext_iff, ← AlgHom.toLinearMap_injective.eq_iff]
    change f.ofConv.toLinearMap.comp (toConv (antipode R (A := A)) * toConv LinearMap.id).ofConv =
      ofConv (1 : WithConv <| A →ₗ[R] C)
    rw [LinearMap.antipode_mul_id]
    ext
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
have : Module.rank R (M ⧸ N) ≠ 0 := by
    intro e
    rw [← rank_quotient_add_rank N, e, zero_add] at h
    exact h.ne rfl
  rw [ne_eq, rank_eq_zero_iff, (Submodule.Quotient.mk_surjective N).forall] at this
  push Not at this
  simp_rw [← N.mkQ_apply, ← map_smul, N.mkQ_apply, ne_eq, Submodule.Quotient.mk_eq_zero] at this
  exact this

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

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) ≤ finrank K V

Tactic:
hdisjoint.eq_bot,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
⊢ finrank K ↥(s ⊔ t) + finrank K ↥⊥ ≤ finrank K V
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case neg
K : Type u
inst✝¹ : DivisionRing K
ι : Type u_1
inst✝ : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : ¬Nonempty ι
i x✝ : ι
⊢ (have this := ⋯;
      Basis.empty (ι → K))
      i x✝ =
    b i x✝

Tactic:
exact ((not_nonempty_iff.mp hι).false i).elim

Goal state after:
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K (Dual K V) V (Dual K V)).symm ∘ₗ LinearMap.lTensor (Dual K V) (coevaluation K V))
      ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1) =
    (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V)))
      ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1)

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_toLinearMap]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V))
      ((TensorProduct.assoc K (Dual K V) V (Dual K V)).symm
        ((LinearMap.lTensor (Dual K V) (coevaluation K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1))) =
    (TensorProduct.lid K (Dual K V)).symm
      ((TensorProduct.rid K (Dual K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1))
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V))
      (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j) =
    (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j)

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_toLinearMap]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V))
      ((TensorProduct.assoc K V (Dual K V) V)
        ((LinearMap.rTensor V (coevaluation K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j))) =
    (TensorProduct.rid K V).symm ((TensorProduct.lid K V) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j))
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:
rw [linearIndependent_iff']

Goal state after:
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
⊢ ∀ (s : Finset n) (g : n → K₁), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
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
this : 0 + (B a) b + (B a) c = (B a) c + (B b) c + 0
⊢ (B a) b = (B b) c

Tactic:
zero_add,

Goal state after:
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
this : (B a) b + (B a) c = (B a) c + (B b) c + 0
⊢ (B a) b = (B b) c
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: 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
h : ∀ (x : M₁), B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), (B x) y = 0
h' : B x = 0
⊢ x = 0

Tactic:
exact h x h'

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer

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
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map f ≫ F.map π = F.map g ≫ F.map π

Tactic:
rw [← F.map_comp, q.condition, F.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer

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
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : C ⥤ D
⊢ F.map ι ≫ F.map f = F.map ι ≫ F.map g

Tactic:
rw [← F.map_comp, q.condition, F.map_comp]

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

Goal state before:
pp: K : Type uK
V : Type uV
inst✝¹⁰ : CommSemiring K
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module K V
inst✝⁷ : Projective K V
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : IsReflexive R M
inst✝ : IsReflexive R N
⊢ Bijective ⇑(Dual.eval R (M × N))

Tactic:
by
    let e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
      (dualProdDualEquivDual R M N).dualMap.trans
        (dualProdDualEquivDual R (Dual R M) (Dual R N)).symm
    have : Dual.eval R (M × N) = e.symm.comp ((Dual.eval R M).prodMap (Dual.eval R N)) := by
      ext m f <;> simp [e]
    simp only [this,
      coe_comp, LinearEquiv.coe_coe, EquivLike.comp_bijective]
    exact (bijective_dual_eval R M).prodMap (bijective_dual_eval R N)

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.ker = ⊥ ∧ W.quotDualCoannihilatorToDual.flip.ker = ⊥

Tactic:
ker_eq_bot

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R (Dual R M)
⊢ Function.Injective ⇑W.quotDualCoannihilatorToDual ∧ Function.Injective ⇑W.quotDualCoannihilatorToDual.flip
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:
← (LinearMap.ker f).finrank_quotient_add_finrank,

Goal state after:
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₁ ⧸ LinearMap.ker f) + finrank K ↥(LinearMap.ker f)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₂
⊢ Injective ⇑B.flip ↔ Surjective ⇑B

Tactic:
rw [← dualMap_injective_iff]

Goal state after:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₂
⊢ Injective ⇑B.flip ↔ Injective ⇑B.dualMap
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K v s
⊢ ∃ f, ∀ i ∈ s, f (v i) = 1

Tactic:
replace hli : LinearIndepOn K id (v '' s) := LinearIndepOn.id_image hli

Goal state after:
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
⊢ ∃ f, ∀ i ∈ s, f (v i) = 1
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ Epi (Abelian.factorThruImage f)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
⊢ IsIso (Abelian.factorThruImage f)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ Mono (Abelian.factorThruCoimage f)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Epi f
⊢ IsIso (Abelian.factorThruCoimage f)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ Mono (image.ι f)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ HasImages C

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ HasImageMaps C

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ s.ι ≫ (biprod.fst ≫ f + -biprod.snd ≫ g) = 0

Tactic:
← comp_neg,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ s.ι ≫ (biprod.fst ≫ f + biprod.snd ≫ (-g)) = 0