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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
⊢ normalizer ↑(map N.subtype ↑P) ⊔ N = ⊤

Tactic:
by
  refine top_le_iff.mp fun g _ => ?_
  obtain ⟨n, hn⟩ := exists_smul_eq N ((MulAut.conjNormal g : MulAut N) • P) P
  rw [← inv_mul_cancel_left (↑n) g, sup_comm]
  apply mul_mem_sup (N.inv_mem n.2)
  rw [smul_def, ← mul_smul, ← MulAut.conjNormal_val, ← MulAut.conjNormal.map_mul,
    Sylow.ext_iff, pointwise_smul_def, Subgroup.pointwise_smul_def] at hn
  have : Function.Injective (MulAut.conj (n * g)).toMonoidHom := (MulAut.conj (n * g)).injective
  refine fun x ↦ (mem_map_iff_mem this).symm.trans ?_
  rw [map_map, ← congr_arg (map N.subtype) hn, map_map]
  rfl

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this✝ : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
this : ∀ g ∈ (↑H \ {1}).toFinset, p ∣ orderOf g
⊢ p ^ (p ^ k - 1) ∣ p ^ #(↑H \ {1}).toFinset

Tactic:
simp [Finset.card_sdiff, ← Nat.card_eq_fintype_card, hH]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ∏ p, Nat.card ↥↑(P ↑p) = ∏ p, ↑p ^ (Nat.card G).factorization ↑p

Tactic:
by
        congr 1 with ⟨p, hp⟩
        exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_primeFactors hp⟩ (P p)

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case mp
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ (fun i ↦ s.toFun ⟨↑i, ⋯⟩) i ≠ last s ∧ (fun i ↦ s.toFun ⟨↑i, ⋯⟩) i ∈ range s.toFun

Tactic:
have hi : (i : ℕ) < s.length := by lia

Goal state after:
case mp
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
hi : ↑i < s.length
⊢ (fun i ↦ s.toFun ⟨↑i, ⋯⟩) i ≠ last s ∧ (fun i ↦ s.toFun ⟨↑i, ⋯⟩) i ∈ range s.toFun
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 : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : IsSemisimpleModule R M
P : Type u_6
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : N →ₗ[R] M
hf : Function.Injective ⇑f
g : N →ₗ[R] P
m : Submodule R M
compl : IsCompl f.range m
⊢ (g ∘ₗ LinearMap.linearProjOfIsCompl m f hf compl) ∘ₗ f = g

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_2.refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i✝¹ : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
i✝ : Fin ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)
i : Fin (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)
⊢ Iso
    (((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun i.castSucc.castSucc.castSucc,
      ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun i.castSucc.castSucc.succ)
    (((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun
        ((Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc) i.castSucc.castSucc).castSucc,
      ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun
        ((Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc) i.castSucc.castSucc).succ)

Tactic:
Equiv.swap_apply_of_ne_of_ne h2 h1,

Goal state after:
case refine_2.refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i✝¹ : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
i✝ : Fin ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)
i : Fin (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)
⊢ Iso
    (((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun i.castSucc.castSucc.castSucc,
      ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun i.castSucc.castSucc.succ)
    (((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun i.castSucc.castSucc.castSucc,
      ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun i.castSucc.castSucc.succ)
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
⊢ p ⊔ q = ⨆ i ∈ Set.univ, f i

Tactic:
iSup_univ,

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
⊢ p ⊔ q = ⨆ x, f x
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this✝ : Module R S := Module.compHom S f
this : RingHomSurjective f
e : S →ₛₗ[f] S :=
  let __src := AddMonoidHom.id S;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleRing S

Tactic:
rw [IsSemisimpleRing, ← e.isSemisimpleModule_iff_of_bijective Function.bijective_id]

Goal state after:
R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this✝ : Module R S := Module.compHom S f
this : RingHomSurjective f
e : S →ₛₗ[f] S :=
  let __src := AddMonoidHom.id S;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleModule R S
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
n : ℕ
m₁ m₂ : M
⊢ single R n (m₁ + m₂) = single R n m₁ + single R n m₂

Tactic:
by ext; simp

Goal state after:
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
⊢ (fun q ↦ ⟨(Submodule.orderIsoMapComap (of R M a)).symm (Submodule.restrictScalars R q), ⋯⟩)
      ((fun p ↦
          let __AddSubmonoid := AddSubmonoid.map (of R M a) (↑p).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ })
        p) =
    p

Tactic:
by ext; simp

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
inst✝ : Module.Finite R M
hM : IsTorsion R M
⊢ (↑⊤.annihilator ∩ ↑R⁰).Nonempty

Tactic:
obtain ⟨S, hS⟩ := ‹Module.Finite R M›.fg_top
  refine ⟨_, ?_, (∏ x ∈ S, (@hM x).choose : R⁰).prop⟩
  rw [Submonoid.coe_finsetProd, SetLike.mem_coe, ← hS, mem_annihilator_span]
  intro n
  let := Classical.decEq M
  rw [← Finset.prod_erase_mul _ _ n.prop, mul_smul, ← Submonoid.smul_def, (@hM n).choose_spec,
    smul_zero]

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

Goal state before:
pp: case mp
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : a • (mk (R ∙ a * b)) x = 0
⊢ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x

Tactic:
rw [← mk_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero, Submodule.mem_span_singleton] at h
    obtain ⟨c, h⟩ := h
    rw [smul_eq_mul, smul_eq_mul, mul_comm, mul_assoc, mul_cancel_left_mem_nonZeroDivisors ha,
      mul_comm] at h
    use c
    rw [← h, ← mk_eq_mk, ← Quotient.mk_smul, smul_eq_mul, mk_eq_mk]

Goal state after:
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case smul₀
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 p : M
hp : p ∈ P
⊢ r • p ∈ N

Tactic:
← Submodule.Quotient.mk_eq_zero,

Goal state after:
case smul₀
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 p : M
hp : p ∈ P
⊢ Quotient.mk (r • p) = 0
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case add
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 x✝ y✝ : M
hx✝ : x✝ ∈ r • P
hy✝ : y✝ ∈ r • P
hx : x✝ ∈ N
hy : y✝ ∈ N
⊢ x✝ + y✝ ∈ N

Tactic:
exact N.add_mem hx hy

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp
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₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : (Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l = single R (n + 1) x
⊢ x ∈ I • F.N n

Tactic:
replace hl := congr_arg (fun f : PolynomialModule R M => f.coeff (n + 1)) hl

Goal state after:
case mp
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₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l).coeff (n + 1) = (single R (n + 1) x).coeff (n + 1)
⊢ x ∈ I • F.N n
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr
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
⊢ x ∈ ⨅ i, I ^ i • ⊤

Tactic:
Submodule.mem_iInf

Goal state after:
case mpr
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 : ℕ), x ∈ I ^ i • ⊤
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
⊢ (fun i ↦ i) = ⇑e.symm ∘ ⇑e

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
⊢ ⇑e ∘ ⇑e.symm = fun i ↦ i

Tactic:
by ext; simp

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
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X✝ : α → V
d_X : (n : α) → X✝ (n + 1) ⟶ X✝ n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y✝ : α → V
d_Y : (n : α) → Y✝ (n + 1) ⟶ Y✝ n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
X Y : ChainComplex V α
f : (i : α) → X.X i ⟶ Y.X i
comm : ∀ (i : α), f (i + 1) ≫ Y.d (i + 1) i = X.d (i + 1) i ≫ f i
n m : α
⊢ (ComplexShape.down α).Rel n m → f n ≫ Y.d n m = X.d n m ≫ f m

Tactic:
simp only [ComplexShape.down_Rel]
    rintro rfl
    simpa using comm m

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝ : ∀ (n : ι), HasLimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
⊢ limMap { app := fun j ↦ (F.obj j).d n m, naturality := ⋯ } = 0

Tactic:
ext j

Goal state after:
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝ : ∀ (n : ι), HasLimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
⊢ limMap { app := fun j ↦ (F.obj j).d n m, naturality := ⋯ } ≫ limit.π (F ⋙ eval C c m) j =
    0 ≫ limit.π (F ⋙ eval C c m) j
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝ : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
⊢ colimMap { app := fun j ↦ (F.obj j).d n m, naturality := ⋯ } = 0

Tactic:
ext j

Goal state after:
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝ : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
⊢ colimit.ι (F ⋙ eval C c n) j ≫ colimMap { app := fun j ↦ (F.obj j).d n m, naturality := ⋯ } =
    colimit.ι (F ⋙ eval C c n) j ≫ 0
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteColimits C
K L : HomologicalComplex C c
φ : K ⟶ L
inst✝ : Epi φ
n : ι
⊢ Epi (φ.f n)

Tactic:
change Epi ((HomologicalComplex.eval C c n).map φ)

Goal state after:
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteColimits C
K L : HomologicalComplex C c
φ : K ⟶ L
inst✝ : Epi φ
n : ι
⊢ Epi ((eval C c n).map φ)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
⊢ (Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f =
      IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) ↔
    (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S

Tactic:
by
  rw [AlgHom.ext_iff, AlgHom.ext_iff]
  apply forall_congr'
  intro x
  have e₁ : (TensorProduct.lmul' R : S ⊗[R] S →ₐ[R] S).kerSquareLift (f x) =
      KaehlerDifferential.quotientCotangentIdealRingEquiv R S
        (Ideal.Quotient.mk (KaehlerDifferential.ideal R S).cotangentIdeal <| f x) := by
    generalize f x = y; obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y; rfl
  have e₂ :
    x = KaehlerDifferential.quotientCotangentIdealRingEquiv R S (IsScalarTower.toAlgHom R S _ x) :=
    (mul_one x).symm
  constructor
  · intro e
    exact (e₁.trans (@RingEquiv.congr_arg _ _ _ _ _ _
      (KaehlerDifferential.quotientCotangentIdealRingEquiv R S) _ _ e)).trans e₂.symm
  · intro e; apply (KaehlerDifferential.quotientCotangentIdealRingEquiv R S).injective
    exact e₁.symm.trans (e.trans e₂)

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

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology i
hij : ¬c.Rel i j
⊢ K.iCycles i ≫ K.d i j = 0

Tactic:
· rw [K.shape _ _ hij, comp_zero]

Goal state after:
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 n₁ n₂ n₃ n₁₂ n₂₃ n₁₂₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
h₁₂ : n₁ + n₂ = n₁₂
h₂₃ : n₂ + n₃ = n₂₃
h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃
⊢ n₁ + n₂₃ = n₁₂₃

Tactic:
rw [← h₂₃, ← h₁₂₃, add_assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ (-z₁).comp z₂ h = -z₁.comp z₂ h

Tactic:
ext p q hpq
  simp only [comp_v _ _ h p _ q rfl (by lia), neg_v, neg_comp]

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

Goal state before:
pp: 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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ f = desc φ (inr φ ≫ f) ((Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯)))

Tactic:
ext j

Goal state after:
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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
⊢ f.f j =
    (desc φ (inr φ ≫ f) ((Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯)))).f j
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: 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
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i : ι
hi : c.Rel i (c.next i)
⊢ H.obj ((homotopyCofiber φ).X i) ≅ (homotopyCofiber ((H.mapHomologicalComplex c).map φ)).X i

Tactic:
by
    haveI := preservesBinaryBiproducts_of_preservesBiproducts H
    haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hi
    haveI := HasHomotopyCofiber.hasBinaryBiproduct ((H.mapHomologicalComplex c).map φ) _ _ hi
    exact H.mapIso (homotopyCofiber.XIsoBiprod φ _ _ hi) ≪≫ H.mapBiprod _ _ ≪≫
      (homotopyCofiber.XIsoBiprod ((H.mapHomologicalComplex c).map φ) _ _ hi).symm

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

Goal state before:
pp: case e_a.e_a.succ
ι : 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 : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
n✝ : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ (xPrevIso Q ⋯).inv =
    if h : (ComplexShape.up ℕ).prev (n✝ + 1) + 1 = n✝ + 1 then
      (xNextIso P h).inv ≫
        (mkCoinductiveAux₂ e zero comm_zero one comm_one succ ((ComplexShape.up ℕ).prev (n✝ + 1))).snd.fst
    else 0

Tactic:
simp only [CochainComplex.prev_nat_succ, dite_true]

Goal state after:
case e_a.e_a.succ
ι : 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 : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
n✝ : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ (xPrevIso Q ⋯).inv =
    (xNextIso P ⋯).inv ≫
      (mkCoinductiveAux₂ e zero comm_zero one comm_one succ ((ComplexShape.up ℕ).prev (n✝ + 1))).snd.fst
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : Linear R (Quotient r) := linear R r hr
⊢ Functor.Linear R (functor r)

Tactic:
(Tactic.exact
 "exact"
 (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))

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

Goal state before:
pp: 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
h : Homotopy φ₀ φ₁
hc : ∀ (j : ι), ∃ i, c.Rel i j
inst✝² : ∀ (i : ι), HasBinaryBiproduct (F.X i) (F.X i)
inst✝¹ : HasHomotopyCofiber (biprod.lift (𝟙 F) (-𝟙 F))
D : Type u_3
inst✝ : Category.{v_2, u_3} D
H : HomologicalComplex C c ⥤ D
hH : (homotopyEquivalences C c).IsInvertedBy H
⊢ H.map φ₀ = H.map φ₁

Tactic:
by
  classical
  simp only [← cylinder.ι₀_desc _ _ h, ← cylinder.ι₁_desc _ _ h, H.map_comp,
    cylinder.map_ι₀_eq_map_ι₁ _ hc _ hH]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
h : n = 0
X✝ Y✝ : CochainComplex C ℤ
x✝ : X✝ ⟶ Y✝
⊢ (shiftFunctor C n).map x✝ ≫ (Hom.isoOfComponents (fun i ↦ Y✝.shiftFunctorObjXIso n i i ⋯) ⋯).hom =
    (Hom.isoOfComponents (fun i ↦ X✝.shiftFunctorObjXIso n i i ⋯) ⋯).hom ≫ (𝟭 (CochainComplex C ℤ)).map x✝

Tactic:
by ext; simp

Goal state after: