mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case union
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)ᶜ
s : Set X
hs : IsConstructible s
t : Set X
ht : IsConstructible t
hs' : IsConstructible (f '' s)
ht' : IsConstructible (f '' t)
⊢ IsConstructible (f '' (s ∪ t))

Tactic:
| union s hs t ht hs' ht' =>

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

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h✝ : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ PrimeSpectrum.comap (algebraMap R S) Q
P : Ideal S
hle : P ≤ Q.asIdeal
hP : P.IsPrime
h : P.LiesOver p.asIdeal
⊢ (PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := hP }).asIdeal = p.asIdeal

Tactic:
exact h.over.symm

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

Goal state before:
pp: case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : GeneralizingMap (PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
· have : (⟨p, hp⟩ : PrimeSpectrum R) ⤳ (PrimeSpectrum.comap (algebraMap R S) ⟨Q, hQ⟩) :=
      (PrimeSpectrum.le_iff_specializes _ _).mp hlt.le
    obtain ⟨P, hs, heq⟩ := h this
    refine ⟨P.asIdeal, (PrimeSpectrum.le_iff_specializes _ _).mpr hs, P.2, ⟨?_⟩⟩
    simpa [PrimeSpectrum.ext_iff] using heq.symm

Goal state after:
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
d : Derivation R A ↥I
x : A
⊢ (Ideal.Quotient.mk I) ↑(d x) + (algebraMap A (B ⧸ I)) x = (algebraMap A (B ⧸ I)) x

Tactic:
by
  simp only [Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop, zero_add]

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

Goal state before:
pp: a b : ℕ
⊢ 0 < a.factorizationLCMRight b

Tactic:
by
  apply Nat.pos_of_ne_zero
  rw [factorizationLCMRight, Finsupp.prod_ne_zero_iff]
  intro p _ H
  by_cases h : b.factorization p ≤ a.factorization p
  · simp only [h, reduceIte, reduceCtorEq] at H
  · simp only [h, ↓reduceIte, pow_eq_zero_iff', ne_eq] at H
    simpa [H.1] using H.2

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
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ (∃ s, zeroLocus s = Z) ↔ ∃ a, comap (algebraMap R S) ⁻¹' zeroLocus a = Z

Tactic:
preimage_comap_zeroLocus

Goal state after:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ (∃ s, zeroLocus s = Z) ↔ ∃ a, zeroLocus (⇑(algebraMap R S) '' a) = Z
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
⊢ ↑(Submonoid.powers r) ⊓ ↑x.asIdeal ⊆ ⊥ → r ∉ x.asIdeal

Tactic:
intro h₁ h₂
    exact h₁ ⟨Submonoid.mem_powers r, h₂⟩

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ IsOpen (Set.range (comap (algebraMap R S)))

Tactic:
rw [localization_away_comap_range S r]

Goal state after:
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ IsOpen ↑(basicOpen r)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
⊢ ∃ a, (toPiLocalization R) a = x

Tactic:
replace hf a : (basicOpen a.1 : Set _) = {e.symm a} := by
    simp_rw [e, ← hf, Equiv.apply_ofInjective_symm]

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf✝ : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
⊢ ∃ a, (toPiLocalization R) a = x
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
g : G
hg : orderOf g = Nat.card G
⊢ (toMonoidHom G 1) g = g

Tactic:
MulDistribMulAction.toMonoidHom_apply,

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
g : G
hg : orderOf g = Nat.card G
⊢ 1 • g = g
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).Infinite

Tactic:
have := exponent_ne_zero_iff_range_orderOf_finite h
  rwa [Ne, not_iff_comm, Iff.comm] at this

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

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
g : G
hg : orderOf g = Nat.card G
⊢ (toMonoidHom G (m * n)) g = (toMonoidHom G m) ((toMonoidHom G n) g)

Tactic:
MulDistribMulAction.toMonoidHom_apply,

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
g : G
hg : orderOf g = Nat.card G
⊢ (m * n) • g = (toMonoidHom G m) ((toMonoidHom G n) g)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
g : G
hg : orderOf g = Nat.card G
⊢ (m * n) • g = (toMonoidHom G m) ((toMonoidHom G n) g)

Tactic:
MulDistribMulAction.toMonoidHom_apply,

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
g : G
hg : orderOf g = Nat.card G
⊢ (m * n) • g = m • (toMonoidHom G n) g
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
g : G
hg : orderOf g = Nat.card G
⊢ (m * n) • g = m • (toMonoidHom G n) g

Tactic:
MulDistribMulAction.toMonoidHom_apply,

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
g : G
hg : orderOf g = Nat.card G
⊢ (m * n) • g = m • n • g
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(QuotientGroup.mk' K).ker

Tactic:
QuotientGroup.ker_mk'

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥K
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ zeroLocus ↑I ⊆ comap f ⁻¹' zeroLocus ↑(Ideal.comap f I)

Tactic:
preimage_comap_zeroLocus

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
⊢ zeroLocus ↑I ⊆ zeroLocus (⇑f '' ↑(Ideal.comap f I))
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ IsPGroup p ↥(QuotientGroup.mk' (↑P).normalCore).ker

Tactic:
QuotientGroup.ker_mk'

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ IsPGroup p ↥(↑P).normalCore
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: p : ℕ
G : Type u_5
inst✝¹ : AddCommGroup G
hp : Nat.Prime p
inst✝ : Module (ZMod p) G
H : Submodule (ZMod p) G
k : ℕ
hk : k ≤ Nat.card ↥H
h'k : k ≠ 0
⊢ ∃ H', Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H' ∧ H' ≤ H

Tactic:
obtain ⟨H'm, H'mHm, H'mk, kH'm⟩ := Sylow.exists_subgroup_le_card_le
    (H := AddSubgroup.toSubgroup ((AddSubgroup.toZModSubmodule _).symm H)) hp
      isPGroup_multiplicative hk h'k
  exact ⟨AddSubgroup.toZModSubmodule _ (AddSubgroup.toSubgroup.symm H'm), H'mk, kH'm, H'mHm⟩

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints (↥H) (Sylow p G) ↔ ∀ ⦃x : G⦄, x ∈ H → x • P = P

Tactic:
exact Subtype.forall

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := ⋯
⊢ IsPGroup p ↥(QuotientGroup.mk' ↑P).ker

Tactic:
QuotientGroup.ker_mk'

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ IsPGroup p ↥↑P
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p ↥Q
hp : (QuotientGroup.mk' ↑P).ker < comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ False

Tactic:
QuotientGroup.ker_mk'

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p ↥Q
hp : ↑P < comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (zmodAddEquivOfGenerator hg hn) ↑i = i • g

Tactic:
change (ZMod.cast (i : ZMod n) : ℤ) • g = i • g

Goal state after:
G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (↑i).cast • g = i • g
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
x y : G
⊢ g' ^ Classical.choose ⋯ = g' ^ Classical.choose ⋯ * g' ^ Classical.choose ⋯

Tactic:
by
    simp only [← zpow_add, zpow_eq_zpow_iff_modEq]
    apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr hg')
    rw [← zpow_eq_zpow_iff_modEq, zpow_add]
    simp only [fun x ↦ Classical.choose_spec <| mem_zpowers_iff.mp <| hg x]

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

Goal state before:
pp: case refine_2.mp
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1
⊢ ((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤

Tactic:
Finset.sum_cons

Goal state after:
case refine_2.mp
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
⊢ ((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝⁴ : Ring R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite (End R M) M
s : Finset M
hs : span (End R M) ↑s = ⊤
f : End (End R M) M
r : R
hr : ∀ m ∈ s, f m = r • m
m : M
⊢ ((toModuleEnd (End R M) M) r) m = f m

Tactic:
induction hs.ge (trivial : m ∈ ⊤) using Submodule.span_induction with
  | mem m hm => exact (hr m hm).symm
  | zero => simp
  | add _ _ _ _ h₁ h₂ => simpa using congr($h₁ + $h₂)
  | smul g _ _ h => simp_rw [map_smul, h]

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

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

Tactic:
add_smul

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

Goal state before:
pp: case single.add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : (eval r) (p✝ • single R i m) = Polynomial.eval r p✝ • (eval r) (single R i m)
e₂ : (eval r) (q✝ • single R i m) = Polynomial.eval r q✝ • (eval r) (single R i m)
⊢ Polynomial.eval r p✝ • (eval r) (single R i m) + Polynomial.eval r q✝ • (eval r) (single R i m) =
    (Polynomial.eval r p✝ + Polynomial.eval r q✝) • (eval r) (single R i m)

Tactic:
add_smul

Goal state after:
case single.add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : (eval r) (p✝ • single R i m) = Polynomial.eval r p✝ • (eval r) (single R i m)
e₂ : (eval r) (q✝ • single R i m) = Polynomial.eval r q✝ • (eval r) (single R i m)
⊢ Polynomial.eval r p✝ • (eval r) (single R i m) + Polynomial.eval r q✝ • (eval r) (single R i m) =
    Polynomial.eval r p✝ • (eval r) (single R i m) + Polynomial.eval r q✝ • (eval r) (single R i m)
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : ↥I
e :
  ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) (I.toCotangent x)) =
    ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) (I.toCotangent y))
⊢ I.toCotangent x = I.toCotangent y

Tactic:
I.toCotangent_eq

Goal state after:
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : ↥I
e :
  ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) (I.toCotangent x)) =
    ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) (I.toCotangent y))
⊢ ↑x - ↑y ∈ I ^ 2
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
S✝ : Type v
S' : Type w
inst✝¹⁴ : CommRing R
inst✝¹³ : CommSemiring S✝
inst✝¹² : Algebra S✝ R
inst✝¹¹ : CommSemiring S'
inst✝¹⁰ : Algebra S' R
inst✝⁹ : Algebra S✝ S'
inst✝⁸ : IsScalarTower S✝ S' R
I✝ : Ideal R
A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
I : Ideal S
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ↥I →ₗ[R] M
hf : ∀ (x y : ↥I), f (x * y) = 0
x : ↥I
hx : x ∈ (I • ⊤).toAddSubgroup
⊢ x ∈ f.toAddMonoidHom.ker

Tactic:
by
    simp only [Submodule.mem_toAddSubgroup, AddMonoidHom.mem_ker] at hx ⊢
    refine Submodule.smul_induction_on hx (fun r hr y _ ↦ hf ⟨r, hr⟩ y) fun x y hx hy ↦ ?_
    simp only [map_add, hx, hy, add_zero]

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

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
⊢ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J)) ≤
    (J.mapCotangent I (Algebra.ofId A B) ⋯).ker

Tactic:
rw [Submodule.map_le_iff_le_comap, ← LinearMap.ker_comp]

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
⊢ Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J) ≤
    (J.mapCotangent I (Algebra.ofId A B) ⋯ ∘ₗ J.toCotangent).ker
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
i : ι
⊢ Subsingleton { j // c.Rel i j }

Tactic:
constructor
  rintro ⟨j, rij⟩ ⟨k, rik⟩
  congr
  exact c.next_eq rij rik

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : ↑(M₁.obj X)
⊢ (ConcreteCategory.hom ((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).map (n • f))) x =
    (ModuleCat.Hom.hom (n • f.app X)) x

Tactic:
Functor.map_zsmul

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : ↑(M₁.obj X)
⊢ (ConcreteCategory.hom (n • (toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).map f)) x = (ModuleCat.Hom.hom (n • f.app X)) 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 ι
C : HomologicalComplex V c
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ C.d i j ≫ C.d j k = 0

Tactic:
exact C.d_comp_d' i j k hij hjk

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = ideal R S

Tactic:
by
  apply le_antisymm
  · rw [Ideal.span_le]
    rintro _ ⟨s, rfl⟩
    exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _
  · change (KaehlerDifferential.ideal R S).restrictScalars S ≤ (Ideal.span _).restrictScalars S
    rw [← KaehlerDifferential.submodule_span_range_eq_ideal, Ideal.span]
    conv_rhs => rw [← Submodule.span_span_of_tower S]
    exact Submodule.subset_span

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

Goal state before:
pp: ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
⊢ ((singleMapHomologicalComplex F c j).hom.app X).f j =
    F.map (singleObjXSelf c j X).hom ≫ (singleObjXSelf c j (F.obj X)).inv

Tactic:
by
  simp [singleMapHomologicalComplex, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]

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

Goal state before:
pp: ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
⊢ ((singleMapHomologicalComplex F c j).inv.app X).f j =
    (singleObjXSelf c j (F.obj X)).hom ≫ F.map (singleObjXSelf c j X).inv

Tactic:
by
  simp [singleMapHomologicalComplex, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

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
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ homologyMap (-φ) i = -homologyMap φ i

Tactic:
dsimp [homologyMap]
  rw [← ShortComplex.homologyMap_neg]
  rfl

Goal state after: