awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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
⊢ IsProper f

Tactic:
have : IsProper f := .of_comp f g
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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
suffices : UniversallyClosed (Scheme.Hom.imageι f ≫ g)
⊢ IsProper (Scheme.Hom.imageι f ≫ g)

Tactic:
suffices UniversallyClosed (f.imageι ≫ g) from ⟨⟩
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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
rw : UniversallyClosed (f ≫ g)
⊢ UniversallyClosed (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f ≫ g)

Tactic:
rw [Scheme.Hom.toImage_imageι_assoc]

Premises used: AlgebraicGeometry.Scheme.Hom.toImage_imageι_assoc
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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 (f ≫ g)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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)

Tactic:
have : UniversallyClosed (f.toImage ≫ f.imageι ≫ g) := by
      rw [Scheme.Hom.toImage_imageι_assoc]; infer_instance
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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 : UniversallyClosed (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f ≫ g)
⊢ UniversallyClosed (Scheme.Hom.imageι f ≫ g)

Tactic:
.of_comp_surjective f.toImage _

Premises used: AlgebraicGeometry.UniversallyClosed.of_comp_surjective, AlgebraicGeometry.Scheme.Hom.toImage
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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 : UniversallyClosed (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f ≫ g)
⊢ UniversallyClosed (Scheme.Hom.imageι f ≫ g)

Tactic:
refine .of_comp_surjective f.toImage _
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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)

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 _
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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)

Tactic:
exists_isFinite_morphismRestrict_of_finite_preimage_singleton _ _ ?_

Premises used: AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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)
refine : Set.Finite (α := ↥(Scheme.Hom.image f)) (Set.preimage (β := ↥S) ⇑(Scheme.Hom.imageι f ≫ g) {s})
⊢ ∃ (U : S.Opens), s ∈ U ∧ IsFinite ((Scheme.Hom.imageι f ≫ g) ∣_ U)

Tactic:
refine exists_isFinite_morphismRestrict_of_finite_preimage_singleton _ _ ?_

Premises used: AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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})

Tactic:
.of_finite_image (f := f.imageι) (H.subset ?_) f.imageι.isClosedEmbedding.injective.injOn

Premises used: AlgebraicGeometry.Scheme.Hom.imageι, Function.Injective.injOn, Set.Finite.subset, Topology.IsClosedEmbedding.toIsEmbedding, Set.Finite.of_finite_image, AlgebraicGeometry.Scheme.Hom.isClosedEmbedding, Topology.IsEmbedding.injective
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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)
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}))
⊢ Set.Finite (α := ↥(Scheme.Hom.image f)) (Set.preimage (β := ↥S) ⇑(Scheme.Hom.imageι f ≫ g) {s})

Tactic:
refine .of_finite_image (f := f.imageι) (H.subset ?_) f.imageι.isClosedEmbedding.injective.injOn
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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
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)
⊢ Membership.mem (α := ↥Y) (γ := Set ↥Y) (Set.image (α := ↥X) (⇑f) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}))
    ((Scheme.Hom.imageι f) x : ↥Y)

Tactic:
obtain ⟨x, rfl⟩ := f.toImage.surjective x

Premises used: AlgebraicGeometry.Scheme.Hom.toImage, AlgebraicGeometry.Scheme.Hom.surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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))
⊢ Eq (α := ↥Y) (f x : ↥Y) ((Scheme.Hom.imageι f) ((Scheme.Hom.toImage f) x : ↥(Scheme.Hom.image f)) : ↥Y)

Tactic:
simp [← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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))
refine : Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}) x
⊢ 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:
refine ⟨x, ?_, by simp [← Scheme.Hom.comp_apply]⟩
-- Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem
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 (γ := Set ↥X) (Set.preimage (β := ↥S) ⇑(f ≫ g) {s}) x

Tactic:
simpa [← Scheme.Hom.comp_apply, -Scheme.Hom.comp_base] using hx

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.Hom.comp_base
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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 : ℕ
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
⊢ objD X (n + 1) ≫ objD X n = 0

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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 : ℕ
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
⊢ 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:
simp only [comp_sum, sum_comp, ← Finset.sum_product']

Premises used: CategoryTheory.Preadditive.sum_comp, Finset.sum_product', CategoryTheory.Preadditive.comp_sum
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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 : ℕ)}
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))
⊢ 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:
rw [Finset.univ_product_univ, ← Finset.sum_add_sum_compl S, ← eq_neg_iff_add_eq_zero,
    ← Finset.sum_neg_distrib]

Premises used: Finset.univ_product_univ, eq_neg_iff_add_eq_zero, Finset.sum_neg_distrib, Finset.sum_add_sum_compl
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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
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)
⊢ 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:
apply Finset.sum_bij φ

Premises used: Finset.sum_bij
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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
hi : ∀ (hij : (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)), ¬(↑ij.1 : ℕ) + 1 ≤ (↑ij.2 : ℕ)
⊢ φ ij hij ∈ Sᶜ

Tactic:
simp_rw [S, φ, Finset.compl_filter, Finset.mem_filter_univ, Fin.val_succ,
      Fin.val_castLT] at hij ⊢

Premises used: Finset.mem_filter_univ, Fin.val_succ, Finset.compl_filter, Fin.val_castLT
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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_1 : Membership.mem (γ := Finset P) {ij : P | (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)} ij
hij : (↑ij.2 : ℕ) ≤ (↑ij.1 : ℕ)
⊢ ¬(↑ij.1 : ℕ) + 1 ≤ (↑ij.2 : ℕ)

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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_inj : i = i' ∧ j = j'
⊢ (i, j) = (i', j')

Tactic:
rw [Prod.mk_inj]

Premises used: Prod.mk_inj
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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 = i'

Tactic:
simpa [φ] using congr_arg Prod.snd h

Premises used: congr_arg, Prod.snd
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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'
⊢ j = j'

Tactic:
simpa [φ, Fin.castSucc_castLT] using congr_arg Fin.castSucc (congr_arg Prod.fst h)

Premises used: Prod.fst, congr_arg, Fin.castSucc, Fin.castSucc_castLT
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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 = i' ∧ j = j'

Tactic:
exact ⟨by simpa [φ] using congr_arg Prod.snd h,
      by simpa [φ, Fin.castSucc_castLT] using congr_arg Fin.castSucc (congr_arg Prod.fst h)⟩
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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' : ℕ) < (↑j' : ℕ)

Tactic:
simp_rw [S, Finset.compl_filter, Finset.mem_filter_univ, not_le] at hij'

Premises used: not_le, Finset.mem_filter_univ, Finset.compl_filter
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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')

Tactic:
⟨(j'.pred <| ?_, Fin.castSucc i'), ?_, ?_⟩

Premises used: Fin.pred, Prod.mk, Exists.intro, Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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
i_surj₂ : φ (j'.pred ⋯, i'.castSucc) ⋯ = (i', j')
⊢ ∃ (a : P) (ha : a ∈ S), φ a ha = (i', j')

Tactic:
refine ⟨(j'.pred <| ?_, Fin.castSucc i'), ?_, ?_⟩
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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' : ℕ)
⊢ j' ≠ 0

Tactic:
exact_mod_cast hij'.ne_zero

Premises used: LT.lt.ne_zero
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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' : ℕ)
⊢ (j'.pred ⋯, i'.castSucc) ∈ S

Tactic:
simpa [S] using Nat.le_sub_one_of_lt hij'

Premises used: Nat.le_sub_one_of_lt
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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' : ℕ)
⊢ φ (j'.pred ⋯, i'.castSucc) ⋯ = (i', j')

Tactic:
simp only [φ, Fin.castLT_castSucc, Fin.succ_pred]

Premises used: Fin.castLT_castSucc, Fin.succ_pred
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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
h :
  (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) =
    -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ) • X.δ (φ (i, j) hij).2) ≫
        (HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) • X.δ (φ (i, j) hij).1)
⊢ (HPow.hPow (α := ℤ) (-1) (↑(i, j).2 : ℕ) • X.δ (i, j).2) ≫ (HPow.hPow (α := ℤ) (-1) (↑(i, j).1 : ℕ) • X.δ (i, j).1) =
    -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ) • X.δ (φ (i, j) hij).2) ≫
        (HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) • X.δ (φ (i, j) hij).1)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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
h :
  (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (↑j : ℕ)) • X.δ j ≫ X.δ i =
    -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ)) •
      X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1
⊢ (HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • X.δ j) ≫ (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • X.δ i) =
    -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ) • X.δ (φ (i, j) hij).2) ≫
        (HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) • X.δ (φ (i, j) hij).1)

Tactic:
simp only [zsmul_comp, comp_zsmul, smul_smul, ← neg_smul]

Premises used: neg_smul, smul_smul, CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.Preadditive.zsmul_comp
-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
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
h :
  HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (↑j : ℕ) =
    -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ))
h₁ : X.δ j ≫ X.δ i = X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1
⊢ (HPow.hPow (α := ℤ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤ) (-1) (↑j : ℕ)) • X.δ j ≫ X.δ i =
    -(HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).1 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑(φ (i, j) hij).2 : ℕ)) •
      X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1

Tactic:
congr 1