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

Goal state before:
pp: R✝ : Type u
A✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Bialgebra R✝ A✝
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : Coalgebra R A
counit_one : counit 1 = 1
counit_mul : ∀ {a b : A}, counit (a * b) = counit a * counit b
comul_one : comul 1 = 1
comul_mul : ∀ {a b : A}, comul (a * b) = comul a * comul b
x✝¹ x✝ : A
⊢ (((LinearMap.mul R A).compr₂ counit) x✝¹) x✝ = (((LinearMap.mul R R).compl₁₂ counit counit) x✝¹) x✝

Tactic:
exact counit_mul

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : Coalgebra R B
e : A ≃ B
this✝ : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
⊢ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul = LinearMap.lTensor A comul ∘ₗ comul

Tactic:
by
      ext
      apply (TensorProduct.map_bijective (e.linearEquiv R).bijective <|
        TensorProduct.map_bijective (e.linearEquiv R).bijective
        (e.linearEquiv R).bijective).injective
      simp +instances [coalgebraStruct, e.tensorProductAssoc_def R, TensorProduct.congr,
        ← LinearMap.comp_assoc, TensorProduct.map_map, ← TensorProduct.map_comp]
      simpa [LinearMap.comp_assoc, -coassoc_apply] using! coassoc_apply (R := R) (A := B) _

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a ⊔ a ⊓ b = a

Tactic:
dsimp only [(· ⊔ ·), (· ⊓ ·)]
  rw [← mul_assoc, mul_self, add_assoc, add_self, add_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O : C
inst✝⁸ : ComonObj M
inst✝⁷ : ComonObj N
inst✝⁶ : ComonObj O
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.OplaxMonoidal
X Y : C
inst✝² : ComonObj X
inst✝¹ : ComonObj Y
f : X ⟶ Y
inst✝ : IsComonHom f
⊢ F.map f ≫ Δ = Δ ≫ (F.map f ⊗ₘ F.map f)

Tactic:
dsimp
    rw [Category.assoc, δ_natural, ← F.map_comp_assoc, ← F.map_comp_assoc, hom_comul]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
P : Type u_3
inst✝⁵ : CommSemiring P
x : R
inst✝⁴ : Away x S
g : R →+* P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (f r))

Tactic:
rintro x ⟨n, rfl⟩
      use n
      simp

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
⊢ s ⊆ ↑(span s)

Tactic:
by
  intro x hx
  rw [SetLike.mem_coe, mem_iff]
  exact RingConGen.Rel.of _ _ (by simpa using hx)

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2.inl.inl.inl
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z y x : R
hy : y ∈ s
⊢ y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_2.inl.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) y r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_2.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) r y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_2.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
· exact .inl <| .inl <| .inr ⟨y, hy, x, mem_univ _, rfl⟩

Goal state after:
case refine_2.inl.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) y r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

case refine_2.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) r y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

case refine_2.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝ : Field K
a : K
h : a = 0
⊢ IsUnit 1

Tactic:
exact isUnit_one

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : TwoSidedIdeal R
x✝ : R
⊢ x✝ ∈ asIdeal I.jacobson ↔ x✝ ∈ (asIdeal I).jacobson

Tactic:
simp [jacobson]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: case left
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
h : 1 ∈ maximalIdeal R
⊢ IsUnit 1

Tactic:
exact isUnit_one

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Quiver.IsThin C
I A : C
f : A ⟶ I
hI : IsInitial I
⊢ IsIso f

Tactic:
isIso_iff_of_thin

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Quiver.IsThin C
I A : C
f : A ⟶ I
hI : IsInitial I
⊢ Nonempty (I ⟶ A)
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ c, c • x✝¹ = c • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝

Tactic:
simp_rw [Subtype.exists, Algebra.algebraMapSubmonoid]

Goal state after:
case refine_3
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ a, ∃ (b : a ∈ S), ⟨a, b⟩ • x✝¹ = ⟨a, b⟩ • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ a, ∃ (_ : a ∈ Submonoid.map (algebraMap R A) S), a * x✝¹ = a * x✝
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| μ ⊗ₘ tensorμ N P N P ≫ (μ ⊗ₘ μ)

pp: case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| (α_ M N P).hom ⊗ₘ (α_ M N P).hom

pp: case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| tensorμ M (N ⊗ P) M (N ⊗ P)

Tactic:
rw [← Category.id_comp μ, ← tensorHom_comp_tensorHom]

Goal state after:
case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| (𝟙 (M ⊗ M) ⊗ₘ tensorμ N P N P) ≫ (μ ⊗ₘ μ ⊗ₘ μ)

case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| (α_ M N P).hom ⊗ₘ (α_ M N P).hom

case a.a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| tensorμ M (N ⊗ P) M (N ⊗ P)
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: case h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → Mₛ
hf : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
h✝ : Nonempty ι
inj : Function.Injective fun r ↦ r • v (Classical.arbitrary ι)
sec : Mₛ → M × ↥S
hsec : ∀ (y : Mₛ), (sec y).2 • y = f (sec y).1
t : Finset ι
g g' : ι → R
eq : ∑ i ∈ t, g i • (sec (v i)).1 = ∑ i ∈ t, g' i • (sec (v i)).1
i : ι
hit : i ∈ t
⊢ ∑ i ∈ t, (g i * ↑(sec (v i)).2) • v i = ∑ i ∈ t, (g' i * ↑(sec (v i)).2) • v i

Tactic:
simp_rw [mul_smul, ← Submonoid.smul_def, hsec, ← map_smul, ← map_sum, eq]

Goal state after:
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
⊢ ⇑(OreLocalization.oreEqv S M) = r S M

Tactic:
by
  ext a b
  constructor
  · rintro ⟨u, v, h₁, h₂⟩
    use u
    simp only [Submonoid.smul_def, smul_smul, h₂]
    rw [mul_comm, mul_smul, ← h₁, mul_comm, mul_smul, Submonoid.smul_def]
  · rintro ⟨u, hu⟩
    use u * a.2, u * b.2
    rw [mul_smul, ← hu, mul_smul, Submonoid.coe_mul, mul_assoc, mul_assoc, mul_comm (a.2 : R)]
    simp [Submonoid.smul_def]

Goal state after:
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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : u₁ • (b₁, t₁).2 • (a₁, s₁).1 = u₁ • (a₁, s₁).2 • (b₁, t₁).1
u₂ : ↥S
e₂ : u₂ • (b₂, t₂).2 • (a₂, s₂).1 = u₂ • (a₂, s₂).2 • (b₂, t₂).1
⊢ mk (a₁ * a₂) (s₁ * s₂) = mk (b₁ * b₂) (t₁ * t₂)

Tactic:
mk_eq

Goal state after:
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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : u₁ • (b₁, t₁).2 • (a₁, s₁).1 = u₁ • (a₁, s₁).2 • (b₁, t₁).1
u₂ : ↥S
e₂ : u₂ • (b₂, t₂).2 • (a₂, s₂).1 = u₂ • (a₂, s₂).2 • (b₂, t₂).1
⊢ ∃ u, u • (t₁ * t₂) • (a₁ * a₂) = u • (s₁ * s₂) • (b₁ * b₂)
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
r : R
m : M
s s' : ↥S
⊢ mk ((IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m)
      ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') =
    mk (r • m) (s * s')

Tactic:
mk_eq

Goal state after:
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
r : R
m : M
s s' : ↥S
⊢ ∃ u,
    u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
      u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Quiver.IsThin C
P X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
⊢ Nonempty (IsColimit (BinaryCofan.mk inl inr))

Tactic:
exact ⟨BinaryCofan.IsColimit.mk _ (fun u v ↦ h.desc u v (by subsingleton))
      (by subsingleton) (by subsingleton) (by subsingleton)⟩

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

Goal state before:
pp: case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ u, u • t • r • m = u • s • n) ↔ mk m s = mk n (⟨r, hr⟩ * t)

Tactic:
mk_eq

Goal state after:
case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ u, u • t • r • m = u • s • n) ↔ ∃ u, u • (⟨r, hr⟩ * t) • m = u • s • n
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
⊢ Function.Injective ⇑f ↔ ∀ (c : ↥S), IsSMulRegular M c

Tactic:
by
  simp_rw [IsSMulRegular, Function.Injective, eq_iff_exists S, exists_imp, forall_comm (α := S)]

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
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x₁✝ x₂✝ : M''
h : f (e x₁✝) = f (e x₂✝)
⊢ ∃ c, c • x₁✝ = c • x₂✝

Tactic:
obtain ⟨c, hc⟩ := hf.exists_of_eq h

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x₁✝ x₂✝ : M''
h : f (e x₁✝) = f (e x₂✝)
c : ↥S
hc : c • e x₁✝ = c • e x₂✝
⊢ ∃ c, c • x₁✝ = c • x₂✝
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
M : Type u_2
inst✝¹⁰ : AddCommMonoid M
A : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Module R M
S : Submonoid R
N : Type u_6
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Module A M
inst✝³ : Module A N
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R A N
f : M →ₗ[A] N
inst✝ : IsLocalizedModule S (↑R f)
y : N
x : M
t : ↥S
e : (x, t).2 • y = (↑R f) (x, t).1
⊢ (x, ⟨(algebraMap R A) ↑t, ⋯⟩).2 • y = f (x, ⟨(algebraMap R A) ↑t, ⋯⟩).1

Tactic:
simpa [Submonoid.smul_def] using e

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
s : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m 1) = f m

Tactic:
← mk'_one S f,

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
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m 1) = mk' f m 1
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
j : J
⊢ (L.mapCocone ((fst L R).mapCocone c)).ι.app j ≫ L.map (h₁.desc ((fst L R).mapCocone s)) ≫ s.pt.hom =
    (L.mapCocone ((fst L R).mapCocone c)).ι.app j ≫ c.pt.hom ≫ R.map (h₂.desc ((snd L R).mapCocone s))

Tactic:
by
        simp [← Functor.map_comp_assoc, ← Functor.map_comp,
          dsimp% h₁.fac ((fst _ _).mapCocone s) j,
          dsimp% h₂.fac ((snd _ _).mapCocone s) j]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n✝ : ℕ
hI : I.FG
n : ℕ
ih : (I ^ n).FG
⊢ (I ^ n.succ).FG

Tactic:
IsTwoSided.pow_succ

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n✝ : ℕ
hI : I.FG
n : ℕ
ih : (I ^ n).FG
⊢ (I * I ^ n).FG
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ F j₁ = F j₀ ↔ F j₂ = F j₀

Tactic:
simp [a f]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ (ιOfLE h).IsEquivalence ↔ Q ≤ P.isoClosure

Tactic:
rw [← essSurj_ιOfLE_iff h]
  exact ⟨fun _ ↦ inferInstance, fun _ ↦ { }⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : LocallySmall.{w', v_1, u_1} C
⊢ (∃ J x, Nonempty (C ≌ J)) ↔ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤

Tactic:
rw [← ObjectProperty.exists_equivalence_iff]
  exact ⟨fun ⟨J, _, ⟨e⟩⟩ ↦ ⟨J, _, ⟨(ObjectProperty.topEquivalence C).trans e⟩⟩,
    fun ⟨J, _, ⟨e⟩⟩ ↦ ⟨J, _, ⟨(ObjectProperty.topEquivalence C).symm.trans e⟩⟩⟩

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

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q W : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
A B : P.Arrow Q W
f g : A ⟶ B
hl : f.left = g.left
hr : f.right = g.right
⊢ f = g

Tactic:
by
  ext
  · exact hl
  · exact hr

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type (max w v)
X✝ Y✝ : CostructuredArrow uliftYoneda.{w, v, u} F
f : X✝ ⟶ Y✝
⊢ uliftYonedaEquiv (uliftYoneda.{w, v, u}.map f.left.op.unop ≫ Y✝.hom) =
    uliftYonedaEquiv (uliftYoneda.{w, v, u}.map f.left ≫ Y✝.hom)

Tactic:
Quiver.Hom.unop_op

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type (max w v)
X✝ Y✝ : CostructuredArrow uliftYoneda.{w, v, u} F
f : X✝ ⟶ Y✝
⊢ uliftYonedaEquiv (uliftYoneda.{w, v, u}.map f.left ≫ Y✝.hom) =
    uliftYonedaEquiv (uliftYoneda.{w, v, u}.map f.left ≫ Y✝.hom)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ c.op.unop.π ≫ (Iso.refl c.op.unop.pt).hom = c.π

Tactic:
by simp [op_unop_π]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt
hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j
⊢ m ≫ (IsPullback.cone small_k).fst = small_k.lift s.fst s.snd ⋯ ≫ (IsPullback.cone small_k).fst

Tactic:
exact (hm WalkingCospan.left).trans (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝² : HasPullback f₁ f₂
inst✝¹ : HasPullback f₃ f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ IsLimit
    (PullbackCone.mk
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)) ⋯)

Tactic:
apply topSquareIsPullback _ rfl (pullbackIsPullback f₁ f₂)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝² : HasPullback f₁ f₂
inst✝¹ : HasPullback f₃ f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ IsLimit
    ((PullbackCone.mk (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ⋯).pasteVert
      (PullbackCone.mk
        (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
          (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)) ⋯)
      ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inr g₁ g₂ ≫
      pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯ =
    pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)

Tactic:
· exact pushout.inr_desc _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inr g₃ g₄ ≫
      pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯ =
    pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄

Tactic:
· exact pushout.inr_desc _ _ _

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ pullback (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≅ pullback f g

Tactic:
refine @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (pullback.fst _ _) ?_ ?_) ?_

Goal state after:
case refine_2.refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S) = 𝟙 X ≫ f

case refine_2.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S) = 𝟙 Y ≫ g

case refine_2.refine_3
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ IsIso
    (map (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) f g (𝟙 X) (𝟙 Y) (fst i (𝟙 S)) ?refine_2.refine_1
      ?refine_2.refine_2)