mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : ι →₀ R
i : ι
⊢ (b.toDual (b i)) ((Finsupp.linearCombination R ⇑b) f) = f i

Tactic:
by
  rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum]
  simp_rw [map_smul, toDual_apply, smul_eq_mul, mul_boole, Finset.sum_ite_eq,
    Finsupp.if_mem_support]

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

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

Tactic:
exact lift_rank_lt_rank_dual' h

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

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
h : s ≠ ⊤
⊢ finrank K ↥s < finrank K V

Tactic:
rw [← s.finrank_quotient_add_finrank, add_comm]
  rw [← Quotient.nontrivial_iff] at h
  exact Nat.lt_add_of_pos_right finrank_pos

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⊗ Y ⟶ Z
⊢ (fun f ↦ f ▷ Y ≫ (α_ Z Y' Y).hom ≫ Z ◁ ε_ Y Y' ≫ (ρ_ Z).hom)
      ((fun f ↦ (ρ_ X).inv ≫ X ◁ η_ Y Y' ≫ (α_ X Y Y').inv ≫ f ▷ Y') f) =
    f

Tactic:
calc
      _ = 𝟙 _ ⊗≫ X ◁ η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 _ := by
        monoidal
      _ = 𝟙 _ ⊗≫ X ◁ (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ⊗≫ f := by
        rw [← whisker_exchange]; monoidal
      _ = f := by
        rw [evaluation_coevaluation'']; monoidal

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

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
⊢ W = ⊤ ↔ finrank K ↥W = finrank K V

Tactic:
refine ⟨fun h ↦ by rw [h, finrank_top], fun h ↦ ?_⟩

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
h : finrank K ↥W = finrank K V
⊢ W = ⊤
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
hsum : ∑ j ∈ s, I₁ (w j) • (B (v j)) (v i) = I₁ (w i) • (B (v i)) (v i)
⊢ w i = 0

Tactic:
B.map_sum₂,

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
hsum : ∑ j ∈ s, I₁ (w j) • (B (v j)) (v i) = I₁ (w i) • (B (v i)) (v i)
this : ∑ i_1 ∈ s, (B (w i_1 • v i_1)) (v i) = 0
⊢ w i = 0
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
g : P →ₗ[R] N
comp_eq_id : g ∘ₗ f = LinearMap.id
h : Function.Bijective ⇑(dualTensorHom R M P)
⊢ lTensor (Dual R M) (g ∘ₗ f) = LinearMap.id

Tactic:
comp_eq_id,

Goal state after:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
g : P →ₗ[R] N
comp_eq_id : g ∘ₗ f = LinearMap.id
h : Function.Bijective ⇑(dualTensorHom R M P)
⊢ lTensor (Dual R M) LinearMap.id = LinearMap.id
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 ↥(LinearMap.ker f) + 1 = finrank K V₁

Tactic:
suffices finrank K (LinearMap.range f) = 1 by
    rw [← (LinearMap.ker f).finrank_quotient_add_finrank, add_comm, add_left_inj,
    f.quotKerEquivRange.finrank_eq, this]
  rw [range_eq_top_of_ne_zero hf, finrank_top, finrank_self]

Goal state after:
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₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
y : V₁
hy' : g y = 0
hy : f y = 0
t : K
hz : t • x ∈ p
⊢ f (y + t • x) = g (y + t • x)

Tactic:
simp [h', hy, hy']

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

Goal state before:
pp: 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
          (parallelPair.ext (Iso.refl ((parallelPair g 0).obj WalkingParallelPair.zero)) (Arrow.leftFunc.mapIso e) ⋯
              ⋯).inv).obj
      (CokernelCofork.ofπ f ⋯) ≅
    CokernelCofork.ofπ f' ⋯

Tactic:
· exact Cofork.ext (Arrow.rightFunc.mapIso e) (by simp [Cofork.π])

Goal state after:
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)
⊢ coimage.π f ≫ coimageImageComparison f ≫ image.ι f = f

Tactic:
by
  simp [coimageImageComparison]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ NormalMono.Z u := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
⊢ ((t ≫ kernel.ι g) ≫ i) ≫ h = t ≫ u ≫ h

Tactic:
simp only [u, Category.assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.coimage f
i : Abelian.coimage f ⟶ Q := Abelian.factorThruCoimage f
p : P ⟶ cokernel (kernel.ι f) := cokernel.π (kernel.ι f)
R : C
g : R ⟶ I
hgi : g ≫ i = 0
u : P ⟶ cokernel g := p ≫ cokernel.π g
hu : NormalEpi u
h : NormalEpi.W u ⟶ P := NormalEpi.g
t : cokernel g ⟶ Q
ht : cokernel.π g ≫ t = i
⊢ h ≫ p ≫ cokernel.π g ≫ t = h ≫ u ≫ t

Tactic:
simp only [u, Category.assoc]

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✝² : HasFiniteProducts C
inst✝¹ : HasKernels C
inst✝ : IsNormalMonoCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : equalizer.ι u v ≫ w = 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
hwf : f ≫ w = 0
n : (CokernelCofork.ofπ 0 ⋯).pt ⟶ W
hn : 0 = w
⊢ u = v

Tactic:
have : IsIso (equalizer.ι u v) := by apply isIso_limit_cone_parallelPair_of_eq hn.symm hl

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteProducts C
inst✝¹ : HasKernels C
inst✝ : IsNormalMonoCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : equalizer.ι u v ≫ w = 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
hwf : f ≫ w = 0
n : (CokernelCofork.ofπ 0 ⋯).pt ⟶ W
hn : 0 = w
this : IsIso (equalizer.ι u v)
⊢ u = v
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
⊢ IsLimit (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp)

Tactic:
refine Fork.IsLimit.mk _ (fun s => Fork.ι s ≫ Limits.prod.fst) ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
⊢ ∀ (s : Fork prod.snd 0), (s.ι ≫ prod.fst) ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
⊢ ∀ (s : Fork prod.snd 0) (m : s.pt ⟶ (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp).pt),
    m ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι → m = s.ι ≫ prod.fst
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
inst✝ : Epi f
⊢ ∀ (b : ↑B), ∃ a, (ConcreteCategory.hom f) a = b

Tactic:
by_contra! ⟨b, hb⟩

Goal state after:
A B : GrpCat
f : A ⟶ B
inst✝ : Epi f
b : ↑B
hb : ∀ (a : ↑A), (ConcreteCategory.hom f) a ≠ b
⊢ False
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
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
⊢ LeftHomologyMapData φ h₁ h₂

Tactic:
have commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f' := by
    rw [← cancel_mono h₂.i, assoc, assoc, LeftHomologyData.liftK_i,
      LeftHomologyData.f'_i_assoc, LeftHomologyData.f'_i, φ.comm₁₂]

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
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
⊢ LeftHomologyMapData φ h₁ h₂
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₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃

Tactic:
by
  let γ₁ := leftHomologyMapData φ₁ h₁ h₂
  let γ₂ := leftHomologyMapData φ₂ h₂ h₃
  rw [γ₁.leftHomologyMap'_eq, γ₂.leftHomologyMap'_eq, (γ₁.comp γ₂).leftHomologyMap'_eq,
    LeftHomologyMapData.comp_φH]

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

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✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ leftHomologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapLeftHomologyIso F).hom =
    (S₁.mapLeftHomologyIso F).hom ≫ F.map (leftHomologyMap φ)

Tactic:
by
  dsimp only [leftHomologyMap, mapLeftHomologyIso, LeftHomologyData.leftHomologyIso,
    leftHomologyMapIso', Iso.refl]
  simp only [LeftHomologyData.map_leftHomologyMap', Functor.mapShortComplex_obj,
    ← leftHomologyMap'_comp, comp_id, id_comp]

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

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : (S.map F).HasHomology
⊢ (S.map F).Exact

Tactic:
have := h.hasHomology
  rw [S.leftHomologyData.exact_iff, IsZero.iff_id_eq_zero] at h
  rw [S.leftHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_zero]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
⊢ S.Exact ↔ Mono S.g

Tactic:
constructor
  · intro h
    have := h.hasHomology
    simp only [exact_iff_isZero_homology] at h
    have := S.isIso_pOpcycles hf
    have := mono_of_isZero_kernel' _ S.homologyIsKernel h
    rw [← S.p_fromOpcycles]
    apply mono_comp
  · intro
    rw [(HomologyData.ofIsLimitKernelFork S hf _
      (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι (0 : 0 ⟶ S.X₂) zero_comp)
        inferInstance (isZero_zero C))).exact_iff]
    exact isZero_zero C

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : P.Factors g
⊢ f ≫ P.factorThru g h = P.factorThru (f ≫ g) ⋯

Tactic:
apply (cancel_mono P.arrow).mp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : P.Factors g
⊢ (f ≫ P.factorThru g h) ≫ P.arrow = P.factorThru (f ≫ g) ⋯ ≫ P.arrow
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P Q : MonoOver X
f : P ⟶ Q
h : Subobject.mk P.obj.hom = Subobject.mk Q.obj.hom
⊢ Over.Hom.left f.hom ≫ Subobject.ofMkLEMk Q.obj.hom P.obj.hom ⋯ = 𝟙 P.obj.left

Tactic:
by simp [← cancel_mono P.1.hom]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasCoproducts C
inst✝ : HasStrongEpiMonoFactorisations C
⊢ HasColimitsOfSize.{w, w', max u₁ v₁, max u₁ v₁} (Subobject X)

Tactic:
by
  apply hasColimitsOfSize_thinSkeleton

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
tfae_2_to_1 :
  (∀ (S : ShortComplex C), S.Exact → (S.map F).Exact) → ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact,
      F.PreservesHomology, PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE

Tactic:
tfae_have 3 → 4
  | h => ⟨preservesFiniteLimits_of_preservesHomology F,
      preservesFiniteColimits_of_preservesHomology F⟩

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
tfae_2_to_1 :
  (∀ (S : ShortComplex C), S.Exact → (S.map F).Exact) → ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
tfae_3_to_4 : F.PreservesHomology → PreservesFiniteLimits F ∧ PreservesFiniteColimits F
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact,
      F.PreservesHomology, PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X Y : C
f : X ⟶ Y
s : yoneda.obj X ⟶ A
t : yoneda.obj Y ⟶ A
hst : yoneda.map f ≫ t = s
u : F.obj (op Y)
h : MakesOverArrow η t u
⊢ (ConcreteCategory.hom (η.app (op X))) ((ConcreteCategory.hom (F.map f.op)) u) = yonedaEquiv s

Tactic:
simp [h.app, yonedaEquiv_naturality, hst]

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

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : Category.{v_4, u_4} D
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝² : F'.IsLeftKanExtension α
inst✝¹ : HasColimit F
inst✝ : HasColimit F'
i : C
⊢ α.app i ≫ colimit.ι F' (L.obj i) ≫ (F'.colimitIsoOfIsLeftKanExtension α).hom = colimit.ι F i

Tactic:
by
  simp [colimitIsoOfIsLeftKanExtension]

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✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : ℰ
f : P ⟶ Q
g : Q ⟶ (restrictedULiftYoneda A).obj X
⊢ (restrictedULiftYonedaHomEquiv L α P X).symm (f ≫ g) = L.map f ≫ (restrictedULiftYonedaHomEquiv L α Q X).symm g

Tactic:
apply (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P).hom_ext

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : ℰ
f : P ⟶ Q
g : Q ⟶ (restrictedULiftYoneda A).obj X
⊢ ∀ (j : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P),
    ((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫ (restrictedULiftYonedaHomEquiv L α P X).symm (f ≫ g) =
      ((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫ L.map f ≫ (restrictedULiftYonedaHomEquiv L α Q X).symm g
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✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X Y : ℰ
f : L.obj P ⟶ X
g : X ⟶ Y
this :
  ∀ {W W' : ℰ}
    (f :
      CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
        (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj W)
    (g : W ⟶ W'),
    (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm
        (f ≫ (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).map g) =
      (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm f ≫ g
⊢ (restrictedULiftYonedaHomEquiv L α P Y).symm ((restrictedULiftYonedaHomEquiv L α P Y) (f ≫ g)) =
    (restrictedULiftYonedaHomEquiv L α P Y).symm
      ((restrictedULiftYonedaHomEquiv L α P X) f ≫ (restrictedULiftYoneda A).map g)

Tactic:
apply (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P).hom_ext

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X Y : ℰ
f : L.obj P ⟶ X
g : X ⟶ Y
this :
  ∀ {W W' : ℰ}
    (f :
      CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
        (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj W)
    (g : W ⟶ W'),
    (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm
        (f ≫ (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).map g) =
      (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm f ≫ g
⊢ ∀ (j : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P),
    ((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫
        (restrictedULiftYonedaHomEquiv L α P Y).symm ((restrictedULiftYonedaHomEquiv L α P Y) (f ≫ g)) =
      ((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫
        (restrictedULiftYonedaHomEquiv L α P Y).symm
          ((restrictedULiftYonedaHomEquiv L α P X) f ≫ (restrictedULiftYoneda A).map g)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ IsDetector (unop G) ↔ IsCodetector G

Tactic:
by
  rw [IsDetector, IsCodetector, ← isDetecting_unop_iff, unop_singleton]

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

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.g.app k)) ((ConcreteCategory.hom (S.X₂.map e₁)) y) = 0
t : ↑(S.map ((evaluation J AddCommGrpCat).obj k)).X₁
ht : (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj k)).f) t = (ConcreteCategory.hom (S.X₂.map e₁)) y
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range

Tactic:
use colimit.ι S.X₁ k t

Goal state after:
case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.g.app k)) ((ConcreteCategory.hom (S.X₂.map e₁)) y) = 0
t : ↑(S.map ((evaluation J AddCommGrpCat).obj k)).X₁
ht : (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj k)).f) t = (ConcreteCategory.hom (S.X₂.map e₁)) y
⊢ (AddCommGrpCat.Hom.hom (S.map colim).f) ((ConcreteCategory.hom (colimit.ι S.X₁ k)) t) =
    (ConcreteCategory.hom (colimit.ι S.X₂ j)) y
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case mp
n : ℤ
⊢ n.negOnePow = -1 → Odd n

Tactic:
intro h
    rw [← Int.not_even_iff_odd]
    intro h'
    rw [negOnePow_even _ h'] at h
    contradiction

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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r r' : R
eq1 : r • y = r' • y
⊢ (extendIdealTo i f h y) r = (extendIdealTo i f h y) r'

Tactic:
by
  rw [← sub_eq_zero, ← map_sub]
  convert! ExtensionOfMaxAdjoin.extendIdealTo_wd' i f h (r - r') _
  rw [sub_smul, sub_eq_zero, eq1]

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a b : ℕ
⊢ (range (a + b)).val = (range a).val ∪ (map (addLeftEmbedding a) (range b)).val

Tactic:
exact Multiset.range_add_eq_union a b

Goal state after:
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case basic
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s✝ : Set α
h : s✝ ∈ insert A S
⊢ s✝ ∈ S ∨ ∃ Q ∈ S, s✝ = A ∩ Q

Tactic:
| basic h =>

Goal state after: