mathlib-initiative/mathlib-tactics huggingface dataset:
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
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : ∀ a ∈ W, (B x) a = 0
⊢ ⟨x, hx⟩ = 0

Tactic:
specialize h x hx

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
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : (B x) x = 0
⊢ ⟨x, hx⟩ = 0
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✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
⊢ K ∈ span 𝕜 (Set.range L)

Tactic:
by
  have _ := Fintype.ofFinite ι
  let φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
  let p := ⨅ i, ker (L i)
  have p_eq : p = ker φ := (ker_pi L).symm
  let ψ : (E ⧸ p) →ₗ[𝕜] ι → 𝕜 := p.liftQ φ p_eq.le
  have _ : FiniteDimensional 𝕜 (E ⧸ p) := of_injective ψ (ker_eq_bot.1 (ker_liftQ_eq_bot' p φ p_eq))
  let L' i : (E ⧸ p) →ₗ[𝕜] 𝕜 := p.liftQ (L i) (iInf_le _ i)
  let K' : (E ⧸ p) →ₗ[𝕜] 𝕜 := p.liftQ K h
  have : ⨅ i, ker (L' i) ≤ ker K' := by
    simp_rw +zetaDelta [← ker_pi, pi_liftQ_eq_liftQ_pi, ker_liftQ_eq_bot' p φ p_eq]
    exact bot_le
  obtain ⟨c, hK'⟩ :=
    (mem_span_range_iff_exists_fun 𝕜).1 (FiniteDimensional.mem_span_of_iInf_ker_le_ker this)
  refine (mem_span_range_iff_exists_fun 𝕜).2 ⟨c, ?_⟩
  conv_lhs => enter [2]; intro i; rw [← p.liftQ_mkQ (L i) (iInf_le _ i)]
  rw [← p.liftQ_mkQ K h]
  ext x
  convert! LinearMap.congr_fun hK' (p.mkQ x)
  simp only [L', LinearMap.coe_sum, Finset.sum_apply, smul_apply, coe_comp, Function.comp_apply,
    smul_eq_mul]

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

Goal state before:
pp: case mp
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
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
by_cases hr : r = 0

Goal state after:
case pos
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
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : r = 0
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

case neg
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
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x
Module: Mathlib.LinearAlgebra.Dual.Lemmas

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

Tactic:
← (evalEquiv K V₁).toEquiv.surjective_comp

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
b : Basis (↑(hli.extend ⋯)) K V := Basis.mk ⋯ ⋯
i : ι
hi : v i ∈ hli.extend ⋯
⊢ ((b.constr K) 1) (v i) = 1

Tactic:
let ri : hli.extend (Set.subset_univ _) := ⟨v i, hi⟩

Goal state after:
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
b : Basis (↑(hli.extend ⋯)) K V := Basis.mk ⋯ ⋯
i : ι
hi : v i ∈ hli.extend ⋯
ri : ↑(hli.extend ⋯) := ⟨v i, hi⟩
⊢ ((b.constr K) 1) (v i) = 1
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
⊢ coprod.inl ≫ coprod.desc f g ≫ cokernel.π (coprod.desc f g) = coprod.inl ≫ 0

Tactic:
by rw [cokernel.condition]

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
⊢ coprod.inr ≫ coprod.desc f g ≫ cokernel.π (coprod.desc f g) = coprod.inr ≫ 0

Tactic:
by rw [cokernel.condition]

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 φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W'✝ : C
x : W'✝ ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
b : W'✝ ⟶ h.K
hb : b ≫ i = x
⊢ b = h.liftK (x ≫ φ.τ₂) ⋯

Tactic:
rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc,
      hb, liftK_i_assoc, assoc, IsIso.hom_inv_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₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (cyclesMap φ)
h₂ : Epi φ.τ₁
⊢ S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0

Tactic:
simp only [← cancel_epi φ.τ₁, ← toCycles_naturality_assoc,
      IsIso.hom_inv_id_assoc, toCycles_comp_homologyπ, comp_zero]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₂.τ₂ = S₁.g ≫ (-h.h₂) + (-h.h₁) ≫ S₂.f + φ₁.τ₂

Tactic:
by rw [h.comm₂, comp_neg, neg_comp]; abel

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ f ≫ (kernel.ι f.op).unop = 0

Tactic:
← f.unop_op,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ f.op.unop ≫ (kernel.ι f.op.unop.op).unop = 0
Module: Mathlib.CategoryTheory.Abelian.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π f.op).unop ≫ f = 0

Tactic:
← f.unop_op,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π f.op.unop.op).unop ≫ f.op.unop = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₁ ≫ S₁.f ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀

Tactic:
ψ.comm₁₂_assoc

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀
Module: Mathlib.CategoryTheory.Abelian.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ kernel.lift f (cokernel.π f.op).unop ⋯ ≫ (cokernel.desc f.op (kernel.ι f).op ⋯).unop =
    𝟙 (Opposite.unop (cokernel f.op))

Tactic:
rw [← unop_id, ← (kernel.lift f _ _).unop_op, ← unop_comp]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.desc f.op (kernel.ι f).op ⋯ ≫ (kernel.lift f (cokernel.π f.op).unop ⋯).op).unop = (𝟙 (cokernel f.op)).unop
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g

Tactic:
use Limits.prod.lift (factorThru (g ≫ Limits.prod.fst) f) (factorThru (g ≫ Limits.prod.snd) f)
    simp only [prod.comp_lift, comp_factorThru]
    ext
    · simp only [prod.lift_fst]
    · simp only [prod.lift_snd]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f + Hom.τ₂ 0

Tactic:
nullHomotopic_τ₂,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ h₁ ≫ S₂.f + S₁.g ≫ h₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f + Hom.τ₂ 0
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ 0 ≫ H₂.ι = H₁.ι ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯

Tactic:
H₁.ι_descQ_eq_zero_of_boundary (S₁.g ≫ h₂ ≫ H₂.p) (h₂ ≫ H₂.p) rfl,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ 0 ≫ H₂.ι = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' φ₁ h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂

Tactic:
rw [h.eq_add_nullHomotopic, rightHomologyMap'_add, rightHomologyMap'_nullHomotopic, add_zero]

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

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
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : F.PreservesHomology
inst✝² : HasZeroObject C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasCokernels C
this✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this : HasBinaryBiproducts C
⊢ PreservesFiniteColimits F

Tactic:
have : HasCoequalizers C := Preadditive.hasCoequalizers_of_hasCokernels

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : F.PreservesHomology
inst✝² : HasZeroObject C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasCokernels C
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝ : HasBinaryBiproducts C
this : HasCoequalizers C
⊢ PreservesFiniteColimits F
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ S.Exact ↔ imageSubobject S.f = kernelSubobject S.g

Tactic:
by
  rw [exact_iff_isIso_imageToKernel]
  constructor
  · intro
    exact Subobject.eq_of_comm (asIso (imageToKernel _ _ S.zero)) (by simp)
  · intro h
    exact ⟨Subobject.ofLE _ _ h.ge, by ext; simp, by ext; simp⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteProducts C
f : α → C
inst✝¹ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
inst✝ : HasProduct f
⊢ ∀ (j : (Finset (Discrete α))ᵒᵖ),
    (limit.cone (liftToFinsetObj (Discrete.functor f))).π.app j =
      ((liftToFinsetLimitCone (Discrete.functor f)).isLimit.conePointUniqueUpToIso
            (limit.isLimit (Discrete.functor f))).hom ≫
        (finiteSubproductsCone f).π.app j

Tactic:
intro S
    simp only [limit.cone_x, Functor.const_obj_obj, liftToFinsetObj_obj, Discrete.functor_obj_eq_as,
      limit.cone_π, finiteSubproductsCone_pt, finiteSubproductsCone_π_app]
    ext j
    simp only [Discrete.functor_obj_eq_as, Category.assoc, limit.lift_π, Fan.mk_pt, Fan.mk_π_app,
      limit.conePointUniqueUpToIso_hom_comp, liftToFinsetLimitCone_cone_pt, Discrete.mk_as,
      liftToFinsetLimitCone_cone_π_app]
    simp [← limit.w (liftToFinsetObj _)
      (Quiver.Hom.op (homOfLE (x := {j.1}) (y := S.unop) (by simp)))]

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

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel (cokernel.π f) ⟶ A

Tactic:
exact Abelian.monoLift f _ (kernel.condition (cokernel.π f))

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
y y' : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
f : y ⟶ y'
⊢ (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A).map f ≫ (uliftYonedaEquiv (y'.hom ≫ g)).down =
    (uliftYonedaEquiv (y.hom ≫ g)).down ≫
      ((Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E).map f

Tactic:
by
        dsimp
        rw [comp_id, ← CostructuredArrow.w f, assoc, map_comp_uliftYonedaEquiv_down]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
m : (F'.coconeOfIsLeftKanExtension α c).pt ⟶ s.pt
hm : ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ m = s.ι.app j
j : C
this : (F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι).app (L.obj j) ≫ m = s.ι.app (L.obj j)
⊢ α.app j ≫ s.ι.app (L.obj j) = α.app j ≫ (L.whiskerLeft s.ι).app j

Tactic:
whiskerLeft_app

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
m : (F'.coconeOfIsLeftKanExtension α c).pt ⟶ s.pt
hm : ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ m = s.ι.app j
j : C
this : (F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι).app (L.obj j) ≫ m = s.ι.app (L.obj j)
⊢ α.app j ≫ s.ι.app (L.obj j) = α.app j ≫ s.ι.app (L.obj j)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this : m ≫ (F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π).app (L.obj j) = s.π.app (L.obj j)
⊢ s.π.app (L.obj j) ≫ α.app j = (L.whiskerLeft s.π).app j ≫ α.app j

Tactic:
whiskerLeft_app

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this : m ≫ (F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π).app (L.obj j) = s.π.app (L.obj j)
⊢ s.π.app (L.obj j) ≫ α.app j = s.π.app (L.obj j) ≫ α.app j
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
j : P.Elementsᵒᵖ
X : Cᵒᵖ
x : ULift.{w, v₁} (unop X ⟶ unop (unop j).fst)
φ : unop j ⟶ P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x) := ⟨Quiver.Hom.op x.down, ⋯⟩
this :
  uliftYoneda.{w, v₁, u₁}.map x.down ≫ s.ι.app j =
    s.ι.app (op (P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x)))
⊢ uliftYonedaEquiv (s.ι.app (op (P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x)))) =
    (hom ((s.ι.app j).app X)) x

Tactic:
rw [← this, uliftYonedaEquiv_apply]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
j : P.Elementsᵒᵖ
X : Cᵒᵖ
x : ULift.{w, v₁} (unop X ⟶ unop (unop j).fst)
φ : unop j ⟶ P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x) := ⟨Quiver.Hom.op x.down, ⋯⟩
this :
  uliftYoneda.{w, v₁, u₁}.map x.down ≫ s.ι.app j =
    s.ι.app (op (P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x)))
⊢ (hom ((uliftYoneda.{w, v₁, u₁}.map x.down ≫ s.ι.app j).app (op (unop X)))) { down := 𝟙 (unop X) } =
    (hom ((s.ι.app j).app X)) x
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
⊢ (hom ((uliftYonedaMap F X).app (op X))) { down := 𝟙 X } = { down := 𝟙 (F.obj X) }

Tactic:
simp [uliftYonedaMap]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
⊢ IsColimit (coconeπOpCompShrinkYonedaObj F X)

Tactic:
by
  refine Nonempty.some ((Types.isColimit_iff_coconeTypesIsColimit _).2
    ⟨?_, fun x ↦ ?_⟩)
  · let G := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w}.obj X
    let c := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
    have (u : G.ColimitType) (x : F.obj X) (h : G.descColimitType c u = x) :
        G.ιColimitType (op (elementsMk _ _ x))
          (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u := by
      obtain ⟨⟨u⟩, v, rfl⟩ := Functor.ιColimitType_jointly_surjective _ u
      obtain ⟨v, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective v
      dsimp [c] at v h
      simp only [Equiv.apply_symm_apply] at h
      rw [← G.ιColimitType_map (show u ⟶ F.elementsMk _ x from ⟨v, h⟩).op]
      simp [G, shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm.{w}]
    intro u₁ u₂ hu
    generalize hx₁ : G.descColimitType c u₁ = x
    have hx₂ : G.descColimitType c u₂ = x := by rw [← hx₁]; exact hu.symm
    rw [← this _ _ hx₁, ← this _ _ hx₂]
  · exact ⟨Functor.ιColimitType _ (op (elementsMk _ _ x))
      (shrinkYonedaObjObjEquiv.symm (𝟙 X)), by simp⟩

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: 𝕜 : Type ?u.3
inst✝¹ : DivisionRing 𝕜
inst✝ : CharZero 𝕜
n : ℤ
q : 𝕜
hn : n ≠ 0
⊢ n • (q / ↑n) = q

Tactic:
rw [zsmul_eq_mul, (Int.cast_commute n _).eq, div_mul_cancel₀ q (Int.cast_ne_zero.mpr hn)]

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X1 X2 : ExtensionOf i f
x : M
⊢ ↑X1.toLinearPMap ⟨i x, ⋯⟩ = ↑X2.toLinearPMap ⟨i x, ⋯⟩

Tactic:
← X1.is_extension x,

Goal state after:
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
X1 X2 : ExtensionOf i f
x : M
⊢ f x = ↑X2.toLinearPMap ⟨i x, ⋯⟩
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: motive : ℕ → Prop
zero : motive 0
one : motive 1
prime : ∀ (p : ℕ), Prime p → motive p
composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)
n : ℕ
⊢ motive n

Tactic:
by
  refine induction_on_primes zero one ?_ _
  rintro p (_ | _ | a) hp ha
  · simpa
  · simpa using prime _ hp
  · exact composite _ hp.two_le (prime _ hp) _ a.one_lt_succ_succ ha

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case succ
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + n % a + a * i + a) | a.Coprime x}) ≤ φ a * i + φ a + φ a

Tactic:
calc
    #{x ∈ Ico k (k + n % a + a * i + a) | a.Coprime x}
      ≤ #{x ∈ Ico k (k + n % a + a * i) ∪
        Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x} := by
      gcongr
      apply Ico_subset_Ico_union_Ico
    _ ≤ #{x ∈ Ico k (k + n % a + a * i) | a.Coprime x} + a.totient := by
      rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
      apply card_union_le
    _ ≤ a.totient * i + a.totient + a.totient := by grw [← mul_add_one, ih]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, p x
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y

Tactic:
← Filter.eventually_forall_le_atBot

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, ∀ y ≤ x, p y
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k ↦ φ (p ^ k)) = n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)

Tactic:
apply Finsupp.prod_congr _

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ ∀ x ∈ n.factorization.support, φ (x ^ n.factorization x) = x ^ (n.factorization x - 1) * (x - 1)