awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
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₁)
⊢ (K.shortComplexTruncLE e₁).X₃.ExactAt (e₁.f i₁)

Tactic:
have h₂ := (K.shortComplexTruncLE_X₃_isSupportedOutside e₁).exactAt i₁
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
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₁)
h₂ : (K.shortComplexTruncLE e₁).X₃.ExactAt (e₁.f i₁)
⊢ QuasiIsoAt (K := (K.shortComplexTruncLE e₁).X₃) (L := K.truncGE e₂) (K.shortComplexTruncLEX₃ToTruncGE ac) (e₁.f i₁)

Tactic:
simpa only [quasiIsoAt_iff_exactAt _ _ h₂] using h₁

Premises used: quasiIsoAt_iff_exactAt
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
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.shortComplexTruncLE e₁).g (e₂.f i₂)

Tactic:
have := quasiIsoAt_shortComplexTruncLE_g K e₁ (e₂.f i₂) (fun _ => ac.disjoint _ _)
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
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₂)
inr : QuasiIsoAt (L := K.truncGE e₂) (K.πTruncGE e₂) (e₂.f i₂)
⊢ QuasiIsoAt (K := (K.shortComplexTruncLE e₁).X₃) (L := K.truncGE e₂) (K.shortComplexTruncLEX₃ToTruncGE ac) (e₂.f i₂)

Tactic:
rw [← quasiIsoAt_iff_comp_left (K.shortComplexTruncLE e₁).g
        (K.shortComplexTruncLEX₃ToTruncGE ac), g_shortComplexTruncLEX₃ToTruncGE]

Premises used: HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE, HomologicalComplex.shortComplexTruncLE, HomologicalComplex.shortComplexTruncLEX₃ToTruncGE, quasiIsoAt_iff_comp_left, CategoryTheory.ShortComplex.g
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
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₂)
inr : QuasiIsoAt (L := K.truncGE e₂) (K.πTruncGE e₂) (e₂.f i₂)
⊢ QuasiIsoAt (L := K.truncGE e₂) (K.πTruncGE e₂) (e₂.f i₂)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Embedding.AreComplementary
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₂)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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₂
mpr : c.Rel i₁ i₂ → c'.Rel (e.f i₁) (e.f i₂)
⊢ c'.Rel (e.f i₁) (e.f i₂) ↔ c.Rel i₁ i₂

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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₂

Tactic:
apply IsRelIff.rel'

Premises used: ComplexShape.Embedding.IsRelIff.rel'
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
i₁ i₂ : ι
⊢ c.Rel i₁ i₂ → c'.Rel (e.f i₁) (e.f i₂)

Tactic:
e.rel

Premises used: ComplexShape.Embedding.rel
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
i₁ i₂ : ι
⊢ c.Rel i₁ i₂ → c'.Rel (e.f i₁) (e.f i₂)

Tactic:
exact e.rel

Premises used: ComplexShape.Embedding.rel
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsTruncGE
j : ι
k' : ι'
h : c'.Rel (e.f j) k'
⊢ ∃ (k : ι), e.f k = k'

Tactic:
IsTruncGE.mem_next h

Premises used: ComplexShape.Embedding.IsTruncGE.mem_next
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsTruncLE
i' : ι'
j : ι
h : c'.Rel i' (e.f j)
⊢ ∃ (i : ι), e.f i = i'

Tactic:
IsTruncLE.mem_prev h

Premises used: ComplexShape.Embedding.IsTruncLE.mem_prev
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
⊢ ∃ (i : ι), e.f i = i'

Tactic:
have h : ∃ (i : ι), e.f i = i' := ⟨i, hi⟩
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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'
⊢ h.choose (p := fun (i : ι) ↦ e.f i = i') = i

Tactic:
have : h.choose = i := e.injective_f (h.choose_spec.trans (hi.symm))
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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
rw₁ rw₂ : some 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

Tactic:
rw [dif_pos ⟨i, hi⟩, this]

Premises used: dif_pos
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
hi : ∀ (i : ι), e.f i ≠ i'
i : ι
hi' : e.f i = i'
⊢ False

Tactic:
hi i hi'
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
hi : ∀ (i : ι), e.f i ≠ i'
i : ι
hi' : e.f i = i'
⊢ False

Tactic:
exact hi i hi'
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
⊢ e.r (e.f i) = some i

Tactic:
r_eq_some _ rfl

Premises used: ComplexShape.Embedding.r_eq_some, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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'
neg : ∀ (h : ¬∃ (k : ι), e.f k = i'), e.f i = i'
⊢ e.f i = i'

Tactic:
by_cases h : ∃ (k : ι), e.f k = i'
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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'
pos : ∀ (k : ι) (hi : e.r (e.f k) = some i), e.f i = e.f k
⊢ e.f i = i'

Tactic:
obtain ⟨k, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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
⊢ some k = some i

Tactic:
rw [r_f] at hi

Premises used: ComplexShape.Embedding.r_f
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i k : ι
hi : some k = some i
pos : i = k
⊢ e.f i = e.f k

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i k : ι
hi : some k = some i
⊢ i = k

Tactic:
simpa using hi.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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'

Tactic:
simp [e.r_eq_none i' (by simpa using h)] at hi

Premises used: ComplexShape.Embedding.r_eq_none
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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 x x_1 : A
h : Eq.{u_3 + 1} (α := A) ((fun (x : A) ↦ x + b) x) ((fun (x : A) ↦ x + b) x_1)
⊢ x = x_1

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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
dsimp : ∀ (i₁ i₂ : A), i₁ + a = i₂ ↔ i₁ + b + a = i₂ + b
⊢ ∀ (i₁ i₂ : A), (up' a).Rel i₁ i₂ ↔ (up' a).Rel ((fun (x : A) ↦ x + b) i₁) ((fun (x : A) ↦ x + b) i₂)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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
simp_rw₁ : ∀ (i₁ i₂ : A), True
⊢ ∀ (i₁ i₂ : A), i₁ + a = i₂ ↔ i₁ + b + a = i₂ + b

Tactic:
simp_rw [add_right_comm _ b a, add_right_cancel_iff, implies_true]

Premises used: add_right_comm, add_right_cancel_iff, implies_true
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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
⊢ (Embedding.mk' (up' a) (up' a) (fun (x : A) ↦ x + b) ⋯ ⋯).IsRelIff

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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
dsimp : ∀ (i₁ i₂ : A), i₂ + a = i₁ ↔ i₂ + b + a = i₁ + b
⊢ ∀ (i₁ i₂ : A), (down' a).Rel i₁ i₂ ↔ (down' a).Rel ((fun (x : A) ↦ x + b) i₁) ((fun (x : A) ↦ x + b) i₂)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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
simp_rw₁ : ∀ (i₁ i₂ : A), True
⊢ ∀ (i₁ i₂ : A), i₂ + a = i₁ ↔ i₂ + b + a = i₁ + b

Tactic:
simp_rw [add_right_comm _ b a, add_right_cancel_iff, implies_true]

Premises used: add_right_comm, add_right_cancel_iff, implies_true
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
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
⊢ (Embedding.mk' (down' a) (down' a) (fun (x : A) ↦ x + b) ⋯ ⋯).IsRelIff

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
x x_1 : ℕ
h : Eq (α := ℤ) ((fun (n : ℕ) ↦ ((↑n : ℤ) : ℤ)) x) ((fun (n : ℕ) ↦ ((↑n : ℤ) : ℤ)) x_1)
⊢ x = x_1

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
⊢ ∀ (i₁ i₂ : ℕ), i₁ + 1 = i₂ ↔ HAdd.hAdd (α := ℤ) (↑i₁ : ℤ) 1 = (↑i₂ : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
⊢ (Embedding.mk' (up ℕ) (up ℤ) (fun (n : ℕ) ↦ (↑n : ℤ)) ⋯ embeddingUpNat._proof_3).IsRelIff

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
x x_1 : ℕ
h : Eq (α := ℤ) ((fun (n : ℕ) ↦ (-(↑n : ℤ) : ℤ)) x) ((fun (n : ℕ) ↦ (-(↑n : ℤ) : ℤ)) x_1)
⊢ x = x_1

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
⊢ ∀ (i₁ i₂ : ℕ), i₂ + 1 = i₁ ↔ HAdd.hAdd (α := ℤ) (-(↑i₁ : ℤ)) 1 = -(↑i₂ : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
⊢ (Embedding.mk' (down ℕ) (up ℤ) (fun (n : ℕ) ↦ -(↑n : ℤ)) ⋯ embeddingDownNat._proof_3).IsRelIff

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
i : ℤ
j : ℕ
h : i + 1 = -(↑j : ℤ)
⊢ -HAdd.hAdd (α := ℤ) (↑j : ℤ) 1 = i

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
x x_1 : ℕ
h : p + (↑x : ℤ) = p + (↑x_1 : ℤ)
⊢ x = x_1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
⊢ ∀ (i₁ i₂ : ℕ), i₁ + 1 = i₂ ↔ p + (↑i₁ : ℤ) + 1 = p + (↑i₂ : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
⊢ (Embedding.mk' (up ℕ) (up ℤ) (fun (n : ℕ) ↦ p + (↑n : ℤ)) ⋯ ⋯).IsRelIff

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
j : ℕ
x : ℤ
h : p + (↑j : ℤ) + 1 = x
⊢ p + HAdd.hAdd (α := ℤ) (↑j : ℤ) 1 = x

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
x x_1 : ℕ
h : p - (↑x : ℤ) = p - (↑x_1 : ℤ)
⊢ x = x_1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
⊢ ∀ (i₁ i₂ : ℕ), i₂ + 1 = i₁ ↔ p - (↑i₁ : ℤ) + 1 = p - (↑i₂ : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
⊢ (Embedding.mk' (down ℕ) (up ℤ) (fun (n : ℕ) ↦ p - (↑n : ℤ)) ⋯ ⋯).IsRelIff

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p x : ℤ
k : ℕ
h : x + 1 = p - (↑k : ℤ)
⊢ p - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 = x

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
p n : ℤ
mp : (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) → p < n
mpr : p < n → ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
⊢ (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) ↔ p < n

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
mp : ∀ (this : ¬p < n), False
⊢ p < n

Tactic:
by_contra
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
this : ¬p < n
⊢ p - (↑(p - n).natAbs : ℤ) = n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
this : ¬p < n
⊢ False

Tactic:
exact h (p - n).natAbs (by simp; lia)

Premises used: HSub.hSub, Int.natAbs
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
p n : ℤ
h : p < n
i : ℕ
⊢ ¬p - (↑i : ℤ) = n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
p n : ℤ
mp : (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) → n < p
mpr : n < p → ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
⊢ (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) ↔ n < p

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
mp : ∀ (this : ¬n < p), False
⊢ n < p

Tactic:
by_contra
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
this : ¬n < p
⊢ p + (↑(n - p).natAbs : ℤ) = n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
this : ¬n < p
⊢ False

Tactic:
exact h (n - p).natAbs (by simp; lia)

Premises used: HSub.hSub, Int.natAbs
-- Module: Mathlib.Algebra.Homology.Embedding.Basic
Goal:
p n : ℤ
h : n < p
i : ℕ
⊢ ¬p + (↑i : ℤ) = n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
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)
right : ∀ (i : ι), ¬c'.Rel (e.f i) (e.f j)
⊢ e.BoundaryGE j

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
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'
⊢ c'.Rel (c'.prev (e.f j)) (e.f j)

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

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'
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 = i'
⊢ False

Tactic:
apply hi' i
-- Module: Mathlib.Algebra.Homology.Embedding.Boundary
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)
right₁ right₂ : e.f i = e.f i
⊢ e.f i = i'

Tactic:
rw [← c'.prev_eq' hj, c'.prev_eq' hi]

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 k : ι
hk : c.Rel j k
simp : c'.Rel (c'.prev (e.f k)) (e.f k) → ∃ (x : ι), c'.Rel (e.f x) (e.f k)
⊢ ¬(c'.Rel (c'.prev (e.f k)) (e.f k) ∧ ∀ (i : ι), ¬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
j k : ι
hk : c.Rel j k
h : c'.Rel (c'.prev (e.f k)) (e.f k)
⊢ c'.Rel (e.f j) (e.f k)

Tactic:
simpa only [e.rel_iff] using 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 k : ι
hk : c.Rel j k
h : c'.Rel (c'.prev (e.f k)) (e.f k)
⊢ ∃ (x : ι), c'.Rel (e.f x) (e.f k)

Tactic:
exact ⟨j, by simpa only [e.rel_iff] 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 : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
pos : ∀ (hjk : c.Rel j k), ¬e.BoundaryGE k
neg : ∀ (hjk : ¬c.Rel j k), ¬e.BoundaryGE k
⊢ ¬e.BoundaryGE 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 : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
hjk : c.Rel j k
⊢ ¬e.BoundaryGE k

Tactic:
e.not_boundaryGE_next hjk

Premises used: ComplexShape.Embedding.not_boundaryGE_next
-- 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 : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
hjk : c.Rel j k
⊢ ¬e.BoundaryGE k

Tactic:
exact e.not_boundaryGE_next hjk

Premises used: ComplexShape.Embedding.not_boundaryGE_next
-- 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 : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
hjk : ¬c.Rel j k
neg : ∀ (hjk : ¬c.Rel j (c.next j)), ¬e.BoundaryGE (c.next j)
⊢ ¬e.BoundaryGE k

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.BoundaryGE j
hjk : ¬c.Rel j (c.next j)
⊢ ¬e.BoundaryGE (c.next j)

Tactic:
simpa only [c.next_eq_self j hjk] using hj

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'
j : ι
hj : e.BoundaryGE j
i' : ι'
hi' : c'.Rel i' (e.f j)
a : ι
ha : e.f a = i'
⊢ c'.Rel (e.f a) (e.f j)

Tactic:
simpa only [ha] 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 : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
pos : ∀ (hij' : c.Rel i j), c'.prev (e.f j) = e.f i
neg : ∀ (hij' : ¬c.Rel i j), c'.prev (e.f j) = e.f i
⊢ c'.prev (e.f j) = e.f 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 : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : c.Rel i j
⊢ c'.Rel (e.f i) (e.f j)

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

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 : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : c.Rel i j
⊢ c'.prev (e.f j) = e.f i

Tactic:
exact c'.prev_eq' (by simpa only [e.rel_iff] using 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
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
⊢ ¬c.Rel (c.prev j) j

Tactic:
simpa only [hij] using hij'
-- 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 : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
⊢ j = i

Tactic:
simpa only [c.prev_eq_self j (by simpa only [hij] using hij')] using hij

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
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
neg : ∀ (hij : c.prev j = j) (hij' : ¬c.Rel j j), c'.prev (e.f j) = e.f j
⊢ c'.prev (e.f j) = e.f i

Tactic:
obtain rfl : j = i := by
      simpa only [c.prev_eq_self j (by simpa only [hij] using hij')] using hij

Premises used: rfl