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

Goal state before:
pp: K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
⊢ ∀ (b_1 : B ⊗[K] C), b_1 * includeLeft b = includeLeft b * b_1

Tactic:
intro bc

Goal state after:
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
bc : B ⊗[K] C
⊢ bc * includeLeft b = includeLeft b * bc
Module: Mathlib.Algebra.Central.TensorProduct

Goal state before:
pp: K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
⊢ ∀ (b : B ⊗[K] C), b * includeRight c = includeRight c * b

Tactic:
intro bc

Goal state after:
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
bc : B ⊗[K] C
⊢ bc * includeRight c = includeRight c * bc
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
f : ι → M
t : Finset κ
inst✝ : DecidableEq ι
m : κ → ι
hm : Set.InjOn m ↑t
⊢ (↑(#t))⁻¹ • ∑ x ∈ image m t, f x = (↑(#t))⁻¹ • ∑ x ∈ t, f (m x)

Tactic:
sum_image hm

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

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i

Tactic:
rw [expect, ← Nat.cast_smul_eq_nsmul ℚ≥0, smul_inv_smul₀]
    exact mod_cast hs.card_ne_zero

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

Goal state before:
pp: case i_inj
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a₁ ∈ range k, ∀ a₂ ∈ range k, ((p ↑a₁).2, (p ↑a₁.succ).1) = ((p ↑a₂).2, (p ↑a₂.succ).1) → a₁ = a₂

Tactic:
intro i hi j hj hij
    rw [mem_range] at hi hj
    apply F.intervalGapsWithin_injOn h a b <;> grind

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
inst : Fintype (Sym2 α)
⊢ univ.sym2 = univ

Tactic:
ext
  simp only [mem_sym2_iff, mem_univ, implies_true]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
inst✝ : LT M
⊢ ∑ i ∈ s, f i < ⊤ ↔ ∀ i ∈ s, f i < ⊤

Tactic:
simp [WithTop.lt_top_iff_ne_top]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
w : α
hw : w ∈ s
⊢ g w = f w

Tactic:
simp [hw, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
w : α
hw : w ∈ s
⊢ f w = g w

Tactic:
simp [hw, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := fun p H ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq✝ : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
⊢ f p.1 ⋯ = f q.1 ⋯ ∧ f p.2 ⋯ = f q.2 ⋯ ∨ (f p.1 ⋯, f p.2 ⋯) = (f q.1 ⋯, f q.2 ⋯).swap

Tactic:
Prod.swap_prod_mk

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := fun p H ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq✝ : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
⊢ f p.1 ⋯ = f q.1 ⋯ ∧ f p.2 ⋯ = f q.2 ⋯ ∨ (f p.1 ⋯, f p.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
a✝ b✝ : Push σ
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ reverse (reverse (PushQuiver.arrow f)) = PushQuiver.arrow f

Tactic:
by dsimp [reverse]; congr; apply h.inv'

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

Goal state before:
pp: case mp
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ IsIso f → ∀ (i : I), IsIso (f i)

pp: case mpr
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ (∀ (i : I), IsIso (f i)) → IsIso f

Tactic:
· intro _ i
    exact (Pi.isoApp (asIso f) i).isIso_hom

Goal state after:
case mpr
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ (∀ (i : I), IsIso (f i)) → IsIso f
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (i : I), IsIso (f i)

Tactic:
constructor
  · intro _ i
    exact (Pi.isoApp (asIso f) i).isIso_hom
  · intro
    exact ⟨fun i => inv (f i), by cat_disch, by cat_disch⟩

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z✝ : C
g h : Y ⟶ Z✝
w : se.section_ ≫ f ≫ g = se.section_ ≫ f ≫ h
⊢ g = h

Tactic:
simpa using w

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⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
h : Epi (f ≫ g)
⊢ Epi f
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: X Y : Type u
⊢ Function.LeftInverse (fun f ↦ { toFun := f }) fun f ↦ ⇑f

Tactic:
intro; rfl

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

Goal state before:
pp: X Y : Type u
⊢ Function.RightInverse (fun f ↦ { toFun := f }) fun f ↦ ⇑f

Tactic:
intro; rfl

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

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
F : C ⥤ D
G : D ⥤ E
inst✝ : F.IsEquivalence
⊢ (F ⋙ G).IsLeftAdjoint ↔ G.IsLeftAdjoint

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩

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
F : C ⥤ D
G : D ⥤ E
inst✝ : F.IsEquivalence
h : (F ⋙ G).IsLeftAdjoint
⊢ G.IsLeftAdjoint
Module: Mathlib.CategoryTheory.Adjunction.Basic

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
F : C ⥤ D
G : D ⥤ E
inst✝ : F.IsEquivalence
⊢ (F ⋙ G).IsRightAdjoint ↔ G.IsRightAdjoint

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩

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
F : C ⥤ D
G : D ⥤ E
inst✝ : F.IsEquivalence
h : (F ⋙ G).IsRightAdjoint
⊢ G.IsRightAdjoint
Module: Mathlib.CategoryTheory.Adjunction.Basic

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
F : C ⥤ D
G : D ⥤ E
inst✝ : G.IsEquivalence
⊢ (F ⋙ G).IsLeftAdjoint ↔ F.IsLeftAdjoint

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩

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
F : C ⥤ D
G : D ⥤ E
inst✝ : G.IsEquivalence
h : (F ⋙ G).IsLeftAdjoint
⊢ F.IsLeftAdjoint
Module: Mathlib.CategoryTheory.Adjunction.Basic

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
F : C ⥤ D
G : D ⥤ E
inst✝ : G.IsEquivalence
⊢ (F ⋙ G).IsRightAdjoint ↔ F.IsRightAdjoint

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩

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
F : C ⥤ D
G : D ⥤ E
inst✝ : G.IsEquivalence
h : (F ⋙ G).IsRightAdjoint
⊢ F.IsRightAdjoint
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (c : C), IsIso ((yoneda.map f).app (op c))

Tactic:
by
  rw [isIso_iff_yoneda_map_bijective]
  exact forall_congr' fun _ ↦ (bijective_iff_isIso_ofHom _)

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
F : C ⥤ Type v₁
t : F.obj X
⊢ coyonedaEquiv.symm ((ConcreteCategory.hom (F.map f)) t) = coyoneda.map f.op ≫ coyonedaEquiv.symm t

Tactic:
by
  obtain ⟨u, rfl⟩ := coyonedaEquiv.surjective t
  simp [coyonedaEquiv_naturality u f]

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

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i p
φ : mk i ⟶ mk p
sq : CommSq (Hom.left φ) i p (Hom.right φ)
⊢ Nonempty (LiftStruct φ)

Tactic:
exact ⟨{ l := sq.lift }⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝¹ : F.PreservesMonomorphisms
f : G ⟶ F
inst✝ : ∀ (X : C), Mono (f.app X)
X Y : C
π : X ⟶ Y
hπ : Mono π
⊢ Mono (G.map π ≫ f.app Y)

Tactic:
rw [f.naturality π]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝¹ : F.PreservesMonomorphisms
f : G ⟶ F
inst✝ : ∀ (X : C), Mono (f.app X)
X Y : C
π : X ⟶ Y
hπ : Mono π
⊢ Mono (f.app X ≫ F.map π)
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ sq.HasLift

Tactic:
rw [← sq.right_adjoint_hasLift_iff adj]

Goal state after:
case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ ⋯.HasLift
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✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
m :
  s.pt ⟶
    { pt := f default,
        π :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => eqToHom ⋯ }.pt
w :
  m ≫
      { pt := f default,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.π.app
        default =
    s.π.app default
⊢ m = s.π.app default

Tactic:
simpa using w

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal X
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) ↔ Nonempty (IsLimit (mk c.snd c.fst))

Tactic:
exact
    ⟨fun h => ⟨BinaryFan.isLimitFlip h.some⟩, fun h =>
      ⟨(BinaryFan.isLimitFlip h.some).ofIsoLimit (isoBinaryFanMk c).symm⟩⟩

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
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
⊢ IsColimit (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1)

Tactic:
refine Cofan.IsColimit.mk _ (fun t ↦ ?_) ?_ fun t m hm ↦ ?_

Goal state after:
case refine_1
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
t : Cofan fun p ↦ X p.1 p.2
⊢ (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).pt ⟶ t.pt

case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
⊢ ∀ (t : Cofan fun p ↦ X p.1 p.2) (j : ι × ι'),
    (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).inj j ≫ ?refine_1 = t.inj j

case refine_3
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
t : Cofan fun p ↦ X p.1 p.2
m : (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).pt ⟶ t.pt
hm : ∀ (j : ι × ι'), (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).inj j ≫ m = t.inj j
⊢ m = ?refine_1
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
w : 𝟙 t.pt ≫ t.π.app WalkingCospan.one = t.π.app WalkingCospan.left ≫ f
⊢ t.π.app WalkingCospan.one = t.fst ≫ f

Tactic:
simpa using w

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv = map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯

Tactic:
by
  ext <;> simp [Iso.inv_comp_eq]

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.Full
inst✝ : F.EssSurj
B : Over (F.obj X)
⊢ (post F).essImage B

Tactic:
obtain ⟨A', ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := F) B.left
    obtain ⟨f, hf⟩ := F.map_surjective (e.hom ≫ B.hom)
    exact ⟨Over.mk f, ⟨Over.isoMk e⟩⟩

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
f f' : CostructuredArrow S T
g : f.left ≅ f'.left
w : S.map g.hom ≫ f'.hom = f.hom
⊢ S.map g.hom ≫ f'.hom = f.hom ≫ (Functor.fromPUnit T).map (eqToIso ⋯).hom

Tactic:
simpa using w

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
⊢ I = J

Tactic:
by
  have : I.zero = J.zero := by
    funext X Y
    specialize w X Y
    apply congrArg Zero.mk w
  cases I; cases J
  congr
  · apply proof_irrel_heq
  · apply proof_irrel_heq

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
β : Type u'
inst✝¹ : HasZeroMorphisms C
f : β → C
inst✝ : HasLimit (Discrete.functor f)
b : β
⊢ IsSplitEpi (Pi.π f b)

Tactic:
classical exact IsSplitEpi.mk' { section_ := Pi.lift <| Pi.single b (𝟙 _) }

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
⊢ f ≫ Cofork.π c = g ≫ Cofork.π c

Tactic:
by rw [← sub_eq_zero, ← sub_comp, c.condition]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J✝ : Type v
inst✝ : HasFiniteColimits C
J : Type
x✝ : Finite J
⊢ HasColimitsOfShape (WidePushoutShape J) C

Tactic:
cases nonempty_fintype J; exact HasFiniteColimits.out _

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
⊢ Injective (@toMonoid M)

Tactic:
rintro ⟨⟩ ⟨⟩ h
  congr

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
⊢ Injective (@toLeftCancelMonoid M)

Tactic:
rintro ⟨⟩ ⟨⟩ h
  congr

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun j ↦ G.obj (f j)
i : IsIso (piComparison G f)
⊢ IsLimit (Fan.mk (G.obj (∏ᶜ f)) fun j ↦ G.map (Pi.π f j))

Tactic:
exact @IsLimit.ofPointIso _ _ _ _ _ _ _
    (limit.isLimit (Discrete.functor fun j : J => G.obj (f j))) i

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).inv = lift prod.fst prod.snd

Tactic:
by
  ext <;> simp [Iso.inv_comp_eq]

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

Goal state before:
pp: J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D : Type uD
inst✝⁸ : Category.{uD', uD} D
inst✝⁷ : HasZeroMorphisms D
F : J✝¹ → C✝¹
J✝ : Type w
K✝ : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
⊢ components (matrix m) = m

Tactic:
ext
    apply biproduct.matrix_components

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
r : R
⊢ r • 0 = 0

Tactic:
by rw [smul_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j : Fin n
hab : q < q.succAbove j
⊢ q ≤ j.castSucc

Tactic:
simpa [lt_succAbove_iff_le_castSucc] using hab

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

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
⊢ HasBinaryBiproduct X X

Tactic:
convert! (inferInstance : HasBinaryBiproduct X X); subsingleton

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

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
⊢ HasBinaryBiproduct X X

Tactic:
convert! (inferInstance : HasBinaryBiproduct X X); subsingleton

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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
⊢ ∅.piAntidiag n = if n = 0 then {0} else ∅

Tactic:
split_ifs with hn <;> simp [*]

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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
⊢ ∅.finsuppAntidiag n = if n = 0 then {0} else ∅

Tactic:
split_ifs with hn <;> simp [*]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n a : ℕ
ha1 : 1 ≤ a
ha : a ≤ n
q : (n - a).Partition
⊢ (a ::ₘ q.parts).sum = n

Tactic:
simp [q.parts_sum, ha]

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

Goal state before:
pp: n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
⊢ _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))

Tactic:
wlog h' : i₁ < i₂

Goal state after:
case inr
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
this :
  ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin c.length},
    i₁ ≠ i₂ → i₁ < i₂ → _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
h' : ¬i₁ < i₂
⊢ _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))

n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
⊢ _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
exact ⟨hσ, σ.injective (h.trans hσ.symm)⟩

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

Goal state before:
pp: n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : ⟨n, c⟩.snd.blocks = ⟨n', c'⟩.snd.blocks
this : n = n'
⊢ ⟨n, c⟩ = ⟨n', c'⟩

Tactic:
induction this

Goal state after:
case refl
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : ⟨n, c⟩.snd.blocks = ⟨n, c'⟩.snd.blocks
⊢ ⟨n, c⟩ = ⟨n, c'⟩
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case right
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ (mapRange ⇑e ⋯ g).support ⊆ s

Tactic:
· exact subset_trans (support_mapRange) hsupp

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

Goal state before:
pp: case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length),
    (l.splitWrtCompositionAux ns)[i] = drop (take i ns).sum (take (take (i + 1) ns).sum l)
l : List α
i : ℕ
hi : i < (l.splitWrtCompositionAux (n :: ns)).length
⊢ (l.splitWrtCompositionAux (n :: ns))[i] = drop (take i (n :: ns)).sum (take (take (i + 1) (n :: ns)).sum l)

Tactic:
rcases i with - | i
    · simp
    · simp only [splitWrtCompositionAux, getElem_cons_succ, IH, take,
          sum_cons, splitAt_eq, drop_take, drop_drop]
      rw [Nat.add_sub_add_left]

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : Finite ↑{x | p x}
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ e.extendSubtype x = ↑(e ⟨x, hx⟩)

Tactic:
by
  simp [extendSubtype, subtypeCongr, sumCompl_symm_apply_of_pos hx]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith Equiv.swap l l').prod.support
⊢ x ∈ {x | (zipWith Equiv.swap l l').prod x ≠ x}

Tactic:
simpa using hx

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
⊢ x ∈ {x | l.formPerm x ≠ x}

Tactic:
simpa using hx

Goal state after: