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 : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).1 * ((↑a).2 * (↑b).2) + (↑a).2 * (↑a).2 * 0 = 0

Tactic:
mul_zero,

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

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

Tactic:
mul_add,

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

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

Tactic:
mul_add,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑b).1 * (↑a).1 + (↑b).1 * ((↑a).2 * (↑b).1) = (↑b).1
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 * ((↑a).2 * (↑c).2)) =
    (↑a).2 * ((↑b).2 + (↑b).1 * (↑c).2)

Tactic:
mul_add,

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 + ((↑a).1 * ((↑a).2 * (↑c).2) + (↑a).2 * (↑b).1 * ((↑a).2 * (↑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
inst✝ : CommRing R
a b c : { x // IsIdempotentElem x }
⊢ ↑a * (↑b + ↑c) - ↑a * (↑b * ↑c) = ↑a * ↑b + ↑a * ↑c - ↑a * ↑b * (↑a * ↑c)

Tactic:
mul_add,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b c : { x // IsIdempotentElem x }
⊢ ↑a * ↑b + ↑a * ↑c - ↑a * (↑b * ↑c) = ↑a * ↑b + ↑a * ↑c - ↑a * ↑b * (↑a * ↑c)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx : x ∈ p
⊢ ∃ y ∉ I, x * y ∈ I

Tactic:
obtain ⟨y, hy, n, hx⟩ := Ideal.iUnion_minimalPrimes.subset (Set.mem_biUnion hp hx)

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx✝ : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
⊢ ∃ y ∉ I, x * y ∈ I
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: case mpr.left
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsCompact (⋃ i ∈ s, b i)

Tactic:
exact hs.isCompact_biUnion fun i _ => hb' i

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case insert.inr
α✝ : Type u_1
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s✝ : Set (Set α)
a✝ : Set α
s : Set (Set α)
ha : a✝ ∉ s
hs : s.Finite
ih :
  (∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t) →
    (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen[inst✝¹] t) → s.Nonempty → IsCompact (⋂₀ s)
ho : ∀ t ∈ insert a✝ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ insert a✝ s, IsCompact t
h : ∀ t ∈ insert a✝ s, IsOpen[inst✝¹] t
hne : s.Nonempty
⊢ (insert a✝ s).Nonempty → IsCompact (⋂₀ insert a✝ s)

Tactic:
· grind [IsCompact.inter_of_isOpen, hs.isOpen_sInter, Set.sInter_insert]

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsCodirectedOrder P
x : P
I✝ J✝ s t I J : Ideal P
⊢ {x | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j}.Nonempty

Tactic:
obtain ⟨w, h⟩ := inter_nonempty I J

Goal state after:
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsCodirectedOrder P
x : P
I✝ J✝ s t I J : Ideal P
w : P
h : w ∈ ↑I ∩ ↑J
⊢ {x | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j}.Nonempty
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : Nonempty α
⊢ Nonempty (PositiveCompacts α)

Tactic:
inhabit α
  rcases exists_compact_mem_nhds (default : α) with ⟨K, hKc, hK⟩
  exact ⟨⟨K, hKc⟩, _, mem_interior_iff_mem_nhds.2 hK⟩

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
hs : IsConstructible s
⊢ IsConstructible (f '' s)

Tactic:
induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    have hfU : IsOpen (f '' U ∪ (range f)ᶜ) := by
      simpa [← range_sdiff_image hf.injective, sdiff_eq, compl_inter, union_comm]
        using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl
    suffices h : IsRetrocompact (f '' U ∪ (range f)ᶜ) by
      simpa [union_inter_distrib_right, inter_eq_left.2 (image_subset_range ..)]
        using (h.isConstructible hfU).sdiff (hfcomp.isConstructible hf.isClosed_range.isOpen_compl)
    rintro V hVcomp hVopen
    rw [union_inter_distrib_right, ← image_inter_preimage]
    exact ((hUcomp (hf.isCompact_preimage hVcomp) (hVopen.preimage hf.continuous)).image
      hf.continuous).union <| hfcomp hVcomp hVopen
  | union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht'
  | compl s hs hs' =>
    rw [← range_sdiff_image hf.injective]
    exact (hfcomp.isConstructible hf.isClosed_range.isOpen_compl).of_compl.sdiff hs'

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case a
X : Type u_2
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : X → Set X
hU : ∀ (x : X), IsOpen[inst✝²] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
⊢ s ⊆ ⋃ i ∈ ↑σ, U i ∩ s

Tactic:
rw [← Set.iUnion₂_inter, Set.subset_inter_iff]
    exact ⟨hst.trans htσ, subset_rfl⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
⊢ IsCompact (Set.range (comap (algebraMap R (Localization (Submonoid.powers f)))))

Tactic:
exact isCompact_range (continuous_comap _)

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ exponent G ≤ n

Tactic:
classical
  rw [exponent, dif_pos]
  · apply Nat.find_min'
    exact ⟨hpos, hG⟩
  · exact ⟨n, hpos, hG⟩

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)
⊢ StableUnderGeneralization sᶜ

Tactic:
convert! h₂.stableUnderGeneralization_image hsc.isOpen_compl.stableUnderGeneralization

Goal state after:
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)ᶜ
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * 0
hm0 : m = 0
⊢ False

Tactic:
mul_zero,

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = 0
hm0 : m = 0
⊢ False
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
n : ℕ
hG : Nat.card G ∣ p ^ n
⊢ IsPGroup p G

Tactic:
refine fun g ↦ ⟨n, ?_⟩
  grw [← orderOf_dvd_iff_pow_eq_one, ← hG, orderOf_dvd_natCard]

Goal state after:
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : FG G
h : rank G = 0
s : Finset G
hs : s.card = rank G
hs' : Subgroup.closure ↑s = ⊤
⊢ Subsingleton G

Tactic:
rw [h, Finset.card_eq_zero] at hs

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : FG G
h : rank G = 0
s : Finset G
hs : s = ∅
hs' : Subgroup.closure ↑s = ⊤
⊢ Subsingleton G
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ zeroLocus ∘ SetLike.coe '' minimalPrimes R = irreducibleComponents (PrimeSpectrum R)

Tactic:
rw [← vanishingIdeal_irreducibleComponents, ← Set.image_comp, Set.EqOn.image_eq_self]

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ Set.EqOn ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) id (irreducibleComponents (PrimeSpectrum R))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ IsClosed {closedPoint R}

Tactic:
by
  rw [PrimeSpectrum.isClosed_singleton_iff_isMaximal, closedPoint]
  infer_instance

Goal state after:
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, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b) = y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b)

Tactic:
mem_center_iff.1 ha

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
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b) = y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
h : IsCyclic G
⊢ Nat.card (MulAut G) = (Nat.card G).totient

Tactic:
rw [← ZMod.card_units_eq_totient, ← Nat.card_eq_fintype_card]

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
h : IsCyclic G
⊢ Nat.card (MulAut G) = Nat.card (ZMod (Nat.card G))ˣ
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
⊢ ∀ (ι : Type u_2) (s : ι → ↑(Iic a)), b ≤ iSup s → ∃ t, b ≤ ⨆ a_2 ∈ t, s a_2

Tactic:
intro ι

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
⊢ ∀ (s : ι → ↑(Iic a)), b ≤ iSup s → ∃ t, b ≤ ⨆ a_2 ∈ t, s a_2
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this✝ : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
this : ∀ g ∈ (↑H \ {1}).toFinset, p ∣ orderOf g
⊢ p ^ k ∣ ∏ i ∈ (↑H \ {1}).toFinset, p

Tactic:
prod_const,

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this✝ : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
this : ∀ g ∈ (↑H \ {1}).toFinset, p ∣ orderOf g
⊢ p ^ k ∣ p ^ #(↑H \ {1}).toFinset
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
⊢ (↑P).Characteristic

Tactic:
by
  have _ := unique_of_normal P h
  exact characteristic_of_subsingleton _

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i✝ : Fin (snoc s₁ x₁ hsat₁).length
i : Fin (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)
⊢ Iso ((snoc s₁ x₁ hsat₁).toFun i.castSucc.castSucc, (snoc s₁ x₁ hsat₁).toFun i.castSucc.succ)
    ((snoc s₂ x₂ hsat₂).toFun ((Exists.choose hequiv) i).castSucc.castSucc,
      (snoc s₂ x₂ hsat₂).toFun ((Exists.choose hequiv) i).castSucc.succ)

Tactic:
simpa [snoc_castSucc, ← Fin.castSucc_succ] using hequiv.choose_spec i

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_6
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
N' : Type u_7
inst✝² : AddCommGroup N'
inst✝¹ : Module S N'
σ : R →+* S
l : M' →ₛₗ[σ] N'
inst✝ : RingHomSurjective σ
hl : Function.Bijective ⇑l
⊢ ComplementedLattice (Submodule R M') ↔ ComplementedLattice (Submodule S N')

Tactic:
(Submodule.orderIsoMapComapOfBijective l hl).complementedLattice_iff

Goal state after:
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
⊢ torsionOf R M m = ⊤ ↔ m = 0

Tactic:
by
  refine ⟨fun h => ?_, fun h => by simp [h]⟩
  rw [← one_smul R m, ← mem_torsionOf_iff m (1 : R), h]
  exact Submodule.mem_top

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

Goal state before:
pp: ι : Type u_1
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
m : Submodule R✝ M
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R✝ N
R : Type u_6
inst✝² : DivisionRing R
inst✝¹ : Module R M
inst✝ : Nontrivial M
v : M
hv : v ≠ 0
w : M
f : M →ₗ[R] M
eq : f ∘ₗ toSpanSingleton R M v = toSpanSingleton R M w
⊢ (toSpanSingleton (Module.End R M) M v) f = w

Tactic:
simpa using congr($eq 1)

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

Goal state before:
pp: R : Type u_1
A : Type u_3
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
f : R[X]
m : AEval R M a
⊢ (r • (aeval a) f) • (of R M a).symm m = (of R M a).symm (r • f • m)

Tactic:
smul_assoc,

Goal state after:
R : Type u_1
A : Type u_3
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
f : R[X]
m : AEval R M a
⊢ r • (aeval a) f • (of R M a).symm m = (of R M a).symm (r • f • m)
Module: Mathlib.Algebra.Polynomial.Module.Basic

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

Tactic:
| single =>

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

Goal state before:
pp: case h.left
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
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
z : M
hz : z ∈ I • span R s
c : R
hci : c ∈ I
hyz : c • i + z = r • i
⊢ r - 1 - c ∈ I

Tactic:
exact I.sub_mem hr1 hci

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: M : Type u_2
inst✝ : AddCommMonoid M
⊢ IsAddTorsion M ↔ IsTorsion ℕ M

Tactic:
refine ⟨fun h x => ?_, fun h x => ?_⟩

Goal state after:
case refine_1
M : Type u_2
inst✝ : AddCommMonoid M
h : IsAddTorsion M
x : M
⊢ ∃ a, a • x = 0

case refine_2
M : Type u_2
inst✝ : AddCommMonoid M
h : IsTorsion ℕ M
x : M
⊢ IsOfFinAddOrder x
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: M : Type u_2
inst✝ : AddCommGroup M
⊢ IsAddTorsion M ↔ IsTorsion ℤ M

Tactic:
refine ⟨fun h x => ?_, fun h x => ?_⟩

Goal state after:
case refine_1
M : Type u_2
inst✝ : AddCommGroup M
h : IsAddTorsion M
x : M
⊢ ∃ a, a • x = 0

case refine_2
M : Type u_2
inst✝ : AddCommGroup M
h : IsTorsion ℤ M
x : M
⊢ IsOfFinAddOrder x
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x y : ↥I
⊢ I.toCotangent x = I.toCotangent y ↔ ↑x - ↑y ∈ I ^ 2

Tactic:
by
  rw [← sub_eq_zero]
  exact I.mem_toCotangent_ker

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.cotangentToQuotientSquare.range = (I.cotangentToQuotientSquare ∘ₗ I.toCotangent).range

pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ (I.cotangentToQuotientSquare ∘ₗ I.toCotangent).range = Submodule.restrictScalars R I.cotangentIdeal

Tactic:
· rw [LinearMap.range_comp, I.toCotangent_range, Submodule.map_top]

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ (I.cotangentToQuotientSquare ∘ₗ I.toCotangent).range = Submodule.restrictScalars R I.cotangentIdeal
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr
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
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
⊢ (⨆ i ∈ Finset.range n.succ, Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))).FG

Tactic:
iSup_subtype'

Goal state after:
case mpr
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
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
⊢ (⨆ x, Submodule.span (↥(reesAlgebra I)) (single R ↑x '' ↑(F.N ↑x))).FG
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
⊢ Submodule.span R s = ⊤

Tactic:
change Submodule.span R s = ⊤

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
⊢ Submodule.span R s = ⊤
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_2.refine_1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * 0) =
    (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo 0 +
      (TensorProduct.lmul' R) 0 • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

Tactic:
mul_zero,

Goal state after:
case refine_2.refine_1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ D.tensorProductTo 0 =
    (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo 0 +
      (TensorProduct.lmul' R) 0 • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_2.refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁✝ x₂ : S
x₁ y₁ : S ⊗[R] S
h₁ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * x₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo x₁ +
      (TensorProduct.lmul' R) x₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
h₂ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * y₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo y₁ +
      (TensorProduct.lmul' R) y₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
⊢ D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * (x₁ + y₁)) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo (x₁ + y₁) +
      (TensorProduct.lmul' R) (x₁ + y₁) • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)

Tactic:
mul_add,

Goal state after:
case refine_2.refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁✝ x₂ : S
x₁ y₁ : S ⊗[R] S
h₁ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * x₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo x₁ +
      (TensorProduct.lmul' R) x₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
h₂ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * y₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo y₁ +
      (TensorProduct.lmul' R) y₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
⊢ D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * x₁ + x₁✝ ⊗ₜ[R] x₂ * y₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo (x₁ + y₁) +
      (TensorProduct.lmul' R) (x₁ + y₁) • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }.d i j
i j : ι
hij : c.Rel i j
⊢ d₁ i j = d₂ i j

pp: case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }.d i j
i j : ι
hij : ¬c.Rel i j
⊢ d₁ i j = d₂ i j

Tactic:
· simpa only [comp_id, id_comp, eqToHom_refl] using h_d i j hij

Goal state after:
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }.d i j
i j : ι
hij : ¬c.Rel i j
⊢ d₁ i j = d₂ i j