mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h✝ : Nat.card α ∣ p
h : Nat.card α = p
⊢ IsCyclic α

Tactic:
· exact isCyclic_of_prime_card h

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
g : G
hg : orderOf g = Nat.card G
⊢ ↑⋯.choose = ↑⋯.choose * ↑⋯.choose

Tactic:
← Int.cast_mul,

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
g : G
hg : orderOf g = Nat.card G
⊢ ↑⋯.choose = ↑(⋯.choose * ⋯.choose)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst✝ : MulAction G α
hpα : ¬p ∣ Nat.card α
this : Finite α
⊢ Nonempty ↑(fixedPoints G α)

Tactic:
by
      rw [← Finite.card_pos_iff, pos_iff_ne_zero]
      contrapose hpα
      rw [← Nat.modEq_zero_iff_dvd, ← hpα]
      exact hG.card_modEq_card_fixedPoints α

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
h : IsClopen s
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e)

Tactic:
have ⟨e, f, h⟩ := exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen h

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
h✝ : IsClopen s
e f : R
h : e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h✝ : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
h : b.coeff 0 = 1
this : b.natTrailingDegree = 0
⊢ b.reverse.leadingCoeff = 1

Tactic:
reverse_leadingCoeff,

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h✝ : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
h : b.coeff 0 = 1
this : b.natTrailingDegree = 0
⊢ b.trailingCoeff = 1
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n✝ : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n✝
inst✝ : AddCommMonoid M
n : ℕ
h : ∀ (x : M), (n + 1) • x = 0
h_mod : ∀ (c : ℕ) (x : M), (c % (n + 1)) • x = c • x
this : n + 1 ≠ 0
⊢ Module (ZMod (n + 1)) M

Tactic:
| =>

Goal state after:
n✝ : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n✝
inst✝ : AddCommMonoid M
n : ℕ
h : ∀ (x : M), (n + 1) • x = 0
h_mod : ∀ (c : ℕ) (x : M), (c % (n + 1)) • x = c • x
this : n + 1 ≠ 0
⊢ Module (ZMod (n + 1)) M
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: case mk
G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
g✝ : G ⧸ torsion G
g : G
hne : Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g ≠ 1
hfin : IsOfFinOrder (Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g)
m : ℕ
mpos : 0 < m
hm : Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g ^ m = 1
n : ℕ
npos : 0 < n
hn : (fun x ↦ x ^ m) g ^ n = 1
⊢ Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g = 1

Tactic:
exact (QuotientGroup.eq_one_iff g).mpr
    (isOfFinOrder_iff_pow_eq_one.mpr ⟨m * n, mul_pos mpos npos, (pow_mul g m n).symm ▸ hn⟩)

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ comap (normalizer ↑H).subtype H) % p
⊢ Nat.card (↥(normalizer ↑H) ⧸ comap (normalizer ↑H).subtype H) % p = 0

Tactic:
Nat.mod_eq_zero_of_dvd (dvd_mul_left _ _),

Goal state after:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : 0 = Nat.card (↥(normalizer ↑H) ⧸ comap (normalizer ↑H).subtype H) % p
⊢ Nat.card (↥(normalizer ↑H) ⧸ comap (normalizer ↑H).subtype H) % p = 0
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
⊢ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p = 0

Tactic:
Nat.mod_eq_zero_of_dvd (dvd_mul_left _ _),

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : 0 = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
⊢ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p = 0
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
⊢ ↑((Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ + fun i ↦ ⟨↑(μ i), ⋯⟩) i) = Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)

Tactic:
Pi.add_apply,

Goal state after:
case a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
⊢ ↑(Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ i + ⟨↑(μ i), ⋯⟩) = Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p : ↥((Algebra.lsmul R R M) a).invtSubmodule
f : R[X]
m : M
h : m ∈ ↑p
⊢ ∃ x ∈ ↑p, (of R M a) x = f • (of R M a) m

Tactic:
exact ⟨aeval a f • m, aeval_apply_smul_mem_of_le_comap' h f a p.2, of_aeval_smul a f m⟩

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single.monomial
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ single R' (n✝ + i) (f (a✝ • m)) = Polynomial.map (algebraMap R R') ((monomial n✝) a✝) • (map R' f) (single R i m)

Tactic:
Polynomial.map_monomial,

Goal state after:
case single.monomial
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ single R' (n✝ + i) (f (a✝ • m)) = (monomial n✝) ((algebraMap R R') a✝) • (map R' f) (single R i m)
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Algebra.adjoin R ↑(Finset.image (⇑(monomial 1)) s) = Algebra.adjoin R ↑(Submodule.map (monomial 1) (Ideal.span ↑s))

Tactic:
Finset.coe_image

Goal state after:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Algebra.adjoin R (⇑(monomial 1) '' ↑s) = Algebra.adjoin R ↑(Submodule.map (monomial 1) (Ideal.span ↑s))
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ ⊥.jacobson
hNN : N' ≤ N ⊔ I • N'
⊢ N ⊔ ⊥ • N' = N

Tactic:
bot_smul,

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ ⊥.jacobson
hNN : N' ≤ N ⊔ I • N'
⊢ N ⊔ ⊥ = N
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
⊢ iSup
      ⇑{ toFun := fun n₀ ↦ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)),
          monotone' := ⋯ } =
    F.submodule

Tactic:
dsimp
      rw [← Submodule.span_iUnion, ← submodule_span_single]
      simp [Set.biUnion_le_eq_iUnion]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Projective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
P : ModuleCat R
inst✝⁵ : Small.{v, u} R
inst✝⁴ : CategoryTheory.Projective P
M✝ N✝ : Type v
inst✝³ : AddCommGroup M✝
inst✝² : AddCommGroup N✝
inst✝¹ : Module R M✝
inst✝ : Module R N✝
f : M✝ →ₗ[R] N✝
⊢ ∀ (g : ↑P →ₗ[R] N✝), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g

Tactic:
g

Goal state after:
R : Type u
inst✝⁶ : Ring R
P : ModuleCat R
inst✝⁵ : Small.{v, u} R
inst✝⁴ : CategoryTheory.Projective P
M✝ N✝ : Type v
inst✝³ : AddCommGroup M✝
inst✝² : AddCommGroup N✝
inst✝¹ : Module R M✝
inst✝ : Module R N✝
f : M✝ →ₗ[R] N✝
g : ↑P →ₗ[R] N✝
⊢ Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M✝ N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
α β : relativeDifferentials' φ' ⟶ M
h : Derivation.postcomp (derivation' φ') α = Derivation.postcomp (derivation' φ') β
⊢ α = β

Tactic:
ext1 X

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M✝ N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
α β : relativeDifferentials' φ' ⟶ M
h : Derivation.postcomp (derivation' φ') α = Derivation.postcomp (derivation' φ') β
X : Dᵒᵖ
⊢ α.app X = β.app X
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
s t : M.sections
h : ∀ (X : Cᵒᵖ), ↑s X = ↑t X
⊢ ↑s = ↑t

Tactic:
ext; apply h

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (μ F m' n').app X =
    (μ F m n).app X ≫ (F.map (f ⊗ₘ g)).app X

Tactic:
by
  have := congr_app (μ_natural F f g) X
  dsimp at this
  simpa using this

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m : M
X Y : C
f : X ⟶ (F.obj m).obj Y
inst✝ : F.Monoidal
⊢ (F.obj (𝟙_ M)).map f ≫ (μ F m (𝟙_ M)).app Y = (η F).app X ≫ f ≫ (F.map (ρ_ m).inv).app Y

Tactic:
by
  rw [← cancel_epi ((ε F).app _), ← cancel_mono ((δ F _ _).app _)]
  simp

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

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f g : A ⟶ B
w : (single V c j).map f = (single V c j).map g
⊢ f = g

Tactic:
by
    rw [← cancel_mono (singleObjXSelf c j B).inv,
      ← cancel_epi (singleObjXSelf c j A).hom, ← single_map_f_self,
      ← single_map_f_self, w]

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd' C 0 a a ⋯).hom.app X = (shiftFunctor C a).map ((shiftFunctorZero C A).inv.app X)

Tactic:
by
  simpa using NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd'_zero_add C a)) X

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

Goal state before:
pp: V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
j : α
⊢ 𝟙 (X (j + 1)) ≫ d j = d j

Tactic:
Category.id_comp

Goal state after:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
j : α
⊢ d j = d j
Module: Mathlib.Algebra.Homology.Additive

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹⁰ : Category.{v, u} V
inst✝⁹ : Preadditive V
W : Type u_2
inst✝⁸ : Category.{v_1, u_2} W
inst✝⁷ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁶ : Category.{v_2, u_3} W₁
inst✝⁵ : Category.{v_3, u_4} W₂
inst✝⁴ : HasZeroMorphisms W₁
inst✝³ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f✝ : C ⟶ D
i✝ : ι
F : V ⥤ W
inst✝² : F.Additive
c : ComplexShape ι
inst✝¹ : F.Faithful
inst✝ : F.Full
X Y : HomologicalComplex V c
f : (F.mapHomologicalComplex c).obj X ⟶ (F.mapHomologicalComplex c).obj Y
i j : ι
x✝ : c.Rel i j
⊢ F.preimage (f.f i) ≫ Y.d i j = X.d i j ≫ F.preimage (f.f j)

Tactic:
by
        apply F.map_injective
        simp only [Functor.map_comp, Functor.map_preimage]
        exact f.comm i j

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ 𝟙 X₁ ≫ d₀ = d₀

Tactic:
Category.id_comp

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ d₀ = d₀
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ 𝟙 X₂ ≫ d₁ = d₁

Tactic:
Category.id_comp

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ d₁ = d₁
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ 𝟙 X₁ ≫ d₀ = d₀

Tactic:
Category.id_comp

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ d₀ = d₀
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
n : ℕ
⊢ (mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').X (n + 1 + 2) ≅
    (succ' ((mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d (n + 1 + 1) (n + 1))).fst

Tactic:
exact mkXIso _ _ _ _ _ (succ' d₀).2.2 (fun S => succ' S.f) n

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ homologyMap (φ ≫ ψ) i = homologyMap φ i ≫ homologyMap ψ i

Tactic:
dsimp [homologyMap]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ ≫ ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.homologyMap ((shortComplexFunctor C c i).map ψ)
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ homologyMap (-φ) i = -homologyMap φ i

Tactic:
dsimp [homologyMap]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (-φ)) =
    -ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ)
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ homologyMap (φ + ψ) i = homologyMap φ i + homologyMap ψ i

Tactic:
dsimp [homologyMap]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ + ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ) +
      ShortComplex.homologyMap ((shortComplexFunctor C c i).map ψ)
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ homologyMap (φ - ψ) i = homologyMap φ i - homologyMap ψ i

Tactic:
dsimp [homologyMap]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ - ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ) -
      ShortComplex.homologyMap ((shortComplexFunctor C c i).map ψ)
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ Y✝ : (j : J) → C j
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi W f
⊢ IsIso ((Functor.pi F).map f)

Tactic:
rw [isIso_pi_iff]

Goal state after:
J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ Y✝ : (j : J) → C j
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi W f
⊢ ∀ (i : J), IsIso ((Functor.pi F).map f i)
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k✝ : D ⟶ E
i✝ : ι
e f g : C ⟶ D
h : Homotopy e f
k : Homotopy f g
i j : ι
w : ¬c.Rel j i
⊢ (h.hom + k.hom) i j = 0

Tactic:
Pi.add_apply,

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k✝ : D ⟶ E
i✝ : ι
e f g : C ⟶ D
h : Homotopy e f
k : Homotopy f g
i j : ι
w : ¬c.Rel j i
⊢ (h.hom i + k.hom i) j = 0
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k✝ : D ⟶ E
i✝ : ι
e f g : C ⟶ D
h : Homotopy e f
k : Homotopy f g
i j : ι
w : ¬c.Rel j i
⊢ (h.hom i + k.hom i) j = 0

Tactic:
Pi.add_apply,

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k✝ : D ⟶ E
i✝ : ι
e f g : C ⟶ D
h : Homotopy e f
k : Homotopy f g
i j : ι
w : ¬c.Rel j i
⊢ h.hom i j + k.hom i j = 0
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f₁ g₁ f₂ g₂ : C ⟶ D
h₁ : Homotopy f₁ g₁
h₂ : Homotopy f₂ g₂
i j : ι
hij : ¬c.Rel j i
⊢ (h₁.hom + h₂.hom) i j = 0

Tactic:
Pi.add_apply,

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f₁ g₁ f₂ g₂ : C ⟶ D
h₁ : Homotopy f₁ g₁
h₂ : Homotopy f₂ g₂
i j : ι
hij : ¬c.Rel j i
⊢ (h₁.hom i + h₂.hom i) j = 0
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f₁ g₁ f₂ g₂ : C ⟶ D
h₁ : Homotopy f₁ g₁
h₂ : Homotopy f₂ g₂
i j : ι
hij : ¬c.Rel j i
⊢ (h₁.hom i + h₂.hom i) j = 0

Tactic:
Pi.add_apply,

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f₁ g₁ f₂ g₂ : C ⟶ D
h₁ : Homotopy f₁ g₁
h₂ : Homotopy f₂ g₂
i j : ι
hij : ¬c.Rel j i
⊢ h₁.hom i j + h₂.hom i j = 0