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

Goal state before:
pp: case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun x y ↦ (swap x y).signAux3 hs = -1

Tactic:
change
    signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧
    Pairwise fun x y => signAux2 l (swap x y) = -1

Goal state after:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ Pairwise fun x y ↦ signAux2 l (swap x y) = -1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ Multiset.filter (fun x ↦ n = x.support.val.card) σ.cycleFactorsFinset.val =
    Multiset.filter (fun x ↦ ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n) σ.cycleFactorsFinset.val

Tactic:
apply Multiset.filter_congr

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ ∀ x ∈ σ.cycleFactorsFinset.val, n = x.support.val.card ↔ ∃ (_ : x ∈ σ.cycleFactorsFinset), x.support.val.card = n
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : #σ.support < 2 * orderOf σ
n : ℕ
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle

Tactic:
← σ.sum_cycleType,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : σ.cycleType.sum < 2 * orderOf σ
n : ℕ
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle
Module: Mathlib.GroupTheory.Perm.Option

Goal state before:
pp: case one
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Perm.sign (optionCongr 1) = Perm.sign 1

Tactic:
simp [Perm.one_def]

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

Goal state before:
pp: case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
h : cycleType 1 = τ.cycleType
⊢ IsConj 1 τ

Tactic:
rw [cycleType_one, eq_comm, cycleType_eq_zero] at h

Goal state after:
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
h : τ = 1
⊢ IsConj 1 τ
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
⊢ g.cycleOf y * (((g.cycleOf x)⁻¹ * g).cycleOf y)⁻¹ = 1

Tactic:
cycleOf_inv

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
⊢ g.cycleOf y * ((g.cycleOf x)⁻¹ * g)⁻¹.cycleOf y = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : 0 = 3
h0 : σ.cycleType = 0
⊢ σ.IsThreeCycle

Tactic:
exact (ne_of_lt zero_lt_three h).elim

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : a ∈ (k * c * k⁻¹).support
⊢ c (k⁻¹ a) = g (k⁻¹ a)

Tactic:
apply hc

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
a : α
ha : a ∈ (k * c * k⁻¹).support
⊢ k⁻¹ a ∈ c.support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ (g * g).IsThreeCycle

Tactic:
rw [← pow_two, ← card_support_eq_three_iff, support_pow_coprime, ht.card_support]
  rw [ht.orderOf]
  norm_num

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommSemiring R
M : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis (ιM i) R (M i)
h : ∀ (v : (i : ι) → ιM i), (f fun i ↦ (e i) (v i)) = g fun i ↦ (e i) (v i)
⊢ f = g

Tactic:
cases nonempty_fintype ι
  classical
  ext m
  rcases Function.Surjective.piMap (fun i ↦ (e i).repr.symm.surjective) m with ⟨x, rfl⟩
  unfold Pi.map
  simp_rw [(e _).repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum,
    map_sum_finset, map_smul_univ, h]

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
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₂
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
f : (i : ι) → M₁ i →ₗ[R] M₁' i
hf : ∀ (i : ι), Surjective ⇑(f i)
g₁ g₂ : MultilinearMap R M₁' M₂
h : (fun g ↦ g.compLinearMap f) g₁ = (fun g ↦ g.compLinearMap f) g₂
x : (i : ι) → M₁' i
⊢ g₁ x = g₂ x

Tactic:
simpa [fun i => surjInv_eq (hf i)]
      using MultilinearMap.ext_iff.mp h fun i => surjInv (hf i) (x i)

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x✝ : ↑(colimitCocone F).pt
x : Prequotient F
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) x) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x)

Tactic:
induction x with
    | zero => simp
    | one => simp
    | neg x ih => simp [ih]
    | of j x =>
      exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
    | add x y ih_x ih_y => simp [ih_x, ih_y]
    | mul x y ih_x ih_y => simp [ih_x, ih_y]

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)
h : ∀ {s t : ℤˣ}, detp s A * detp t B = ∑ σ ∈ ofSign s, ∑ τ ∈ ofSign (t * s), ∏ k, A k (σ k) * B (σ k) (τ k)
ι : 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)) ⋯)
s : ℤˣ
⊢ ∑ y, ∑ x ∈ ofSign s, ∏ i, A i (y i) * B (y i) (x i) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) +
      (∑ x ∈ ofSign 1, ∑ x_1 ∈ ofSign s, ∏ k, A k (x k) * B (x k) (x_1 k) +
        ∑ x ∈ ofSign (-1), ∑ x_1 ∈ ofSign s, ∏ k, A k (x k) * B (x k) (x_1 k))

Tactic:
← sum_compl_add_sum bij,

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)
h : ∀ {s t : ℤˣ}, detp s A * detp t B = ∑ σ ∈ ofSign s, ∑ τ ∈ ofSign (t * s), ∏ k, A k (σ k) * B (σ k) (τ k)
ι : 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)) ⋯)
s : ℤˣ
⊢ ∑ i ∈ bijᶜ, ∑ x ∈ ofSign s, ∏ i_1, A i_1 (i i_1) * B (i i_1) (x i_1) +
      ∑ i ∈ bij, ∑ x ∈ ofSign s, ∏ i_1, A i_1 (i i_1) * B (i i_1) (x i_1) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) +
      (∑ x ∈ ofSign 1, ∑ x_1 ∈ ofSign s, ∏ k, A k (x k) * B (x k) (x_1 k) +
        ∑ x ∈ ofSign (-1), ∑ x_1 ∈ ofSign s, ∏ k, A k (x k) * B (x k) (x_1 k))
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x✝ : ↑(colimitCocone F).pt
x : Prequotient F
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) x) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x)

Tactic:
induction x with
    | zero => simp
    | one => simp
    | neg x ih => simp [ih]
    | of j x =>
      exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
    | add x y ih_x ih_y => simp [ih_x, ih_y]
    | mul x y ih_x ih_y => simp [ih_x, ih_y]

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

Goal state before:
pp: 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) := ⋯
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) := ⋯
C : (a : ι) → Finset (α a) := ⋯
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
i : ι
hi : i = i₀
⊢ A i₀ ∪ {j₂} = A i₀

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

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
⊢ g ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) =
    h ≫
      coeqHom f g ≫
        leftToMax (coeq f g) (coeq g h) ≫
          coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))

Tactic:
slice_rhs 2 4 => rw [← Category.assoc, coeq_condition _ _]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
⊢ g ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) =
    h ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : c.IsColimit
⊢ Nonempty (Limits.IsColimit (F.coconeTypesEquiv c))

Tactic:
exact
     ⟨{ desc s := ↾fun x => hc.desc (F.coconeTypesEquiv.symm s) x
        fac s j := by
          ext x
          exact congr_fun (hc.fac (F.coconeTypesEquiv.symm s) j) x
        uniq s m hm := by
          ext x
          exact congr_fun (hc.funext fun j ↦ funext fun y ↦ by simp [← hm j]) x }⟩

Goal state after:
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
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
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (σ x).2 = x.2
k : n
x : o
hkx : ¬(σ (k, x)).2 = (k, x).2
⊢ blockDiagonal M (σ (k, x)) (k, x) = 0

Tactic:
rw [blockDiagonal_apply_ne]

Goal state after:
case h
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
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (σ x).2 = x.2
k : n
x : o
hkx : ¬(σ (k, x)).2 = (k, x).2
⊢ (σ (k, x)).2 ≠ x
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_4
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ ∀ a ∈ univ,
    (↑↑(sign a.1) * ∏ i, A (a.1 i) i) * (↑↑(sign a.2) * ∏ i, D (a.2 i) i) =
      ↑↑(sign (a.1.sumCongr a.2)) * ∏ i, fromBlocks A B 0 D ((a.1.sumCongr a.2) i) i

Tactic:
simp only [forall_prop_of_true, Prod.forall, mem_univ]
        intro σ₁ σ₂
        rw [Fintype.prod_sum_type]
        simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁,
          fromBlocks_apply₂₂]
        rw [mul_mul_mul_comm]
        congr
        rw [sign_sumCongr, Units.val_mul, Int.cast_mul]

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✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s✝ : Finset ι
j : ι
s : Finset ι
j_notMem_s : j ∉ s
Hrec : f (s.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ s, c i) • f m
i : ι
h : i = j
⊢ update (s.piecewise (fun i ↦ c i • m i) m) j (m j) i = s.piecewise (fun i ↦ c i • m i) m i

Tactic:
rw [h]
      simp [j_notMem_s]

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 : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j

Tactic:
rw [if_pos hjs]

Goal state after:
case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    if j < i then a j else if j = i then a j - b j else b j
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
⊢ { obj := fun X ↦ (X✝.obj X.1).obj X.2, map := fun {X Y} f ↦ (X✝.map f.1).app X.2 ≫ (X✝.obj Y.1).map f.2, map_id := ⋯,
            map_comp := ⋯ }.map
        f ≫
      (T.app Y.1).app Y.2 =
    (T.app X.1).app X.2 ≫
      { obj := fun X ↦ (Y✝.obj X.1).obj X.2, map := fun {X Y} f ↦ (Y✝.map f.1).app X.2 ≫ (Y✝.obj Y.1).map f.2,
            map_id := ⋯, map_comp := ⋯ }.map
        f

Tactic:
by
        simp only [Category.assoc]
        slice_lhs 2 3 => rw [NatTrans.naturality]
        slice_lhs 1 2 => rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]
        rw [Category.assoc]

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
hc : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.unop = (Quiver.Hom.op ((hom ((hc (unop s.pt)).lift ((yoneda.obj (unop s.pt)).mapCone s))) (𝟙 (unop s.pt)))).unop

Tactic:
by
    apply (Types.isLimitEquivSections (hc s.pt.unop)).injective
    ext j
    have eq := congr_hom ((hc s.pt.unop).fac ((yoneda.obj s.pt.unop).mapCone s) j) (𝟙 (unop s.pt))
    dsimp [Types.isLimitEquivSections, Types.sectionOfCone]
    simp_all [← hm]

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

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
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesLimit K₁ F
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c) :=
  (IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ (c.π.app j ≫ F.map (h.inv.app j)) ≫ F.map (h.hom.app j) = 𝟙 c.pt ≫ c.π.app j

Tactic:
rw [Category.assoc, ← F.map_comp]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesLimit K₁ F
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c) :=
  (IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ c.π.app j ≫ F.map (h.inv.app j ≫ h.hom.app j) = 𝟙 c.pt ≫ c.π.app j
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 t
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
J : Type w
inst✝ : Category.{r, w} J
F : J ⥤ C
D : Cocone F
i j : J
x : ToType (F.obj i)
y : ToType (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
k : J
f : i ⟶ k
g : j ⟶ k
hfg : (ConcreteCategory.hom ((F ⋙ forget C).map f)) x = (ConcreteCategory.hom (F.map g)) y
h1 : (F ⋙ forget C).map f ≫ E.ι.app k = E.ι.app i := E.ι.naturality f
⊢ (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y

Tactic:
let h2 : (F ⋙ forget C).map g ≫ E.ι.app k = E.ι.app j := E.ι.naturality g

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
J : Type w
inst✝ : Category.{r, w} J
F : J ⥤ C
D : Cocone F
i j : J
x : ToType (F.obj i)
y : ToType (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
k : J
f : i ⟶ k
g : j ⟶ k
hfg : (ConcreteCategory.hom ((F ⋙ forget C).map f)) x = (ConcreteCategory.hom (F.map g)) y
h1 : (F ⋙ forget C).map f ≫ E.ι.app k = E.ι.app i := E.ι.naturality f
h2 : (F ⋙ forget C).map g ≫ E.ι.app k = E.ι.app j := E.ι.naturality g
⊢ (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
⊢ (s : Cone F) →
    s.pt ⟶
      {
            liftedCone :=
              { pt := of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
                π := { app := fun j ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ } },
            validLift :=
              Cone.ext ((Types.isLimitEquivSections t).trans (equivShrink ↑(F ⋙ forget MonCat).sections)).symm.toIso
                ⋯ }.liftedCone.pt

pp: case refine_2.refine_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
⊢ ∀ (s : Cone F),
    (forget MonCat).map (?refine_2.refine_1 s) =
      (Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s)

Tactic:
· intro _
    refine ofHom
      { toFun := (Types.Small.limitConeIsLimit.{v, u} _).lift ((forget MonCat).mapCone _),
        map_one' := by simp; rfl, map_mul' := ?_ }
    · intro x y
      simp only [Types.Small.limitCone_pt, Functor.comp_obj, Functor.mapCone_pt,
        Types.Small.limitConeIsLimit_lift, Functor.const_obj_obj, Functor.mapCone_π_app,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, map_mul]
      rw [← equivShrink_mul]
      rfl

Goal state after:
case refine_2.refine_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
⊢ ∀ (s : Cone F),
    (forget MonCat).map
        (ofHom
          {
            toFun :=
              ⇑(ConcreteCategory.hom
                  ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s))),
            map_one' := ⋯, map_mul' := ⋯ }) =
      (Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s)
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: 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.Full
inst✝ : R.Faithful
⊢ IsIso (whiskerRight h.unit L)

Tactic:
by
  have := h.left_triangle
  rw [← IsIso.eq_comp_inv] at this
  rw [this]
  infer_instance

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

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
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ adj.unit.app (𝟙_ C) = adj.unit.app (𝟙_ C) ≫ G.map (η F) ≫ G.map (ε F)

Tactic:
Monoidal.map_η_ε

Goal state after:
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
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ adj.unit.app (𝟙_ C) = adj.unit.app (𝟙_ C) ≫ 𝟙 (G.obj (F.obj (𝟙_ C)))
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: C✝ : Type u
inst✝¹⁰ : Category.{v, u} C✝
FC✝ : C✝ → C✝ → Type u_1
CC✝ : C✝ → Type w
inst✝⁹ : (X Y : C✝) → FunLike (FC✝ X Y) (CC✝ X) (CC✝ Y)
inst✝⁸ : ConcreteCategory C✝ FC✝
C : Type u
D : Type u'
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Category.{v', u'} D
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
FD : D → D → Type u_3
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).PreservesMonomorphisms
⊢ (forget₂ C D ⋙ forget D).PreservesMonomorphisms

Tactic:
by
    simp only [HasForget₂.forget_comp]
    infer_instance

Goal state after: