mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : a = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

case neg
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
⊢ IsCompact ↑(basicOpen f)

Tactic:
rw [← localization_away_comap_range (Localization (Submonoid.powers f))]

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R
⊢ IsCompact (Set.range (comap (algebraMap R (Localization (Submonoid.powers f)))))
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ Injective
    ⇑(QuotientAddGroup.map (zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ⋯)

Tactic:
rw [← ker_eq_bot_iff, eq_bot_iff]

Goal state after:
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ (QuotientAddGroup.map (zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b)) (stabilizer (↥(zmultiples a)) b)
        ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) ⋯).ker ≤
    ⊥
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
g : G
⊢ g ^ n = g ^ (n % exponent G + exponent G * (n / exponent G))

Tactic:
by rw [Nat.mod_add_div]

Goal state after:
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ (orbitZPowersEquiv a b).symm ↑k = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩

Tactic:
rw [orbitZPowersEquiv_symm_apply, ZMod.coe_intCast]
  exact Subtype.ext (zpow_smul_mod_minimalPeriod _ _ k)

Goal state after:
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: G : Type u_3
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ℤ
⊢ g ^ k • Quotient.out q = (H.quotientEquivSigmaZMod g).symm ⟨q, ↑k⟩

Tactic:
quotientEquivSigmaZMod_symm_apply,

Goal state after:
G : Type u_3
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ℤ
⊢ g ^ k • Quotient.out q = g ^ (↑k).cast • Quotient.out q
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
⊢ exponent G ∣ n ↔ ∀ (g : G), orderOf g ∣ n

Tactic:
simp_rw [exponent_dvd_iff_forall_pow_eq_one, orderOf_dvd_iff_pow_eq_one]

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'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(k % ↑(Nat.find hex)).natAbs
⊢ g ^ (k % ↑(Nat.find hex)).natAbs ∈ H

Tactic:
by rwa [← zpow_natCast, ← hk₄]

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

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ DenseRange (comap f) → ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)

pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ (∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)) →
    DenseRange (comap f)

Tactic:
· intro H I hI
    have : I ∈ (RingHom.ker f).minimalPrimes := by
      rw [denseRange_comap_iff_ker_le_nilRadical] at H
      simp only [Set.mem_ofPred, Ideal.IsMinimalPrime] at hI ⊢
      convert! hI using 2 with p
      exact ⟨fun h ↦ ⟨h.1, bot_le⟩, fun h ↦ ⟨h.1, H.trans (h.1.radical_le_iff.mpr bot_le)⟩⟩
    obtain ⟨p, hp, _, rfl⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f (I := ⊥) I this
    exact ⟨⟨p, hp⟩, rfl⟩

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ (∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)) →
    DenseRange (comap f)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case inl
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Subsingleton R
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

pp: case inr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

Tactic:
· refine ⟨0, 0, ?_, ?_, ?_, ?_⟩ <;> apply Subsingleton.elim

Goal state after:
case inr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)
Module: Mathlib.GroupTheory.PGroup

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

Tactic:
← hG,

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
n : ℕ
hG : Nat.card G ∣ p ^ n
g : G
⊢ orderOf g ∣ Nat.card G
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
⊢ (Nat.card ↥H₁).Coprime (Nat.card ↥H₂)

Tactic:
obtain ⟨n₁, heq₁⟩ := iff_card.mp hH₁

Goal state after:
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
n₁ : ℕ
heq₁ : Nat.card ↥H₁ = p₁ ^ n₁
⊢ (Nat.card ↥H₁).Coprime (Nat.card ↥H₂)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
n₁ n₂ : ℕ
⊢ (p₁ ^ n₁).Coprime (p₂ ^ n₂)

Tactic:
exact Nat.coprime_pow_primes _ _ hp₁.elim hp₂.elim hne

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ p * Nat.card (G ⧸ center G) ∣ p ^ 2

Tactic:
← hG,

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
hG : Nat.card G = p ^ 2
⊢ p * Nat.card (G ⧸ center G) ∣ Nat.card G
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, IsPGroup p ↥(H i)
hn : ∀ i ∈ s, (H i).Normal
⊢ IsPGroup p ↥(⨆ i ∈ s, H i)

Tactic:
rw [← iSup_subtype'']

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, IsPGroup p ↥(H i)
hn : ∀ i ∈ s, (H i).Normal
⊢ IsPGroup p ↥(⨆ i, H ↑i)
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n
inst✝ : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
this : (c % n) • x + (c / n * n) • x = c • x
⊢ (c % n) • x = c • x

Tactic:
mul_nsmul,

Goal state after:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n
inst✝ : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
this : (c % n) • x + n • (c / n) • x = c • x
⊢ (c % n) • x = c • x
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
⊢ exponent α = Nat.card α

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := α)
  apply Nat.dvd_antisymm Group.exponent_dvd_nat_card
  rw [← hg]
  exact order_dvd_exponent _

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
cyc : IsCyclic (M × N)
inst✝¹ : Finite M
inst✝ : Finite N
hM : IsCyclic M
hN : IsCyclic N
x✝ : CommGroup (M × N) := IsCyclic.commGroup
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
let _ := hM.commGroup

Goal state after:
M : Type u_4
N : Type u_5
inst✝³ : Group M
inst✝² : Group N
cyc : IsCyclic (M × N)
inst✝¹ : Finite M
inst✝ : Finite N
hM : IsCyclic M
hN : IsCyclic N
x✝¹ : CommGroup (M × N) := IsCyclic.commGroup
x✝ : CommGroup M := IsCyclic.commGroup
⊢ (Nat.card M).Coprime (Nat.card N)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_2
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
x✝ : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
f : M × N →* N := MonoidHom.snd M N
e : ↥f.ker ≃* M := ⋯.mpr (((⊤.prodEquiv ⊥).trans MulEquiv.prodUnique).trans Subgroup.topEquiv)
⊢ IsCyclic (M × N)

Tactic:
let _ := hM.commGroup

Goal state after:
case refine_2
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
x✝¹ : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
f : M × N →* N := MonoidHom.snd M N
e : ↥f.ker ≃* M := ⋯.mpr (((⊤.prodEquiv ⊥).trans MulEquiv.prodUnique).trans Subgroup.topEquiv)
x✝ : CommGroup M := IsCyclic.commGroup
⊢ IsCyclic (M × N)
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: ι : 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
⊢ ∑ i ∈ t, ↑((Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ + fun i ↦ ⟨↑(μ i), ⋯⟩) i) = 1

Tactic:
← @if_pos _ _ h.choose_spec R (μ a) 0,

Goal state after:
ι : 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
hμ : (if Exists.choose h ∈ t then ↑(μ a) else 0) + ∑ x ∈ t, ↑(μ x) = 1
⊢ ∑ i ∈ t, ↑((Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ + fun i ↦ ⟨↑(μ i), ⋯⟩) i) = 1

ι : 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
⊢ Decidable (Exists.choose h ∈ t)
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: case refine_2
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
I : Ideal R
coatom : IsCoatom I
equiv : M ≃ₗ[R] R ⧸ I
⊢ IsSimpleModule R M

Tactic:
convert! congr equiv

Goal state after:
case refine_2
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
I : Ideal R
coatom : IsCoatom I
equiv : M ≃ₗ[R] R ⧸ I
⊢ IsSimpleModule R (R ⧸ I)
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
z : R
hzy : z * y = 1
⊢ IsUnit x

Tactic:
exact ⟨⟨x, y, left_inv_eq_right_inv hzy hyx ▸ hzy, hyx⟩, rfl⟩

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
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this✝ : Module R S := Module.compHom S f
this : RingHomSurjective f
⊢ IsSemisimpleRing S

Tactic:
let e : S →ₛₗ[f] S := { AddMonoidHom.id S with map_smul' := fun _ _ ↦ rfl }

Goal state after:
R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this✝ : Module R S := Module.compHom S f
this : RingHomSurjective f
e : S →ₛₗ[f] S :=
  let __src := AddMonoidHom.id S;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleRing S
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
a : R
⊢ torsionBySet R M {a} = torsionBy R M a

Tactic:
by
  ext x
  simp only [mem_torsionBySet_iff, SetCoe.forall, Set.mem_singleton_iff, forall_eq,
    mem_torsionBy_iff]

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

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ 0 = ∑ x ∈ Finset.antidiagonal i, r.coeff x.1 * ((monomial n) a).coeff x.2

Tactic:
Finset.sum_eq_zero

Goal state after:
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ 0 = 0

case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ ∀ x ∈ Finset.antidiagonal i, r.coeff x.1 * ((monomial n) a).coeff x.2 = 0
Module: Mathlib.Algebra.Polynomial.Module.Basic

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

Tactic:
induction p using Polynomial.induction_on' with

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
map : Fin 2 → Ideal R :=
  fun x ↦
    match x with
    | 0 => P
    | 1 => Q
⊢ (↑⊤).Pairwise fun i j ↦ map i ⊔ map j = ⊤

Tactic:
· simp_all [Set.pairwise_pair, Fin.univ_succ, map, sup_comm]

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case a
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ reesAlgebra I ≤ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
intro p hp
    rw [p.as_sum_support]
    apply Subalgebra.sum_mem _ _
    rintro i -
    exact monomial_mem_adjoin_monomial (hp i)

Goal state after:
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
p : R[X]
r : R
i : ℕ
m : M
⊢ (eval r) (p • single R i m) = Polynomial.eval r p • (eval r) (single R i m)

Tactic:
induction p using Polynomial.induction_on' with

Goal state after:
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
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
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(F.N n')
e : n' ≤ n
this : I ^ (n - n' + 1) • F.N n' ≤ I ^ 1 • F.N (n - n' + n')
⊢ (↑(l ⟨single R n' m, ⋯⟩)).coeff (n + 1 - n') • m ∈ I • F.N n

Tactic:
rw [tsub_add_cancel_of_le e, pow_one, add_comm _ 1, ← add_tsub_assoc_of_le e, add_comm] at this

Goal state after:
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
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(F.N n')
e : n' ≤ n
this : I ^ (n + 1 - n') • F.N n' ≤ I • F.N n
⊢ (↑(l ⟨single R n' m, ⋯⟩)).coeff (n + 1 - n') • m ∈ I • F.N n
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_2
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
f : A →ₐ[R] B
⊢ ∀ (r : R),
    (↑↑(Quotient.lift (RingHom.ker f.toRingHom ^ 2) f.toRingHom ⋯)).toFun
        ((algebraMap R (A ⧸ RingHom.ker f.toRingHom ^ 2)) r) =
      (algebraMap R B) r

Tactic:
intro r
    rw [IsScalarTower.algebraMap_apply R A, RingHom.toFun_eq_coe, Ideal.Quotient.algebraMap_eq,
      Ideal.Quotient.lift_mk]
    exact f.map_algebraMap r

Goal state after:
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
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
⊢ I₁.Cotangent →ₗ[R] I₂.Cotangent

Tactic:
refine Submodule.mapQ ((I₁ • ⊤ : Submodule A I₁).restrictScalars R)
    ((I₂ • ⊤ : Submodule B I₂).restrictScalars R) ?_ ?_
  · exact f.toLinearMap.restrict (p := I₁.restrictScalars R) (q := I₂.restrictScalars R) h
  · intro x hx
    rw [Submodule.restrictScalars_mem] at hx
    refine Submodule.smul_induction_on hx ?_ (fun _ _ ↦ add_mem)
    rintro a ha ⟨b, hb⟩ -
    simp only [SetLike.mk_smul_mk, smul_eq_mul, Submodule.mem_comap, Submodule.restrictScalars_mem]
    convert!
      (Submodule.smul_mem_smul (M := I₂) (r := f a) (n := ⟨f b, h hb⟩) (h ha)
        (Submodule.mem_top)) using 1
    ext
    exact map_mul f a b

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

Goal state before:
pp: 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
x' : ↥I
⊢ ∃ a, (J.mapCotangent I (Algebra.ofId A B) ⋯) a = I.toCotangent x'

Tactic:
rcases Ideal.exists_of_comap_eq_ker_sup _ surj eq x'.2 with ⟨y', mem, hy'⟩

Goal state after:
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
x' : ↥I
y' : A
mem : y' ∈ J
hy' : (algebraMap A B) y' = ↑x'
⊢ ∃ a, (J.mapCotangent I (Algebra.ofId A B) ⋯) a = I.toCotangent x'
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
inst✝³ : IsDomain R
inst✝² : IsNoetherianRing R
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
⊢ ⨅ i, I ^ i • ⊤ = ⊥

Tactic:
by
  rw [eq_bot_iff]
  intro x hx
  by_contra hx'
  have := Ideal.mem_iInf_smul_pow_eq_bot_iff I x
  obtain ⟨r, hr⟩ := this.mp hx
  have := smul_left_injective _ hx' (hr.trans (one_smul _ x).symm)
  exact I.eq_top_iff_one.not.mp h (this ▸ r.prop)

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

Goal state before:
pp: case e_a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
X : Cᵒᵖ
hX : Limits.IsInitial X
M : PresheafOfModules R
Y Z : Cᵒᵖ
f : Y ⟶ Z
r : ↑(R.obj X)
x : ↑(forgetToPresheafModuleCatObjObj X hX M Y)
⊢ hX.to Y ≫ f = hX.to Z

Tactic:
apply hX.hom_ext

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
i j : ι
P : C
inst✝ : Projective P
⊢ Projective (((single C c i).obj P).X j)

Tactic:
by_cases hij : j = i
  · subst hij
    simp only [single_obj_X_self]
    infer_instance
  · exact (isZero_single_obj_X _ _ _ _ hij).projective

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
m n : A
hmn : m + n = 0
X : C
⊢ (shiftFunctorComm C m n).hom.app X =
    (shiftFunctorCompIsoId C m n hmn).hom.app X ≫ (shiftFunctorCompIsoId C n m ⋯).inv.app X

Tactic:
simp [shiftFunctorCompIsoId, shiftFunctorComm_eq C m n 0 hmn]

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
m n : A
hmn : m + n = 0
X : C
⊢ (shiftFunctorComm C m n).inv.app X =
    (shiftFunctorCompIsoId C n m ⋯).hom.app X ≫ (shiftFunctorCompIsoId C m n hmn).inv.app X

Tactic:
simp [shiftFunctorCompIsoId, shiftFunctorComm_eq C m n 0 hmn]

Goal state after: