mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod' G) X Y).2 = μ G X Y

Tactic:
change _ ≫ G.map (𝟙 _) = _

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 ≫ G.map (𝟙 ((diag C).obj X ⊗ (diag C).obj Y).2) = μ G X Y
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (adj.homEquiv (X✝ ⊗ x✝) (F.obj Y✝ ⊗ F.obj x✝)).symm
      ((adj.unit.app X✝ ⊗ₘ adj.unit.app x✝) ≫ G.map (F.map x✝¹) ▷ G.obj (F.obj x✝) ≫ μ G (F.obj Y✝) (F.obj x✝)) =
    (adj.homEquiv (X✝ ⊗ x✝) (F.obj Y✝ ⊗ F.obj x✝)).symm
      (x✝¹ ▷ x✝ ≫ (adj.unit.app Y✝ ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj Y✝) (F.obj x✝))

Tactic:
simp [← tensorHom_id]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
⊢ (Hom.hom f).range ≤ (Hom.hom (cokernel.π f)).ker

Tactic:
rintro _ ⟨x, rfl⟩
      exact cokernel.condition_apply f x

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (TensorAlgebra R M)) r
this : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
⊢ x = 0 ∧ r = 0

Tactic:
have : IsCentralScalar R M := ⟨fun r m => rfl⟩

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (TensorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R M
⊢ x = 0 ∧ r = 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2.inr.inr
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha : a.fst ≠ 0
hb : b.fst ≠ 0
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))

Tactic:
mul_inv_cancel_left₀ hb

Goal state after:
case h2.inr.inr
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha : a.fst ≠ 0
hb : b.fst ≠ 0
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
f g : A →ₗc[R] R
x : A
⊢ f x = g x

Tactic:
by
    have hf := CoalgHomClass.counit_comp_apply f x
    have hg := CoalgHomClass.counit_comp_apply g x
    simp_all only [CommSemiring.counit_apply]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : WfDvdMonoid α
a : α
ha : ¬IsUnit a
n : ℕ
c : α
ndvd : ¬a ∣ c
hb : a ^ n * c ≠ 0
⊢ FiniteMultiplicity a (a ^ n * c)

Tactic:
exact ⟨n, by rwa [pow_succ, mul_dvd_mul_iff_left (left_ne_zero_of_mul hb)]⟩

Goal state after:
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:
← (prod_normalizedFactors hb).dvd_iff_dvd_right,

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) ∣ (normalizedFactors b).prod
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ ⊥.jacobson = Ring.jacobson R

Tactic:
by
  simp_rw [jacobson, Ring.jacobson, Module.jacobson, bot_le, true_and, isMaximal_def]

Goal state after:
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 : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ M N M N ▷ (M ⊗ N) ≫ tensorμ (M ⊗ M) (N ⊗ N) M N ≫ ((α_ M M M).hom ⊗ₘ (α_ N N N).hom)

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

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

Tactic:
rw [tensor_associativity]

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

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| M ◁ μ ⊗ₘ N ◁ μ

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| μ ⊗ₘ μ
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc : IsColimit (PushoutCocone.mk (c.ι.app { as := WalkingPair.left }) (c.ι.app { as := WalkingPair.right }) ⋯)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
⊢ c.ι.app { as := WalkingPair.left } ≫ m =
    c.ι.app { as := WalkingPair.left } ≫
      hc.desc (PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)

pp: case some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc : IsColimit (PushoutCocone.mk (c.ι.app { as := WalkingPair.left }) (c.ι.app { as := WalkingPair.right }) ⋯)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
⊢ c.ι.app { as := WalkingPair.left } ≫ m =
    c.ι.app { as := WalkingPair.left } ≫
      hc.desc (PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)

pp: case some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc : IsColimit (PushoutCocone.mk (c.ι.app { as := WalkingPair.left }) (c.ι.app { as := WalkingPair.right }) ⋯)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
⊢ c.ι.app { as := WalkingPair.right } ≫ m =
    c.ι.app { as := WalkingPair.right } ≫
      hc.desc (PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)

Tactic:
exacts [(hc.fac c' WalkingSpan.left).symm, (hc.fac c' WalkingSpan.left).symm,
      (hc.fac c' WalkingSpan.right).symm]

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁷ : CommSemiring A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : IsLocalization S A
M : Type u_3
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
M' : Type u_4
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : Module A M'
inst✝⁹ : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
α : Type u_7
inst✝ : IsLocalizedModule S f
⊢ IsLocalizedModule S (Finsupp.mapRange.linearMap f)

Tactic:
let e : Localization S ⊗[R] M ≃ₗ[R] M' :=
    (LocalizedModule.equivTensorProduct S M).symm.restrictScalars R ≪≫ₗ IsLocalizedModule.iso S f

Goal state after:
R : Type u_1
inst✝¹⁸ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁷ : CommSemiring A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : IsLocalization S A
M : Type u_3
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
M' : Type u_4
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : Module A M'
inst✝⁹ : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
α : Type u_7
inst✝ : IsLocalizedModule S f
e : Localization S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LocalizedModule.equivTensorProduct S M).symm ≪≫ₗ IsLocalizedModule.iso S f
⊢ IsLocalizedModule S (Finsupp.mapRange.linearMap f)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : Epi g
⊢ Epi inl

Tactic:
constructor
  intro W fst' snd' heq
  exact h.hom_ext heq (by simp [← cancel_epi g, ← h.w_assoc, heq])

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

Goal state before:
pp: case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ u • b.2 • a.1 = ↑u • ↑b.2 • a.1 ∧ ↑u * (↑a.2 * ↑b.2) = ↑u * (↑b.2 * ↑a.2)

Tactic:
mul_comm (a.2 : R)

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ u • b.2 • a.1 = ↑u • ↑b.2 • a.1 ∧ ↑u * (↑b.2 * ↑a.2) = ↑u * (↑b.2 * ↑a.2)
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 : IsPushout f f' g g
⊢ ∀ (s : Cofork f f') (m : (Cofork.ofπ g ⋯).pt ⟶ s.pt),
    (Cofork.ofπ g ⋯).π ≫ m = s.π → m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
intro s m e
    apply PushoutCocone.IsColimit.hom_ext H.isColimit <;> refine e.trans ?_ <;> symm <;>
      exact H.isColimit.fac _ _

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_3
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
z : α
hzs : z ∈ s
n✝ : FreeCommRing α
a✝ : ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) n✝ = ↑n
⊢ ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) (of z * n✝) = ↑n

Tactic:
use 0

Goal state after:
case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
z : α
hzs : z ∈ s
n✝ : FreeCommRing α
a✝ : ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) n✝ = ↑n
⊢ (lift fun a ↦ if a ∈ s then 0 else X) (of z * n✝) = ↑0
Module: Mathlib.CategoryTheory.Adjunction.Limits

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
K : J ⥤ C
E : C ⥤ D
inst✝¹ : E.IsEquivalence
inst✝ : HasColimit (K ⋙ E)
⊢ HasColimit (K ⋙ E.asEquivalence.functor ⋙ E.asEquivalence.inverse)

Tactic:
exact hasColimit_comp_equivalence (K ⋙ E) E.inv

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case property.right.right
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
h : (pushoutCocone R A B).pt ⟶ s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
⊢ ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ h = s.inr →
    h = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom

Tactic:
eq2

Goal state after:
case property.right.right
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
h : (pushoutCocone R A B).pt ⟶ s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ h = s.inr
⊢ h = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: case h₁
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
x : Over X
y : Over Y
v : x ⟶ (pullback f).obj y
⊢ pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯ ≫ pullback.snd y.hom f = Hom.left v ≫ pullback.snd y.hom f

Tactic:
· simpa using (Over.w v).symm

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
R₀ : Type u_6
inst✝⁵ : SMul R₀ R
inst✝⁴ : SMul R₀ M
inst✝³ : SMul R₀ M'
inst✝² : IsScalarTower R₀ R R
inst✝¹ : IsScalarTower R₀ R M
inst✝ : IsScalarTower R₀ R M'
r : R₀
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (r • LocalizedModule.mk m s) = r • (fromLocalizedModule S f) (LocalizedModule.mk m s)

Tactic:
LinearMap.map_smul_of_tower

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
R₀ : Type u_6
inst✝⁵ : SMul R₀ R
inst✝⁴ : SMul R₀ M
inst✝³ : SMul R₀ M'
inst✝² : IsScalarTower R₀ R R
inst✝¹ : IsScalarTower R₀ R M
inst✝ : IsScalarTower R₀ R M'
r : R₀
m : M
s : ↥S
⊢ r • (fromLocalizedModule S f) (LocalizedModule.mk m s) = r • (fromLocalizedModule S f) (LocalizedModule.mk m s)
Module: Mathlib.CategoryTheory.Adjunction.Comma

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B₁ B₂ : D
A : C
f : B₁ ⟶ B₂
g : G.obj B₂ ⟶ A
⊢ (rightAdjointOfCostructuredArrowTerminalsAux G B₁ A) (G.map f ≫ g) =
    f ≫ (rightAdjointOfCostructuredArrowTerminalsAux G B₂ A) g

Tactic:
← Equiv.eq_symm_apply

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B₁ B₂ : D
A : C
f : B₁ ⟶ B₂
g : G.obj B₂ ⟶ A
⊢ G.map f ≫ g =
    (rightAdjointOfCostructuredArrowTerminalsAux G B₁ A).symm
      (f ≫ (rightAdjointOfCostructuredArrowTerminalsAux G B₂ A) g)
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_inj : Function.Injective ⇑h
⊢ Function.Injective ⇑((map S f g) h)

Tactic:
by
  intro x y
  obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f x
  obtain ⟨⟨y, t⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f y
  simp only [Function.uncurry_apply_pair, map_mk', mk'_eq_mk'_iff, Subtype.exists,
    Submonoid.mk_smul, exists_prop, forall_exists_index, and_imp]
  intro c hc e
  exact ⟨c, hc, h_inj (by simpa)⟩

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ⟶ g
inst✝ : IsIso η
⊢ F.map₂ (inv η) = inv (F.map₂ η)

Tactic:
by
  apply IsIso.eq_inv_of_hom_inv_id
  simp [← F.map₂_comp η (inv η)]

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P Q : ObjectProperty C
h : P.op = Q.op
⊢ P = Q

Tactic:
rw [← P.unop_op, ← Q.unop_op, h]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
h : Function.Injective ⇑(algebraMap A B)
⊢ (algebraMap A B) ((aeval x) p) = (algebraMap A B) 0 ↔ (aeval x) p = 0

Tactic:
h.eq_iff

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
h : Function.Injective ⇑(algebraMap A B)
⊢ (aeval x) p = 0 ↔ (aeval x) p = 0
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
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P
right✝ : P ≤ Q.isoClosure
⊢ P.isoClosure ≤ Q.isoClosure

Tactic:
isoClosure_le_iff

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P
right✝ : P ≤ Q.isoClosure
⊢ P ≤ Q.isoClosure
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
⊢ Q.isoClosure ≤ P

Tactic:
isoClosure_le_iff

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
⊢ Q ≤ P
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case h₂
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
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right

Tactic:
exact hr

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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ colimMap
        (whiskerRight (Grothendieck.ιNatTrans (f ≫ g)) G ≫
          ((F.map (f ≫ g)).toFunctor.associator (Grothendieck.ι F Z) G).hom) ≫
      colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map (f ≫ g)).toFunctor =
    (colimMap
          (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F Y) G).hom) ≫
        colimit.pre (Grothendieck.ι F Y ⋙ G) (F.map f).toFunctor) ≫
      colimMap
          (whiskerRight (Grothendieck.ιNatTrans g) G ≫ ((F.map g).toFunctor.associator (Grothendieck.ι F Z) G).hom) ≫
        colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map g).toFunctor

Tactic:
ext d
    simp only [Functor.comp_obj, Grothendieck.ιNatTrans, ι_colimMap_assoc, NatTrans.comp_app,
      whiskerRight_app, Functor.associator_hom_app, Category.comp_id, colimit.ι_pre, Category.assoc,
      colimit.ι_pre_assoc]
    rw [← Category.assoc, ← G.map_comp]
    conv_rhs => rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F Z ⋙ G)
      (j := (F.map (f ≫ g)).toFunctor.obj d) (by simp)]
    rw [← Category.assoc, ← eqToHom_map G (by simp), ← G.map_comp, Grothendieck.eqToHom_eq]
    congr 2
    fapply Grothendieck.ext
    · simp only [eqToHom_refl, Category.assoc, Grothendieck.comp_base,
        Category.comp_id]
    · simp only [Grothendieck.ι_obj, eqToHom_refl,
        Grothendieck.comp_base, Category.comp_id, Grothendieck.comp_fiber, Functor.map_id]
      conv_rhs => enter [2, 1]; rw [eqToHom_map (F.map (𝟙 Z)).toFunctor]
      conv_rhs => rw [eqToHom_trans, eqToHom_trans]

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ comp f Y.id = f

Tactic:
by
    ext
    · simp [comp, id]
    · dsimp [comp, id]
      rw [← NatIso.naturality_2 ((Cat.Hom.toNatIso <| eqToIso (F.map_id Y.base)) ≪≫
        (eqToIso Cat.Hom.id_toFunctor)) f.fiber]
      simp

Goal state after: