mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
by_cases! hm : m < x.1

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : m < x.1
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.1 ≤ m
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : p.degree = ↑i
⊢ 1 * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
simp [natDegree_eq_of_degree_eq_some h, leadingCoeff,
      ← pow_succ', tsub_add_cancel_of_le (natDegree_eq_of_degree_eq_some h ▸ hp)]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
h : Invertible (C a * X + C b).leadingCoeff
ha : a ≠ 0
⊢ (C a * X + C b).Splits

Tactic:
· replace h : Invertible a := by simpa [leadingCoeff, ha] using h
    rw [← mul_invOf_cancel_left a b, C_mul, ← mul_add]
    exact (Splits.C a).mul (Splits.X_add_C _)

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : FaithfullyFlat R M
e : N ≃ₗ[R] M
⊢ FaithfullyFlat R N

Tactic:
rw [iff_flat_and_lTensor_faithful]
  exact ⟨Flat.of_linearEquiv e,
    fun P _ _ hP ↦ (TensorProduct.congr e (LinearEquiv.refl R P)).toEquiv.nontrivial⟩

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h : IsIntegral R (y • z)
⊢ IsAlgebraic R z

Tactic:
have ⟨p, monic, eval0⟩ := h
  refine ⟨p.comp (C y * X), fun h ↦ ?_, by simpa [aeval_comp, Algebra.smul_def] using! eval0⟩
  apply_fun (coeff · p.natDegree) at h
  have hy0 : y ≠ 0 := by rintro rfl; exact hy .zero
  rw [coeff_zero, ← mul_one p.natDegree, ← natDegree_C_mul_X y hy0,
    coeff_comp_degree_mul_degree, monic, one_mul, leadingCoeff_C_mul_X] at h
  · exact hy ⟨_, h⟩
  · rw [natDegree_C_mul_X _ hy0]; rintro ⟨⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
r : R
hr : IsUnit r
s : Set R
⊢ zeroLocus (r • s) = zeroLocus s

Tactic:
ext; simp [Set.subset_def, ← Set.image_smul, Ideal.unit_mul_mem_iff_mem _ hr]

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
T : Type u_3
inst✝⁶ : CommRing T
S' : Type u_4
T' : Type u_5
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
⊢ (Algebra.TensorProduct.map f g).SurjectiveOnStalks

Tactic:
convert!
    RingHom.SurjectiveOnStalks.tensorProductMap_id (T := T') Hf |>.comp <|
      (Algebra.TensorProduct.comm _ _ _).toRingEquiv.surjectiveOnStalks |>.comp <|
        RingHom.SurjectiveOnStalks.tensorProductMap_id (T := S) Hg |>.comp <|
          (Algebra.TensorProduct.comm _ _ _).toRingEquiv.surjectiveOnStalks
  simp only [AlgHom.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, ← AlgEquiv.toAlgHom_toRingHom, ← AlgHom.comp_toRingHom]
  congr
  ext <;> simp

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

Goal state before:
pp: case intro
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
⊢ ∃ i q, comap (Pi.evalRingHom R i) q = p

Tactic:
obtain ⟨i, hi⟩ : ∃ i, e i ∈ p.asIdeal := by
    simpa [← H, Ideal.IsPrime.prod_mem_iff] using p.asIdeal.zero_mem

Goal state after:
case intro
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
⊢ ∃ i q, comap (Pi.evalRingHom R i) q = p
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c : { a // IsIdempotentElem a }
hac : a ≤ c
hbc : b ≤ c
⊢ ↑a * ↑c + ↑b * ↑c - ↑a * (↑b * ↑c) = ↑a + ↑b - ↑a * ↑b

Tactic:
rw [hbc, hac]

Goal state after:
Module: Mathlib.RingTheory.Localization.AsSubring

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ ofField K S hS = subalgebra K S hS

Tactic:
by
  simp_rw [ofField, subalgebra, Subalgebra.copy_eq]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ = ⊥

Tactic:
by
  ext x
  rw [Algebra.mem_bot, Algebra.mem_iInf]
  constructor
  · contrapose
    intro hrange hlocal
    let denom : Ideal R := (1 : Submodule R K).comap (LinearMap.toSpanSingleton R K x)
    have hdenom : (1 : R) ∉ denom := by simpa [denom] using hrange
    rcases denom.exists_le_maximal (denom.ne_top_iff_one.mpr hdenom) with ⟨max, hmax, hle⟩
    rcases hlocal ⟨max, hmax⟩ with ⟨n, d, hd, rfl⟩
    exact hd (hle ⟨n, by simp [Algebra.smul_def, mul_left_comm, mul_inv_cancel₀ <|
      (map_ne_zero_iff _ <| IsFractionRing.injective R K).mpr fun h ↦ hd (h ▸ max.zero_mem :)]⟩)
  · rintro ⟨y, rfl⟩ ⟨v, hv⟩
    exact ⟨y, 1, v.ne_top_iff_one.mp hv.ne_top, by rw [map_one, inv_one, mul_one]⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
⊢ I.asIdeal.IsMaximal

Tactic:
obtain ⟨r, hr⟩ := surj (Function.update 0 ⟨J, max.isPrime⟩ 1)

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
⊢ I.asIdeal.IsMaximal
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
U : Opens α
⊢ U ≠ ⊥ ↔ (↑U).Nonempty

Tactic:
rw [Ne, ← not_nonempty_iff_eq_bot, not_not]

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsLocallyClosed s
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
⊢ IsLocallyClosed (f '' s)

Tactic:
obtain ⟨t, ht, rfl⟩ := hf.isLocallyClosed_iff.mp hs
  rw [image_preimage_eq_inter_range]
  exact ht.inter hf'

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsClosed[inst✝] (range f) ↔
    ∀ (x : ι), IsClosed[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))

Tactic:
· simp_rw [range_restrictPreimage]
    exact hU.isClosed_iff_coe_preimage

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (f '' f ⁻¹' T)
hx : IsGenericPoint x (closure[inst✝¹] (f '' f ⁻¹' T))
⊢ ∃ x, IsGenericPoint x (f ⁻¹' T)

Tactic:
rw [image_preimage_eq_inter_range] at hx hS''

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst✝¹] (T ∩ range f))
⊢ ∃ x, IsGenericPoint x (f ⁻¹' T)
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
⊢ IsLocallyConstructible (s ∪ t)

Tactic:
by
  rintro x
  obtain ⟨U, hxU, hU, hsU⟩ := hs x
  obtain ⟨V, hxV, hV, htV⟩ := ht x
  refine ⟨U ∩ V, Filter.inter_mem hxU hxV, hU.inter hV, ?_⟩
  have : (U ∩ V) ↓∩ (s ∪ t) =
      inclusion inter_subset_left ⁻¹' (U ↓∩ s) ∪ inclusion inter_subset_right ⁻¹' (V ↓∩ t) := by
    ext; simp
  rw [this]
  exact .union (hsU.preimage_of_isOpenEmbedding <| .inclusion _ <|
      .preimage continuous_subtype_val <| hU.inter hV)
    (htV.preimage_of_isOpenEmbedding <| .inclusion _ <|
      .preimage continuous_subtype_val <| hU.inter hV)

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I.radical = J.radical → zeroLocus ↑I = zeroLocus ↑J

Tactic:
· intro h; rw [← zeroLocus_radical, h, zeroLocus_radical]

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:
by
    rw [← ht.closure_subset_iff, ← ht.closure_eq]
    convert! ← zeroLocus_anti_mono_ideal h <;> apply zeroLocus_vanishingIdeal_eq_closure

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ b.factorization.support ⊆ (a.lcm b).factorization.support

Tactic:
intro p hp; rw [mem_support_iff] at hp ⊢
    rw [factorization_lcm ha hb]; exact (lt_sup_iff.mpr <| .inr <| Nat.pos_of_ne_zero hp).ne'

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ Continuous (comap f)

Tactic:
by
  simp only [continuous_iff_isClosed, isClosed_iff_zeroLocus]
  rintro _ ⟨s, rfl⟩
  exact ⟨_, preimage_comap_zeroLocus_aux f s⟩

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
⊢ g' ∈ ⊤

Tactic:
Subgroup.mem_top

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr.mpr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : ¬exponent G ∣ n
⊢ False

Tactic:
Nat.dvd_iff_mod_eq_zero,

Goal state after:
case inr.mpr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : ¬n % exponent G = 0
⊢ False
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : Type u_3
inst✝ : Group α
a : α
⊢ Nat.card ↥(zpowers a) = orderOf a

Tactic:
by
  have := Nat.card_congr (MulAction.orbitZPowersEquiv a (1 : α))
  rwa [Nat.card_zmod, orbit_subgroup_one_eq_self] at this

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
h : IsCyclic α
⊢ ∃ g, orderOf g = Nat.card α

Tactic:
obtain ⟨g, hg⟩ := h.exists_generator
  use g
  rw [← card_zpowers g, (eq_top_iff' (zpowers g)).mpr hg]
  exact Nat.card_congr (Equiv.Set.univ α)

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ IsPGroup 1 G ↔ Subsingleton G

Tactic:
refine ⟨?_, fun h ↦ .of_subsingleton 1 G⟩

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ IsPGroup 1 G → Subsingleton G
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ IsPGroup 1 G → Subsingleton G

Tactic:
simpa [isPGroup_iff_pow_pow_eq_one] using subsingleton_of_forall_eq 1

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

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x✝¹ x✝ : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
x : R × R
hx : x.1 * x.2 = 0 ∧ x.1 + x.2 = 1
y : R × R
hy : y.1 * y.2 = 0 ∧ y.1 + y.2 = 1
eq :
  (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) ⟨x, hx⟩ =
    (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) ⟨y, hy⟩
⊢ (↑⟨x, hx⟩).1 = (↑⟨y, hy⟩).1

Tactic:
exact basicOpen_injOn_isIdempotentElem (IsIdempotentElem.of_mul_add hx.1 hx.2).1
          (IsIdempotentElem.of_mul_add hy.1 hy.2).1 <| SetLike.ext' (congr_arg (·.1) eq)

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
P Q : Sylow p G
h : ↑P = ↑Q
⊢ P = Q

Tactic:
cases P

Goal state after:
case mk
p : ℕ
G : Type u_1
inst✝ : Group G
Q : Sylow p G
toSubgroup✝ : Subgroup G
isPGroup'✝ : IsPGroup p ↥toSubgroup✝
is_maximal'✝ : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup✝ ≤ Q → Q = toSubgroup✝
h : ↑{ toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ } = ↑Q
⊢ { toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ } = Q
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
e : ↑{p | p.IsPrime ∧ I ≤ p} ≃o ↑(zeroLocus ↑I) :=
  { toFun := fun x ↦ ⟨{ asIdeal := ↑x, isPrime := ⋯ }, ⋯⟩, invFun := fun x ↦ ⟨(↑x).asIdeal, ⋯⟩, left_inv := ⋯,
    right_inv := ⋯, map_rel_iff' := ⋯ }
⊢ ↑I.minimalPrimes ≃o (↑{s | Maximal (fun x ↦ IsClosed x ∧ IsIrreducible x) s})ᵒᵈ

Tactic:
exact OrderIso.setOfPredMinimalIsoSetOfPredMaximal
    (e.trans ((PrimeSpectrum.zeroLocusEquivIrreducibleCloseds (I : Set R)).trans
    (TopologicalSpace.IrreducibleCloseds.orderIsoSubtype' (zeroLocus (I : Set R))).dual))

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

Goal state before:
pp: G : Type u_2
inst✝¹ : CommGroup G
inst✝ : IsSimpleGroup G
⊢ ∃ p, Nat.Prime p ∧ Nonempty (Additive G ≃+ ZMod p)

Tactic:
obtain ⟨g, hg⟩ := isCyclic_iff_exists_zpowers_eq_top.mp (inferInstance : IsCyclic G)

Goal state after:
G : Type u_2
inst✝¹ : CommGroup G
inst✝ : IsSimpleGroup G
g : G
hg : zpowers g = ⊤
⊢ ∃ p, Nat.Prime p ∧ Nonempty (Additive G ≃+ ZMod p)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : Infinite G
inst✝ : Group G
g : G
hg : zpowers g = ⊤
⊢ (intEquivOfZPowersEqTop g hg).symm g = Multiplicative.ofAdd 1

Tactic:
simp [MulEquiv.symm_apply_eq]

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

Goal state before:
pp: G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : g < 1
⊢ StrictAnti ⇑(intEquivOfZPowersEqTop g hg)

Tactic:
intro x y hxy
  simp only [intEquivOfZPowersEqTop, MulEquiv.ofBijective_apply, zpowersHom_apply]
  exact zpow_right_strictAnti hg1 hxy

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Group M
inst✝² : Group N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
⊢ ¬IsAddCyclic (Additive (M × N))

Tactic:
(AddEquiv.prodAdditive ..).isAddCyclic

Goal state after:
M : Type u_4
N : Type u_5
inst✝³ : Group M
inst✝² : Group N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
⊢ ¬IsAddCyclic (Additive M × Additive N)
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
hy : y ≠ 0
⊢ IsUnit x

Tactic:
obtain ⟨z, hzy : z * y = 1⟩ := h y hy 1

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
z : R
hzy : z * y = 1
⊢ IsUnit x
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
hp' : ⨆ i ∈ s, p i = ⊤
⊢ IsSemisimpleModule R M

Tactic:
by
  simp_rw [isSemisimpleModule_iff] at hp ⊢
  refine complementedLattice_of_complementedLattice_Iic (fun i hi ↦ ?_) hp'
  simpa only [← (p i).mapIic.complementedLattice_iff] using hp i hi

Goal state after:
Module: Mathlib.RingTheory.Nakayama

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
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'
⊢ map N.mkQ P ≤ map N.mkQ (I • N')

pp: case a
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'
⊢ map N.mkQ (I • N') ≤ map N.mkQ P

Tactic:
· simpa using map_mono (f := N.mkQ) hNN'

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
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'
⊢ map N.mkQ (I • N') ≤ map N.mkQ P
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
F : I.Filtration M
h : F.Stable
⊢ ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Tactic:
obtain ⟨n₀, hn₀⟩ := h.exists_pow_smul_eq
  use n₀
  intro n hn
  convert! hn₀ (n - n₀)
  rw [add_comm, tsub_add_cancel_of_le hn]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
x✝ : β
⊢ x✝ + (m + n) • s = x✝ + n • s + m • s

Tactic:
rw [add_comm m n, add_zsmul, add_assoc]

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

Goal state before:
pp: case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
this : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)
⊢ x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1) ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
refine Submodule.smul_mem _ x ?_

Goal state after:
case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
this : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)
⊢ 1 ⊗ₜ[R] y - y ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
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
j : ι
h : ¬c.Rel (c.prev j) j
⊢ c.prev j = j

Tactic:
dsimp [ComplexShape.prev]
        rw [dif_neg]
        push Not; intro i hi
        have : c.prev j = i := c.prev_eq' hi
        rw [this] at h; contradiction

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
⊢ F.map ((add hF s i (m₁ + m₂) m₃).hom.app X ≫ (s m₃).map ((add hF s i m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯ ≫ (add hF s i m₁ (m₂ + m₃)).hom.app X ≫ (add hF s i m₂ m₃).hom.app ((s m₁).obj X))

Tactic:
have h := shiftFunctorAdd'_assoc_hom_app m₁ m₂ m₃ _ _ (m₁ + m₂ + m₃) rfl rfl rfl (F.obj X)

Goal state after:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  (shiftFunctorAdd' D (m₁ + m₂) m₃ (m₁ + m₂ + m₃) ⋯).hom.app (F.obj X) ≫
      (shiftFunctor D m₃).map ((shiftFunctorAdd' D m₁ m₂ (m₁ + m₂) ⋯).hom.app (F.obj X)) =
    (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯).hom.app (F.obj X) ≫
      (shiftFunctorAdd' D m₂ m₃ (m₂ + m₃) ⋯).hom.app ((shiftFunctor D m₁).obj (F.obj X))
⊢ F.map ((add hF s i (m₁ + m₂) m₃).hom.app X ≫ (s m₃).map ((add hF s i m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯ ≫ (add hF s i m₁ (m₂ + m₃)).hom.app X ≫ (add hF s i m₂ m₃).hom.app ((s m₁).obj X))
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₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap' h).f k₀ = 0

Tactic:
by
  simp only [nullHomotopicMap']
  apply nullHomotopicMap_f_eq_zero hk₀ hk₀'

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
j : ι
hjk : c.Rel j (c.next j)
⊢ inlX φ (c.next j) j hjk ≫ (fstX φ j (c.next j) hjk ≫ hα.hom (c.next j) j + sndX φ j ≫ α.f j) = hα.hom (c.next j) j

Tactic:
comp_add,

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
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
⊢ inlX φ (c.next j) j hjk ≫ fstX φ j (c.next j) hjk ≫ hα.hom (c.next j) j + inlX φ (c.next j) j hjk ≫ sndX φ j ≫ α.f j =
    hα.hom (c.next j) j
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✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)
i j : ℕ
w : ¬(ComplexShape.down ℕ).Rel j i
⊢ (if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom else 0) = 0

Tactic:
by rw [dif_neg]; exact w

Goal state after: