mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ IsPullback fst' snd' f' g'

Tactic:
by
  apply h.of_iso e₁.symm e₂.symm e₃.symm e₄.symm
  · simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commfst, Iso.inv_hom_id_assoc]
  · simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commsnd, Iso.inv_hom_id_assoc]
  · simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commf, Iso.inv_hom_id_assoc]
  · simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commg, Iso.inv_hom_id_assoc]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g' : W ⟶ Y
inst✝¹ : HasPullback f g
inst✝ : HasPullback (pullback.snd f g) g'
⊢ (pullbackLeftPullbackSndIso f g g').inv ≫ pullback.snd (pullback.snd f g) g' ≫ g' = pullback.snd f (g' ≫ g) ≫ g'

Tactic:
exact pullbackLeftPullbackSndIso_inv_snd_snd_assoc f g g' g'

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'
x : T
p : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
⊢ ∀ (p p' : M × ↥S), p ≈ p' → mk (a.1 • p.1) (a.2 * p.2) = mk (a.1 • p'.1) (a.2 * p'.2)

Tactic:
rintro p p' ⟨s, h⟩

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'
x : T
p✝ : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : M × ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ mk (a.1 • p.1) (a.2 * p.2) = mk (a.1 • p'.1) (a.2 * p'.2)
Module: Mathlib.CategoryTheory.Monad.Algebra

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
A B : T.Algebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ f ≫ { f := inv f.f, h := ⋯ } = 𝟙 A ∧ { f := inv f.f, h := ⋯ } ≫ f = 𝟙 B

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : Comonad C
A B : G.Coalgebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ f ≫ { f := inv f.f, h := ⋯ } = 𝟙 A ∧ { f := inv f.f, h := ⋯ } ≫ f = 𝟙 B

Tactic:
by cat_disch

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_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
⊢ ∀ (s s' : ↥S), lift' S g h (mk a s + mk a' s') = lift' S g h (mk a s) + lift' S g h (mk a' s')

Tactic:
b

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b : ↥S
⊢ ∀ (s' : ↥S), lift' S g h (mk a b + mk a' s') = lift' S g h (mk a b) + lift' S g h (mk a' 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_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ lift' S g h (mk a b + mk a' b') = lift' S g h (mk a b) + lift' S g h (mk a' b')

Tactic:
rw [mk_add_mk, LocalizedModule.lift'_mk, LocalizedModule.lift'_mk, LocalizedModule.lift'_mk]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (g (b' • a + b • a')) = ↑⋯.unit⁻¹ (g a) + ↑⋯.unit⁻¹ (g 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 y : LocalizedModule S M
a a' : M
⊢ ∀ (s s' : ↥S),
    fromLocalizedModule' S f (LocalizedModule.mk a s + LocalizedModule.mk a' s') =
      fromLocalizedModule' S f (LocalizedModule.mk a s) + fromLocalizedModule' S f (LocalizedModule.mk a' s')

Tactic:
b

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 y : LocalizedModule S M
a a' : M
b : ↥S
⊢ ∀ (s' : ↥S),
    fromLocalizedModule' S f (LocalizedModule.mk a b + LocalizedModule.mk a' s') =
      fromLocalizedModule' S f (LocalizedModule.mk a b) + fromLocalizedModule' S f (LocalizedModule.mk a' 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
r : R
x : LocalizedModule S M
a : M
⊢ ∀ (s : ↥S),
    r • fromLocalizedModule' S f (LocalizedModule.mk a s) = fromLocalizedModule' S f (r • LocalizedModule.mk a s)

Tactic:
b

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 : R
x : LocalizedModule S M
a : M
b : ↥S
⊢ r • fromLocalizedModule' S f (LocalizedModule.mk a b) = fromLocalizedModule' S f (r • LocalizedModule.mk a b)
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
x : Over X
y : Over Y
⊢ Function.LeftInverse (fun v ↦ homMk (Hom.left v ≫ pullback.fst y.hom f) ⋯) fun u ↦
    homMk (pullback.lift (Hom.left u) x.hom ⋯) ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: 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' : A ⊗[R] B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
this : h' = Algebra.TensorProduct.productMap f' g'
⊢ h = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom

Tactic:
by
      ext x
      change h' x = Algebra.TensorProduct.productMap f' g' x
      rw [this]

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
eq2 : ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ h = s.inr
h' : A ⊗[R] B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
a : A
⊢ ∀ (b : B), h' (a ⊗ₜ[R] b) = (Algebra.TensorProduct.productMap f' g') (a ⊗ₜ[R] b)

Tactic:
b

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' : A ⊗[R] B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
a : A
b : B
⊢ h' (a ⊗ₜ[R] b) = (Algebra.TensorProduct.productMap f' g') (a ⊗ₜ[R] b)
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✝ : HasPushoutsAlong f
x : Under X
y : Under Y
⊢ Function.RightInverse (fun v ↦ homMk (pushout.desc (Hom.right v) y.hom ⋯) ⋯) fun u ↦
    homMk (pushout.inl x.hom f ≫ Hom.right u) ⋯

Tactic:
by cat_disch

Goal state after:
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 : D
A : C
⊢ Function.LeftInverse (fun g ↦ G.map g ≫ (⊤_ CostructuredArrow G A).hom) fun g ↦
    (terminal.from (CostructuredArrow.mk g)).left

Tactic:
by cat_disch

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
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a : M'
⊢ ∀ ⦃a₂ : M'⦄, g a = g a₂ → a = a₂

Tactic:
b

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
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
⊢ g a = g b → a = b
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
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
hab : g a = g b
x : M
m : ↥S
hxm : m • a = f x
y : M
n : ↥S
hym : n • b = f y
h : g (f (↑n • x)) = g (f (↑m • y))
⊢ a = b

Tactic:
apply H at h

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
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
hab : g a = g b
x : M
m : ↥S
hxm : m • a = f x
y : M
n : ↥S
hym : n • b = f y
h : f (↑n • x) = f (↑m • y)
⊢ a = b
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
F : J ⥤ Arrow T
i₁ : HasLimit (F ⋙ leftFunc)
i₂ : HasLimit (F ⋙ rightFunc)
this : HasLimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
⊢ HasLimit F

Tactic:
have : HasLimit (F ⋙ Comma.snd _ _) := i₂

Goal state after:
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
F : J ⥤ Arrow T
i₁ : HasLimit (F ⋙ leftFunc)
i₂ : HasLimit (F ⋙ rightFunc)
this✝ : HasLimit (F ⋙ Comma.fst (𝟭 T) (𝟭 T))
this : HasLimit (F ⋙ Comma.snd (𝟭 T) (𝟭 T))
⊢ HasLimit F
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ ((algebraMap R (End R M₁')) ↑s) (((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m s)) =
    ((algebraMap R (End R M₁')) ↑s)
      ((↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s))

Tactic:
rw [Module.algebraMap_end_apply, Module.algebraMap_end_apply,
    ← CompatibleSMul.map_smul, ← CompatibleSMul.map_smul, smul'_mk, ← mk_smul _ s.2, mk_cancel]

Goal state after:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m 1) =
    (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m 1)
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
F : J ⥤ C
c : Cone F
⊢ Function.LeftInverse (fun h s ↦ { default := h.from s, uniq := ⋯ }) fun x ↦ IsTerminal.ofUnique c

Tactic:
by cat_disch

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
F : J ⥤ C
c : Cone F
⊢ Function.RightInverse (fun h s ↦ { default := h.from s, uniq := ⋯ }) fun x ↦ IsTerminal.ofUnique c

Tactic:
by cat_disch

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
F : J ⥤ C
c : Cocone F
⊢ Function.LeftInverse (fun h s ↦ { default := h.to s, uniq := ⋯ }) fun x ↦ IsInitial.ofUnique c

Tactic:
by cat_disch

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
F : J ⥤ C
c : Cocone F
⊢ Function.RightInverse (fun h s ↦ { default := h.to s, uniq := ⋯ }) fun x ↦ IsInitial.ofUnique c

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : P.op.FullSubcategory
⊢ ((P.lift P.op.ι.leftOp ⋯).rightOp.map ((Iso.refl (𝟭 P.op.FullSubcategory)).hom.app X) ≫
        (Iso.refl (P.op.lift P.ι.op ⋯ ⋙ (P.lift P.op.ι.leftOp ⋯).rightOp)).hom.app
          ((P.lift P.op.ι.leftOp ⋯).rightOp.obj X)).unop =
    (𝟙 ((P.lift P.op.ι.leftOp ⋯).rightOp.obj X)).unop

Tactic:
by cat_disch

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

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
x : R
n : ℕ
hn : x ^ n ∈ J
⊢ (R ∙ x) ^ n ≤ J

Tactic:
by simpa [span_singleton_pow, span_le]

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Over X
F : C ⥤ D
t t₁ t₂ : Cone K
f : t₁ ⟶ t₂
⊢ Over.Hom.left f.hom ≫
      { pt := t₂.pt.left,
              π :=
                {
                  app := fun x ↦
                    match x with
                    | of a => Over.Hom.left (t₂.π.app a)
                    | star => t₂.pt.hom,
                  naturality := ⋯ } }.π.app
        star =
    { pt := t₁.pt.left,
            π :=
              {
                app := fun x ↦
                  match x with
                  | of a => Over.Hom.left (t₁.π.app a)
                  | star => t₁.pt.hom,
                naturality := ⋯ } }.π.app
      star

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Under X
F : C ⥤ D
t t₁ t₂ : Cocone K
f : t₁ ⟶ t₂
⊢ { pt := t₁.pt.right,
              ι :=
                {
                  app := fun x ↦
                    match x with
                    | of a => Under.Hom.right (t₁.ι.app a)
                    | star => t₁.pt.hom,
                  naturality := ⋯ } }.ι.app
        star ≫
      Under.Hom.right f.hom =
    { pt := t₂.pt.right,
            ι :=
              {
                app := fun x ↦
                  match x with
                  | of a => Under.Hom.right (t₂.ι.app a)
                  | star => t₂.pt.hom,
                naturality := ⋯ } }.ι.app
      star

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
α : Type u₂
F : J ⥤ Discrete α
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    (liftToDiscrete F ⋙ Discrete.functor F.obj).map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ F.map f

Tactic:
by cat_disch

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
⊢ ∀ (X : ⊤.FullSubcategory),
    ⊤.ι.map ((Iso.refl (𝟭 ⊤.FullSubcategory)).hom.app X) ≫ (Iso.refl (⊤.lift (𝟭 C) ⋯ ⋙ ⊤.ι)).hom.app (⊤.ι.obj X) =
      𝟙 (⊤.ι.obj X)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
F : C ⥤ Type w
X : C
snd✝ : F.obj X
Y : C
y : F.obj Y
⊢ Function.Injective fun g ↦ ↑g

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ {X Y : WithTerminal C} (f : X ⟶ Y),
    (map (𝟭 C)).map f ≫
        (match Y with
          | of a => Iso.refl ((map (𝟭 C)).obj (of a))
          | star => Iso.refl ((map (𝟭 C)).obj star)).hom =
      (match X with
          | of a => Iso.refl ((map (𝟭 C)).obj (of a))
          | star => Iso.refl ((map (𝟭 C)).obj star)).hom ≫
        (𝟭 (WithTerminal C)).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
E : Type u_2
inst✝¹ : Category.{v_1, u_1} D
inst✝ : Category.{v_2, u_2} E
F : C ⥤ D
G : D ⥤ E
⊢ ∀ {X Y : WithTerminal C} (f : X ⟶ Y),
    (map (F ⋙ G)).map f ≫
        (match Y with
          | of a => Iso.refl ((map (F ⋙ G)).obj (of a))
          | star => Iso.refl ((map (F ⋙ G)).obj star)).hom =
      (match X with
          | of a => Iso.refl ((map (F ⋙ G)).obj (of a))
          | star => Iso.refl ((map (F ⋙ G)).obj star)).hom ≫
        (map F ⋙ map G).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : WithTerminal C
⊢ ∀ (a : X ⟶ star),
    a =
      match X with
      | of a => PUnit.unit
      | star => PUnit.unit

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝¹ x✝ : WithTerminal (Discrete J)
a : x✝¹ ⟶ x✝
⊢ ∀ (b : x✝¹ ⟶ x✝), a = b

Tactic:
b

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝¹ x✝ : WithTerminal (Discrete J)
a b : x✝¹ ⟶ x✝
⊢ a = b
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ {X Y : WithInitial C} (f : X ⟶ Y),
    (map (𝟭 C)).map f ≫
        (match Y with
          | of a => Iso.refl ((map (𝟭 C)).obj (of a))
          | star => Iso.refl ((map (𝟭 C)).obj star)).hom =
      (match X with
          | of a => Iso.refl ((map (𝟭 C)).obj (of a))
          | star => Iso.refl ((map (𝟭 C)).obj star)).hom ≫
        (𝟭 (WithInitial C)).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
E : Type u_2
inst✝¹ : Category.{v_1, u_1} D
inst✝ : Category.{v_2, u_2} E
F : C ⥤ D
G : D ⥤ E
⊢ ∀ {X Y : WithInitial C} (f : X ⟶ Y),
    (map (F ⋙ G)).map f ≫
        (match Y with
          | of a => Iso.refl ((map (F ⋙ G)).obj (of a))
          | star => Iso.refl ((map (F ⋙ G)).obj star)).hom =
      (match X with
          | of a => Iso.refl ((map (F ⋙ G)).obj (of a))
          | star => Iso.refl ((map (F ⋙ G)).obj star)).hom ≫
        (map F ⋙ map G).map f

Tactic:
by cat_disch

Goal state after: