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

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Nat.card G = d
h : ∀ (t : G), t ^ a.val = t ^ b.val
⊢ a = b

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
  specialize h g
  subst hGcard
  rw [pow_eq_pow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers hg,
    ← ZMod.natCast_eq_natCast_iff] at h
  simpa [ZMod.natCast_val, ZMod.cast_id'] using h

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ I ^ n ⊔ J ^ n = ⊤

Tactic:
eq_top_iff,

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ ⊤ ≤ I ^ n ⊔ J ^ n
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
hG : Monoid.exponent G = 2
x : G
⊢ orderOf x = 2 → x ≠ 1

Tactic:
by rintro hx rfl; norm_num at hx

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

Goal state before:
pp: case h.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
h1 : ∑ m ∈ d.properDivisors, #{a | orderOf a = m} = ∑ m ∈ d.properDivisors, φ m
⊢ #{a | orderOf a = d} = φ d

Tactic:
have h2 :
    (∑ m ∈ d.divisors, #{a : α | orderOf a = m}) =
      ∑ m ∈ d.divisors, φ m := by
    rw [sum_card_orderOf_eq_card_pow_eq_one hd0, sum_totient,
      ← ha, card_pow_eq_one_eq_orderOf_aux hn a]

Goal state after:
case h.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
h1 : ∑ m ∈ d.properDivisors, #{a | orderOf a = m} = ∑ m ∈ d.properDivisors, φ m
h2 : ∑ m ∈ d.divisors, #{a | orderOf a = m} = ∑ m ∈ d.divisors, φ m
⊢ #{a | orderOf a = d} = φ d
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
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
⊢ f (y ^ (-m)) * f a = 1

Tactic:
f.map_zpow,

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, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
⊢ f y ^ (-m) * f a = 1
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
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
⊢ f (y ^ (-n)) * f b = 1

Tactic:
f.map_zpow,

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, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
⊢ f y ^ (-n) * f b = 1
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a | IsAtom a}
hu₂ : sSup u = ⨆ i ∈ s, f i
⊢ sSup {a | IsAtom a} = ⊤

Tactic:
eq_top_iff,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a | IsAtom a}
hu₂ : sSup u = ⨆ i ∈ s, f i
⊢ ⊤ ≤ sSup {a | IsAtom a}
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
⊢ normalizer ↑↑P = ⊤

Tactic:
← normalizer_sup_eq_top' P le_normalizer,

Goal state after:
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
⊢ normalizer ↑↑P = normalizer ↑P ⊔ normalizer ↑↑P
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (x ⊔ y)
hyz : IsMaximal y (x ⊔ y)
⊢ IsMaximal (x ⊓ y) y

Tactic:
rw [inf_comm]
  rw [sup_comm] at hxz hyz
  exact isMaximal_inf_left_of_isMaximal_sup hyz hxz

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
a : R
⊢ torsionBySet R M {a} = torsionBy R M a

Tactic:
ext x
  simp only [mem_torsionBySet_iff, SetCoe.forall, Set.mem_singleton_iff, forall_eq,
    mem_torsionBy_iff]

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
a : R
⊢ IsTorsionBy R M a ↔ torsionBy R M a = ⊤

Tactic:
rw [← torsionBySet_singleton_eq, ← isTorsionBySet_singleton_iff,
    isTorsionBySet_iff_torsionBySet_eq_top]

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
i : ℕ
m : M
⊢ (comp p) (single R i m) = p ^ i • single R 0 m

Tactic:
by
  rw [comp_apply, map_single, eval_single]
  rfl

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
q : PolynomialModule R M
r : R
⊢ (eval r) ((comp p) q) = (eval (Polynomial.eval r p)) q

Tactic:
rw [← LinearMap.comp_apply]
  induction q using induction_linear with
  | zero => simp_rw [map_zero]
  | add _ _ e₁ e₂ => simp_rw [map_add, e₁, e₂]
  | single i m =>
    rw [LinearMap.comp_apply, comp_single, eval_single, eval_smul, eval_single, eval_pow]
    module

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
h : (Ideal.span {r}).IsTwoSided
hM : IsTorsionBy R M r
⊢ IsTorsionBySet R M ↑(Ideal.span {r})

Tactic:
finally
  rwa [← isTorsionBySet_span_singleton_iff] at hM

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

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
oj : Option (Fin d) := List.argmax (fun i ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
⊢ torsionBy R M (p ^ pOrder hM (s (oj.get hoj))) = ⊤

Tactic:
eq_top_iff,

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
oj : Option (Fin d) := List.argmax (fun i ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
⊢ ⊤ ≤ torsionBy R M (p ^ pOrder hM (s (oj.get hoj)))
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case h.refine_2.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hsspan : span R s = map (I • N).mkQ N
⊢ span R (Quotient.out '' s) = N

Tactic:
symm

Goal state after:
case h.refine_2.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hsspan : span R s = map (I • N).mkQ N
⊢ N = span R (Quotient.out '' s)
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:
intros; ext1; simp only [add_app]; apply add_comm

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:
by
    ext i
    exact congr_fun h i

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
A B : V
f : A ⟶ B
⊢ ((single₀ V).map f).f 0 = f

Tactic:
by
  rw [HomologicalComplex.single_map_f_self]
  dsimp [HomologicalComplex.singleObjXSelf, HomologicalComplex.singleObjXIsoOfEq]
  rw [comp_id, id_comp]

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
X Y : C
f : X ⟶ Y
⊢ (shiftFunctor C 0).map f = (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv

Tactic:
symm

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv = (shiftFunctor C 0).map f
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case zero
ι : 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
⊢ (mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').X (0 + 2) ≅ (succ' ((mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d (0 + 1) 0)).fst

Tactic:
apply eqToIso
    dsimp [mk', mk, of, mkAux, of.d]
    rw [id_comp]

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

Goal state before:
pp: case h
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
this : ∑ i ∈ x.support with (algebraMap A B) i = c, x i ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
⊢ ((∑ x_1 ∈ x.support with (algebraMap A B) x_1 = c, x x_1) • 1) ⊗ₜ[A] (D R A) a = 0

Tactic:
← Algebra.algebraMap_eq_smul_one,

Goal state after:
case h
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
this : ∑ i ∈ x.support with (algebraMap A B) i = c, x i ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
⊢ (algebraMap A B) (∑ x_1 ∈ x.support with (algebraMap A B) x_1 = c, x x_1) ⊗ₜ[A] (D R A) a = 0
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 : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
k : Rˣ
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ z₁.comp (k • z₂) h = k • z₁.comp z₂ h

Tactic:
apply Cochain.comp_smul

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₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁

Tactic:
by
  dsimp only [nullHomotopicMap]
  rw [dNext_eq hom r₁₀, prevD_eq hom r₂₁]

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

Goal state before:
pp: case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬1 = 0

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v, u_1} C
inst✝³ : Category.{v', u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
⊢ 1 + m = n

Tactic:
by rw [← h, add_comm]

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

Goal state before:
pp: case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬1 = 0

Tactic:
decide

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z}, CompClosure r g g' → CompClosure r (f ≫ g) (f ≫ g')

Tactic:
by
    rintro a b e f _ _ ⟨c, d, g, h₁, h₂, i, h⟩
    simpa using CompClosure.intro _ _ (f ≫ g) _ _ i h

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: case mk.mk.mk
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a✝³ : P ⟶ Q
a✝² : P.as ⟶ Q.as
b✝ : P ⟶ Q
a✝¹ : P.as ⟶ Q.as
c✝ : P ⟶ Q
a✝ : P.as ⟶ Q.as
⊢ Quot.mk (HomRel.CompClosure r) a✝² + Quot.mk (HomRel.CompClosure r) a✝¹ + Quot.mk (HomRel.CompClosure r) a✝ =
    Quot.mk (HomRel.CompClosure r) a✝² + (Quot.mk (HomRel.CompClosure r) a✝¹ + Quot.mk (HomRel.CompClosure r) a✝)

Tactic:
exact congr_arg (functor r).map (add_assoc _ _ _)

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

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
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
⊢ isoAdd' ⋯ e (isoZero F A) = e

Tactic:
ext X
  simp [shiftFunctorAdd'_add_zero_hom_app, ← Functor.map_comp_assoc,
    shiftFunctorAdd'_add_zero_inv_app]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
⊢ (-γ).rightShift a n' hn' = -γ.rightShift a n' hn'

Tactic:
change rightShiftAddEquiv K L n a n' hn' (-γ) = _

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn') (-γ) = -γ.rightShift a n' hn'
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
γ' : Cochain L M 0
⊢ Int.negOnePow 0 • (γ.leftShift a n' hn').comp γ' ⋯ = (γ.leftShift a n' hn').comp γ' ⋯

Tactic:
Int.negOnePow_zero,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
γ' : Cochain L M 0
⊢ 1 • (γ.leftShift a n' hn').comp γ' ⋯ = (γ.leftShift a n' hn').comp γ' ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ (snd φ).v n n ⋯ ≫ ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)).f +
      ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)).g ≫ (-(inl φ).v (n + 1) n ⋯) =
    𝟙 ((triangleRotateShortComplex φ).map (eval C (ComplexShape.up ℤ) n)).X₂

Tactic:
by simp [ext_from_iff φ _ _ rfl]

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

Goal state before:
pp: C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C :=
  { X₁ := K.homology i, X₂ := K.opcycles i, X₃ := K.cycles j, f := K.homologyι i, g := K.opcyclesToCycles i j,
    zero := ⋯ }
S' : ShortComplex C :=
  { X₁ := K.homology i, X₂ := K.opcycles i, X₃ := K.X j, f := K.homologyι i, g := K.fromOpcycles i j, zero := ⋯ }
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex C :=
  { X₁ := K.opcycles i, X₂ := K.cycles j, X₃ := K.homology j, f := K.opcyclesToCycles i j, g := K.homologyπ j,
    zero := ⋯ }
T' : ShortComplex C :=
  { X₁ := K.X i, X₂ := K.cycles j, X₃ := K.homology j, f := K.toCycles i j, g := K.homologyπ j, zero := ⋯ }
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ T.Exact

Tactic:
rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono π]

Goal state after:
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C :=
  { X₁ := K.homology i, X₂ := K.opcycles i, X₃ := K.cycles j, f := K.homologyι i, g := K.opcyclesToCycles i j,
    zero := ⋯ }
S' : ShortComplex C :=
  { X₁ := K.homology i, X₂ := K.opcycles i, X₃ := K.X j, f := K.homologyι i, g := K.fromOpcycles i j, zero := ⋯ }
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex C :=
  { X₁ := K.opcycles i, X₂ := K.cycles j, X₃ := K.homology j, f := K.opcyclesToCycles i j, g := K.homologyπ j,
    zero := ⋯ }
T' : ShortComplex C :=
  { X₁ := K.X i, X₂ := K.cycles j, X₃ := K.homology j, f := K.toCycles i j, g := K.homologyπ j, zero := ⋯ }
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ T'.Exact
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.6
inst✝ : Category.{v_1, ?u.6} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ g') =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) g'
⊢ Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ g'.cons p) =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (g'.cons p)

Tactic:
have : f ≫ Quiver.Path.cons g' p = (f ≫ g').cons p := by apply Quiver.Path.comp_cons
      rw [this]
      simp only at ih ⊢
      rw [ih, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case mpr.cons.inl
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₂.obj ⟶ X₃.obj
⊢ P (G.map (Quiver.Hom.toPath (Sum.inl g)))

pp: case mpr.cons.inr
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₃.obj ⟶ X₂.obj
hg : W g
⊢ P (G.map (Quiver.Hom.toPath (Sum.inr ⟨g, hg⟩)))

Tactic:
· apply hP₁

Goal state after:
case mpr.cons.inr
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₃.obj ⟶ X₂.obj
hg : W g
⊢ P (G.map (Quiver.Hom.toPath (Sum.inr ⟨g, hg⟩)))
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map L ⋯
α : W.LeftFraction φ.Y' φ'.Y'
hα : { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.f ≫ α.s = { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.s ≫ α.f
ψ : W.LeftFraction₂ X Y := { Y' := α.Y', f := φ.f ≫ α.f, f' := φ'.f ≫ α.s, s := φ'.s ≫ α.s, hs := ⋯ }
this : IsIso (L.map (φ'.s ≫ α.s))
⊢ f' ≫ L.map (φ'.s ≫ α.s) = ψ.snd.map L ⋯ ≫ L.map (φ'.s ≫ α.s)

Tactic:
hφ'

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map L ⋯
α : W.LeftFraction φ.Y' φ'.Y'
hα : { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.f ≫ α.s = { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.s ≫ α.f
ψ : W.LeftFraction₂ X Y := { Y' := α.Y', f := φ.f ≫ α.f, f' := φ'.f ≫ α.s, s := φ'.s ≫ α.s, hs := ⋯ }
this : IsIso (L.map (φ'.s ≫ α.s))
⊢ φ'.map L ⋯ ≫ L.map (φ'.s ≫ α.s) = ψ.snd.map L ⋯ ≫ L.map (φ'.s ≫ α.s)