mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
⊢ (Algebra.TensorProduct.map f (AlgHom.id R D)).Flat

Tactic:
· have : (Algebra.TensorProduct.map f (AlgHom.id R D)).restrictScalars R =
        (Algebra.TensorProduct.comm _ _ _).toAlgHom.comp
          ((Algebra.TensorProduct.lTensor _ (f.restrictScalars R)).comp
            (Algebra.TensorProduct.comm _ _ _).toAlgHom) := by
      ext <;> simp
    change ((Algebra.TensorProduct.map f (AlgHom.id R D)).restrictScalars R).Flat
    rw [this]
    refine RingHom.Flat.comp ?_ (.of_bijective <| AlgEquiv.bijective _)
    change RingHom.Flat (RingHom.comp (Algebra.TensorProduct.lTensor D
      (AlgHom.restrictScalars R f)).toRingHom _)
    exact RingHom.Flat.comp (.of_bijective <| (TensorProduct.comm R A D).bijective) (lTensor D hf)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ s ⊆ t

Tactic:
rw [← ht.closure_subset_iff, ← ht.closure_eq]
    convert! ← zeroLocus_anti_mono_ideal h <;> apply zeroLocus_vanishingIdeal_eq_closure

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
⊢ ∃ g, g ^ m ≠ 1

Tactic:
by_contra! h
  have hcon : exponent G ≤ m := exponent_min' m hpos h
  lia

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))
x : (i : ι) → R i
hx : x i = 0
j : ι
⊢ (Pi.single i f * x) j = 0 j

Tactic:
by_cases h : i = j

Goal state after:
case pos
ι : 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))
x : (i : ι) → R i
hx : x i = 0
j : ι
h : i = j
⊢ (Pi.single i f * x) j = 0 j

case neg
ι : 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))
x : (i : ι) → R i
hx : x i = 0
j : ι
h : ¬i = j
⊢ (Pi.single i f * x) j = 0 j
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ ∀ b ∈ Finset.univ, orderOf b ∣ exponent G

Tactic:
intro g _

Goal state after:
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
a✝ : g ∈ Finset.univ
⊢ orderOf g ∣ exponent G
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr.hnot
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ ¬(g ^ k) ^ p ^ t = 1

pp: case hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ (g ^ k) ^ p ^ (t + 1) = 1

Tactic:
· rwa [hk, mul_comm, ht, pow_succ, ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg

Goal state after:
case hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ (g ^ k) ^ p ^ (t + 1) = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G ≠ 0 ↔ (Set.range orderOf).Finite

Tactic:
refine ⟨fun he => ?_, fun he => ?_⟩
  · by_contra h
    obtain ⟨m, ⟨t, rfl⟩, het⟩ := Set.Infinite.exists_gt h (exponent G)
    exact pow_ne_one_of_lt_orderOf he het (pow_exponent_eq_one t)
  · lift Set.range (orderOf (G := G)) to Finset ℕ using he with t ht
    have htpos : 0 < t.prod id := by
      refine Finset.prod_pos fun a ha => ?_
      rw [← Finset.mem_coe, ht] at ha
      obtain ⟨k, rfl⟩ := ha
      exact h k
    suffices exponent G ∣ t.prod id by
      intro h
      rw [h, zero_dvd_iff] at this
      exact htpos.ne' this
    rw [exponent_dvd]
    intro g
    apply Finset.dvd_prod_of_mem id (?_ : orderOf g ∈ _)
    rw [← Finset.mem_coe, ht]
    exact Set.mem_range_self g

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 α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
a : ↑(fixedPoints G α)
ha : a ∈ Finset.univ
x✝ : ↑1 ≠ 0
⊢ ↑1 = ↑(card { x // Quotient.mk'' x = Quotient.mk'' ↑a })

Tactic:
rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2]

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 ⊔ J = ⊤

Tactic:
← zeroLocus_empty_iff_eq_top,

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
⊢ zeroLocus ↑(I ⊔ J) = ∅
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ⟨↑g ^ p ^ j, hj⟩ ^ p ^ k = 1
⊢ ∃ k, g ^ p ^ k = 1

Tactic:
rw [Subtype.ext_iff, ϕ.ker.coe_pow, Subtype.coe_mk, ← pow_mul, ← pow_add] at hk

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ p ^ (j + k) = ↑1
⊢ ∃ k, g ^ p ^ k = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p})
⊢ Ideal.comap (mapRingHom f) (Ideal.span {p}) ⊔ Ideal.span {X} = ⊤

Tactic:
← zeroLocus_empty_iff_eq_top,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p})
⊢ zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p}) ⊔ Ideal.span {X}) = ∅
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Finset G
⊢ rank ↥(closure ↑s) ≤ s.card

Tactic:
let t : Finset (closure (s : Set G)) := s.preimage Subtype.val Subtype.coe_injective.injOn

Goal state after:
G : Type u_1
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
⊢ rank ↥(closure ↑s) ≤ s.card
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, ⋯⟩
⊢ a * b = b * a

Tactic:
have hm : x ^ m = f a := by simpa [Subtype.ext_iff] using hm

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
⊢ a * b = b * a
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)
⊢ ∃ n ∈ normalizer ↑P, g⁻¹ * x * g = n⁻¹ * x * n

Tactic:
obtain ⟨h, hh⟩ :=
    exists_smul_eq (centralizer (zpowers x : Set G)) ((g • P).subtype h2) (P.subtype h1)

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)
h : ↥(centralizer ↑(zpowers x))
hh : h • (g • P).subtype h2 = P.subtype h1
⊢ ∃ n ∈ normalizer ↑P, g⁻¹ * x * g = n⁻¹ * x * n
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

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

Tactic:
card_powMonoidHom_range

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
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))
⊢ Nat.card ↑(Subtype.val '' ↑(comap (mk' (H.subgroupOf (normalizer ↑H))) (zpowers x))) = p ^ (n + 1)

Tactic:
Nat.card_image_of_injective Subtype.val_injective
        ((zpowers x).comap (mk' (H.subgroupOf (normalizer H))) : Set (normalizer (H : Set G))),

Goal state after:
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))
⊢ Nat.card ↑↑(comap (mk' (H.subgroupOf (normalizer ↑H))) (zpowers x)) = p ^ (n + 1)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G✝ : Type u_2
G' : Type u_3
a : α
G : Type u_4
inst✝¹ : Group G
inst✝ : IsCyclic G
⊢ IsCyclic (WithZero G)ˣ

Tactic:
apply isCyclic_of_injective (G := (WithZero G)ˣ) (WithZero.unitsWithZeroEquiv).toMonoidHom

Goal state after:
α : Type u_1
G✝ : Type u_2
G' : Type u_3
a : α
G : Type u_4
inst✝¹ : Group G
inst✝ : IsCyclic G
⊢ Function.Injective ⇑WithZero.unitsWithZeroEquiv.toMonoidHom
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
⊢ Nat.card ↥↑P = p ^ (Nat.card G).factorization p

Tactic:
by
  obtain ⟨n, heq : Nat.card P = _⟩ := IsPGroup.iff_card.mp P.isPGroup'
  refine Nat.dvd_antisymm ?_ (P.pow_dvd_card_of_pow_dvd_card (Nat.ordProj_dvd _ p))
  rw [heq, ← hp.out.pow_dvd_iff_dvd_ordProj (show Nat.card G ≠ 0 from Nat.card_pos.ne'), ← heq]
  exact P.1.card_subgroup_dvd_card

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Ring S
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module S N
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] N
hl : Function.Bijective ⇑l
⊢ IsSimpleModule R M ↔ IsSimpleModule S N

Tactic:
simp_rw [isSimpleModule_iff, (Submodule.orderIsoMapComapOfBijective l hl).isSimpleOrder_iff]

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

Goal state before:
pp: R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
⊢ IsUnit x

Tactic:
have hy : y ≠ 0 := left_ne_zero_of_mul (hyx.symm ▸ one_ne_zero)

Goal state after:
R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
hy : y ≠ 0
⊢ IsUnit x
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
s : Set R
⊢ IsTorsionBySet R M s ↔ s ⊆ ↑(annihilator R M)

Tactic:
by
  simp_rw [IsTorsionBySet, Set.subset_def, SetLike.mem_coe, mem_annihilator]
  rw [forall_comm, SetCoe.forall]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn : ∃ S, S.Finite ∧ span R S = N
hin : N ≤ I • N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0

Tactic:
rcases hn with ⟨s, hfs, hs⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
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
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'
r : R
i : ℕ
m : M
⊢ (eval ((algebraMap R R') r)) ((map R' f) (single R i m)) = f ((eval r) (single R i m))

Tactic:
simp only [map_single, eval_single, f.map_smul]; module

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
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
x✝¹ : ι
x✝ : x✝¹ ∈ S
⊢ torsionBy R M (q x✝¹) = torsionBySet R M ↑(Ideal.span {q x✝¹})

Tactic:
exact (torsionBySet_span_singleton_eq _).symm

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
m n m' : M
f : m ⟶ m'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.obj n).map ((F.map f).app X) ≫ (μ F m' n).app X = (μ F m n).app X ≫ (F.map (f ⊗ₘ 𝟙 n)).app X

Tactic:
← μ_naturality₂ F f (𝟙 n) X

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 n m' : M
f : m ⟶ m'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.obj n).map ((F.map f).app X) ≫ (μ F m' n).app X =
    (F.map (𝟙 n)).app ((F.obj m).obj X) ≫ (F.obj n).map ((F.map f).app X) ≫ (μ F m' n).app X
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : (single V c j).obj A ⟶ K
hfg : f.f j = g.f j
i : ι
⊢ f.f i = g.f i

Tactic:
by_cases h : i = j

Goal state after:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : (single V c j).obj A ⟶ K
hfg : f.f j = g.f j
i : ι
h : i = j
⊢ f.f i = g.f i

case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : (single V c j).obj A ⟶ K
hfg : f.f j = g.f j
i : ι
h : ¬i = j
⊢ f.f i = g.f i
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
i : ι
⊢ f.f i = g.f i

Tactic:
by_cases h : i = j

Goal state after:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
i : ι
h : i = j
⊢ f.f i = g.f i

case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : K ⟶ (single V c j).obj A
hfg : f.f j = g.f j
i : ι
h : ¬i = j
⊢ f.f i = g.f i
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
X : C
⊢ (shiftFunctorAdd C a 0).inv.app X = (shiftFunctorZero C A).hom.app ((shiftFunctor C a).obj X) ≫ eqToHom ⋯

Tactic:
by
  simp [← shiftFunctorAdd'_add_zero_inv_app, shiftFunctorAdd']

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 : HomologicalComplex V c
inst✝ : HasKernels V
i j : ι
r : c.Rel i j
⊢ kernelSubobject (C.dFrom i) = kernelSubobject (C.d i j)

Tactic:
by
  rw [C.dFrom_eq r]
  apply kernelSubobject_comp_mono

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
P Q : ChainComplex V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' f'' ≫ Q.d (n + 2) (n + 1) = P.d (n + 2) (n + 1) ≫ p.snd.fst
n m : ℕ
⊢ (ComplexShape.down ℕ).Rel n m →
    (P.mkHomAux Q zero one one_zero_comm succ n).fst ≫ Q.d n m =
      P.d n m ≫ (P.mkHomAux Q zero one one_zero_comm succ m).fst

Tactic:
rintro (rfl : m + 1 = n)

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : ChainComplex V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' f'' ≫ Q.d (n + 2) (n + 1) = P.d (n + 2) (n + 1) ≫ p.snd.fst
m : ℕ
⊢ (P.mkHomAux Q zero one one_zero_comm succ (m + 1)).fst ≫ Q.d (m + 1) m =
    P.d (m + 1) m ≫ (P.mkHomAux Q zero one one_zero_comm succ m).fst
Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
e : pair K L ⋙ eval C c i ≅ pair (K.X i) (L.X i)
⊢ HasColimit (pair K L ⋙ eval C c i)

Tactic:
exact hasColimit_of_iso e

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

Goal state before:
pp: case a
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
⊢ (mapBaseChange R A B).range ≤ (map R A B B).ker

pp: case a
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
⊢ (map R A B B).ker ≤ (mapBaseChange R A B).range

Tactic:
· rintro _ ⟨x, rfl⟩
    induction x with
    | zero => simp
    | tmul r s =>
      obtain ⟨x, rfl⟩ := linearCombination_surjective _ _ s
      simp only [mapBaseChange_tmul, LinearMap.mem_ker, map_smul]
      induction x using Finsupp.induction_linear
      · simp
      · simp [smul_add, *]
      · simp
    | add => rw [map_add]; exact add_mem ‹_› ‹_›

Goal state after:
case a
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
⊢ (map R A B B).ker ≤ (mapBaseChange R A B).range
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 E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Linear R V
h : Homotopy f g
a : R
i : ι
⊢ a • f.f i =
    (C.dFrom i ≫ (fromNext i) fun i j ↦ a • h.hom i j) + ((toPrev i) fun i j ↦ a • h.hom i j) ≫ D.dTo i + a • g.f i

Tactic:
h.comm

Goal state after:
ι : 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✝ : ι
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Linear R V
h : Homotopy f g
a : R
i : ι
⊢ a • ((dNext i) h.hom + (prevD i) h.hom + g.f i) =
    (C.dFrom i ≫ (fromNext i) fun i j ↦ a • h.hom i j) + ((toPrev i) fun i j ↦ a • h.hom i j) ≫ D.dTo i + a • g.f i
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (nullHomotopicMap hom).f k₀ = hom k₀ k₁ ≫ D.d k₁ k₀

Tactic:
by
  dsimp only [nullHomotopicMap]
  rw [prevD_eq hom r₁₀, dNext, AddMonoidHom.mk'_apply, C.shape, zero_comp, zero_add]
  exact hk₀ _

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

Goal state before:
pp: case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel (c.prev k₀) k₀

Tactic:
apply_assumption

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

Goal state before:
pp: case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel k₀ (c.next k₀)

Tactic:
apply_assumption

Goal state after: