awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.op Y ⟶ Opposite.op B
g : Opposite.op X ⟶ Opposite.op A
sq : CommSq f p.op i.op g
⊢ sq.HasLift
have simp : CommSq.HasLift (g := f.unop) sorry
Tactic: simp only [CommSq.HasLift.iff_unop, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty.{v_1, u_1} (C := Cᵒᵖ) (A := A) (B := B) (X := X) (Y := Y) i p
f : Opposite.unop Y ⟶ Opposite.unop B
g : Opposite.unop X ⟶ Opposite.unop A
sq : CommSq f p.unop i.unop g
⊢ sq.HasLift
have rw : sorry.HasLift
Tactic: rw [CommSq.HasLift.iff_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty.{v_1, u_1} (C := Cᵒᵖ) (A := A) (B := B) (X := X) (Y := Y) i p
f : Opposite.unop Y ⟶ Opposite.unop B
g : Opposite.unop X ⟶ Opposite.unop A
sq : CommSq f p.unop i.unop g
⊢ ⋯.HasLift
have simp : CommSq.HasLift (g := f.op) sorry
Tactic: simp only [Quiver.Hom.op_unop]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst_1 : HasLiftingProperty i p
inst_2 : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
⊢ sq.HasLift
have fac : f ≫ p = (i ≫ i') ≫ g
Tactic: have fac := sq.w
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst_1 : HasLiftingProperty i p
inst_2 : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = (i ≫ i') ≫ g
⊢ sq.HasLift
have fac₁ : f ≫ p = i ≫ i' ≫ g
Tactic: rw [assoc] at fac
Cleared hypotheses: fac
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i' p
have rw : HasLiftingProperty (Arrow.Hom.left e.inv ≫ i ≫ Arrow.Hom.right e.hom) p
Tactic: rw [Arrow.iso_w' e]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i p'
have rw : HasLiftingProperty i (Arrow.Hom.left e.inv ≫ p ≫ Arrow.Hom.right e.hom)
Tactic: rw [Arrow.iso_w' e]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
⊢ HasLiftingProperty i p ↔ HasLiftingProperty i' p
have mp : HasLiftingProperty i p → HasLiftingProperty i' p
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
mp : HasLiftingProperty i p → HasLiftingProperty i' p
⊢ HasLiftingProperty i p ↔ HasLiftingProperty i' p
have mpr : HasLiftingProperty i' p → HasLiftingProperty i p
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
⊢ HasLiftingProperty i p ↔ HasLiftingProperty i p'
have mp : HasLiftingProperty i p → HasLiftingProperty i p'
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
mp : HasLiftingProperty i p → HasLiftingProperty i p'
⊢ HasLiftingProperty i p ↔ HasLiftingProperty i p'
have mpr : HasLiftingProperty i p' → HasLiftingProperty i p
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W Z' W' : C
g : Z ⟶ W
g' : Z' ⟶ W'
h : RetractArrow g' g
f : X ⟶ Y
inst_1 : HasLiftingProperty g f
u : Z' ⟶ X
v : W' ⟶ Y
sq : CommSq u g' f v
⊢ sq.HasLift
have sq' : CommSq (Arrow.Hom.left h.r ≫ u) g f (Arrow.Hom.right h.r ≫ v)
Tactic: have sq' : CommSq (h.r.left ≫ u) g f (h.r.right ≫ v) := by simp only [Arrow.mk_left,
      Arrow.mk_right, Category.assoc, sq.w, Arrow.w_mk_right_assoc, Arrow.mk_hom, CommSq.mk]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
h : RetractArrow f' f
g : Z ⟶ W
inst_1 : HasLiftingProperty g f
u : Z ⟶ X'
v : W ⟶ Y'
sq : CommSq u g f' v
⊢ (u ≫ Arrow.Hom.left h.i) ≫ f = g ≫ v ≫ Arrow.Hom.right h.i
have rw : (u ≫ Arrow.Hom.left h.i) ≫ f = (g ≫ v) ≫ Arrow.Hom.right h.i
Tactic: rw [← Category.assoc, ← sq.w, Category.assoc, RetractArrow.i_w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
h : RetractArrow f' f
g : Z ⟶ W
inst_1 : HasLiftingProperty g f
u : Z ⟶ X'
v : W ⟶ Y'
sq : CommSq u g f' v
rw : (u ≫ Arrow.Hom.left h.i) ≫ f = (g ≫ v) ≫ Arrow.Hom.right h.i
⊢ (u ≫ Arrow.Hom.left h.i) ≫ f = g ≫ v ≫ Arrow.Hom.right h.i
have rw₁ : (u ≫ Arrow.Hom.left h.i) ≫ f = (u ≫ f') ≫ Arrow.Hom.right h.i
Tactic: rw [← Category.assoc, ← sq.w, Category.assoc, RetractArrow.i_w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
h : RetractArrow f' f
g : Z ⟶ W
inst_1 : HasLiftingProperty g f
u : Z ⟶ X'
v : W ⟶ Y'
sq : CommSq u g f' v
rw : (u ≫ Arrow.Hom.left h.i) ≫ f = (g ≫ v) ≫ Arrow.Hom.right h.i
rw₁ : (u ≫ Arrow.Hom.left h.i) ≫ f = (u ≫ f') ≫ Arrow.Hom.right h.i
⊢ (u ≫ Arrow.Hom.left h.i) ≫ f = g ≫ v ≫ Arrow.Hom.right h.i
have rw₂ : u ≫ Arrow.Hom.left h.i ≫ f = (u ≫ f') ≫ Arrow.Hom.right h.i
Tactic: rw [← Category.assoc, ← sq.w, Category.assoc, RetractArrow.i_w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
h : RetractArrow f' f
g : Z ⟶ W
inst_1 : HasLiftingProperty g f
u : Z ⟶ X'
v : W ⟶ Y'
sq : CommSq u g f' v
rw : (u ≫ Arrow.Hom.left h.i) ≫ f = (g ≫ v) ≫ Arrow.Hom.right h.i
rw₁ : (u ≫ Arrow.Hom.left h.i) ≫ f = (u ≫ f') ≫ Arrow.Hom.right h.i
rw₂ : u ≫ Arrow.Hom.left h.i ≫ f = (u ≫ f') ≫ Arrow.Hom.right h.i
⊢ (u ≫ Arrow.Hom.left h.i) ≫ f = g ≫ v ≫ Arrow.Hom.right h.i
have rw₃ : u ≫ f' ≫ Arrow.Hom.right h.i = (u ≫ f') ≫ Arrow.Hom.right h.i
Tactic: rw [← Category.assoc, ← sq.w, Category.assoc, RetractArrow.i_w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
h : RetractArrow f' f
g : Z ⟶ W
inst_1 : HasLiftingProperty g f
u : Z ⟶ X'
v : W ⟶ Y'
sq : CommSq u g f' v
rw : (u ≫ Arrow.Hom.left h.i) ≫ f = (g ≫ v) ≫ Arrow.Hom.right h.i
rw₁ : (u ≫ Arrow.Hom.left h.i) ≫ f = (u ≫ f') ≫ Arrow.Hom.right h.i
rw₂ : u ≫ Arrow.Hom.left h.i ≫ f = (u ≫ f') ≫ Arrow.Hom.right h.i
rw₃ : u ≫ f' ≫ Arrow.Hom.right h.i = (u ≫ f') ≫ Arrow.Hom.right h.i
⊢ (u ≫ Arrow.Hom.left h.i) ≫ f = g ≫ v ≫ Arrow.Hom.right h.i
have rw₄ : u ≫ f' ≫ Arrow.Hom.right h.i = u ≫ f' ≫ Arrow.Hom.right h.i
Tactic: rw [← Category.assoc, ← sq.w, Category.assoc, RetractArrow.i_w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i p ↔ ∀ (φ : mk i ⟶ mk p), Nonempty.{v_1 + 1} (LiftStruct φ)
have mp : HasLiftingProperty i p → ∀ (φ : mk i ⟶ mk p), Nonempty.{v_1 + 1} (LiftStruct φ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
mp : HasLiftingProperty i p → ∀ (φ : mk i ⟶ mk p), Nonempty.{v_1 + 1} (LiftStruct φ)
⊢ HasLiftingProperty i p ↔ ∀ (φ : mk i ⟶ mk p), Nonempty.{v_1 + 1} (LiftStruct φ)
have mpr : (∀ (φ : mk i ⟶ mk p), Nonempty.{v_1 + 1} (LiftStruct φ)) → HasLiftingProperty i p
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
φ : mk i ⟶ mk p
⊢ Nonempty.{v_1 + 1} (LiftStruct φ)
have sq : CommSq (Hom.left φ) i p (Hom.right φ)
Tactic: have sq : CommSq φ.left i p φ.right := CommSq.mk φ.w
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
⊢ (s ≫ u) ≫ g' = f ≫ t ≫ v
have rw : (s ≫ u) ≫ g' = (f ≫ t) ≫ v
Tactic: rw [← Category.assoc, ← h.w, Category.assoc, Category.assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
rw : (s ≫ u) ≫ g' = (f ≫ t) ≫ v
⊢ (s ≫ u) ≫ g' = f ≫ t ≫ v
have rw₁ : (s ≫ u) ≫ g' = (s ≫ g) ≫ v
Tactic: rw [← Category.assoc, ← h.w, Category.assoc, Category.assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
rw : (s ≫ u) ≫ g' = (f ≫ t) ≫ v
rw₁ : (s ≫ u) ≫ g' = (s ≫ g) ≫ v
⊢ (s ≫ u) ≫ g' = f ≫ t ≫ v
have rw₂ : s ≫ u ≫ g' = (s ≫ g) ≫ v
Tactic: rw [← Category.assoc, ← h.w, Category.assoc, Category.assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
rw : (s ≫ u) ≫ g' = (f ≫ t) ≫ v
rw₁ : (s ≫ u) ≫ g' = (s ≫ g) ≫ v
rw₂ : s ≫ u ≫ g' = (s ≫ g) ≫ v
⊢ (s ≫ u) ≫ g' = f ≫ t ≫ v
have rw₃ : s ≫ u ≫ g' = s ≫ g ≫ v
Tactic: rw [← Category.assoc, ← h.w, Category.assoc, Category.assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
rw : (s ≫ u) ≫ g' = (f ≫ t) ≫ v
rw₁ : (s ≫ u) ≫ g' = (s ≫ g) ≫ v
rw₂ : s ≫ u ≫ g' = (s ≫ g) ≫ v
rw₃ : s ≫ u ≫ g' = s ≫ g ≫ v
⊢ (s ≫ u) ≫ g' = f ≫ t ≫ v
have rw₄ : s ≫ g ≫ v = s ≫ g ≫ v
Tactic: rw [← Category.assoc, ← h.w, Category.assoc, Category.assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
⊢ sq.HasLift
have w : (s ≫ u) ≫ g' = f ≫ t ≫ v
Tactic: have w : (s ≫ u) ≫ g' = f ≫ (t ≫ v) := by
      rw [← Category.assoc, ← h.w, Category.assoc, Category.assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ s ≫ u = f ≫ ⋯.lift
have rw : s ≫ u = s ≫ u
Tactic: rw [CommSq.fac_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ g ≫ h.desc u ⋯.lift ⋯ ≫ g' = g ≫ v
have rw : u ≫ g' = g ≫ v
Tactic: rw [h.inl_desc_assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
rw : u ≫ g' = g ≫ v
⊢ g ≫ h.desc u ⋯.lift ⋯ ≫ g' = g ≫ v
have rw₁ : g ≫ v = g ≫ v
Tactic: rw [h.inl_desc_assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ t ≫ h.desc u ⋯.lift ⋯ ≫ g' = t ≫ v
have rw : sorry.lift ≫ g' = t ≫ v
Tactic: rw [h.inr_desc_assoc, CommSq.fac_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst_1 : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
rw : ⋯.lift ≫ g' = t ≫ v
⊢ t ≫ h.desc u ⋯.lift ⋯ ≫ g' = t ≫ v
have rw₁ : t ≫ v = t ≫ v
Tactic: rw [h.inr_desc_assoc, CommSq.fac_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
⊢ (u ≫ s) ≫ g = f' ≫ v ≫ t
have rw : u ≫ s ≫ g = f' ≫ v ≫ t
Tactic: rw [Category.assoc, h.toCommSq.w, ← Category.assoc, ← Category.assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
rw : u ≫ s ≫ g = f' ≫ v ≫ t
⊢ (u ≫ s) ≫ g = f' ≫ v ≫ t
have rw₁ : u ≫ f ≫ t = f' ≫ v ≫ t
Tactic: rw [Category.assoc, h.toCommSq.w, ← Category.assoc, ← Category.assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
rw : u ≫ s ≫ g = f' ≫ v ≫ t
rw₁ : u ≫ f ≫ t = f' ≫ v ≫ t
⊢ (u ≫ s) ≫ g = f' ≫ v ≫ t
have rw₂ : (u ≫ f) ≫ t = f' ≫ v ≫ t
Tactic: rw [Category.assoc, h.toCommSq.w, ← Category.assoc, ← Category.assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
rw : u ≫ s ≫ g = f' ≫ v ≫ t
rw₁ : u ≫ f ≫ t = f' ≫ v ≫ t
rw₂ : (u ≫ f) ≫ t = f' ≫ v ≫ t
⊢ (u ≫ s) ≫ g = f' ≫ v ≫ t
have rw₃ : (u ≫ f) ≫ t = (f' ≫ v) ≫ t
Tactic: rw [Category.assoc, h.toCommSq.w, ← Category.assoc, ← Category.assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
rw : u ≫ s ≫ g = f' ≫ v ≫ t
rw₁ : u ≫ f ≫ t = f' ≫ v ≫ t
rw₂ : (u ≫ f) ≫ t = f' ≫ v ≫ t
rw₃ : (u ≫ f) ≫ t = (f' ≫ v) ≫ t
⊢ (u ≫ s) ≫ g = f' ≫ v ≫ t
have rw₄ : (f' ≫ v) ≫ t = (f' ≫ v) ≫ t
Tactic: rw [Category.assoc, h.toCommSq.w, ← Category.assoc, ← Category.assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
⊢ sq.HasLift
have w : (u ≫ s) ≫ g = f' ≫ v ≫ t
Tactic: have w : (u ≫ s) ≫ g = f' ≫ v ≫ t := by
      rw [Category.assoc, h.toCommSq.w, ← Category.assoc, ← Category.assoc, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ ⋯.lift ≫ g = v ≫ t
have rw : v ≫ t = v ≫ t
Tactic: rw [CommSq.fac_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ (f' ≫ h.lift ⋯.lift v ⋯) ≫ s = u ≫ s
have rw : f' ≫ h.lift sorry.lift v sorry ≫ s = u ≫ s
Tactic: rw [Category.assoc, h.lift_fst, CommSq.fac_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
rw : f' ≫ h.lift ⋯.lift v ⋯ ≫ s = u ≫ s
⊢ (f' ≫ h.lift ⋯.lift v ⋯) ≫ s = u ≫ s
have rw₁ : f' ≫ sorry.lift = u ≫ s
Tactic: rw [Category.assoc, h.lift_fst, CommSq.fac_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
rw : f' ≫ h.lift ⋯.lift v ⋯ ≫ s = u ≫ s
rw₁ : f' ≫ ⋯.lift = u ≫ s
⊢ (f' ≫ h.lift ⋯.lift v ⋯) ≫ s = u ≫ s
have rw₂ : u ≫ s = u ≫ s
Tactic: rw [Category.assoc, h.lift_fst, CommSq.fac_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ (f' ≫ h.lift ⋯.lift v ⋯) ≫ f = u ≫ f
have rw : f' ≫ h.lift sorry.lift v sorry ≫ f = u ≫ f
Tactic: rw [Category.assoc, h.lift_snd, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
rw : f' ≫ h.lift ⋯.lift v ⋯ ≫ f = u ≫ f
⊢ (f' ≫ h.lift ⋯.lift v ⋯) ≫ f = u ≫ f
have rw₁ : f' ≫ v = u ≫ f
Tactic: rw [Category.assoc, h.lift_snd, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst_1 : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
rw : f' ≫ h.lift ⋯.lift v ⋯ ≫ f = u ≫ f
rw₁ : f' ≫ v = u ≫ f
⊢ (f' ≫ h.lift ⋯.lift v ⋯) ≫ f = u ≫ f
have rw₂ : f' ≫ v = f' ≫ v
Tactic: rw [Category.assoc, h.lift_snd, sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z W : C
f_1 : X_1 ⟶ Y_1
s : X_1 ⟶ Z
g : Z ⟶ W
t_1 : Y_1 ⟶ W
J : Type u_2
A B : J → C
inst_1 : HasProduct.{u_2, v_1, u_1} A
inst_2 : HasProduct.{u_2, v_1, u_1} B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst_3 : ∀ (j : J), HasLiftingProperty p (f j)
t : X ⟶ piObj.{u_2, v_1, u_1} A
b : Y ⟶ piObj.{u_2, v_1, u_1} B
sq : CommSq t p (Limits.Pi.map f) b
j : J
⊢ (t ≫ Pi.π A j) ≫ f j = p ≫ b ≫ Pi.π B j
have rw : (t ≫ Pi.π A j) ≫ f j = CategoryStruct.comp (Y := piObj.{u_2, v_1, u_1} B) (t ≫ Limits.Pi.map f) (Pi.π B j)
Tactic: rw [← Category.assoc, ← sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z W : C
f_1 : X_1 ⟶ Y_1
s : X_1 ⟶ Z
g : Z ⟶ W
t_1 : Y_1 ⟶ W
J : Type u_2
A B : J → C
inst_1 : HasProduct.{u_2, v_1, u_1} A
inst_2 : HasProduct.{u_2, v_1, u_1} B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst_3 : ∀ (j : J), HasLiftingProperty p (f j)
t : X ⟶ piObj.{u_2, v_1, u_1} A
b : Y ⟶ piObj.{u_2, v_1, u_1} B
sq : CommSq t p (Limits.Pi.map f) b
⊢ sq.HasLift
have sq' : ∀ (j : J), CommSq (t ≫ Pi.π A j) p (f j) (b ≫ Pi.π B j)
Tactic: have sq' (j : J) :
        CommSq (t ≫ Pi.π _ j) p (f j) (b ≫ Pi.π _ j) :=
      ⟨by rw [← Category.assoc, ← sq.w]; simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Limits (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z W : C
f_1 : X_1 ⟶ Y_1
s : X_1 ⟶ Z
g : Z ⟶ W
t_1 : Y_1 ⟶ W
J : Type u_2
A B : J → C
inst_1 : HasCoproduct.{u_2, v_1, u_1} A
inst_2 : HasCoproduct.{u_2, v_1, u_1} B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst_3 : ∀ (j : J), HasLiftingProperty (f j) p
t : sigmaObj.{u_2, v_1, u_1} A ⟶ X
b : sigmaObj.{u_2, v_1, u_1} B ⟶ Y
sq : CommSq t (Limits.Sigma.map f) p b
⊢ sq.HasLift
have sq' : ∀ (j : J), CommSq (Sigma.ι A j ≫ t) (f j) p (Sigma.ι B j ≫ b)
Tactic: have sq' (j : J) :
        CommSq (Sigma.ι _ j ≫ t) (f j) p (Sigma.ι _ j ≫ b) :=
      ⟨by simp [sq.w]⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
X₁ X₂ X₃ X₄ : Over.{v, u} S
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : CommSq t l r b
inst_1 :
  HasLift (A := X₁.left) (B := X₃.left) (X := X₂.left) (Y := X₄.left) (f := Over.Hom.left t) (i := Over.Hom.left l)
    (p := Over.Hom.left r) (g := Over.Hom.left b) ⋯
sq' : CommSq (Over.Hom.left t) (Over.Hom.left l) (Over.Hom.left r) (Over.Hom.left b) := ⋯
⊢ sq'.lift ≫ X₂.hom = X₃.hom
have rw : sq'.lift ≫ X₂.hom = Over.Hom.left b ≫ X₄.hom
Tactic: rw [← Over.w b, ← sq'.fac_right_assoc, Over.w r]
-- Lean 4 proof step from Mathlib.CategoryTheory.LiftingProperties.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
X₁ X₂ X₃ X₄ : Over.{v, u} S
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : CommSq t l r b
inst_1 :
  HasLift (A := X₁.left) (B := X₃.left) (X := X₂.left) (Y := X₄.left) (f := Over.Hom.left t) (i := Over.Hom.left l)
    (p := Over.Hom.left r) (g := Over.Hom.left b) ⋯
sq' : CommSq (Over.Hom.left t) (Over.Hom.left l) (Over.Hom.left r) (Over.Hom.left b) := ⋯
rw : sq'.lift ≫ X₂.hom = Over.Hom.left b ≫ X₄.hom
⊢ sq'.lift ≫ X₂.hom = X₃.hom
have rw₁ : sq'.lift ≫ X₂.hom = sq'.lift ≫ Over.Hom.left r ≫ X₄.hom
Tactic: rw [← Over.w b, ← sq'.fac_right_assoc, Over.w r]