awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (goal)
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex.{v_1, u_4, u_1} C c
x : Subtype e₂.BoundaryGE
i₂ : ι₂
h : e₂.BoundaryGE i₂
⊢ (fun (x : Subtype e₁.BoundaryLE) ↦
        (match (motive := Subtype e₁.BoundaryLE → Subtype e₂.BoundaryGE) x with
          | ⟨i₁, h⟩ => Subtype.mk (p := e₂.BoundaryGE) (indexOfBoundaryLE ac h) ⋯ :
          Subtype e₂.BoundaryGE))
      ((fun (x : Subtype e₂.BoundaryGE) ↦
          (match (motive := Subtype e₂.BoundaryGE → Subtype e₁.BoundaryLE) x with
            | ⟨i₂, h⟩ => Subtype.mk (p := e₁.BoundaryLE) (indexOfBoundaryGE ac h) ⋯ :
            Subtype e₁.BoundaryLE))
        (Subtype.mk (p := e₂.BoundaryGE) i₂ h)) =
    Subtype.mk (p := e₂.BoundaryGE) i₂ h
have a : (↑((fun (x : Subtype e₁.BoundaryLE) ↦
          (match (motive := Subtype e₁.BoundaryLE → Subtype e₂.BoundaryGE) x with
            | ⟨i₁, h⟩ => Subtype.mk (p := e₂.BoundaryGE) (indexOfBoundaryLE ac h) sorry :
            Subtype e₂.BoundaryGE))
        ((fun (x : Subtype e₂.BoundaryGE) ↦
            (match (motive := Subtype e₂.BoundaryGE → Subtype e₁.BoundaryLE) x with
              | ⟨i₂, h⟩ => Subtype.mk (p := e₁.BoundaryLE) (indexOfBoundaryGE ac h) sorry :
              Subtype e₁.BoundaryLE))
          (Subtype.mk (p := e₂.BoundaryGE) i₂ h))) :
    ι₂) =
  (↑(Subtype.mk (p := e₂.BoundaryGE) i₂ h) : ι₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (hypothesis)
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex.{v_1, u_4, u_1} C c
x : Subtype e₂.BoundaryGE
i₂ : ι₂
h : e₂.BoundaryGE i₂
⊢ (↑((fun (x : Subtype e₁.BoundaryLE) ↦
            (match (motive := Subtype e₁.BoundaryLE → Subtype e₂.BoundaryGE) x with
              | ⟨i₁, h⟩ => Subtype.mk (p := e₂.BoundaryGE) (indexOfBoundaryLE ac h) ⋯ :
              Subtype e₂.BoundaryGE))
          ((fun (x : Subtype e₂.BoundaryGE) ↦
              (match (motive := Subtype e₂.BoundaryGE → Subtype e₁.BoundaryLE) x with
                | ⟨i₂, h⟩ => Subtype.mk (p := e₁.BoundaryLE) (indexOfBoundaryGE ac h) ⋯ :
                Subtype e₁.BoundaryLE))
            (Subtype.mk (p := e₂.BoundaryGE) i₂ h))) :
      ι₂) =
    (↑(Subtype.mk (p := e₂.BoundaryGE) i₂ h) : ι₂)
have h' : ac.Boundary (indexOfBoundaryGE ac h) i₂
Tactic: have h' := of_boundaryGE ac h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (hypothesis)
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex.{v_1, u_4, u_1} C c
x : Subtype e₂.BoundaryGE
i₂ : ι₂
h : e₂.BoundaryGE i₂
h' : ac.Boundary (indexOfBoundaryGE ac h) i₂
⊢ (↑((fun (x : Subtype e₁.BoundaryLE) ↦
            (match (motive := Subtype e₁.BoundaryLE → Subtype e₂.BoundaryGE) x with
              | ⟨i₁, h⟩ => Subtype.mk (p := e₂.BoundaryGE) (indexOfBoundaryLE ac h) ⋯ :
              Subtype e₂.BoundaryGE))
          ((fun (x : Subtype e₂.BoundaryGE) ↦
              (match (motive := Subtype e₂.BoundaryGE → Subtype e₁.BoundaryLE) x with
                | ⟨i₂, h⟩ => Subtype.mk (p := e₁.BoundaryLE) (indexOfBoundaryGE ac h) ⋯ :
                Subtype e₁.BoundaryLE))
            (Subtype.mk (p := e₂.BoundaryGE) i₂ h))) :
      ι₂) =
    (↑(Subtype.mk (p := e₂.BoundaryGE) i₂ h) : ι₂)
have h'' : ac.Boundary (indexOfBoundaryGE ac h) (indexOfBoundaryLE ac sorry)
Tactic: have h'' := of_boundaryLE ac h'.fst
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (goal)
Goal:
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
i : ℤ
⊢ (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i
have pos : ∀ (hi : i ≤ n₀), (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i
Tactic: by_cases hi : i ≤ n₀
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (goal)
Goal:
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
i : ℤ
pos : ∀ (hi : i ≤ n₀), (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i
⊢ (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i
have neg : ∀ (hi : ¬i ≤ n₀), (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i
Tactic: by_cases hi : i ≤ n₀
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (goal)
Goal:
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
i : ℤ
hi : i ≤ n₀
⊢ (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i
have pos : ∀ (k : ℕ) (h : i + (↑k : ℤ) + 1 = n₁) (hi : i ≤ i + (↑k : ℤ)),
  (∃ (i₁ : ℕ), (embeddingUpIntLE (i + (↑k : ℤ))).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i
Tactic: obtain ⟨k, rfl⟩ := Int.exists_add_of_le hi
Cleared hypotheses: n₀, h, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (goal)
Goal:
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
i : ℤ
hi : ¬i ≤ n₀
⊢ (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = i) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = i
have neg : ∀ (k : ℕ) (hi : ¬n₁ + (↑k : ℤ) ≤ n₀),
  (∃ (i₁ : ℕ), (embeddingUpIntLE n₀).f i₁ = n₁ + (↑k : ℤ)) ∨ ∃ (i₂ : ℕ), (embeddingUpIntGE n₁).f i₂ = n₁ + (↑k : ℤ)
Tactic: obtain ⟨k, rfl⟩ := Int.exists_add_of_le (show n₁ ≤ i by lia)
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (goal)
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : Abelian.{v_1, u_4} C
K : HomologicalComplex.{v_1, u_4, u_1} C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst_2 : e₁.IsTruncLE
inst_3 : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i : ι
⊢ QuasiIsoAt (K := (K.shortComplexTruncLE e₁).X₃) (L := K.truncGE e₂) (K.shortComplexTruncLEX₃ToTruncGE ac) i
have inl : ∀ (i₁ : ι₁),
  QuasiIsoAt (K := (K.shortComplexTruncLE e₁).X₃) (L := K.truncGE e₂) (K.shortComplexTruncLEX₃ToTruncGE ac) (e₁.f i₁)
Tactic: obtain ⟨i₁, rfl⟩ | ⟨i₂, rfl⟩ := ac.union i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (goal)
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : Abelian.{v_1, u_4} C
K : HomologicalComplex.{v_1, u_4, u_1} C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst_2 : e₁.IsTruncLE
inst_3 : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i : ι
inl :
  ∀ (i₁ : ι₁),
    QuasiIsoAt (K := (K.shortComplexTruncLE e₁).X₃) (L := K.truncGE e₂) (K.shortComplexTruncLEX₃ToTruncGE ac) (e₁.f i₁)
⊢ QuasiIsoAt (K := (K.shortComplexTruncLE e₁).X₃) (L := K.truncGE e₂) (K.shortComplexTruncLEX₃ToTruncGE ac) i
have inr : ∀ (i₂ : ι₂),
  QuasiIsoAt (K := (K.shortComplexTruncLE e₁).X₃) (L := K.truncGE e₂) (K.shortComplexTruncLEX₃ToTruncGE ac) (e₂.f i₂)
Tactic: obtain ⟨i₁, rfl⟩ | ⟨i₂, rfl⟩ := ac.union i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (hypothesis)
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : Abelian.{v_1, u_4} C
K : HomologicalComplex.{v_1, u_4, u_1} C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst_2 : e₁.IsTruncLE
inst_3 : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i₁ : ι₁
⊢ QuasiIsoAt (K := (K.shortComplexTruncLE e₁).X₃) (L := K.truncGE e₂) (K.shortComplexTruncLEX₃ToTruncGE ac) (e₁.f i₁)
have h₁ : (K.truncGE e₂).ExactAt (e₁.f i₁)
Tactic: have h₁ := ((ac.isSupportedOutside₁_iff (K.truncGE e₂)).2 inferInstance).exactAt i₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (hypothesis)
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : Abelian.{v_1, u_4} C
K : HomologicalComplex.{v_1, u_4, u_1} C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst_2 : e₁.IsTruncLE
inst_3 : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i₁ : ι₁
h₁ : (K.truncGE e₂).ExactAt (e₁.f i₁)
⊢ QuasiIsoAt (K := (K.shortComplexTruncLE e₁).X₃) (L := K.truncGE e₂) (K.shortComplexTruncLEX₃ToTruncGE ac) (e₁.f i₁)
have h₂ : (K.shortComplexTruncLE e₁).X₃.ExactAt (e₁.f i₁)
Tactic: have h₂ := (K.shortComplexTruncLE_X₃_isSupportedOutside e₁).exactAt i₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (hypothesis)
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : Abelian.{v_1, u_4} C
K : HomologicalComplex.{v_1, u_4, u_1} C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst_2 : e₁.IsTruncLE
inst_3 : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i₂ : ι₂
⊢ QuasiIsoAt (K := (K.shortComplexTruncLE e₁).X₃) (L := K.truncGE e₂) (K.shortComplexTruncLEX₃ToTruncGE ac) (e₂.f i₂)
have this : QuasiIsoAt (K.shortComplexTruncLE e₁).g (e₂.f i₂)
Tactic: have := quasiIsoAt_shortComplexTruncLE_g K e₁ (e₂.f i₂) (fun _ => ac.disjoint _ _)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (goal)
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : Abelian.{v_1, u_4} C
K : HomologicalComplex.{v_1, u_4, u_1} C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst_2 : e₁.IsTruncLE
inst_3 : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i₂ : ι₂
this : QuasiIsoAt (K.shortComplexTruncLE e₁).g (e₂.f i₂)
⊢ QuasiIsoAt (K := (K.shortComplexTruncLE e₁).X₃) (L := K.truncGE e₂) (K.shortComplexTruncLEX₃ToTruncGE ac) (e₂.f i₂)
have inr : QuasiIsoAt (L := K.truncGE e₂) (K.πTruncGE e₂) (e₂.f i₂)
Tactic: rw [← quasiIsoAt_iff_comp_left (K.shortComplexTruncLE e₁).g
        (K.shortComplexTruncLEX₃ToTruncGE ac), g_shortComplexTruncLEX₃ToTruncGE]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (goal)
Goal:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst : Category.{v_1, u_4} C
inst_1 : Abelian.{v_1, u_4} C
K : HomologicalComplex.{v_1, u_4, u_1} C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst_2 : e₁.IsTruncLE
inst_3 : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i₂ : ι₂
this : QuasiIsoAt (K.shortComplexTruncLE e₁).g (e₂.f i₂)
⊢ QuasiIsoAt (L := K.truncGE e₂) (K.πTruncGE e₂) (e₂.f i₂)
have inr : QuasiIsoAt (L := K.truncGE e₂) (K.πTruncGE e₂) (e₂.f i₂)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
i₁ i₂ : ι
⊢ c'.Rel (e.f i₁) (e.f i₂) ↔ c.Rel i₁ i₂
have mp : c'.Rel (e.f i₁) (e.f i₂) → c.Rel i₁ i₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
i₁ i₂ : ι
mp : c'.Rel (e.f i₁) (e.f i₂) → c.Rel i₁ i₂
⊢ c'.Rel (e.f i₁) (e.f i₂) ↔ c.Rel i₁ i₂
have mpr : c.Rel i₁ i₂ → c'.Rel (e.f i₁) (e.f i₂)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
⊢ e.r i' = some i
have h : ∃ (i : ι), e.f i = i'
Tactic: have h : ∃ (i : ι), e.f i = i' := ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
h : ∃ (i : ι), e.f i = i'
⊢ e.r i' = some i
have this : h.choose (p := fun (i : ι) ↦ e.f i = i') = i
Tactic: have : h.choose = i := e.injective_f (h.choose_spec.trans (hi.symm))
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
h : ∃ (i : ι), e.f i = i'
this : h.choose (p := fun (i : ι) ↦ e.f i = i') = i
⊢ (if h : ∃ (i : ι), e.f i = i' then some (h.choose (p := fun (i : ι) ↦ e.f i = i')) else none) = some i
have rw : some (Exists.choose (p := fun (i : ι) ↦ e.f i = i') sorry) = some i
Tactic: rw [dif_pos ⟨i, hi⟩, this]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
h : ∃ (i : ι), e.f i = i'
this : h.choose (p := fun (i : ι) ↦ e.f i = i') = i
rw : some (Exists.choose (p := fun (i : ι) ↦ e.f i = i') ⋯) = some i
⊢ (if h : ∃ (i : ι), e.f i = i' then some (h.choose (p := fun (i : ι) ↦ e.f i = i')) else none) = some i
have rw₁ : some i = some i
Tactic: rw [dif_pos ⟨i, hi⟩, this]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.r i' = some i
⊢ e.f i = i'
have pos : ∀ (h : ∃ (k : ι), e.f k = i'), e.f i = i'
Tactic: by_cases h : ∃ (k : ι), e.f k = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.r i' = some i
pos : ∀ (h : ∃ (k : ι), e.f k = i'), e.f i = i'
⊢ e.f i = i'
have neg : ∀ (h : ¬∃ (k : ι), e.f k = i'), e.f i = i'
Tactic: by_cases h : ∃ (k : ι), e.f k = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.r i' = some i
h : ∃ (k : ι), e.f k = i'
⊢ e.f i = i'
have pos : ∀ (k : ι) (hi : e.r (e.f k) = some i), e.f i = e.f k
Tactic: obtain ⟨k, rfl⟩ := h
Cleared hypotheses: i', hi, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i k : ι
hi : e.r (e.f k) = some i
⊢ e.f i = e.f k
have hi₁ : some k = some i
Tactic: rw [r_f] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i k : ι
hi : some k = some i
⊢ e.f i = e.f k
have pos : i = k
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst : AddCommSemigroup A
inst_1 : IsRightCancelAdd A
inst_2 : One A
a b : A
⊢ ∀ (i₁ i₂ : A), (up' a).Rel i₁ i₂ ↔ (up' a).Rel ((fun (x : A) ↦ x + b) i₁) ((fun (x : A) ↦ x + b) i₂)
have dsimp : ∀ (i₁ i₂ : A), i₁ + a = i₂ ↔ i₁ + b + a = i₂ + b
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst : AddCommSemigroup A
inst_1 : IsRightCancelAdd A
inst_2 : One A
a b : A
⊢ ∀ (i₁ i₂ : A), i₁ + a = i₂ ↔ i₁ + b + a = i₂ + b
have simp_rw : ∀ (i₁ i₂ : A), i₁ + a = i₂ ↔ i₁ + a + b = i₂ + b
Tactic: simp_rw [add_right_comm _ b a, add_right_cancel_iff, implies_true]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst : AddCommSemigroup A
inst_1 : IsRightCancelAdd A
inst_2 : One A
a b : A
simp_rw : ∀ (i₁ i₂ : A), i₁ + a = i₂ ↔ i₁ + a + b = i₂ + b
⊢ ∀ (i₁ i₂ : A), i₁ + a = i₂ ↔ i₁ + b + a = i₂ + b
have simp_rw₁ : ∀ (i₁ i₂ : A), True
Tactic: simp_rw [add_right_comm _ b a, add_right_cancel_iff, implies_true]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst : AddCommSemigroup A
inst_1 : IsRightCancelAdd A
inst_2 : One A
a b : A
⊢ ∀ (i₁ i₂ : A), (down' a).Rel i₁ i₂ ↔ (down' a).Rel ((fun (x : A) ↦ x + b) i₁) ((fun (x : A) ↦ x + b) i₂)
have dsimp : ∀ (i₁ i₂ : A), i₂ + a = i₁ ↔ i₂ + b + a = i₁ + b
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst : AddCommSemigroup A
inst_1 : IsRightCancelAdd A
inst_2 : One A
a b : A
⊢ ∀ (i₁ i₂ : A), i₂ + a = i₁ ↔ i₂ + b + a = i₁ + b
have simp_rw : ∀ (i₁ i₂ : A), i₂ + a = i₁ ↔ i₂ + a + b = i₁ + b
Tactic: simp_rw [add_right_comm _ b a, add_right_cancel_iff, implies_true]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst : AddCommSemigroup A
inst_1 : IsRightCancelAdd A
inst_2 : One A
a b : A
simp_rw : ∀ (i₁ i₂ : A), i₂ + a = i₁ ↔ i₂ + a + b = i₁ + b
⊢ ∀ (i₁ i₂ : A), i₂ + a = i₁ ↔ i₂ + b + a = i₁ + b
have simp_rw₁ : ∀ (i₁ i₂ : A), True
Tactic: simp_rw [add_right_comm _ b a, add_right_cancel_iff, implies_true]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
p n : ℤ
⊢ (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) ↔ p < n
have mp : (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) → p < n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
p n : ℤ
mp : (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) → p < n
⊢ (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) ↔ p < n
have mpr : p < n → ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
⊢ p < n
have mp : ∀ (this : ¬p < n), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
p n : ℤ
⊢ (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) ↔ n < p
have mp : (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) → n < p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
p n : ℤ
mp : (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) → n < p
⊢ (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) ↔ n < p
have mpr : n < p → ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Basic (goal)
Goal:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
⊢ n < p
have mp : ∀ (this : ¬n < p), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ e.BoundaryGE j
have left : c'.Rel (c'.prev (e.f j)) (e.f j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
left : c'.Rel (c'.prev (e.f j)) (e.f j)
⊢ e.BoundaryGE j
have right : ∀ (i : ι), ¬c'.Rel (e.f i) (e.f j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
hi : c'.Rel (e.f i) (e.f j)
⊢ False
have right : e.f i = i'
Tactic: apply hi' i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
hi : c'.Rel (e.f i) (e.f j)
⊢ e.f i = i'
have right : e.f i = c'.prev (e.f j)
Tactic: rw [← c'.prev_eq' hj, c'.prev_eq' hi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
hi : c'.Rel (e.f i) (e.f j)
right : e.f i = c'.prev (e.f j)
⊢ e.f i = i'
have right₁ : e.f i = e.f i
Tactic: rw [← c'.prev_eq' hj, c'.prev_eq' hi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j k : ι
hk : c.Rel j k
⊢ ¬(c'.Rel (c'.prev (e.f k)) (e.f k) ∧ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f k))
have simp : c'.Rel (c'.prev (e.f k)) (e.f k) → ∃ (x : ι), c'.Rel (e.f x) (e.f k)
Tactic: simp only [not_and, not_forall, not_not]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j k : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
⊢ ¬e.BoundaryGE k
have pos : ∀ (hjk : c.Rel j k), ¬e.BoundaryGE k
Tactic: by_cases hjk : c.Rel j k
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j k : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
pos : ∀ (hjk : c.Rel j k), ¬e.BoundaryGE k
⊢ ¬e.BoundaryGE k
have neg : ∀ (hjk : ¬c.Rel j k), ¬e.BoundaryGE k
Tactic: by_cases hjk : c.Rel j k
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j k : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
hjk : ¬c.Rel j k
⊢ ¬e.BoundaryGE k
have neg : ∀ (hjk : ¬c.Rel j (c.next j)), ¬e.BoundaryGE (c.next j)
Tactic: subst hk
Cleared hypotheses: k, hk, hjk
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
⊢ c'.prev (e.f j) = e.f i
have pos : ∀ (hij' : c.Rel i j), c'.prev (e.f j) = e.f i
Tactic: by_cases hij' : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
pos : ∀ (hij' : c.Rel i j), c'.prev (e.f j) = e.f i
⊢ c'.prev (e.f j) = e.f i
have neg : ∀ (hij' : ¬c.Rel i j), c'.prev (e.f j) = e.f i
Tactic: by_cases hij' : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
⊢ c'.prev (e.f j) = e.f i
have neg : ∀ (hij : c.prev j = j) (hij' : ¬c.Rel j j), c'.prev (e.f j) = e.f j
Tactic: obtain rfl : j = i := by
      simpa only [c.prev_eq_self j (by simpa only [hij] using hij')] using hij
Cleared hypotheses: i, hij, hij'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hj : ¬e.BoundaryGE j
hij : c.prev j = j
hij' : ¬c.Rel j j
⊢ c'.prev (e.f j) = e.f j
have neg : ¬c'.Rel (c'.prev (e.f j)) (e.f j)
Tactic: apply c'.prev_eq_self
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hj : ¬e.BoundaryGE j
hij : c.prev j = j
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
⊢ False
have hj₁ : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ (x : ι), c'.Rel (e.f x) (e.f j)
Tactic: simp only [BoundaryGE, not_and, not_forall, not_not] at hj
Cleared hypotheses: hj