mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case intro
β : Type u_3
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val✝ : Fintype β
l : List (Perm β)
⊢ (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod

Tactic:
induction l with
  | nil => exact fun _ _ => base_one
  | cons σ l ih =>
    intro h1 h2
    rw [List.prod_cons]
    exact
      induction_disjoint σ l.prod (disjoint_prod_right _ (List.pairwise_cons.mp h2).1)
        (h1 _ List.mem_cons_self) (base_cycles σ (h1 σ List.mem_cons_self))
        (ih (fun τ hτ => h1 τ (List.mem_cons_of_mem σ hτ)) h2.of_cons)

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inl
n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
hφD : Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D
x✝ : (_ : Fin n) × Fin n
x₁ x₂ : Fin n
hx : x₂ < x₁
hlt : σ x₁ < σ x₂
⊢ f (σ ⟨x₁, x₂⟩.snd) (σ ⟨x₁, x₂⟩.fst) =
    ↑↑(if
              σ⁻¹ ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.snd <
                σ⁻¹ ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.fst then
            1
          else -1) *
      f ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.snd
        ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.fst

Tactic:
simp [inf_eq_left.2 hlt.le, sup_eq_right.2 hlt.le, hx.not_gt, ← hf]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3.inl.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = σ a
x : α
hx : σ x = x
⊢ τ x = x ∨ (σ * f⁻¹) x = x

Tactic:
refine Or.inr ?_
          by_cases hfx : f x = x
          · rw [← hfx]
            simpa [hx] using hfx.symm
          · rw [mul_apply]
            rw [← hf.right _ (mem_support.mpr hfx)] at hx
            contradiction

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3.inr.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = τ a
x : α
hx : τ x = x
⊢ σ x = x ∨ (τ * f⁻¹) x = x

Tactic:
refine Or.inr ?_
          by_cases hfx : f x = x
          · rw [← hfx]
            simpa [hx] using hfx.symm
          · rw [mul_apply]
            rw [← hf.right _ (mem_support.mpr hfx)] at hx
            contradiction

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

Goal state before:
pp: case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
i : ι
hi : i = i₀
⊢ C i₀ ⊆ A i₀

Tactic:
simp only [C, hj₂, Finset.singleton_subset_iff, update_self]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
⊢ ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign 1, ∏ i, A i (σ i) * B (σ i) (τ i) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i, A i (σ i) * B (σ i) (τ i) +
      (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B))

Tactic:
refine congr_arg₂ (· + ·) (sum_congr rfl fun σ hσ ↦ ?_) (add_comm _ _)

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
σ : n → n
hσ : σ ∈ bijᶜ
⊢ ∑ τ ∈ ofSign 1, ∏ i, A i (σ i) * B (σ i) (τ i) = ∑ τ ∈ ofSign (-1), ∏ i, A i (σ i) * B (σ i) (τ i)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
⊢ (-A).det = (-1) ^ Fintype.card n * A.det

Tactic:
by
  rw [← det_smul, neg_one_smul]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type w
I : α → Type u₁
inst✝¹ : (i : α) → Category.{v₁, u₁} (I i)
inst✝ : ∀ (i : α), IsCofilteredOrEmpty (I i)
k l : (i : α) → I i
f g : k ⟶ l
s : α
⊢ ((fun s ↦ eqHom (f s) (g s)) ≫ f) s = ((fun s ↦ eqHom (f s) (g s)) ≫ g) s

Tactic:
by simp [eq_condition (f s) (g s)]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
G : J ⥤ Type w₀'
e : (j : J) → G.obj j ≃ F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)
c' : G.CoconeTypes
j : J
⊢ hc.desc (c'.precompose (fun {j'} ↦ ⇑(e j').symm) ⋯) ∘ (c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).ι j = c'.ι j

Tactic:
by
    rw [precompose_ι, ← Function.comp_assoc, hc.fac, precompose_ι, Function.comp_assoc,
      Equiv.symm_comp_self, Function.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬(hom (t.ι.app x_1)) x_2 = x
⊢ (↾fun x ↦ { down := True }) = ↾fun y ↦ { down := y ≠ x }

pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬(hom (t.ι.app x_1)) x_2 = x
⊢ (↾fun x ↦ { down := True }) ≠ ↾fun y ↦ { down := y ≠ x }

Tactic:
· refine h.hom_ext fun j ↦ ?_
    ext y
    simp only [TypeCat.Fun.toFun_apply, comp_apply, hom_ofHom,
      TypeCat.Fun.coe_mk, ne_eq, true_iff]
    exact hx j y

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬(hom (t.ι.app x_1)) x_2 = x
⊢ (↾fun x ↦ { down := True }) ≠ ↾fun y ↦ { down := y ≠ x }
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M'
f✝ f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
a b : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) (a + b)) =
    f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) a) +
      f (update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) b)

Tactic:
simp only [MultilinearMap.map_update_add]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', y⟩ → FilteredColimit.Rel F ⟨j, x⟩ ⟨j', y⟩

Tactic:
rw [← (FilteredColimit.rel_equiv F).eqvGen_iff]
    exact Relation.EqvGen.mono (rel_of_colimitTypeRel F) _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_4
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : (a : o) → a ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ (∏ x, ↑↑(sign (σ x ⋯))) * ∏ x, ∏ x_1, M x ((σ x ⋯) x_1) x_1 =
    ↑↑(sign (prodCongrLeft fun k ↦ σ k ⋯)) * ∏ i ∈ univ ×ˢ univ, blockDiagonal M ((prodCongrLeft fun k ↦ σ k ⋯) i) i

Tactic:
Finset.prod_product_right

Goal state after:
case refine_4
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : (a : o) → a ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ (∏ x, ↑↑(sign (σ x ⋯))) * ∏ x, ∏ x_1, M x ((σ x ⋯) x_1) x_1 =
    ↑↑(sign (prodCongrLeft fun k ↦ σ k ⋯)) * ∏ y, ∏ x, blockDiagonal M ((prodCongrLeft fun k ↦ σ k ⋯) (x, y)) (x, y)
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x y : ↑(F.obj j)
⊢ M.mk F ⟨j, x⟩ * M.mk F ⟨j, y⟩ = M.mk F ⟨j, x * y⟩

Tactic:
simpa using! colimit_mul_mk_eq F ⟨j, x⟩ ⟨j, y⟩ j (𝟙 _) (𝟙 _)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: α β : Type u
f✝ : α ⟶ β
f g : Arrow (Type u)
st : f ⟶ g
x : (monoFactorisation f.hom).I
⊢ (ConcreteCategory.hom g.hom) ((ConcreteCategory.hom (Arrow.Hom.left st)) (Classical.choose ⋯)) =
    (ConcreteCategory.hom (Arrow.Hom.right st)) ↑x

Tactic:
rw [elementwise_of% st.w]

Goal state after:
α β : Type u
f✝ : α ⟶ β
f g : Arrow (Type u)
st : f ⟶ g
x : (monoFactorisation f.hom).I
⊢ (ConcreteCategory.hom (Arrow.Hom.right st)) ((ConcreteCategory.hom f.hom) (Classical.choose ⋯)) =
    (ConcreteCategory.hom (Arrow.Hom.right st)) ↑x
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det = ∑ j, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
simp_rw [pow_add, mul_assoc, ← mul_sum]
  have : det A = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by
    calc
      det A = ↑((-1 : ℤˣ) ^ (i : ℕ) * (-1 : ℤˣ) ^ (i : ℕ) : ℤˣ) * det A := by simp
      _ = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by simp [-Int.units_mul_self]
  rw [this, mul_assoc]
  congr
  rw [← det_permute, det_succ_row_zero]
  refine Finset.sum_congr rfl fun j _ => ?_
  rw [mul_assoc, Matrix.submatrix_apply, submatrix_submatrix, id_comp, Function.comp_def, id]
  simp

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
t : Cocone F
x : ↑(R F)
⊢ (descMonoidHom t) x = (descAddMonoidHom t) x

Tactic:
by
  obtain ⟨j, x⟩ := x
  rw [descMonoidHom_quotMk t x, descAddMonoidHom_quotMk t x]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Yoneda

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
F : J ⥤ C
X : C
s : ↑(F ⋙ coyoneda.obj (op X)).sections
j j' : J
f : j ⟶ j'
⊢ ((const J).obj X).map f ≫ ↑s j' = ↑s j ≫ F.map f

Tactic:
by
        dsimp
        rw [Category.id_comp]
        exact (s.property f).symm

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ Cᵒᵖ
X : C
c : Cone F
hc : IsLimit c
s : (j : J) → (F ⋙ yoneda.obj X).obj j
hs : s ∈ (F ⋙ yoneda.obj X).sections
⊢ ∃! x, ∀ (j : J), (hom (((yoneda.obj X).mapCone c).π.app j)) x = s j

Tactic:
exact ⟨(hc.lift (Limits.coneOfSectionCompYoneda F X ⟨s, hs⟩)).unop,
      fun j => Quiver.Hom.op_inj (hc.fac (Limits.coneOfSectionCompYoneda F X ⟨s, hs⟩) j),
      fun m hm => Quiver.Hom.op_inj
        (hc.uniq (Limits.coneOfSectionCompYoneda F X ⟨s, hs⟩) _
          (fun j => Quiver.Hom.unop_inj (hm j)))⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cocone F
x✝¹ : (X : C) → IsLimit ((yoneda.obj X).mapCone c.op)
x✝ : C
⊢ (fun h x ↦ isLimitOfPreserves (yoneda.obj x) h.op) ((fun h ↦ (yonedaJointlyReflectsLimits F.op c.op h).unop) x✝¹) x✝ =
    x✝¹ x✝

Tactic:
apply Subsingleton.elim

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cone F
x✝¹ : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
x✝ : Cᵒᵖ
⊢ (fun h x ↦ isLimitOfPreserves (coyoneda.obj x) h) ((fun h ↦ coyonedaJointlyReflectsLimits F c h) x✝¹) x✝ = x✝¹ x✝

Tactic:
apply Subsingleton.elim

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
x : E.pt
y : ToType D.pt
H : (fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x) x = (fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x) y
j : J
⊢ ↑((Types.isLimitEquivSections (isLimitOfPreserves (forget C) hD)) x) j =
    ↑((Types.isLimitEquivSections (isLimitOfPreserves (forget C) hD)) y) j

Tactic:
exact funext_iff.mp H j

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (limitObjIsoLimitCompEvaluation F k).inv ≫ (limit.π F j).app k = limit.π (F ⋙ (evaluation K C).obj k) j

Tactic:
by
  dsimp [limitObjIsoLimitCompEvaluation]
  rw [Iso.inv_comp_eq]
  simp

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
⊢ L.essImage X → IsIso (h.counit.app X)

Tactic:
rintro ⟨_, ⟨i⟩⟩

Goal state after:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
w✝ : C
i : L.obj w✝ ≅ X
⊢ IsIso (h.counit.app X)
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
⊢ R.essImage Y → IsIso (h.unit.app Y)

Tactic:
rintro ⟨_, ⟨i⟩⟩

Goal state after:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
w✝ : D
i : R.obj w✝ ≅ Y
⊢ IsIso (h.unit.app Y)
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Finite J
val✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
⊢ ∑ j, b.π j ▷ X ≫ b.ι j ▷ X = 𝟙 (b.pt ⊗ X)

Tactic:
simp_rw [← tensorHom_id]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Finite J
val✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
⊢ ∑ x, (b.π x ⊗ₘ 𝟙 X) ≫ (b.ι x ⊗ₘ 𝟙 X) = 𝟙 (b.pt ⊗ X)
Module: Mathlib.CategoryTheory.Monoidal.Linear

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
⊢ ∀ (r : R) {Y Z : D} (f : Y ⟶ Z) (X : D), (r • f) ▷ X = r • f ▷ X

Tactic:
intro r X Y f Z

Goal state after:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ (r • f) ▷ Z = r • f ▷ Z
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X Y : C
val✝ : Fintype J
j✝ : J
⊢ ∑ x, (biproduct.π f x ▷ X ⊗ₘ 𝟙 Y) ≫ (biproduct.ι (fun j ↦ f j ⊗ X) x ⊗ₘ 𝟙 Y) ≫ biproduct.π (fun j ↦ f j ⊗ X) j✝ ▷ Y =
    (α_ (⨁ f) X Y).hom ≫ biproduct.π f j✝ ▷ (X ⊗ Y) ≫ (α_ (f j✝) X Y).inv

Tactic:
simp_rw [← tensorHom_id]

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X Y : C
val✝ : Fintype J
j✝ : J
⊢ ∑ x,
      ((biproduct.π f x ⊗ₘ 𝟙 X) ⊗ₘ 𝟙 Y) ≫
        (biproduct.ι (fun j ↦ f j ⊗ X) x ⊗ₘ 𝟙 Y) ≫ (biproduct.π (fun j ↦ f j ⊗ X) j✝ ⊗ₘ 𝟙 Y) =
    (α_ (⨁ f) X Y).hom ≫ (biproduct.π f j✝ ⊗ₘ 𝟙 (X ⊗ Y)) ≫ (α_ (f j✝) X Y).inv
Module: Mathlib.CategoryTheory.Monoidal.Functor

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

Tactic:
simpa using NatTrans.whiskerLeft_app_tensor_app adj.counit adj.counit (f := g) _

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
j : J
x : ↑(F.obj j)
⊢ (Quot.desc F s)
      ((AddEquiv.ofBijective (Quot.desc F c) h).symm ((AddEquiv.ofBijective (Quot.desc F c) h) ((Quot.ι F j) x))) =
    (Hom.hom (s.ι.app j)) x

Tactic:
AddEquiv.symm_apply_apply

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
j : J
x : ↑(F.obj j)
⊢ (Quot.desc F s) ((Quot.ι F j) x) = (Hom.hom (s.ι.app j)) x
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ (Hom.hom m) ((AddEquiv.ofBijective (Quot.desc F c) h) x) =
    (Quot.desc F s) ((AddEquiv.ofBijective (Quot.desc F c) h).symm ((AddEquiv.ofBijective (Quot.desc F c) h) x))

Tactic:
AddEquiv.symm_apply_apply

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ (Hom.hom m) ((AddEquiv.ofBijective (Quot.desc F c) h) x) = (Quot.desc F s) x
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x
⊢ (⅟x).fst * x.fst = 1

Tactic:
← fst_mul,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x
⊢ (⅟x * x).fst = 1
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x
⊢ x.fst * (⅟x).fst = 1

Tactic:
← fst_mul,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x
⊢ (x * ⅟x).fst = 1