mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ι) → DivisionRing (G i)
inst✝² : DivisionRing C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
x✝ : ℚ
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_ratCast _ _) i, mul_def, Rat.smul_def]

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: m n : ℕ
⊢ Ioo (-(↑m + 1)) (↑n + 1) = Ioo (-↑m) ↑n ∪ {-↑m, ↑n}

Tactic:
by
  ext
  simp only [mem_Ioo, union_insert, union_singleton, mem_insert]
  lia

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ i ∈ s with ¬Even (f i), f i % 2) % 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})

Tactic:
Finset.sum_filter

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ a ∈ s, if ¬Even (f a) then f a % 2 else 0) % 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})
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:
by 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:
by simp [mk_mem_sym2_iff]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.sym2 = ∅ ↔ s = ∅

Tactic:
exact sym2_eq_empty

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
⊢ (map g s).sym n = map { toFun := Sym.map ⇑g, inj' := ⋯ } (s.sym n)

Tactic:
by
  ext d
  simp only [mem_sym_iff, mem_map, Function.Embedding.coeFn_mk]
  refine ⟨fun hd ↦ ?_, fun ⟨b, hb, hd'⟩ d' hd ↦ ?_⟩
  · let g' : {x // x ∈ d} → α := fun ⟨x, hx⟩ ↦ (hd x hx).choose
    refine ⟨(fun p ↦ Sym.map g' p) d.attach, ?_, ?_⟩
    · simp only [Sym.mem_map, Sym.mem_attach, true_and, Subtype.exists, forall_exists_index, g']
      intro i e he hi
      rw [← hi]
      exact (hd e he).choose_spec.1
    · simp only [Sym.map_map, Function.comp_apply, g']
      convert! Sym.attach_map_coe d with ⟨x, hx⟩ hx'
      exact (hd x hx).choose_spec.2
  · rw [← hd', Sym.mem_map] at hd
    obtain ⟨a, ha, rfl⟩ := hd
    exact ⟨a, hb a ha, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
r : R
q : Q
⊢ ?m.148

Tactic:
let _ := I₂; exact r • q

Goal state after:
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
⊢ (∏ x ∈ s.erase i, f x) * f i = ⊤

Tactic:
refine WithTop.mul_eq_top_iff.mpr (Or.inl ⟨?_, hi'⟩)

Goal state after:
ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
⊢ ∏ x ∈ s.erase i, f x ≠ 0
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
P : α → Prop
f : α → β
z : Sym2 α
h : ∀ a ∈ z, P a
⊢ pmap (fun a x ↦ f a) z h = map f z

Tactic:
cases z; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
Q : β → Prop
f : α → β
g : (b : β) → Q b → γ
z : Sym2 α
h : ∀ b ∈ map f z, Q b
⊢ pmap g (map f z) h = pmap (fun a ha ↦ g (f a) ⋯) z ⋯

Tactic:
cases z; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : β → γ
z : Sym2 α
h : ∀ a ∈ z, P a
h' : ∀ b ∈ pmap f z h, Q b
⊢ map g (pmap f z h) = pmap (fun a ha ↦ g (f a ⋯)) z ⋯

Tactic:
cases z; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : (b : β) → Q b → γ
z : Sym2 α
h : ∀ a ∈ z, P a
h' : ∀ b ∈ pmap f z h, Q b
⊢ pmap g (pmap f z h) h' = pmap (fun a ha ↦ g (f a ⋯) ⋯) z ⋯

Tactic:
cases z; rfl

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
⊢ fromRel sym = Set.univ ↔ r = ⊤

Tactic:
refine ⟨fun h ↦ ?_, (· ▸ fromRel_top)⟩

Goal state after:
α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : fromRel sym = Set.univ
⊢ r = ⊤
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫ e.inverse.map (e.counit.app Y)

pp: case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))

Tactic:
rw [← e.unitInv_naturality]

Goal state after:
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.inverse.map (e.counit.app Y))) ≫ e.unitInv.app (e.inverse.obj Y)

case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
⊢ autoParam (∀ (X Y : Discrete I) (f : X ⟶ Y), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯) Functor.ext._auto_1

Tactic:
intro ⟨X⟩ ⟨Y⟩ ⟨⟨p⟩⟩; simp only at p; induction p; simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
⊢ NatTrans.op α.inv ≫ NatTrans.op α.hom = 𝟙 F.op

Tactic:
by ext; dsimp; rw [← op_comp]; rw [α.hom_inv_id_app]; rfl

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

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

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩
  simpa using (inferInstance : Epi ((f ≫ g) ≫ inv g))

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
s : Cone F
⊢ (limitCone h).extend (homOfCone h (coneOfHom h (homOfCone h s))) = coneOfHom h (homOfCone h s)

Tactic:
conv_lhs => simp only [homOfCone_coneOfHom]

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
s : Cone F
⊢ (limitCone h).extend (homOfCone h s) = coneOfHom h (homOfCone h s)
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
⊢ (λ_ (𝟙 a)).inv = (ρ_ (𝟙 a)).inv

Tactic:
by simp [Iso.inv_eq_inv]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ ∀ {X_1 Y : C ⥤ Type (max w v₁)} (f : X_1 ⟶ Y),
    ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).map f ≫
        (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation C (Type (max v₁ w)) ⋙
                  (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                    uliftFunctor.{u₁, max v₁ w}).obj
              X).map
          f

Tactic:
intros Y Z f
        ext g
        rw [← ULift.down_inj]
        simpa using uliftCoyonedaEquiv_comp _ _

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

Goal state before:
pp: J : Type w
x✝¹ x✝ : WidePullbackShape J
a b : x✝¹ ⟶ x✝
⊢ a = b

Tactic:
casesm* WidePullbackShape _, (_ : WidePullbackShape _) ⟶ (_ : WidePullbackShape _)

Goal state after:
case none.none.id.id
J : Type w
⊢ Hom.id none = Hom.id none

case some.none.term.term
J : Type w
b : J
⊢ Hom.term b = Hom.term b

case some.some.id.id
J : Type w
x✝ : J
⊢ Hom.id (some x✝) = Hom.id (some x✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case some
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
j : ι
⊢ k ≫ s.π.app (some j) = l ≫ s.π.app (some j)

Tactic:
· exact hπ j

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
E : Type u₃
inst✝⁴ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
A B : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))
inst✝ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)
⊢ prodComparison (F ⋙ G) A B = G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B)

Tactic:
by
  unfold prodComparison
  ext <;> simp [← G.map_comp]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ ∀ ⦃X_1 Y_1 : WalkingCospan⦄ (f_1 : X_1 ⟶ Y_1),
    (((Functor.const WalkingCospan).obj W).map f_1 ≫
        Option.casesOn Y_1 (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
      (Option.casesOn X_1 (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map f_1

Tactic:
rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) j <;> cases j

Goal state after:
case none.none.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (WidePullbackShape.Hom.id none) ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (WidePullbackShape.Hom.id none)

case some.left.none.term
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (term WalkingPair.left) ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (term WalkingPair.left)

case some.left.some.left.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (WidePullbackShape.Hom.id (some WalkingPair.left))

case some.right.none.term
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (term WalkingPair.right) ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (term WalkingPair.right)

case some.right.some.right.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (WidePullbackShape.Hom.id (some WalkingPair.right))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
s : PullbackCone g f
m : s.pt ⟶ t.pt
h₁ : m ≫ t.snd = s.fst
h₂ : m ≫ t.fst = s.snd
⊢ m = ht.lift s.flip

Tactic:
apply IsLimit.hom_ext ht

Goal state after:
case h₀
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
s : PullbackCone g f
m : s.pt ⟶ t.pt
h₁ : m ≫ t.snd = s.fst
h₂ : m ≫ t.fst = s.snd
⊢ m ≫ t.fst = ht.lift s.flip ≫ t.fst

case h₁
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
s : PullbackCone g f
m : s.pt ⟶ t.pt
h₁ : m ≫ t.snd = s.fst
h₂ : m ≫ t.fst = s.snd
⊢ m ≫ t.snd = ht.lift s.flip ≫ t.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    F.map f ≫ (WalkingParallelPair.casesOn Y zero one).hom = (WalkingParallelPair.casesOn X zero one).hom ≫ G.map f

Tactic:
by rintro _ _ ⟨_⟩ <;> simp [left, right]

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

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g f' g' : X ⟶ Y
hf : f = f'
hg : g = g'
⊢ (parallelPair f g).map right ≫ (Iso.refl ((parallelPair f g).obj one)).hom =
    (Iso.refl ((parallelPair f g).obj zero)).hom ≫ (parallelPair f' g').map right

Tactic:
simp [hg]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ Mono (preComp f g)

Tactic:
by
  refine @mono_of_mono _ _ _ _ _ _ (image.ι g) ?_
  simp only [image.preComp_ι]
  infer_instance

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

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g✝ f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h
hc : IsLimit c
⊢ ∀ (s_1 : Fork (h ≫ f) (h ≫ g)), liftPrecomp h hs hc s_1 ≫ (precompFork h s c).ι = s_1.ι

Tactic:
by simp [liftPrecomp, precompFork]

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
inst✝¹ : HasCokernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasCokernel f'
p : X ≅ X'
q : Y ≅ Y'
w : f ≫ q.hom = p.hom ≫ f'
⊢ f' ≫ q.inv = p.inv ≫ f

Tactic:
by
          refine (cancel_mono q.hom).1 ?_
          simp [w]

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
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
⊢ G.map (kernel.ι f) ≫ G.map f = 0

Tactic:
simp only [← G.map_comp, kernel.condition, Functor.map_zero]

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

Goal state before:
pp: case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
as✝ : J
⊢ t.ι as✝ ≫ ∑ j, t.π j ≫ t.ι j = t.ι as✝ ≫ 𝟙 t.pt

Tactic:
comp_sum,

Goal state after:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
as✝ : J
⊢ ∑ j, t.ι as✝ ≫ t.π j ≫ t.ι j = t.ι as✝ ≫ 𝟙 t.pt
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
j : Discrete J
⊢ t.toCocone.ι.app j ≫ ∑ j, t.π j ≫ t.ι j = t.toCocone.ι.app j ≫ 𝟙 t.pt

Tactic:
classical
      cases j
      simp_rw [Bicone.toCocone_ι_app, comp_sum, ← Category.assoc, t.ι_π, dite_comp]
      simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
inst✝ : HasFiniteBiproducts C
f g : J → C
h : (j : J) → f j ⟶ g j
⊢ map h = ∑ j, π f j ≫ h j ≫ ι g j

Tactic:
by
  classical
  ext
  simp [biproduct.ι_π, biproduct.ι_π_assoc, sum_comp, comp_dite, dite_comp]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
r : R
⊢ (forget₂ (ModuleCat R) AddCommGrpCat).map f ≫ N.smul r = M.smul r ≫ (forget₂ (ModuleCat R) AddCommGrpCat).map f

Tactic:
by
  ext x
  exact (f.hom.map_smul r x).symm

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
h : p ≠ last n
x : { x // x ≠ p }
⊢ some ((finSuccAboveEquiv p).symm x) = some ((p.castLT ⋯).predAbove ↑x)

Tactic:
simpa [finSuccAboveEquiv, OrderIso.symm] using finSuccEquiv'_ne_last_apply h x.property

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
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl + biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst = 0

Tactic:
add_comp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
      (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst =
    0
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple 0 ni.2))
      (map (fun i ↦ (i, n - i)) (range n ++ [n])) =
    [![n]]

Tactic:
List.map_append,

Goal state after:
n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple 0 ni.2))
      (map (fun i ↦ (i, n - i)) (range n) ++ map (fun i ↦ (i, n - i)) [n]) =
    [![n]]
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.boundary 0 = 0

Tactic:
by simp [boundary]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app j =
    (id (Iso.refl (F.obj b.pt))).hom ≫ (F.mapBinaryBicone b).toCone.π.app j

Tactic:
by
          rcases j with ⟨⟨⟩⟩ <;> simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesColimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).ι.app j ≫
      (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app j

Tactic:
by
          rcases j with ⟨⟨⟩⟩ <;> simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
s : Finset α
f : α → Perm β
comm : (↑s).Pairwise (Commute on f)
x : β
hx : ∀ a ∈ s, x ∉ (f a).support
⊢ x ∉ (s.noncommProd f comm).support

Tactic:
revert hx comm s
  apply Finset.induction
  · simp
  · intro a s ha ih comm hs
    rw [Finset.noncommProd_insert_of_notMem s a f comm ha]
    apply mt (Finset.mem_of_subset (support_mul_le _ _))
    rw [Finset.sup_eq_union, Finset.notMem_union]
    exact ⟨hs a (s.mem_insert_self a), ih (fun a ha ↦ hs a (Finset.mem_insert_of_mem ha))⟩

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

Goal state before:
pp: case pos
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ ↑(f ⟨σ x, ?pos.hx✝⟩) = τ (f.extendSubtype x)

pp: case pos.hx
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ σ x ∈ ↑σ.support

Tactic:
Equiv.extendSubtype_apply_of_mem

Goal state after:
case pos
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ ↑(f ⟨σ x, ?pos.hx✝⟩) = τ ↑(f ⟨x, ?pos.hx✝¹⟩)

case pos.hx
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ x ∈ ↑σ.support

case pos.hx
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ σ x ∈ ↑σ.support