mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Flat
hg : g.Flat
⊢ (g.comp f).Flat

Tactic:
algebraize [f, g, (g.comp f)]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Flat
hg : g.Flat
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.Flat R S
algebraizeInst✝ : Module.Flat S T
⊢ (g.comp f).Flat
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S T : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Flat
hg : g.Flat
⊢ (g.comp f).Flat

Tactic:
exact hf.comp hg

Goal state after:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case succ.inr
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
⊢ D (a ^ (n + 1)) = (n + 1) • a ^ (n + 1 - 1) • D a

Tactic:
have : a * a ^ (n - 1) = a ^ n := by rw [← pow_succ', Nat.sub_add_cancel hpos]
      simp only [pow_succ', leibniz, ihn, smul_comm a n (_ : M), smul_smul a, add_smul, this,
        Nat.add_succ_sub_one, add_zero, one_nsmul]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
| Ideal.span (Set.range Subtype.val) = ⊤

Tactic:
← iSup_basicOpen_eq_top_iff

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
| ⨆ i, basicOpen ↑i = ⊤
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ Injective
    ⇑(QuotientAddGroup.map (zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ⋯)

Tactic:
rw [← ker_eq_bot_iff, eq_bot_iff]
            refine fun q => induction_on q fun n hn => ?_
            rw [mem_bot, eq_zero_iff, Int.mem_zmultiples_iff, ←
              zsmul_vadd_eq_iff_minimalPeriod_dvd]
            exact (eq_zero_iff _).mp hn

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsCompact s ∧ IsOpen s ↔ ∃ I, I.FG ∧ (zeroLocus ↑I)ᶜ = s

Tactic:
by
  rw [isCompact_isOpen_iff]
  exact ⟨fun ⟨s, e⟩ ↦ ⟨.span s, ⟨s, rfl⟩, by simpa using e⟩,
    fun ⟨I, ⟨s, hs⟩, e⟩ ↦ ⟨s, by simpa [hs.symm] using e⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
⊢ (m ^ univ.lcm fun x ↦ exponent (M x)) = 1

Tactic:
ext i

Goal state after:
case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ (m ^ univ.lcm fun x ↦ exponent (M x)) i = 1 i
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal '' irreducibleComponents (PrimeSpectrum R) = minimalPrimes R

Tactic:
rw [irreducibleComponents_eq_maximals_closed, minimalPrimes_eq_minimals,
    image_antitone_setOfPred_maximal (fun s t hs _ ↦ (vanishingIdeal_anti_mono_iff hs.1).symm),
    ← funext (@Set.mem_ofPred_eq _ · Ideal.IsPrime), ← vanishingIdeal_isClosed_isIrreducible]
  rfl

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

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
⊢ a * b = b * a

Tactic:
let ⟨⟨x, y, (hxy : f y = x)⟩, (hx : ∀ a : f.range, a ∈ zpowers _)⟩ :=
    IsCyclic.exists_generator (α := f.range)

Goal state after:
G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
⊢ a * b = b * a
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr
A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
h_ne : g ≠ 0
this :
  ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_1 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A),
    (Function.Surjective fun x ↦ x • g) → g ≠ 0 → 0 < g → Nonempty (A ≃+o ℤ)
hg' : ¬0 < g
⊢ Nonempty (A ≃+o ℤ)

pp: A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
h_ne : g ≠ 0
hg' : 0 < g
⊢ Nonempty (A ≃+o ℤ)

Tactic:
· exact this (g := -g) (by simpa using! neg_surjective.comp hs) (by grind) (by grind)

Goal state after:
A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
h_ne : g ≠ 0
hg' : 0 < g
⊢ Nonempty (A ≃+o ℤ)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_exp : exponent α = p
h_cyc : IsCyclic α
⊢ False

Tactic:
obtain (rfl | rfl) := eq_zero_or_one_of_sq_eq_self <| hα ▸ h_exp ▸ (h_cyc.exponent_eq_card).symm
    · exact Nat.not_prime_zero hp
    · exact Nat.not_prime_one hp

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
h : IsCyclic G
⊢ Nat.card (MulAut G) = (Nat.card G).totient

Tactic:
← ZMod.card_units_eq_totient,

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
h : IsCyclic G
⊢ Nat.card (MulAut G) = Fintype.card (ZMod (Nat.card G))ˣ
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
⊢ ↑P ≠ ⊥

Tactic:
refine fun h => hp.out.not_dvd_one ?_

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
h : ↑P = ⊥
⊢ p ∣ 1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hn : (normalizer ↑P).Normal
⊢ (↑P).Normal

Tactic:
rw [← normalizer_eq_top_iff, ← normalizer_sup_eq_top' P le_normalizer, P.coe_coe, sup_idem]

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSemisimpleModule R ↥N
⊢ N = ⊥ ∨ ∃ m ≤ N, IsSimpleModule R ↥m

Tactic:
rw [← N.subsingleton_iff_eq_bot, ← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top]

Goal state after:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSemisimpleModule R ↥N
⊢ ⊥ = ⊤ ∨ ∃ m ≤ N, IsSimpleModule R ↥m
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι✝ : Type u_1
R : Type u_2
S : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
M✝ : Type u_4
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R M✝
m : Submodule R M✝
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type u_7
M : ι → Type u_6
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), IsSemisimpleModule R (M i)
⊢ IsSemisimpleModule R (Π₀ (i : ι), M i)

Tactic:
by
  classical
  exact isSemisimpleModule_of_isSemisimpleModule_submodule'
    (fun _ ↦ .range _) DFinsupp.iSup_range_lsingle

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

Goal state before:
pp: ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hv : iSupIndep fun i ↦ R ∙ v i
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
⊢ LinearIndependent R v

Tactic:
refine linearIndependent_iff_eq_zero_of_smul_mem_span.mpr fun i r hi => ?_
  replace hv := iSupIndep_def.mp hv i
  simp only [iSup_subtype', ← Submodule.span_range_eq_iSup (ι := Subtype _), disjoint_iff] at hv
  have : r • v i ∈ (⊥ : Submodule R M) := by
    rw [← hv, Submodule.mem_inf]
    refine ⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, ?_⟩
    convert! hi
    ext
    simp
  rw [← Submodule.mem_bot R, ← h_ne_zero i]
  simpa using this

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
this : Ideal.span s ≤ Ideal.torsionOf R M x
⊢ ∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0

Tactic:
rintro ⟨a, ha⟩
    exact this ha

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

Goal state before:
pp: R : Type u_3
A : Type u_1
M : Type u_2
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
inst✝ : FaithfulSMul A M
p : R[X]
⊢ (∀ (m : AEval R M a), p • m = 0) ↔ (aeval a) p = 0

Tactic:
change (∀ m : M, aeval a p • m = 0) ↔ _

Goal state after:
R : Type u_3
A : Type u_1
M : Type u_2
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
inst✝ : FaithfulSMul A M
p : R[X]
⊢ (∀ (m : M), (aeval a) p • m = 0) ↔ (aeval a) p = 0
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type u_3
A : Type u_1
M : Type u_2
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
inst✝ : FaithfulSMul A M
p : R[X]
⊢ (∀ (n : AEval R M a), p • n = 0) ↔ (aeval a) p = 0

Tactic:
change (∀ m : M, aeval a p • m = 0) ↔ _

Goal state after:
R : Type u_3
A : Type u_1
M : Type u_2
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
inst✝ : FaithfulSMul A M
p : R[X]
⊢ (∀ (m : M), (aeval a) p • m = 0) ↔ (aeval a) p = 0
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
r : R[X]
n : ℕ
a : R
⊢ (toFinsuppIso R).symm (AddMonoidAlgebra.coeffAddEquiv.symm (coeffAddEquiv (r • single R n a))) =
    r * (toFinsuppIso R).symm (AddMonoidAlgebra.coeffAddEquiv.symm (coeffAddEquiv (single R n a)))

Tactic:
ext i

Goal state after:
case single
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
r : R[X]
n : ℕ
a : R
i : ℕ
⊢ ((toFinsuppIso R).symm (AddMonoidAlgebra.coeffAddEquiv.symm (coeffAddEquiv (r • single R n a)))).coeff i =
    (r * (toFinsuppIso R).symm (AddMonoidAlgebra.coeffAddEquiv.symm (coeffAddEquiv (single R n a)))).coeff i
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x : M
⊢ 0 ∈ N

Tactic:
exact N.zero_mem

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
h : I ≠ ⊤
x✝ : ℕ
⊢ I ^ x✝ = I ^ x✝ • ⊤

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
h : I ≠ ⊤
x✝ : ℕ
i : R
⊢ i ∈ I ^ x✝ ↔ i ∈ I ^ x✝ • ⊤
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: α : Type u_1
inst✝¹ : AddRightCancelSemigroup α
inst✝ : DecidableEq α
a x✝¹ x✝ : α
⊢ Decidable ((up' a).Rel x✝¹ x✝)

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
w : (total β C).map f = (total β C).map g
⊢ f = g

Tactic:
ext i

Goal state after:
β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
w : (total β C).map f = (total β C).map g
i : β
⊢ f i = g i
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 : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ (if i = j then X✝ else 0) = X✝

Tactic:
rw [if_pos h]

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 : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ { X := fun i ↦ if i = j then X✝ else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i = X✝

Tactic:
by dsimp; rw [if_pos h]

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 : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ Y✝ = if i = j then Y✝ else 0

Tactic:
rw [if_pos h]

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 : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ Y✝ = { X := fun i ↦ if i = j then Y✝ else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i

Tactic:
by dsimp; rw [if_pos h]

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 ι
K : HomologicalComplex V c
j : ι
A : V
f g : (single V c j).obj A ⟶ K
hfg : f.f j = g.f j
⊢ f = g

Tactic:
ext i

Goal state after:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : (single V c j).obj A ⟶ K
hfg : f.f j = g.f j
i : ι
⊢ f.f i = g.f i
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 ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
⊢ f = g

Tactic:
ext i

Goal state after:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
i : ι
⊢ f.f i = g.f i
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Mono (φ.f i)
Z✝ : HomologicalComplex V c
g h : Z✝ ⟶ K
eq : g ≫ φ = h ≫ φ
⊢ g = h

Tactic:
ext i

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Mono (φ.f i)
Z✝ : HomologicalComplex V c
g h : Z✝ ⟶ K
eq : g ≫ φ = h ≫ φ
i : ι
⊢ g.f i = h.f i
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z✝ : HomologicalComplex V c
g h : L ⟶ Z✝
eq : φ ≫ g = φ ≫ h
⊢ g = h

Tactic:
ext i

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z✝ : HomologicalComplex V c
g h : L ⟶ Z✝
eq : φ ≫ g = φ ≫ h
i : ι
⊢ g.f i = h.f i
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
⊢ shiftFunctorAdd' C 0 a a ⋯ =
    (shiftFunctor C a).leftUnitor.symm ≪≫ isoWhiskerRight (shiftFunctorZero C A).symm (shiftFunctor C a)

Tactic:
by
  ext X
  dsimp [shiftFunctorAdd', shiftFunctorZero, shiftFunctor]
  simp only [eqToHom_app, obj_ε_app, Discrete.addMonoidal_leftUnitor, eqToIso.inv,
    eqToHom_map, Category.id_comp]
  rfl

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C X✝ Y✝ : HomologicalComplex V c
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (forget V c).map a₁✝ = (forget V c).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext i

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C X✝ Y✝ : HomologicalComplex V c
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (forget V c).map a₁✝ = (forget V c).map a₂✝
i : ι
⊢ a₁✝.f i = a₂✝.f i
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
⊢ { f := fun i ↦ (f i).hom, comm' := hf } ≫ { f := fun i ↦ (f i).inv, comm' := ⋯ } = 𝟙 C₁

Tactic:
ext i

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ ({ f := fun i ↦ (f i).hom, comm' := hf } ≫ { f := fun i ↦ (f i).inv, comm' := ⋯ }).f i = (𝟙 C₁).f i
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
⊢ { f := fun i ↦ (f i).inv, comm' := ⋯ } ≫ { f := fun i ↦ (f i).hom, comm' := hf } = 𝟙 C₂

Tactic:
ext i

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ ({ f := fun i ↦ (f i).inv, comm' := ⋯ } ≫ { f := fun i ↦ (f i).hom, comm' := hf }).f i = (𝟙 C₂).f i
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ m + -m = 0

Tactic:
add_neg_cancel

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ m + -m = 0

Tactic:
add_neg_cancel

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ 0 = 0
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 : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
⊢ { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ } ≫
      { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ } =
    𝟙 ((single W₁ c j ⋙ F.mapHomologicalComplex c).obj X)

Tactic:
ext i

Goal state after:
ι : 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✝ : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
i : ι
⊢ ({ f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ } ≫
          { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }).f
      i =
    (𝟙 ((single W₁ c j ⋙ F.mapHomologicalComplex c).obj X)).f i
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 : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
⊢ { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ } ≫
      { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ } =
    𝟙 ((F ⋙ single W₂ c j).obj X)

Tactic:
ext i

Goal state after:
ι : 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✝ : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
i : ι
⊢ ({ f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ } ≫
          { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }).f
      i =
    (𝟙 ((F ⋙ single W₂ c j).obj X)).f i