awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X_1 Y_1 S_1 : Scheme
f_1 : X_1 ⟶ S_1
inst : LocallyOfFiniteType f_1
X Y S : Scheme
f : X ⟶ Y
inst_1 : LocallyQuasiFinite f
inst_2 : LocallyOfFiniteType f
inst_3 : IsSeparated f
inst_4 : QuasiCompact f
⊢ IsOpenImmersion (Y := Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
have h : Eq (α := X ⟶ Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
  (X.topIso.inv ≫ Iso.inv (X.isoOfEq sorry) ≫ (Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f)
Tactic: convert!
    (inferInstance :
      IsOpenImmersion
        (X.topIso.inv ≫
          (X.isoOfEq f.quasiFiniteLocus_eq_top).inv ≫
            f.quasiFiniteLocus.ι ≫ f.toNormalization)) using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
inst_1 : LocallyQuasiFinite f
⊢ IsFinite f
have this : IsIso (Y := Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
Tactic: have : IsIso f.toNormalization :=
    (isIso_iff_isOpenImmersion_and_surjective _).mpr ⟨inferInstance, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
inst_1 : LocallyQuasiFinite f
this : IsIso (Y := Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
⊢ IsFinite f
have refine : IsIntegralHom f
Tactic: refine (IsFinite.iff_isIntegralHom_and_locallyOfFiniteType _).mpr ⟨?_, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
inst_1 : LocallyQuasiFinite f
this : IsIso (Y := Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
⊢ IsIntegralHom f
have rw : IsIntegralHom
  (CategoryStruct.comp (Y := Scheme.Hom.normalization f) (Scheme.Hom.toNormalization f)
    (Scheme.Hom.fromNormalization f))
Tactic: rw [← f.toNormalization_fromNormalization]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
⊢ @IsFinite = @IsProper ⊓ @LocallyQuasiFinite
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), IsFinite x_2 ↔ (@IsProper ⊓ @LocallyQuasiFinite) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔ IsProper f ∧ Mono f
have this : Mono f → IsProper f → LocallyQuasiFinite f
Tactic: have (_ : Mono f) (_ : IsProper f) : LocallyQuasiFinite f := inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
this : Mono f → IsProper f → LocallyQuasiFinite f
⊢ IsClosedImmersion f ↔ IsProper f ∧ Mono f
have rw : (IsProper f ∧ LocallyQuasiFinite f) ∧ Mono f ↔ IsProper f ∧ Mono f
Tactic: rw [IsClosedImmersion.iff_isFinite_and_mono, IsFinite.iff_isProper_and_locallyQuasiFinite]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
⊢ @IsClosedImmersion = @IsProper ⊓ MorphismProperty.monomorphisms Scheme
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1),
  IsClosedImmersion x_2 ↔ (@IsProper ⊓ MorphismProperty.monomorphisms Scheme) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
⊢ ∃ (V : Y.Opens), y ∈ V ∧ IsFinite (f ∣_ V)
have refine_1 : y ∈ V
Tactic: refine ⟨V, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
refine_1 : y ∈ V
⊢ ∃ (V : Y.Opens), y ∈ V ∧ IsFinite (f ∣_ V)
have refine_2 : IsFinite (f ∣_ V)
Tactic: refine ⟨V, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
⊢ y ∈ V
have refine_1 : ∀ (x : ↥X), f x = y → Scheme.Hom.QuasiFiniteAt f x
Tactic: suffices ∀ x, f x = y → f.QuasiFiniteAt x by simpa [V, not_imp_not]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
x : ↥X
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) (⇑f) (singleton (α := ↥Y) (f x : ↥Y)))
⊢ Scheme.Hom.QuasiFiniteAt f x
have this : Finite.{u + 1} ↥(Scheme.Hom.fiber f (f x))
Tactic: have : Finite (f.fiber (f x)) := (f.fiberHomeo (f x)).finite_iff.mpr ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
⊢ IsFinite (f ∣_ V)
have refine_2 : LocallyQuasiFinite (f ∣_ V)
Tactic: suffices LocallyQuasiFinite (f ∣_ V) from .of_isProper_of_locallyQuasiFinite _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
⊢ LocallyQuasiFinite (f ∣_ V)
have refine_2 : Scheme.Hom.quasiFiniteLocus (f ∣_ V) = ⊤
Tactic: rw [← Scheme.Hom.quasiFiniteLocus_eq_top_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
⊢ Scheme.Hom.quasiFiniteLocus (f ∣_ V) = ⊤
have refine_2 : ∀ (x : ↥(↑(f ⁻¹ᵁ V) : Scheme)),
  x ∈ (↑(Scheme.Hom.quasiFiniteLocus (f ∣_ V)) : Set ↥(↑(f ⁻¹ᵁ V) : Scheme)) ↔ x ∈ (↑⊤ : Set ↥(↑(f ⁻¹ᵁ V) : Scheme))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
x : ↥(↑(f ⁻¹ᵁ V) : Scheme)
⊢ Scheme.Hom.QuasiFiniteAt f ((f ⁻¹ᵁ V).ι x)
have by_contra : ∀ (H : ¬Scheme.Hom.QuasiFiniteAt f ((f ⁻¹ᵁ V).ι x)), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
x : ↥(↑(f ⁻¹ᵁ V) : Scheme)
⊢ x ∈ (↑(Scheme.Hom.quasiFiniteLocus (f ∣_ V)) : Set ↥(↑(f ⁻¹ᵁ V) : Scheme)) ↔ x ∈ (↑⊤ : Set ↥(↑(f ⁻¹ᵁ V) : Scheme))
have this : Scheme.Hom.QuasiFiniteAt f ((f ⁻¹ᵁ V).ι x)
Tactic: have : f.QuasiFiniteAt ((f ⁻¹ᵁ V).ι x) := by by_contra H; exact x.2 ⟨_, H, by simp⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsProper f
y : ↥Y
hx : Set.Finite (α := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f) : Set ↥X)ᶜ)ᶜ, is_open' := ⋯ }
x : ↥(↑(f ⁻¹ᵁ V) : Scheme)
this : Scheme.Hom.QuasiFiniteAt f ((f ⁻¹ᵁ V).ι x)
⊢ x ∈ (↑(Scheme.Hom.quasiFiniteLocus (f ∣_ V)) : Set ↥(↑(f ⁻¹ᵁ V) : Scheme)) ↔ x ∈ (↑⊤ : Set ↥(↑(f ⁻¹ᵁ V) : Scheme))
have this₁ : Scheme.Hom.QuasiFiniteAt (f ∣_ V) x
Tactic: rw [← Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, ← morphismRestrict_ι,
      Scheme.Hom.quasiFiniteAt_comp_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (hypothesis)
Goal:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : Set.Finite (α := ↥Y) (Set.image (α := ↥X) (⇑f) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}))
inst : IsProper (f ≫ g)
inst_1 : IsSeparated g
inst_2 : LocallyOfFiniteType g
⊢ ∃ (U : S.Opens), s ∈ U ∧ IsFinite ((Scheme.Hom.imageι f ≫ g) ∣_ U)
have this : IsProper f
Tactic: have : IsProper f := .of_comp f g
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : Set.Finite (α := ↥Y) (Set.image (α := ↥X) (⇑f) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}))
inst : IsProper (f ≫ g)
inst_1 : IsSeparated g
inst_2 : LocallyOfFiniteType g
this : IsProper f
⊢ IsProper (Scheme.Hom.imageι f ≫ g)
have suffices : UniversallyClosed (Scheme.Hom.imageι f ≫ g)
Tactic: suffices UniversallyClosed (f.imageι ≫ g) from ⟨⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : Set.Finite (α := ↥Y) (Set.image (α := ↥X) (⇑f) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}))
inst : IsProper (f ≫ g)
inst_1 : IsSeparated g
inst_2 : LocallyOfFiniteType g
this : IsProper f
⊢ UniversallyClosed (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f ≫ g)
have rw : UniversallyClosed (f ≫ g)
Tactic: rw [Scheme.Hom.toImage_imageι_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (hypothesis)
Goal:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : Set.Finite (α := ↥Y) (Set.image (α := ↥X) (⇑f) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}))
inst : IsProper (f ≫ g)
inst_1 : IsSeparated g
inst_2 : LocallyOfFiniteType g
this : IsProper f
⊢ UniversallyClosed (Scheme.Hom.imageι f ≫ g)
have this₁ : UniversallyClosed (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f ≫ g)
Tactic: have : UniversallyClosed (f.toImage ≫ f.imageι ≫ g) := by
      rw [Scheme.Hom.toImage_imageι_assoc]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (hypothesis)
Goal:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : Set.Finite (α := ↥Y) (Set.image (α := ↥X) (⇑f) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}))
inst : IsProper (f ≫ g)
inst_1 : IsSeparated g
inst_2 : LocallyOfFiniteType g
this : IsProper f
⊢ ∃ (U : S.Opens), s ∈ U ∧ IsFinite ((Scheme.Hom.imageι f ≫ g) ∣_ U)
have this₁ : IsProper (Scheme.Hom.imageι f ≫ g)
Tactic: have : IsProper (f.imageι ≫ g) := by
    suffices UniversallyClosed (f.imageι ≫ g) from ⟨⟩
    have : UniversallyClosed (f.toImage ≫ f.imageι ≫ g) := by
      rw [Scheme.Hom.toImage_imageι_assoc]; infer_instance
    refine .of_comp_surjective f.toImage _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : Set.Finite (α := ↥Y) (Set.image (α := ↥X) (⇑f) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}))
inst : IsProper (f ≫ g)
inst_1 : IsSeparated g
inst_2 : LocallyOfFiniteType g
this_1 : IsProper f
this : IsProper (Scheme.Hom.imageι f ≫ g)
⊢ ∃ (U : S.Opens), s ∈ U ∧ IsFinite ((Scheme.Hom.imageι f ≫ g) ∣_ U)
have refine : Set.Finite (α := ↥(Scheme.Hom.image f)) (Set.preimage (β := ↥S) ⇑(Scheme.Hom.imageι f ≫ g) {s})
Tactic: refine exists_isFinite_morphismRestrict_of_finite_preimage_singleton _ _ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : Set.Finite (α := ↥Y) (Set.image (α := ↥X) (⇑f) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}))
inst : IsProper (f ≫ g)
inst_1 : IsSeparated g
inst_2 : LocallyOfFiniteType g
this_1 : IsProper f
this : IsProper (Scheme.Hom.imageι f ≫ g)
⊢ Set.Finite (α := ↥(Scheme.Hom.image f)) (Set.preimage (β := ↥S) ⇑(Scheme.Hom.imageι f ≫ g) {s})
have refine : Subset (α := Set ↥Y)
  (Set.image (α := ↥(Scheme.Hom.image f)) (⇑(Scheme.Hom.imageι f))
    (Set.preimage (β := ↥S) ⇑(Scheme.Hom.imageι f ≫ g) {s}))
  (Set.image (α := ↥X) (⇑f) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}))
Tactic: refine .of_finite_image (f := f.imageι) (H.subset ?_) f.imageι.isClosedEmbedding.injective.injOn
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : Set.Finite (α := ↥Y) (Set.image (α := ↥X) (⇑f) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}))
inst : IsProper (f ≫ g)
inst_1 : IsSeparated g
inst_2 : LocallyOfFiniteType g
this_1 : IsProper f
this : IsProper (Scheme.Hom.imageι f ≫ g)
x : ↥(Scheme.Hom.image f)
hx : Membership.mem (γ := Set ↥(Scheme.Hom.image f)) (Set.preimage (β := ↥S) ⇑(Scheme.Hom.imageι f ≫ g) {s}) x
⊢ Membership.mem (α := ↥Y) (γ := Set ↥Y) (Set.image (α := ↥X) (⇑f) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}))
    ((Scheme.Hom.imageι f) x : ↥Y)
have obtain : ∀ (x : ↥X)
  (hx :
    Membership.mem (α := ↥(Scheme.Hom.image f)) (γ := Set ↥(Scheme.Hom.image f))
      (Set.preimage (β := ↥S) ⇑(Scheme.Hom.imageι f ≫ g) {s}) ((Scheme.Hom.toImage f) x : ↥(Scheme.Hom.image f))),
  Membership.mem (α := ↥Y) (γ := Set ↥Y) (Set.image (α := ↥X) (⇑f) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}))
    ((Scheme.Hom.imageι f) ((Scheme.Hom.toImage f) x : ↥(Scheme.Hom.image f)) : ↥Y)
Tactic: obtain ⟨x, rfl⟩ := f.toImage.surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ZariskisMainTheorem (goal)
Goal:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : Set.Finite (α := ↥Y) (Set.image (α := ↥X) (⇑f) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}))
inst : IsProper (f ≫ g)
inst_1 : IsSeparated g
inst_2 : LocallyOfFiniteType g
this_1 : IsProper f
this : IsProper (Scheme.Hom.imageι f ≫ g)
x : ↥X
hx :
  Membership.mem (α := ↥(Scheme.Hom.image f)) (γ := Set ↥(Scheme.Hom.image f))
    (Set.preimage (β := ↥S) ⇑(Scheme.Hom.imageι f ≫ g) {s}) ((Scheme.Hom.toImage f) x : ↥(Scheme.Hom.image f))
⊢ Membership.mem (α := ↥Y) (γ := Set ↥Y) (Set.image (α := ↥X) (⇑f) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}))
    ((Scheme.Hom.imageι f) ((Scheme.Hom.toImage f) x : ↥(Scheme.Hom.image f)) : ↥Y)
have refine : Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}) x
Tactic: refine ⟨x, ?_, by simp [← Scheme.Hom.comp_apply]⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ objD X (n + 1) ≫ objD X n = 0
have dsimp : Eq.{v_1 + 1} (α := X _⦋n + 1 + 1⦌ ⟶ X _⦋n⦌)
  (CategoryStruct.comp (Y := X _⦋n + 1⦌) (∑ i : Fin (n + 1 + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i)
    (∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i))
  0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq.{v_1 + 1} (α := X _⦋n + 1 + 1⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n + 1⦌) (∑ i : Fin (n + 1 + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i)
      (∑ i : Fin (n + 2), HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i))
    0
have simp : Eq.{v_1 + 1} (α := X _⦋n + 1 + 1⦌ ⟶ X _⦋n⦌)
  (∑ x ∈ SProd.sprod (α := Finset (Fin (n + 2))) (β := Finset (Fin (n + 1 + 2))) Finset.univ Finset.univ,
    (HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) • X.δ x.2) ≫ (HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ) • X.δ x.1))
  0
Tactic: simp only [comp_sum, sum_comp, ← Finset.sum_product']
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
⊢ Eq.{v_1 + 1} (α := X _⦋n + 1 + 1⦌ ⟶ X _⦋n⦌)
    (∑ x ∈ SProd.sprod (α := Finset (Fin (n + 2))) (β := Finset (Fin (n + 1 + 2))) Finset.univ Finset.univ,
      (HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) • X.δ x.2) ≫ (HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ) • X.δ x.1))
    0
have rw : Eq.{v_1 + 1} (α := X _⦋n + 1 + 1⦌ ⟶ X _⦋n⦌)
  (∑ i ∈ S, (HPow.hPow (α := ℤ) (-1) (↑i.2 : ℕ) • X.δ i.2) ≫ (HPow.hPow (α := ℤ) (-1) (↑i.1 : ℕ) • X.δ i.1))
  (∑ x ∈ Sᶜ, -(HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) • X.δ x.2) ≫ (HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ) • X.δ x.1))
Tactic: rw [Finset.univ_product_univ, ← Finset.sum_add_sum_compl S, ← eq_neg_iff_add_eq_zero,
    ← Finset.sum_neg_distrib]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
⊢ Eq.{v_1 + 1} (α := X _⦋n + 1 + 1⦌ ⟶ X _⦋n⦌)
    (∑ i ∈ S, (HPow.hPow (α := ℤ) (-1) (↑i.2 : ℕ) • X.δ i.2) ≫ (HPow.hPow (α := ℤ) (-1) (↑i.1 : ℕ) • X.δ i.1))
    (∑ x ∈ Sᶜ, -(HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) • X.δ x.2) ≫ (HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ) • X.δ x.1))
have hi : ∀ (a : P) (ha : a ∈ S), φ a ha ∈ Sᶜ
Tactic: apply Finset.sum_bij φ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
hi : ∀ (a : P) (ha : a ∈ S), φ a ha ∈ Sᶜ
⊢ Eq.{v_1 + 1} (α := X _⦋n + 1 + 1⦌ ⟶ X _⦋n⦌)
    (∑ i ∈ S, (HPow.hPow (α := ℤ) (-1) (↑i.2 : ℕ) • X.δ i.2) ≫ (HPow.hPow (α := ℤ) (-1) (↑i.1 : ℕ) • X.δ i.1))
    (∑ x ∈ Sᶜ, -(HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) • X.δ x.2) ≫ (HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ) • X.δ x.1))
have i_inj : ∀ (a₁ : P) (ha₁ : a₁ ∈ S) (a₂ : P) (ha₂ : a₂ ∈ S), φ a₁ ha₁ = φ a₂ ha₂ → a₁ = a₂
Tactic: apply Finset.sum_bij φ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
hi : ∀ (a : P) (ha : a ∈ S), φ a ha ∈ Sᶜ
i_inj : ∀ (a₁ : P) (ha₁ : a₁ ∈ S) (a₂ : P) (ha₂ : a₂ ∈ S), φ a₁ ha₁ = φ a₂ ha₂ → a₁ = a₂
⊢ Eq.{v_1 + 1} (α := X _⦋n + 1 + 1⦌ ⟶ X _⦋n⦌)
    (∑ i ∈ S, (HPow.hPow (α := ℤ) (-1) (↑i.2 : ℕ) • X.δ i.2) ≫ (HPow.hPow (α := ℤ) (-1) (↑i.1 : ℕ) • X.δ i.1))
    (∑ x ∈ Sᶜ, -(HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) • X.δ x.2) ≫ (HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ) • X.δ x.1))
have i_surj : ∀ b ∈ Sᶜ, ∃ (a : P) (ha : a ∈ S), φ a ha = b
Tactic: apply Finset.sum_bij φ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
hi : ∀ (a : P) (ha : a ∈ S), φ a ha ∈ Sᶜ
i_inj : ∀ (a₁ : P) (ha₁ : a₁ ∈ S) (a₂ : P) (ha₂ : a₂ ∈ S), φ a₁ ha₁ = φ a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ Sᶜ, ∃ (a : P) (ha : a ∈ S), φ a ha = b
⊢ Eq.{v_1 + 1} (α := X _⦋n + 1 + 1⦌ ⟶ X _⦋n⦌)
    (∑ i ∈ S, (HPow.hPow (α := ℤ) (-1) (↑i.2 : ℕ) • X.δ i.2) ≫ (HPow.hPow (α := ℤ) (-1) (↑i.1 : ℕ) • X.δ i.1))
    (∑ x ∈ Sᶜ, -(HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) • X.δ x.2) ≫ (HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ) • X.δ x.1))
have h : ∀ (a : P) (ha : a ∈ S),
  (HPow.hPow (α := ℤ) (-1) (↑a.2 : ℕ) • X.δ a.2) ≫ (HPow.hPow (α := ℤ) (-1) (↑a.1 : ℕ) • X.δ a.1) =
    -(HPow.hPow (α := ℤ) (-1) (↑(φ a ha).2 : ℕ) • X.δ (φ a ha).2) ≫
        (HPow.hPow (α := ℤ) (-1) (↑(φ a ha).1 : ℕ) • X.δ (φ a ha).1)
Tactic: apply Finset.sum_bij φ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
ij : P
hij : ij ∈ S
⊢ φ ij hij ∈ Sᶜ
have hi : ∀ (hij : (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)), ¬(↑ij.1 : ℕ) + 1 ≤ (↑ij.2 : ℕ)
Tactic: simp_rw [S, φ, Finset.compl_filter, Finset.mem_filter_univ, Fin.val_succ,
      Fin.val_castLT] at hij ⊢
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ (i, j) = (i', j')
have i_inj : i = i' ∧ j = j'
Tactic: rw [Prod.mk_inj]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ Sᶜ
⊢ ∃ (a : P) (ha : a ∈ S), φ a ha = (i', j')
have hij'₁ : (↑i' : ℕ) < (↑j' : ℕ)
Tactic: simp_rw [S, Finset.compl_filter, Finset.mem_filter_univ, not_le] at hij'
Cleared hypotheses: hij'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (↑i' : ℕ) < (↑j' : ℕ)
⊢ ∃ (a : P) (ha : a ∈ S), φ a ha = (i', j')
have i_surj : j' ≠ 0
Tactic: refine ⟨(j'.pred <| ?_, Fin.castSucc i'), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (↑i' : ℕ) < (↑j' : ℕ)
i_surj : j' ≠ 0
⊢ ∃ (a : P) (ha : a ∈ S), φ a ha = (i', j')
have i_surj₁ : (j'.pred sorry, i'.castSucc) ∈ S
Tactic: refine ⟨(j'.pred <| ?_, Fin.castSucc i'), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)}
φ : (ij : P) → ij ∈ S → P := fun (ij : P) (hij : ij ∈ S) ↦ (ij.2.castLT ⋯, ij.1.succ)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (↑i' : ℕ) < (↑j' : ℕ)
i_surj : j' ≠ 0
i_surj₁ : (j'.pred ⋯, i'.castSucc) ∈ S
⊢ ∃ (a : P) (ha : a ∈ S), φ a ha = (i', j')
have i_surj₂ : φ (j'.pred sorry, i'.castSucc) sorry = (i', j')
Tactic: refine ⟨(j'.pred <| ?_, Fin.castSucc i'), ?_, ?_⟩