mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
n : Q
q : N
⊢ (inverse_of_rightInverse Q hfg✝ hgh ∘ₗ lTensor Q g) (n ⊗ₜ[R] q) = (lTensor Q f).range.mkQ (n ⊗ₜ[R] q)

Tactic:
suffices Submodule.Quotient.mk (n ⊗ₜ[R] h (g q)) = Submodule.Quotient.mk (n ⊗ₜ[R] q) by
    simpa

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
n : Q
q : N
⊢ Submodule.Quotient.mk (n ⊗ₜ[R] h (g q)) = Submodule.Quotient.mk (n ⊗ₜ[R] q)
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case insert.refine_3
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x y : M ⊗[R] N
hx : ∃ M' N', M'.FG ∧ N'.FG ∧ insert x s ⊆ ↑(mapIncl M' N').range
hy : ∃ M' N', M'.FG ∧ N'.FG ∧ insert y s ⊆ ↑(mapIncl M' N').range
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ ↑(mapIncl M' N').range

Tactic:
obtain ⟨M₁', N₁', hM₁', hN₁', h₁⟩ := hx
    obtain ⟨M₂', N₂', hM₂', hN₂', h₂⟩ := hy
    refine ⟨_, _, hM₁'.sup hM₂', hN₁'.sup hN₂', Set.insert_subset (add_mem ?_ ?_) fun z hz ↦ ?_⟩
    · exact range_mapIncl_mono le_sup_left le_sup_left (h₁ (Set.mem_insert x s))
    · exact range_mapIncl_mono le_sup_right le_sup_right (h₂ (Set.mem_insert y s))
    · exact range_mapIncl_mono le_sup_left le_sup_left (h₁ (Set.subset_insert x s hz))

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝ : MonoidWithZero R
hx : nilpotencyClass x = 1
⊢ x = 0

Tactic:
have : IsNilpotent x := isNilpotent_of_pos_nilpotencyClass (hx ▸ Nat.one_pos)

Goal state after:
R : Type u_1
x : R
inst✝ : MonoidWithZero R
hx : nilpotencyClass x = 1
this : IsNilpotent x
⊢ x = 0
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (G i)
inst✝¹ : (i : ι) → Module R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)
x✝³ : ∀ (i j : ι) (h : i ≤ j), DistribMulActionHomClass (T h) R (G i) (G j)
x✝² x✝¹ : R
i : ι
x✝ : G i
⊢ (x✝² + x✝¹) • ⟦⟨i, x✝⟩⟧ = x✝² • ⟦⟨i, x✝⟩⟧ + x✝¹ • ⟦⟨i, x✝⟩⟧

Tactic:
by simp_rw [smul_def, add_smul, add_def]

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
inst✝¹ : Neg α
R : Type u_3
inst✝ : Mul R
f g : α → R
hf : Function.Even f
hg : Function.Even g
a : α
⊢ (f * g) (-a) = (f * g) a

Tactic:
simp only [Pi.mul_apply, hf a, hg a]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₁
inst✝ : Module R N₂
ist : Function.Bijective ⇑(TensorProduct.lift f)
e₁ : N₁ ≃ₗ[R] M₁
e₂ : N₂ ≃ₗ[R] M₂
⊢ Function.Bijective ⇑(TensorProduct.lift ((f ∘ₗ ↑e₁).compl₂ ↑e₂))

Tactic:
← TensorProduct.lift_comp_map,

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₁
inst✝ : Module R N₂
ist : Function.Bijective ⇑(TensorProduct.lift f)
e₁ : N₁ ≃ₗ[R] M₁
e₂ : N₂ ≃ₗ[R] M₂
⊢ Function.Bijective ⇑(TensorProduct.lift f ∘ₗ TensorProduct.map ↑e₁ ↑e₂)
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons_cons
α : Type u_1
xs ys l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : l₁✝.sym2 <+ l₂✝.sym2
⊢ (a :: l₁✝).sym2 <+ (a :: l₂✝).sym2

Tactic:
simp only [List.sym2, map_cons, cons_append]
    exact cons_cons _ (append (Sublist.map _ h) ih)

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_2
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
⊢ (↑ULift.moduleEquiv ∘ₗ g) ∘ₗ f'' = LinearMap.id

Tactic:
ext x
    change (g <| (1 : S) • f x).down = _
    rw [one_smul, hg]
    rfl

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
x y z w : α
⊢ Rel α (x, y) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
x y z w : α
⊢ s(x, y) = s(z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
p q : α × α
⊢ s(p.1, p.2) = s(q.1, q.2) ↔ p = q ∨ p = q.swap

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
p : α → Prop
a b : α
⊢ (∀ c ∈ s(a, b), p c) ↔ p a ∧ p b

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
r : α → α → Prop
hr : Std.Symm r
f : α → β
x✝ : Sym2 β
a b : β
⊢ ∀ (x x_1 : α), r x x_1 → f x = b → f x_1 = a → ∃ a_4 b_1, r a_4 b_1 ∧ f a_4 = a ∧ f b_1 = b

Tactic:
exact fun c d hcd hc hd ↦ ⟨d, c, symm hcd, hd, hc⟩

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Y ⟶ X
⊢ α.hom ≫ f = 𝟙 X ↔ f = α.inv

Tactic:
by
  rw [← eq_inv_comp, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Category

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
F G : C ⥤ D
H : D ⥤ E
α : F ⟶ G
X : C
⊢ (α ◫ 𝟙 H).app X = H.map (α.app X)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
X : C
Y : D
g g' : G.obj X ⟶ Y
⊢ α.hom.app X ≫ g = α.hom.app X ≫ g' ↔ g = g'

Tactic:
simp only [cancel_epi, refl]

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
X : C
Y : D
g g' : F.obj X ⟶ Y
⊢ α.inv.app X ≫ g = α.inv.app X ≫ g' ↔ g = g'

Tactic:
simp only [cancel_epi, refl]

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
α : F ≅ G
f : X ⟶ Y
⊢ α.inv.app X ≫ F.map f ≫ α.hom.app Y = G.map f

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
α : F ≅ G
f : X ⟶ Y
⊢ α.hom.app X ≫ G.map f ≫ α.inv.app Y = F.map f

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
e : X ≅ Y
⊢ F.map e.inv ≫ α.app X ≫ G.map e.hom = α.app Y

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
e : X ≅ Y
⊢ F.map e.hom ≫ α.app Y ≫ G.map e.inv = α.app X

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ e.unit.app X ≫ e.unitInv.app X = 𝟙 X

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ e.unitInv.app X ≫ e.unit.app X = 𝟙 (e.inverse.obj (e.functor.obj X))

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.counit.app Y ≫ e.counitInv.app Y = 𝟙 (e.functor.obj (e.inverse.obj Y))

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.counitInv.app Y ≫ e.counit.app Y = 𝟙 Y

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

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
e : C ≌ D
f : D ≌ E
X : C
⊢ (e.functor ⋙ f.functor).map
        ((e.unitIso ≪≫
                isoWhiskerRight
                    (e.functor.rightUnitor.symm ≪≫
                      e.functor.isoWhiskerLeft f.unitIso ≪≫ (e.functor.associator f.functor f.inverse).symm)
                    e.inverse ≪≫
                  (e.functor ⋙ f.functor).associator f.inverse e.inverse).hom.app
          X) ≫
      (((f.inverse ⋙ e.inverse).associator e.functor f.functor).symm ≪≫
              isoWhiskerRight
                  (f.inverse.associator e.inverse e.functor ≪≫
                    f.inverse.isoWhiskerLeft e.counitIso ≪≫ f.inverse.rightUnitor)
                  f.functor ≪≫
                f.counitIso).hom.app
        ((e.functor ⋙ f.functor).obj X) =
    𝟙 ((e.functor ⋙ f.functor).obj X)

Tactic:
dsimp
    simp only [comp_id, id_comp, map_comp, fun_inv_map, comp_obj, id_obj, counitInv,
      functor_unit_comp_assoc, assoc]
    slice_lhs 2 3 => rw [← Functor.map_comp, Iso.inv_hom_id_app]
    simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ single f ≤ W ↔ W f

Tactic:
by
  simp

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : T
i : X ≅ Y
p : Arrow T
sq : mk i.hom ⟶ p
⊢ i.inv ≫ Hom.left sq ≫ p.hom = Hom.right sq

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.RespectsIso
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
L : A ⥤ C
R : B ⥤ C
f g : Comma L R
e : f ≅ g
⊢ P f.hom ↔ P g.hom

Tactic:
by
  simp [← Comma.inv_left_hom_right e.hom, cancel_left_of_respectsIso, cancel_right_of_respectsIso]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ (P.map F).RespectsIso

Tactic:
by
  rw [map_eq_isoClosure]
  infer_instance

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

Goal state before:
pp: 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
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ L.map e.left ≫ Y.hom ≫ R.map (inv e.right) = X.hom

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ≅ Y
⊢ F.mapIso ((α.isoCongr β) f) = ((F.mapIso α).isoCongr (F.mapIso β)) (F.mapIso f)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N : MonCat
e : M ≅ N
x : ↑M
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N : MonCat
e : M ≅ N
s : ↑N
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N : CommMonCat
e : M ≅ N
x : ↑M
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N : CommMonCat
e : M ≅ N
s : ↑N
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by
  simp

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

Goal state before:
pp: X Y : GrpCat
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by
  simp

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

Goal state before:
pp: X Y : GrpCat
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by
  simp

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

Goal state before:
pp: X Y : CommGrpCat
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by
  simp

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

Goal state before:
pp: X Y : CommGrpCat
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by
  simp

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

Goal state before:
pp: R S : SemiRingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
by
  simp

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

Goal state before:
pp: R S : SemiRingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by
  simp

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

Goal state before:
pp: X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
⊢ IsIso f

Tactic:
by
    let i := asIso ((forget SemiRingCat).map f)
    let ff : X →+* Y := f.hom
    let e : X ≃+* Y := { ff, i.toEquiv with }
    exact e.toSemiRingCatIso.isIso_hom

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

Goal state before:
pp: R S : RingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
by
  simp

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

Goal state before:
pp: R S : RingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by
  simp

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

Goal state before:
pp: R S : CommSemiRingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
by
  simp

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

Goal state before:
pp: R S : CommSemiRingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by
  simp

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

Goal state before:
pp: R S : CommRingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
by
  simp

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

Goal state before:
pp: R S : CommRingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
⊢ (adj.homEquiv X (F.obj X)).symm (adj.unit.app X) = 𝟙 (F.obj X)

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
⊢ (adj.homEquiv X' Y).symm (f ≫ g) = F.map f ≫ (adj.homEquiv X Y).symm g

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
Y Y' : D
f : F.obj X ⟶ Y
g : Y ⟶ Y'
⊢ (adj.homEquiv X Y') (f ≫ g) = (adj.homEquiv X Y) f ≫ G.map g

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
H : D ⥤ C
adj : F ⊣ H
iso : F ≅ G
X : C
Y : D
f : G.obj X ⟶ Y
⊢ ((adj.ofNatIsoLeft iso).homEquiv X Y) f = (adj.homEquiv X Y) (iso.hom.app X ≫ f)

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
H : D ⥤ C
adj : F ⊣ H
iso : F ≅ G
X : C
Y : D
f : X ⟶ H.obj Y
⊢ ((adj.ofNatIsoLeft iso).homEquiv X Y).symm f = iso.inv.app X ≫ (adj.homEquiv X Y).symm f

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G H : D ⥤ C
adj : F ⊣ G
iso : G ≅ H
X : C
Y : D
f : F.obj X ⟶ Y
⊢ ((adj.ofNatIsoRight iso).homEquiv X Y) f = (adj.homEquiv X Y) f ≫ iso.hom.app Y

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G H : D ⥤ C
adj : F ⊣ G
iso : G ≅ H
X : C
Y : D
f : X ⟶ H.obj Y
⊢ ((adj.ofNatIsoRight iso).homEquiv X Y).symm f = (adj.homEquiv X Y).symm (f ≫ iso.inv.app Y)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : op X ⟶ op Y
⊢ (ConcreteCategory.hom ((yoneda.obj X).map f)) (𝟙 X) = (ConcreteCategory.hom ((yoneda.map f.unop).app (op Y))) (𝟙 Y)

Tactic:
by
  simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
k : c ⟶ d
⊢ η.hom ▷ h ▷ k ≫ η.inv ▷ h ▷ k = 𝟙 ((f ≫ h) ≫ k)

Tactic:
simp [← comp_whiskerRight]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
k : c ⟶ d
⊢ η.inv ▷ h ▷ k ≫ η.hom ▷ h ▷ k = 𝟙 ((g ≫ h) ≫ k)

Tactic:
simp [← comp_whiskerRight]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom =
    f ◁ (α_ g h i).inv ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv

Tactic:
← cancel_mono (α_ (f ≫ g) h i).inv

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom) ≫ (α_ (f ≫ g) h i).inv =
    (f ◁ (α_ g h i).inv ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) ≫ (α_ (f ≫ g) h i).inv
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ 𝟙 a ◁ η ≫ (λ_ g).hom = (λ_ f).hom ≫ η

Tactic:
by
  simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (λ_ f).inv ≫ 𝟙 a ◁ η ≫ (λ_ g).hom

Tactic:
by
  simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (ρ_ f).inv ≫ η ▷ 𝟙 b ≫ (ρ_ g).hom

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C : Cat
X : ↑C
⊢ (𝟙 C).toFunctor.obj X = X

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C : Cat
X Y : ↑C
f : X ⟶ Y
⊢ (𝟙 C).toFunctor.map f = f

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C D E : Cat
F : C ⟶ D
G : D ⟶ E
X : ↑C
⊢ (F ≫ G).toFunctor.obj X = G.toFunctor.obj (F.toFunctor.obj X)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C D E : Cat
F : C ⟶ D
G : D ⟶ E
X Y : ↑C
f : X ⟶ Y
⊢ (F ≫ G).toFunctor.map f = G.toFunctor.map (F.toFunctor.map f)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C D : Cat
F : C ⟶ D
X : ↑C
⊢ (𝟙 F).toNatTrans.app X = 𝟙 (F.toFunctor.obj X)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C D : Cat
F G : C ⟶ D
h : F = G
X : ↑C
⊢ (eqToHom h).toNatTrans.app X = eqToHom ⋯

Tactic:
by
  simp

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c : Cocone F
j j' : J
f : j' ⟶ j
F' : C → C → Type uF
carrier : C → Type w
instFunLike : (X Y : C) → FunLike (F' X Y) (carrier X) (carrier Y)
inst : ConcreteCategory C F'
x : carrier (F.obj j')
⊢ (ConcreteCategory.hom (c.ι.app j)) ((ConcreteCategory.hom (F.map f)) x) = (ConcreteCategory.hom (c.ι.app j')) x

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ sq.HasLift

Tactic:
rw [← sq.right_adjoint_hasLift_iff adj]
    infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ f =
    hl.lift { pt := c.pt, π := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } } ≫
      hi.hom

Tactic:
dsimp
    rw [← hl.uniq _ (f ≫ hi.inv) _]
    · simp only [Category.assoc, Iso.inv_hom_id, Category.comp_id]
    · simp

Goal state after: