mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : Set S
⊢ zeroLocus ↑(Ideal.span (⇑(algebraMap R S) '' ↑(Ideal.comap (algebraMap R S) (Ideal.span s)))) = zeroLocus s

Tactic:
← zeroLocus_span s,

Goal state after:
case mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : Set S
⊢ zeroLocus ↑(Ideal.span (⇑(algebraMap R S) '' ↑(Ideal.comap (algebraMap R S) (Ideal.span s)))) =
    zeroLocus ↑(Ideal.span s)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
⊢ sigmaToPi R '' Sigma.mk i '' ↑(basicOpen f) = ↑(basicOpen (Pi.single i f))

Tactic:
simp only [Set.image_image, sigmaToPi_apply]
  exact PrimeSpectrum.comap_evalRingHom_basicOpen _ _

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

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ DenseRange (comap f) → ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)

Tactic:
intro H I hI

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
H : DenseRange (comap f)
I : Ideal R
hI : I ∈ minimalPrimes R
⊢ { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fact (Nat.Prime p)
⊢ IsPGroup p G ↔ ∃ n, Monoid.exponent G = p ^ n

Tactic:
isPGroup_iff_exponent_dvd_pow,

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fact (Nat.Prime p)
⊢ (∃ n, Monoid.exponent G ∣ p ^ n) ↔ ∃ n, Monoid.exponent G = p ^ n
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ IsPGroup p ↥Q

Tactic:
apply h.comap_of_ker_isPGroup

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := ⋯
⊢ IsPGroup p ↥(QuotientGroup.mk' ↑P).ker
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Infinite ↥f.ker
⊢ IsCyclic M

pp: case inr
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Finite ↥f.ker
⊢ IsCyclic M

Tactic:
· rw [Nat.card_eq_zero_of_infinite, Nat.coprime_zero_left] at h
    rw [← f.range.eq_bot_iff_card, f.range_eq_bot_iff, ← f.ker_eq_top_iff] at h
    rwa [← Subgroup.topEquiv.isCyclic, ← h]

Goal state after:
case inr
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Finite ↥f.ker
⊢ IsCyclic M
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr.inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime 0
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Infinite ↥f.range
⊢ IsCyclic M

Tactic:
Nat.coprime_zero_right

Goal state after:
case inr.inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : Nat.card ↥f.ker = 1
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Infinite ↥f.range
⊢ IsCyclic M
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Group M
inst✝² : Group N
cyc✝ : IsCyclic (M × N)
inst✝¹ : Finite M
inst✝ : Finite N
hM✝ : IsCyclic M
hN✝ : IsCyclic N
x✝² : CommGroup (M × N) := IsCyclic.commGroup
cyc : Monoid.exponent (M × N) = Nat.card (M × N)
x✝¹ : CommGroup M := IsCyclic.commGroup
hM : Monoid.exponent M = Nat.card M
x✝ : CommGroup N := IsCyclic.commGroup
hN : Monoid.exponent N = Nat.card N
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
Monoid.exponent_prod,

Goal state after:
M : Type u_4
N : Type u_5
inst✝³ : Group M
inst✝² : Group N
cyc✝ : IsCyclic (M × N)
inst✝¹ : Finite M
inst✝ : Finite N
hM✝ : IsCyclic M
hN✝ : IsCyclic N
x✝² : CommGroup (M × N) := IsCyclic.commGroup
cyc : lcm (Monoid.exponent M) (Monoid.exponent N) = Nat.card (M × N)
x✝¹ : CommGroup M := IsCyclic.commGroup
hM : Monoid.exponent M = Nat.card M
x✝ : CommGroup N := IsCyclic.commGroup
hN : Monoid.exponent N = Nat.card N
⊢ (Nat.card M).Coprime (Nat.card N)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_1
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
cases (finite_or_infinite M).symm

Goal state after:
case refine_1.inl
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝ : Infinite M
⊢ (Nat.card M).Coprime (Nat.card N)

case refine_1.inr
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝ : Finite M
⊢ (Nat.card M).Coprime (Nat.card N)
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 = ⊤
⊢ ComplementedLattice α

Tactic:
by
  apply complementedLattice_of_sSup_atoms_eq_top
  have : ∀ i ∈ s, ∃ t : Set α, f i = sSup t ∧ ∀ a ∈ t, IsAtom a := fun i hi ↦ by
    replace h := complementedLattice_iff_isAtomistic.mp (h i hi)
    obtain ⟨u, hu, hu'⟩ := eq_sSup_atoms (⊤ : Iic (f i))
    refine ⟨(↑) '' u, ?_, ?_⟩
    · replace hu : f i = ↑(sSup u) := Subtype.ext_iff.mp hu
      simp_rw [hu, Iic.coe_sSup]
    · rintro b ⟨⟨a, ha'⟩, ha, rfl⟩
      exact IsAtom.of_isAtom_coe_Iic (hu' _ ha)
  choose t ht ht' using this
  let u : Set α := ⋃ i, ⋃ hi : i ∈ s, t i hi
  have hu₁ : u ⊆ {a | IsAtom a} := by
    rintro a ⟨-, ⟨i, rfl⟩, ⟨-, ⟨hi, rfl⟩, ha : a ∈ t i hi⟩⟩
    exact ht' i hi a ha
  have hu₂ : sSup u = ⨆ i ∈ s, f i := by simp_rw [u, sSup_iUnion, biSup_congr' ht]
  rw [eq_top_iff, ← h', ← hu₂]
  exact sSup_le_sSup hu₁

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
⊢ H ≤ Subgroup.map (normalizer ↑H).subtype (comap (mk' (H.subgroupOf (normalizer ↑H))) (zpowers x))

Tactic:
intro y hy
    simp only [Subgroup.coe_subtype, mk'_apply, Subgroup.mem_map, Subgroup.mem_comap]
    refine ⟨⟨y, le_normalizer hy⟩, ⟨0, ?_⟩, rfl⟩
    dsimp only
    rw [zpow_zero, eq_comm, QuotientGroup.eq_one_iff]
    simpa using! hy

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
hnm✝ : n ≤ m
hnm : n < m
h0m : 0 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Nat.card ↥K = p ^ (m - 1) ∧ H ≤ K
hdvd' : p ^ (m - 1 + 1) ∣ Nat.card G
K' : Subgroup G
hK' : Nat.card ↥K' = p ^ (m - 1 + 1) ∧ K ≤ K'
⊢ Nat.card ↥K' = p ^ m

Tactic:
rw [hK'.1, tsub_add_cancel_of_le h0m.nat_succ_le]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case refine_1
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 : ℕ
hp : p ∈ ps
hp' : Fact (Nat.Prime p)
this : Unique (Sylow p G) := (P p).unique_of_normal ⋯
⊢ ((P : Sylow (↑⟨p, hp⟩) G) → ↥P) ≃* ↥↑(P ↑⟨p, hp⟩)

Tactic:
apply MulEquiv.piUnique

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
x : X
h : 0 < s.length
⊢ (x ∈ range fun i ↦ s.toFun ⟨↑i, ⋯⟩) → x ≠ last s ∧ x ∈ range s.toFun

Tactic:
rintro ⟨i, rfl⟩
    have hi : (i : ℕ) < s.length := by lia
    simp [last, Fin.ext_iff, ne_of_lt hi, -Set.mem_range, Set.mem_range_self]

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ≠ last s ∧ x ∈ range s.toFun → x ∈ range fun i ↦ s.toFun ⟨↑i, ⋯⟩

Tactic:
intro h
    exact mem_eraseLast_of_ne_of_mem h.1 h.2

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 : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
⊢ ∀ {a b : M}, a ∈ {x | ∃ a, a • x = 0} → b ∈ {x | ∃ a, a • x = 0} → a + b ∈ {x | ∃ a, a • x = 0}

Tactic:
intro x y ⟨a,hx⟩ ⟨b,hy⟩
    use b * a
    rw [smul_add, mul_smul, mul_comm, mul_smul, hx, hy, smul_zero, smul_zero, add_zero]

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
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
⊢ ⨆ i ∈ S, torsionBySet R M ↑(p i) = torsionBySet R M ↑(⨅ i ∈ S, p i)

Tactic:
rcases S.eq_empty_or_nonempty with h | h

Goal state after:
case inl
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S = ∅
⊢ ⨆ i ∈ S, torsionBySet R M ↑(p i) = torsionBySet R M ↑(⨅ i ∈ S, p i)

case inr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
⊢ ⨆ i ∈ S, torsionBySet R M ↑(p i) = torsionBySet R M ↑(⨅ i ∈ S, p i)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n n✝ : ℕ
m✝ : M
⊢ ((monomial i) r • single R n✝ m✝).coeff n = if i ≤ n then r • (single R n✝ m✝).coeff (n - i) else 0

Tactic:
simp [monomial_smul_single, Finsupp.single_apply]

Goal state after:
case single
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n n✝ : ℕ
m✝ : M
⊢ (if i + n✝ = n then r • m✝ else 0) = if i ≤ n then if n✝ = n - i then r • m✝ else 0 else 0
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case succ
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I ^ (n + 1)
⊢ (monomial (n + 1)) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
rw [pow_succ'] at hr

Goal state after:
case succ
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
⊢ (monomial (n + 1)) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) 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 J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this✝ : map N.mkQ (I • N') = map N.mkQ N'
this : N' ⊔ N.mkQ.ker = J • N' ⊔ N.mkQ.ker
⊢ N ⊔ N' = N ⊔ J • N'

Tactic:
Submodule.ker_mkQ,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this✝ : map N.mkQ (I • N') = map N.mkQ N'
this : N' ⊔ N = J • N' ⊔ N
⊢ N ⊔ N' = N ⊔ J • N'
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R ⧸ R ∙ a * b
⊢ x ∈ torsionBy R (R ⧸ R ∙ a * b) a ↔ x ∈ R ∙ (mk (R ∙ a * b)) b

Tactic:
rw [mem_torsionBy_iff, Submodule.mem_span_singleton]

Goal state after:
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R ⧸ R ∙ a * b
⊢ a • x = 0 ↔ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = x
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Submodule.map (Submodule.subtype I) (I • ⊤).mkQ.ker = I ^ 2

Tactic:
Submodule.ker_mkQ,

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Submodule.map (Submodule.subtype I) (I • ⊤) = I ^ 2
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✝¹ : 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
k : ℕ
hk :
  ∀ n ≥ k,
    I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N n = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (n + 1)
this : I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (k + 1)
⊢ N ≤ I • N

Tactic:
rw [hN, hN] at this

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✝¹ : 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
k : ℕ
hk :
  ∀ n ≥ k,
    I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N n = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (n + 1)
this : I • N = N
⊢ N ≤ I • N
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ X✝ Y✝ : PresheafOfModules R
f : X✝ ⟶ Y✝
X Y : Cᵒᵖ
g : X ⟶ Y
⊢ X✝.presheaf.map g ≫ AddCommGrpCat.ofHom (AddMonoidHom.mk' ⇑(ConcreteCategory.hom (f.app Y)) ⋯) =
    AddCommGrpCat.ofHom (AddMonoidHom.mk' ⇑(ConcreteCategory.hom (f.app X)) ⋯) ≫ Y✝.presheaf.map g

Tactic:
by ext x; exact naturality_apply f g x

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

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

Tactic:
map_rightUnitor

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (η F).app ((F.obj n).obj X) = (μ F n (𝟙_ M)).app X ≫ (δ F n (𝟙_ M) ≫ F.obj n ◁ η F ≫ (ρ_ (F.obj n)).hom).app X
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((δ F m₁ m₂).app X) =
    (μ F (m₁ ⊗ m₂) m₃).app X ≫
      (F.map (α_ m₁ m₂ m₃).hom).app X ≫ (δ F m₁ (m₂ ⊗ m₃)).app X ≫ (δ F m₂ m₃).app ((F.obj m₁).obj X)

Tactic:
map_associator

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((δ F m₁ m₂).app X) =
    (μ F (m₁ ⊗ m₂) m₃).app X ≫
      (δ F (m₁ ⊗ m₂) m₃ ≫
              δ F m₁ m₂ ▷ F.obj m₃ ≫
                (α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)).hom ≫ F.obj m₁ ◁ μ F m₂ m₃ ≫ μ F m₁ (m₂ ⊗ m₃)).app
          X ≫
        (δ F m₁ (m₂ ⊗ m₃)).app X ≫ (δ F m₂ m₃).app ((F.obj m₁).obj X)
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
by
  refine dif_neg ?_
  push Not
  intro
  apply Nat.noConfusion

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

Goal state before:
pp: ⊢ (ComplexShape.up ℕ).prev 0 = 0

Tactic:
by
  refine dif_neg ?_
  push Not
  intro
  apply Nat.noConfusion

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
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

Tactic:
limMap_π

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
⊢ limit.π (F ⋙ eval C c n) j ≫ { app := fun j ↦ (F.obj j).d n m, naturality := ⋯ }.app j =
    0 ≫ limit.π (F ⋙ eval C c m) j
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ (mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d (0 + 2) (0 + 1) =
    (mk'XIso X₀ X₁ d₀ (fun {X₀ X₁} ↦ succ') 0).hom ≫ (succ' ((mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d (0 + 1) 0)).snd.fst

pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
n : ℕ
⊢ (mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d (n + 1 + 2) (n + 1 + 1) =
    (mk'XIso X₀ X₁ d₀ (fun {X₀ X₁} ↦ succ') (n + 1)).hom ≫
      (succ' ((mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d (n + 1 + 1) (n + 1))).snd.fst

Tactic:
· dsimp [mk'XIso, mk']
    rw [mk_d_2_1]
    apply mk'_congr_succ'_d
    rw [mk_d_1_0]

Goal state after:
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
n : ℕ
⊢ (mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d (n + 1 + 2) (n + 1 + 1) =
    (mk'XIso X₀ X₁ d₀ (fun {X₀ X₁} ↦ succ') (n + 1)).hom ≫
      (succ' ((mk' X₀ X₁ d₀ fun {X₀ X₁} ↦ succ').d (n + 1 + 1) (n + 1))).snd.fst
Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
j : ι
I : C
inst✝ : Injective I
⊢ Injective (((single C c j).obj I).X j)

Tactic:
simp only [single_obj_X_self]

Goal state after:
case pos
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
j : ι
I : C
inst✝ : Injective I
⊢ Injective I
Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
j : ι
P : C
inst✝ : Projective P
⊢ Projective (((single C c j).obj P).X j)

Tactic:
simp only [single_obj_X_self]

Goal state after:
case pos
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
j : ι
P : C
inst✝ : Projective P
⊢ Projective P
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 : HomologicalComplex C c
i j k : ι
inst✝ : K.HasHomology i
⊢ K.fromOpcycles i j ≫ K.d j k = 0

Tactic:
simp only [← cancel_epi (K.pOpcycles i), p_fromOpcycles_assoc, d_comp_d, comp_zero]

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ (dNext i) f = C.d i (i - 1) ≫ f (i - 1) i

Tactic:
dsimp [dNext]
  cases i
  · simp
  · congr <;> simp

Goal state after:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
hG : IsZero (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero (F.X j)
h : ¬c.Rel i (c.next i)
⊢ IsZero (X φ i)

Tactic:
exact hG.of_iso (XIso φ i h)

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 G K n₂
h : n₁ + n₂ = n₁₂
⊢ comp 0 z₂ h = 0

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

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
e f : ℤ
hf : -1 + e = f
γ : Cochain G K e
he : 0 + e = e
⊢ (inl φ).comp ((snd φ).comp γ he) hf = 0

Tactic:
← Cochain.comp_assoc_of_second_is_zero_cochain,

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
e f : ℤ
hf : -1 + e = f
γ : Cochain G K e
he : 0 + e = e
⊢ ((inl φ).comp (snd φ) ⋯).comp γ hf = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain G K d
he : 0 + d = e
⊢ (Cochain.ofHom (inr φ)).comp ((snd φ).comp γ he) ⋯ = γ

Tactic:
obtain rfl : d = e := by lia
  rw [← Cochain.comp_assoc_of_first_is_zero_cochain, inr_snd, Cochain.id_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
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
i j : ι
hjk : c.Rel j i
⊢ inlX φ i j hjk ≫ (desc φ α hα).f j = hα.hom i j

Tactic:
obtain rfl := c.next_eq' hjk
  dsimp [desc]
  rw [dif_pos hjk, comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero]

Goal state after: