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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
e : ↑{p | p.IsPrime ∧ I ≤ p} ≃o ↑(zeroLocus ↑I) :=
  { toFun := fun x ↦ ⟨{ asIdeal := ↑x, isPrime := ⋯ }, ⋯⟩, invFun := fun x ↦ ⟨(↑x).asIdeal, ⋯⟩, left_inv := ⋯,
    right_inv := ⋯, map_rel_iff' := ⋯ }
⊢ ↑I.minimalPrimes ≃o (↑(irreducibleComponents ↑(zeroLocus ↑I)))ᵒᵈ

Tactic:
irreducibleComponents_eq_maximals_closed

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal R
e : ↑{p | p.IsPrime ∧ I ≤ p} ≃o ↑(zeroLocus ↑I) :=
  { toFun := fun x ↦ ⟨{ asIdeal := ↑x, isPrime := ⋯ }, ⋯⟩, invFun := fun x ↦ ⟨(↑x).asIdeal, ⋯⟩, left_inv := ⋯,
    right_inv := ⋯, map_rel_iff' := ⋯ }
⊢ ↑I.minimalPrimes ≃o (↑{s | Maximal (fun x ↦ IsClosed x ∧ IsIrreducible x) s})ᵒᵈ
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
e : ↑{p | p.IsPrime ∧ ⊥ ≤ p} ≃o PrimeSpectrum R :=
  { toFun := fun x ↦ { asIdeal := ↑x, isPrime := ⋯ }, invFun := fun x ↦ ⟨x.asIdeal, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
    map_rel_iff' := ⋯ }
⊢ ↑(minimalPrimes R) ≃o (↑(irreducibleComponents (PrimeSpectrum R)))ᵒᵈ

Tactic:
irreducibleComponents_eq_maximals_closed

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
e : ↑{p | p.IsPrime ∧ ⊥ ≤ p} ≃o PrimeSpectrum R :=
  { toFun := fun x ↦ { asIdeal := ↑x, isPrime := ⋯ }, invFun := fun x ↦ ⟨x.asIdeal, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
    map_rel_iff' := ⋯ }
⊢ ↑(minimalPrimes R) ≃o (↑{s | Maximal (fun x ↦ IsClosed x ∧ IsIrreducible x) s})ᵒᵈ
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
rintro rfl

Goal state after:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ closedPoint R ∈ ⊤
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
⊢ freeRank G = 0 ↔ IsMulTorsion G

Tactic:
freeRank,

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
⊢ Group.rank (G ⧸ torsion G) = 0 ↔ IsMulTorsion G
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: 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
⊢ ↥f.ker ≃* M

Tactic:
MonoidHom.ker_snd

Goal state after:
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
⊢ ↥(⊤.prod ⊥) ≃* M
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 : ι
this : i ∈ Finset.cons a t hat → i ≠ a → ↑(μ a) ∈ I i
hi : i ∈ t
i✝ : i ≠ Exists.choose h
⊢ i ≠ a

Tactic:
rintro rfl

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝¹ : DecidableEq ι
t : Finset ι
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 : ι
hi : i ∈ t
i✝ : i ≠ Exists.choose h
hat : i ∉ t
μ : (i_1 : ι) → ↥(⨅ j ∈ Finset.cons i t hat, ⨅ (_ : j ≠ i_1), I j)
hμ : ↑(μ i) + ∑ x ∈ t, ↑(μ x) = 1
this : i ∈ Finset.cons i t hat → i ≠ i → ↑(μ i) ∈ I i
⊢ False
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 : ι
this : ∀ i_1 ∈ Finset.cons a t hat, i_1 ≠ i → ↑(μ i) ∈ I i_1
⊢ ∀ i_1 ∈ t, i_1 ≠ i → ↑(μ i) ∈ I i_1

Tactic:
intro j hj ij

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
i : ι
this : ∀ i_1 ∈ Finset.cons a t hat, i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj : j ∈ t
ij : j ≠ i
⊢ ↑(μ i) ∈ I j
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (x ⊔ y)
hyz : IsMaximal y (x ⊔ y)
⊢ IsMaximal (y ⊓ x) y

Tactic:
rw [sup_comm] at hxz hyz

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (y ⊔ x)
hyz : IsMaximal y (y ⊔ x)
⊢ IsMaximal (y ⊓ x) y
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_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μ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
x : ι
hx : x ∈ t
this : ∀ i ∈ Finset.cons a t hat, i ≠ x → ↑(μ x) ∈ I i
⊢ a ≠ x

Tactic:
rintro rfl

Goal state after:
case refine_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μ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
hx : a ∈ t
this : ∀ i ∈ Finset.cons a t hat, i ≠ a → ↑(μ a) ∈ I i
⊢ False
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr.refine_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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ i ∈ t, v ∈ I i
⊢ ∀ i_1 ∈ Finset.cons a t hat, i_1 ≠ i → v ∈ I i_1

Tactic:
intro j hj ij

Goal state after:
case refine_2.mpr.refine_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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ i ∈ t, v ∈ I i
j : ι
hj : j ∈ Finset.cons a t hat
ij : j ≠ i
⊢ v ∈ I j
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr.refine_2
ι : 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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ∀ i_1 ∈ t, i_1 ≠ i → ↑(μ i) ∈ I i_1
⊢ ∀ i_1 ∈ Finset.cons a t hat, i_1 ≠ i → u * ↑(μ i) ∈ I i_1

Tactic:
intro j hj ij

Goal state after:
case refine_2.mpr.refine_2
ι : 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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ∀ i_1 ∈ t, i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj : j ∈ Finset.cons a t hat
ij : j ≠ i
⊢ u * ↑(μ i) ∈ I j
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
⊢ IsSemisimpleRing S

Tactic:
by
  let : Module R S := Module.compHom _ f
  have : RingHomSurjective f := ⟨hf⟩
  let e : S →ₛₗ[f] S := { AddMonoidHom.id S with map_smul' := fun _ _ ↦ rfl }
  rw [IsSemisimpleRing, ← e.isSemisimpleModule_iff_of_bijective Function.bijective_id]
  infer_instance

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

Goal state before:
pp: case smul
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
g : End R M
x✝ : M
hx✝ : x✝ ∈ span (End R M) ↑s
h : ((toModuleEnd (End R M) M) r) x✝ = f x✝
⊢ ((toModuleEnd (End R M) M) r) (g • x✝) = f (g • x✝)

Tactic:
simp_rw [map_smul, h]

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

Goal state before:
pp: case refine_2.mpr.refine_3.e_a.hnc
ι : 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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
⊢ ¬j = a

Tactic:
rintro rfl

Goal state after:
case refine_2.mpr.refine_3.e_a.hnc
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
t : Finset ι
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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
hat : j ∉ t
Hb : ∀ b ∈ ↑t, j ≠ b → I j ⊔ I b = ⊤
hu : u ∈ I j
⊢ False
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 : R[X]
k : R
m : AEval R M a
⊢ (f ∘ₗ ↑(of R M a).symm).toFun (C k • m) = (RingHom.id R[X]) (C k) • (f ∘ₗ ↑(of R M a).symm).toFun m

Tactic:
by simp [C_eq_algebraMap]

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : R[X]
q : PolynomialModule R M
⊢ eval₂ (algebraMap R R[X]) p p' • (eval p) ((map R[X] (lsingle R 0)) q) = eval₂ C p p' • (comp p) q

Tactic:
comp_apply

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : R[X]
q : PolynomialModule R M
⊢ eval₂ (algebraMap R R[X]) p p' • (eval p) ((map R[X] (lsingle R 0)) q) =
    eval₂ C p p' • (eval p) ((map R[X] (lsingle R 0)) q)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this : torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i)
j : ι
hj : j ∈ T
⊢ i ≠ j

Tactic:
rintro rfl

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this : torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i)
hj : i ∈ T
⊢ False
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : R
⊢ Function.LeftInverse (fun p ↦ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ })
    (restrictScalarsEmbedding R (R ⧸ R ∙ a) ↥(torsionBy R M a)).toFun

Tactic:
intro; ext; simp [restrictScalarsEmbedding]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a : R
⊢ Function.RightInverse (fun p ↦ { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ })
    (restrictScalarsEmbedding R (R ⧸ R ∙ a) ↥(torsionBy R M a)).toFun

Tactic:
intro; ext; simp [restrictScalarsEmbedding]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : ↥I
⊢ x • I.toCotangent m = 0

Tactic:
rw [← map_smul, Ideal.toCotangent_eq_zero, pow_two]

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : ↥I
⊢ ↑(x • m) ∈ I * I
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)
⊢ M = ⊤ → Submodule.map (maximalIdeal R).toCotangent M = ⊤

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ Submodule.map (maximalIdeal R).toCotangent ⊤ = ⊤
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) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
rw [Module.finrank_le_one_iff_top_isPrincipal, isPrincipal_iff,
    (maximalIdeal R).toCotangent_surjective.exists, isPrincipal_iff]
  simp_rw [← Set.image_singleton, eq_comm (a := ⊤), CotangentSpace.span_image_eq_top_iff,
    ← (map_injective_of_injective (injective_subtype _)).eq_iff, map_span, Set.image_singleton,
    Submodule.map_top, range_subtype, eq_comm (a := maximalIdeal R)]
  exact ⟨fun ⟨x, h⟩ ↦ ⟨_, h⟩, fun ⟨x, h⟩ ↦ ⟨⟨x, h ▸ subset_span (Set.mem_singleton x)⟩, h⟩⟩

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₁ 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)
⊢ (ConcreteCategory.hom (M.map f)) (r • x) = (RingHom.id ↑(R.obj X)) r • (ConcreteCategory.hom (M.map f)) x

Tactic:
simp only [ModuleCat.restrictScalars.smul_def (R := R.obj X), RingHom.id_apply, M.map_smul]
      rw [← RingCat.comp_apply, ← R.map_comp]
      congr
      apply hX.hom_ext

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✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd C 0 a).hom.app X = eqToHom ⋯ ≫ (shiftFunctor C a).map ((shiftFunctorZero C A).inv.app X)

Tactic:
simp [← shiftFunctorAdd'_zero_add_hom_app, shiftFunctorAdd']

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
φ : C ⟶ (single₀ V).obj X
⊢ C.d 1 0 ≫ φ.f 0 = 0

Tactic:
rw [← φ.comm 1 0, HomologicalComplex.single_obj_d, comp_zero]

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
f : { f // C.d 1 0 ≫ f = 0 }
i : ℕ
hi : (ComplexShape.down ℕ).Rel i 0
⊢ C.d i 0 ≫ ↑f = 0

Tactic:
obtain rfl : i = 1 := by simpa using hi.symm
    exact f.2

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f : { f // f ≫ C.d 0 1 = 0 }
i : ℕ
hi : (ComplexShape.up ℕ).Rel 0 i
⊢ ↑f ≫ C.d 0 i = 0

Tactic:
obtain rfl : i = 1 := by simpa using hi.symm
    exact f.2

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✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv = (shiftFunctor C 0).map f

Tactic:
rw [Iso.app_inv, Iso.app_hom]

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftFunctorZero C A).hom.app X ≫ f ≫ (shiftFunctorZero C A).inv.app Y = (shiftFunctor C 0).map f
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X✝ : α → V
d_X : (n : α) → X✝ (n + 1) ⟶ X✝ n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y✝ : α → V
d_Y : (n : α) → Y✝ (n + 1) ⟶ Y✝ n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
X Y : ChainComplex V α
f : (i : α) → X.X i ⟶ Y.X i
comm : ∀ (i : α), f (i + 1) ≫ Y.d (i + 1) i = X.d (i + 1) i ≫ f i
n m : α
⊢ m + 1 = n → f n ≫ Y.d n m = X.d n m ≫ f m

Tactic:
rintro rfl

Goal state after:
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X✝ : α → V
d_X : (n : α) → X✝ (n + 1) ⟶ X✝ n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y✝ : α → V
d_Y : (n : α) → Y✝ (n + 1) ⟶ Y✝ n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
X Y : ChainComplex V α
f : (i : α) → X.X i ⟶ Y.X i
comm : ∀ (i : α), f (i + 1) ≫ Y.d (i + 1) i = X.d (i + 1) i ≫ f i
m : α
⊢ f (m + 1) ≫ Y.d (m + 1) m = X.d (m + 1) m ≫ f m
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'
j : J
eq : ∀ (k : ι) (j : J), (hs k).lift ((eval C c k).mapCone t) ≫ (s.π.app j).f k = (t.π.app j).f k
⊢ (hs i).lift ((eval C c i).mapCone t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' =
    t.pt.d i i' ≫ (hs i').lift ((eval C c i').mapCone t) ≫ (s.π.app j).f i'

Tactic:
eq 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
eq : ∀ (k : ι) (j : J), (hs k).lift ((eval C c k).mapCone t) ≫ (s.π.app j).f k = (t.π.app j).f k
⊢ (hs i).lift ((eval C c i).mapCone t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' = t.pt.d i i' ≫ (t.π.app j).f i'
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ p' + m + n = 0

Tactic:
rw [add_assoc, h, hp]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X✝ : α → V
d_X : (n : α) → X✝ n ⟶ X✝ (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y✝ : α → V
d_Y : (n : α) → Y✝ n ⟶ Y✝ (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
X Y : CochainComplex V α
f : (i : α) → X.X i ⟶ Y.X i
comm : ∀ (i : α), f i ≫ Y.d i (i + 1) = X.d i (i + 1) ≫ f (i + 1)
n m : α
⊢ n + 1 = m → f n ≫ Y.d n m = X.d n m ≫ f m

Tactic:
rintro rfl

Goal state after:
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X✝ : α → V
d_X : (n : α) → X✝ n ⟶ X✝ (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y✝ : α → V
d_Y : (n : α) → Y✝ n ⟶ Y✝ (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
X Y : CochainComplex V α
f : (i : α) → X.X i ⟶ Y.X i
comm : ∀ (i : α), f i ≫ Y.d i (i + 1) = X.d i (i + 1) ≫ f (i + 1)
n : α
⊢ f n ≫ Y.d n (n + 1) = X.d n (n + 1) ≫ f (n + 1)
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 : Cocone F
hs : (i : ι) → IsColimit ((eval C c i).mapCocone s)
t : Cocone F
i i' : ι
x✝ : c.Rel i i'
j : J
eq : ∀ (k : ι) (j : J), (s.ι.app j).f k ≫ (hs k).desc ((eval C c k).mapCocone t) = (t.ι.app j).f k
⊢ (t.ι.app j).f i ≫ t.pt.d i i' = (F.obj j).d i i' ≫ (s.ι.app j).f i' ≫ (hs i').desc ((eval C c i').mapCocone t)

Tactic:
eq 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 : Cocone F
hs : (i : ι) → IsColimit ((eval C c i).mapCocone s)
t : Cocone F
i i' : ι
x✝ : c.Rel i i'
j : J
eq : ∀ (k : ι) (j : J), (s.ι.app j).f k ≫ (hs k).desc ((eval C c k).mapCocone t) = (t.ι.app j).f k
⊢ (t.ι.app j).f i ≫ t.pt.d i i' = (F.obj j).d i i' ≫ (t.ι.app j).f i'
Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod

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
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
A : C
i : ι
f g : (K ⊞ L).X i ⟶ A
⊢ f = g → biprod.inl.f i ≫ f = biprod.inl.f i ≫ g ∧ biprod.inr.f i ≫ f = biprod.inr.f i ≫ g

Tactic:
rintro rfl

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
A : C
i : ι
f : (K ⊞ L).X i ⟶ A
⊢ biprod.inl.f i ≫ f = biprod.inl.f i ≫ f ∧ biprod.inr.f i ≫ f = biprod.inr.f i ≫ f
Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod

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
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
A : C
i : ι
f g : A ⟶ (K ⊞ L).X i
⊢ f = g → f ≫ biprod.fst.f i = g ≫ biprod.fst.f i ∧ f ≫ biprod.snd.f i = g ≫ biprod.snd.f i

Tactic:
rintro rfl

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
A : C
i : ι
f : A ⟶ (K ⊞ L).X i
⊢ f ≫ biprod.fst.f i = f ≫ biprod.fst.f i ∧ f ≫ biprod.snd.f i = f ≫ biprod.snd.f i