mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cone D
hc : IsLimit c
j : J
inst✝ : (Over.forget j).Initial
this : Nonempty (Over j)
c'' : Cone
  (Over.lift (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)) :=
  Over.liftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯
⊢ IsLimit (c.overPost j)

Tactic:
letI hc'' : IsLimit c'' :=
    Over.isLimitLiftCone _ _ _ _ _ <| (Functor.Initial.isLimitWhiskerEquiv _ _).symm hc

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cone D
hc : IsLimit c
j : J
inst✝ : (Over.forget j).Initial
this : Nonempty (Over j)
c'' : Cone
  (Over.lift (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)) :=
  Over.liftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯
hc'' : IsLimit c'' :=
  Over.isLimitLiftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯ ((Functor.Initial.isLimitWhiskerEquiv (Over.forget j) c).symm hc)
⊢ IsLimit (c.overPost j)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
S S' X Y : C
f : S' ⟶ S
v₁₂ : X ⟶ S
v₂₂ : Y ⟶ S
g : X ⟶ Y
hv₁₂ : v₁₂ = g ≫ v₂₂
inst✝¹ : HasPullback v₁₂ f
inst✝ : HasPullback v₂₂ f
H : P g
⊢ P (pullback.lift (pullback.fst v₁₂ f ≫ g) (pullback.snd v₁₂ f) ⋯)

Tactic:
subst hv₁₂

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
S S' X Y : C
f : S' ⟶ S
v₂₂ : Y ⟶ S
g : X ⟶ Y
inst✝¹ : HasPullback v₂₂ f
H : P g
inst✝ : HasPullback (g ≫ v₂₂) f
⊢ P (pullback.lift (pullback.fst (g ≫ v₂₂) f ≫ g) (pullback.snd (g ≫ v₂₂) f) ⋯)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_2
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f ∧ Q f
⊢ P (f.comp e.toRingHom) ∧ Q (f.comp e.toRingHom)

Tactic:
exact ⟨hP.2 f e hf.1, hQ.2 f e hf.2⟩

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ ∃ P, Nonempty (A ≃ₐ[R] ↑(FGAlgCatSkeleton.eval R P).obj)

Tactic:
exact ⟨⟨n, RingHom.ker f⟩, ⟨(Ideal.quotientKerAlgEquivOfSurjective hf).symm⟩⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₁₂ : S ⟶ X
v₂₂ : S ⟶ Y
g : Y ⟶ X
hv₁₂ : v₁₂ = v₂₂ ≫ g
inst✝¹ : HasPushout v₁₂ f
inst✝ : HasPushout v₂₂ f
H : P g
⊢ P (pushout.desc (g ≫ pushout.inl v₁₂ f) (pushout.inr v₁₂ f) ⋯)

Tactic:
subst hv₁₂

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₂₂ : S ⟶ Y
g : Y ⟶ X
inst✝¹ : HasPushout v₂₂ f
H : P g
inst✝ : HasPushout (v₂₂ ≫ g) f
⊢ P (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case w₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ (e ≪≫ pullbackDiagonalMapIdIso g (𝟙 X) f ≪≫ asIso (fst g (𝟙 X))).symm.hom ≫
      snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) =
    lift (𝟙 Y) g ⋯

Tactic:
ext <;> simp [e, i]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

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
J : Type u'
inst✝¹ : Category.{v', u'} J
P : ObjectProperty D
inst✝ : P.IsClosedUnderIsomorphisms
e : C ≌ D
⊢ (P.inverseImage e.functor).IsClosedUnderColimitsOfShape J ↔ P.IsClosedUnderColimitsOfShape J

Tactic:
by
  refine ⟨fun H ↦ ?_, fun _ ↦ inferInstance⟩
  convert!
    (inferInstance :
      ((P.inverseImage e.functor).inverseImage e.inverse).IsClosedUnderColimitsOfShape J)
  ext X
  simpa using P.prop_iff_of_iso (e.counitIso.app X).symm

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
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv'.symm 1 ▷ X ≫ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) = (λ_ X).hom

Tactic:
apply α.homEquiv'.injective

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
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv' (α.homEquiv'.symm 1 ▷ X ≫ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))) =
    α.homEquiv' (λ_ X).hom
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
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ X ◁ α.homEquiv'.symm 1 ≫ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) = (ρ_ X).hom

Tactic:
apply α.homEquiv'.injective

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
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv' (X ◁ α.homEquiv'.symm 1 ≫ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))) =
    α.homEquiv' (ρ_ X).hom
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
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ▷ X ≫
      α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) =
    (α_ X X X).hom ≫
      X ◁ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ≫
        α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))

Tactic:
apply α.homEquiv'.injective

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
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv'
      (α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ▷ X ≫
        α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))) =
    α.homEquiv'
      ((α_ X X X).hom ≫
        X ◁ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ≫
          α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)))
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 (M.X ⊗ M.X)))) (lift (fst M.X M.X) (snd M.X M.X) ≫ μ) =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ μ

Tactic:
refine ((α.app _).hom.map_mul _ _).trans ?_

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
⊢ (MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (fst M.X M.X) * (MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (snd M.X M.X) =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ CategoryTheory.inv (CategoryTheory.inv ι) ≫ ι = 𝟙 A

Tactic:
IsIso.inv_inv,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ ι ≫ ι = 𝟙 A
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ ((ρ_ (X ⊗ (ihom X).obj Y)).inv ≫ (α_ X ((ihom X).obj Y) (𝟙_ C)).hom) ≫
      (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫ (ihom.ev X).app Y ▷ 𝟙_ C ≫ (ρ_ Y).hom ≫ f =
    (ihom.ev X).app Y ≫ f

Tactic:
MonoidalCategory.whiskerRight_id_assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ ((ρ_ (X ⊗ (ihom X).obj Y)).inv ≫ (α_ X ((ihom X).obj Y) (𝟙_ C)).hom) ≫
      (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫
        (ρ_ (X ⊗ (ihom X).obj Y)).hom ≫ (ihom.ev X).app Y ≫ (ρ_ Y).inv ≫ (ρ_ Y).hom ≫ f =
    (ihom.ev X).app Y ≫ f
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: case mk
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : Nonempty ((i : α) × (β i → γ) ↪ γ)
⊢ #(WType β) ≤ #γ

Tactic:
obtain ⟨hκ⟩ := hκ

Goal state after:
case mk
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (i : α) × (β i → γ) ↪ γ
⊢ #(WType β) ≤ #γ
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ ((b.constr ℕ) fun w ↦ if w = i then 1 else 0) (b j) = if i = j then 1 else 0

Tactic:
constr_basis b

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ (if j = i then 1 else 0) = if i = j then 1 else 0
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
by
  obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V)
  rw [← b.mk_eq_rank'', aleph0_le_mk_iff] at h
  have e := (b.constr K (M' := K)).symm
  rw [e.rank_eq, e.toEquiv.cardinal_eq]
  apply rank_fun_infinite

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

Goal state before:
pp: case e_a.refine_1
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ (cd.prod (-ce)).ker = ⊥

Tactic:
ker_prod,

Goal state after:
case e_a.refine_1
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ cd.ker ⊓ (-ce).ker = ⊥
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
s t : Submodule R M
⊢ Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)

Tactic:
comap_inf,

Goal state after:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
s t : Submodule R M
⊢ Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype s ⊓ comap s.subtype t) +
        Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: case e_a.refine_2
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
d : V₂
e : V₃
⊢ (d, e) ∈ (db.coprod eb).ker → (d, e) ∈ (cd.prod (-ce)).range

Tactic:
have h := eq₂ d (-e)

Goal state after:
case e_a.refine_2
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
d : V₂
e : V₃
h : db d = eb (-e) → ∃ c, cd c = d ∧ ce c = -e
⊢ (d, e) ∈ (db.coprod eb).ker → (d, e) ∈ (cd.prod (-ce)).range
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✝ : Module.Finite K V
W : Submodule K V
h : W = ⊤
⊢ finrank K ↥W = finrank K V

Tactic:
h,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
h : W = ⊤
⊢ finrank K ↥⊤ = finrank K V
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case refine_1
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank K ↥f.range + finrank K ↥f.ker = finrank K V
h : f.ker = ⊥
⊢ f.range = ⊤

Tactic:
h,

Goal state after:
case refine_1
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank K ↥f.range + finrank K ↥⊥ = finrank K V
h : f.ker = ⊥
⊢ f.range = ⊤
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢ (tensorRightHomEquiv (𝟙_ C) Y Y' Z).symm (η_ Y Y' ≫ f ▷ Y') = η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z

Tactic:
dsimp [tensorRightHomEquiv]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢ (η_ Y Y' ≫ f ▷ Y') ▷ Y ≫ (α_ Z Y' Y).hom ≫ Z ◁ ε_ Y Y' ≫ (ρ_ Z).hom =
    η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case refine_2
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank K ↥f.range + finrank K ↥f.ker = finrank K V
h : f.range = ⊤
⊢ f.ker = ⊥

Tactic:
h,

Goal state after:
case refine_2
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank K ↥⊤ + finrank K ↥f.ker = finrank K V
h : f.range = ⊤
⊢ f.ker = ⊥
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ (tensorRightHomEquiv Y X Xᘁ (𝟙_ C)) (f ▷ X ≫ ε_ X Xᘁ) = 𝟙 Y ⊗≫ (Y ◁ η_ X Xᘁ ≫ f ▷ (X ⊗ Xᘁ)) ⊗≫ ε_ X Xᘁ ▷ Xᘁ

Tactic:
dsimp [tensorRightHomEquiv]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ (ρ_ Y).inv ≫ Y ◁ η_ X Xᘁ ≫ (α_ Y X Xᘁ).inv ≫ (f ▷ X ≫ ε_ X Xᘁ) ▷ Xᘁ =
    𝟙 Y ⊗≫ (Y ◁ η_ X Xᘁ ≫ f ▷ (X ⊗ Xᘁ)) ⊗≫ ε_ X Xᘁ ▷ Xᘁ
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst✝¹ : FiniteDimensional K (V ⧸ p)
inst✝ : FiniteDimensional K (W ⧸ f.range)
⊢ FiniteDimensional K (W ⧸ map f p)

Tactic:
by
  grw [FiniteDimensional, ← rank_lt_aleph0_iff, ← lift_lt, f.lift_rank_quot_map_le p, lift_aleph0]
  apply add_lt_aleph0 <;> rwa [lift_lt_aleph0, rank_lt_aleph0_iff]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : C
p₁ : ExactPairing X Y₁
p₂ : ExactPairing X Y₂
⊢ 𝟙 Xᘁ ≫ 𝟙 Xᘁ = 𝟙 Y₁

Tactic:
rw [← @comp_rightAdjointMate, Category.comp_id, @rightAdjointMate_id]
    rfl

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : C
p₁ : ExactPairing X Y₁
p₂ : ExactPairing X Y₂
⊢ 𝟙 Xᘁ ≫ 𝟙 Xᘁ = 𝟙 Y₂

Tactic:
rw [← @comp_rightAdjointMate, Category.comp_id, @rightAdjointMate_id]
    rfl

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ ModuleCat.isFG R (ModuleCat.of R PUnit.{v + 1})

Tactic:
unfold ModuleCat.isFG

Goal state after:
R : Type u
inst✝ : Ring R
⊢ Module.Finite R ↑(ModuleCat.of R PUnit.{v + 1})
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case neg
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 i' : n
j' : m
hij : ¬(i = i' ∧ j = j')
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'

Tactic:
and_iff_not_or_not,

Goal state after:
case neg
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 i' : n
j' : m
hij : ¬¬(¬i = i' ∨ ¬j = j')
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'
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₁
h : (B x) y = 0
⊢ -(B x) y = 0

Tactic:
h,

Goal state after:
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₁
h : (B x) y = 0
⊢ -0 = 0
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 x)) x✝ + (B' (f' x)) x✝ = (B x) (g x✝) + (B x) (g' x✝)

Tactic:
h,

Goal state after:
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 x) (g x✝) + (B' (f' x)) x✝ = (B x) (g x✝) + (B x) (g' 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
fin : Finite ι ∨ Module.Finite R M
h : Function.Bijective ⇑(dualTensorHom R M N)
⊢ Function.Bijective ⇑(dualTensorHom R M (ι →₀ N))

Tactic:
dualTensorHom_finsupp,

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
fin : Finite ι ∨ Module.Finite R M
h : Function.Bijective ⇑(dualTensorHom R M N)
⊢ Function.Bijective
    ⇑(finsuppLinearMap R ∘ₗ Finsupp.mapRange.linearMap (dualTensorHom R M N) ∘ₗ ↑(finsuppRight R R (Dual R M) N ι))