awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
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
neg : ¬c'.Rel (c'.prev (e.f j)) (e.f j)
⊢ c'.prev (e.f j) = e.f j

Tactic:
apply c'.prev_eq_self

Premises used: ComplexShape.prev_eq_self
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
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)
⊢ 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

Premises used: ComplexShape.Embedding.BoundaryGE, Classical.not_not, not_and, Classical.not_forall
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hij : c.prev j = j
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ (x : ι), c'.Rel (e.f x) (e.f j)
neg : ∀ (i : ι) (hi : c'.Rel (e.f i) (e.f j)), False
⊢ False

Tactic:
obtain ⟨i, hi⟩ := hj hj'
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hij : c.prev j = j
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ (x : ι), c'.Rel (e.f x) (e.f j)
i : ι
hi : c'.Rel (e.f i) (e.f j)
⊢ c.Rel i j

Tactic:
rw [e.rel_iff] at hi

Premises used: ComplexShape.Embedding.rel_iff
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hij : c.prev j = j
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ (x : ι), c'.Rel (e.f x) (e.f j)
i : ι
hi : c.Rel i j
⊢ i = j

Tactic:
rw [c.prev_eq' hi] at hij

Premises used: ComplexShape.prev_eq'
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hij : c.prev j = j
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ (x : ι), c'.Rel (e.f x) (e.f j)
i : ι
hi : c.Rel i j
hij₁ : i = j
⊢ c.Rel i j

Tactic:
rw [c.prev_eq' hi] at hij

Premises used: ComplexShape.prev_eq'
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ (x : ι), c'.Rel (e.f x) (e.f j)
i : ι
hij : i = j
hi : c.Rel i j
⊢ c.Rel j j

Tactic:
simpa only [hij] using hi
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ (x : ι), c'.Rel (e.f x) (e.f j)
i : ι
hij : i = j
hi : c.Rel i j
⊢ False

Tactic:
exact hij' (by simpa only [hij] using hi)
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryGE j
inst : e.IsTruncLE
obtain : ∀ (i : ι) (hi : e.f i = c'.prev (e.f j)), False
⊢ False

Tactic:
obtain ⟨i, hi⟩ := e.mem_prev hj.1

Premises used: ComplexShape.Embedding.mem_prev, And.left
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryGE j
inst : e.IsTruncLE
i : ι
hi : e.f i = c'.prev (e.f j)
⊢ c'.Rel (e.f i) (e.f j)

Tactic:
simpa only [hi] using hj.1

Premises used: And.left
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryGE j
inst : e.IsTruncLE
i : ι
hi : e.f i = c'.prev (e.f j)
⊢ False

Tactic:
exact hj.2 i (by simpa only [hi] using hj.1)

Premises used: And.right
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
left : c'.Rel (e.f j) (c'.next (e.f j))
right : ∀ (k : ι), ¬c'.Rel (e.f j) (e.f k)
⊢ e.BoundaryLE j

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ c'.Rel (e.f j) (c'.next (e.f j))

Tactic:
simpa only [c'.next_eq' hj] using hj

Premises used: ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
k : ι
hk : c'.Rel (e.f j) (e.f k)
right : e.f k = k'
⊢ False

Tactic:
apply hk' k
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
k : ι
hk : c'.Rel (e.f j) (e.f k)
right : e.f k = c'.next (e.f j)
right₁ right₂ : e.f k = e.f k
⊢ e.f k = k'

Tactic:
rw [← c'.next_eq' hj, c'.next_eq' hk]

Premises used: ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
i j : ι
hi : c.Rel i j
simp : c'.Rel (e.f i) (c'.next (e.f i)) → ∃ (x : ι), c'.Rel (e.f i) (e.f x)
⊢ ¬(c'.Rel (e.f i) (c'.next (e.f i)) ∧ ∀ (k : ι), ¬c'.Rel (e.f i) (e.f k))

Tactic:
simp only [not_and, not_forall, not_not]

Premises used: Classical.not_not, not_and, Classical.not_forall
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
i j : ι
hi : c.Rel i j
h : c'.Rel (e.f i) (c'.next (e.f i))
⊢ c'.Rel (e.f i) (e.f j)

Tactic:
simpa only [e.rel_iff] using hi

Premises used: ComplexShape.Embedding.rel_iff
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
i j : ι
hi : c.Rel i j
h : c'.Rel (e.f i) (c'.next (e.f i))
⊢ ∃ (x : ι), c'.Rel (e.f i) (e.f x)

Tactic:
exact ⟨j, by simpa only [e.rel_iff] using hi⟩
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
pos : ∀ (hij : c.Rel i j), ¬e.BoundaryLE i
neg : ∀ (hij : ¬c.Rel i j), ¬e.BoundaryLE i
⊢ ¬e.BoundaryLE i

Tactic:
by_cases hij : c.Rel i j

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
hij : c.Rel i j
⊢ ¬e.BoundaryLE i

Tactic:
e.not_boundaryLE_prev hij

Premises used: ComplexShape.Embedding.not_boundaryLE_prev
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
hij : c.Rel i j
⊢ ¬e.BoundaryLE i

Tactic:
exact e.not_boundaryLE_prev hij

Premises used: ComplexShape.Embedding.not_boundaryLE_prev
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
hij : ¬c.Rel i j
neg : ∀ (hij : ¬c.Rel (c.prev j) j), ¬e.BoundaryLE (c.prev j)
⊢ ¬e.BoundaryLE i

Tactic:
subst hk
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hj : ¬e.BoundaryLE j
hij : ¬c.Rel (c.prev j) j
⊢ ¬e.BoundaryLE (c.prev j)

Tactic:
simpa only [c.prev_eq_self j hij] using hj

Premises used: ComplexShape.prev_eq_self
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryLE j
k' : ι'
hk' : c'.Rel (e.f j) k'
a : ι
ha : e.f a = k'
⊢ c'.Rel (e.f j) (e.f a)

Tactic:
simpa only [ha] using hk'
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j k : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
pos : ∀ (hjk' : c.Rel j k), c'.next (e.f j) = e.f k
neg : ∀ (hjk' : ¬c.Rel j k), c'.next (e.f j) = e.f k
⊢ c'.next (e.f j) = e.f k

Tactic:
by_cases hjk' : c.Rel j k

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j k : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
hjk' : c.Rel j k
⊢ c'.Rel (e.f j) (e.f k)

Tactic:
simpa only [e.rel_iff] using hjk'

Premises used: ComplexShape.Embedding.rel_iff
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j k : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
hjk' : c.Rel j k
⊢ c'.next (e.f j) = e.f k

Tactic:
exact c'.next_eq' (by simpa only [e.rel_iff] using hjk')

Premises used: ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j k : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
hjk' : ¬c.Rel j k
⊢ ¬c.Rel j (c.next j)

Tactic:
simpa only [hjk] using hjk'
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j k : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
hjk' : ¬c.Rel j k
⊢ j = k

Tactic:
simpa only [c.next_eq_self j (by simpa only [hjk] using hjk')] using hjk

Premises used: ComplexShape.next_eq_self
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j k : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
hjk' : ¬c.Rel j k
neg : ∀ (hjk : c.next j = j) (hjk' : ¬c.Rel j j), c'.next (e.f j) = e.f j
⊢ c'.next (e.f j) = e.f k

Tactic:
obtain rfl : j = k := by
      simpa only [c.next_eq_self j (by simpa only [hjk] using hjk')] using hjk

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hj : ¬e.BoundaryLE j
hjk : c.next j = j
hjk' : ¬c.Rel j j
neg : ¬c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f j

Tactic:
apply c'.next_eq_self

Premises used: ComplexShape.next_eq_self
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hj : ¬e.BoundaryLE j
hjk : c.next j = j
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.Rel (e.f j) (c'.next (e.f j)) → ∃ (x : ι), c'.Rel (e.f j) (e.f x)

Tactic:
simp only [BoundaryLE, not_and, not_forall, not_not] at hj

Premises used: Classical.not_not, not_and, Classical.not_forall, ComplexShape.Embedding.BoundaryLE
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hjk : c.next j = j
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ (x : ι), c'.Rel (e.f j) (e.f x)
neg : ∀ (k : ι) (hk : c'.Rel (e.f j) (e.f k)), False
⊢ False

Tactic:
obtain ⟨k, hk⟩ := hj hj'
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hjk : c.next j = j
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ (x : ι), c'.Rel (e.f j) (e.f x)
k : ι
hk : c'.Rel (e.f j) (e.f k)
⊢ c.Rel j k

Tactic:
rw [e.rel_iff] at hk

Premises used: ComplexShape.Embedding.rel_iff
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hjk : c.next j = j
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ (x : ι), c'.Rel (e.f j) (e.f x)
k : ι
hk : c.Rel j k
⊢ k = j

Tactic:
rw [c.next_eq' hk] at hjk

Premises used: ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hjk : c.next j = j
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ (x : ι), c'.Rel (e.f j) (e.f x)
k : ι
hk : c.Rel j k
hjk₁ : k = j
⊢ c.Rel j k

Tactic:
rw [c.next_eq' hk] at hjk

Premises used: ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ (x : ι), c'.Rel (e.f j) (e.f x)
k : ι
hjk : k = j
hk : c.Rel j k
⊢ c.Rel j j

Tactic:
simpa only [hjk] using hk
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
j : ι
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ (x : ι), c'.Rel (e.f j) (e.f x)
k : ι
hjk : k = j
hk : c.Rel j k
⊢ False

Tactic:
exact hjk' (by simpa only [hjk] using hk)
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsTruncGE
j k : ι
hjk : c.next j = k
pos : ∀ (hj : c'.Rel (e.f j) (c'.next (e.f j))), c'.next (e.f j) = e.f k
neg : ∀ (hj : ¬c'.Rel (e.f j) (c'.next (e.f j))), c'.next (e.f j) = e.f k
⊢ c'.next (e.f j) = e.f k

Tactic:
by_cases hj : c'.Rel (e.f j) (c'.next (e.f j))

Premises used: ComplexShape.next, ComplexShape.Embedding.f, ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : c'.Rel (e.f j) (c'.next (e.f j))
pos : ∀ (k' : ι) (hk' : e.f k' = c'.next (e.f j)), c'.next (e.f j) = e.f k
⊢ c'.next (e.f j) = e.f k

Tactic:
obtain ⟨k', hk'⟩ := e.mem_next hj

Premises used: ComplexShape.Embedding.mem_next
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : c'.Rel (e.f j) (c'.next (e.f j))
k' : ι
hk' : e.f k' = c'.next (e.f j)
⊢ c.Rel j k'

Tactic:
rw [← hk', e.rel_iff] at hj

Premises used: ComplexShape.Embedding.rel_iff
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : c'.Rel (e.f j) (c'.next (e.f j))
k' : ι
hk' : e.f k' = c'.next (e.f j)
hj₁ : c.Rel j k'
⊢ e.f k' = c'.next (e.f j)

Tactic:
rw [← hk', e.rel_iff] at hj

Premises used: ComplexShape.Embedding.rel_iff
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsTruncGE
j k : ι
hjk : c.next j = k
k' : ι
hj : c.Rel j k'
hk' : e.f k' = c'.next (e.f j)
pos : e.f k' = e.f k
pos₁ : e.f (c.next j) = e.f k
pos₂ pos₃ : e.f k = e.f k
⊢ c'.next (e.f j) = e.f k

Tactic:
rw [← hk', ← c.next_eq' hj, hjk]

Premises used: ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : ¬c'.Rel (e.f j) (c'.next (e.f j))
neg : ¬c.Rel j (c.next j)
⊢ c'.next (e.f j) = e.f k

Tactic:
rw [c'.next_eq_self _ hj, ← hjk, c.next_eq_self j]

Premises used: ComplexShape.next_eq_self
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : ¬c'.Rel (e.f j) (c'.next (e.f j))
hj' : c.Rel j (c.next j)
neg : c'.Rel (e.f j) (c'.next (e.f j))
⊢ False

Tactic:
apply hj
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : ¬c'.Rel (e.f j) (c'.next (e.f j))
hj' : c.Rel j (c.next j)
⊢ c'.Rel (e.f j) (e.f (c.next j))

Tactic:
rw [← e.rel_iff] at hj'

Premises used: ComplexShape.Embedding.rel_iff
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : ¬c'.Rel (e.f j) (c'.next (e.f j))
hj' : c'.Rel (e.f j) (e.f (c.next j))
⊢ c'.Rel (e.f j) (c'.next (e.f j))

Tactic:
simpa only [c'.next_eq' hj'] using hj'

Premises used: ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsTruncLE
i j : ι
hij : c.prev j = i
⊢ c'.prev (e.f j) = e.f i

Tactic:
e.op.next_f hij

Premises used: ComplexShape.prev, ComplexShape.Embedding.op, ComplexShape.Embedding.next_f
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryLE j
inst : e.IsTruncGE
obtain : ∀ (k : ι) (hk : e.f k = c'.next (e.f j)), False
⊢ False

Tactic:
obtain ⟨k, hk⟩ := e.mem_next hj.1

Premises used: And.left, ComplexShape.Embedding.mem_next
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryLE j
inst : e.IsTruncGE
k : ι
hk : e.f k = c'.next (e.f j)
⊢ c'.Rel (e.f j) (e.f k)

Tactic:
simpa only [hk] using hj.1

Premises used: And.left
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryLE j
inst : e.IsTruncGE
k : ι
hk : e.f k = c'.next (e.f j)
⊢ False

Tactic:
exact hj.2 k (by simpa only [hk] using hj.1)

Premises used: And.right
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
⊢ e.op.BoundaryLE j ↔ e.BoundaryGE j

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
⊢ e.op.BoundaryGE j ↔ e.BoundaryLE j

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
n : ℕ
mp : (embeddingUpIntGE p).BoundaryGE n → n = 0
mpr : n = 0 → (embeddingUpIntGE p).BoundaryGE n
⊢ (embeddingUpIntGE p).BoundaryGE n ↔ n = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE n
mp : ∀ (h : (embeddingUpIntGE p).BoundaryGE 0), Eq (α := ℕ) 0 0
mp₁ : ∀ (n : ℕ) (h : (embeddingUpIntGE p).BoundaryGE (n + 1)), n + 1 = 0
⊢ n = 0

Tactic:
obtain _ | n := n
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
h : (embeddingUpIntGE p).BoundaryGE 0
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
⊢ ¬(up ℤ).Rel ((embeddingUpIntGE p).f n) ((embeddingUpIntGE p).f (n + 1))

Tactic:
have := h.2 n
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
this : ¬p + (↑n : ℤ) + 1 = p + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
⊢ n + 1 = 0

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
mpr : (up ℤ).Rel ((up ℤ).prev ((embeddingUpIntGE p).f 0)) ((embeddingUpIntGE p).f 0)
mpr₁ : ∀ (i : ℕ), ¬(up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)
⊢ (embeddingUpIntGE p).BoundaryGE 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
⊢ (up ℤ).Rel ((up ℤ).prev ((embeddingUpIntGE p).f 0)) ((embeddingUpIntGE p).f 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
i : ℕ
hi : p + (↑i : ℤ) + 1 = p + 0
⊢ False

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
n : ℕ
mp : (embeddingUpIntLE p).BoundaryLE n → n = 0
mpr : n = 0 → (embeddingUpIntLE p).BoundaryLE n
⊢ (embeddingUpIntLE p).BoundaryLE n ↔ n = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE n
mp : ∀ (h : (embeddingUpIntLE p).BoundaryLE 0), Eq (α := ℕ) 0 0
mp₁ : ∀ (n : ℕ) (h : (embeddingUpIntLE p).BoundaryLE (n + 1)), n + 1 = 0
⊢ n = 0

Tactic:
obtain _ | n := n
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
h : (embeddingUpIntLE p).BoundaryLE 0
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE (n + 1)
⊢ ¬(up ℤ).Rel ((embeddingUpIntLE p).f (n + 1)) ((embeddingUpIntLE p).f n)

Tactic:
have := h.2 n
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE (n + 1)
this : ¬p - HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 = p - (↑n : ℤ)
⊢ n + 1 = 0

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
mpr : (up ℤ).Rel ((embeddingUpIntLE p).f 0) ((up ℤ).next ((embeddingUpIntLE p).f 0))
mpr₁ : ∀ (k : ℕ), ¬(up ℤ).Rel ((embeddingUpIntLE p).f 0) ((embeddingUpIntLE p).f k)
⊢ (embeddingUpIntLE p).BoundaryLE 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
⊢ (up ℤ).Rel ((embeddingUpIntLE p).f 0) ((up ℤ).next ((embeddingUpIntLE p).f 0))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
Goal:
p : ℤ
i : ℕ
hi : p - 0 + 1 = p - (↑i : ℤ)
⊢ False

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : ∀ (i : ℤ), HasHomology K i
n q : ℤ
hq : q ≤ n
obtain : ∀ (k : ℕ) (hq : q ≤ q + (↑k : ℤ)), QuasiIsoAt (K := K.truncLE (q + (↑k : ℤ))) (K.ιTruncLE (q + (↑k : ℤ))) q
⊢ QuasiIsoAt (K := K.truncLE n) (K.ιTruncLE n) q

Tactic:
obtain ⟨k, rfl⟩ := Int.le.dest hq

Premises used: Int.le.dest, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : ∀ (i : ℤ), HasHomology K i
q : ℤ
k : ℕ
hq : q ≤ q + (↑k : ℤ)
⊢ (embeddingUpIntLE (q + (↑k : ℤ))).f k = q

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : ∀ (i : ℤ), HasHomology K i
q : ℤ
k : ℕ
hq : q ≤ q + (↑k : ℤ)
⊢ QuasiIsoAt (K := K.truncLE (q + (↑k : ℤ))) (K.ιTruncLE (q + (↑k : ℤ))) q

Tactic:
exact HomologicalComplex.quasiIsoAt_ιTruncLE (j := k) _ _ (by simp)

Premises used: HomologicalComplex.quasiIsoAt_ιTruncLE