mathlib-initiative/mathlib-tactics huggingface dataset:
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 H✝ : ∀ a ∈ s(p.1, p.2), P a
⊢ Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) ⋯ H✝ = g p Hp

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: 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
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
f : M →ₗ[R] N
hf : IsBaseChange S f
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower R T Q
i : M →ₗ[R] Q
this✝¹ : Module S Q := Module.compHom Q (algebraMap S T)
this✝ : IsScalarTower S T Q
this : IsScalarTower R S Q
g' : O →ₗ[T] Q
e : ↑R g' ∘ₗ ↑R g ∘ₗ f = i
x✝ : M
⊢ (↑R (↑S g' ∘ₗ g) ∘ₗ f) x✝ = (↑R g' ∘ₗ ↑R g ∘ₗ f) x✝

Tactic:
rfl

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y : V
f : X ⟶ Y
⊢ homOfEq (homOfEq f ⋯ ⋯) ⋯ ⋯ = homOfEq f ⋯ ⋯

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case refl.refl
V : Type u_1
inst✝ : Quiver V
X Y : V
f g : X ⟶ Y
⊢ homOfEq f ⋯ ⋯ ≍ g ↔ f ≍ g

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case refl.refl
V : Type u_1
inst✝ : Quiver V
X Y : V
f g : X ⟶ Y
⊢ f ≍ homOfEq g ⋯ ⋯ ↔ f ≍ g

Tactic:
rfl

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

Goal state before:
pp: case h
α : Type u_1
P : α → Prop
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
⊢ map Subtype.val (pmap Subtype.mk s(x✝, y✝) h) = s(x✝, y✝)

Tactic:
rfl

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

Goal state before:
pp: case h
α : Type u_1
P : α → Prop
x✝ y✝ : α
h : ∀ a ∈ s(x✝, y✝), P a
⊢ map Subtype.val (s(x✝, y✝).attachWith h) = s(x✝, y✝)

Tactic:
rfl

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

Goal state before:
pp: case refl
α : Type u_1
x : α
h : diag x = diag x
⊢ x = x

Tactic:
rfl

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

Goal state before:
pp: case swap
α : Type u_1
x : α
h : diag x = diag x
⊢ x = x

Tactic:
rfl

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

Goal state before:
pp: case refl.refl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a : α
⊢ Eq.ndrec (motive := fun x ↦ x.IsDiag → α) (fun x ↦ a) ⋯ ⋯ = a

Tactic:
rfl

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

Goal state before:
pp: case refl.swap
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a : α
⊢ Eq.ndrec (motive := fun x ↦ x.IsDiag → α) (fun x ↦ a) ⋯ ⋯ = a

Tactic:
rfl

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

Goal state before:
pp: case h.refl
α : Type u_1
x✝ : α
⊢ diag (s(x✝, x✝).diagElem ⋯) = s(x✝, x✝)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α
f✝ : α → β
r r₁ r₂ : α → α → Prop
sym : Std.Symm r
f : α → β
hf : r ≤ ⇑(Setoid.ker f)
z : ↑(fromRel sym)
a₁ a₂ : α
h : r a₁ a₂
⊢ ⟨f a₂, ⟨s(⟨a₂, ⋯⟩, ⟨a₁, ⋯⟩), ⋯⟩⟩ = ⟨f a₂, ⟨s(⟨a₂, ⋯⟩, ⟨a₁, ⋯⟩), ⋯⟩⟩

Tactic:
rfl

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f✝ : α → β
r r₁ r₂ : α → α → Prop
sym : Std.Symm r
f : α → β
hf : r ≤ ⇑(Setoid.ker f)
val✝ : Sym2 α
a₁ a₂ : α
h : Quot.mk (Rel α) (a₁, a₂) ∈ fromRel sym
⊢ (fun z ↦ ⟨map Subtype.val ↑z.snd, ⋯⟩)
      ((fun z ↦ fromRelNdrec ↑z ⋯ (fun a₁ a₂ h ↦ ⟨f a₁, ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩) ⋯) ⟨Quot.mk (Rel α) (a₁, a₂), h⟩) =
    ⟨Quot.mk (Rel α) (a₁, a₂), h⟩

Tactic:
rfl

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f✝ : α → β
r r₁ r₂ : α → α → Prop
sym : Std.Symm r
f : α → β
hf : r ≤ ⇑(Setoid.ker f)
a₁ : α
val✝ : Sym2 { a // f a = f a₁ }
a₂ : α
ha₂ : f a₂ = f a₁
h : Quot.mk (Rel { a // f a = f a₁ }) (⟨a₁, ⋯⟩, ⟨a₂, ha₂⟩) ∈ fromRel ⋯
⊢ (fun z ↦ fromRelNdrec ↑z ⋯ (fun a₁ a₂ h ↦ ⟨f a₁, ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩) ⋯)
      ((fun z ↦ ⟨map Subtype.val ↑z.snd, ⋯⟩) ⟨f a₁, ⟨Quot.mk (Rel { a // f a = f a₁ }) (⟨a₁, ⋯⟩, ⟨a₂, ha₂⟩), h⟩⟩) =
    ⟨f a₁, ⟨Quot.mk (Rel { a // f a = f a₁ }) (⟨a₁, ⋯⟩, ⟨a₂, ha₂⟩), h⟩⟩

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
r₁ r₂ : α → α → Prop
sym₁ : Std.Symm r₁
sym₂ : Std.Symm r₂
⊢ fromRel sym₁ = fromRel sym₂ ↔ (fromRelOrderIso α) ⟨r₁, sym₁⟩ = (fromRelOrderIso α) ⟨r₂, sym₂⟩

Tactic:
rfl

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

Goal state before:
pp: case swap
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ y✝ : α
⊢ [].Perm []

Tactic:
rfl

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

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := F_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := F_obj, map := map✝ }.map f))
X Y : V
f : X ⟶ Y
⊢ map✝¹ f = map✝ f

Tactic:
simpa using h_map X Y f

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

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F G : Prefunctor V W
h_obj : ∀ (X : V), F.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn ⋯ (Eq.recOn ⋯ (G.map f))
⊢ F = G

Tactic:
obtain ⟨F_obj, _⟩ := F
  obtain ⟨G_obj, _⟩ := G
  obtain rfl : F_obj = G_obj := by
    ext X
    apply h_obj
  congr
  funext X Y f
  simpa using h_map X Y f

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

Goal state before:
pp: case refl
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X : U
⊢ F.obj X = F.obj X

Tactic:
rfl

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

Goal state before:
pp: case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨[head✝¹, head✝], hx⟩⟧) = ⟦⟨[head✝¹, head✝], hx⟩⟧

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst✝ : DecidableEq α
a b c d e : α
h✝ : Rel α (b, c) (d, e)
hy : a ∈ s(d, e)
h : a ∈ s(b, c)
⊢ Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ h = if a = b then c else b

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.NatTrans

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : NatTrans F G
X Y U V : C
f : X ⟶ Y
g : Y ⟶ U
h : U ⟶ V
⊢ α.app X ≫ G.map f ≫ G.map g ≫ G.map h = F.map f ≫ F.map g ≫ F.map h ≫ α.app V

Tactic:
grind

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v_1, u₁} C
D : Type u₂
inst✝ : Category.{v_2, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : D
h : F.obj Z ⟶ W
⊢ F.map (f ≫ g) ≫ h = F.map f ≫ F.map g ≫ h

Tactic:
grind

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id✝¹ : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
map_id✝ : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
h :
  { obj := obj, map := map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.toPrefunctor =
    { obj := obj, map := map, map_id := map_id✝, map_comp := map_comp✝ }.toPrefunctor
⊢ { obj := obj, map := map, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := obj, map := map, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
rfl

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
C : Type u_11
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
⊢ ↑(cancelBaseChangeAlg R S A B C) = cancelBaseChange R S A B C

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ α.inv = α.inv ≫ β.hom ≫ β.inv

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α β : X ≅ Y
w : α.hom = β.hom
⊢ α.inv ≫ β.hom ≫ β.inv = β.inv

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ β.hom = α.symm.hom ↔ β.hom = α.inv

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
g : Y ⟶ X
hom_inv_id : f ≫ g = 𝟙 X
⊢ inv f = g

Tactic:
have := congrArg (inv f ≫ ·) hom_inv_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
g : Y ⟶ X
hom_inv_id : f ≫ g = 𝟙 X
this : inv f ≫ f ≫ g = inv f ≫ 𝟙 X
⊢ inv f = g
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
g : Y ⟶ X
hom_inv_id : f ≫ g = 𝟙 X
this : inv f ≫ f ≫ g = inv f ≫ 𝟙 X
⊢ inv f = g

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
X Y : C
e : X ≅ Y
F : C ⥤ D
⊢ F.map e.hom ≫ F.map e.inv = 𝟙 (F.obj X)

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
X Y : C
e : X ≅ Y
F : C ⥤ D
⊢ F.map e.inv ≫ F.map e.hom = 𝟙 (F.obj Y)

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⥤ D
α : F ≅ G
X : C
⊢ α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X)

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⥤ D
α : F ≅ G
X : C
⊢ α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X)

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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
E' : Type u₄
inst✝¹ : Category.{v₄, u₄} E'
F G : C ⥤ D
X✝ Y : C
α : F ⟶ G
inst✝ : IsIso α
X : C
⊢ α.app X ≫ (inv α).app X = 𝟙 (F.obj X)

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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
E' : Type u₄
inst✝¹ : Category.{v₄, u₄} E'
F G : C ⥤ D
X✝ Y : C
α : F ⟶ G
inst✝ : IsIso α
X : C
⊢ (inv α).app X ≫ α.app X = 𝟙 (G.obj X)

Tactic:
grind

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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
X : C
⊢ G.map (map (𝟙 X)) = G.map (𝟙 (obj X))

Tactic:
grind

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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : p
h✝ : q
⊢ a h✝¹ = a h✝¹

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : p
h✝ : ¬q
⊢ a h✝¹ = a h✝¹

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : ¬p
h✝ : q
⊢ b h✝¹ h✝ = b h✝¹ ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : ¬p
h✝ : ¬q
⊢ c h✝¹ h✝ = c h✝¹ ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : p
h✝ : q
⊢ a h✝¹ h✝ = a h✝¹ ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : p
h✝ : ¬q
⊢ b h✝¹ h✝ = b h✝¹ ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case pos
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : ¬p
h✝ : q
⊢ c h✝¹ = c h✝¹

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case neg
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : ¬p
h✝ : ¬q
⊢ c h✝¹ = c h✝¹

Tactic:
rfl

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

Goal state before:
pp: case nil
V : Type u
inst✝ : Quiver V
a : V
hzero : nil.length = 0
⊢ a = a

Tactic:
rfl

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

Goal state before:
pp: case nil
V : Type u
inst✝ : Quiver V
a : V
hzero : nil.length = 0
⊢ nil = nil

Tactic:
rfl

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

Goal state before:
pp: case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
Φ : Push σ ⥤q W'
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
h : ∀ (x : V), (of σ ⋙q Φ).obj x = Φ.obj (σ x)
⊢ Φ.map (PushQuiver.arrow f✝) = ⋯.mpr (⋯.mpr (Φ.map ((of σ).map f✝)))

Tactic:
rfl

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

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
q₁ : Path b c
hq : q₁.length = q₁.length
⊢ p₁.comp q₁ = p₁.comp q₁

Tactic:
rfl

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

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
q₁ : Path b c
h : p₁.length = p₁.length
⊢ p₁.comp q₁ = p₁.comp q₁

Tactic:
rfl

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

Goal state before:
pp: case cons
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : a✝¹.reverse.reverse = a✝¹
⊢ a✝¹.comp a✝.toPath = a✝¹.cons a✝

Tactic:
rfl

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

Goal state before:
pp: case h_obj
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
X : V
⊢ (of ⋙q lift φ).obj X = φ.obj X

Tactic:
rfl

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

Goal state before:
pp: case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
X Y : V
f : X ⟶ Y
⊢ (of ⋙q lift φ).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
rfl

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

Goal state before:
pp: case inl
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ (match (Sum.inl val✝).swap with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse (φ.map val✝)

Tactic:
rfl

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

Goal state before:
pp: case inr
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ (match (Sum.inr val✝).swap with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    φ.map val✝

Tactic:
rfl

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

Goal state before:
pp: case h_obj
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X : Symmetrify V
⊢ Φ.obj X = (lift (of ⋙q Φ)).obj X

Tactic:
rfl

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

Goal state before:
pp: case h_map.inl
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ Φ.map (Sum.inl val✝) = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map (Sum.inl val✝)))

Tactic:
rfl

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

Goal state before:
pp: case inl
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
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
val✝ : u✝ ⟶ v✝
⊢ φ.symmetrify.map (reverse (Sum.inl val✝)) = reverse (φ.symmetrify.map (Sum.inl val✝))

Tactic:
rfl

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

Goal state before:
pp: case inr
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
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
val✝ : v✝ ⟶ u✝
⊢ φ.symmetrify.map (reverse (Sum.inr val✝)) = reverse (φ.symmetrify.map (Sum.inr val✝))

Tactic:
rfl

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

Goal state before:
pp: case nil
V : Type u₁
inst✝² : Quiver V
W : Type u₂
inst✝¹ : Quiver W
F : V ⥤q W
U : Type u₃
inst✝ : Quiver U
G : W ⥤q U
a b : V
⊢ (F ⋙q G).mapPath Path.nil = G.mapPath (F.mapPath Path.nil)

Tactic:
rfl

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

Goal state before:
pp: V : Type u₁
inst✝² : Quiver V
W : Type u₂
inst✝¹ : Quiver W
F : V ⥤q W
U : Type u₃
inst✝ : Quiver U
G : W ⥤q U
a b : V
p : Path a b
⊢ (F ⋙q G).mapPath p = G.mapPath (F.mapPath p)

Tactic:
by
  induction p with
  | nil => rfl
  | cons x y h => simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ P.isoClosure X ↔ ∃ Y x, Nonempty (X ≅ Y)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ eqToHom ⋯ ≍ 𝟙 X

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ (eqToHom ⋯).op = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
⊢ (eqToHom ⋯).unop = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

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_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), map✝¹ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
      eqToHom ⋯ ≫ { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ map✝¹ f = map✝ f

Tactic:
simpa using h_map X Y f

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (eqToHom ⋯).app X = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
β : Sort u_1
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
C : Type u_2
D : Type u_3
inst✝ : Category.{?u.12, u_3} D
F : C → D
X : InducedCategory D F
⊢ F X = F X

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u_2
D : Type u_3
inst✝ : Category.{u_4, u_3} D
F : C → D
X : InducedCategory D F
⊢ (eqToHom ⋯).hom = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
β : Sort u_1
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u_2
inst✝ : Category.{?u.11, u_2} C
P : ObjectProperty C
X : P.FullSubcategory
⊢ X.obj = X.obj

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u_2
inst✝ : Category.{u_3, u_2} C
P : ObjectProperty C
X : P.FullSubcategory
⊢ (eqToHom ⋯).hom = eqToHom ⋯

Tactic:
rfl

Goal state after: