mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : M →ₗ[A] N
⊢ (r • D).compDer = (RingHom.id A) r • D.compDer

Tactic:
ext; rfl

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

Goal state before:
pp: case h_nhds
R : Type u
inst✝ : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : f ∉ ↑p.asIdeal
⊢ ↑(basicOpen f) ⊆ U

Tactic:
← Set.compl_subset_compl,

Goal state after:
case h_nhds
R : Type u
inst✝ : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : f ∉ ↑p.asIdeal
⊢ Uᶜ ⊆ (↑(basicOpen f))ᶜ
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : Monoid G
h : ExponentExists G
⊢ exponent G = sInf {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}

Tactic:
have h' : {d : ℕ | 0 < d ∧ ∀ x : G, x ^ d = 1}.Nonempty := h
    rw [Monoid.exponent, dif_pos h, Nat.sInf_def h']
    congr

Goal state after:
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
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
⊢ p ∈ Set.range (comap (Pi.evalRingHom R i))

Tactic:
range_comap_of_surjective _ _ (RingHom.surjective _),

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
⊢ p ∈ zeroLocus ↑(RingHom.ker (Pi.evalRingHom R i))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
⊢ Function.Injective (sigmaToPi R)

Tactic:
exact sigmaToPi_injective R

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Simple

Goal state before:
pp: case refine_2
G : Type u_1
inst✝³ : Group G
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ⇑f
H : Subgroup H✝
iH : H.Normal
h : comap f H = ⊤
⊢ H = ⊤

Tactic:
rw [← comap_top f] at h
      exact comap_injective hf h

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
s : Set (PrimeSpectrum R)
hsc : IsClosed (comap f ⁻¹' s)
⊢ sᶜ = comap f '' (comap f ⁻¹' s)ᶜ

Tactic:
rw [← Set.preimage_compl, Set.image_preimage_eq _ h₁]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b

Tactic:
have hα : 1 < Nat.card (fixedPoints G α) :=
    (Fact.out (p := p.Prime)).one_lt.trans_le (Nat.le_of_dvd (Finite.card_pos_iff.2 ⟨⟨a, ha⟩⟩) hpf)

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : 1 < Nat.card ↑(fixedPoints G α)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : Nontrivial ↑(fixedPoints G α)
b : α
hb : b ∈ fixedPoints G α
hba : ⟨b, hb⟩ ≠ ⟨a, ha⟩
hab : a = b
⊢ ⟨b, hb⟩ = ⟨a, ha⟩

Tactic:
simp_rw [hab]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_3
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
⊢ exponent M₂ ∣ exponent (M₁ × M₂)

Tactic:
exact MonoidHom.exponent_dvd (f := MonoidHom.snd M₁ M₂) Prod.snd_surjective

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

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

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 | orderOf a = d} = φ d

Tactic:
· cases Fintype.card_ne_zero (eq_zero_of_zero_dvd hd)

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 | orderOf a = d} = φ d
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
m : ℕ
hm₁ : m ∈ c.divisors
hm₂ : m ∉ c.divisors.erase d
⊢ #{a | orderOf a = m} = 0

Tactic:
have : m = d := by
        contrapose! hm₂
        exact mem_erase_of_ne_of_mem hm₂ hm₁

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
m : ℕ
hm₁ : m ∈ c.divisors
hm₂ : m ∉ c.divisors.erase d
this : m = d
⊢ #{a | orderOf a = m} = 0
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (M × N)
⊢ False

Tactic:
rw [← ((zmodAddCyclicAddEquiv <| isAddCyclic_left_of_prod M N).prodCongr (zmodAddCyclicAddEquiv <|
    isAddCyclic_right_of_prod M N)).isAddCyclic, Nat.card_eq_zero_of_infinite] at hMN

Goal state after:
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_2
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
x✝ : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
f : M × N →* N := MonoidHom.snd M N
⊢ IsCyclic (M × N)

Tactic:
let e : f.ker ≃* M := by
      rw [MonoidHom.ker_snd]
      exact ((Subgroup.prodEquiv ..).trans .prodUnique).trans Subgroup.topEquiv

Goal state after:
case refine_2
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
x✝ : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
f : M × N →* N := MonoidHom.snd M N
e : ↥f.ker ≃* M := ⋯.mpr (((⊤.prodEquiv ⊥).trans MulEquiv.prodUnique).trans Subgroup.topEquiv)
⊢ IsCyclic (M × 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✝ : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ Function.Surjective ⇑(toSpanSingleton R M m)

Tactic:
← range_eq_top,

Goal state after:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ (toSpanSingleton R M m).range = ⊤
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✝ : IsSimpleModule R N
f : M →ₗ[R] N
⊢ Function.Surjective ⇑f ∨ f = 0

Tactic:
← range_eq_top,

Goal state after:
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✝ : IsSimpleModule R N
f : M →ₗ[R] N
⊢ f.range = ⊤ ∨ f = 0
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
h : torsionOf R M m = ⊤
⊢ m = 0

Tactic:
← one_smul R m,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
h : torsionOf R M m = ⊤
⊢ 1 • m = 0
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
imxs : IsMaximal (x ⊓ (eraseLast s).last) (eraseLast s).last
t : CompositionSeries X
htb : head t = (eraseLast s).head
htl : t.length + 1 = n
htt : last t = x ⊓ (eraseLast s).last
hteqv : Equivalent (eraseLast s) (snoc t (eraseLast s).last ⋯)
hmtx : IsMaximal (last t) x
⊢ (snoc t x hmtx).head = head s ∧
    (snoc t x hmtx).length + 1 = n + 1 ∧
      ∃ (htx : (snoc t x hmtx).last = x), s.Equivalent ((snoc t x hmtx).snoc (last s) ⋯)

Tactic:
refine ⟨by simp [htb], by simp [htl], by simp, ?_⟩

Goal state after:
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
imxs : IsMaximal (x ⊓ (eraseLast s).last) (eraseLast s).last
t : CompositionSeries X
htb : head t = (eraseLast s).head
htl : t.length + 1 = n
htt : last t = x ⊓ (eraseLast s).last
hteqv : Equivalent (eraseLast s) (snoc t (eraseLast s).last ⋯)
hmtx : IsMaximal (last t) x
⊢ s.Equivalent ((snoc t x hmtx).snoc (last s) ⋯)
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case succ.refine_1
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
r : R
⊢ r ∈ I → ∀ n_1 ∈ I ^ n, (monomial (n + 1)) (r • n_1) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
hr

Goal state after:
case succ.refine_1
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
r : R
hr : r ∈ I
⊢ ∀ n_1 ∈ I ^ n, (monomial (n + 1)) (r • n_1) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
map : Fin 2 → Ideal R :=
  fun x ↦
    match x with
    | 0 => P
    | 1 => Q
heq : ⨆ i ∈ ⊤, torsionBySet R M ↑(map i) = torsionBySet R M ↑(⨅ i ∈ ⊤, map i)
⊢ torsionBySet R M ↑P ⊔ torsionBySet R M ↑Q = torsionBySet R M ↑(P ⊓ Q)

Tactic:
have : ⨆ i, ⨆ (_ : i = 0 ∨ i = 1), torsionBySet R M ↑(map i) =
        torsionBySet R M ↑(map 0) ⊔ torsionBySet R M ↑(map 1) := iSup_pair

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
map : Fin 2 → Ideal R :=
  fun x ↦
    match x with
    | 0 => P
    | 1 => Q
heq : ⨆ i ∈ ⊤, torsionBySet R M ↑(map i) = torsionBySet R M ↑(⨅ i ∈ ⊤, map i)
this : ⨆ i, ⨆ (_ : i = 0 ∨ i = 1), torsionBySet R M ↑(map i) = torsionBySet R M ↑(map 0) ⊔ torsionBySet R M ↑(map 1)
⊢ torsionBySet R M ↑P ⊔ torsionBySet R M ↑Q = torsionBySet R M ↑(P ⊓ Q)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single.monomial
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ (map R' f) ((monomial n✝) a✝ • single R i m) =
    Polynomial.map (algebraMap R R') ((monomial n✝) a✝) • (map R' f) (single R i m)

Tactic:
monomial_smul_single,

Goal state after:
case single.monomial
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ (map R' f) (single R (n✝ + i) (a✝ • m)) =
    Polynomial.map (algebraMap R R') ((monomial n✝) a✝) • (map R' f) (single R i m)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single.monomial
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ single R' (n✝ + i) (f (a✝ • m)) = (monomial n✝) ((algebraMap R R') a✝) • single R' i (f m)

Tactic:
monomial_smul_single,

Goal state after:
case single.monomial
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ single R' (n✝ + i) (f (a✝ • m)) = single R' (n✝ + i) ((algebraMap R R') a✝ • f m)
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Algebra.adjoin R (⇑(monomial 1) '' ↑s) = Algebra.adjoin R ↑(Submodule.map (monomial 1) (Submodule.span R ↑s))

Tactic:
Submodule.map_span,

Goal state after:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Algebra.adjoin R (⇑(monomial 1) '' ↑s) = Algebra.adjoin R ↑(Submodule.span R (⇑(monomial 1) '' ↑s))
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
hM : IsTorsionBySet R M ↑(⨅ a ∈ S, Ideal.span {q a})
⊢ DirectSum.IsInternal fun i ↦ torsionBy R M (q ↑i)

Tactic:
convert!
    torsionBySet_isInternal
      (fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime (q i) _).mpr <| hq hi hj ij) hM

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
hM : IsTorsionBySet R M ↑(⨅ a ∈ S, Ideal.span {q a})
x✝ : ↥S
⊢ torsionBy R M (q ↑x✝) = torsionBySet R M ↑(Ideal.span {q ↑x✝})
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case a
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
i : ℕ
m : M
hm : m ∈ ↑(F.N i)
j : ℕ
⊢ (single R i m).coeff j ∈ F.N j

Tactic:
rw [coeff_single, Finsupp.single_apply]

Goal state after:
case a
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
i : ℕ
m : M
hm : m ∈ ↑(F.N i)
j : ℕ
⊢ (if i = j then m else 0) ∈ F.N j
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_2
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
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
⊢ f.toRingHom ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
exact f.map_algebraMap r

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case neg
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ ∀ (i : ℕ), I ≤ I ^ i

Tactic:
rintro (_ | n) <;> simp [H.pow_succ_eq]

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel i (if h : ∃ j, c.Rel i j then h.choose else i)

Tactic:
rw [dif_pos]

Goal state after:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel i (Exists.choose ?hc)

case hc
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ ∃ j, c.Rel i j
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
X : Cᵒᵖ
hX : Limits.IsInitial X
M : PresheafOfModules R
Y Z : Cᵒᵖ
f : Y ⟶ Z
r : ↑(R.obj X)
x : ↑(forgetToPresheafModuleCatObjObj X hX M Y)
⊢ (ConcreteCategory.hom (M.map f)) (r • x) = (RingHom.id ↑(R.obj X)) r • (ConcreteCategory.hom (M.map f)) x

Tactic:
simp only [ModuleCat.restrictScalars.smul_def (R := R.obj X), RingHom.id_apply, M.map_smul]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
X : Cᵒᵖ
hX : Limits.IsInitial X
M : PresheafOfModules R
Y Z : Cᵒᵖ
f : Y ⟶ Z
r : ↑(R.obj X)
x : ↑(forgetToPresheafModuleCatObjObj X hX M Y)
⊢ (ConcreteCategory.hom (R.map f)) ((RingCat.Hom.hom (R.map (hX.to Y))) r) • (ConcreteCategory.hom (M.map f)) x =
    (RingCat.Hom.hom (R.map (hX.to Z))) r • (ConcreteCategory.hom (M.map f)) x
Module: Mathlib.CategoryTheory.GradedObject

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

Tactic:
hom_inv_id_eval,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
X Y✝ : GradedObject J C
e : X ≅ Y✝
F : C ⥤ D ⥤ E
j : J
Y : D
⊢ (F.map (𝟙 (X j))).app Y = 𝟙 ((F.obj (X j)).obj Y)
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 : HomologicalComplex V c
i j : ι
rij rij' : c.Rel i j
⊢ C.d i j ≫ eqToHom ⋯ = C.d i j

Tactic:
simp only [eqToHom_refl, comp_id]

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
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ (shiftFunctor C a₃).map ((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X) ≫
      (shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).inv.app X =
    (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((shiftFunctor C a₁).obj X) ≫
      (shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).inv.app X

Tactic:
by
  simpa using NatTrans.congr_app (congr_arg Iso.inv
    (shiftFunctorAdd'_assoc C _ _ _ _ _ _ h₁₂ h₂₃ h₁₂₃)) X

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 : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
k : α
⊢ ((if h : k + 1 + 1 = k + 1 + 1 then eqToHom ⋯ ≫ d (k + 1) else 0) ≫
      if h : k + 1 = k + 1 then eqToHom ⋯ ≫ d k else 0) =
    0

Tactic:
simp only [eqToHom_refl, id_comp, dite_eq_ite, ite_true, sq]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹⁰ : Category.{v, u} V
inst✝⁹ : Preadditive V
W : Type u_2
inst✝⁸ : Category.{v_1, u_2} W
inst✝⁷ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁶ : Category.{v_2, u_3} W₁
inst✝⁵ : Category.{v_3, u_4} W₂
inst✝⁴ : HasZeroMorphisms W₁
inst✝³ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f✝ : C ⟶ D
i✝ : ι
F : V ⥤ W
inst✝² : F.Additive
c : ComplexShape ι
inst✝¹ : F.Faithful
inst✝ : F.Full
X Y : HomologicalComplex V c
f : (F.mapHomologicalComplex c).obj X ⟶ (F.mapHomologicalComplex c).obj Y
i j : ι
x✝ : c.Rel i j
⊢ F.preimage (f.f i) ≫ Y.d i j = X.d i j ≫ F.preimage (f.f j)

Tactic:
apply F.map_injective

Goal state after:
ι : Type u_1
V : Type u
inst✝¹⁰ : Category.{v, u} V
inst✝⁹ : Preadditive V
W : Type u_2
inst✝⁸ : Category.{v_1, u_2} W
inst✝⁷ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁶ : Category.{v_2, u_3} W₁
inst✝⁵ : Category.{v_3, u_4} W₂
inst✝⁴ : HasZeroMorphisms W₁
inst✝³ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f✝ : C ⟶ D
i✝ : ι
F : V ⥤ W
inst✝² : F.Additive
c : ComplexShape ι
inst✝¹ : F.Faithful
inst✝ : F.Full
X Y : HomologicalComplex V c
f : (F.mapHomologicalComplex c).obj X ⟶ (F.mapHomologicalComplex c).obj Y
i j : ι
x✝ : c.Rel i j
⊢ F.map (F.preimage (f.f i) ≫ Y.d i j) = F.map (X.d i j ≫ F.preimage (f.f j))
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
i j : A
⊢ (shiftFunctorComm C i j).inv = (shiftFunctorComm C j i).hom

Tactic:
rw [shiftFunctorComm_eq C i j (i + j) rfl, shiftFunctorComm_eq C j i (i + j) (add_comm j i)]

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ ((shiftFunctorAdd' C i j (i + j) ⋯).symm ≪≫ shiftFunctorAdd' C j i (i + j) ⋯).inv =
    ((shiftFunctorAdd' C j i (i + j) ⋯).symm ≪≫ shiftFunctorAdd' C i j (i + j) ⋯).hom
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✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i : ι
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesLimitsOfShape J (single C c i)

Tactic:
intros; infer_instance

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
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i : ι
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesColimitsOfShape J (single C c i)

Tactic:
intros; infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝² : HasFiniteLimits C
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits F
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesLimitsOfShape J (F.mapHomologicalComplex c)

Tactic:
intros; infer_instance

Goal state after: