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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
⊢ Function.Bijective (fromSum e₁ e₂)
have left : Function.Injective (fromSum e₁ e₂)
Tactic: constructor
-- 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
left : Function.Injective (fromSum e₁ e₂)
⊢ Function.Bijective (fromSum e₁ e₂)
have right : Function.Surjective (fromSum e₁ e₂)
Tactic: constructor
-- 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ j₁ : ι₁
h : fromSum e₁ e₂ (Sum.inl i₁) = fromSum e₁ e₂ (Sum.inl j₁)
⊢ Eq (α := ι₁ ⊕ ι₂) (Sum.inl i₁) (Sum.inl j₁)
have left : ∀ (h : fromSum e₁ e₂ (Sum.inl i₁) = fromSum e₁ e₂ (Sum.inl i₁)), Eq (α := ι₁ ⊕ ι₂) (Sum.inl i₁) (Sum.inl i₁)
Tactic: obtain rfl := e₁.injective_f h
Cleared hypotheses: j₁, h
-- 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ j₂ : ι₂
h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inr j₂)
⊢ Eq (α := ι₁ ⊕ ι₂) (Sum.inr i₂) (Sum.inr j₂)
have left : ∀ (h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inr i₂)), Eq (α := ι₁ ⊕ ι₂) (Sum.inr i₂) (Sum.inr i₂)
Tactic: obtain rfl := e₂.injective_f h
Cleared hypotheses: j₂, h
-- 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
n : ι
⊢ ∃ (a : ι₁ ⊕ ι₂), fromSum e₁ e₂ a = n
have right : ∀ (i₁ : ι₁), ∃ (a : ι₁ ⊕ ι₂), fromSum e₁ e₂ a = e₁.f i₁
Tactic: obtain ⟨i₁, rfl⟩ | ⟨i₂, rfl⟩ := ac.union n
Cleared hypotheses: n
-- 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
n : ι
right : ∀ (i₁ : ι₁), ∃ (a : ι₁ ⊕ ι₂), fromSum e₁ e₂ a = e₁.f i₁
⊢ ∃ (a : ι₁ ⊕ ι₂), fromSum e₁ e₂ a = n
have right₁ : ∀ (i₂ : ι₂), ∃ (a : ι₁ ⊕ ι₂), fromSum e₁ e₂ a = e₂.f i₂
Tactic: obtain ⟨i₁, rfl⟩ | ⟨i₂, rfl⟩ := ac.union n
Cleared hypotheses: n
-- 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₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i j : ι
hij : i = j
⊢ X i ≃ X j
have subst : X i ≃ X i
Tactic: subst hij
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.AreComplementary (goal)
Goal:
ι : Type u_1
X : ι → Type u_5
i j k : ι
hij : i = j
hjk : j = k
x : X i
⊢ Eq (α := X k) ((aux X j k hjk : (a : X j) → X k) ((aux X i j hij : (a : X i) → X j) x : X j) : X k)
    ((aux X i k ⋯ : (a : X i) → X k) x : X k)
have subst : Eq (α := X i) ((aux X i i sorry : (a : X i) → X i) ((aux X i i sorry : (a : X i) → X i) x : X i) : X i)
  ((aux X i i sorry : (a : X i) → X i) x : X i)
Tactic: subst hij hjk
Cleared hypotheses: j, k, hij, hjk
-- 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₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i : ι₁ ⊕ ι₂
i₁ : ι₁
h : Sum.inl i₁ = i
⊢ e₁.f i₁ = (ac.equiv : (a : ι₁ ⊕ ι₂) → ι) i
have subst : e₁.f i₁ = (ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inl i₁)
Tactic: subst h
Cleared hypotheses: i, h
-- 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i : ι₁ ⊕ ι₂
i₁ : ι₁
h : Sum.inl i₁ = i
⊢ ac.desc' (X := X) x₁ x₂ i =
    (desc.aux X (e₁.f i₁) ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) i) ⋯ :
        (a : X (e₁.f i₁)) → X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) i))
      (x₁ i₁)
have subst : Eq (α := X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inl i₁))) (ac.desc' (X := X) x₁ x₂ (Sum.inl i₁))
  ((desc.aux X (e₁.f i₁) ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inl i₁)) sorry :
      (a : X (e₁.f i₁)) → X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inl i₁)))
    (x₁ i₁))
Tactic: subst h
Cleared hypotheses: i, h
-- 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₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i : ι₁ ⊕ ι₂
i₂ : ι₂
h : Sum.inr i₂ = i
⊢ e₂.f i₂ = (ac.equiv : (a : ι₁ ⊕ ι₂) → ι) i
have subst : e₂.f i₂ = (ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inr i₂)
Tactic: subst h
Cleared hypotheses: i, h
-- 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i : ι₁ ⊕ ι₂
i₂ : ι₂
h : Sum.inr i₂ = i
⊢ ac.desc' (X := X) x₁ x₂ i =
    (desc.aux X (e₂.f i₂) ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) i) ⋯ :
        (a : X (e₂.f i₂)) → X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) i))
      (x₂ i₂)
have subst : Eq (α := X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inr i₂))) (ac.desc' (X := X) x₁ x₂ (Sum.inr i₂))
  ((desc.aux X (e₂.f i₂) ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inr i₂)) sorry :
      (a : X (e₂.f i₂)) → X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) (Sum.inr i₂)))
    (x₂ i₂))
Tactic: subst h
Cleared hypotheses: i, h
-- 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
⊢ ac.desc (X := X) x₁ x₂ (e₁.f i₁) = x₁ i₁
have dsimp : (desc.aux X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₁.f i₁) : ι₁ ⊕ ι₂)) (e₁.f i₁) sorry :
      (a : X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₁.f i₁)))) → X (e₁.f i₁))
    (ac.desc' (X := X) x₁ x₂ ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₁.f i₁))) =
  x₁ i₁
Tactic: dsimp [desc]
-- 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
⊢ (desc.aux X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₁.f i₁) : ι₁ ⊕ ι₂)) (e₁.f i₁) ⋯ :
        (a : X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₁.f i₁)))) → X (e₁.f i₁))
      (ac.desc' (X := X) x₁ x₂ ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₁.f i₁))) =
    x₁ i₁
have rw : (desc.aux X (e₁.f i₁) (e₁.f i₁) sorry : (a : X (e₁.f i₁)) → X (e₁.f i₁)) (x₁ i₁) = x₁ i₁
Tactic: rw [ac.desc'_inl _ _ _ i₁ (ac.equiv.injective (by simp)), desc.aux_trans]
-- 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
⊢ ac.desc (X := X) x₁ x₂ (e₂.f i₂) = x₂ i₂
have dsimp : (desc.aux X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₂.f i₂) : ι₁ ⊕ ι₂)) (e₂.f i₂) sorry :
      (a : X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₂.f i₂)))) → X (e₂.f i₂))
    (ac.desc' (X := X) x₁ x₂ ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₂.f i₂))) =
  x₂ i₂
Tactic: dsimp [desc]
-- 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
⊢ (desc.aux X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₂.f i₂) : ι₁ ⊕ ι₂)) (e₂.f i₂) ⋯ :
        (a : X ((ac.equiv : (a : ι₁ ⊕ ι₂) → ι) ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₂.f i₂)))) → X (e₂.f i₂))
      (ac.desc' (X := X) x₁ x₂ ((ac.equiv.symm : (a : ι) → ι₁ ⊕ ι₂) (e₂.f i₂))) =
    x₂ i₂
have rw : (desc.aux X (e₂.f i₂) (e₂.f i₂) sorry : (a : X (e₂.f i₂)) → X (e₂.f i₂)) (x₂ i₂) = x₂ i₂
Tactic: rw [ac.desc'_inr _ _ _ i₂ (ac.equiv.injective (by simp)), desc.aux_trans]
-- 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 : HomologicalComplex.{v_1, u_4, u_1} C c
⊢ K.IsStrictlySupportedOutside e₁ ↔ K.IsStrictlySupported e₂
have mp : K.IsStrictlySupportedOutside e₁ → K.IsStrictlySupported e₂
Tactic: constructor
-- 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 : HomologicalComplex.{v_1, u_4, u_1} C c
mp : K.IsStrictlySupportedOutside e₁ → K.IsStrictlySupported e₂
⊢ K.IsStrictlySupportedOutside e₁ ↔ K.IsStrictlySupported e₂
have mpr : K.IsStrictlySupported e₂ → K.IsStrictlySupportedOutside e₁
Tactic: constructor
-- 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 : HomologicalComplex.{v_1, u_4, u_1} C c
h : K.IsStrictlySupportedOutside e₁
i : ι
hi : ∀ (i_1 : ι₂), e₂.f i_1 ≠ i
⊢ IsZero.{v_1, u_4} (K.X i)
have obtain : ∀ (i₁ : ι₁) (hi : ∀ (i : ι₂), e₂.f i ≠ e₁.f i₁), IsZero.{v_1, u_4} (K.X (e₁.f i₁))
Tactic: obtain ⟨i₁, rfl⟩ := ac.exists_i₁ i hi
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 : HasZeroMorphisms.{v_1, u_4} C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex.{v_1, u_4, u_1} C c
⊢ K.IsSupportedOutside e₁ ↔ K.IsSupported e₂
have mp : K.IsSupportedOutside e₁ → K.IsSupported e₂
Tactic: constructor
-- 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 : HomologicalComplex.{v_1, u_4, u_1} C c
mp : K.IsSupportedOutside e₁ → K.IsSupported e₂
⊢ K.IsSupportedOutside e₁ ↔ K.IsSupported e₂
have mpr : K.IsSupported e₂ → K.IsSupportedOutside e₁
Tactic: constructor
-- 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 : HomologicalComplex.{v_1, u_4, u_1} C c
h : K.IsSupportedOutside e₁
i : ι
hi : ∀ (i_1 : ι₂), e₂.f i_1 ≠ i
⊢ K.ExactAt i
have obtain : ∀ (i₁ : ι₁) (hi : ∀ (i : ι₂), e₂.f i ≠ e₁.f i₁), K.ExactAt (e₁.f i₁)
Tactic: obtain ⟨i₁, rfl⟩ := ac.exists_i₁ i hi
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 : 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
φ : K ⟶ L
hK : K.IsStrictlySupportedOutside e₂
hL : L.IsStrictlySupportedOutside e₁
⊢ φ = 0
have h : ∀ (i : ι), φ.f i = HomologicalComplex.Hom.f 0 i
Tactic: ext 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 : 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
φ : K ⟶ L
hK : K.IsStrictlySupportedOutside e₂
hL : L.IsStrictlySupportedOutside e₁
i : ι
⊢ φ.f i = HomologicalComplex.Hom.f 0 i
have h : ∀ (i₁ : ι₁), φ.f (e₁.f i₁) = HomologicalComplex.Hom.f 0 (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 : 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
φ : K ⟶ L
hK : K.IsStrictlySupportedOutside e₂
hL : L.IsStrictlySupportedOutside e₁
i : ι
h : ∀ (i₁ : ι₁), φ.f (e₁.f i₁) = HomologicalComplex.Hom.f 0 (e₁.f i₁)
⊢ φ.f i = HomologicalComplex.Hom.f 0 i
have h₁ : ∀ (i₂ : ι₂), φ.f (e₂.f i₂) = HomologicalComplex.Hom.f 0 (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 : 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
inst_2 : K.IsStrictlySupported e₁
inst_3 : L.IsStrictlySupported e₂
φ : K ⟶ L
⊢ φ = 0
have hK : K.IsStrictlySupportedOutside e₂
Tactic: apply ac.hom_ext'
-- 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
inst_2 : K.IsStrictlySupported e₁
inst_3 : L.IsStrictlySupported e₂
φ : K ⟶ L
hK : K.IsStrictlySupportedOutside e₂
⊢ φ = 0
have hL : L.IsStrictlySupportedOutside e₁
Tactic: apply ac.hom_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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
h : e₁.BoundaryLE i₁
⊢ ∃ (i₂ : ι₂), ac.Boundary i₁ i₂
have h₁ : c.Rel (e₁.f i₁) (c.next (e₁.f i₁))
Tactic: obtain ⟨h₁, h₂⟩ := h
Cleared hypotheses: 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
h : e₁.BoundaryLE i₁
h₁ : c.Rel (e₁.f i₁) (c.next (e₁.f i₁))
⊢ ∃ (i₂ : ι₂), ac.Boundary i₁ i₂
have h₂ : ∀ (k : ι₁), ¬c.Rel (e₁.f i₁) (e₁.f k)
Tactic: obtain ⟨h₁, h₂⟩ := h
Cleared hypotheses: h
-- 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
h₁ : c.Rel (e₁.f i₁) (c.next (e₁.f i₁))
h₂ : ∀ (k : ι₁), ¬c.Rel (e₁.f i₁) (e₁.f k)
⊢ ∃ (i₂ : ι₂), ac.Boundary i₁ i₂
have obtain : ∀ (i₂ : ι₂) (hi₂ : c.next (e₁.f i₁) = e₂.f i₂), ∃ (i₂ : ι₂), ac.Boundary i₁ i₂
Tactic: obtain ⟨i₂, hi₂⟩ := ac.exists_i₂ (c.next (e₁.f i₁))
    (fun i₁' hi₁' => h₂ i₁' (by simpa only [← hi₁'] using 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ : ι₂
h : e₂.BoundaryGE i₂
⊢ ∃ (i₁ : ι₁), ac.Boundary i₁ i₂
have h₁ : c.Rel (c.prev (e₂.f i₂)) (e₂.f i₂)
Tactic: obtain ⟨h₁, h₂⟩ := h
Cleared hypotheses: 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ : ι₂
h : e₂.BoundaryGE i₂
h₁ : c.Rel (c.prev (e₂.f i₂)) (e₂.f i₂)
⊢ ∃ (i₁ : ι₁), ac.Boundary i₁ i₂
have h₂ : ∀ (i : ι₂), ¬c.Rel (e₂.f i) (e₂.f i₂)
Tactic: obtain ⟨h₁, h₂⟩ := h
Cleared hypotheses: h
-- 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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ : ι₂
h₁ : c.Rel (c.prev (e₂.f i₂)) (e₂.f i₂)
h₂ : ∀ (i : ι₂), ¬c.Rel (e₂.f i) (e₂.f i₂)
⊢ ∃ (i₁ : ι₁), ac.Boundary i₁ i₂
have obtain : ∀ (i₁ : ι₁) (hi₁ : c.prev (e₂.f i₂) = e₁.f i₁), ∃ (i₁ : ι₁), ac.Boundary i₁ i₂
Tactic: obtain ⟨i₁, hi₁⟩ := ac.exists_i₁ (c.prev (e₂.f i₂))
    (fun i₂' hi₂' => h₂ i₂' (by simpa only [← hi₂'] using h₁))
-- 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₁.BoundaryLE
i₁ : ι₁
h : e₁.BoundaryLE i₁
⊢ (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))
      ((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))
        (Subtype.mk (p := e₁.BoundaryLE) i₁ h)) =
    Subtype.mk (p := e₁.BoundaryLE) i₁ h
have a : (↑((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))
        ((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))
          (Subtype.mk (p := e₁.BoundaryLE) i₁ h))) :
    ι₁) =
  (↑(Subtype.mk (p := e₁.BoundaryLE) 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₁.BoundaryLE
i₁ : ι₁
h : e₁.BoundaryLE i₁
⊢ (↑((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))
          ((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))
            (Subtype.mk (p := e₁.BoundaryLE) i₁ h))) :
      ι₁) =
    (↑(Subtype.mk (p := e₁.BoundaryLE) i₁ h) : ι₁)
have h' : ac.Boundary i₁ (indexOfBoundaryLE ac h)
Tactic: have h' := of_boundaryLE 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₁.BoundaryLE
i₁ : ι₁
h : e₁.BoundaryLE i₁
h' : ac.Boundary i₁ (indexOfBoundaryLE ac h)
⊢ (↑((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))
          ((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))
            (Subtype.mk (p := e₁.BoundaryLE) i₁ h))) :
      ι₁) =
    (↑(Subtype.mk (p := e₁.BoundaryLE) i₁ h) : ι₁)
have h'' : ac.Boundary (indexOfBoundaryGE ac sorry) (indexOfBoundaryLE ac h)
Tactic: have h'' := of_boundaryGE ac h'.snd