mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Colimit.TensorProduct

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq :
  (directLimitLeft (Module.fgSystem R P) M)
      ((LinearMap.rTensor M (↑(Module.fgSystem.equiv R P).symm ∘ₗ (↑N).subtype)) x) =
    (directLimitLeft (Module.fgSystem R P) M)
      ((LinearMap.rTensor M (↑(Module.fgSystem.equiv R P).symm ∘ₗ (↑N).subtype)) y)
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Tactic:
← (LinearEquiv.eq_toLinearMap_symm_comp _ _).mpr
    (Module.fgSystem.equiv_comp_of N),

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq :
  (directLimitLeft (Module.fgSystem R P) M)
      ((LinearMap.rTensor M (Module.DirectLimit.of R { N // N.FG } (fun i ↦ ↥↑i) (Module.fgSystem R P) N)) x) =
    (directLimitLeft (Module.fgSystem R P) M)
      ((LinearMap.rTensor M (Module.DirectLimit.of R { N // N.FG } (fun i ↦ ↥↑i) (Module.fgSystem R P) N)) y)
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ι : Type u_3
P : ι → Submodule R M
inst✝¹ : Small.{u, u_3} ι
inst✝ : ∀ (i : ι), Small.{u, u_2} ↥(P i)
⊢ Small.{u, u_2} ↥(iSup P)

Tactic:
by
  classical
  rw [iSup_eq_range_dfinsupp_lsum]
  apply small_range

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
p m✝ : ℕ
s : Set (σ →₀ ℕ)
hs : IsUpperSet s
x y : MvPolynomial σ R
hy : y ∈ (restrictSupport R s).carrier
m : σ →₀ ℕ
hm : ¬∑ x_1 ∈ Finset.antidiagonal m, coeff x_1.1 x * coeff x_1.2 y = 0
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal m
e : coeff (i, j).1 x * coeff (i, j).2 y ≠ 0
⊢ m ∈ s

Tactic:
refine hs (by simp_all [eq_comm]) (hy (show j ∈ y.support by aesop))

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

Goal state before:
pp: R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
s : Set ℕ := {k | x ^ k = 0}
hx : 0 < sInf s
contra : ¬s.Nonempty
⊢ False

Tactic:
simp [not_nonempty_iff_eq_empty.mp contra] at hx

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

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

Tactic:
star_add,

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✝⁴ : Nonempty ι
inst✝³ : (i : ι) → AddMonoid (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)
inst✝¹ : (i : ι) → StarAddMonoid (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ ⟦⟨i, star x✝¹ + star x✝⟩⟧ = ⟦⟨i, star x✝¹⟩⟧ + ⟦⟨i, star x✝⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → DivisionSemiring (G i)
inst✝² : DivisionSemiring C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
x✝ : ℚ≥0
i : ι
x : G i
⊢ ⟦⟨⟨i, x⟩.fst, (fun x x_1 ↦ x✝ • x_1) ⟨i, x⟩.fst ⟨i, x⟩.snd⟩⟧ = (map₀ f fun x ↦ ↑x✝) * ⟦⟨i, x⟩⟧

Tactic:
simp_rw [map₀_def _ _ (fun _ _ _ ↦ map_nnratCast _ _) i, mul_def, NNRat.smul_def]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ ∏ m ∈ Icc (-↑(N + 1)) ↑(N + 1), f m = (∏ m ∈ range (N + 1 + 1), f ↑m) ^ 2 / f 0

Tactic:
| succ N ih =>

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b
⊢ ∏ x ∈ Ico (-↑b) ↑b ∪ {-(↑b + 1), ↑b}, f x / f (x + 1) = f (-(↑b + 1)) / f (↑b + 1)

Tactic:
rw [prod_union (by simp), prod_insert (by grind), prod_singleton, ihb, ← mul_assoc, mul_div]

Goal state after:
case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b
⊢ f (-↑b) / f ↑b * (f (-(↑b + 1)) / f (-(↑b + 1) + 1)) * f ↑b / f (↑b + 1) = f (-(↑b + 1)) / f (↑b + 1)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ ∏ t ∈ (insert a s).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t)

Tactic:
rw [powerset_insert, prod_union, prod_image]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ Set.InjOn (insert a) ↑s.powerset

α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ Disjoint s.powerset (image (insert a) s.powerset)
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
m : Multiset α
z : Sym2 α
a b : α
⊢ s(a, b) ∈ {z | z ∈ m.sym2} ↔ s(a, b) ∈ {x | x ∈ m}.sym2

Tactic:
simp [mk_mem_sym2_iff]

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

Goal state before:
pp: α : Type u_1
xs : List α
z : Sym2 α
a b : α
⊢ s(a, b) ∈ xs.sym2 ↔ ∀ y ∈ s(a, b), y ∈ xs

Tactic:
simp [mk_mem_sym2_iff]

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

Goal state before:
pp: α : Type u_1
xs : List α
z : Sym2 α
a b : α
⊢ s(a, b) ∈ {z | z ∈ xs.sym2} ↔ s(a, b) ∈ {x | x ∈ xs}.sym2

Tactic:
simp [mk_mem_sym2_iff]

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

Goal state before:
pp: α : Type u_1
x : α
xs : List α
h : x ∉ xs
⊢ (map (fun y ↦ s(x, y)) xs).Disjoint xs.sym2

Tactic:
by
  induction xs with
  | nil => simp
  | cons x' xs ih => aesop (add simp mk_mem_sym2_iff, unfold safe List.Disjoint)

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
⊢ Std.Irrefl r → ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬z.IsDiag

Tactic:
by intro ⟨h⟩; apply Sym2.ind; aesop

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : Algebra R S
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra S B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsScalarTower R S B
inst✝⁴ : IsPushout R S A B
M : Type u_10
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : S
m : M
⊢ (cancelBaseChangeAux R S A B M).symm (s ⊗ₜ[R] m) = (algebraMap S B) s ⊗ₜ[A] m

Tactic:
by
  simp [IsPushout.cancelBaseChangeAux, IsPushout.equiv_tmul]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case refine_1
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.length ≠ 0
⊢ ∃ c p' e, p = p'.cons e

Tactic:
cases p with

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Z : C
f : W ⟶ X
h' : X = Z
g : W ⟶ Z
⊢ f = eqToHom ⋯ ≫ g ≫ eqToHom ⋯ ↔ f ≍ g

Tactic:
cases h'

Goal state after:
case refl.refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X : C
f g : W ⟶ X
⊢ f = eqToHom ⋯ ≫ g ≫ eqToHom ⋯ ↔ f ≍ g
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₂
inst✝¹ : (i : I) → Category.{v₂, u₂} (D i)
F✝ G✝ : (i : I) → C i ⥤ D i
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F G : E ⥤ ((i : I) → C i)
τ : (i : I) → F ⋙ Pi.eval C i ⟶ G ⋙ Pi.eval C i
x✝¹ x✝ : E
f : x✝¹ ⟶ x✝
i : I
⊢ (F.map f ≫ fun i ↦ (τ i).app x✝) i = ((fun i ↦ (τ i).app x✝¹) ≫ G.map f) i

Tactic:
exact (τ i).naturality f

Goal state after:
Module: Mathlib.CategoryTheory.Conj

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : End X
⊢ α.symm.conj (α.conj f) = f

Tactic:
rw [← trans_conj, α.self_symm_id, refl_conj]

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
s t : Cone F
h : IsLimit t
f f' : s ⟶ t
⊢ ∀ {g : s ⟶ t}, g = h.liftConeMorphism s

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

Goal state after:
Module: Mathlib.CategoryTheory.Skeletal

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
⊢ ∀ (a₁ b₁ a₂ b₂ : C), a₁ ≈ a₂ → b₁ ≈ b₂ → Nonempty (a₁ ⟶ b₁) = Nonempty (a₂ ⟶ b₂)

Tactic:
rintro _ _ _ _ ⟨i₁⟩ ⟨i₂⟩

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
a₁✝ b₁✝ a₂✝ b₂✝ : C
i₁ : a₁✝ ≅ a₂✝
i₂ : b₁✝ ≅ b₂✝
⊢ Nonempty (a₁✝ ⟶ b₁✝) = Nonempty (a₂✝ ⟶ b₂✝)
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
φ : Arrow C → (s : C) × (t : C) × (s ⟶ t) := fun f ↦ ⟨f.left, ⟨f.right, f.hom⟩⟩
s t : C
f : (𝟭 C).obj s ⟶ (𝟭 C).obj t
s' t' : C
f' : (𝟭 C).obj s' ⟶ (𝟭 C).obj t'
h : φ { left := s, right := t, hom := f } = φ { left := s', right := t', hom := f' }
⊢ { left := s, right := t, hom := f } = { left := s', right := t', hom := f' }

Tactic:
obtain rfl : s = s' := congr_arg Sigma.fst h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
φ : Arrow C → (s : C) × (t : C) × (s ⟶ t) := fun f ↦ ⟨f.left, ⟨f.right, f.hom⟩⟩
s t : C
f : (𝟭 C).obj s ⟶ (𝟭 C).obj t
t' : C
f' : (𝟭 C).obj s ⟶ (𝟭 C).obj t'
h : φ { left := s, right := t, hom := f } = φ { left := s, right := t', hom := f' }
⊢ { left := s, right := t, hom := f } = { left := s, right := t', hom := f' }
Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
⊢ ∀ {g_1 : R ⟶ Y} (sq : CommSq u g z g_1), sq.HasLift

Tactic:
v

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
⊢ ∀ (sq : CommSq u g z v), sq.HasLift
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
⊢ x ⟶ h.inverse.obj { as := PUnit.unit }

Tactic:
convert! h.unit.app x

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (hI.to X)
I' X : C
hI' : IsInitial I'
⊢ Mono (hI'.to X)

Tactic:
rw [hI'.hom_ext (hI'.to X) ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)]
    apply mono_comp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : C
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (yoneda.obj X ⋙ (piConst.obj X).rightOp).map x✝ ≫ (Pi.lift id).op = (Pi.lift id).op ≫ (𝟭 Cᵒᵖ).map x✝

Tactic:
by apply Quiver.Hom.unop_inj; cat_disch

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : C
x✝ : Type v
⊢ (piConst.obj X).rightOp.map ({ app := fun n ↦ ↾fun i ↦ Pi.π (fun x ↦ X) i, naturality := ⋯ }.app x✝) ≫
      { app := fun Y ↦ (Pi.lift id).op, naturality := ⋯ }.app ((piConst.obj X).rightOp.obj x✝) =
    𝟙 ((piConst.obj X).rightOp.obj x✝)

Tactic:
by apply Quiver.Hom.unop_inj; cat_disch

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

Goal state before:
pp: case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
⊢ m = IsLimit.lift h (s.fst ≫ inv f) s.snd

Tactic:
apply BinaryFan.IsLimit.hom_ext h

Goal state after:
case uniq.h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
⊢ m ≫ c.fst = IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst

case uniq.h₂
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
⊢ m ≫ c.snd = IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryCoproduct W Y
inst✝ : HasBinaryCoproduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ desc (g ≫ inl) (g' ≫ inr) = map g g'

Tactic:
rw [← coprod.map_desc]; simp

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

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Over X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Over X
f : (post F).obj A ⟶ (post F).obj B
a : A.left ⟶ B.left
ha : F.map a = Hom.left f
⊢ ∃ a, (post F).map a = f

Tactic:
exact ⟨Over.homMk a (F.map_injective (by simp [ha, dsimp% f.w])), by cat_disch⟩

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

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
F : T ⥤ D
inst✝ : F.Faithful
A B : Under X
f g : A ⟶ B
h : (post F).map f = (post F).map g
⊢ Hom.right f = Hom.right g

Tactic:
exact F.map_injective (congrArg CommaMorphism.right h)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ IsIso (pushout.inl f g)

Tactic:
refine ⟨⟨pushout.desc (𝟙 _) (inv g ≫ f) (by simp), by simp, ?_⟩⟩
  ext
  · simp
  · simp [pushout.condition]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : F✝ ⋙ U ⟶ S ⋙ G✝
β✝ : G✝.obj T ⟶ V
F : C ≌ A
G : D ≌ B
α : F.functor ⋙ U ⟶ S ⋙ G.functor
α' : F.inverse ⋙ S ⟶ U ⋙ G.inverse
hα'α :
  S.leftUnitor.hom ≫ S.rightUnitor.inv ≫ S.whiskerLeft G.unitIso.hom ≫ (S.associator G.functor G.inverse).inv =
    Functor.whiskerRight F.unitIso.hom S ≫
      (F.functor.associator F.inverse S).hom ≫
        F.functor.whiskerLeft α' ≫ (F.functor.associator U G.inverse).inv ≫ Functor.whiskerRight α G.inverse
hαα' :
  F.inverse.whiskerLeft α ≫
      (F.inverse.associator S G.functor).inv ≫
        Functor.whiskerRight α' G.functor ≫ (U.associator G.inverse G.functor).hom ≫ U.whiskerLeft G.counitIso.hom =
    (F.inverse.associator F.functor U).inv ≫
      Functor.whiskerRight F.counitIso.hom U ≫ U.leftUnitor.hom ≫ U.rightUnitor.inv
β : G.functor.obj T ⟶ V
β' : G.inverse.obj V ⟶ T
hββ' : G.inverse.map β ≫ β' = G.unitIso.inv.app T
hβ'β : G.functor.map β' ≫ β = G.counitIso.hom.app V
⊢ G.functor.map β' ≫ β = G.counitIso.hom.app V ≫ 𝟙 ((𝟭 B).obj V)

Tactic:
simp [hβ'β]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
W'✝ : C
s : W'✝ ⟶ X'
hs : s ≫ g' = 0
m : W'✝ ⟶ c.pt
hm : m ≫ Fork.ι c ≫ e.hom = s
⊢ m ≫ Fork.ι c = hc.lift (ofι (s ≫ e.inv) ⋯) ≫ Fork.ι c

Tactic:
by simpa [← cancel_mono e.hom] using hm

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

Goal state before:
pp: case pos
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j j' : J
h : j = j'
⊢ F.map (b.ι j ≫ b.π j') = eqToHom ⋯

Tactic:
subst h
      simp only [bicone_ι_π_self, CategoryTheory.Functor.map_id, eqToHom_refl]; dsimp

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
i : Fin n
hlt : i.castSucc < q
this : q.succAbove i < q
⊢ f i < x

Tactic:
simpa using h this

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
i : Fin n
hlt : q ≤ i.castSucc
this : q < q.succAbove i
⊢ x < f i

Tactic:
simpa using h this

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
⊢ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ ofComponents g₁₁ g₁₂ g₂₁ g₂₂ =
    ofComponents (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂)

Tactic:
dsimp [Biprod.ofComponents]
  ext <;>
    simp only [add_comp, comp_add, add_zero, zero_add, biprod.inl_fst,
      biprod.inl_snd, biprod.inr_fst, biprod.inr_snd, biprod.inl_fst_assoc, biprod.inl_snd_assoc,
      biprod.inr_fst_assoc, biprod.inr_snd_assoc, comp_zero, zero_comp, Category.assoc]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case mpr
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
⊢ (s.sum f = n * m ∧ (∀ (i : ι), f i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ f i) →
    ∃ y, s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f

Tactic:
rintro ⟨hfsum, hfsup, hfdvd⟩

Goal state after:
case mpr
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
⊢ ∃ y, s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ ofSym (Sym.map (⇑e) s) = ofSym s

Tactic:
simp only [ofSym, Sym.val_eq_coe, Sym.coe_map, mk.injEq]

Goal state after:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ map (fun a ↦ count a (map ⇑e ↑s)) (map ⇑e ↑s).dedup = map (fun a ↦ count a ↑s) (↑s).dedup
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ ofSym (Sym.map (⇑e) s) = ofSym s

Tactic:
by
  simp only [ofSym, Sym.val_eq_coe, Sym.coe_map, mk.injEq]
  rw [Multiset.dedup_map_of_injective e.injective]
  simp only [map_map, Function.comp_apply]
  congr; funext i
  rw [← Multiset.count_map_eq_count' e _ e.injective]

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

Goal state before:
pp: α : Type u_1
f : Perm α
s : Set α
⊢ SurjOn (⇑f) s s → ∀ (n : ℕ), SurjOn (⇑(f ^ n)) s s

Tactic:
simp_rw [Equiv.Perm.coe_pow]; exact SurjOn.iterate

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

Goal state before:
pp: α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : σ a = a ∧ τ a = a
⊢ (σ * τ) a = a

Tactic:
rw [mul_apply, h.2, h.1]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (swap x (f x) * f) y ≠ y
⊢ f y ≠ y ∧ y ≠ x

Tactic:
simp only [swap_apply_def, mul_apply, f.injective.eq_iff] at *

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if f y = x then f x else if y = x then x else f y) ≠ y
⊢ f y ≠ y ∧ y ≠ x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : (∀ f ∈ l, f x = x) → l.prod x = x
hx : ∀ f_1 ∈ f :: l, f_1 x = x
⊢ (f :: l).prod x = x

Tactic:
| cons f l ih =>

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
this : ∀ (j : Fin c.length), j = i
⊢ c.length = 1

Tactic:
simpa using Fintype.card_eq_one_of_forall_eq this

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.boundaries → ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

Tactic:
intro hj

Goal state after:
case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
⊢ σ ∈ (sumCongrHom m n).range

Tactic:
have h1 : ∀ x : m ⊕ n, (∃ a : m, Sum.inl a = x) → ∃ a : m, Sum.inl a = σ x := by
    rintro _ ⟨a, rfl⟩; exact h ⟨a, rfl⟩
  have h3 : ∀ x : m ⊕ n, (∃ b : n, Sum.inr b = x) → ∃ b : n, Sum.inr b = σ x := by
    rintro _ ⟨b, rfl⟩; exact (perm_mapsTo_inl_iff_mapsTo_inr σ).mp h ⟨b, rfl⟩
  let σ₁' := subtypePermOfFintype σ h1
  let σ₂' := subtypePermOfFintype σ h3
  let σ₁ := permCongr (Equiv.ofInjective _ Sum.inl_injective).symm σ₁'
  let σ₂ := permCongr (Equiv.ofInjective _ Sum.inr_injective).symm σ₂'
  rw [MonoidHom.mem_range, Prod.exists]
  use σ₁, σ₂
  rw [Perm.sumCongrHom_apply]
  ext (a | b)
  · rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inl_injective, ofInjective_apply]
    rfl
  · rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inr_injective, ofInjective_apply]
    rfl

Goal state after: