mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Injective ⇑f → Injective ⇑(rTensor M f)
P : Type u
x✝⁴ : AddCommMonoid P
x✝³ : Module R P
x✝² : Module.Finite R P
x✝¹ : Submodule R P
x✝ : x✝¹.FG
⊢ Injective ⇑(rTensor M x✝¹.subtype)

Tactic:
have := Finite.small.{v'} R P

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Injective ⇑f → Injective ⇑(rTensor M f)
P : Type u
x✝⁴ : AddCommMonoid P
x✝³ : Module R P
x✝² : Module.Finite R P
x✝¹ : Submodule R P
x✝ : x✝¹.FG
this : Small.{v', u} P
⊢ Injective ⇑(rTensor M x✝¹.subtype)
Module: Mathlib.Algebra.Azumaya.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
⊢ (AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e)) =
    (↑(LinearEquiv.conjAlgEquiv R ↑e)).comp (AlgHom.mulLeftRight R A)

Tactic:
ext <;> simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
s : Finset α
⊢ s.dens ≤ 1

Tactic:
by
  cases isEmpty_or_nonempty α
  · simp [Subsingleton.elim s ∅]
  · simpa using dens_le_dens s.subset_univ

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ (s ∪ t).dens = s.dens + t.dens

Tactic:
← disjUnion_eq_union s t h,

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ (s.disjUnion t h).dens = s.dens + t.dens
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) = (↑(#(s ∩ t)) / ↑(#s)) • 𝔼 i ∈ s ∩ t, f i

Tactic:
obtain hst | hst := (s ∩ t).eq_empty_or_nonempty
  · simp [expect, hst]
  · simp [expect, smul_smul, ← inv_mul_eq_div, hst.card_ne_zero]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case e_6
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
this : ↑j ≠ last k
⊢ j < k.succ

Tactic:
lia

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

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝⁴ : Semifield K
inst✝³ : CharZero K
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → K
i : ι
⊢ ((↑(Fintype.card ι))⁻¹ • ∑ x, if i = x then ↑(Fintype.card ι) * f x else 0 * f x) = f i

Tactic:
zero_mul,

Goal state after:
ι : Type u_1
K : Type u_3
inst✝⁴ : Semifield K
inst✝³ : CharZero K
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → K
i : ι
⊢ ((↑(Fintype.card ι))⁻¹ • ∑ x, if i = x then ↑(Fintype.card ι) * f x else 0) = f i
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : ¬j = 0
this :
  a ≤ ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j - 1)).1 ∧
    ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j - 1)).1 ≤
        ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j - 1)).2 ∧
      ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j - 1)).2 ≤ b
⊢ j - 1 + 1 = j

Tactic:
lia

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

Goal state before:
pp: case mp
a b x : ℤ
⊢ (∃ a_1 < (b + 1 - a).toNat, a + ↑a_1 = x) → a ≤ x ∧ x ≤ b

Tactic:
lia

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

Goal state before:
pp: case h
a b x : ℤ
a✝ : a ≤ x ∧ x ≤ b
⊢ (x - a).toNat < (b + 1 - a).toNat ∧ a + ↑(x - a).toNat = x

Tactic:
lia

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

Goal state before:
pp: case mp
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + ↑a_1 = x) → a ≤ x ∧ x < b

Tactic:
lia

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

Goal state before:
pp: case h
a b x : ℤ
a✝ : a ≤ x ∧ x < b
⊢ (x - a).toNat < (b - a).toNat ∧ a + ↑(x - a).toNat = x

Tactic:
lia

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

Goal state before:
pp: case mp
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + 1 + ↑a_1 = x) → a < x ∧ x ≤ b

Tactic:
lia

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

Goal state before:
pp: case h
a b x : ℤ
a✝ : a < x ∧ x ≤ b
⊢ (x - (a + 1)).toNat < (b - a).toNat ∧ a + 1 + ↑(x - (a + 1)).toNat = x

Tactic:
lia

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

Goal state before:
pp: α : 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
⊢ -(↑N + 1) ≠ ↑N + 1

Tactic:
lia

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

Goal state before:
pp: case mp
a b x : ℤ
⊢ (∃ a_1 < (b - a - 1).toNat, a + 1 + ↑a_1 = x) → a < x ∧ x < b

Tactic:
lia

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

Goal state before:
pp: case h
a b x : ℤ
a✝ : a < x ∧ x < b
⊢ (x - (a + 1)).toNat < (b - a - 1).toNat ∧ a + 1 + ↑(x - (a + 1)).toNat = x

Tactic:
lia

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

Goal state before:
pp: m n : ℕ
a✝ : ℤ
⊢ -(↑m + 1) < a✝ ∧ a✝ ≤ ↑n + 1 ↔ a✝ = -↑m ∨ a✝ = ↑n + 1 ∨ -↑m < a✝ ∧ a✝ ≤ ↑n

Tactic:
lia

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

Goal state before:
pp: m n : ℕ
a✝ : ℤ
⊢ -(↑m + 1) < a✝ ∧ a✝ < ↑n + 1 ↔ a✝ = -↑m ∨ a✝ = ↑n ∨ -↑m < a✝ ∧ a✝ < ↑n

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R✝ : Type u_1
inst✝³⁵ : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝³⁴ : AddCommMonoid M₁✝
inst✝³³ : AddCommMonoid M₂✝
inst✝³² : AddCommMonoid M
inst✝³¹ : AddCommMonoid M'
inst✝³⁰ : Module R✝ M₁✝
inst✝²⁹ : Module R✝ M₂✝
inst✝²⁸ : Module R✝ M
inst✝²⁷ : Module R✝ M'
f✝ : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝²⁶ : AddCommMonoid N₁
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid N
inst✝²³ : Module R✝ N₁
inst✝²² : Module R✝ N₂
inst✝²¹ : Module R✝ N
g✝ : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid M₃
inst✝¹⁴ : AddCommMonoid M₁₂
inst✝¹³ : AddCommMonoid M₂₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module S M₂
inst✝⁹ : IsScalarTower R S M₂
inst✝⁸ : Module R M₃
inst✝⁷ : Module S M₃
inst✝⁶ : IsScalarTower R S M₃
inst✝⁵ : Module R M₁₂
inst✝⁴ : Module S M₁₂
inst✝³ : IsScalarTower R S M₁₂
inst✝² : Module R M₂₃
inst✝¹ : Module S M₂₃
inst✝ : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this✝ : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), s • y ⊗ₜ[R] x = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
x : M₂ ⊗[R] M₁
⊢ (↑(TensorProduct.comm R M₂ M₁)).toFun (s • x) = (RingHom.id S) s • (↑(TensorProduct.comm R M₂ M₁)).toFun x

Tactic:
induction x <;> simp_all [TensorProduct.smul_tmul']

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

Goal state before:
pp: α : Type u_1
m : Multiset α
a b : α
xs : List α
⊢ s(a, b) ∈ Multiset.sym2 ⟦xs⟧ ↔ a ∈ ⟦xs⟧ ∧ b ∈ ⟦xs⟧

Tactic:
by simp [List.mk_mem_sym2_iff]

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

Goal state before:
pp: case cons.inr.inl
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
c : α
hc : c ∈ xs
h : a = x ∧ b = c ∨ a = c ∧ b = x
⊢ a = x ∨ a ∈ xs

Tactic:
obtain (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) := h <;> simp [hc]

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

Goal state before:
pp: case nil
α : Type u_1
h : [].Nodup
⊢ [].sym2.Nodup

Tactic:
simp only [List.sym2, nodup_nil]

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

Goal state before:
pp: case refine_4
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ Sigma.map id (fun i a ↦ ↑a)
      ((fun m ↦ ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩)
        ((fun m ↦ ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩)) =
    Sigma.map id (fun i a ↦ ↑a) ⟨i, ⟨m, hm⟩⟩

Tactic:
refine Eq.trans ?_ (Sym.filter_ne_fill a _ ?_)

Goal state after:
case refine_4.refine_1
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ Sigma.map id (fun i a ↦ ↑a)
      ((fun m ↦ ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩)
        ((fun m ↦ ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩)) =
    Sym.filterNe a
      (Sym.fill a (Sigma.map id (fun i a ↦ ↑a) ⟨i, ⟨m, hm⟩⟩).fst (Sigma.map id (fun i a ↦ ↑a) ⟨i, ⟨m, hm⟩⟩).snd)

case refine_4.refine_2
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ a ∉ (Sigma.map id (fun i a ↦ ↑a) ⟨i, ⟨m, hm⟩⟩).snd
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mp.h
α : Type u_1
x y : α
hne : x ≠ y
x✝ y✝ : α
⊢ (x = x✝ ∨ x = y✝) ∧ y ∈ s(x✝, y✝) → s(x✝, y✝) = s(x, y)

Tactic:
mem_iff

Goal state after:
case mp.h
α : Type u_1
x y : α
hne : x ≠ y
x✝ y✝ : α
⊢ (x = x✝ ∨ x = y✝) ∧ (y = x✝ ∨ y = y✝) → s(x✝, y✝) = s(x, y)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ s(a, Mem.other' h) = z

Tactic:
by
  induction z
  aesop (add norm unfold [Sym2.rec, Quot.rec]) (rule_sets := [Sym2])

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
R : Type u_1
M✝ : Type v₁
N : Type v₂
S : Type v₃
inst✝⁵⁰ : AddCommMonoid M✝
inst✝⁴⁹ : AddCommMonoid N
inst✝⁴⁸ : CommSemiring R
inst✝⁴⁷ : CommSemiring S
inst✝⁴⁶ : Algebra R S
inst✝⁴⁵ : Module R M✝
inst✝⁴⁴ : Module R N
inst✝⁴³ : Module S N
inst✝⁴² : IsScalarTower R S N
f : M✝ →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝⁴¹ : AddCommMonoid P
inst✝⁴⁰ : Module R P
inst✝³⁹ : AddCommMonoid Q
inst✝³⁸ : Module S Q
inst✝³⁷ : Module R Q
inst✝³⁶ : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝³⁵ : CommSemiring T
inst✝³⁴ : Algebra R T
inst✝³³ : Algebra S T
inst✝³² : IsScalarTower R S T
inst✝³¹ : AddCommMonoid O
inst✝³⁰ : Module R O
inst✝²⁹ : Module S O
inst✝²⁸ : Module T O
inst✝²⁷ : IsScalarTower S T O
inst✝²⁶ : IsScalarTower R S O
inst✝²⁵ : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst✝²⁴ : CommSemiring R'
inst✝²³ : CommSemiring S'
inst✝²² : Algebra R R'
inst✝²¹ : Algebra S S'
inst✝²⁰ : Algebra R' S'
inst✝¹⁹ : Algebra R S'
inst✝¹⁸ : IsScalarTower R R' S'
inst✝¹⁷ : IsScalarTower R S 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
C : Type u_11
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
⊢ (cancelBaseChange R S A B C).symm 1 = 1

Tactic:
simp [TensorProduct.one_def]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : X ⟶ Z
g : Y ⟶ Z
H : α.inv ≫ f = g
⊢ f = α.hom ≫ g

Tactic:
by simp [H.symm]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
f : Z ⟶ Y
g : Z ⟶ X
H : f ≫ α.inv = g
⊢ f = g ≫ α.hom

Tactic:
by simp [H.symm]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
inst✝¹ : F.Full
inst✝ : F.Faithful
f : X ≅ Y
⊢ F.preimageIso (F.mapIso f) = f

Tactic:
ext
  simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α β : 𝟭 C ⟶ 𝟭 C
X : C
⊢ (α ≫ β).app X = (β ≫ α).app X

Tactic:
exact (α.naturality (β.app X)).symm

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : C
⊢ ⇑(ConcreteCategory.hom (𝟙 X)) = id

Tactic:
ext
  simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ⇑(ConcreteCategory.hom (f ≫ g)) = ⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f)

Tactic:
ext
  simp

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.length ≠ 0
⊢ p.length = p.length - 1 + 1

Tactic:
lia

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b c : V
e : a ⟶ c
p' : Path c b
h : (e.toPath.comp p').length ≠ 0
h_len : (e.toPath.comp p').length = (e.toPath.comp p').length - 1 + 1
hp' : p'.length = (e.toPath.comp p').length - 1
⊢ (e.toPath.comp p').length = p'.length + 1

Tactic:
lia

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

Goal state before:
pp: V✝ : Type u
inst✝² : Quiver V✝
a b c d : V✝
inst✝¹ : ∀ (a b : V✝), Subsingleton (a ⟶ b)
V : Type u_1
inst✝ : Quiver V
n : ℕ
h₁ : DecidableEq V
h₂ : (v w : V) → DecidableEq (v ⟶ w)
h₃ : (v w : V) → DecidableEq (BoundedPaths v w n)
v w : V
p q : Path v w
a✝¹ x✝² v' v'' : V
x✝¹ x✝ : BoundedPaths a✝¹ x✝² (n + 1)
a✝ : V
p' : Path a✝¹ a✝
α : a✝ ⟶ x✝²
q' : Path a✝¹ a✝
β : a✝ ⟶ x✝²
hq : (q'.cons β).length ≤ n + 1
h : α = β
hp : p'.length ≤ n
⊢ p'.length ≤ n

Tactic:
lia

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

Goal state before:
pp: V✝ : Type u
inst✝² : Quiver V✝
a b c d : V✝
inst✝¹ : ∀ (a b : V✝), Subsingleton (a ⟶ b)
V : Type u_1
inst✝ : Quiver V
n : ℕ
h₁ : DecidableEq V
h₂ : (v w : V) → DecidableEq (v ⟶ w)
h₃ : (v w : V) → DecidableEq (BoundedPaths v w n)
v w : V
p q : Path v w
a✝¹ x✝² v' v'' : V
x✝¹ x✝ : BoundedPaths a✝¹ x✝² (n + 1)
a✝ : V
p' : Path a✝¹ a✝
α : a✝ ⟶ x✝²
q' : Path a✝¹ a✝
β : a✝ ⟶ x✝²
hp : (p'.cons α).length ≤ n + 1
h : α = β
hp' : p'.length ≤ n
hq : q'.length ≤ n
⊢ q'.length ≤ n

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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 H : D ⥤ E
α : G ⟶ H
⊢ 𝟙 F ◫ α = F.whiskerLeft α

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
⊢ α ◫ 𝟙 F = whiskerRight α F

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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 G : C ⥤ D
H K : D ⥤ E
α : F ⟶ G
β : H ⟶ K
⊢ F.whiskerLeft β ≫ whiskerRight α K = whiskerRight α H ≫ G.whiskerLeft β

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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 G : C ⥤ D
H K : D ⥤ E
α : F ⟶ G
β : H ⟶ K
⊢ α ◫ β = F.whiskerLeft β ≫ whiskerRight α K

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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 G : C ⥤ D
H K : D ⥤ E
α : F ≅ G
β : H ≅ K
⊢ F.isoWhiskerLeft β ≪≫ isoWhiskerRight α K = isoWhiskerRight α H ≪≫ G.isoWhiskerLeft β

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
i : Y ⟶ Z
g : W ≅ Y
h : X ≅ Z
p : CommSq f g.hom h.hom i
⊢ i ≫ h.inv = g.inv ≫ f

Tactic:
rw [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, p.w]

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
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquivUnitCounit F G
⊢ (mk' adj).homEquiv = adj.homEquiv

Tactic:
ext
  rw [homEquiv_unit, adj.homEquiv_unit, mk'_unit]

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
X : C
h : F.cones.RepresentableBy X
s : Cone F
m : s.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = s.π.app j
⊢ m = homOfCone h s

Tactic:
rw [← homOfCone_coneOfHom h m]

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
X : C
h : F.cones.RepresentableBy X
s : Cone F
m : s.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = s.π.app j
⊢ homOfCone h (coneOfHom h m) = homOfCone h s
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
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    F.map ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g)) ≫
      (e (G_obj Y') Y'').symm ((e (G_obj Y') Y'') ((e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'))

Tactic:
Equiv.symm_apply_apply

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    F.map ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g)) ≫ (e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'
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
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| (e (G_obj Y) Y').symm ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g)) ≫ g'

Tactic:
Equiv.symm_apply_apply

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) ≫ g'
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e : F.RepresentableBy Y
X : C
f : X ⟶ Y
⊢ e.homEquiv f = (ConcreteCategory.hom (F.map f.op)) (e.homEquiv (𝟙 Y))

Tactic:
by
  conv_lhs => rw [← Category.comp_id f, e.homEquiv_comp]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom = f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv

Tactic:
by
  rw [← cancel_epi (f ◁ (α_ g h i).inv), ← cancel_mono (α_ (f ≫ g) h i).inv]
  simp

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₁
u : yoneda.obj (unop X) ⟶ F
⊢ yoneda.map f.unop ≫ u = yoneda.map f.unop ≫ yonedaEquiv.symm (yonedaEquiv u)

Tactic:
Equiv.symm_apply_apply

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type v₁
u : yoneda.obj (unop X) ⟶ F
⊢ yoneda.map f.unop ≫ u = yoneda.map f.unop ≫ u
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
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 : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ (unop X).unop.ι.app j ≫ f.unop.hom.unop = (unop Y).unop.ι.app j

Tactic:
apply Quiver.Hom.op_inj
            dsimp
            apply ConeMorphism.w

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasLimitsOfShape K C
E : K ⥤ J
⊢ lim.map α ≫ pre G E = pre F E ≫ lim.map (E.whiskerLeft α)

Tactic:
ext
  simp

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
c : Cocone F
⊢ pre F E ≫ desc F c = desc (E ⋙ F) (Cocone.whisker E c)

Tactic:
ext
  simp

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

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
⊢ post (F ⋙ G) H ≫ H.map (post F G) = post F (G ⋙ H)

Tactic:
by
  ext j
  rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_post]
  have : HasColimit (F ⋙ G ⋙ H) := h
  exact (colimit.ι_post F (G ⋙ H) j).symm

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

Goal state before:
pp: β : Type w
C : Type u
inst✝² : Category.{v, u} C
f g : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct g
p : (b : β) → f b ⟶ g b
b : β
⊢ map p ≫ π g b = π f b ≫ p b

Tactic:
by simp [Pi.map]

Goal state after: