awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (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
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
⊢ F.map f₀ = F.map f₁
have obtain : ∀ (P : Precylinder.{v_1, u_1} X) (h : P.LeftHomotopy f₀ f₁) (hπ : W P.π), F.map f₀ = F.map f₁
Tactic: obtain ⟨P, h, hπ⟩ := hr f₀ f₁ hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (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
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
P : Precylinder.{v_1, u_1} X
h : P.LeftHomotopy f₀ f₁
hπ : W P.π
⊢ F.map f₀ = F.map f₁
have simp : F.map P.i₀ ≫ F.map h.h = F.map P.i₁ ≫ F.map h.h
Tactic: simp only [← h.h₀, ← h.h₁, Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (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
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
P : Precylinder.{v_1, u_1} X
h : P.LeftHomotopy f₀ f₁
hπ : W P.π
⊢ F.map P.i₀ ≫ F.map h.h = F.map P.i₁ ≫ F.map h.h
have e_a : F.map P.i₀ = F.map P.i₁
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (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
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
P : Precylinder.{v_1, u_1} X
h : P.LeftHomotopy f₀ f₁
hπ : W P.π
⊢ F.map P.i₀ = F.map P.i₁
have this : IsIso (F.map P.π)
Tactic: have := hF _ hπ
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (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
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} (Quotient r) E
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ F₁ = F₂
have h_obj : ∀ (X : Quotient r), F₁.obj X = F₂.obj X
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (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
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} (Quotient r) E
h : functor r ⋙ F₁ = functor r ⋙ F₂
h_obj : ∀ (X : Quotient r), F₁.obj X = F₂.obj X
⊢ F₁ = F₂
have h_map : autoParam (∀ (X Y : Quotient r) (f : X ⟶ Y), F₁.map f = eqToHom sorry ≫ F₂.map f ≫ eqToHom sorry) Functor.ext._auto_1
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
⊢ (functor r).IsLocalization W
have h₁ : Localization.StrictUniversalPropertyFixedTarget (functor r) W (Quotient r)
Tactic: apply Functor.IsLocalization.mk'
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
h₁ : Localization.StrictUniversalPropertyFixedTarget (functor r) W (Quotient r)
⊢ (functor r).IsLocalization W
have h₂ : Localization.StrictUniversalPropertyFixedTarget (functor r) W W.Localization
Tactic: apply Functor.IsLocalization.mk'
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (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
inst_2 : L.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
F : Functor.{v_1, v_2, u_1, u_2} (Quotient L.homRel) D := Quotient.lift L.homRel L ⋯
x x_1 : C
f : x ⟶ x_1
hf : W f
⊢ IsIso ((Quotient.functor L.homRel).map f)
have this : IsIso (F.map ((Quotient.functor L.homRel).map f))
Tactic: have : IsIso (F.map ((Quotient.functor L.homRel).map f)) := hW _ hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (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
inst_2 : L.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
F : Functor.{v_1, v_2, u_1, u_2} (Quotient L.homRel) D := Quotient.lift L.homRel L ⋯
⊢ L.IsLocalization W
have hW' : W.IsInvertedBy (Quotient.functor L.homRel)
Tactic: have hW' : W.IsInvertedBy (Quotient.functor L.homRel) := fun _ _ f hf ↦ by
    have : IsIso (F.map ((Quotient.functor L.homRel).map f)) := hW _ hf
    apply isIso_of_reflects_iso _ F
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (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
inst_2 : L.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
F : Functor.{v_1, v_2, u_1, u_2} (Quotient L.homRel) D := Quotient.lift L.homRel L ⋯
hW' : W.IsInvertedBy (Quotient.functor L.homRel)
⊢ L.IsLocalization W
have this : (Quotient.functor L.homRel).IsLocalization W
Tactic: have := Quotient.isLocalization_functor L.homRel W hW' hr
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (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
inst_2 : L.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y),
    L.map f₀ = L.map f₁ → ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι
⊢ L.IsLocalization W
have rw : L.op.IsLocalization W.op
Tactic: rw [← Functor.IsLocalization.op_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (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
inst_2 : L.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y),
    L.map f₀ = L.map f₁ → ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι
⊢ L.op.IsLocalization W.op
have refine : ∀ (X Y : Cᵒᵖ) (f₀ f₁ : X ⟶ Y) (hf : L.op.map f₀ = L.op.map f₁),
  ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W.op P.π
Tactic: refine isLocalization_of_essSurj_of_full_of_exists_cylinders L.op W.op hW.op
    (fun X Y f₀ f₁ hf ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (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
inst_2 : L.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y),
    L.map f₀ = L.map f₁ → ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι
X Y : Cᵒᵖ
f₀ f₁ : X ⟶ Y
hf : L.op.map f₀ = L.op.map f₁
⊢ ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W.op P.π
have obtain : ∀ (P : PrepathObject.{v_1, u_1} (Opposite.unop X)) (h : P.RightHomotopy f₀.unop f₁.unop) (hι : W P.ι),
  ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W.op P.π
Tactic: obtain ⟨P, h, hι⟩ := hr f₀.unop f₁.unop (Quiver.Hom.op_inj hf)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.OfQuotient (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : Congruence r
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι
X Y : C
f₀ f₁ : X ⟶ Y
hf : (functor r).map f₀ = (functor r).map f₁
⊢ ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι
have hf₁ : r f₀ f₁
Tactic: rw [functor_map_eq_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Opposite (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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
h : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L W Eᵒᵖ
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
this : F₁.rightOp = F₂.rightOp
⊢ F₁ = F₂
have rw : F₁.rightOp.leftOp = F₂
Tactic: rw [← F₁.rightOp_leftOp_eq, ← F₂.rightOp_leftOp_eq, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Opposite (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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
h : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L W Eᵒᵖ
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
this : F₁.rightOp = F₂.rightOp
rw : F₁.rightOp.leftOp = F₂
⊢ F₁ = F₂
have rw₁ : F₁.rightOp.leftOp = F₂.rightOp.leftOp
Tactic: rw [← F₁.rightOp_leftOp_eq, ← F₂.rightOp_leftOp_eq, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Opposite (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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
h : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L W Eᵒᵖ
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
this : F₁.rightOp = F₂.rightOp
rw : F₁.rightOp.leftOp = F₂
rw₁ : F₁.rightOp.leftOp = F₂.rightOp.leftOp
⊢ F₁ = F₂
have rw₂ : F₂.rightOp.leftOp = F₂.rightOp.leftOp
Tactic: rw [← F₁.rightOp_leftOp_eq, ← F₂.rightOp_leftOp_eq, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Opposite (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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
h : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L W Eᵒᵖ
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
⊢ F₁ = F₂
have suffices : F₁.rightOp = F₂.rightOp
Tactic: suffices F₁.rightOp = F₂.rightOp by
      rw [← F₁.rightOp_leftOp_eq, ← F₂.rightOp_leftOp_eq, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Opposite (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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
h : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L W Eᵒᵖ
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
⊢ F₁.rightOp = F₂.rightOp
have eq' : (L.op ⋙ F₁).rightOp = (L.op ⋙ F₂).rightOp
Tactic: have eq' := congr_arg Functor.rightOp eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Opposite (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_1 : Functor.{v_1, v_2, u_1, u_2} C D
W_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L_1.IsLocalization W_1
L : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ Dᵒᵖ
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
inst_3 : L.IsLocalization W
this : CatCommSq (Equivalence.functor (opOpEquivalence C)) L.op L.unop (Equivalence.functor (opOpEquivalence D))
x x_1 : C
x_2 : x ⟶ x_1
hf : W.unop x_2
⊢ IsIso (L.unop.map x_2)
have this₁ : IsIso (L.map x_2.op)
Tactic: have := Localization.inverts L W _ hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Opposite (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_1 : Functor.{v_1, v_2, u_1, u_2} C D
W_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L_1.IsLocalization W_1
L : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ Dᵒᵖ
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
inst_3 : L.IsLocalization W
this_1 : CatCommSq (Equivalence.functor (opOpEquivalence C)) L.op L.unop (Equivalence.functor (opOpEquivalence D))
x x_1 : C
x_2 : x ⟶ x_1
hf : W.unop x_2
this : IsIso (L.map x_2.op)
⊢ IsIso (L.unop.map x_2)
have dsimp : IsIso (L.map x_2.op).unop
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Opposite (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
X Y : Cᵒᵖ
w : X ⟶ Y
hw : W.op w
⊢ (isoOfHom L.op W.op w hw).unop = isoOfHom L W w.unop hw
have w₁ : (isoOfHom L.op W.op w hw).unop.hom = (isoOfHom L W w.unop hw).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
Goal:
⊢ ∀ {J : Type w} [Finite J] {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J), (W j).ContainsIdentities]
    [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
have of_equiv : ∀ {α β : Type w} (a : α ≃ β),
  (∀ {C : α → Type u₁} {D : α → Type u₂} [inst : (j : α) → Category.{v₁, u₁} (C j)]
      [inst_1 : (j : α) → Category.{v₂, u₂} (D j)] (L : (j : α) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
      (W : (j : α) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : α), (W j).ContainsIdentities]
      [∀ (j : α), (L j).IsLocalization (W j)],
      (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)) →
    ∀ {C : β → Type u₁} {D : β → Type u₂} [inst : (j : β) → Category.{v₁, u₁} (C j)]
      [inst_1 : (j : β) → Category.{v₂, u₂} (D j)] (L : (j : β) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
      (W : (j : β) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : β), (W j).ContainsIdentities]
      [∀ (j : β), (L j).IsLocalization (W j)],
      (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
Tactic: apply Finite.induction_empty_option
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
Goal:
of_equiv :
  ∀ {α β : Type w} (a : α ≃ β),
    (∀ {C : α → Type u₁} {D : α → Type u₂} [inst : (j : α) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : α) → Category.{v₂, u₂} (D j)] (L : (j : α) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
        (W : (j : α) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : α), (W j).ContainsIdentities]
        [∀ (j : α), (L j).IsLocalization (W j)],
        (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)) →
      ∀ {C : β → Type u₁} {D : β → Type u₂} [inst : (j : β) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : β) → Category.{v₂, u₂} (D j)] (L : (j : β) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
        (W : (j : β) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : β), (W j).ContainsIdentities]
        [∀ (j : β), (L j).IsLocalization (W j)],
        (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
⊢ ∀ {J : Type w} [Finite J] {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J), (W j).ContainsIdentities]
    [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
have h_empty : ∀ {C : PEmpty.{w + 1} → Type u₁} {D : PEmpty.{w + 1} → Type u₂} [inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)]
  [inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)]
  (L : (j : PEmpty.{w + 1}) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
  (W : (j : PEmpty.{w + 1}) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities]
  [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
  (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
Tactic: apply Finite.induction_empty_option
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
Goal:
of_equiv :
  ∀ {α β : Type w} (a : α ≃ β),
    (∀ {C : α → Type u₁} {D : α → Type u₂} [inst : (j : α) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : α) → Category.{v₂, u₂} (D j)] (L : (j : α) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
        (W : (j : α) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : α), (W j).ContainsIdentities]
        [∀ (j : α), (L j).IsLocalization (W j)],
        (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)) →
      ∀ {C : β → Type u₁} {D : β → Type u₂} [inst : (j : β) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : β) → Category.{v₂, u₂} (D j)] (L : (j : β) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
        (W : (j : β) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : β), (W j).ContainsIdentities]
        [∀ (j : β), (L j).IsLocalization (W j)],
        (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
h_empty :
  ∀ {C : PEmpty.{w + 1} → Type u₁} {D : PEmpty.{w + 1} → Type u₂}
    [inst : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)] [inst_1 : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)]
    (L : (j : PEmpty.{w + 1}) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : PEmpty.{w + 1}) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities]
    [∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
⊢ ∀ {J : Type w} [Finite J] {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : J) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J), (W j).ContainsIdentities]
    [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
have h_option : ∀ {α : Type w} [Fintype α],
  (∀ {C : α → Type u₁} {D : α → Type u₂} [inst : (j : α) → Category.{v₁, u₁} (C j)]
      [inst_1 : (j : α) → Category.{v₂, u₂} (D j)] (L : (j : α) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
      (W : (j : α) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : α), (W j).ContainsIdentities]
      [∀ (j : α), (L j).IsLocalization (W j)],
      (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)) →
    ∀ {C : Option α → Type u₁} {D : Option α → Type u₂} [inst : (j : Option α) → Category.{v₁, u₁} (C j)]
      [inst_1 : (j : Option α) → Category.{v₂, u₂} (D j)] (L : (j : Option α) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
      (W : (j : Option α) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : Option α), (W j).ContainsIdentities]
      [∀ (j : Option α), (L j).IsLocalization (W j)],
      (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
Tactic: apply Finite.induction_empty_option
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Pi (goal)
Goal:
J₁ J₂ : Type w
e : J₁ ≃ J₂
hJ₁ :
  ∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
    [inst_4 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → Functor.{v₁, v₂, u₁, u₂} (C j) (D j))
    (W : (j : J₁) → MorphismProperty.{v₁, u₁} (C j)) [∀ (j : J₁), (W j).ContainsIdentities]
    [∀ (j : J₁), (L j).IsLocalization (W j)],
    (Functor.pi (C := C) (D := D) L).IsLocalization (MorphismProperty.pi (C := C) W)
C₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst_1 : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → Functor.{v₁, v₂, u₁, u₂} (C₂ j) (D₂ j)
W₂ : (j : J₂) → MorphismProperty.{v₁, u₁} (C₂ j)
inst_2 : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst_3 : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
L₁ : (j : J₁) → Functor.{v₁, v₂, u₁, u₂} (C₂ ((e : (a : J₁) → J₂) j)) (D₂ ((e : (a : J₁) → J₂) j)) :=
  fun (j : J₁) ↦ L₂ ((e : (a : J₁) → J₂) j)
E : ((j : J₁) → C₂ ((e : (a : J₁) → J₂) j)) ≌ (i : J₂) → C₂ i := Pi.equivalenceOfEquiv C₂ e
E' : ((j : J₁) → D₂ ((e : (a : J₁) → J₂) j)) ≌ (i : J₂) → D₂ i := Pi.equivalenceOfEquiv D₂ e
⊢ (Functor.pi (C := C₂) (D := D₂) L₂).IsLocalization (MorphismProperty.pi (C := C₂) W₂)
have of_equiv : ∀
  (this :
    CatCommSq E.functor
      (Functor.pi (C := fun (j : J₁) ↦ C₂ ((e : (a : J₁) → J₂) j)) (D := fun (i : J₁) ↦ D₂ ((e : (a : J₁) → J₂) i)) L₁)
      (Functor.pi (C := C₂) (D := D₂) L₂) E'.functor),
  (Functor.pi (C := C₂) (D := D₂) L₂).IsLocalization (MorphismProperty.pi (C := C₂) W₂)
Tactic: haveI : CatCommSq E.functor (Functor.pi L₁) (Functor.pi L₂) E'.functor :=
      (CatCommSq.hInvEquiv E (Functor.pi L₁) (Functor.pi L₂) E').symm ⟨Iso.refl _⟩