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

Goal state before:
pp: A : Type u_1
inst✝⁶ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁵ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁴ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝³ : Q.IsMultiplicative
inst✝² : W.IsMultiplicative
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
inst✝¹ : Q.RespectsIso
inst✝ : W.RespectsIso
X : MorphismProperty.Comma L R P Q W
⊢ P (X.hom ≫ (𝟙 R).app X.right)

Tactic:
by simpa using X.prop

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
inst✝² : P.RespectsIso
inst✝¹ : Q.RespectsIso
inst✝ : W.RespectsIso
e : R₁ ≅ R₂
X : MorphismProperty.Comma L R₁ P Q W
⊢ P (X.hom ≫ (𝟙 R₁).app X.right)

Tactic:
by simpa using X.prop

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork f g
⊢ c.unop.op.π = c.π

Tactic:
by
  simp [Fork.op_π, Cofork.unop_ι]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
⊢ { l // l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }

Tactic:
refine ⟨p, hp₂, ?_⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
⊢ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = p
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l ≫ a = 𝟙 X
h₂ : l ≫ (IsPullback.cone h).snd = 𝟙 X
⊢ Mono f

Tactic:
← IsIso.eq_comp_inv,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = 𝟙 X ≫ inv a
h₂ : l ≫ (IsPullback.cone h).snd = 𝟙 X
⊢ Mono f
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

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

Tactic:
simp only [condition_assoc, Category.assoc, diagonal_snd, Category.comp_id, limit.lift_π,
          PullbackCone.mk_π_app, limit.lift_π_assoc, cospan_right]

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.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : Mono g
hcomp : P (f ≫ g)
⊢ P f

Tactic:
by
    have : f = (asIso (pullback.fst (f ≫ g) g)).inv ≫ pullback.snd (f ≫ g) g := by
      simp [← cancel_mono g, pullback.condition]
    rw [this, cancel_left_of_respectsIso (P := P)]
    exact P.pullback_snd _ _ hcomp

Goal state after:
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.strictColimitsOfShape J).isoClosure = P.colimitsOfShape J

Tactic:
refine le_antisymm ?_ ?_
  · rw [isoClosure_le_iff]
    apply strictColimitsOfShape_le_colimitsOfShape
  · intro X ⟨h⟩
    have := h.hasColimit
    exact ⟨colimit h.diag, strictColimitsOfShape.colimit h.diag h.prop_diag_obj,
      ⟨h.isColimit.coconePointUniqueUpToIso (colimit.isColimit _)⟩⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f : WithConv (C →ₗ[R] A)
⊢ f * 1 = f

Tactic:
ext; simp [convOne_def, ← map_comp_lTensor]

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
G✝ H✝ H₁ H₂ G H : Grp C
⊢ homMk' (snd G.toMon H.toMon) = (IsTerminal.ofUniqueHom (fun G ↦ homMk' (toUnit G.toMon)) ⋯).from G ▷ H ≫ (λ_ H).hom

Tactic:
by ext; apply snd_def

Goal state after:
Module: Mathlib.Logic.Equiv.Finset

Goal state before:
pp: m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ m_1 ∈ m :: l, n ≤ m_1
h₂ : (m :: l).SortedLT
this : n ≤ m
⊢ raise' (lower' (m :: l) n) n = m :: l

Tactic:
simp [raise', lower', Nat.sub_add_cancel this,
      raise_lower' (fun _ => List.rel_of_pairwise_cons h₂.pairwise : ∀ a ∈ l, m < a)
      h₂.pairwise.of_cons.sortedLT]

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)
inst✝ : Encodable α
h' : (n : ℕ) → Encodable (WType' β n)
f : WType β → (n : ℕ) × WType' β n := fun t ↦ ⟨t.depth, ⟨t, ⋯⟩⟩
finv : (n : ℕ) × WType' β n → WType β := fun p ↦ ↑p.snd
this : ∀ (t : WType β), finv (f t) = t
⊢ Encodable (WType β)

Tactic:
exact Encodable.ofLeftInverse f finv this

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ #(WType (Operands s)) ≤ max #↑s ℵ₀

Tactic:
convert! WType.cardinalMk_le_max_aleph0_of_finite' using 1

Goal state after:
case e'_4
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ max #↑s ℵ₀ = max (lift.{0, u} #(Fin 6 ⊕ ↑s)) ℵ₀

case convert_3
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ ∀ (a : Fin 6 ⊕ ↑s), Finite (Operands s a)
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
b : Basis ι R M
inst✝ : Fintype ι
f : Dual R M
⊢ ∑ x, f (b x) • b.coord x = f

Tactic:
by
  ext m
  simp_rw [LinearMap.sum_apply, LinearMap.smul_apply, smul_eq_mul, mul_comm (f _), ← smul_eq_mul,
    ← f.map_smul, ← map_sum, Basis.coord_apply, Basis.sum_repr]

Goal state after:
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
inst✝ : Finite ι
⊢ b.dualBasis.toDual ∘ₗ b.toDual = Dual.eval R M

Tactic:
by
  refine b.ext fun i => b.dualBasis.ext fun j => ?_
  rw [LinearMap.comp_apply, toDual_apply_left, coe_toDual_self, ← coe_dualBasis,
    Dual.eval_apply, Basis.repr_self, Finsupp.single_apply, dualBasis_apply_self]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
v w : M
i : ι
⊢ (h.coeffs (v + w)) i = (h.coeffs v + h.coeffs w) i

Tactic:
exact (ε i).map_add v w

Goal state after:
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)) ⋯
⊢ Surjective ⇑L

Tactic:
rw [← range_eq_top, eq_top_iff, LinearMap.range_codRestrict, ← map_le_iff_le_comap,
      Submodule.map_top, range_subtype]

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)) ⋯
⊢ (db.coprod eb).ker ≤ (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
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
⊢ IsSimpleOrder (Submodule A V)

Tactic:
refine ⟨fun S => or_iff_not_imp_left.2 fun hn => ?_⟩

Goal state after:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
S : Submodule A V
hn : ¬S = ⊥
⊢ S = ⊤
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝ : FiniteDimensional F E
this : FiniteDimensional F ↥S
⊢ S = ⊥ ∨ S = ⊤

Tactic:
have : finrank F S ≤ 2 := hr ▸ S.toSubmodule.finrank_le

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝¹ : FiniteDimensional F E
this✝ : FiniteDimensional F ↥S
this : finrank F ↥S ≤ 2
⊢ S = ⊥ ∨ S = ⊤
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
s : Finset n
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
this : (B (∑ i ∈ s, w i • v i)) (v i) = 0
j : n
⊢ j ∈ s → j ≠ i → I₁ (w j) • (B (v j)) (v i) = 0

Tactic:
_hj

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
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
this : (B (∑ i ∈ s, w i • v i)) (v i) = 0
j : n
_hj : j ∈ s
⊢ j ≠ i → I₁ (w j) • (B (v j)) (v i) = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case h₀
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
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
j : n
⊢ j ∈ vi.support → j ≠ i → (RingHom.id R) (vi j) • (B (v j)) (v i) = 0

Tactic:
_hj

Goal state after:
case h₀
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
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
j : n
_hj : j ∈ vi.support
⊢ j ≠ i → (RingHom.id R) (vi j) • (B (v j)) (v i) = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ Cofork.π
        ((Cocone.precompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).inv).obj (G.mapCocone (Cofork.ofπ h w))) ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoParallelPair (parallelPair f g ⋙ G)).inv).obj
              (G.mapCocone (Cofork.ofπ h w))).pt).hom =
    (Cofork.ofπ (G.map h) ⋯).π

Tactic:
by
        dsimp only [Cofork.π, Cofork.ofπ_ι_app]
        dsimp; rw [Category.comp_id, Category.id_comp]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
he : (B x) y * (B y) x = (B x) x * (B y) y
⊢ (B x) y • x - (B x) x • y = 0

Tactic:
by_contra hc

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
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
he : (B x) y * (B y) x = (B x) x * (B y) y
hc : ¬(B x) y • x - (B x) x • y = 0
⊢ False
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

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

Tactic:
i.condition_assoc,

Goal state after:
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
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ i.ι ≫ c₁.π.app { as := j₂ } = i.ι ≫ t ≫ c₂.π.app { as := ⟨(j₁, j₂), f⟩ }
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

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

Tactic:
dsimp [P, Q, t, Fan.mk]

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

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

Tactic:
finrank_self

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₁
⊢ 1 = 1
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₁
h : IsCompl W W'
⊢ IsCompl (dualAnnihilator W) (dualAnnihilator W')

Tactic:
rw [isCompl_iff, disjoint_iff, codisjoint_iff] at h ⊢
  rw [← dualAnnihilator_inf_eq, ← dualAnnihilator_sup_eq, h.1, h.2, dualAnnihilator_top,
    dualAnnihilator_bot]
  exact ⟨rfl, rfl⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ kernelComparison f G ≫ kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ =
    G.map (kernel.map f g p q hpq) ≫ kernelComparison g G

Tactic:
kernelComparison_comp_kernel_map

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (kernel.map f g p q ?hpq) ≫ kernelComparison g G = G.map (kernel.map f g p q hpq) ≫ kernelComparison g G

case hpq
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ f ≫ q = p ≫ g
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
c : Cone (parallelPair 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ KernelFork.ofι (𝟙 (G.obj X)) ⋯ ≅ KernelFork.map c G

Tactic:
exact (Fork.ext (G.mapIso (asIso (Fork.ι c))).symm (by simp))

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
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
reassoc' : ∀ {W : C} (h' : R ⟶ W), NormalEpi.g ≫ g ≫ h' = 0 ≫ h'
⊢ NormalEpi.g ≫ g ≫ k = 0

Tactic:
reassoc',

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
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
reassoc' : ∀ {W : C} (h' : R ⟶ W), NormalEpi.g ≫ g ≫ h' = 0 ≫ h'
⊢ 0 ≫ k = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ⋯
Q : C := ⋯
s : Q ⟶ P := ⋯
t : Q ⟶ P := ⋯
I : C := ⋯
i : P ⟶ I := ⋯
⊢ Cofork (G.map s) (G.map t)

Tactic:
refine Cofork.ofπ (G.map i) ?_
      rw [← G.map_comp, ← G.map_comp]
      apply congrArg G.map
      apply coequalizer.condition

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
x : ↑B
⊢ (((Equiv.symm τ).trans (g x)).trans τ) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Tactic:
simp [-MonoidHom.coe_range, τ_symm_apply_fromCoset, g_apply_infinity, τ_apply_infinity]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g₁ : X ⟶ W
inst✝¹ : Epi g₁
g₂ : W ⟶ Z
inst✝ : Mono g₂
hg : g₁ ≫ g₂ = g
f' : W ⟶ Y
hf : g₁ ≫ f' = f
t : PushoutCocone f g
ht : IsColimit t
⊢ Mono t.inl

Tactic:
by
  apply mono_inl_of_isColimit _ _ (PushoutCocone.isColimitOfFactors _ _ _ _ _ hf hg t ht)

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

Goal state before:
pp: 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₂
inst✝ : QuasiIso φ
⊢ QuasiIso (opMap φ)

Tactic:
rw [quasiIso_opMap_iff]
  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 S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₂.LeftHomologyData

Tactic:
let i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
⊢ S₂.LeftHomologyData