awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
⊢ φ.fst (W := W).map (W := W) L ⋯ = ψ.fst (W := W).map (W := W) L ⋯ ∧
      φ.snd (W := W).map (W := W) L ⋯ = ψ.snd (W := W).map (W := W) L ⋯ ↔
    LeftFraction₂Rel (W := W) φ ψ
have simp : LeftFractionRel (W := W) (φ.fst (W := W)) (ψ.fst (W := W)) ∧
    LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W)) ↔
  LeftFraction₂Rel (W := W) φ ψ
Tactic: simp only [LeftFraction.map_eq_iff L W]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
⊢ LeftFractionRel (W := W) (φ.fst (W := W)) (ψ.fst (W := W)) ∧
      LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W)) ↔
    LeftFraction₂Rel (W := W) φ ψ
have mp : LeftFractionRel (W := W) (φ.fst (W := W)) (ψ.fst (W := W)) ∧
    LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W)) →
  LeftFraction₂Rel (W := W) φ ψ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
mp :
  LeftFractionRel (W := W) (φ.fst (W := W)) (ψ.fst (W := W)) ∧
      LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W)) →
    LeftFraction₂Rel (W := W) φ ψ
⊢ LeftFractionRel (W := W) (φ.fst (W := W)) (ψ.fst (W := W)) ∧
      LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W)) ↔
    LeftFraction₂Rel (W := W) φ ψ
have mpr : LeftFraction₂Rel (W := W) φ ψ →
  LeftFractionRel (W := W) (φ.fst (W := W)) (ψ.fst (W := W)) ∧
    LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
h : LeftFractionRel (W := W) (φ.fst (W := W)) (ψ.fst (W := W))
h' : LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W))
⊢ LeftFraction₂Rel (W := W) φ ψ
have mp : ∀ (Z : C) (t₁ : φ.fst (W := W).Y' (W := W) ⟶ Z) (t₂ : ψ.fst (W := W).Y' (W := W) ⟶ Z)
  (hst : φ.fst (W := W).s (W := W) ≫ t₁ = ψ.fst (W := W).s (W := W) ≫ t₂)
  (hft : φ.fst (W := W).f (W := W) ≫ t₁ = ψ.fst (W := W).f (W := W) ≫ t₂) (ht : W (φ.fst (W := W).s (W := W) ≫ t₁)),
  LeftFraction₂Rel (W := W) φ ψ
Tactic: obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
h' : LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W))
Z : C
t₁ : φ.fst (W := W).Y' (W := W) ⟶ Z
t₂ : ψ.fst (W := W).Y' (W := W) ⟶ Z
hst : φ.fst (W := W).s (W := W) ≫ t₁ = ψ.fst (W := W).s (W := W) ≫ t₂
hft : φ.fst (W := W).f (W := W) ≫ t₁ = ψ.fst (W := W).f (W := W) ≫ t₂
ht : W (φ.fst (W := W).s (W := W) ≫ t₁)
⊢ LeftFraction₂Rel (W := W) φ ψ
have mp : ∀ (Z' : C) (t₁' : φ.snd (W := W).Y' (W := W) ⟶ Z') (t₂' : ψ.snd (W := W).Y' (W := W) ⟶ Z')
  (hst' : φ.snd (W := W).s (W := W) ≫ t₁' = ψ.snd (W := W).s (W := W) ≫ t₂')
  (hft' : φ.snd (W := W).f (W := W) ≫ t₁' = ψ.snd (W := W).f (W := W) ≫ t₂')
  (ht' : W (φ.snd (W := W).s (W := W) ≫ t₁')), LeftFraction₂Rel (W := W) φ ψ
Tactic: obtain ⟨Z', t₁', t₂', hst', hft', ht'⟩ := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
⊢ LeftFraction₂Rel (W := W) φ ψ
have mp : ∀ (α : W.LeftFraction Z Z')
  (hα :
    (RightFraction.mk (W := W) (φ.s (W := W) ≫ t₁) ht (φ.s (W := W) ≫ t₁')).f (W := W) ≫ α.s (W := W) =
      (RightFraction.mk (W := W) (φ.s (W := W) ≫ t₁) ht (φ.s (W := W) ≫ t₁')).s (W := W) ≫ α.f (W := W)),
  LeftFraction₂Rel (W := W) φ ψ
Tactic: have ⟨α, hα⟩ := (RightFraction.mk _ ht (φ.s ≫ t₁')).exists_leftFraction
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα :
  (RightFraction.mk (W := W) (φ.s (W := W) ≫ t₁) ht (φ.s (W := W) ≫ t₁')).f (W := W) ≫ α.s (W := W) =
    (RightFraction.mk (W := W) (φ.s (W := W) ≫ t₁) ht (φ.s (W := W) ≫ t₁')).s (W := W) ≫ α.f (W := W)
⊢ LeftFraction₂Rel (W := W) φ ψ
have hα₁ : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
Tactic: simp only [Category.assoc] at hα
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
⊢ LeftFraction₂Rel (W := W) φ ψ
have mp : ∀ (Z'' : C) (u : α.Y' (W := W) ⟶ Z'') (hu : W u) (fac : (t₁' ≫ α.s (W := W)) ≫ u = (t₁ ≫ α.f (W := W)) ≫ u),
  LeftFraction₂Rel (W := W) φ ψ
Tactic: obtain ⟨Z'', u, hu, fac⟩ := HasLeftCalculusOfFractions.ext _ _ _ φ.hs hα
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
Z'' : C
u : α.Y' (W := W) ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s (W := W)) ≫ u = (t₁ ≫ α.f (W := W)) ≫ u
⊢ ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
have rw : φ.s (W := W) ≫ t₁ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
Tactic: rw [← reassoc_of% hst, ← reassoc_of% hα, ← reassoc_of% hst']
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
Z'' : C
u : α.Y' (W := W) ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s (W := W)) ≫ u = (t₁ ≫ α.f (W := W)) ≫ u
rw : φ.s (W := W) ≫ t₁ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
⊢ ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
have rw₁ : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
Tactic: rw [← reassoc_of% hst, ← reassoc_of% hα, ← reassoc_of% hst']
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
Z'' : C
u : α.Y' (W := W) ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s (W := W)) ≫ u = (t₁ ≫ α.f (W := W)) ≫ u
rw : φ.s (W := W) ≫ t₁ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
rw₁ : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
⊢ ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
have rw₂ : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u = φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u
Tactic: rw [← reassoc_of% hst, ← reassoc_of% hα, ← reassoc_of% hst']
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
Z'' : C
u : α.Y' (W := W) ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s (W := W)) ≫ u = (t₁ ≫ α.f (W := W)) ≫ u
⊢ LeftFraction₂Rel (W := W) φ ψ
have hα' : ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
Tactic: have hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u := by
      rw [← reassoc_of% hst, ← reassoc_of% hα, ← reassoc_of% hst']
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
Z'' : C
u : α.Y' (W := W) ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s (W := W)) ≫ u = (t₁ ≫ α.f (W := W)) ≫ u
hα' : ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
⊢ LeftFraction₂Rel (W := W) φ ψ
have mp : ∀ (Z''' : C) (u' : Z'' ⟶ Z''') (hu' : W u') (fac' : (t₂ ≫ α.f (W := W) ≫ u) ≫ u' = (t₂' ≫ α.s (W := W) ≫ u) ≫ u'),
  LeftFraction₂Rel (W := W) φ ψ
Tactic: obtain ⟨Z''', u', hu', fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ ψ.hs hα'
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
Z'' : C
u : α.Y' (W := W) ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s (W := W)) ≫ u = (t₁ ≫ α.f (W := W)) ≫ u
hα' : ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac' : (t₂ ≫ α.f (W := W) ≫ u) ≫ u' = (t₂' ≫ α.s (W := W) ≫ u) ≫ u'
⊢ LeftFraction₂Rel (W := W) φ ψ
have fac₁ : t₁' ≫ α.s (W := W) ≫ u = t₁ ≫ α.f (W := W) ≫ u
Tactic: simp only [Category.assoc] at fac fac'
Cleared hypotheses: fac, fac'
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
Z'' : C
u : α.Y' (W := W) ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s (W := W)) ≫ u = (t₁ ≫ α.f (W := W)) ≫ u
hα' : ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac' : (t₂ ≫ α.f (W := W) ≫ u) ≫ u' = (t₂' ≫ α.s (W := W) ≫ u) ≫ u'
fac₁ : t₁' ≫ α.s (W := W) ≫ u = t₁ ≫ α.f (W := W) ≫ u
⊢ LeftFraction₂Rel (W := W) φ ψ
have fac'₁ : t₂ ≫ α.f (W := W) ≫ u ≫ u' = t₂' ≫ α.s (W := W) ≫ u ≫ u'
Tactic: simp only [Category.assoc] at fac fac'
Cleared hypotheses: fac, fac'
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
Z'' : C
u : α.Y' (W := W) ⟶ Z''
hu : W u
hα' : ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac : t₁' ≫ α.s (W := W) ≫ u = t₁ ≫ α.f (W := W) ≫ u
fac' : t₂ ≫ α.f (W := W) ≫ u ≫ u' = t₂' ≫ α.s (W := W) ≫ u ≫ u'
⊢ LeftFraction₂Rel (W := W) φ ψ
have mp : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
Tactic: refine ⟨Z''', t₁' ≫ α.s ≫ u ≫ u', t₂' ≫ α.s ≫ u ≫ u', ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
Z'' : C
u : α.Y' (W := W) ⟶ Z''
hu : W u
hα' : ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac : t₁' ≫ α.s (W := W) ≫ u = t₁ ≫ α.f (W := W) ≫ u
fac' : t₂ ≫ α.f (W := W) ≫ u ≫ u' = t₂' ≫ α.s (W := W) ≫ u ≫ u'
mp : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
⊢ LeftFraction₂Rel (W := W) φ ψ
have mp₁ : φ.f (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.f (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
Tactic: refine ⟨Z''', t₁' ≫ α.s ≫ u ≫ u', t₂' ≫ α.s ≫ u ≫ u', ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
Z'' : C
u : α.Y' (W := W) ⟶ Z''
hu : W u
hα' : ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac : t₁' ≫ α.s (W := W) ≫ u = t₁ ≫ α.f (W := W) ≫ u
fac' : t₂ ≫ α.f (W := W) ≫ u ≫ u' = t₂' ≫ α.s (W := W) ≫ u ≫ u'
mp : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
mp₁ : φ.f (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.f (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
⊢ LeftFraction₂Rel (W := W) φ ψ
have mp₂ : φ.f' (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.f' (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
Tactic: refine ⟨Z''', t₁' ≫ α.s ≫ u ≫ u', t₂' ≫ α.s ≫ u ≫ u', ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
Z'' : C
u : α.Y' (W := W) ⟶ Z''
hu : W u
hα' : ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac : t₁' ≫ α.s (W := W) ≫ u = t₁ ≫ α.f (W := W) ≫ u
fac' : t₂ ≫ α.f (W := W) ≫ u ≫ u' = t₂' ≫ α.s (W := W) ≫ u ≫ u'
mp : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
mp₁ : φ.f (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.f (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
mp₂ : φ.f' (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.f' (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
⊢ LeftFraction₂Rel (W := W) φ ψ
have mp₃ : W (φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u')
Tactic: refine ⟨Z''', t₁' ≫ α.s ≫ u ≫ u', t₂' ≫ α.s ≫ u ≫ u', ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
Z'' : C
u : α.Y' (W := W) ⟶ Z''
hu : W u
hα' : ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac : t₁' ≫ α.s (W := W) ≫ u = t₁ ≫ α.f (W := W) ≫ u
fac' : t₂ ≫ α.f (W := W) ≫ u ≫ u' = t₂' ≫ α.s (W := W) ≫ u ≫ u'
⊢ φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
have mp : ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u' = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
Tactic: rw [reassoc_of% hst']