awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
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)
⊢ False
have neg : ∀ (i : ι) (hi : c'.Rel (e.f i) (e.f j)), False
Tactic: obtain ⟨i, hi⟩ := hj hj'
-- 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 : ι
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)
⊢ False
have hi₁ : c.Rel i j
Tactic: rw [e.rel_iff] at hi
Cleared hypotheses: hi
-- 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 : ι
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
⊢ False
have hij₁ : i = j
Tactic: rw [c.prev_eq' hi] at hij
Cleared hypotheses: hij, 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'
j : ι
hj : e.BoundaryGE j
inst : e.IsTruncLE
⊢ False
have obtain : ∀ (i : ι) (hi : e.f i = c'.prev (e.f j)), False
Tactic: obtain ⟨i, hi⟩ := e.mem_prev hj.1
-- 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'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ e.BoundaryLE j
have left : c'.Rel (e.f j) (c'.next (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'
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))
⊢ e.BoundaryLE j
have right : ∀ (k : ι), ¬c'.Rel (e.f j) (e.f k)
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'
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)
⊢ False
have right : e.f k = k'
Tactic: apply hk' 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'
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)
⊢ e.f k = k'
have right : e.f k = c'.next (e.f j)
Tactic: rw [← c'.next_eq' hj, c'.next_eq' hk]
-- 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'
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)
⊢ e.f k = k'
have right₁ : e.f k = e.f k
Tactic: rw [← c'.next_eq' hj, c'.next_eq' hk]
-- 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 : ι
hi : c.Rel i j
⊢ ¬(c'.Rel (e.f i) (c'.next (e.f i)) ∧ ∀ (k : ι), ¬c'.Rel (e.f i) (e.f k))
have simp : c'.Rel (e.f i) (c'.next (e.f i)) → ∃ (x : ι), c'.Rel (e.f i) (e.f x)
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
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
⊢ ¬e.BoundaryLE i
have pos : ∀ (hij : c.Rel i j), ¬e.BoundaryLE 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 : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
pos : ∀ (hij : c.Rel i j), ¬e.BoundaryLE i
⊢ ¬e.BoundaryLE i
have neg : ∀ (hij : ¬c.Rel i j), ¬e.BoundaryLE 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 : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
hij : ¬c.Rel i j
⊢ ¬e.BoundaryLE i
have neg : ∀ (hij : ¬c.Rel (c.prev j) j), ¬e.BoundaryLE (c.prev j)
Tactic: subst hk
Cleared hypotheses: i, hk, 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 k : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
⊢ c'.next (e.f j) = e.f k
have pos : ∀ (hjk' : c.Rel j k), c'.next (e.f j) = e.f 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 : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
pos : ∀ (hjk' : c.Rel j k), c'.next (e.f j) = e.f k
⊢ c'.next (e.f j) = e.f k
have neg : ∀ (hjk' : ¬c.Rel j k), c'.next (e.f j) = e.f 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 : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
hjk' : ¬c.Rel j k
⊢ c'.next (e.f j) = e.f k
have neg : ∀ (hjk : c.next j = j) (hjk' : ¬c.Rel j j), c'.next (e.f j) = e.f j
Tactic: obtain rfl : j = k := by
      simpa only [c.next_eq_self j (by simpa only [hjk] using hjk')] using hjk
Cleared hypotheses: k, hjk, 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
j : ι
hj : ¬e.BoundaryLE j
hjk : c.next j = j
hjk' : ¬c.Rel j j
⊢ c'.next (e.f j) = e.f j
have neg : ¬c'.Rel (e.f j) (c'.next (e.f j))
Tactic: apply c'.next_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.BoundaryLE j
hjk : c.next j = j
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
⊢ False
have hj₁ : 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
Cleared hypotheses: hj
-- 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 : ι
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)
⊢ False
have neg : ∀ (k : ι) (hk : c'.Rel (e.f j) (e.f k)), False
Tactic: obtain ⟨k, hk⟩ := hj hj'
-- 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 : ι
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)
⊢ False
have hk₁ : c.Rel j k
Tactic: rw [e.rel_iff] at hk
Cleared hypotheses: hk
-- 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 : ι
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
⊢ False
have hjk₁ : k = j
Tactic: rw [c.next_eq' hk] at hjk
Cleared hypotheses: hjk, hk
-- 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.IsTruncGE
j k : ι
hjk : c.next j = k
⊢ c'.next (e.f j) = e.f k
have pos : ∀ (hj : c'.Rel (e.f j) (c'.next (e.f j))), c'.next (e.f j) = e.f k
Tactic: by_cases hj : c'.Rel (e.f j) (c'.next (e.f 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.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
⊢ c'.next (e.f j) = e.f k
have neg : ∀ (hj : ¬c'.Rel (e.f j) (c'.next (e.f j))), c'.next (e.f j) = e.f k
Tactic: by_cases hj : c'.Rel (e.f j) (c'.next (e.f 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.IsTruncGE
j k : ι
hjk : c.next j = k
hj : c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f k
have pos : ∀ (k' : ι) (hk' : e.f k' = c'.next (e.f j)), c'.next (e.f j) = e.f k
Tactic: obtain ⟨k', hk'⟩ := e.mem_next hj
-- 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.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'.next (e.f j) = e.f k
have hj₁ : c.Rel j k'
Tactic: rw [← hk', e.rel_iff] at hj
Cleared hypotheses: hj, hk'
-- 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.IsTruncGE
j k : ι
hjk : c.next j = k
k' : ι
hj : c.Rel j k'
hk' : e.f k' = c'.next (e.f j)
⊢ c'.next (e.f j) = e.f k
have pos : e.f k' = e.f k
Tactic: rw [← hk', ← c.next_eq' hj, 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.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
⊢ c'.next (e.f j) = e.f k
have pos₁ : e.f (c.next j) = e.f k
Tactic: rw [← hk', ← c.next_eq' hj, 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.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
⊢ c'.next (e.f j) = e.f k
have pos₂ : e.f k = e.f k
Tactic: rw [← hk', ← c.next_eq' hj, 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.IsTruncGE
j k : ι
hjk : c.next j = k
hj : ¬c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f k
have neg : ¬c.Rel j (c.next j)
Tactic: rw [c'.next_eq_self _ hj, ← hjk, c.next_eq_self 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.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)
⊢ False
have neg : c'.Rel (e.f j) (c'.next (e.f j))
Tactic: apply hj
-- 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.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) (c'.next (e.f j))
have hj'₁ : c'.Rel (e.f j) (e.f (c.next j))
Tactic: rw [← e.rel_iff] at hj'
Cleared hypotheses: hj'
-- 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'
j : ι
hj : e.BoundaryLE j
inst : e.IsTruncGE
⊢ False
have obtain : ∀ (k : ι) (hk : e.f k = c'.next (e.f j)), False
Tactic: obtain ⟨k, hk⟩ := e.mem_next hj.1
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
p : ℤ
n : ℕ
⊢ (embeddingUpIntGE p).BoundaryGE n ↔ n = 0
have mp : (embeddingUpIntGE p).BoundaryGE n → n = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
p : ℤ
n : ℕ
mp : (embeddingUpIntGE p).BoundaryGE n → n = 0
⊢ (embeddingUpIntGE p).BoundaryGE n ↔ n = 0
have mpr : n = 0 → (embeddingUpIntGE p).BoundaryGE n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE n
⊢ n = 0
have mp : ∀ (h : (embeddingUpIntGE p).BoundaryGE 0), Eq (α := ℕ) 0 0
Tactic: obtain _ | n := n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE n
mp : ∀ (h : (embeddingUpIntGE p).BoundaryGE 0), Eq (α := ℕ) 0 0
⊢ n = 0
have mp₁ : ∀ (n : ℕ) (h : (embeddingUpIntGE p).BoundaryGE (n + 1)), n + 1 = 0
Tactic: obtain _ | n := n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (hypothesis)
Goal:
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
⊢ n + 1 = 0
have this : ¬(up ℤ).Rel ((embeddingUpIntGE p).f n) ((embeddingUpIntGE p).f (n + 1))
Tactic: have := h.2 n
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
p : ℤ
⊢ (embeddingUpIntGE p).BoundaryGE 0
have mpr : (up ℤ).Rel ((up ℤ).prev ((embeddingUpIntGE p).f 0)) ((embeddingUpIntGE p).f 0)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
p : ℤ
mpr : (up ℤ).Rel ((up ℤ).prev ((embeddingUpIntGE p).f 0)) ((embeddingUpIntGE p).f 0)
⊢ (embeddingUpIntGE p).BoundaryGE 0
have mpr₁ : ∀ (i : ℕ), ¬(up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
p : ℤ
n : ℕ
⊢ (embeddingUpIntLE p).BoundaryLE n ↔ n = 0
have mp : (embeddingUpIntLE p).BoundaryLE n → n = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
p : ℤ
n : ℕ
mp : (embeddingUpIntLE p).BoundaryLE n → n = 0
⊢ (embeddingUpIntLE p).BoundaryLE n ↔ n = 0
have mpr : n = 0 → (embeddingUpIntLE p).BoundaryLE n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE n
⊢ n = 0
have mp : ∀ (h : (embeddingUpIntLE p).BoundaryLE 0), Eq (α := ℕ) 0 0
Tactic: obtain _ | n := n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE n
mp : ∀ (h : (embeddingUpIntLE p).BoundaryLE 0), Eq (α := ℕ) 0 0
⊢ n = 0
have mp₁ : ∀ (n : ℕ) (h : (embeddingUpIntLE p).BoundaryLE (n + 1)), n + 1 = 0
Tactic: obtain _ | n := n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (hypothesis)
Goal:
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE (n + 1)
⊢ n + 1 = 0
have this : ¬(up ℤ).Rel ((embeddingUpIntLE p).f (n + 1)) ((embeddingUpIntLE p).f n)
Tactic: have := h.2 n
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
p : ℤ
⊢ (embeddingUpIntLE p).BoundaryLE 0
have mpr : (up ℤ).Rel ((embeddingUpIntLE p).f 0) ((up ℤ).next ((embeddingUpIntLE p).f 0))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Boundary (goal)
Goal:
p : ℤ
mpr : (up ℤ).Rel ((embeddingUpIntLE p).f 0) ((up ℤ).next ((embeddingUpIntLE p).f 0))
⊢ (embeddingUpIntLE p).BoundaryLE 0
have mpr₁ : ∀ (k : ℕ), ¬(up ℤ).Rel ((embeddingUpIntLE p).f 0) ((embeddingUpIntLE p).f k)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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
⊢ QuasiIsoAt (K := K.truncLE n) (K.ιTruncLE n) q
have obtain : ∀ (k : ℕ) (hq : q ≤ q + (↑k : ℤ)), QuasiIsoAt (K := K.truncLE (q + (↑k : ℤ))) (K.ιTruncLE (q + (↑k : ℤ))) q
Tactic: obtain ⟨k, rfl⟩ := Int.le.dest hq
Cleared hypotheses: n, hq
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 : n ≤ q
⊢ QuasiIsoAt (L := K.truncGE n) (K.πTruncGE n) q
have obtain : ∀ (k : ℕ) (hq : n ≤ n + (↑k : ℤ)), QuasiIsoAt (L := K.truncGE n) (K.πTruncGE n) (n + (↑k : ℤ))
Tactic: obtain ⟨k, rfl⟩ := Int.le.dest hq
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
n : ℤ
⊢ K.IsStrictlyGE n ↔ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
have mp : K.IsStrictlyGE n → ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
n : ℤ
mp : K.IsStrictlyGE n → ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
⊢ K.IsStrictlyGE n ↔ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
have mpr : (∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)) → K.IsStrictlyGE n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
n : ℤ
h : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
⊢ K.IsStrictlyGE n
have mpr : ∀ (i : ℤ) (hi : ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i), IsZero.{v_1, u_1} (K.X i)
Tactic: refine IsStrictlySupported.mk (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (hypothesis)
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 ℤ
n : ℤ
h : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i
⊢ IsZero.{v_1, u_1} (K.X i)
have hi₁ : i < n
Tactic: rw [notMem_range_embeddingUpIntGE_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
n : ℤ
⊢ K.IsStrictlyLE n ↔ ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X i)
have mp : K.IsStrictlyLE n → ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
n : ℤ
mp : K.IsStrictlyLE n → ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X i)
⊢ K.IsStrictlyLE n ↔ ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X i)
have mpr : (∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X i)) → K.IsStrictlyLE n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X i)
⊢ K.IsStrictlyLE n
have mpr : ∀ (i : ℤ) (hi : ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i), IsZero.{v_1, u_1} (K.X i)
Tactic: refine IsStrictlySupported.mk (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (hypothesis)
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 ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X i)
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i
⊢ IsZero.{v_1, u_1} (K.X i)
have hi₁ : n < i
Tactic: rw [notMem_range_embeddingUpIntLE_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
n : ℤ
⊢ K.IsGE n ↔ ∀ i < n, ExactAt K i
have mp : K.IsGE n → ∀ i < n, ExactAt K i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
n : ℤ
mp : K.IsGE n → ∀ i < n, ExactAt K i
⊢ K.IsGE n ↔ ∀ i < n, ExactAt K i
have mpr : (∀ i < n, ExactAt K i) → K.IsGE n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
⊢ K.IsGE n
have mpr : ∀ (i : ℤ) (hi : ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i), ExactAt K i
Tactic: refine IsSupported.mk (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (hypothesis)
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 ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i
⊢ ExactAt K i
have hi₁ : i < n
Tactic: rw [notMem_range_embeddingUpIntGE_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
n : ℤ
⊢ K.IsLE n ↔ ∀ (i : ℤ), n < i → ExactAt K i
have mp : K.IsLE n → ∀ (i : ℤ), n < i → ExactAt K i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
n : ℤ
mp : K.IsLE n → ∀ (i : ℤ), n < i → ExactAt K i
⊢ K.IsLE n ↔ ∀ (i : ℤ), n < i → ExactAt K i
have mpr : (∀ (i : ℤ), n < i → ExactAt K i) → K.IsLE n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
⊢ K.IsLE n
have mpr : ∀ (i : ℤ) (hi : ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i), ExactAt K i
Tactic: refine IsSupported.mk (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (hypothesis)
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 ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i
⊢ ExactAt K i
have hi₁ : n < i
Tactic: rw [notMem_range_embeddingUpIntLE_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsStrictlyLE p
⊢ K.IsStrictlyLE q
have rw : ∀ (i : ℤ), q < i → IsZero.{v_1, u_1} (K.X i)
Tactic: rw [isStrictlyLE_iff]