mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z ↔ z = s(x, y)

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z → z = s(x, y)

case mpr
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ z = s(x, y) → x ∈ z ∧ y ∈ z
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
y : β
⊢ (∃ a ∈ s, f a = y) ↔ ∃ a ∈ s, g a = y

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ (∃ a ∈ s, f a = y) → ∃ a ∈ s, g a = y

case mpr
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ (∃ a ∈ s, g a = y) → ∃ a ∈ s, f a = y
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
⊢ (fun g' ↦ ↑R g' ∘ₗ ↑R g ∘ₗ f = i) (hg.lift (hf.lift i))

Tactic:
ext

Goal state after:
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
x✝ : M
⊢ (↑R (hg.lift (hf.lift i)) ∘ₗ ↑R g ∘ₗ f) x✝ = i x✝
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
⊢ ↑R (↑S g' ∘ₗ g) ∘ₗ f = ↑R g' ∘ₗ ↑R g ∘ₗ f

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : { a // a.IsDiag }
⊢ (fun a ↦ ⟨diag a, ⋯⟩) ((fun x ↦ (↑x).diagElem ⋯) x) = x

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : { a // a.IsDiag }
x✝ : α
⊢ x✝ ∈ ↑((fun a ↦ ⟨diag a, ⋯⟩) ((fun x ↦ (↑x).diagElem ⋯) x)) ↔ x✝ ∈ ↑x
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
⊢ diagSet = Set.univ

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : Subsingleton α
x✝ : Sym2 α
⊢ x✝ ∈ diagSet ↔ x✝ ∈ Set.univ
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ s(x, y).toFinset = {x, y}

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y a✝ : α
⊢ a✝ ∈ s(x, y).toFinset ↔ a✝ ∈ {x, y}
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂].Perm [a₂, b₂]

Tactic:
constructor

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

Goal state before:
pp: case refl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ y✝ : α
⊢ (Vector.Perm.isSetoid α 2) ⟨[(x✝, y✝).1, (x✝, y✝).2], ⋯⟩ ⟨[(x✝, y✝).1, (x✝, y✝).2], ⋯⟩

Tactic:
constructor

Goal state after:
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ y✝ : α
⊢ [(x✝, y✝).2].Perm [(x✝, y✝).2]
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil.cons.cons.nil.inl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝¹ head✝ : α
hx hy : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨[head✝¹, head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨[head✝¹, head✝], hy⟩)

Tactic:
constructor

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

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb✝ = a

Tactic:
convert! other_invol' ha hb using 2

Goal state after:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other ha = Mem.other' ha
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra R S
x✝¹ : Algebra (A ⊗[R] S) (B ⊗[R] S)
x✝ : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H : (algebraMap (A ⊗[R] S) (B ⊗[R] S)).comp TensorProduct.includeRight.toRingHom = TensorProduct.includeRight.toRingHom
⊢ IsPushout A B (A ⊗[R] S) (B ⊗[R] S)

Tactic:
constructor

Goal state after:
R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra R S
x✝¹ : Algebra (A ⊗[R] S) (B ⊗[R] S)
x✝ : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H : (algebraMap (A ⊗[R] S) (B ⊗[R] S)).comp TensorProduct.includeRight.toRingHom = TensorProduct.includeRight.toRingHom
⊢ IsBaseChange B (toAlgHom A (A ⊗[R] S) (B ⊗[R] S)).toLinearMap
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_8
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
C : Type u_11
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra A C
inst✝² : IsScalarTower R A C
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (↑(cancelBaseChangeAlg R S A (S ⊗[R] A) C).symm).comp (TensorProduct.lTensor S (toAlgHom R A C)) =
    TensorProduct.includeLeft

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_8
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
C : Type u_11
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra A C
inst✝² : IsScalarTower R A C
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : A
⊢ ((AlgHom.restrictScalars R
            ((↑(cancelBaseChangeAlg R S A (S ⊗[R] A) C).symm).comp (TensorProduct.lTensor S (toAlgHom R A C)))).comp
        TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R TensorProduct.includeLeft).comp TensorProduct.includeRight) x✝
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z Z' : C
α : X ≅ Y
β : Y ≅ Z
γ : Z ≅ Z'
⊢ (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z Z' : C
α : X ≅ Y
β : Y ≅ Z
γ : Z ≅ Z'
⊢ ((α ≪≫ β) ≪≫ γ).hom = (α ≪≫ β ≪≫ γ).hom
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ refl X ≪≫ α = α

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ (refl X ≪≫ α).hom = α.hom
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ α ≪≫ refl Y = α

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ (α ≪≫ refl Y).hom = α.hom
Module: Mathlib.CategoryTheory.Iso

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 Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ (F.mapIso (i ≪≫ j)).hom = (F.mapIso i ≪≫ F.mapIso j).hom
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
Y : C
⊢ ofObj X Y ↔ ∃ i, X i = Y

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
Y : C
⊢ ofObj X Y → ∃ i, X i = Y

case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
Y : C
⊢ (∃ i, X i = Y) → ofObj X Y
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ pair X Y Z ↔ X = Z ∨ Y = Z

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ pair X Y Z → X = Z ∨ Y = Z

case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ X = Z ∨ Y = Z → pair X Y Z
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

Goal state after:
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)).hom = f.hom
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
X : C
hX : P X
⊢ P.strictMap F (F.obj X)

Tactic:
exact ⟨X, hX⟩

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

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
X : C
F : C ⥤ D
⊢ (singleton X).strictMap F = singleton (F.obj X)

Tactic:
ext

Goal state after:
C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
X : C
F : C ⥤ D
x✝ : D
⊢ (singleton X).strictMap F x✝ ↔ singleton (F.obj X) x✝
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map✝¹ : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map✝ : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
⊢ f₁ = f₂

Tactic:
ext

Goal state after:
case mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map✝¹ : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map✝ : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
x✝² x✝¹ : C
x✝ : F.obj x✝² ⟶ F.obj x✝¹
⊢ f₁ x✝ = f₂ x✝
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
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
G_obj : D → E
map✝¹ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : D), map✝¹ (𝟙 X) = 𝟙 (G_obj X)
map_comp✝¹ : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
inst✝¹ : { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.Faithful
map✝ : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 ((G_obj ∘ obj) X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
inst✝ : { obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.Faithful
h_obj :
  ∀ (X : C),
    { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj (obj X) =
      { obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map✝ :
  ∀ {X Y : C} {f : X ⟶ Y},
    { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map (map f) ≍
      { obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h_map : ∀ {X Y : C} {f : X ⟶ Y}, map✝¹ (map f) = map✝ f
⊢ (fun {X Y} f ↦
      { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map
        ({ obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }.map f)) =
    map✝

Tactic:
ext

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
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
G_obj : D → E
map✝¹ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : D), map✝¹ (𝟙 X) = 𝟙 (G_obj X)
map_comp✝¹ : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
inst✝¹ : { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.Faithful
map✝ : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 ((G_obj ∘ obj) X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
inst✝ : { obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.Faithful
h_obj :
  ∀ (X : C),
    { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj (obj X) =
      { obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map✝ :
  ∀ {X Y : C} {f : X ⟶ Y},
    { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map (map f) ≍
      { obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h_map : ∀ {X Y : C} {f : X ⟶ Y}, map✝¹ (map f) = map✝ f
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map
      ({ obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }.map x✝) =
    map✝ x✝
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
⊢ ⇑(hom (𝟙 X)) = id

Tactic:
ext

Goal state after:
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
x✝ : CC X
⊢ (hom (𝟙 X)) x✝ = id x✝
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
⊢ ⇑(hom (f ≫ g)) = ⇑(hom g) ∘ ⇑(hom f)

Tactic:
ext

Goal state after:
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
x✝ : CC X
⊢ (hom (f ≫ g)) x✝ = (⇑(hom g) ∘ ⇑(hom f)) x✝
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

Goal state after:
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
x✝ : CC X
⊢ (ConcreteCategory.hom (𝟙 X)) x✝ = id x✝
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

Goal state after:
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
x✝ : CC X
⊢ (ConcreteCategory.hom (f ≫ g)) x✝ = (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f)) x✝
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
C : Type u
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_2
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
f : C → D
X✝ Y✝ : InducedCategory D f
x✝ : X✝ ⟶ Y✝
⊢ homMk (ofHom (hom x✝.hom)) = x✝

Tactic:
ext

Goal state after:
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
C : Type u
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_2
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
f : C → D
X✝ Y✝ : InducedCategory D f
x✝ : X✝ ⟶ Y✝
⊢ hom (homMk (ofHom (hom x✝.hom))).hom = hom x✝.hom
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✝
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_2
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
P : ObjectProperty C
X✝ Y✝ : P.FullSubcategory
x✝ : X✝ ⟶ Y✝
⊢ homMk (ofHom (hom x✝.hom)) = x✝

Tactic:
ext

Goal state after:
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✝
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_2
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
P : ObjectProperty C
X✝ Y✝ : P.FullSubcategory
x✝ : X✝ ⟶ Y✝
⊢ hom (homMk (ofHom (hom x✝.hom))).hom = hom x✝.hom
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
⊢ f p

Tactic:
by_cases hp : p

Goal state after:
case pos
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : p
⊢ f p

case neg
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : ¬p
⊢ f p
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g ↔ f = g

Tactic:
constructor

Goal state after:
case mp
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g → f = g

case mpr
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ f = g → reverse f = reverse g
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
⊢ (ObjectProperty.isoClosure fun x ↦ x ∈ Set.range F.obj) = F.essImage

Tactic:
ext

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : D
⊢ ObjectProperty.isoClosure (fun x ↦ x ∈ Set.range F.obj) x✝ ↔ F.essImage x✝
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
⊢ (P.ι ⋙ F).essImage Y ↔ P.map F Y

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
⊢ (P.ι ⋙ F).essImage Y → P.map F Y

case mpr
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
⊢ P.map F Y → (P.ι ⋙ F).essImage Y
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ eqToIso p ≪≫ eqToIso q = eqToIso ⋯

Tactic:
ext

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ (eqToIso p ≪≫ eqToIso q).hom = (eqToIso ⋯).hom
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 Y : C
p : X = Y
⊢ F.mapIso (eqToIso p) = eqToIso ⋯

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
p : X = Y
⊢ (F.mapIso (eqToIso p)).hom = (eqToIso ⋯).hom
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

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 H : D ⥤ E
α : G ⟶ H
x✝ : C
⊢ (𝟙 F ◫ α).app x✝ = (F.whiskerLeft α).app x✝
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

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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
x✝ : C
⊢ (α ◫ 𝟙 F).app x✝ = (whiskerRight α F).app x✝