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

Goal state before:
pp: case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
⊢ (f ^ n).IsCycle

Tactic:
refine hf'.of_pow fun x hx => ?_

Goal state after:
case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
x : β
hx : x ∈ (f ^ n).support
⊢ x ∈ ((f ^ n) ^ m).support
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
s : Set α
hs : s.Countable
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

Tactic:
obtain hs' | hs' := s.finite_or_infinite
  · refine ⟨hs'.toFinset.toList.formPerm, ?_, fun x hx => by
      simpa using List.mem_of_formPerm_apply_ne hx⟩
    convert! hs'.toFinset.nodup_toList.isCycleOn_formPerm
    simp
  · have := hs.to_subtype
    have := hs'.to_subtype
    obtain ⟨f⟩ : Nonempty (ℤ ≃ s) := inferInstance
    refine ⟨(Equiv.addRight 1).extendDomain f, ?_, fun x hx =>
      of_not_not fun h => hx <| Perm.extendDomain_apply_not_subtype _ _ h⟩
    convert! Int.addRight_one_isCycle.isCycleOn.extendDomain f
    rw [Set.image_comp, Equiv.image_eq_preimage_symm]
    ext
    simp

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
hind : iSupIndep fun i ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)
⊢ Function.Injective ⇑(noncommPiCoprod ϕ hcomm)

Tactic:
by
  apply (MonoidHom.ker_eq_bot_iff _).mp
  rw [eq_bot_iff]
  intro f heq1
  have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
    Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep _ _ (fun _ _ _ _ h => hcomm h _ _)
      _ hind (by simp) heq1
  ext i
  apply hinj
  simp [this i (Finset.mem_univ i)]

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

Goal state before:
pp: case neg
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
h : f x = x
y : α
hy : ¬f y = y
⊢ (if f.SameCycle x y then f y else y) = y

Tactic:
exact if_neg (mt SameCycle.apply_eq_self_iff (by tauto))

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
⊢ f ^ 1 = 1

Tactic:
← orderOf_dvd_iff_pow_eq_one

Goal state after:
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
⊢ orderOf f ∣ 1
Module: Mathlib.GroupTheory.Perm.Option

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
⊢ (removeNone σ).optionCongr x = (swap none (σ none) * σ) x

Tactic:
have : Option.map (⇑(removeNone σ)) x = (swap none (σ none)) (σ x) := by
    obtain - | x := x
    · simp
    · cases h : σ (some _)
      · simp [removeNone_none _ h]
      · have hn : σ (some x) ≠ none := by simp [h]
        have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)
        simp [removeNone_some _ ⟨_, h⟩, ← h, swap_apply_of_ne_of_ne hn hσn]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
this : Option.map (⇑(removeNone σ)) x = (swap none (σ none)) (σ x)
⊢ (removeNone σ).optionCongr x = (swap none (σ none) * σ) x
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
⊢ ∀ {x : α}, g x ≠ x → x ∈ l

Tactic:
by
        intro y hy; exact List.mem_of_ne_of_mem (fun h => hy (by rwa [h])) (hg hy)

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

Goal state before:
pp: n x : ℕ
hx : x < n + 2
⊢ (finRotate (n + 2) ^ ↑⟨x, hx⟩) 0 = ⟨x, hx⟩

Tactic:
Fin.ext_iff,

Goal state after:
n x : ℕ
hx : x < n + 2
⊢ ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ ¬(finRotate (n + 2) ^ x) 0 = Fin.last (n + 1)

Tactic:
Fin.ext_iff,

Goal state after:
case succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ ¬↑((finRotate (n + 2) ^ x) 0) = ↑(Fin.last (n + 1))
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case base_one
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ 0 = cycleType 1

Tactic:
cycleType_one

Goal state after:
case base_one
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ 0 = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : ↑(vectorsProdEqOne G (n + 1))
⊢ (↑v).toList.prod = 1

Tactic:
exact v.2

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : l.toFinset = f.cycleFactorsFinset
⊢ p ∈ l.toFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a

Tactic:
rw [eq_comm, cycleFactorsFinset_eq_list_toFinset hl] at hl'

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = f
⊢ p ∈ l.toFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
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 f' : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ f (update m i (x + y)) + f' (update m i (x + y)) =
    f (update m i x) + f' (update m i x) + (f (update m i y) + f' (update m i y))

Tactic:
by simp [add_left_comm, add_assoc]

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 : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
c : R
⊢ (c • A).IsDetpBalanced a b

Tactic:
by
  simp_rw [IsDetpBalanced, detp_smul, ← mul_assoc, mul_comm _ (c ^ _), mul_assoc,
    ← mul_add, h.mul_add_mul_eq]

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

Goal state before:
pp: n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
⊢ (A.submatrix f g).IsDetpBalanced a b

Tactic:
by_cases hf : f.Injective; swap
  · obtain ⟨p, q, eq, ne⟩ := Function.not_injective_iff.mp hf
    exact .of_eq (detp_eq_of_row_eq ne <| by ext; simp [eq])
  by_cases hg : g.Injective; swap
  · obtain ⟨p, q, eq, ne⟩ := Function.not_injective_iff.mp hg
    exact .of_eq (detp_eq_of_col_eq ne <| by ext; simp [eq])
  let f' := Equiv.ofBijective f <| (Fintype.bijective_iff_injective_and_card _).mpr
    ⟨hf, (Fintype.card_le_of_injective f hf).antisymm le⟩
  let g' := Equiv.ofBijective g <| (Fintype.bijective_iff_injective_and_card _).mpr
    ⟨hg, (Fintype.card_le_of_injective g hg).antisymm le⟩
  rwa [show f = f' by rfl, show g = g' by rfl, isDetpBalanced_submatrix_equiv_iff]

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
⊢ detp 1 (A * B) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    detp (-1) (A * B) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)

Tactic:
have hf {s t} {σ : Perm n} (hσ : σ ∈ ofSign s) :
      ofSign (t * s) = (ofSign t).map (mulRightEmbedding σ) := by
    ext τ
    simp_rw [mem_map, mulRightEmbedding_apply, ← eq_mul_inv_iff_mul_eq, exists_eq_right,
      mem_ofSign, map_mul, map_inv, mul_inv_eq_iff_eq_mul, mem_ofSign.mp hσ]

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)
⊢ detp 1 (A * B) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    detp (-1) (A * B) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)
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 : Matrix n n R
i j : n
h : i ≠ j
⊢ (adjp 1 A * A) i j = (adjp (-1) A * A) i j

Tactic:
simp_rw [← transpose_apply (_ * _) j i, transpose_mul,
    ← adjp_transpose, mul_adjp_apply_ne _ _ _ h.symm]

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
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
h : ∃ x, ¬x = τ (σ x)
⊢ IsAddUnit ((∏ k, A k (σ k)) * ∏ k, B k (τ k))

Tactic:
obtain ⟨k, hk⟩ := h

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
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
k : n
hk : ¬k = τ (σ k)
⊢ IsAddUnit ((∏ k, A k (σ k)) * ∏ k, B k (τ k))
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
f₃ : j₃ ⟶ k₁
g₃ : j₃ ⟶ k₂
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β

Tactic:
obtain ⟨s, α, β, H⟩ := crown ![j₁, j₂, j₃] (Fin.cons f₁ (Fin.cons f₂ (Fin.cons f₃ nofun)))
     (Fin.cons g₁ (Fin.cons g₂ (Fin.cons g₃ nofun)))

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
f₃ : j₃ ⟶ k₁
g₃ : j₃ ⟶ k₂
s : C
α : k₁ ⟶ s
β : k₂ ⟶ s
H :
  ∀ (i : Fin (Nat.succ 0).succ.succ),
    Fin.cons f₁ (Fin.cons f₂ (Fin.cons f₃ fun a ↦ nomatch a)) i ≫ α =
      Fin.cons g₁ (Fin.cons g₂ (Fin.cons g₃ fun a ↦ nomatch a)) i ≫ β
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β
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) := 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
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC : (fun i ↦ ∑ j ∈ A i, g i j) = update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)
Beq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i ↦ ∑ j ∈ B i, g i j
Ceq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i ↦ ∑ j ∈ C i, g i j
⊢ {j₂} ⊆ A i₀

Tactic:
simp [hj₂]

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
c : F.CoconeTypes
hc : Limits.IsColimit (F.coconeTypesEquiv c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : F.ColimitType → ULift.{u, 0} Bool := fun z ↦ { down := decide (x = z) }
this :
  ∀ (z : F.ColimitType),
    (ConcreteCategory.hom (hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f)))) (F.descColimitType c z) = f z
⊢ (ConcreteCategory.hom (hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f)))) (F.descColimitType c y) = f y

Tactic:
← this y

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : Limits.IsColimit (F.coconeTypesEquiv c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : F.ColimitType → ULift.{u, 0} Bool := fun z ↦ { down := decide (x = z) }
this :
  ∀ (z : F.ColimitType),
    (ConcreteCategory.hom (hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f)))) (F.descColimitType c z) = f z
⊢ (ConcreteCategory.hom (hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f)))) (F.descColimitType c y) =
    (ConcreteCategory.hom (hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f)))) (F.descColimitType c y)
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

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

Tactic:
rintro ⟨hc⟩
    classical
    refine ⟨⟨fun x y h ↦ ?_, fun x ↦ ?_⟩⟩
    · let f (z : F.ColimitType) : ULift.{u} Bool := ULift.up (x = z)
      suffices f x = f y by simpa [f] using this
      suffices ∀ z, hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f))
          (F.descColimitType c z) = f z by rw [← this x, h, ← this y]
      intro z
      obtain ⟨j, z, rfl⟩ := F.ιColimitType_jointly_surjective z
      exact ConcreteCategory.congr_hom (hc.fac _ j) z
    · let f₁ : (F.coconeTypesEquiv c).pt ⟶ (ULift.{u} Bool) :=
        ↾fun _ => ULift.up true
      let f₂ : (F.coconeTypesEquiv c).pt ⟶ (ULift.{u} Bool) :=
        ↾fun x => ULift.up (∃ a, F.descColimitType c a = x)
      suffices f₁ = f₂ by
        have := ConcreteCategory.congr_hom this x
        simpa [f₁, f₂] using this
      refine hc.hom_ext fun j => ?_
      ext x
      simpa [f₁, f₂] using ⟨F.ιColimitType j x, by simp⟩

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

Goal state before:
pp: case mp
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h : (hom (F.map f)) x = (hom (F.map g)) y
⊢ ∃ j f, (hom (F.map f)) x = (hom (F.map f)) y

Tactic:
refine ⟨IsFiltered.coeq f g, f ≫ IsFiltered.coeqHom f g, ?_⟩

Goal state after:
case mp
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h : (hom (F.map f)) x = (hom (F.map g)) y
⊢ (hom (F.map (f ≫ IsFiltered.coeqHom f g))) x = (hom (F.map (f ≫ IsFiltered.coeqHom f g))) y
Module: Mathlib.CategoryTheory.Limits.Preserves.Ulift

Goal state before:
pp: J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ Type u
x✝ : ↑(K ⋙ uliftFunctor.{v, u}).sections
u : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j
hu : u ∈ (K ⋙ uliftFunctor.{v, u}).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (K.map f)) ((fun j ↦ (u j).down) j) = (fun j ↦ (u j).down) j'

Tactic:
simp [← hu f]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: case refine_2
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
s : Cone F
r : R
x : ↑s.1
⊢ {
          toFun :=
            ⇑(ConcreteCategory.hom
                ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s))),
          map_add' := ⋯ }.toFun
      (r • x) =
    (RingHom.id R) r •
      {
            toFun :=
              ⇑(ConcreteCategory.hom
                  ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s))),
            map_add' := ⋯ }.toFun
        x

Tactic:
simp [← equivShrink_smul]

Goal state after:
case refine_2
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
s : Cone F
r : R
x : ↑s.1
⊢ ⟨fun j ↦ r • (ConcreteCategory.hom (s.π.app j)) x, ⋯⟩ = r • ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x, ⋯⟩
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝¹³ : Semiring R
C : Type u_2
D : Type u_3
inst✝¹² : Category.{v_1, u_2} C
inst✝¹¹ : Category.{v_2, u_3} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryTheory.Linear R C
inst✝⁷ : CategoryTheory.Linear R D
F : C ⥤ D
inst✝⁶ : Linear R F
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
inst✝⁴ : Preadditive E
inst✝³ : CategoryTheory.Linear R E
G : D ⥤ E
inst✝² : F.Full
inst✝¹ : F.EssSurj
inst✝ : Linear R (F ⋙ G)
X Y : D
r : R
X' Y' : C
eX : F.obj X' ≅ X
eY : F.obj Y' ≅ Y
f' : X' ⟶ Y'
⊢ G.map (r • eX.inv ≫ F.map f' ≫ eY.hom) = r • G.map (eX.inv ≫ F.map f' ≫ eY.hom)

Tactic:
simpa only [comp_map, map_smul, Linear.smul_comp, Linear.comp_smul, ← G.map_comp]
    using G.map eX.inv ≫= ((F ⋙ G).map_smul r f') =≫ G.map eY.hom

Goal state after:
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
⊢ ∀ (X : D) {Y Z : D} (r : R) (f : Y ⟶ Z), X ◁ (r • f) = r • X ◁ f

Tactic:
intro X Y Z r f

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
X Y Z : D
r : R
f : Y ⟶ Z
⊢ X ◁ (r • f) = r • X ◁ f
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case μ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
x✝¹ x✝ : C
⊢ μ F x✝¹ x✝ = μ F x✝¹ x✝

Tactic:
← cancel_mono (μIso F _ _).inv

Goal state after:
case μ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
x✝¹ x✝ : C
⊢ μ F x✝¹ x✝ ≫ (μIso F x✝¹ x✝).inv = μ F x✝¹ x✝ ≫ (μIso F x✝¹ x✝).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 Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ δ F (G.obj X ⊗ G.obj Y) (G.obj Z) ≫
      δ F (G.obj X) (G.obj Y) ▷ F.obj (G.obj Z) ≫
        (adj.counit.app X ⊗ₘ adj.counit.app Y) ▷ F.obj (G.obj Z) ≫ (X ⊗ Y) ◁ adj.counit.app Z ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))

Tactic:
← tensorHom_def_assoc,

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ δ F (G.obj X ⊗ G.obj Y) (G.obj Z) ≫
      δ F (G.obj X) (G.obj Y) ▷ F.obj (G.obj Z) ≫
        ((adj.counit.app X ⊗ₘ adj.counit.app Y) ⊗ₘ adj.counit.app Z) ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g

Tactic:
simp only [← G.map_comp, comm]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : ReflectsLimit (cospan f g) G
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g

Tactic:
simp only [← G.map_comp, comm]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ G.map f ≫ G.map h = G.map g ≫ G.map k

Tactic:
simp only [← G.map_comp, comm]

Goal state after: