mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : PrimeSpectrum (R × S)
⊢ p ∈ Set.range (comap (RingHom.fst R S)) → p ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))

pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : PrimeSpectrum (R × S)
h : p ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
⊢ p ∈ Set.range (comap (RingHom.fst R S))

Tactic:
· rintro ⟨I, hI, rfl⟩; exact Ideal.comap_mono bot_le

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : PrimeSpectrum (R × S)
h : p ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
⊢ p ∈ Set.range (comap (RingHom.fst R S))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : PrimeSpectrum (R × S)
⊢ p ∈ Set.range (comap (RingHom.snd R S)) → p ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))

pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : PrimeSpectrum (R × S)
h : p ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
⊢ p ∈ Set.range (comap (RingHom.snd R S))

Tactic:
· rintro ⟨I, hI, rfl⟩; exact Ideal.comap_mono bot_le

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : PrimeSpectrum (R × S)
h : p ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
⊢ p ∈ Set.range (comap (RingHom.snd R S))
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 : β
⊢ zmultiples ↑(minimalPeriod (fun x ↦ a +ᵥ x) b) ≤
    comap ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) (stabilizer (↥(zmultiples a)) b)

Tactic:
zmultiples_le,

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 : β
⊢ ↑(minimalPeriod (fun x ↦ a +ᵥ x) b) ∈ comap ((zmultiplesHom ↥(zmultiples a)) ⟨a, ⋯⟩) (stabilizer (↥(zmultiples a)) b)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

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

Tactic:
by
  simp_rw [isCyclic_iff_exists_zpowers_eq_top, ← card_eq_iff_eq_top, Nat.card_zpowers]

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:
by
  classical
  rw [exponent, dif_pos]
  · apply Nat.find_min'
    exact ⟨hpos, hG⟩
  · exact ⟨n, hpos, hG⟩

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
⊢ IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k

Tactic:
by
  simp_rw [isPGroup_iff_orderOf_dvd_pow, Nat.dvd_prime_pow Fact.out]
  exact forall_congr' fun g ↦ ⟨by grind, .imp <| by grind⟩

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : H.FiniteIndex
n : ℕ
hn : Nat.card (G ⧸ H.normalCore) = p ^ n
k : ℕ
left✝ : k ≤ n
hk2 : H.index = p ^ k
⊢ ∃ n, H.index = p ^ n

Tactic:
exact ⟨k, hk2⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ¬ExponentExists G
⊢ exponent G = sSup (Set.range fun g ↦ orderOf g)

Tactic:
← exponent_eq_zero_iff

Goal state after:
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G = 0
⊢ exponent G = sSup (Set.range fun g ↦ orderOf g)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1.fst
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ (g ^ GCDMonoid.lcm (exponent M₁) (exponent M₂)).1 = 1.1

Tactic:
rw [Prod.pow_fst, Prod.fst_one, ← orderOf_dvd_iff_pow_eq_one]

Goal state after:
case refine_1.fst
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ orderOf g.1 ∣ GCDMonoid.lcm (exponent M₁) (exponent M₂)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun x ↦ a ^ x) i = ↑b
⊢ ↑b ^ orderOf a = 1

Tactic:
← hi,

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun x ↦ a ^ x) i = ↑b
⊢ (fun x ↦ a ^ x) i ^ orderOf a = 1
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:
by
  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.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
x✝ : ℤ
⊢ ↑(addOrderOf g) ∣ x✝ ↔ ∃ k, ↑(addOrderOf g) * k = x✝

Tactic:
dvd_def,

Goal state after:
G : Type u_2
inst✝ : AddGroup G
g : G
x✝ : ℤ
⊢ (∃ c, x✝ = ↑(addOrderOf g) * c) ↔ ∃ k, ↑(addOrderOf g) * k = x✝
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
n : ℕ
hn : n ≠ 0
⊢ IsMulTorsion (G ⧸ (powMonoidHom n).range)

Tactic:
simp only [IsMulTorsion, isOfFinOrder_iff_pow_eq_one]

Goal state after:
G : Type u_1
inst✝ : CommGroup G
n : ℕ
hn : n ≠ 0
⊢ ∀ (g : G ⧸ (powMonoidHom n).range), ∃ n_1, 0 < n_1 ∧ g ^ n_1 = 1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case h
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯.some
Q : Subgroup G := map (comap f ↑P).subtype ↑Q₀
hPQ : map f Q ≤ ↑P
hpQ : IsPGroup p ↥Q
hQ : ¬p ∣ Q.index
⊢ ↑P = map f ↑(hpQ.toSylow hQ)

Tactic:
exact ((hpQ.map f).toSylow (fun h ↦ hQ (h.trans (Q.index_map_dvd hf)))).3 P.2 hPQ

Goal state after:
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
hab : a < b
⊢ ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
obtain ⟨x, hx, hxmin⟩ := (LocallyFiniteOrder.finsetIoc a b).exists_minimal
      ⟨b, by simpa [LocallyFiniteOrder.finset_mem_Ioc]⟩
    simp only [LocallyFiniteOrder.finset_mem_Ioc] at hx hxmin
    exact ⟨x, ⟨hx.1, fun c hac hcx ↦ hcx.not_ge <| hxmin ⟨hac, hcx.le.trans hx.2⟩ hcx.le⟩, hx.2⟩

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

Goal state before:
pp: case inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : Nat.card ↥f.range = 1
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Infinite ↥f.ker
⊢ IsCyclic M

Tactic:
rw [← f.range.eq_bot_iff_card, f.range_eq_bot_iff, ← f.ker_eq_top_iff] at h

Goal state after:
case inl
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : f.ker = ⊤
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝ : Infinite ↥f.ker
⊢ IsCyclic M
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
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
have hM := isCyclic_left_of_prod M N

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
⊢ (Nat.card M).Coprime (Nat.card N)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: 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

Tactic:
apply MulEquiv.ofBijective (Subgroup.noncommPiCoprod hcomm)

Goal state after:
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 ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Bijective ⇑(noncommPiCoprod hcomm)
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
A B : Submodule R M
hAB : A ≤ B
f : Submodule R ↥B ≃o ↑(Set.Iic B) := B.mapIic
hf : f = B.mapIic
⊢ IsCoatom ⟨A, hAB⟩ ↔ IsCoatom (B.mapIic (Submodule.comap B.subtype A))

Tactic:
simp [-OrderIso.isCoatom_iff, Submodule.map_comap_subtype, inf_eq_right.2 hAB]

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

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

Tactic:
le_biSup p ‹_›

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
hS : IsSemisimpleModule S S
this✝ : Module (R × S) R := Module.compHom R (RingHom.fst R S)
hR : IsSemisimpleModule (R × S) R
this : Module (R × S) S := Module.compHom S (RingHom.snd R S)
_e₁ : R →ₛₗ[RingHom.fst R S] R :=
  let __src := AddMonoidHom.id R;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
_e₂ : S →ₛₗ[RingHom.snd R S] S :=
  let __src := AddMonoidHom.id S;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleRing (R × S)

Tactic:
← _e₂.isSemisimpleModule_iff_of_bijective Function.bijective_id

Goal state after:
ι : 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
this✝ : Module (R × S) R := Module.compHom R (RingHom.fst R S)
hR : IsSemisimpleModule (R × S) R
this : Module (R × S) S := Module.compHom S (RingHom.snd R S)
hS : IsSemisimpleModule (R × S) S
_e₁ : R →ₛₗ[RingHom.fst R S] R :=
  let __src := AddMonoidHom.id R;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
_e₂ : S →ₛₗ[RingHom.snd R S] S :=
  let __src := AddMonoidHom.id S;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleRing (R × S)
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
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
N : Type ?u.26
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module R[X] N
inst✝ : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), f (a • m) = X • f m
p✝ p q : R[X]
hp : ∀ (x : AEval R M a), (f ∘ₗ ↑(of R M a).symm).toFun (p • x) = (RingHom.id R[X]) p • (f ∘ₗ ↑(of R M a).symm).toFun x
hq : ∀ (x : AEval R M a), (f ∘ₗ ↑(of R M a).symm).toFun (q • x) = (RingHom.id R[X]) q • (f ∘ₗ ↑(of R M a).symm).toFun x
m : AEval R M a
⊢ (f ∘ₗ ↑(of R M a).symm).toFun ((p + q) • m) = (RingHom.id R[X]) (p + q) • (f ∘ₗ ↑(of R M a).symm).toFun m

Tactic:
by simp_all [add_smul]

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case succ.refine_2
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
x y : R
hx : (monomial (n + 1)) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
hy : (monomial (n + 1)) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
⊢ (monomial (n + 1)) x + (monomial (n + 1)) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
exact Subalgebra.add_mem _ hx hy

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
inst✝ : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ↑(∏ x ∈ S, ⋯.choose) ∈ ↑⊤.annihilator

Tactic:
Submonoid.coe_finsetProd,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ∏ i ∈ S, ↑⋯.choose ∈ ↑⊤.annihilator
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ { coeff := f.coeff.sum Finsupp.single } ∈ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i))

Tactic:
ofCoeff_finsuppSum

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ (f.coeff.sum fun i n ↦ { coeff := Finsupp.single i n }) ∈ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i))
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
⊢ I • Submodule.map (Submodule.subtype I) ⊤ ≤ I ^ 2

Tactic:
Submodule.map_top,

Goal state after:
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
⊢ I • (Submodule.subtype I).range ≤ I ^ 2
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.cotangentIdeal ^ 2 = ⊥

Tactic:
by
  rw [eq_bot_iff, pow_two I.cotangentIdeal, ← smul_eq_mul]
  intro x hx
  refine Submodule.smul_induction_on hx ?_ ?_
  · rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩; apply (Submodule.Quotient.eq _).mpr _
    rw [sub_zero, pow_two]; exact Ideal.mul_mem_mul hx hy
  · intro x y hx hy; exact add_mem hx hy

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
H : Submodule.map (maximalIdeal R).toCotangent M = ⊤
⊢ Submodule.map (Submodule.subtype (maximalIdeal R)) ⊤ ≤ Submodule.map (Submodule.subtype (maximalIdeal R)) M

Tactic:
Submodule.map_top,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
H : Submodule.map (maximalIdeal R).toCotangent M = ⊤
⊢ (Submodule.subtype (maximalIdeal R)).range ≤ Submodule.map (Submodule.subtype (maximalIdeal R)) M
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
H : Submodule.map (maximalIdeal R).toCotangent M = ⊤
⊢ maximalIdeal R ≤ Submodule.map (Submodule.subtype (maximalIdeal R)) ⊤

Tactic:
Submodule.map_top,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
H : Submodule.map (maximalIdeal R).toCotangent M = ⊤
⊢ maximalIdeal R ≤ (Submodule.subtype (maximalIdeal R)).range
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 ↥(maximalIdeal R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span R s = ⊤
⊢ Submodule.map (maximalIdeal R).toCotangent ⊤ = ⊤

Tactic:
Submodule.map_top,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set ↥(maximalIdeal R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span R s = ⊤
⊢ (maximalIdeal R).toCotangent.range = ⊤
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 = Submodule.map (maximalIdeal R • ⊤).mkQ ⊤

Tactic:
Submodule.map_top,

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 = (maximalIdeal R • ⊤).mkQ.range
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ finrank (ResidueField R) (CotangentSpace R) = 0 ↔ IsField R

Tactic:
rw [finrank_zero_iff, subsingleton_cotangentSpace_iff]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, R ∙ (Submodule.subtype (maximalIdeal R)) x = map (Submodule.subtype (maximalIdeal R)) ⊤) ↔
    ∃ a, maximalIdeal R = R ∙ a

Tactic:
Submodule.map_top,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, R ∙ (Submodule.subtype (maximalIdeal R)) x = (Submodule.subtype (maximalIdeal R)).range) ↔
    ∃ a, maximalIdeal R = R ∙ a
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) =
    (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫
      (μ F m₁ (m₂ ⊗ m₃)).app X ≫ (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (δ F (m₁ ⊗ m₂) m₃).app X

Tactic:
by
  rw [← associativity_app_assoc]
  simp

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

Goal state before:
pp: case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
i k : ι
hik : c.Rel i k
hk : k = j
⊢ 0 = K.d i k ≫ (K.XIsoOfEq hk).hom ≫ φ ≫ (singleObjXIsoOfEq c j A k hk).inv

Tactic:
subst hk
      simp only [XIsoOfEq_rfl, Iso.refl_hom, id_comp, reassoc_of% hφ i hik, zero_comp]

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

Goal state before:
pp: case refine_2.refine_2
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✝ : ↥(KaehlerDifferential.ideal R S)
hx : x✝ ∈ Submodule.restrictScalars S (KaehlerDifferential.ideal R S • ⊤)
x y : ↥(KaehlerDifferential.ideal R S)
ex : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) x = 0
⊢ (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) y = 0 →
    (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) (x + y) = 0

Tactic:
ey

Goal state after:
case refine_2.refine_2
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✝ : ↥(KaehlerDifferential.ideal R S)
hx : x✝ ∈ Submodule.restrictScalars S (KaehlerDifferential.ideal R S • ⊤)
x y : ↥(KaehlerDifferential.ideal R S)
ex : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) x = 0
ey : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) y = 0
⊢ (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) (x + y) = 0
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cone F
hs : (i : ι) → IsLimit ((eval C c i).mapCone s)
t : Cone F
i i' : ι
x✝ : c.Rel i i'
⊢ (hs i).lift ((eval C c i).mapCone t) ≫ s.pt.d i i' = t.pt.d i i' ≫ (hs i').lift ((eval C c i').mapCone t)

Tactic:
apply IsLimit.hom_ext (hs i')

Goal state after:
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cone F
hs : (i : ι) → IsLimit ((eval C c i).mapCone s)
t : Cone F
i i' : ι
x✝ : c.Rel i i'
⊢ ∀ (j : J),
    ((hs i).lift ((eval C c i).mapCone t) ≫ s.pt.d i i') ≫ ((eval C c i').mapCone s).π.app j =
      (t.pt.d i i' ≫ (hs i').lift ((eval C c i').mapCone t)) ≫ ((eval C c i').mapCone s).π.app j
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
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftComm X i j).hom ≫ (shiftFunctor C i).map ((shiftFunctor C j).map f) =
    (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫ (shiftComm Y i j).hom

Tactic:
by
  rw [shiftComm', ← shiftComm_symm, Iso.symm_hom, Iso.inv_hom_id_assoc]

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 : ι
I : C
inst✝ : Injective I
⊢ Injective (((single C c i).obj I).X j)

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

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
r : R
x y : S
this : SMulZeroClass R S := inferInstance
⊢ (y𝖣r • x) = r • y𝖣x

Tactic:
rw [Algebra.smul_def, KaehlerDifferential.kerTotal_mkQ_single_mul,
    KaehlerDifferential.kerTotal_mkQ_single_algebraMap, add_zero, ← LinearMap.map_smul_of_tower,
    Finsupp.smul_single, mul_comm, Algebra.smul_def]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.IsInvertedBy F → W.isoClosure.IsInvertedBy F

Tactic:
intro h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
    simp only [Arrow.iso_w' e, F.map_comp]
    have := h _ hf'
    infer_instance

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ C.d i ((ComplexShape.down ℕ).next i) ≫ f ((ComplexShape.down ℕ).next i) i = C.d i (i - 1) ≫ f (i - 1) i

Tactic:
cases i

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ C.d 0 ((ComplexShape.down ℕ).next 0) ≫ f ((ComplexShape.down ℕ).next 0) 0 = C.d 0 (0 - 1) ≫ f (0 - 1) 0

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ C.d (n✝ + 1) ((ComplexShape.down ℕ).next (n✝ + 1)) ≫ f ((ComplexShape.down ℕ).next (n✝ + 1)) (n✝ + 1) =
    C.d (n✝ + 1) (n✝ + 1 - 1) ≫ f (n✝ + 1 - 1) (n✝ + 1)