mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).2 * (↑b).2 + ((↑a).1 * (↑a).2 * (↑c).2 + (↑a).2 * (↑b).1 * (↑c).2) = (↑a).2 * (↑b).2 + (↑a).2 * (↑b).1 * (↑c).2

Tactic:
a.2.1,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).2 * (↑b).2 + (0 * (↑c).2 + (↑a).2 * (↑b).1 * (↑c).2) = (↑a).2 * (↑b).2 + (↑a).2 * (↑b).1 * (↑c).2
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑b * ↑a = ↑a * ↑b

Tactic:
mul_right_comm

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑a * ↑b = ↑a * ↑b
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization (↑f) hf).comp (mapPiLocalization ↑f.symm ⋯) = RingHom.id (PiLocalization S)

Tactic:
rw [← mapPiLocalization_comp]

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization ((↑f).comp ↑f.symm) ⋯ = RingHom.id (PiLocalization S)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization ↑f.symm ⋯).comp (mapPiLocalization (↑f) hf) = RingHom.id (PiLocalization R)

Tactic:
rw [← mapPiLocalization_comp]

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization ((↑f.symm).comp ↑f) ⋯ = RingHom.id (PiLocalization R)
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
⊢ ∀ (a : α), ⊤ \ a = hnot a

Tactic:
simp +instances [eq_le, eq_sdiff, eq_top, eq_hnot]

Goal state after:
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: case inr
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
hne : s.Nonempty
⊢ IsPreirreducible s

Tactic:
choose x hx using hne

Goal state after:
case inr
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
x : X
hx : x ∈ s
⊢ IsPreirreducible s
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
⊢ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

Tactic:
intro U x hx

Goal state after:
case mpr
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
U : Opens α
x : α
hx : x ∈ U
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
hU' : ↑s ⊆ ⋃ i, U i
t : Finset ι
ht : s ≤ t.sup fun i ↦ { carrier := U i, is_open' := ⋯ }
⊢ ↑(t.sup fun i ↦ { carrier := U i, is_open' := ⋯ }) ⊆ ⋃ i ∈ t, U i

Tactic:
rw [coe_finset_sup, Finset.sup_eq_iSup]

Goal state after:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
hU' : ↑s ⊆ ⋃ i, U i
t : Finset ι
ht : s ≤ t.sup fun i ↦ { carrier := U i, is_open' := ⋯ }
⊢ ⨆ a ∈ t, (SetLike.coe ∘ fun i ↦ { carrier := U i, is_open' := ⋯ }) a ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: case refine_3
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝ : Finset (↑s × ↑s)
x✝² : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝¹ : ∃ t_1, (t.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t_1.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝ : (x, y) ∉ t
tc : Finset (↑s × ↑s)
eq : (t.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ∃ t_1, ((insert (x, y) t).sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t_1.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
simp_rw [Finset.sup_insert, compl_sup, eq]

Goal state after:
case refine_3
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝ : Finset (↑s × ↑s)
x✝² : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝¹ : ∃ t_1, (t.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = t_1.sup fun x ↦ ↑x.1 \ ↑x.2
x y : ↑s
x✝ : (x, y) ∉ t
tc : Finset (↑s × ↑s)
eq : (t.sup fun x ↦ ↑x.1 \ ↑x.2)ᶜ = tc.sup fun x ↦ ↑x.1 \ ↑x.2
⊢ ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x ↦ ↑x.1 \ ↑x.2) = t.sup fun x ↦ ↑x.1 \ ↑x.2
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
⊢ IsQuasiSeparated (f '' s) → IsQuasiSeparated s

Tactic:
intro H U V hU hU' hU'' hV hV' hV''

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen[inst✝¹] U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen[inst✝¹] V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
x : α
hxK : x ∈ ↑K
hxL : x ∈ ↑L
h : ↑{x} ⊆ ↑K → ↑{x} ⊆ ↑L → ↑{x} ⊆ ↑⊥
⊢ x ∈ ∅

Tactic:
coe_singleton,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
x : α
hxK : x ∈ ↑K
hxL : x ∈ ↑L
h : {x} ⊆ ↑K → {x} ⊆ ↑L → {x} ⊆ ↑⊥
⊢ x ∈ ∅
Module: Mathlib.Topology.Sober

Goal state before:
pp: case a
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (Subtype.val ⁻¹' t)
⊢ t ⊆ closure (Subtype.val '' {H.genericPoint})

Tactic:
← closure_image_closure continuous_subtype_val,

Goal state after:
case a
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (Subtype.val ⁻¹' t)
⊢ t ⊆ closure (Subtype.val '' closure {H.genericPoint})
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingDown R S
inst✝ : HasGoingDown S T
⊢ GeneralizingMap (PrimeSpectrum.comap (algebraMap R S) ∘ PrimeSpectrum.comap (algebraMap S T))

Tactic:
apply GeneralizingMap.comp

Goal state after:
case hf
R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingDown R S
inst✝ : HasGoingDown S T
⊢ GeneralizingMap (PrimeSpectrum.comap (algebraMap S T))

case hg
R : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : HasGoingDown R S
inst✝ : HasGoingDown S T
⊢ GeneralizingMap (PrimeSpectrum.comap (algebraMap R S))
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ IsLocalHom (algebraMap (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))

Tactic:
rw [RingHom.algebraMap_toAlgebra]

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ IsLocalHom (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯)
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI✝ : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
r : R
⊢ ↑(f ((algebraMap R A) r)) + (algebraMap A B) ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
simp only [Derivation.map_algebraMap, zero_add, Submodule.coe_zero, ←
        IsScalarTower.algebraMap_apply R A B r]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ IsClosed {x} ↔ x.asIdeal.IsMaximal

Tactic:
rw [← closure_subset_iff_isClosed, ← zeroLocus_vanishingIdeal_eq_closure,
      vanishingIdeal_singleton]
  constructor <;> intro H
  · rcases x.asIdeal.exists_le_maximal x.2.1 with ⟨m, hm, hxm⟩
    exact (congr_arg asIdeal (@H ⟨m, hm.isPrime⟩ hxm)) ▸ hm
  · exact fun p hp ↦ PrimeSpectrum.ext (H.eq_of_le p.2.1 hp).symm

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

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

Tactic:
simp_rw [← vanishingIdeal_zeroLocus_eq_radical, h]

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
h : I.radical = J.radical
⊢ zeroLocus ↑J.radical = zeroLocus ↑J

Tactic:
zeroLocus_radical

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : I.radical = J.radical
⊢ zeroLocus ↑J = zeroLocus ↑J
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case succ
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
⊢ D (a ^ (n + 1)) = (n + 1) • a ^ (n + 1 - 1) • D a

Tactic:
rcases eq_zero_or_pos n with (rfl | hpos)

Goal state after:
case succ.inl
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
ihn : D (a ^ 0) = 0 • a ^ (0 - 1) • D a
⊢ D (a ^ (0 + 1)) = (0 + 1) • a ^ (0 + 1 - 1) • D a

case succ.inr
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
⊢ D (a ^ (n + 1)) = (n + 1) • a ^ (n + 1 - 1) • D a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset, id i ≤ I
M : Ideal R
hM : M ∈ fin.toFinset
hMI : id M ≤ I
⊢ I.IsMaximal

Tactic:
rw [fin.mem_toFinset] at hM

Goal state after:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset, id i ≤ I
M : Ideal R
hM : M ∈ {I | I.IsMaximal}
hMI : id M ≤ I
⊢ I.IsMaximal
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : A
⊢ (liftOfRightInverse hf hd) (f x) = f (d x)

Tactic:
suffices f (d (f_inv (f x) - x)) = 0 by simpa [sub_eq_zero]
  apply hd
  simp [hf _]

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
⊢ zeroLocus ↑(RingHom.ker f).radical = zeroLocus ↑(RingHom.ker f)

Tactic:
zeroLocus_radical

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ zeroLocus ↑(RingHom.ker f) = zeroLocus ↑(RingHom.ker f)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
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
this : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
⊢ (b.reverse * X ^ (1 + c.natDegree)).Monic

Tactic:
refine Monic.mul ?_ (by simp)

Goal state after:
case refine_1
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
this : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
⊢ b.reverse.Monic
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h
α : 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}
⊢ #{a | orderOf a = d} = φ d

Tactic:
rcases Decidable.eq_or_ne d 0 with (rfl | hd0)

Goal state after:
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

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.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
F : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₁
inst✝³ : FunLike F M M₁
inst✝² : AddMonoidHomClass F M M₁
inst✝¹ : Module (ZMod n) M
inst✝ : Module (ZMod n) M₁
f : F
c : ZMod n
x : M
⊢ f (c • x) = c • f x

Tactic:
rw [← ZMod.intCast_zmod_cast c]
  exact map_intCast_smul f _ _ (cast c) x

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal '' irreducibleComponents (PrimeSpectrum R) = minimalPrimes R

Tactic:
by
  rw [irreducibleComponents_eq_maximals_closed, minimalPrimes_eq_minimals,
    image_antitone_setOfPred_maximal (fun s t hs _ ↦ (vanishingIdeal_anti_mono_iff hs.1).symm),
    ← funext (@Set.mem_ofPred_eq _ · Ideal.IsPrime), ← vanishingIdeal_isClosed_isIrreducible]
  rfl

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

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ U = ⊤ → closedPoint R ∈ U

Tactic:
rintro rfl
    exact TopologicalSpace.Opens.mem_top _

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

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
p : ℕ
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p
hH : Nat.card G' = p
hGcyc : IsCyclic G
⊢ G ≃* G'

Tactic:
have hHcyc := isCyclic_of_prime_card hH

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
p : ℕ
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p
hH : Nat.card G' = p
hGcyc : IsCyclic G
hHcyc : IsCyclic G'
⊢ G ≃* G'
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
p : ℕ
g : G
x✝ : g ∈ (CommMonoid.primaryComponent G p).carrier
k : ℕ
hk : g ^ p ^ k = 1
⊢ g⁻¹ ^ p ^ k = 1

Tactic:
by rw [inv_pow, hk, inv_one]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

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

Tactic:
refine MulEquiv.trans (N := ∀ p : ps, P p) ?_ ?_

Goal state after:
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 : ↥ps) → (P : Sylow (↑p) G) → ↥P) ≃* ((p : ↥ps) → ↥(P ↑p))

case refine_2
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 : ↥ps) → ↥(P ↑p)) ≃* G
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
x y : M
a : S
hx : a • x = 0
⊢ y ∈ {x | ∃ a, a • x = 0} → x + y ∈ {x | ∃ a, a • x = 0}

Tactic:
⟨b,hy⟩

Goal state after:
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
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
⊢ x + y ∈ {x | ∃ a, a • x = 0}
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
i j k : ℕ
e : (j, k) ∈ Finset.antidiagonal i
⊢ a✝.coeff (j, k).1 * b✝.coeff (j, k).2 ∈ I ^ (j, k).1 * I ^ (j, k).2

Tactic:
exact Ideal.mul_mem_mul (hf j) (hg k)

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 = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
⊢ ((fun i ↦ torsionBySet R M ↑(p i)) i ⊓ T.sup fun i ↦ torsionBySet R M ↑(p i)) = ⊥

Tactic:
Finset.sup_eq_iSup,

Goal state after:
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 = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
⊢ (fun i ↦ torsionBySet R M ↑(p i)) i ⊓ ⨆ a ∈ T, torsionBySet R M ↑(p a) = ⊥
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✝ : N.FG
hin : N ≤ I • N
r : R
hr : r - 1 ∈ I
hr' : ∀ n ∈ N, r • n = 0
n : M
hn : n ∈ N
⊢ -(r - 1) • n = n

Tactic:
simpa [sub_smul] using hr' n hn

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l).coeff (n + 1) = x
⊢ ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l).coeff (n + 1) ∈ I • F.N n

Tactic:
Finsupp.linearCombination_apply,

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l).coeff (n + 1) = x
⊢ (l.sum fun i a ↦ a • ↑i).coeff (n + 1) ∈ I • F.N n
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ ⊤.spanRank = Submodule.spanRank (maximalIdeal R)

Tactic:
← Submodule.spanRank_top (maximalIdeal R)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ ⊤.spanRank = ⊤.spanRank
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
⊢ ∀ (a b c : M₁ ⟶ M₂), a + b + c = a + (b + c)

Tactic:
intros; ext1; simp only [add_app, add_assoc]

Goal state after: