mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ orderOf t < orderOf t / p ^ k * p ^ (k + a + 1)

Tactic:
hk,

Goal state after:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ orderOf t < orderOf t / p ^ (orderOf t).factorization p * p ^ ((orderOf t).factorization p + a + 1)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1.snd
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ (g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂)).2 = 1.2

Tactic:
rw [Prod.pow_snd, Prod.snd_one, ← orderOf_dvd_iff_pow_eq_one]
      exact dvd_trans (Monoid.order_dvd_exponent (g.2)) <| dvd_lcm_right _ _

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, IsPGroup p ↥(H i)
hn : ∀ i ∈ s, (H i).Normal
this : ∀ (i : ↑s), (H ↑i).Normal
⊢ IsPGroup p ↥(⨆ i, H ↑i)

Tactic:
exact iSup_of_normal _ fun i ↦ h i i.property

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

Goal state before:
pp: case refine_2
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
this : p.natDegree ≤ 1
⊢ eval r (reflect b.natDegree (map (algebraMap R S) b) * reflect (1 + c.natDegree) (X ^ 0)) = 0

Tactic:
← reflect_mul _ _ natDegree_map_le (by simp),

Goal state after:
case refine_2
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
this : p.natDegree ≤ 1
⊢ eval r (reflect (b.natDegree + (1 + c.natDegree)) (map (algebraMap R S) b * X ^ 0)) = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
⊢ f.IsIntegral

Tactic:
by
  algebraize [f]
  suffices Algebra.IsIntegral R S by rwa [Algebra.isIntegral_def] at this
  nontriviality R
  nontriviality S
  constructor
  intro r
  let p : S[X] := C r * X - 1
  have : (1 : R[X]) ∈ Ideal.span {X} ⊔ (Ideal.span {p}).comap (mapRingHom f) := by
    have H := h _ (isClosed_zeroLocus {p})
    rw [← zeroLocus_span, ← closure_eq_iff_isClosed, closure_image_comap_zeroLocus] at H
    rw [← Ideal.eq_top_iff_one, sup_comm, ← zeroLocus_empty_iff_eq_top, zeroLocus_sup, H]
    suffices ∀ (a : PrimeSpectrum S[X]), p ∈ a.asIdeal → X ∉ a.asIdeal by
      simpa [Set.eq_empty_iff_forall_notMem]
    intro q hpq hXq
    have : 1 ∈ q.asIdeal := by simpa [p] using! (sub_mem (q.asIdeal.mul_mem_left (C r) hXq) hpq)
    exact q.2.ne_top (q.asIdeal.eq_top_iff_one.mpr this)
  obtain ⟨a, b, hb, e⟩ := Ideal.mem_span_singleton_sup.mp this
  obtain ⟨c, hc : b.map (algebraMap R S) = _⟩ := Ideal.mem_span_singleton.mp hb
  refine ⟨b.reverse * X ^ (1 + c.natDegree), ?_, ?_⟩
  · refine Monic.mul ?_ (by simp)
    have h : b.coeff 0 = 1 := by simpa using! congr(($e).coeff 0)
    have : b.natTrailingDegree = 0 := by simp [h]
    rw [Monic.def, reverse_leadingCoeff, trailingCoeff, this, h]
  · have : p.natDegree ≤ 1 := by simpa using! natDegree_linear_le (a := r) (b := -1)
    rw [eval₂_eq_eval_map, reverse, Polynomial.map_mul, ← reflect_map, Polynomial.map_pow,
      map_X, ← revAt_zero (1 + _), ← reflect_monomial,
      ← reflect_mul _ _ natDegree_map_le (by simp), pow_zero, mul_one, hc,
      ← add_assoc, reflect_mul _ _ (this.trans (by simp)) le_rfl,
      eval_mul, reflect_sub, reflect_mul _ _ (by simp) (by simp)]
    simp [← pow_succ']

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n.Coprime (orderOf g)

Tactic:
· simp only [Nat.coprime_iff_gcd_eq_one]
      have hgn : g ∈ Subgroup.zpowers (g ^ n) := by simp_all only [ne_eq, orderOf_eq_one_iff,
        Subgroup.mem_top]
      exact mem_zpowers_pow_iff.mp hgn

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
p : ℕ
g : G
x✝ : g ∈ (CommMonoid.primaryComponent G p).carrier
k : ℕ
hk : g ^ p ^ k = 1
⊢ (g ^ p ^ k)⁻¹ = 1

Tactic:
hk,

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
p : ℕ
g : G
x✝ : g ∈ (CommMonoid.primaryComponent G p).carrier
k : ℕ
hk : g ^ p ^ k = 1
⊢ 1⁻¹ = 1
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
m : M
x✝ : m ∈ (AddCommGroup.torsion M).carrier
n : ℕ
hn : n > 0
hn' : Function.IsPeriodicPt (fun x ↦ m + x) n 0
⊢ Function.IsPeriodicPt (fun x ↦ r • m + x) n 0

Tactic:
by { simp only [Function.IsPeriodicPt, Function.IsFixedPt, add_left_iterate, add_zero,
      smul_comm n] at hn' ⊢; simp only [hn', smul_zero] }

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

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
inst✝ : Finite G
d : ℕ
⊢ (powMonoidHom d).ker.index = Nat.card G / (Nat.card G).gcd d

Tactic:
Subgroup.index_ker,

Goal state after:
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
inst✝ : Finite G
d : ℕ
⊢ Nat.card ↥(powMonoidHom d).range = Nat.card G / (Nat.card G).gcd d
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
⊢ Nat.card ↥(normalizer ↑H) ≡ Nat.card G [MOD p ^ (n + 1)]

Tactic:
have : H.subgroupOf (normalizer H) ≃ H := (subgroupOfEquivOfLe le_normalizer).toEquiv

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
this : ↥(H.subgroupOf (normalizer ↑H)) ≃ ↥H
⊢ Nat.card ↥(normalizer ↑H) ≡ Nat.card G [MOD p ^ (n + 1)]
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
⊢ ∃ H, Nat.card ↥H = p ^ n

Tactic:
have : Fact p.Prime := ⟨hp⟩

Goal state after:
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this : Fact (Nat.Prime p)
⊢ ∃ H, Nat.card ↥H = p ^ n
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
inst✝ : IsSemisimpleModule R M
⊢ sSup {m | IsSimpleModule R ↥m} = ⊤

Tactic:
simpa only [isSimpleModule_iff_isAtom] using sSup_atoms_eq_top

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
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t ↦ Bool.rec q p t
⊢ IsSemisimpleModule R ↥(p ⊔ q)

Tactic:
show p ⊔ q = ⨆ i ∈ Set.univ, f i by rw [iSup_univ, iSup_bool_eq]

Goal state after:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t ↦ Bool.rec q p t
⊢ IsSemisimpleModule R ↥(⨆ i ∈ Set.univ, f i)
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: 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
⊢ ∃ r, r - 1 ∈ I ∧ r • P ≤ N

Tactic:
refine ⟨r, hmem, fun x hx ↦ ?_⟩

Goal state after:
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
hx : x ∈ r • P
⊢ x ∈ N
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case neg.refine_1
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
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, single R i '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : single R j '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • F.N j)
r : R
hr : r ∈ I
m' : M
hm' : m' ∈ F.N j
⊢ (monomial 1) r • single R j m' ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))

Tactic:
exact F'.smul_mem
        ⟨_, reesAlgebra.monomial_mem.mpr (by rwa [pow_one])⟩ (hj <| Set.mem_image_of_mem _ hm')

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : ↥I
e :
  ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) (I.toCotangent x)) =
    ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) (I.toCotangent y))
⊢ ↑x - ↑y ∈ I ^ 2

Tactic:
dsimp only [toCotangent_to_quotient_square, Submodule.mkQ_apply] at e

Goal state after:
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : ↥I
e : Submodule.Quotient.mk ↑x = Submodule.Quotient.mk ↑y
⊢ ↑x - ↑y ∈ I ^ 2
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
⊢ Submodule.restrictScalars R ⊤ = ⊤

Tactic:
Submodule.restrictScalars_top

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
⊢ ⊤ = ⊤
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr.succ
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⨅ i, I ^ i • ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : ↥I
eq : ↑r • x = x
i : ℕ
hi : x ∈ I ^ i • ⊤
⊢ x ∈ I ^ (i + 1) • ⊤

Tactic:
rw [add_comm, pow_add, ← smul_smul, pow_one, ← eq]
      exact Submodule.smul_mem_smul r.prop hi

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
⊢ I = ⊥ ∨ I = ⊤ → IsIdempotentElem I

Tactic:
rintro (rfl | rfl) <;> simp [IsIdempotentElem]

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsNoetherianRing R
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
hx' : x ∉ ⊥
this : x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x
r : ↥I
hr : ↑r • x = x
⊢ False

Tactic:
have := smul_left_injective _ hx' (hr.trans (one_smul _ x).symm)

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsNoetherianRing R
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
hx' : x ∉ ⊥
this✝ : x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x
r : ↥I
hr : ↑r • x = x
this : ↑r = 1
⊢ False
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a b : M₁ ⟶ M₂), a + b = b + a

Tactic:
by intros; ext1; simp only [add_app]; apply add_comm

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ F.map (𝟙 (X j)) = 𝟙 (F.obj (X j))

Tactic:
Functor.map_id

Goal state after:
C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ 𝟙 (F.obj (X j)) = 𝟙 (F.obj (X j))
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ F.map (𝟙 (Y j)) = 𝟙 (F.obj (Y j))

Tactic:
Functor.map_id

Goal state after:
C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ 𝟙 (F.obj (Y j)) = 𝟙 (F.obj (Y j))
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 : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p).obj ((shiftFunctor C p').obj X)) = (shiftFunctor C p).map (𝟙 ((shiftFunctor C p').obj X))

Tactic:
Functor.map_id

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p).obj ((shiftFunctor C p').obj X)) = 𝟙 ((shiftFunctor C p).obj ((shiftFunctor C p').obj X))
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ 𝟙 ((shiftFunctor C n).obj X) = (shiftFunctor C n).map (𝟙 X)

Tactic:
Functor.map_id

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ 𝟙 ((shiftFunctor C n).obj X) = 𝟙 ((shiftFunctor C n).obj X)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
      (shiftFunctor D m₃).map ((shiftFunctorAdd D m₁ m₂).hom.app (F.obj X)) =
    (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯).hom.app (F.obj X) ≫
      (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
        (shiftFunctor D m₃).map ((i (m₁ + m₂)).inv.app X) ≫
          (i m₃).inv.app ((s (m₁ + m₂)).obj X) ≫
            (i m₃).hom.app ((s (m₁ + m₂)).obj X) ≫ (F ⋙ shiftFunctor D m₃).map ((add hF s i m₁ m₂).hom.app X) =
    F.map (eqToHom ⋯) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        (shiftFunctorAdd D m₁ (m₂ + m₃)).hom.app (F.obj X) ≫
          (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X)) ≫
            (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X)) ≫
              (shiftFunctor D m₃).map ((i m₂).inv.app ((s m₁).obj X))

Tactic:
Functor.comp_map,

Goal state after:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
      (shiftFunctor D m₃).map ((shiftFunctorAdd D m₁ m₂).hom.app (F.obj X)) =
    (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯).hom.app (F.obj X) ≫
      (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
        (shiftFunctor D m₃).map ((i (m₁ + m₂)).inv.app X) ≫
          (i m₃).inv.app ((s (m₁ + m₂)).obj X) ≫
            (i m₃).hom.app ((s (m₁ + m₂)).obj X) ≫ (shiftFunctor D m₃).map (F.map ((add hF s i m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        (shiftFunctorAdd D m₁ (m₂ + m₃)).hom.app (F.obj X) ≫
          (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X)) ≫
            (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X)) ≫
              (shiftFunctor D m₃).map ((i m₂).inv.app ((s m₁).obj X))
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
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A' A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
α : A' ⟶ A
⊢ α ≫ k ≫ K.d i j = 0

Tactic:
hk,

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
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A' A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
α : A' ⟶ A
⊢ α ≫ 0 = 0
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
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
A : C
k : L.X i ⟶ A
j : ι
hj : c.prev i = j
hk : L.d j i ≫ k = 0
φ : K ⟶ L
⊢ φ.f j ≫ L.d j i ≫ k = 0

Tactic:
hk,

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
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
A : C
k : L.X i ⟶ A
j : ι
hj : c.prev i = j
hk : L.d j i ≫ k = 0
φ : K ⟶ L
⊢ φ.f j ≫ 0 = 0
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ (φ ≫ inr φ).f j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j

Tactic:
homotopyCofiber_d,

Goal state after:
case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ (φ ≫ inr φ).f j = inlX φ j i hij ≫ d φ i j
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₁ q₂ : ℤ
hq₁ : q₁ = q - 1
hq₂ : p + 1 = q₂
⊢ p + n = q₁

Tactic:
rw [hq₁, ← hpq, ← hnm, ← add_assoc, add_sub_cancel_right]

Goal state after:
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 : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (dNext k₀) hom + (prevD k₀) hom = hom k₀ k₁ ≫ D.d k₁ k₀

Tactic:
rw [prevD_eq hom r₁₀, dNext, AddMonoidHom.mk'_apply, C.shape, zero_comp, zero_add]

Goal state after:
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel k₀ (c.next k₀)
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
H : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : c.Rel i (c.next i)
⊢ (mapArrowHom φ φ H (𝟙 (Arrow.mk φ))).f i = 𝟙 (X φ i)

Tactic:
refine ext_to_X _ _ _ hi ?_ ?_

Goal state after:
case pos.refine_1
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
H : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : c.Rel i (c.next i)
⊢ (mapArrowHom φ φ H (𝟙 (Arrow.mk φ))).f i ≫ fstX φ i (c.next i) hi = 𝟙 (X φ i) ≫ fstX φ i (c.next i) hi

case pos.refine_2
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
H : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : c.Rel i (c.next i)
⊢ (mapArrowHom φ φ H (𝟙 (Arrow.mk φ))).f i ≫ sndX φ i = 𝟙 (X φ i) ≫ sndX φ i