mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
y : A
G : AwayMap (x + y) C
⊢ G x + mk' G y ⟨x + y, ⋯⟩ = 0

Tactic:
add_mk'_eq_mk'_of_add,

Goal state after:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
y : A
G : AwayMap (x + y) C
⊢ mk' G (x + y) ⟨x + y, ⋯⟩ = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case succ.mpr
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
u : Multiset R
hu : normalizedFactors b = replicate (n + 1) (normalize a) + u
⊢ a ^ (n + 1) ∣ b

Tactic:
rw [← (prod_normalizedFactors hb).dvd_iff_dvd_right, hu, prod_add, prod_replicate]

Goal state after:
case succ.mpr
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
u : Multiset R
hu : normalizedFactors b = replicate (n + 1) (normalize a) + u
⊢ a ^ (n + 1) ∣ normalize a ^ (n + 1) * u.prod
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
S : Under R
⊢ { app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app
        ((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S) ≫
      (Under.forget R ⋙ forget₂ CommRingCat CommMonCat).map
        ({
              app := fun S ↦
                Under.homMk
                  (ofHom
                    (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                      (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                  ⋯,
              naturality := ⋯ }.app
          S) =
    𝟙 ((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)

Tactic:
by dsimp; ext; simp [MonoidAlgebra.liftNCRingHom]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
⊢ a ∣ b

Tactic:
dvd_iff_normalizedFactors_le_normalizedFactors ha hb,

Goal state after:
case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
⊢ normalizedFactors a ≤ normalizedFactors b
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
| comap f (jacobson R₂ M₂)

Tactic:
rw [jacobson, sInf_eq_iInf', comap_iInf]

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
| ⨅ i, comap f ↑i
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: S : Type u_4
T : Type u_5
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
h₁ : Function.Surjective ⇑(algebraMap S T)
r : S
hr : IsUnit ((algebraMap S T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥
x y : S
h : (algebraMap S T) x = (algebraMap S T) y
⊢ x - y ∈ ↑(RingHom.ker (algebraMap S T)) ∧ (DistribSMul.toLinearMap S S (r ^ n)) (x - y) = r ^ n * (x - y)

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
s : S
⊢ ∀ (n : ℕ), ∃ c l m k, f (a ^ (k + n) * c) = f (a ^ (k + l) * b ^ m) * s

Tactic:
n

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
s : S
n : ℕ
⊢ ∃ c l m k, f (a ^ (k + n) * c) = f (a ^ (k + l) * b ^ m) * s
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a

Tactic:
have mem := (Ideal.eq_top_iff_one _).mp span_eq

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span s
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : map (Quotient.mk I) I.jacobson = map (Quotient.mk I) I
⊢ ⊥.jacobson = ⊥

Tactic:
map_jacobson_of_surjective hf (le_of_eq mk_ker)

Goal state after:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : (map (Quotient.mk I) I).jacobson = map (Quotient.mk I) I
⊢ ⊥.jacobson = ⊥
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : I.radical = I.jacobson
this : (map (Quotient.mk I) I).radical = map (Quotient.mk I) I.jacobson
⊢ ⊥.radical = ⊥.jacobson

Tactic:
map_jacobson_of_surjective hf (le_of_eq mk_ker)

Goal state after:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : I.radical = I.jacobson
this : (map (Quotient.mk I) I).radical = (map (Quotient.mk I) I).jacobson
⊢ ⊥.radical = ⊥.jacobson
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝¹ : ↑↑s → R
eq✝¹ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝¹ a)
N✝ : ℕ := s.attach.sup n
r✝ : ↑↑s → R := fun a ↦ ↑a ^ (N✝ - n a) * r✝¹ a
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N✝) = (algebraMap R (Away ↑a)) (r✝ a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2✝ : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
eq2 : ∀ (a b : ↑↑s), r a * ↑b ^ N = r b * ↑a ^ N
c : ↑↑s → R
eq1 : ∑ i, c i • ↑i ^ N = 1
a : ↑↑s
⊢ (algebraMap R (Away ↑a)) (∑ x, c x * (r a * ↑x ^ N)) = (algebraMap R (Away ↑a)) (r a)

Tactic:
mul_left_comm (c _),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝¹ : ↑↑s → R
eq✝¹ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝¹ a)
N✝ : ℕ := s.attach.sup n
r✝ : ↑↑s → R := fun a ↦ ↑a ^ (N✝ - n a) * r✝¹ a
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N✝) = (algebraMap R (Away ↑a)) (r✝ a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2✝ : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
eq2 : ∀ (a b : ↑↑s), r a * ↑b ^ N = r b * ↑a ^ N
c : ↑↑s → R
eq1 : ∑ i, c i • ↑i ^ N = 1
a : ↑↑s
⊢ (algebraMap R (Away ↑a)) (∑ x, r a * (c x * ↑x ^ N)) = (algebraMap R (Away ↑a)) (r a)
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O X✝ : C
inst✝⁸ : MonObj M
inst✝⁷ : MonObj N
inst✝⁶ : MonObj O
inst✝⁵ : BraidedCategory C
X Y Z W : C
inst✝⁴ : MonObj X
inst✝³ : MonObj Y
inst✝² : MonObj Z
inst✝¹ : MonObj W
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ μ ≫ f ▷ Z = (f ▷ Z ⊗ₘ f ▷ Z) ≫ μ

Tactic:
simpa using ((inferInstance : IsMonHom (f ⊗ₘ (𝟙 Z)))).mul_hom

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)

Tactic:
apply PullbackCone.IsLimit.hom_ext H.isLimit <;> refine e.trans ?_

Goal state after:
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ s.ι = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst

case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ s.ι = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
ι : Type u_3
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Submonoid R
t : Finset ι
a : ι → A
s : ι → ↥S
⊢ ∏ i ∈ t, mk (a i) (s i) = mk (∏ i ∈ t, a i) (∏ i ∈ t, s i)

Tactic:
induction t using Finset.cons_induction

Goal state after:
case empty
R : Type u
inst✝² : CommSemiring R
ι : Type u_3
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Submonoid R
a : ι → A
s : ι → ↥S
⊢ ∏ i ∈ ∅, mk (a i) (s i) = mk (∏ i ∈ ∅, a i) (∏ i ∈ ∅, s i)

case cons
R : Type u
inst✝² : CommSemiring R
ι : Type u_3
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Submonoid R
a : ι → A
s : ι → ↥S
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∏ i ∈ s✝, mk (a i) (s i) = mk (∏ i ∈ s✝, a i) (∏ i ∈ s✝, s i)
⊢ ∏ i ∈ Finset.cons a✝¹ s✝ h✝, mk (a i) (s i) = mk (∏ i ∈ Finset.cons a✝¹ s✝ h✝, a i) (∏ i ∈ Finset.cons a✝¹ s✝ h✝, s i)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
p : LocalizedModule S M
⊢ 1 • p = p

Tactic:
by
  induction p with | _ m s
  rw [show (1 : T) = IsLocalization.mk' T (1 : R) (1 : S) by rw [IsLocalization.mk'_one, map_one]]
  rw [mk'_smul_mk, one_smul, one_mul]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Algebra

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : T.Algebra
f : X ⟶ T.forget.obj Y
⊢ T.η.app X ≫ T.map f ≫ Y.a = f

Tactic:
rw [← T.η.naturality_assoc, Y.unit]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : T.Algebra
f : X ⟶ T.forget.obj Y
⊢ (𝟭 C).map f ≫ 𝟙 Y.A = f
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: R S : CommRingCat
A B : Type u
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra (↑R) A
inst✝ : Algebra (↑R) B
f : A →ₐ[↑R] B
⊢ (R.mkUnder A).hom ≫ CommRingCat.ofHom f.toRingHom = (R.mkUnder B).hom

Tactic:
ext a

Goal state after:
R S : CommRingCat
A B : Type u
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra (↑R) A
inst✝ : Algebra (↑R) B
f : A →ₐ[↑R] B
a : ↑R
⊢ (CommRingCat.Hom.hom ((R.mkUnder A).hom ≫ CommRingCat.ofHom f.toRingHom)) a =
    (CommRingCat.Hom.hom (R.mkUnder B).hom) a
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : M'
m : M
s : ↥S
eq1 : (m, s).2 • x = f (m, s).1
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m s) = x

Tactic:
fromLocalizedModule_mk,

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : M'
m : M
s : ↥S
eq1 : (m, s).2 • x = f (m, s).1
⊢ ↑⋯.unit⁻¹ (f m) = x
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝¹ : HasPullbacksAlong f
inst✝ : ∀ (Z : C) (g : Z ⟶ Y), Epi (pullback.fst g f)
⊢ (pullback f).Faithful

Tactic:
by
  have (Z : Over Y) : Epi ((mapPullbackAdj f).counit.app Z) := by
    simp only [Functor.comp_obj, Functor.id_obj, mapPullbackAdj_counit_app]; infer_instance
  exact (mapPullbackAdj f).faithful_R_of_epi_counit_app

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m 1) = f m

Tactic:
fromLocalizedModule_mk,

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
⊢ ↑⋯.unit⁻¹ (f m) = f m
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m 1) = mk' f m 1

Tactic:
fromLocalizedModule_mk,

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ ↑⋯.unit⁻¹ (f m) = mk' f m 1
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case left
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
⊢ (A.coproductCocone B).ι.app { as := WalkingPair.left } ≫
      ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom =
    s.ι.app { as := WalkingPair.left }

Tactic:
ext a

Goal state after:
case left
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
a : ↑((pair A B).obj { as := WalkingPair.left })
⊢ (Hom.hom
        ((A.coproductCocone B).ι.app { as := WalkingPair.left } ≫
          ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom))
      a =
    (Hom.hom (s.ι.app { as := WalkingPair.left })) a
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case right
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
⊢ (A.coproductCocone B).ι.app { as := WalkingPair.right } ≫
      ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom =
    s.ι.app { as := WalkingPair.right }

Tactic:
ext a

Goal state after:
case right
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
a : ↑((pair A B).obj { as := WalkingPair.right })
⊢ (Hom.hom
        ((A.coproductCocone B).ι.app { as := WalkingPair.right } ≫
          ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom))
      a =
    (Hom.hom (s.ι.app { as := WalkingPair.right })) a
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case left
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ { hom' := m }.hom.toIntAlgHom.comp Algebra.TensorProduct.includeLeft =
    (Algebra.TensorProduct.liftEquiv.symm
          (Hom.hom
              (ofHom
                (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                    ⋯).toRingHom)).toIntAlgHom).1.1

Tactic:
ext a

Goal state after:
case left
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
a : ↑A
⊢ ({ hom' := m }.hom.toIntAlgHom.comp Algebra.TensorProduct.includeLeft) a =
    (Algebra.TensorProduct.liftEquiv.symm
            (Hom.hom
                (ofHom
                  (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                      ⋯).toRingHom)).toIntAlgHom).1.1
      a
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
h_surj : Function.Surjective ⇑h
⊢ Function.Surjective ⇑((map S f g) h)

Tactic:
by
  intro x
  obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S g x
  obtain ⟨x, rfl⟩ := h_surj x
  exact ⟨mk' f x s, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConeCategory

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
G : J ⥤ K
X : C
F : K ⥤ C
f : (Y : J) → X ⟶ F.obj (G.obj Y)
h : ∀ {Y Z : J} (g : Y ⟶ Z), f Y ≫ F.map (G.map g) = f Z
⊢ ∀ ⦃X_1 Y : J⦄ (f_1 : X_1 ⟶ Y), ((const J).obj X).map f_1 ≫ f Y = f X_1 ≫ (G ⋙ F).map f_1

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConeCategory

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
G : J ⥤ K
F : K ⥤ C
X : C
f : (Y : J) → F.obj (G.obj Y) ⟶ X
h : ∀ {Y Z : J} (g : Y ⟶ Z), F.map (G.map g) ≫ f Z = f Y
⊢ ∀ ⦃X_1 Y : J⦄ (f_1 : X_1 ⟶ Y), (G ⋙ F).map f_1 ≫ f Y = f X_1 ≫ ((const J).obj X).map f_1

Tactic:
by simp [h]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Finset R
inst✝ : (span ↑s).IsTwoSided
t : Finset M
⊢ (span ↑s • Submodule.span R ↑t).FG

Tactic:
rw [Submodule.span_smul_span, ← s.coe_smul]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Finset R
inst✝ : (span ↑s).IsTwoSided
t : Finset M
⊢ (Submodule.span R ↑(s • t)).FG
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
X : ι → C
inst✝ : Small.{w, u_1} ι
⊢ Function.Surjective fun i ↦ ⟨X i, ⋯⟩

Tactic:
by rintro ⟨_, ⟨i⟩⟩; simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
⊢ colimMap
        (whiskerRight (Grothendieck.ιNatTrans (𝟙 X)) G ≫
          ((F.map (𝟙 X)).toFunctor.associator (Grothendieck.ι F X) G).hom) ≫
      colimit.pre (Grothendieck.ι F X ⋙ G) (F.map (𝟙 X)).toFunctor =
    𝟙 (colimit (Grothendieck.ι F X ⋙ G))

Tactic:
ext d
    simp only [Functor.comp_obj, Grothendieck.ιNatTrans, Grothendieck.ι_obj, ι_colimMap_assoc,
      NatTrans.comp_app, whiskerRight_app, Functor.associator_hom_app, Category.comp_id,
      colimit.ι_pre]
    conv_rhs => rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F X ⋙ G)
      (j := (F.map (𝟙 X)).toFunctor.obj d) (by simp)]
    rw [← eqToHom_map G (by simp), Grothendieck.eqToHom_eq]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: case h
J : Type v₁
⊢ ∀ (p : Set (WidePullbackShape J)),
    ?j₀ ∈ p → (∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : WidePullbackShape J), j ∈ p

Tactic:
introv hp t

Goal state after:
case h
J : Type v₁
p : Set (WidePullbackShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : WidePullbackShape J
⊢ j ∈ p
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: case h
J : Type v₁
⊢ ∀ (p : Set (WidePushoutShape J)),
    ?j₀ ∈ p → (∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : WidePushoutShape J), j ∈ p

Tactic:
introv hp t

Goal state after:
case h
J : Type v₁
p : Set (WidePushoutShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : WidePushoutShape J
⊢ j ∈ p
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫
      ((prod.functor.obj X).mapCone c).π.app j ≫ prod.fst =
    s.π.app j ≫ prod.fst

Tactic:
limMap_π,

Goal state after:
case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫
      limit.π (pair X c.pt) { as := WalkingPair.left } ≫ (mapPair (𝟙 X) (c.π.app j)).app { as := WalkingPair.left } =
    s.π.app j ≫ prod.fst
Module: Mathlib.CategoryTheory.EffectiveEpi.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝¹ : HasCoproduct X
inst✝ : IsIso (Sigma.desc π)
W✝ : C
e : (a : α) → X a ⟶ W✝
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W✝
hm : ∀ (a : α), π a ≫ m = e a
⊢ Sigma.desc π ≫ m = Sigma.desc e

Tactic:
ext a

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝¹ : HasCoproduct X
inst✝ : IsIso (Sigma.desc π)
W✝ : C
e : (a : α) → X a ⟶ W✝
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W✝
hm : ∀ (a : α), π a ≫ m = e a
a : α
⊢ Sigma.ι X a ≫ Sigma.desc π ≫ m = Sigma.ι X a ≫ Sigma.desc e