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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X : C
h : F.RepresentableBy X
Y : F.Elements
⊢ (ConcreteCategory.hom (F.map (h.homEquiv.symm Y.snd).op)) (initialOfRepresentableBy h).snd = Y.snd

Tactic:
by simp [← h.homEquiv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type u_1
X : C
h : F.CorepresentableBy X
Y : F.Elements
⊢ (ConcreteCategory.hom (F.map (h.homEquiv.symm Y.snd))) (initialOfCorepresentableBy h).snd = Y.snd

Tactic:
by simp [← h.homEquiv_comp]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝¹ : HasCoproduct X
inst✝ : IsIso (Sigma.desc π)
W✝ : C
e : (a : α) → X a ⟶ W✝
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
this : π a = Sigma.ι X a ≫ (asIso (Sigma.desc π)).hom
⊢ π a ≫ (asIso (Sigma.desc π)).inv ≫ Sigma.desc e = e a

Tactic:
rw [this, assoc]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝¹ : HasCoproduct X
inst✝ : IsIso (Sigma.desc π)
W✝ : C
e : (a : α) → X a ⟶ W✝
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
this : π a = Sigma.ι X a ≫ (asIso (Sigma.desc π)).hom
⊢ Sigma.ι X a ≫ (asIso (Sigma.desc π)).hom ≫ (asIso (Sigma.desc π)).inv ≫ Sigma.desc e = e a
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
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesLimit G H
c : Cone (F ⋙ G)
hc : IsLimit c
⊢ Nonempty (IsLimit (H.mapCone c))

Tactic:
by
    refine ⟨isLimitExtendConeEquiv (G := G ⋙ H) F (H.mapCone c) ?_⟩
    let hc' := isLimitOfPreserves H ((isLimitExtendConeEquiv F c).symm hc)
    exact IsLimit.ofIsoLimit hc' (Cone.ext (Iso.refl _) (by simp))

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ : (WithTerminal C)ᵒᵖ
x : WithTerminal C
⊢ (match 𝟙 (op x) with
    | op f =>
      match op x, op x, f, 𝟙 (op x) with
      | op (of x), op (of y), f, x_1 => (down f).op
      | op star, op (of a), x, x_1 =>
        WithInitial.starInitial.to
          (match op (of a) with
          | op x =>
            match x with
            | of x => WithInitial.of (op x)
            | star => WithInitial.star)
      | op star, op star, x, x_1 =>
        𝟙
          (match op star with
          | op x =>
            match x with
            | of x => WithInitial.of (op x)
            | star => WithInitial.star)) =
    𝟙
      (match op x with
      | op x =>
        match x with
        | of x => WithInitial.of (op x)
        | star => WithInitial.star)

Tactic:
cases x <;> rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : WithInitial Cᵒᵖ
⊢ (match x, x, 𝟙 x with
    | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
    | WithInitial.star, WithInitial.of (op unop), x =>
      op
        (starTerminal.from
          (Opposite.unop
            (match WithInitial.of (op unop) with
            | WithInitial.of x => op (of (Opposite.unop x))
            | WithInitial.star => op star)))
    | WithInitial.star, WithInitial.star, x =>
      𝟙
        (match WithInitial.star with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star)) =
    𝟙
      (match x with
      | WithInitial.of x => op (of (unop x))
      | WithInitial.star => op star)

Tactic:
cases x <;> rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ : (WithInitial C)ᵒᵖ
x : WithInitial C
⊢ (match 𝟙 (op x) with
    | op f =>
      match op x, op x, f, 𝟙 (op x) with
      | op (of x), op (of y), f, x_1 => (WithTerminal.down f).op
      | op (of a), op star, x, x_1 =>
        WithTerminal.starTerminal.from
          (match op (of a) with
          | op x =>
            match x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star)
      | op star, op star, x, x_1 =>
        𝟙
          (match op star with
          | op x =>
            match x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star)) =
    𝟙
      (match op x with
      | op x =>
        match x with
        | of x => WithTerminal.of (op x)
        | star => WithTerminal.star)

Tactic:
cases x <;> rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : WithTerminal Cᵒᵖ
⊢ (match x, x, 𝟙 x with
    | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
    | WithTerminal.of (op unop), WithTerminal.star, x =>
      op
        (starInitial.to
          (Opposite.unop
            (match WithTerminal.of (op unop) with
            | WithTerminal.of x => op (of (Opposite.unop x))
            | WithTerminal.star => op star)))
    | WithTerminal.star, WithTerminal.star, x =>
      𝟙
        (match WithTerminal.star with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star)) =
    𝟙
      (match x with
      | WithTerminal.of x => op (of (unop x))
      | WithTerminal.star => op star)

Tactic:
cases x <;> rfl

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

Goal state before:
pp: C₀ : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} C₀
inst✝¹ : Category.{v_2, u_2} C
F : C₀ ⥤ C
X : C
inst✝ : F.Initial
Y : Over X
⊢ IsConnected (CostructuredArrow (CostructuredArrow.toOver F X) Y)

Tactic:
rw [isConnected_iff_of_equivalence
      (CostructuredArrow.costructuredArrowToOverEquivalence F Y)]
    infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i =
    fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯)

Tactic:
conv_rhs => rw [← Category.comp_id (pullback.fst _ _)]
  rw [← diagonal_snd f, pullback.condition_assoc, pullback.lift_snd]

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.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : HasPushout f g], P f → P (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
this : HasPushout f g
e : B' ≅ pushout f g := ⋯.isoPushout
⊢ P f'

Tactic:
rw [← P.cancel_right_of_respectsIso _ e.hom, sq.flip.inr_isoPushout_hom]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : HasPushout f g], P f → P (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
this : HasPushout f g
e : B' ≅ pushout f g := ⋯.isoPushout
⊢ P (pushout.inr f g)
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case refine_2
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)
j : Fin (n + 1)
⊢ ∀ (i : Fin n),
    (extendCofan c₁ c₂).ι.app { as := i.castSucc } ≫
          ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
              (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
        s.ι.app { as := i.castSucc } →
      (extendCofan c₁ c₂).ι.app { as := i.succ } ≫
          ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
              (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
        s.ι.app { as := i.succ }

Tactic:
rintro i -
      dsimp only [extendCofan_ι_app]
      rw [Fin.cases_succ, assoc, (BinaryCofan.IsColimit.desc' t₂ _ _).2.2, t₁.fac]
      rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁✝ : Q ≤ P
h₂✝ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
X Y : Subtype R → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = ↑a
y : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ : (g (h a) h₁).fst = (g r hx).fst ∧ (g (h a) h₁).snd ≍ (g r hx).snd
⊢ (h a).r ≫ (h a).i = r.r ≫ r.i

Tactic:
heq_eq_eq

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁✝ : Q ≤ P
h₂✝ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
X Y : Subtype R → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = ↑a
y : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ : (g (h a) h₁).fst = (g r hx).fst ∧ (g (h a) h₁).snd = (g r hx).snd
⊢ (h a).r ≫ (h a).i = r.r ≫ r.i
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : CartesianMonoidalCategory C
⊢ yonedaMon.essImage = fun F ↦ (F ⋙ forget MonCat).IsRepresentable

Tactic:
ext F
  constructor
  · rintro ⟨M, ⟨α⟩⟩
    exact ⟨M.X, ⟨Functor.representableByEquiv.symm (Functor.isoWhiskerRight α (forget _))⟩⟩
  · rintro ⟨X, ⟨e⟩⟩
    let := MonObj.ofRepresentableBy X F e
    exact ⟨Mon.mk X, ⟨yonedaMonObjIsoOfRepresentableBy X F e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ μ ≫ toUnit A ≫ η = lift (snd A A ≫ ι) (lift (fst A A ≫ ι) (𝟙 (A ⊗ A) ≫ μ) ≫ μ) ≫ μ

Tactic:
rw [← lift_fst_snd, ← lift_lift_assoc (fst A A ≫ _), lift_comp_inv_left, lift_comp_one_left,
    lift_comp_inv_left, comp_toUnit_assoc]

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

Goal state before:
pp: case succ.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          n =
        (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (n + 1) =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (m + 1)
⊢ n + 1 = m + 1

Tactic:
· refine congr_arg Nat.succ (ih ?_)
        simp_all [funext_iff]

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

Goal state before:
pp: case intro.h
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∀ (i : ι), 0 • b.dualBasis i = 0

Tactic:
· intro
    rw [zero_smul]

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

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
V : Type u
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
convert! lift_rank_lt_rank_dual' h; rw [lift_id]

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

Goal state before:
pp: K : Type u
V✝ V₁ V₂ V₃ : Type v
ι : Type w
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V✝
inst✝² : Module K V✝
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
V : Type u₀
x✝¹ : AddCommGroup V
x✝ : Module K V
⊢ ∃ s, #↑s = Module.rank K V ∧ LinearIndepOn K id s

Tactic:
let b := Module.Free.chooseBasis K V
    refine ⟨range b, ?_, b.linearIndependent.linearIndepOn_id⟩
    rw [← lift_injective.eq_iff, mk_range_eq_of_injective b.injective,
      Module.Free.rank_eq_card_chooseBasisIndex]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ (∀ (n m : ℕ) (f : (Fin n → R) →ₗ[R] Fin m → R) (g : (Fin m → R) →ₗ[R] Fin n → R), f ∘ₗ g = 1 → m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n

Tactic:
← toLinearMapRight'.toEquiv
    |>.forall_congr_right,

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      toLinearMapRight'.toEquiv a ∘ₗ toLinearMapRight'.toEquiv a_1 = 1 → m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mpr
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 = -B.flip
x : M₁
h' : (B x) x = ((-B.flip) x) x := congr_fun₂ h x x
⊢ (B x) x = 0

Tactic:
simp only [neg_apply, flip_apply, ← add_eq_zero_iff_eq_neg] at h'

Goal state after:
case mpr
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 = -B.flip
x : M₁
h' : (B x) x + (B x) x = 0
⊢ (B x) x = 0
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 y : M
⊢ (B x) y ^ 2 ≤ (B x) x * (B y) y

Tactic:
rw [show (B x y) ^ 2 = (B x y) * (B y x) by rw [sq, ← hB.eq, RingHom.id_apply]]

Goal state after:
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 y : M
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y
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✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (evalEquiv 𝕜 E).symm φ
i : ι
⊢ (L i) φs ∈ ⊥

Tactic:
rw [← hφ, Submodule.mem_map]

Goal state after:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (evalEquiv 𝕜 E).symm φ
i : ι
⊢ ∃ y ∈ span 𝕜 (Set.range L), φ y = (L i) φs
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:
rw [← LinearMap.comp_apply, dualRestrict_comp_dualLift, End.one_apply]

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:
← W.quotEquivAnnihilator.finrank_eq,

Goal state after:
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 (V ⧸ W) = finrank K V
Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks

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

Tactic:
by simp [ι₂, c]

Goal state after:
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
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ IsLimit (KernelFork.ofι g ⋯)

Tactic:
letI gr := regularOfIsPullbackSndOfRegular hn.regularMono comm t

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
gr : RegularMono g := regularOfIsPullbackSndOfRegular (NormalMono.regularMono h) comm t
⊢ IsLimit (KernelFork.ofι g ⋯)
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'
⊢ IsColimit (CokernelCofork.ofπ f' ⋯)

Tactic:
refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1 hf.isColimit

Goal state after:
case refine_1
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'
⊢ parallelPair g 0 ≅ parallelPair (g ≫ Arrow.Hom.left e.hom) 0

case refine_2
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'
⊢ (Cocone.precompose (Iso.inv ?refine_1)).obj (CokernelCofork.ofπ f ⋯) ≅ CokernelCofork.ofπ f' ⋯
Module: Mathlib.CategoryTheory.Abelian.Images

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

Tactic:
ext
  simp [coimageImageComparison, coimageImageComparison']

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b b' : ↑B
x : X'
y : ↑X
⊢ (b * b') • fromCoset y = b • b' • fromCoset y

Tactic:
change fromCoset _ = fromCoset _
    simp only [leftCoset_assoc]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ QuasiIso φ → IsIso (homologyMap φ)

pp: case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ IsIso (homologyMap φ) → QuasiIso φ

Tactic:
· intro h
    infer_instance

Goal state after:
case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ IsIso (homologyMap φ) → QuasiIso φ
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ IsIso γ.φH → IsIso (h₁.homologyIso.hom ≫ γ.φH ≫ h₂.homologyIso.inv)

Tactic:
· intro h
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ IsIso γ.φH → IsIso (h₁.homologyIso.hom ≫ γ.φH ≫ h₂.homologyIso.inv)

Tactic:
· intro h
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ IsIso γ.left.φH → IsIso γ.left.φH.op

Tactic:
· intro h
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hg : S.g = 0
⊢ h.i ≫ h.liftK (𝟙 S.X₂) ⋯ = 𝟙 h.K

Tactic:
by simp only [← cancel_mono h.i, id_comp, assoc, liftK_i, comp_id]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ homologyMap φ ≫ h₂.homologyIso.hom = h₁.homologyIso.hom ≫ γ.φH

Tactic:
by
  simp only [γ.homologyMap_eq, assoc, Iso.inv_hom_id, comp_id]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ homologyMap φ ≫ h₂.homologyIso.hom = h₁.homologyIso.hom ≫ γ.φH

Tactic:
by
  simp only [γ.homologyMap_eq, assoc, Iso.inv_hom_id, comp_id]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = kernel.lift γ f' ⋯ ≫ kernel.ι γ
⊢ f' ≫ cokernel.π (kernel.ι γ) = 0

Tactic:
rw [hf']

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = kernel.lift γ f' ⋯ ≫ kernel.ι γ
⊢ (kernel.lift γ f' ⋯ ≫ kernel.ι γ) ≫ cokernel.π (kernel.ι γ) = 0