mathlib-initiative/mathlib-tactics huggingface dataset:
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'
a : M
b : ↥S
eq1 : b • m = f a
⊢ f (b • ⋯.choose.1) = f (⋯.choose.2 • a)

Tactic:
Submonoid.smul_def,

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'
a : M
b : ↥S
eq1 : b • m = f a
⊢ f (↑b • ⋯.choose.1) = f (⋯.choose.2 • 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
m : M'
a : M
b : ↥S
eq1 : b • m = f a
⊢ f (↑b • ⋯.choose.1) = f (⋯.choose.2 • a)

Tactic:
Submonoid.smul_def,

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'
a : M
b : ↥S
eq1 : b • m = f a
⊢ f (↑b • ⋯.choose.1) = f (↑⋯.choose.2 • a)
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryProducts C
X Y : C
⊢ (forgetAdjStar X).counit.app Y = prod.snd

Tactic:
by
  simp [Over.forgetAdjStar, CategoryTheory.coalgebraEquivOver]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryProducts C
X : C
Y : Over X
⊢ Hom.left ((forgetAdjStar X).unit.app Y) = prod.lift Y.hom (𝟙 Y.left)

Tactic:
by
  simp [Over.forgetAdjStar, CategoryTheory.coalgebraEquivOver]

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
⊢ s • mk' f m s = f m

Tactic:
Submonoid.smul_def,

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
⊢ ↑s • mk' f m s = 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₂ : M
s₁ s₂ : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m₁ s₁) = (fromLocalizedModule S f) (LocalizedModule.mk m₂ s₂) ↔
    ∃ s, s • s₁ • m₂ = s • s₂ • m₁

Tactic:
rw [(fromLocalizedModule.inj S f).eq_iff, LocalizedModule.mk_eq]

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₂ : M
s₁ s₂ : ↥S
⊢ (∃ u, u • s₂ • m₁ = u • s₁ • m₂) ↔ ∃ s, s • s₁ • m₂ = s • s₂ • m₁
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : NonUnitalNonAssocSemiring M
inst✝³ : Semiring M'
inst✝² : Module R M
inst✝¹ : Algebra R M'
f : M →ₗ[R] M'
hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ f (m₁ * m₂, s₁ * s₂).1 = ↑(m₁ * m₂, s₁ * s₂).2 • (mk' f m₁ s₁ * mk' f m₂ s₂)

Tactic:
simp_rw [Submonoid.coe_mul, ← smul_eq_mul]

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : NonUnitalNonAssocSemiring M
inst✝³ : Semiring M'
inst✝² : Module R M
inst✝¹ : Algebra R M'
f : M →ₗ[R] M'
hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ f (m₁ • m₂) = (↑s₁ • ↑s₂) • mk' f m₁ s₁ • mk' f m₂ s₂
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
m' : M'
⊢ s • mk' f m s = s • m' ↔ f m = s • m'

Tactic:
Submonoid.smul_def,

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
m' : M'
⊢ ↑s • mk' f m s = s • m' ↔ f m = s • 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
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
m : M
⊢ (LocalizedModule.mkLinearMap S M) m = s • LocalizedModule.mk m s

Tactic:
Submonoid.smul_def,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
m : M
⊢ (LocalizedModule.mkLinearMap S M) m = ↑s • LocalizedModule.mk m s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case map_units.left
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
a b : S'
e : x • a = x • b
⊢ a = b

Tactic:
Submonoid.smul_def,

Goal state after:
case map_units.left
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
a b : S'
e : ↑x • a = ↑x • b
⊢ a = b
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : (fun x ↦ c • x) x = (fun x ↦ c • x) y
⊢ x = y

Tactic:
by_cases hS₀ : 0 ∈ S

Goal state after:
case pos
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : (fun x ↦ c • x) x = (fun x ↦ c • x) y
hS₀ : 0 ∈ S
⊢ x = y

case neg
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : (fun x ↦ c • x) x = (fun x ↦ c • x) y
hS₀ : 0 ∉ S
⊢ x = y
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (F.comp G.toPrelaxFunctor).map₂ (λ_ f).hom =
    ((G.mapFunctor (F.obj a✝) (F.obj b✝)).map (F.mapComp (𝟙 a✝) f) ≫ G.mapComp (F.map (𝟙 a✝)) (F.map f)) ≫
      ((G.mapFunctor (F.obj a✝) (F.obj a✝)).map (F.mapId a✝) ≫ G.mapId (F.obj a✝)) ▷ (F.comp G.toPrelaxFunctor).map f ≫
        (λ_ ((F.comp G.toPrelaxFunctor).map f)).hom

Tactic:
by
    dsimp
    simp only [map₂_leftUnitor, PrelaxFunctor.map₂_comp, mapComp_naturality_left_assoc,
      comp_whiskerRight, assoc]

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h =
    (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h) ≫ F.map₂ (α_ f g h).inv

Tactic:
by
  rw [← F.map₂_associator_assoc, ← F.map₂_comp]
  simp only [Iso.hom_inv_id, PrelaxFunctor.map₂_id, comp_id]

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

Goal state before:
pp: case h.inr
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : i < n
⊢ J ^ i * K ^ (n + m - i) ≤ I

Tactic:
· exact mul_le_right.trans ((pow_le_pow_right (by lia)).trans hm)

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: case h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
p : Set (ULiftHom (ULift.{u₂, u₁} J))
hj₀ : ?j₀ ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
p' : Set J := {j | { down := j } ∈ p}
⊢ { down := j } ∈ p

Tactic:
have hj₀' : Classical.choice hc.is_nonempty ∈ p' := by
      simp only [p']
      exact hj₀

Goal state after:
case h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
p : Set (ULiftHom (ULift.{u₂, u₁} J))
hj₀ : { down := Classical.choice ⋯ } ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
p' : Set J := {j | { down := j } ∈ p}
hj₀' : Classical.choice ⋯ ∈ p'
⊢ { down := j } ∈ p
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case mpr
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG) → FinitePresentation R A

Tactic:
rintro ⟨ι, hfintype, f, hf⟩
    have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
    use Fintype.card ι, f.comp equiv.symm, hf.1.comp (AlgEquiv.symm equiv).surjective
    refine Ideal.fg_ker_comp (S := MvPolynomial ι R) (A := A) _ f ?_ hf.2 equiv.symm.surjective
    simpa using! Submodule.fg_bot

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : C ⥤ Cat
α : F ⟶ G
X✝ Y✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X✝ ⟶ Y✝
⊢ ((map (whiskerRight α Cat.asSmallFunctor)).map f ≫
        (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj Y✝)).hom).base =
    ((Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X✝)).hom ≫
        ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse).map f).base

pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : C ⥤ Cat
α : F ⟶ G
X✝ Y✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X✝ ⟶ Y✝
⊢ eqToHom ⋯ ≫
      ((map (whiskerRight α Cat.asSmallFunctor)).map f ≫
          (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj Y✝)).hom).fiber =
    ((Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X✝)).hom ≫
        ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse).map f).fiber

Tactic:
· simp [compAsSmallFunctorEquivalenceInverse]

Goal state after:
case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : C ⥤ Cat
α : F ⟶ G
X✝ Y✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X✝ ⟶ Y✝
⊢ eqToHom ⋯ ≫
      ((map (whiskerRight α Cat.asSmallFunctor)).map f ≫
          (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj Y✝)).hom).fiber =
    ((Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X✝)).hom ≫
        ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse).map f).fiber
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
T : C ⥤ D
inst✝ : T.Initial
S : D ⥤ E
X : E
⊢ (pre T S X).Initial

Tactic:
refine ⟨fun f => ?_⟩
  rw [isConnected_iff_of_equivalence (CostructuredArrow.preEquivalence T f)]
  exact Initial.out f.left

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₁₂ : S ⟶ X
v₂₂ : S ⟶ Y
g : Y ⟶ X
hv₁₂ : v₁₂ = v₂₂ ≫ g
inst✝¹ : HasPushout v₁₂ f
inst✝ : HasPushout v₂₂ f
H : P g
⊢ v₂₂ ≫ g ≫ pushout.inl v₁₂ f = f ≫ pushout.inr v₁₂ f

Tactic:
by simp [pushout.condition, ← reassoc_of% hv₁₂]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
Q : ObjectProperty C
h : P ≤ Q
⊢ P.strictLimitsOfShape J ≤ Q.strictLimitsOfShape J

Tactic:
by
  rintro _ ⟨F, hF⟩
  exact ⟨F, fun j ↦ h _ (hF j)⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
X Y : C
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e : { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ (Functor.const J).map e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ (Functor.const J).map e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
j : J
⊢ c₁'.ι.app j ≫ h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } = c₁'.ι.app j ≫ g

Tactic:
h₁'.fac

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
X Y : C
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e : { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ (Functor.const J).map e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ (Functor.const J).map e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
j : J
⊢ { pt := c₂'.pt, ι := f ≫ c₂'.ι }.ι.app j = c₁'.ι.app j ≫ g
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
Q : ObjectProperty C
h : P ≤ Q
⊢ P.strictColimitsOfShape J ≤ Q.strictColimitsOfShape J

Tactic:
by
  rintro _ ⟨F, hF⟩
  exact ⟨F, fun j ↦ h _ (hF j)⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
⊢ ∀ (a b : SymmetricCategory C), a = b

Tactic:
rintro ⟨_⟩ ⟨_⟩; congr; exact Subsingleton.elim _ _

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
X Y Z : C
inst✝ : F.OplaxMonoidal
f : X ⟶ Y
g : X ⟶ Z
⊢ (F.map (lift f g) ≫ δ F Y Z) ≫ fst (F.obj Y) (F.obj Z) = lift (F.map f) (F.map g) ≫ fst (F.obj Y) (F.obj Z)

Tactic:
simp [← map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_snd
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
X Y Z : C
inst✝ : F.OplaxMonoidal
f : X ⟶ Y
g : X ⟶ Z
⊢ (F.map (lift f g) ≫ δ F Y Z) ≫ snd (F.obj Y) (F.obj Z) = lift (F.map f) (F.map g) ≫ snd (F.obj Y) (F.obj Z)

Tactic:
simp [← map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ f = lift g (h ≫ ι) ≫ μ ↔ lift f h ≫ μ = g

Tactic:
refine ⟨?_, ?_⟩ <;> (rintro rfl; simp [lift_lift_assoc])

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ ∀ x ∈ Set.range (WType.elim (↥(closure s)) (operate s)), x⁻¹ ∈ Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
rintro _ ⟨x, rfl⟩; exact ⟨WType.mk (.inl 3) fun _ ↦ x, rfl⟩

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
p : Submodule K V
v x : V
a : K
hx : a • v ∈ p
hx' : a • v = x
hv : ¬a = 0
⊢ v ∈ p

Tactic:
simpa [smul_mem_iff p hv] using hx

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ 𝟙 (𝟙_ C ⊗ X) ⊗≫ (i.hom ≫ i.inv) ⊗≫ 𝟙 (X ⊗ 𝟙_ C) = (λ_ X).hom ≫ (ρ_ X).inv

Tactic:
Iso.hom_inv_id

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ 𝟙 (𝟙_ C ⊗ X) ⊗≫ 𝟙 X ⊗≫ 𝟙 (X ⊗ 𝟙_ C) = (λ_ X).hom ≫ (ρ_ X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' : C
inst✝ : ExactPairing X Y'
i : Y ≅ Y'
⊢ 𝟙 (Y ⊗ 𝟙_ C) ⊗≫ (i.hom ≫ i.inv) ⊗≫ 𝟙 (𝟙_ C ⊗ Y) = (ρ_ Y).hom ≫ (λ_ Y).inv

Tactic:
Iso.hom_inv_id

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' : C
inst✝ : ExactPairing X Y'
i : Y ≅ Y'
⊢ 𝟙 (Y ⊗ 𝟙_ C) ⊗≫ 𝟙 Y ⊗≫ 𝟙 (𝟙_ C ⊗ Y) = (ρ_ Y).hom ≫ (λ_ Y).inv
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
this : (B (∑ i ∈ s, w i • v i)) (v i) = 0
hsum : ∑ j ∈ s, I₁ (w j) • (B (v j)) (v i) = I₁ (w i) • (B (v i)) (v i)
⊢ w i = 0

Tactic:
simp_rw [B.map_sum₂, map_smulₛₗ₂, hsum] at this

Goal state after:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
hsum : ∑ j ∈ s, I₁ (w j) • (B (v j)) (v i) = I₁ (w i) • (B (v i)) (v i)
this : I₁ (w i) • (B (v i)) (v i) = 0
⊢ w i = 0
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : 1 ∈ (dualTensorHom R M M).range
⊢ Module.Finite R M ∧ Projective R M

Tactic:
have ⟨t, eq⟩ := h

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : 1 ∈ (dualTensorHom R M M).range
t : Dual R M ⊗[R] M
eq : (dualTensorHom R M M) t = 1
⊢ Module.Finite R M ∧ Projective R M
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingRight
i : n
⊢ (B (v i)) (v i) ≠ 0

Tactic:
isOrthoᵢ_flip

Goal state after:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.flip.IsOrthoᵢ ⇑v
hB : B.SeparatingRight
i : n
⊢ (B (v i)) (v i) ≠ 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝² : HasEqualizer f g
inst✝¹ : HasEqualizer (G.map f) (G.map g)
inst✝ : PreservesLimit (parallelPair f g) G
⊢ ((iso G f g).hom ≫ (iso G f g).inv) ≫ G.map (equalizer.ι f g) = (iso G f g).hom ≫ equalizer.ι (G.map f) (G.map g)

Tactic:
Iso.hom_inv_id

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝² : HasEqualizer f g
inst✝¹ : HasEqualizer (G.map f) (G.map g)
inst✝ : PreservesLimit (parallelPair f g) G
⊢ 𝟙 (G.obj (equalizer f g)) ≫ G.map (equalizer.ι f g) = (iso G f g).hom ≫ equalizer.ι (G.map f) (G.map g)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
⊢ B.SeparatingRight

Tactic:
isOrthoᵢ_flip

Goal state after:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.flip.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
⊢ B.SeparatingRight