mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case map_units
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
⊢ Function.Bijective ⇑((algebraMap R (End R S')) ↑x)

Tactic:
constructor

Goal state after:
case map_units.left
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
⊢ Function.Injective ⇑((algebraMap R (End R S')) ↑x)

case map_units.right
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
⊢ Function.Surjective ⇑((algebraMap R (End R S')) ↑x)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case map_units.left
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
⊢ Function.Injective ⇑((algebraMap R (End R S')) ↑x)

Tactic:
rintro a b (e : x • a = x • b)
      simp_rw [Submonoid.smul_def, Algebra.smul_def] at e
      exact (h₁ x x.2).mul_left_cancel e

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (∃ i, X i = unop Z) ↔ ∃ i, op (X i) = Z

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (∃ i, X i = unop Z) → ∃ i, op (X i) = Z

case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (∃ i, op (X i) = Z) → ∃ i, X i = unop Z
Module: Mathlib.CategoryTheory.WithTerminal.Cone

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Over X
F : C ⥤ D
t✝ : Cone K
t : Cone (liftFromOver.obj K)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Functor.const J).obj (Over.mk (t.π.app star))).map f ≫ Over.homMk (t.π.app (of x✝)) ⋯ =
    Over.homMk (t.π.app (of x✝¹)) ⋯ ≫ K.map f

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Over X
F : C ⥤ D
t✝ : Cone K
t : Cone (liftFromOver.obj K)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ Over.Hom.left (((Functor.const J).obj (Over.mk (t.π.app star))).map f ≫ Over.homMk (t.π.app (of x✝)) ⋯) =
    Over.Hom.left (Over.homMk (t.π.app (of x✝¹)) ⋯ ≫ K.map f)
Module: Mathlib.CategoryTheory.WithTerminal.Cone

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Over X
F : C ⥤ D
t : Cone K
t₁ t₂ : Cone (liftFromOver.obj K)
f : t₁ ⟶ t₂
j : J
⊢ Over.homMk f.hom ⋯ ≫
      { pt := Over.mk (t₂.π.app star), π := { app := fun a ↦ Over.homMk (t₂.π.app (of a)) ⋯, naturality := ⋯ } }.π.app
        j =
    { pt := Over.mk (t₁.π.app star), π := { app := fun a ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ } }.π.app j

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Over X
F : C ⥤ D
t : Cone K
t₁ t₂ : Cone (liftFromOver.obj K)
f : t₁ ⟶ t₂
j : J
⊢ Over.Hom.left
      (Over.homMk f.hom ⋯ ≫
        { pt := Over.mk (t₂.π.app star), π := { app := fun a ↦ Over.homMk (t₂.π.app (of a)) ⋯, naturality := ⋯ } }.π.app
          j) =
    Over.Hom.left
      ({ pt := Over.mk (t₁.π.app star), π := { app := fun a ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ } }.π.app
        j)
Module: Mathlib.CategoryTheory.WithTerminal.Cone

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Under X
F : C ⥤ D
t✝ : Cocone K
t : Cocone (liftFromUnder.obj K)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ K.map f ≫ Under.homMk (t.ι.app (of x✝)) ⋯ =
    Under.homMk (t.ι.app (of x✝¹)) ⋯ ≫ ((Functor.const J).obj (Under.mk (t.ι.app star))).map f

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Under X
F : C ⥤ D
t✝ : Cocone K
t : Cocone (liftFromUnder.obj K)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ Under.Hom.right (K.map f ≫ Under.homMk (t.ι.app (of x✝)) ⋯) =
    Under.Hom.right (Under.homMk (t.ι.app (of x✝¹)) ⋯ ≫ ((Functor.const J).obj (Under.mk (t.ι.app star))).map f)
Module: Mathlib.CategoryTheory.WithTerminal.Cone

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Under X
F : C ⥤ D
t : Cocone K
t₁ t₂ : Cocone (liftFromUnder.obj K)
f : t₁ ⟶ t₂
j : J
⊢ { pt := Under.mk (t₁.ι.app star), ι := { app := fun a ↦ Under.homMk (t₁.ι.app (of a)) ⋯, naturality := ⋯ } }.ι.app j ≫
      Under.homMk f.hom ⋯ =
    { pt := Under.mk (t₂.ι.app star), ι := { app := fun a ↦ Under.homMk (t₂.ι.app (of a)) ⋯, naturality := ⋯ } }.ι.app j

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Under X
F : C ⥤ D
t : Cocone K
t₁ t₂ : Cocone (liftFromUnder.obj K)
f : t₁ ⟶ t₂
j : J
⊢ Under.Hom.right
      ({ pt := Under.mk (t₁.ι.app star),
                ι := { app := fun a ↦ Under.homMk (t₁.ι.app (of a)) ⋯, naturality := ⋯ } }.ι.app
          j ≫
        Under.homMk f.hom ⋯) =
    Under.Hom.right
      ({ pt := Under.mk (t₂.ι.app star),
              ι := { app := fun a ↦ Under.homMk (t₂.ι.app (of a)) ⋯, naturality := ⋯ } }.ι.app
        j)
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j j' : J
⊢ F.obj j = F.obj j'

Tactic:
ext

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j j' : J
⊢ (F.obj j).as = (F.obj j').as
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ (Discrete.mk ∘ F) X✝ = (Discrete.mk ∘ F) Y✝

Tactic:
ext

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ ((Discrete.mk ∘ F) X✝).as = ((Discrete.mk ∘ F) Y✝).as
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
α✝ : Type u₁
F : J ⥤ Discrete α✝
j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ F.obj j₁✝ = F.obj j₂✝

Tactic:
ext

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
α✝ : Type u₁
F : J ⥤ Discrete α✝
j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ (F.obj j₁✝).as = (F.obj j₂✝).as
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case h
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ Surjective ⇑((↑e).comp f) ∧ (RingHom.ker ((↑e).comp f).toRingHom).FG

Tactic:
constructor

Goal state after:
case h.left
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ Surjective ⇑((↑e).comp f)

case h.right
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ (RingHom.ker ((↑e).comp f).toRingHom).FG
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty C
w✝¹ : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
⊢ P ≤ (P' ⊔ Q').isoClosure ∧ Q ≤ (P' ⊔ Q').isoClosure

Tactic:
constructor

Goal state after:
case left
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty C
w✝¹ : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
⊢ P ≤ (P' ⊔ Q').isoClosure

case right
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty C
w✝¹ : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
⊢ Q ≤ (P' ⊔ Q').isoClosure
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ FinitePresentation R A ↔ ∃ n I x, I.FG

Tactic:
constructor

Goal state after:
case mp
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ FinitePresentation R A → ∃ n I x, I.FG

case mpr
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (∃ n I x, I.FG) → FinitePresentation R A
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ FinitePresentation R A ↔ ∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Tactic:
constructor

Goal state after:
case mp
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ FinitePresentation R A → ∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

case mpr
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG) → FinitePresentation R A
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ IsIso (homFromCommaOfIsIso i)

Tactic:
constructor

Goal state after:
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ ∃ inv, homFromCommaOfIsIso i ≫ inv = 𝟙 X ∧ inv ≫ homFromCommaOfIsIso i = 𝟙 Y
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
hfp : FinitePresentation R A
⊢ FinitePresentation R (MvPolynomial ι A)

Tactic:
iff_quotient_mvPolynomial'

Goal state after:
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
hfp : ∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ ∃ ι_1 x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case h
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ homFromCommaOfIsIso i ≫ homFromCommaOfIsIso (inv i) = 𝟙 X ∧ homFromCommaOfIsIso (inv i) ≫ homFromCommaOfIsIso i = 𝟙 Y

Tactic:
constructor

Goal state after:
case h.left
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ homFromCommaOfIsIso i ≫ homFromCommaOfIsIso (inv i) = 𝟙 X

case h.right
A : Type u_1
inst✝⁷ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁶ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁵ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝⁴ : Q.IsMultiplicative
inst✝³ : W.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ homFromCommaOfIsIso (inv i) ≫ homFromCommaOfIsIso i = 𝟙 Y
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q W : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
A B : P.Arrow Q W
f g : A ⟶ B
hl : f.left = g.left
hr : f.right = g.right
⊢ f = g

Tactic:
ext

Goal state after:
case h₁
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q W : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
A B : P.Arrow Q W
f g : A ⟶ B
hl : f.left = g.left
hr : f.right = g.right
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left

case h₂
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q W : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
A B : P.Arrow Q W
f g : A ⟶ B
hl : f.left = g.left
hr : f.right = g.right
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.left = g.left
⊢ f = g

Tactic:
ext

Goal state after:
case h₁
T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.left = g.left
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left

case h₂
T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.left = g.left
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.right = g.right
⊢ f = g

Tactic:
ext

Goal state after:
case h₁
T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.right = g.right
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left

case h₂
T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.right = g.right
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝ : Q.IsMultiplicative
F : C ⥤ D
X : D
A B : P.CostructuredArrow Q F X
f g : A ⟶ B
h : f.left = g.left
⊢ f = g

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝ : Q.IsMultiplicative
F : C ⥤ D
X : D
A B : P.CostructuredArrow Q F X
f g : A ⟶ B
h : f.left = g.left
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left

case h₂
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝ : Q.IsMultiplicative
F : C ⥤ D
X : D
A B : P.CostructuredArrow Q F X
f g : A ⟶ B
h : f.left = g.left
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Faithful
⊢ (CostructuredArrow.toOver P F X).Faithful

Tactic:
constructor

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Faithful
⊢ autoParam (∀ {X_1 Y : P.CostructuredArrow ⊤ F X}, Function.Injective (CostructuredArrow.toOver P F X).map)
    Functor.Faithful.map_injective._autoParam
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Faithful
A B : P.CostructuredArrow ⊤ F X
f g : A ⟶ B
hfg : (CostructuredArrow.toOver P F X).map f = (CostructuredArrow.toOver P F X).map g
⊢ f = g

Tactic:
ext

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Faithful
A B : P.CostructuredArrow ⊤ F X
f g : A ⟶ B
hfg : (CostructuredArrow.toOver P F X).map f = (CostructuredArrow.toOver P F X).map g
⊢ f.left = g.left
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Full
⊢ (CostructuredArrow.toOver P F X).Full

Tactic:
constructor

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Full
⊢ ∀ {X_1 Y : P.CostructuredArrow ⊤ F X}, Function.Surjective (CostructuredArrow.toOver P F X).map
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ (CostructuredArrow.toOver P F X).map (CostructuredArrow.homMk (F.preimage f.left) trivial ⋯) = f

Tactic:
ext

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ ((CostructuredArrow.toOver P F X).map (CostructuredArrow.homMk (F.preimage f.left) trivial ⋯)).left = f.left
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
X✝ Y✝ : F.Elements
x✝ : X✝ ⟶ Y✝
⊢ ⟨Groupoid.inv ↑x✝, ⋯⟩ ≫ x✝ = 𝟙 Y✝

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
X✝ Y✝ : F.Elements
x✝ : X✝ ⟶ Y✝
⊢ ↑(⟨Groupoid.inv ↑x✝, ⋯⟩ ≫ x✝) = ↑(𝟙 Y✝)
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
X✝ Y✝ : F.Elements
x✝ : X✝ ⟶ Y✝
⊢ x✝ ≫ ⟨Groupoid.inv ↑x✝, ⋯⟩ = 𝟙 X✝

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
X✝ Y✝ : F.Elements
x✝ : X✝ ⟶ Y✝
⊢ ↑(x✝ ≫ ⟨Groupoid.inv ↑x✝, ⋯⟩) = ↑(𝟙 X✝)
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : F.Elements
f : X ⟶ Y
⊢ (StructuredArrow.mk (↾fun x ↦ X.snd)).hom ≫ F.map ↑f = (StructuredArrow.mk (↾fun x ↦ Y.snd)).hom

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : F.Elements
f : X ⟶ Y
x✝ : PUnit.{w + 1}
⊢ (ConcreteCategory.hom ((StructuredArrow.mk (↾fun x ↦ X.snd)).hom ≫ F.map ↑f)).toFun x✝ =
    (ConcreteCategory.hom (StructuredArrow.mk (↾fun x ↦ Y.snd)).hom).toFun x✝
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
x y : F.Elements
f : y ⟶ x
⊢ ((𝟭 F.Elementsᵒᵖ).map (op f) ≫
        (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))) (unop (op y))
              (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))).fst) ⋯).op.hom).unop =
    ((isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))) (unop (op x))
              (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))).fst) ⋯).op.hom ≫
        (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map (op f)).unop

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
x y : F.Elements
f : y ⟶ x
⊢ ↑((𝟭 F.Elementsᵒᵖ).map (op f) ≫
          (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))) (unop (op y))
                (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))).fst)
                ⋯).op.hom).unop =
    ↑((isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))) (unop (op x))
                (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))).fst) ⋯).op.hom ≫
          (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map (op f)).unop