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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
⊢ Flat R M ↔
    ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
      [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)

Tactic:
refine ⟨fun _ ↦ rTensor_exact _, fun H ↦ iff_rTensor_preserves_injective_linearMap'.mpr
    fun N' N'' _ _ _ _ f hf ↦ LinearMap.ker_eq_bot |>.mp <| eq_bot_iff |>.mpr
      fun x (hx : _ = 0) ↦ ?_⟩

Goal state after:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝³ : AddCommGroup N'
x✝² : AddCommGroup N''
x✝¹ : Module R N'
x✝ : Module R N''
f : N' →ₗ[R] N''
hf : Injective ⇑f
x : N' ⊗[R] M
hx : (rTensor M f) x = 0
⊢ x ∈ ⊥
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module ℚ≥0 M
s t : Finset ι
f g : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hst : s = t
hpq : ∀ i ∈ t, p i ↔ q i
h : ∀ i ∈ t, q i → f i = g i
⊢ {i ∈ t | p i} = {i ∈ t | q i}

Tactic:
filter_inj'.2 hpq

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module ℚ≥0 M
s t : Finset ι
f g : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hst : s = t
hpq : ∀ i ∈ t, p i ↔ q i
h : ∀ i ∈ t, q i → f i = g i
⊢ filter q t = {i ∈ t | q i}
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✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝² : (i : ι) → DistribMulAction R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝ : Nonempty ι
i : ι
m : R
x : G i
⊢ ⟦⟨i, m • x⟩⟧ = ⟦⟨i, (MonoidHom.id R) m • x⟩⟧

Tactic:
MonoidHom.id_apply

Goal state after:
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✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝² : (i : ι) → DistribMulAction R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝ : Nonempty ι
i : ι
m : R
x : G i
⊢ ⟦⟨i, m • x⟩⟧ = ⟦⟨i, m • x⟩⟧
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
⊢ G ⟨j - 1, ⋯⟩ ∈ ↑F

Tactic:
by simp [G, F.orderEmbOfFin_mem (α := α ×ₗ α)]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
⊢ G ⟨j, ⋯⟩ ∈ ↑F

Tactic:
by simp [G, F.orderEmbOfFin_mem (α := α ×ₗ α)]

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
N : Type u_8
inst✝¹¹ : AddCommMonoid N₁
inst✝¹⁰ : AddCommMonoid N₂
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
P₁ : Type u_9
P₂ : Type u_10
P : Type u_11
inst✝⁵ : AddCommMonoid P₁
inst✝⁴ : AddCommMonoid P₂
inst✝³ : AddCommMonoid P
inst✝² : Module R P₁
inst✝¹ : Module R P₂
inst✝ : Module R P
p : P₁ →ₗ[R] P₂ →ₗ[R] P
hf : IsTensorProduct f
hg : IsTensorProduct g
hp : IsTensorProduct p
i₁ : N₁ →ₗ[R] P₁
j₁ : M₁ →ₗ[R] N₁
i₂ : N₂ →ₗ[R] P₂
j₂ : M₂ →ₗ[R] N₂
x x✝¹ x✝ : M
h₁ : (hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂)) x✝¹ = (hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂) x✝¹
h₂ : (hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂)) x✝ = (hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂) x✝
⊢ (hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂)) (x✝¹ + x✝) = (hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂) (x✝¹ + x✝)

Tactic:
by simp [h₁, h₂]

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
hf : IsTensorProduct f
x x✝¹ x✝ : M
h₁ : (hf.map hf LinearMap.id LinearMap.id) x✝¹ = LinearMap.id x✝¹
h₂ : (hf.map hf LinearMap.id LinearMap.id) x✝ = LinearMap.id x✝
⊢ (hf.map hf LinearMap.id LinearMap.id) (x✝¹ + x✝) = LinearMap.id (x✝¹ + x✝)

Tactic:
by simp [h₁, h₂]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : (G ⟨j, ⋯⟩).1 < (G ⟨j - 1, ⋯⟩).2
hG : (G ⟨j - 1, ⋯⟩).1 ≤ (G ⟨j, ⋯⟩).1
⊢ G ⟨j, ⋯⟩ ∈ F

Tactic:
by simp [G, F.orderEmbOfFin_mem (α := α ×ₗ α)]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
z : Sym2 α
x y : α
⊢ s(x, y) ∈ m.toFinset.sym2 ↔ s(x, y) ∈ m.sym2.toFinset

Tactic:
simp only [mk_mem_sym2_iff, Multiset.mem_toFinset, Multiset.mk_mem_sym2_iff]

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

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

Tactic:
simp only [List.sym2]
    exact Sublist.append (nil_sublist _) ih

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: 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 : IsBaseChange S f
Q : Type (max v₁ v₂ v₃)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module S Q
inst✝ : IsScalarTower R S Q
⊢ ∀ (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g

Tactic:
g

Goal state after:
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 : IsBaseChange S f
Q : Type (max v₁ v₂ v₃)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module S Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
⊢ ∃! g', ↑R g' ∘ₗ f = g
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
⊢ ∀ (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ ↑e = g

Tactic:
g

Goal state after:
R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
⊢ ∃! g', ↑R g' ∘ₗ ↑e = g
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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 : C ⥤ E
inst✝¹ : F.Faithful
G : D ⥤ E
inst✝ : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
⊢ Faithful.div F G obj h_obj map h_map ⋙ G = F

Tactic:
by
  obtain ⟨F_obj, _, _, _⟩ := F; obtain ⟨G_obj, _, _, _⟩ := G
  unfold Faithful.div Functor.comp
  have : F_obj = G_obj ∘ obj := (funext h_obj).symm
  subst this
  congr
  simp only [Function.comp_apply, heq_eq_eq] at h_map
  ext
  exact h_map

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
h : Y = Z
⊢ f ≫ eqToHom h = 𝟙 X ≫ f ≫ eqToHom h

Tactic:
Category.id_comp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
h : Y = Z
⊢ f ≫ eqToHom h = f ≫ eqToHom h
Module: Mathlib.CategoryTheory.EqToHom

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_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), map✝¹ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
G_obj : C → D
map✝ : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (G_obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
      eqToHom ⋯ ≫ { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯
⊢ { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
| =>

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), map✝¹ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
G_obj : C → D
map✝ : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (G_obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
      eqToHom ⋯ ≫ { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯
⊢ { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: case h_map
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
⊢ ∀ (f_1 : X ⟶ Y), f.map f_1 = eqToHom ⋯ ≫ f'.map f_1 ≫ eqToHom ⋯

Tactic:
g

Goal state after:
case h_map
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
⊢ f.map g = eqToHom ⋯ ≫ f'.map g ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝¹ : IsIso sq
inst✝ : IsIso f.hom
⊢ IsIso g.hom

Tactic:
iso_w (asIso sq)

Goal state after:
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝¹ : IsIso sq
inst✝ : IsIso f.hom
⊢ IsIso (Hom.left (asIso sq).inv ≫ f.hom ≫ Hom.right (asIso sq).hom)
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' : s ⟶ t
⊢ ∀ {g : s ⟶ t}, g = h.liftConeMorphism s

Tactic:
intro g; apply ConeMorphism.ext; exact h.uniq _ _ g.w

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
s : Cone F
s_pt : C
s_π : (const J).obj s_pt ⟶ F
⊢ { pt := { pt := s_pt, π := s_π }.pt, π := h.homEquiv (h.homEquiv.symm { pt := s_pt, π := s_π }.π) } =
    { pt := s_pt, π := s_π }

Tactic:
| =>

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
s : Cone F
s_pt : C
s_π : (const J).obj s_pt ⟶ F
⊢ { pt := { pt := s_pt, π := s_π }.pt, π := h.homEquiv (h.homEquiv.symm { pt := s_pt, π := s_π }.π) } =
    { pt := s_pt, π := s_π }
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
s_pt : C
s_ι : F ⟶ (const J).obj s_pt
⊢ { pt := { pt := s_pt, ι := s_ι }.pt, ι := h.homEquiv (h.homEquiv.symm { pt := s_pt, ι := s_ι }.ι) } =
    { pt := s_pt, ι := s_ι }

Tactic:
| =>

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
s_pt : C
s_ι : F ⟶ (const J).obj s_pt
⊢ { pt := { pt := s_pt, ι := s_ι }.pt, ι := h.homEquiv (h.homEquiv.symm { pt := s_pt, ι := s_ι }.ι) } =
    { pt := s_pt, ι := s_ι }
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
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X X' : C
Y : D
f : X ⟶ X'
⊢ ∀ (g : X' ⟶ (rightAdjointOfEquiv e he).obj Y), (e X Y).symm (f ≫ g) = F.map f ≫ (e X' Y).symm g

Tactic:
g

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X X' : C
Y : D
f : X ⟶ X'
g : X' ⟶ (rightAdjointOfEquiv e he).obj Y
⊢ (e X Y).symm (f ≫ g) = F.map f ≫ (e X' Y).symm g
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
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X : C
Y Y' : D
⊢ ∀ (f : F.obj X ⟶ Y) (g : Y ⟶ Y'), (e X Y') (f ≫ g) = (e X Y) f ≫ (rightAdjointOfEquiv e he).map g

Tactic:
g

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X : C
Y Y' : D
g : F.obj X ⟶ Y
⊢ ∀ (g_1 : Y ⟶ Y'), (e X Y') (g ≫ g_1) = (e X Y) g ≫ (rightAdjointOfEquiv e he).map g_1
Module: Mathlib.CategoryTheory.Limits.Cones

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
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : Discrete PUnit.{?u.56 + 1} ⥤ C
X Y : Discrete PUnit.{?u.56 + 1}
f : X ⟶ Y
A B : PUnit.{?u.56 + 1}
g : PLift ({ as := A }.as = { as := B }.as)
⊢ (((const (Discrete PUnit.{?u.56 + 1})).obj (F.obj { as := PUnit.unit })).map { down := g } ≫
      match { as := B } with
      | { as := PUnit.unit } =>
        𝟙 (((const (Discrete PUnit.{?u.56 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) =
    (match { as := A } with
      | { as := PUnit.unit } =>
        𝟙 (((const (Discrete PUnit.{?u.56 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) ≫
      F.map { down := g }

Tactic:
| =>

Goal state after:
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
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : Discrete PUnit.{?u.56 + 1} ⥤ C
X Y : Discrete PUnit.{?u.56 + 1}
f : X ⟶ Y
A B : PUnit.{?u.56 + 1}
g : PLift ({ as := A }.as = { as := B }.as)
⊢ (((const (Discrete PUnit.{?u.56 + 1})).obj (F.obj { as := PUnit.unit })).map { down := g } ≫
      match { as := B } with
      | { as := PUnit.unit } =>
        𝟙 (((const (Discrete PUnit.{?u.56 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) =
    (match { as := A } with
      | { as := PUnit.unit } =>
        𝟙 (((const (Discrete PUnit.{?u.56 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) ≫
      F.map { down := g }
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mp
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 (G.map i) p
f : A ⟶ F.obj X
⊢ ∀ {g : B ⟶ F.obj Y} (sq : CommSq f i (F.map p) g), sq.HasLift

Tactic:
g

Goal state after:
case mp
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 (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
⊢ ∀ (sq : CommSq f i (F.map p) g), sq.HasLift
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:
g

Goal state after:
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
Module: Mathlib.CategoryTheory.Functor.EpiMono

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 Y : C
f : X ⟶ Y
hf : Epi f
Z : D
⊢ ∀ (g h : F.obj Y ⟶ Z), F.map f ≫ g = F.map f ≫ h → g = h

Tactic:
g

Goal state after:
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 Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g : F.obj Y ⟶ Z
⊢ ∀ (h : F.obj Y ⟶ Z), F.map f ≫ g = F.map f ≫ h → g = h
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
g : β → C
inst✝ : HasProduct f
e : β ≃ α
iso : (j : β) → g j ≅ f (e j)
⊢ HasProduct g

Tactic:
have α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
    Discrete.natIso (fun ⟨j⟩ => iso j)
  exact hasLimit_of_iso α.symm

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
e : c.inl ≫ l ≫ c.inl = 𝟙 X ≫ c.inl
⊢ c.inl ≫ l ≫ c.inl = c.inl

Tactic:
Category.id_comp

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
e : c.inl ≫ l ≫ c.inl = c.inl
⊢ c.inl ≫ l ≫ c.inl = c.inl
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₂
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
Z✝ : C
i₁ i₂ : Z✝ ⟶ W ⨯ X
h : i₁ ≫ map f g = i₂ ≫ map f g
⊢ i₁ ≫ snd = i₂ ≫ snd

Tactic:
← cancel_mono g

Goal state after:
case h₂
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
Z✝ : C
i₁ i₂ : Z✝ ⟶ W ⨯ X
h : i₁ ≫ map f g = i₂ ≫ map f g
⊢ (i₁ ≫ snd) ≫ g = (i₂ ≫ snd) ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ 𝟙 (image f) ≫ image.ι f = image.ι f

Tactic:
Category.id_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ image.ι f = image.ι f
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ g = 𝟙 (image f) ≫ g

Tactic:
Category.id_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ g = g