mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ W ((z₂.s ≫ u₂) ≫ v₅ ≫ w)

Tactic:
]

Goal state after:
case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ W ((z₂.s ≫ u₂) ≫ v₅ ≫ w)
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝ : Φ.functor.IsEquivalence
h : W₂ ≤ W₁.map Φ.functor
⊢ W₂ ≤ W₁.isoClosure.map Φ.functor.asEquivalence.functor

Tactic:
]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝ : Φ.functor.IsEquivalence
h : W₂ ≤ W₁.map Φ.functor
⊢ W₂ ≤ W₁.isoClosure.map Φ.functor.asEquivalence.functor
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝ : Φ.functor.IsEquivalence
h : W₂ ≤ W₁.map Φ.functor
⊢ W₂ ≤ W₁.map Φ.functor.asEquivalence.functor

Tactic:
]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝ : Φ.functor.IsEquivalence
h : W₂ ≤ W₁.map Φ.functor
⊢ W₂ ≤ W₁.map Φ.functor.asEquivalence.functor
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f
⊢ LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')

Tactic:
obtain ⟨z₄, fac⟩ := exists_leftFraction (RightFraction.mk z₃.s z₃.hs z₃'.s)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f
z₄ : W.LeftFraction z₃.Y' z₃'.Y'
fac :
  { X' := z₂.Y', s := z₃.s, hs := ⋯, f := z₃'.s }.f ≫ z₄.s = { X' := z₂.Y', s := z₃.s, hs := ⋯, f := z₃'.s }.s ≫ z₄.f
⊢ LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor ⋙ Ψ.functor
ε₂ : 𝟭 C₂ ⟶ Ψ.functor ⋙ Φ.functor
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
⊢ ∀ (X : C₁), IsIso ((whiskerRight ε₁ W₁.Q).app X)

Tactic:
]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor ⋙ Ψ.functor
ε₂ : 𝟭 C₂ ⟶ Ψ.functor ⋙ Φ.functor
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
⊢ ∀ (X : C₁), IsIso ((whiskerRight ε₁ W₁.Q).app X)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f
z₄ : W.LeftFraction z₃.Y' z₃'.Y'
fac : z₃'.s ≫ z₄.s = z₃.s ≫ z₄.f
⊢ z₂.f ≫ z₃.s ≫ z₄.f = z₂.f ≫ z₃.s ≫ z₄.f

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor ⋙ Ψ.functor
ε₂ : 𝟭 C₂ ⟶ Ψ.functor ⋙ Φ.functor
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this : IsIso (whiskerRight ε₁ W₁.Q)
⊢ ∀ (X : C₂), IsIso ((whiskerRight ε₂ W₂.Q).app X)

Tactic:
]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor ⋙ Ψ.functor
ε₂ : 𝟭 C₂ ⟶ Ψ.functor ⋙ Φ.functor
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this : IsIso (whiskerRight ε₁ W₁.Q)
⊢ ∀ (X : C₂), IsIso ((whiskerRight ε₂ W₂.Q).app X)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case mp.refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac : t₁' ≫ α.s ≫ u = t₁ ≫ α.f ≫ u
fac' : t₂ ≫ α.f ≫ u ≫ u' = t₂' ≫ α.s ≫ u ≫ u'
⊢ ψ.f ≫ t₂' ≫ α.s ≫ u ≫ u' = ψ.f ≫ t₂' ≫ α.s ≫ u ≫ u'

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝ : CatCommSq Φ.functor L₁ L₂ G
hG : G.FullyFaithful
⊢ Nonempty G.FullyFaithful

Tactic:
]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝ : CatCommSq Φ.functor L₁ L₂ G
hG : G.FullyFaithful
⊢ Nonempty G.FullyFaithful
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ L.map (φ.f ≫ t₂ + φ.f' ≫ t₂) = L.map (φ.f ≫ t₂ + φ.f' ≫ t₂)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₃, u₃} C₃
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
h : Φ.IsLocalizedFullyFaithful
inst✝ : CatCommSq Φ.functor L₁ L₂ G
⊢ Nonempty (Φ.localizedFunctor W₁.Q W₂.Q).FullyFaithful

Tactic:
]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₃, u₃} C₃
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
h : Φ.IsLocalizedFullyFaithful
inst✝ : CatCommSq Φ.functor L₁ L₂ G
⊢ Nonempty (Φ.localizedFunctor W₁.Q W₂.Q).FullyFaithful
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case mp.refine_3
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac : t₁' ≫ α.s ≫ u = t₁ ≫ α.f ≫ u
fac' : t₂ ≫ α.f ≫ u ≫ u' = t₂' ≫ α.s ≫ u ≫ u'
⊢ ψ.f' ≫ t₂' ≫ α.s ≫ u ≫ u' = ψ.f' ≫ t₂' ≫ α.s ≫ u ≫ u'

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
⊢ α.add.map L ⋯ = α.add.map L ⋯

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ { Y' := α.Y', f := α.f, f' := 0, s := α.s, hs := ⋯ }.add.map L ⋯ = α.map L ⋯

pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ L.map 0 = { Y' := α.Y', f := α.f, f' := 0, s := α.s, hs := ⋯ }.snd.map L ⋯

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ { Y' := α.Y', f := α.f, f' := 0, s := α.s, hs := ⋯ }.add.map L ⋯ = α.map L ⋯

C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ L.map 0 = { Y' := α.Y', f := α.f, f' := 0, s := α.s, hs := ⋯ }.snd.map L ⋯
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Category.{v₂, u₂} C₂
inst✝⁶ : Category.{v₄, u₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : Φ.IsLocalizedFullyFaithful
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
L₁ : C₁ ⥤ D₁
F : D₁ ⥤ D₂
iso : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : L₁.EssSurj
x✝¹ x✝ : C₁
f : x✝¹ ⟶ x✝
hf : W₁ f
⊢ IsIso (F.map (L₁.map f))

Tactic:
]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Category.{v₂, u₂} C₂
inst✝⁶ : Category.{v₄, u₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : Φ.IsLocalizedFullyFaithful
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
L₁ : C₁ ⥤ D₁
F : D₁ ⥤ D₂
iso : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : L₁.EssSurj
x✝¹ x✝ : C₁
f : x✝¹ ⟶ x✝
hf : W₁ f
⊢ IsIso (F.map (L₁.map f))
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case mp.refine_4
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac : t₁' ≫ α.s ≫ u = t₁ ≫ α.f ≫ u
fac' : t₂ ≫ α.f ≫ u ≫ u' = t₂' ≫ α.s ≫ u ≫ u'
⊢ W ((φ.s ≫ t₁') ≫ α.s ≫ u ≫ u')

Tactic:
]

Goal state after:
case mp.refine_4
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac : t₁' ≫ α.s ≫ u = t₁ ≫ α.f ≫ u
fac' : t₂ ≫ α.f ≫ u ≫ u' = t₂' ≫ α.s ≫ u ≫ u'
⊢ W ((φ.s ≫ t₁') ≫ α.s ≫ u ≫ u')
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ L.map 0 = L.map { Y' := α.Y', f := α.f, f' := 0, s := α.s, hs := ⋯ }.snd.f

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ { Y' := α.Y', f := α.f, s := α.s, hs := ⋯ }.map L ⋯ = α.map L ⋯

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ f = f

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
α : W.LeftFraction X Y
⊢ { Y' := α.Y', f := -α.f, f' := α.f, s := α.s, hs := ⋯ }.add.map L ⋯ = L.map 0

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
α : W.LeftFraction X Y
⊢ { Y' := α.Y', f := -α.f, f' := α.f, s := α.s, hs := ⋯ }.add.map L ⋯ = L.map 0
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ f₃ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₃ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
h₃ : f₃ = α.thd.map L ⋯
⊢ { Y' := α.Y', f := α.f + α.f', f' := α.f'', s := α.s, hs := ⋯ }.add.map L ⋯ =
    { Y' := α.Y', f := α.f, f' := α.f' + α.f'', s := α.s, hs := ⋯ }.add.map L ⋯

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ f₃ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₃ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
h₃ : f₃ = α.thd.map L ⋯
⊢ { Y' := α.Y', f := α.f + α.f', f' := α.f'', s := α.s, hs := ⋯ }.add.map L ⋯ =
    { Y' := α.Y', f := α.f, f' := α.f' + α.f'', s := α.s, hs := ⋯ }.add.map L ⋯
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' ⟶ U
t₂ : b₂.Y' ⟶ U
hst : b₁.s ≫ t₁ = b₂.s ≫ t₂
hft : b₁.f ≫ t₁ = b₂.f ≫ t₂
ht : W (b₁.s ≫ t₁)
z₁ : W.LeftFraction a.Y' b₁.Y'
fac₁ : b₁.f ≫ z₁.s = a.s ≫ z₁.f
z₂ : W.LeftFraction a.Y' b₂.Y'
fac₂ : b₂.f ≫ z₂.s = a.s ≫ z₂.f
w₁ : W.LeftFraction z₁.Y' U
fac₁' : t₁ ≫ w₁.s = z₁.s ≫ w₁.f
w₂ : W.LeftFraction z₂.Y' U
fac₂' : t₂ ≫ w₂.s = z₂.s ≫ w₂.f
u : W.LeftFraction w₁.Y' w₂.Y'
fac₃ : w₂.s ≫ u.s = w₁.s ≫ u.f
⊢ b₂.f ≫ t₂ ≫ w₁.s ≫ u.f = b₂.f ≫ t₂ ≫ w₁.s ≫ u.f

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
φ : W.RightFraction₂ X Y
inst✝ : W.HasLeftCalculusOfFractions
ψ₁ : W.LeftFraction X Y
hψ₁ : φ.f ≫ ψ₁.s = φ.s ≫ ψ₁.f
ψ₂ : W.LeftFraction X Y
hψ₂ : φ.f' ≫ ψ₂.s = φ.s ≫ ψ₂.f
α : W.LeftFraction ψ₁.Y' ψ₂.Y'
hα : ψ₂.s ≫ α.s = ψ₁.s ≫ α.f
⊢ φ.s ≫ ψ₁.f ≫ α.f = φ.s ≫ ψ₁.f ≫ α.f

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ f₃ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₃ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
h₃ : f₃ = α.thd.map L ⋯
⊢ { Y' := α.Y', f := α.f + (α.f' + α.f''), s := α.s, hs := ⋯ }.map L ⋯ =
    { Y' := α.Y', f := α.f + (α.f' + α.f''), s := α.s, hs := ⋯ }.map L ⋯

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
φ : W.RightFraction₂ X Y
inst✝ : W.HasLeftCalculusOfFractions
ψ₁ : W.LeftFraction X Y
hψ₁ : φ.f ≫ ψ₁.s = φ.s ≫ ψ₁.f
ψ₂ : W.LeftFraction X Y
hψ₂ : φ.f' ≫ ψ₂.s = φ.s ≫ ψ₂.f
α : W.LeftFraction ψ₁.Y' ψ₂.Y'
hα : ψ₂.s ≫ α.s = ψ₁.s ≫ α.f
⊢ φ.s ≫ ψ₂.f ≫ α.s = φ.s ≫ { Y' := α.Y', f := ψ₁.f ≫ α.f, f' := ψ₂.f ≫ α.s, s := ψ₂.s ≫ α.s, hs := ⋯ }.f'

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Localization

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
A : Type w
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : W.IsCompatibleWithShift A
a : A
⊢ W ≤ W

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map L ⋯
α : W.LeftFraction φ.Y' φ'.Y'
hα : { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.f ≫ α.s = { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.s ≫ α.f
ψ : W.LeftFraction₂ X Y := { Y' := α.Y', f := φ.f ≫ α.f, f' := φ'.f ≫ α.s, s := φ'.s ≫ α.s, hs := ⋯ }
⊢ IsIso (L.map φ'.s ≫ L.map α.s)

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map L ⋯
α : W.LeftFraction φ.Y' φ'.Y'
hα : { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.f ≫ α.s = { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.s ≫ α.f
ψ : W.LeftFraction₂ X Y := { Y' := α.Y', f := φ.f ≫ α.f, f' := φ'.f ≫ α.s, s := φ'.s ≫ α.s, hs := ⋯ }
⊢ IsIso (L.map φ'.s ≫ L.map α.s)