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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ pullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≅ pullback f g

Tactic:
by
  refine ?_ ≪≫
    pullbackDiagonalMapIso i (𝟙 _) (f ≫ inv (pullback.fst _ _)) (g ≫ inv (pullback.fst _ _)) ≪≫ ?_
  · refine @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 T) ((pullback.congrHom ?_ ?_).hom) (𝟙 _) ?_ ?_)
      ?_
    · rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_assoc]
    · rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_assoc]
    · rw [Category.comp_id, Category.id_comp]
    · ext <;> simp
    · infer_instance
  · refine @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (pullback.fst _ _) ?_ ?_) ?_
    · rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]
    · rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]
    · infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
X Y : C
X₁ X₂ : J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e : { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := (Functor.const J).map e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := (Functor.const J).map e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
h₂' : IsLimit c₂'
⊢ W.limitsOfShape J (Arrow.hom { left := Y₁, right := Y₂, hom := g })

Tactic:
obtain hg : h₂'.lift (Cone.mk _ (c₁'.π ≫ f)) = g :=
      h₂'.hom_ext (fun j ↦ by
        rw [h₂'.fac]
        simp [reassoc_of% fac, c₁', c₂'])

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
X Y : C
X₁ X₂ : J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e : { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := (Functor.const J).map e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := (Functor.const J).map e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
h₂' : IsLimit c₂'
hg : h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } = g
⊢ W.limitsOfShape J (Arrow.hom { left := Y₁, right := Y₂, hom := g })
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
f : Fin 0 → C
⊢ PreservesColimit (Discrete.functor f) F

Tactic:
let : PreservesColimitsOfShape (Discrete (Fin 0)) F :=
      preservesColimitsOfShape_of_equiv.{0, 0} (Discrete.equivalence finZeroEquiv'.symm) _

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
f : Fin 0 → C
this : PreservesColimitsOfShape (Discrete (Fin 0)) F :=
  preservesColimitsOfShape_of_equiv (Discrete.equivalence finZeroEquiv'.symm) F
⊢ PreservesColimit (Discrete.functor f) F
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.limitsOfShape J = (P.op.colimitsOfShape Jᵒᵖ).unop

Tactic:
by
  ext X
  refine ⟨fun ⟨h⟩ => ⟨?_⟩, fun ⟨h⟩ => ⟨?_⟩⟩
  · exact
      { diag := h.diag.op
        ι := NatTrans.op h.π
        isColimit := isColimitOfUnop h.isLimit
        prop_diag_obj _ := h.prop_diag_obj _ }
  · exact
      { diag := h.diag.unop
        π := NatTrans.unop h.ι
        isLimit := isLimitOfOp h.isColimit
        prop_diag_obj _ := h.prop_diag_obj _ }

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 X : C
inst✝¹ : MonObj M
F : C ⥤ D
inst✝ : F.Monoidal
⊢ F.map 1 = 1

Tactic:
by simp [Hom.one_def]

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 : M ⟶ N
inst✝ : IsMonHom f
X : C
⊢ 1 ≫ f = 1

Tactic:
by simp [Hom.one_def]

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 M.X))) (𝟙 M.X) = η

Tactic:
← yonedaMon_naturality,

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)))) (η ≫ 𝟙 M.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) =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ μ

Tactic:
← yonedaMon_naturality,

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 (M.X ⊗ M.X)))) (μ ≫ 𝟙 M.X) =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : CartesianMonoidalCategory C
M N X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
f : M ⟶ N
inst✝ : IsMonHom f
⊢ 1 ≫ f = 1

Tactic:
by simp [Hom.one_def]

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Bialgebra R A
inst✝ : IsCocomm R A
x✝ : ↑(unop (op (CommAlgCat.of R A)))
⊢ (CommAlgCat.Hom.hom ((β_ (op (CommAlgCat.of R A)) (op (CommAlgCat.of R A))).hom ≫ μ).unop) x✝ =
    (CommAlgCat.Hom.hom μ.unop) x✝

Tactic:
exact comm_comul R _

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
A₁ A₂ A₃ : C
inst✝² : Closed A₁
inst✝¹ : Closed A₂
inst✝ : Closed A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ (conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁)) ((tensoringLeft C).map (f ≫ g)) =
    (conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁)) ((tensoringLeft C).map f ≫ (tensoringLeft C).map g)

Tactic:
(tensoringLeft C).map_comp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
A₁ A₂ A₃ : C
inst✝² : Closed A₁
inst✝¹ : Closed A₂
inst✝ : Closed A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ (conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁)) ((tensoringLeft C).map f ≫ (tensoringLeft C).map g) =
    (conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁)) ((tensoringLeft C).map f ≫ (tensoringLeft C).map g)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ ((𝟭 C).obj y)).inv ≫ (𝟭 C).obj y ◁ id y ≫ (ihom.ev y).app y = uncurry (𝟙 ((ihom x).obj y))

Tactic:
← uncurry_id_eq_ev y y

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ ((𝟭 C).obj y)).inv ≫ (𝟭 C).obj y ◁ id y ≫ uncurry (𝟙 ((ihom y).obj y)) =
    uncurry (𝟙 ((ihom x).obj y))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : Closed X
⊢ curry' (𝟙 X) = id X

Tactic:
by
  dsimp [curry']
  rw [Category.comp_id]
  rfl

Goal state after:
Module: Mathlib.Data.W.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
n : ℕ
t : WType β
h : t.depth ≤ n + 1
⊢ (a : α) × (β a → WType' β n)

Tactic:
obtain ⟨a, f⟩ := t
    have h₀ : ∀ i : β a, WType.depth (f i) ≤ n := fun i =>
      Nat.le_of_lt_succ (lt_of_lt_of_le (WType.depth_lt_depth_mk a f i) h)
    exact ⟨a, fun i : β a => ⟨f i, h₀ i⟩⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
a : ↥(closure s)
x✝ : a ∈ ⊤
⊢ a ∈ rangeOfWType s

Tactic:
by
  rw [← SetLike.mem_coe, ← Subtype.val_injective.mem_set_image]
  change ↑a ∈ map (closure s).subtype _
  refine closure_le.mpr (fun a ha ↦ ?_) a.prop
  exact ⟨⟨a, subset_closure ha⟩, ⟨WType.mk (.inr ⟨a, ha⟩) Empty.rec, rfl⟩, rfl⟩

Goal state after:
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
ι : Type u_2
h : Infinite ι
b : Module.Basis ι K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
have e := (b.constr K (M' := K)).symm

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_2
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[K] ι → K
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

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

Tactic:
by
      rw [whisker_exchange]; monoidal

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 Z : C
inst✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ (ᘁX) X ⊗≫ ((ᘁX ⊗ X) ◁ η_ (ᘁY) Y ≫ (ᘁX ◁ f) ▷ (ᘁY ⊗ Y)) ⊗≫ ᘁX ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ ᘁX ◁ g =
    η_ (ᘁX) X ⊗≫ ᘁX ◁ f ⊗≫ ᘁX ◁ (Y ◁ η_ (ᘁY) Y ⊗≫ ε_ (ᘁY) Y ▷ Y) ⊗≫ ᘁX ◁ g

Tactic:
by
      rw [whisker_exchange]; monoidal

Goal state after:
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
⊢ Y' ◁ η_ Y Y' ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z = (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f

Tactic:
by
      rw [whisker_exchange]; monoidal

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 : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ 𝟙 Y ⊗≫ (Y ◁ η_ X Xᘁ ≫ f ▷ (X ⊗ Xᘁ)) ⊗≫ ε_ X Xᘁ ▷ Xᘁ = f ⊗≫ Xᘁ ◁ η_ X Xᘁ ⊗≫ ε_ X Xᘁ ▷ Xᘁ

Tactic:
by
      rw [whisker_exchange]; monoidal

Goal state after:
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 W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ Module.rank K ↥(comap f p) < ℵ₀

Tactic:
← lift_lt,

Goal state after:
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 W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ lift.{?u.48, v} (Module.rank K ↥(comap f p)) < lift.{?u.48, v} ℵ₀
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)
⊢ Module.rank K (W ⧸ map f p) < ℵ₀

Tactic:
← lift_lt,

Goal state after:
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)
⊢ lift.{?u.54, v'} (Module.rank K (W ⧸ map f p)) < lift.{?u.54, v'} ℵ₀
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✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
x y : M₁
⊢ (B x) y = 0 ↔ (B.flip y) x = 0

Tactic:
flip_apply

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

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

Tactic:
by
    simp_rw [domRestrict₁₂_apply]
    exact H.eq _ _

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

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

Tactic:
flip_apply

Goal state after:
case mp
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I : R₁ →+* R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B.IsAlt
x✝¹ x✝ : M₁
⊢ (B x✝¹) x✝ = -(B x✝) x✝¹
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
⊢ (B.domRestrict₁₂ W W).Nondegenerate

Tactic:
by
  have hB' : (B.domRestrict₁₂ W W).IsRefl := fun x y ↦ hB.isRefl (W.subtype x) (W.subtype y)
  rw [LinearMap.IsRefl.nondegenerate_iff_separatingLeft hB']
  intro ⟨x, hx⟩ hx'
  simp only [Submodule.mk_eq_zero]
  replace hx' : ∀ y ∈ W, B x y = 0 := by simpa [Subtype.forall] using! hx'
  replace hx' : x ∈ W ⊓ ker B := by
    refine ⟨hx, ?_⟩
    ext y
    obtain ⟨u, hu, v, hv, rfl⟩ : ∃ u ∈ W, ∃ v ∈ ker B, u + v = y := by
      rw [← Submodule.mem_sup, hW.sup_eq_top]; exact Submodule.mem_top
    suffices B x u = 0 by rw [mem_ker] at hv; simpa [← hB.eq v, hv]
    exact hx' u hu
  simpa [hW.inf_eq_bot] using! hx'

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

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
hB : ∀ (y : M), (B (v.repr.symm vi)) y = 0
⊢ v.repr.symm vi = 0

Tactic:
rw [LinearEquiv.map_eq_zero_iff]

Goal state after:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
hB : ∀ (y : M), (B (v.repr.symm vi)) y = 0
⊢ vi = 0
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
inst✝¹ : IsReflexive R M
s : Set (M →ₗ[R] R)
inst✝ : Projective R ((M →ₗ[R] R) ⧸ span R s)
h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, f z ≠ 0
⊢ span R s = ⊤

Tactic:
by
  by_contra! hn
  obtain ⟨φ, φne, hφ⟩ := exists_dual_map_eq_bot_of_lt_top hn.lt_top inferInstance
  let φs := (evalEquiv R M).symm φ
  have this f (hf : f ∈ s) : f φs = 0 := by
    rw [← mem_bot R, ← hφ, mem_map]
    exact ⟨f, subset_span hf, (apply_evalEquiv_symm_apply R M f φ).symm⟩
  obtain ⟨x, xs, hx⟩ := h φs (by simp [φne, φs])
  exact hx <| this x xs

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

Goal state before:
pp: case refine_1
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.1 ⟶ c₁.pt

pp: case refine_2
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
⊢ ?refine_1 ≫ s = ?refine_1 ≫ t

Tactic:
· refine t₁.lift (Fan.mk _ fun j => ?_)
      apply q.π.app j

Goal state after:
case refine_2
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
⊢ t₁.lift (Fan.mk q.1 fun j ↦ q.π.app j) ≫ s = t₁.lift (Fan.mk q.1 fun j ↦ q.π.app j) ≫ t
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
  rw [B.nondegenerate_iff hs hB]
  contrapose!
  exact exists_congr fun x ↦ ⟨by aesop, fun ⟨h₀, h⟩ ↦ Or.inl ⟨le_antisymm h (hs x), 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.dualAnnihilator
h : (fun φ ↦ ⇑↑φ) φ = (fun φ ↦ ⇑↑φ) ψ
⊢ φ = ψ

Tactic:
ext
    simp only [funext_iff] at h
    exact h _

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

Goal state before:
pp: case e'_3
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.ker.dualAnnihilator = f.rangeRestrict.ker.dualAnnihilator

Tactic:
· apply congr_arg
    exact (ker_rangeRestrict f).symm

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 W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
⊢ F.ker.dualAnnihilator ≤ dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
← LinearMap.range_dualMap_eq_dualAnnihilator_ker

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
⊢ F.dualMap.range ≤ dualAnnihilator W ⊔ dualAnnihilator W'
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₂
f : V₁ →ₗ[K] V₂
not_surj : f.range < ⊤
inj : Function.Injective ⇑f.dualMap
⊢ False

Tactic:
obtain ⟨φ, φ0, range_le_ker⟩ := (range f).exists_le_ker_of_lt_top not_surj

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₂
f : V₁ →ₗ[K] V₂
not_surj : f.range < ⊤
inj : Function.Injective ⇑f.dualMap
φ : V₂ →ₗ[K] K
φ0 : φ ≠ 0
range_le_ker : f.range ≤ φ.ker
⊢ False
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ (g ≫ Arrow.Hom.left e.hom) ≫ f' = 0

Tactic:
by
    have := Arrow.w e.hom
    dsimp at this
    rw [Category.assoc, this, reassoc_of% hf.w, zero_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X : C
⊢ cokernel.π (diag X) ≫ (asIso (r X)).symm.hom = σ

Tactic:
rw [Iso.symm_hom, asIso_inv]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a - a - (0 - a) = a

Tactic:
rw [sub_sub_sub, sub_zero, sub_self, sub_zero]

Goal state after: