awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun (x : Γ') ↦ false) main aux
          (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
            (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S
h : codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
H₂ : codeSupp' f k.cons₂ ⊆ S ∧ trStmts₁ (head stack (Λ'.ret k)) ⊆ S ∧ contSupp k ⊆ S
⊢ Supports (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) S

Tactic:
exact trStmts₁_supports' (head_supports H₂.2.2) (Finset.union_subset_right h) IH
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp k.cons₂ ⊆ S
⊢ contSupp k.cons₂ ⊆ S

Tactic:
have H' := H
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H H' : contSupp k.cons₂ ⊆ S
⊢ trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k ⊆ S

Tactic:
rw [contSupp_cons₂] at H'

Premises used: Turing.PartrecToTM2.contSupp_cons₂
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp k.cons₂ ⊆ S
H' : trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k ⊆ S
⊢ Supports (contSupp k.cons₂) S

Tactic:
trStmts₁_supports' (head_supports <| Finset.union_subset_right H') H' IH

Premises used: Finset.union_subset_right, Turing.PartrecToTM2.trStmts₁_supports', Turing.PartrecToTM2.head_supports, Turing.PartrecToTM2.contSupp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp k.cons₂ ⊆ S
H' : trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k ⊆ S
⊢ Supports (contSupp k.cons₂) S

Tactic:
exact trStmts₁_supports' (head_supports <| Finset.union_subset_right H') H' IH
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
⊢ contSupp (Cont'.comp f k) ⊆ S

Tactic:
have H' := H
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H H' : contSupp (Cont'.comp f k) ⊆ S
⊢ codeSupp f k ⊆ S

Tactic:
rw [contSupp_comp] at H'

Premises used: Turing.PartrecToTM2.contSupp_comp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
H' : codeSupp f k ⊆ S
⊢ contSupp k ⊆ S

Tactic:
have H₂ := Finset.union_subset_right H'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
H' : codeSupp f k ⊆ S
H₂ : contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S

Tactic:
supports_union.2 ⟨codeSupp'_supports H', IH H₂⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, Turing.PartrecToTM2.contSupp, Turing.PartrecToTM2.codeSupp'_supports, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
H' : codeSupp f k ⊆ S
H₂ : contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S

Tactic:
exact supports_union.2 ⟨codeSupp'_supports H', IH H₂⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, Turing.PartrecToTM2.codeSupp'_supports, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : contSupp (Cont'.fix f k) ⊆ S
⊢ codeSupp' f.fix k ∪ contSupp k ⊆ S

Tactic:
rw [contSupp] at H

Premises used: Turing.PartrecToTM2.contSupp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : codeSupp' f.fix k ∪ contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.fix f k)) S

Tactic:
supports_union.2 ⟨codeSupp'_supports H, IH (Finset.union_subset_right H)⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, Finset.union_subset_right, Turing.PartrecToTM2.contSupp, Turing.PartrecToTM2.codeSupp'_supports, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
f : Code
k : Cont'
IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S
H : codeSupp' f.fix k ∪ contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.fix f k)) S

Tactic:
exact supports_union.2 ⟨codeSupp'_supports H, IH (Finset.union_subset_right H)⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, Finset.union_subset_right, Turing.PartrecToTM2.codeSupp'_supports, And.intro
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
k : Cont'
H : contSupp k ⊆ S
halt : ∀ (H : contSupp Cont'.halt ⊆ S), Supports (contSupp Cont'.halt) S
cons₁ :
  ∀ (f : Code) (k : Cont') (IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S) (H : contSupp (Cont'.cons₁ f k) ⊆ S),
    Supports (contSupp (Cont'.cons₁ f k)) S
cons₂ :
  ∀ (k : Cont') (IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S) (H : contSupp k.cons₂ ⊆ S),
    Supports (contSupp k.cons₂) S
comp :
  ∀ (f : Code) (k : Cont') (IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S) (H : contSupp (Cont'.comp f k) ⊆ S),
    Supports (contSupp (Cont'.comp f k)) S
fix :
  ∀ (f : Code) (k : Cont') (IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S) (H : contSupp (Cont'.fix f k) ⊆ S),
    Supports (contSupp (Cont'.fix f k)) S
⊢ Supports (contSupp k) S

Tactic:
induction k with
  | halt => simp [contSupp_halt, Supports]
  | cons₁ f k IH =>
    have H₁ := H; rw [contSupp_cons₁] at H₁; have H₂ := Finset.union_subset_right H₁
    refine trStmts₁_supports' (trNormal_supports H₂) H₁ fun h => ?_
    refine supports_union.2 ⟨codeSupp'_supports H₂, ?_⟩
    simp only [codeSupp, contSupp_cons₂, Finset.union_subset_iff] at H₂
    exact trStmts₁_supports' (head_supports H₂.2.2) (Finset.union_subset_right h) IH
  | cons₂ k IH =>
    have H' := H; rw [contSupp_cons₂] at H'
    exact trStmts₁_supports' (head_supports <| Finset.union_subset_right H') H' IH
  | comp f k IH =>
    have H' := H; rw [contSupp_comp] at H'; have H₂ := Finset.union_subset_right H'
    exact supports_union.2 ⟨codeSupp'_supports H', IH H₂⟩
  | fix f k IH =>
    rw [contSupp] at H
    exact supports_union.2 ⟨codeSupp'_supports H, IH (Finset.union_subset_right H)⟩

Premises used: Turing.PartrecToTM2.contSupp_comp, Turing.PartrecToTM2.halt, Turing.PartrecToTM2.contSupp_halt, Turing.PartrecToTM2.Supports, Turing.PartrecToTM2.contSupp_cons₂, Turing.PartrecToTM2.contSupp, Turing.PartrecToTM2.codeSupp, Turing.PartrecToTM2.contSupp_cons₁, Finset.union_subset_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
S : Finset Λ'
c : Code
k : Cont'
H : codeSupp c k ⊆ S
⊢ Supports (codeSupp c k) S

Tactic:
supports_union.2 ⟨codeSupp'_supports H, contSupp_supports (Finset.union_subset_right H)⟩

Premises used: Iff.mpr, Turing.PartrecToTM2.supports_union, Finset.union_subset_right, Turing.PartrecToTM2.codeSupp'_supports, And.intro, Turing.PartrecToTM2.codeSupp, Turing.PartrecToTM2.contSupp_supports
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
k : Cont'
⊢ TM2.Supports (Γ := fun (x : K') ↦ Γ') tr (codeSupp c k)

Tactic:
⟨codeSupp_self _ _ (trStmts₁_self _), fun _ => codeSupp_supports (Finset.Subset.refl _) _⟩

Premises used: Turing.PartrecToTM2.codeSupp_supports, Turing.PartrecToTM2.codeSupp_self, Finset.Subset.refl, Turing.TM2.Supports, And.intro, Turing.PartrecToTM2.codeSupp, Turing.PartrecToTM2.trStmts₁_self
-- Module: Mathlib.Condensed.AB
Goal:
A : Type u_1
J : Type u_2
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} J
inst_2 : Preadditive.{v_1, u_1} A
inst_3 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X Stonean.toCompHaus.op) A
inst_4 : HasWeakSheafify.{u, v_1, u + 1, u_1} (coherentTopology CompHaus) A
inst_5 : HasWeakSheafify.{u, v_1, u + 1, u_1} (extensiveTopology Stonean) A
inst_6 : HasColimitsOfShape.{v_2, u_2, v_1, u_1} J A
inst_7 : HasExactColimitsOfShape.{v_1, v_2, u_1, u_2} J A
inst_8 : HasFiniteLimits.{v_1, u_1} A
e : Condensed.{u, v_1, u_1} A ≌ Sheaf.{u, v_1, u + 1, u_1} (extensiveTopology Stonean) A :=
  CategoryTheory.Equivalence.trans (CategoryTheory.Equivalence.symm (StoneanCompHaus.equivalence A))
    Presheaf.coherentExtensiveEquivalence
⊢ HasExactColimitsOfShape J (Condensed.{u, v_1, u_1} A)

Tactic:
HasExactColimitsOfShape.domain_of_functor _ e.functor

Premises used: CategoryTheory.HasExactColimitsOfShape.domain_of_functor, CategoryTheory.Equivalence.functor
-- Module: Mathlib.Condensed.AB
Goal:
A : Type u_1
J : Type u_2
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} J
inst_2 : Preadditive.{v_1, u_1} A
inst_3 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X Stonean.toCompHaus.op) A
inst_4 : HasWeakSheafify.{u, v_1, u + 1, u_1} (coherentTopology CompHaus) A
inst_5 : HasWeakSheafify.{u, v_1, u + 1, u_1} (extensiveTopology Stonean) A
inst_6 : HasColimitsOfShape.{v_2, u_2, v_1, u_1} J A
inst_7 : HasExactColimitsOfShape.{v_1, v_2, u_1, u_2} J A
inst_8 : HasFiniteLimits.{v_1, u_1} A
e : Condensed.{u, v_1, u_1} A ≌ Sheaf.{u, v_1, u + 1, u_1} (extensiveTopology Stonean) A :=
  CategoryTheory.Equivalence.trans (CategoryTheory.Equivalence.symm (StoneanCompHaus.equivalence A))
    Presheaf.coherentExtensiveEquivalence
⊢ HasExactColimitsOfShape J (Condensed.{u, v_1, u_1} A)

Tactic:
exact HasExactColimitsOfShape.domain_of_functor _ e.functor

Premises used: CategoryTheory.HasExactColimitsOfShape.domain_of_functor, CategoryTheory.Equivalence.functor
-- Module: Mathlib.Condensed.AB
Goal:
A : Type u_1
J : Type u_2
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} J
inst_2 : Preadditive.{v_1, u_1} A
inst_3 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X Stonean.toCompHaus.op) A
inst_4 : HasWeakSheafify.{u, v_1, u + 1, u_1} (coherentTopology CompHaus) A
inst_5 : HasWeakSheafify.{u, v_1, u + 1, u_1} (extensiveTopology Stonean) A
inst_6 : HasLimitsOfShape.{v_2, u_2, v_1, u_1} J A
inst_7 : HasExactLimitsOfShape.{v_1, v_2, u_1, u_2} J A
inst_8 : HasFiniteColimits.{v_1, u_1} A
e : Condensed.{u, v_1, u_1} A ≌ Sheaf.{u, v_1, u + 1, u_1} (extensiveTopology Stonean) A :=
  CategoryTheory.Equivalence.trans (CategoryTheory.Equivalence.symm (StoneanCompHaus.equivalence A))
    Presheaf.coherentExtensiveEquivalence
⊢ HasExactLimitsOfShape J (Condensed.{u, v_1, u_1} A)

Tactic:
HasExactLimitsOfShape.domain_of_functor _ e.functor

Premises used: CategoryTheory.HasExactLimitsOfShape.domain_of_functor, CategoryTheory.Equivalence.functor
-- Module: Mathlib.Condensed.AB
Goal:
A : Type u_1
J : Type u_2
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} J
inst_2 : Preadditive.{v_1, u_1} A
inst_3 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X Stonean.toCompHaus.op) A
inst_4 : HasWeakSheafify.{u, v_1, u + 1, u_1} (coherentTopology CompHaus) A
inst_5 : HasWeakSheafify.{u, v_1, u + 1, u_1} (extensiveTopology Stonean) A
inst_6 : HasLimitsOfShape.{v_2, u_2, v_1, u_1} J A
inst_7 : HasExactLimitsOfShape.{v_1, v_2, u_1, u_2} J A
inst_8 : HasFiniteColimits.{v_1, u_1} A
e : Condensed.{u, v_1, u_1} A ≌ Sheaf.{u, v_1, u + 1, u_1} (extensiveTopology Stonean) A :=
  CategoryTheory.Equivalence.trans (CategoryTheory.Equivalence.symm (StoneanCompHaus.equivalence A))
    Presheaf.coherentExtensiveEquivalence
⊢ HasExactLimitsOfShape J (Condensed.{u, v_1, u_1} A)

Tactic:
exact HasExactLimitsOfShape.domain_of_functor _ e.functor

Premises used: CategoryTheory.HasExactLimitsOfShape.domain_of_functor, CategoryTheory.Equivalence.functor
-- Module: Mathlib.Condensed.AB
Goal:
A : Type u_1
J : Type u_2
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} J
inst_2 : Preadditive.{v_1, u_1} A
inst_3 :
  ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{?u.19309, ?u.19309 + 1, v_1, u_1} (StructuredArrow X Stonean.toCompHaus.op) A
inst_4 : HasWeakSheafify.{u, v_1, u + 1, u_1} (coherentTopology CompHaus) A
inst_5 : HasWeakSheafify.{u, v_1, u + 1, u_1} (extensiveTopology Stonean) A
R : Type (u + 1)
inst_6 : Ring R
⊢ HasLimitsOfSize.{u, u + 1, u + 1, u + 2} (ModuleCat R)

Tactic:
hasLimitsOfSizeShrink.{u, u + 1, u + 1, u} _

Premises used: CategoryTheory.Limits.hasLimitsOfSizeShrink
-- Module: Mathlib.Condensed.AB
Goal:
A : Type u_1
J : Type u_2
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} J
inst_2 : Preadditive.{v_1, u_1} A
inst_3 :
  ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{?u.74087, ?u.74087 + 1, v_1, u_1} (StructuredArrow X Stonean.toCompHaus.op) A
inst_4 : HasWeakSheafify.{u, v_1, u + 1, u_1} (coherentTopology CompHaus) A
inst_5 : HasWeakSheafify.{u, v_1, u + 1, u_1} (extensiveTopology Stonean) A
R : Type (u + 1)
inst_6 : Ring R
X Y : CondensedMod R
⊢ AB4.{u + 1, u + 2} (CondensedMod R)

Tactic:
AB4.of_AB5 _

Premises used: CategoryTheory.AB4.of_AB5
-- Module: Mathlib.Condensed.Basic
Goal:
C : Type w
inst : Category.{v, w} C
X : Condensed.{u, v, w} C
⊢ InducedCategory.Hom.hom (𝟙 X) = 𝟙 (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Condensed.Basic
Goal:
C : Type w
inst : Category.{v, w} C
X Y Z : Condensed.{u, v, w} C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).hom = f.hom ≫ g.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Condensed.Basic
Goal:
C : Type w
inst : Category.{v, w} C
X Y : Condensed.{u, v, w} C
f g : X ⟶ Y
h h₁ : ∀ (x : CompHausᵒᵖ), f.hom.app x = g.hom.app x
⊢ f = g

Tactic:
ext
-- Module: Mathlib.Condensed.Basic
Goal:
C : Type w
inst : Category.{v, w} C
X Y : Condensed.{u, v, w} C
f g : X ⟶ Y
h : ∀ (S : CompHausᵒᵖ), f.hom.app S = g.hom.app S
x : CompHausᵒᵖ
⊢ f.hom.app x = g.hom.app x

Tactic:
h _
-- Module: Mathlib.Condensed.Basic
Goal:
C : Type w
inst : Category.{v, w} C
X Y : Condensed.{u, v, w} C
f g : X ⟶ Y
h : ∀ (S : CompHausᵒᵖ), f.hom.app S = g.hom.app S
x : CompHausᵒᵖ
⊢ f.hom.app x = g.hom.app x

Tactic:
exact h _
-- Module: Mathlib.Condensed.Basic
Goal:
X Y : CondensedSet
f : X ⟶ Y
S T : CompHausᵒᵖ
g : S ⟶ T
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj S
⊢ Eq (α := (fun (X : Type (u + 1)) ↦ X) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj T))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app T) :
          (a : (fun (X : Type (u + 1)) ↦ X) (X.obj.obj T)) → (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj T))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map g) :
            (a : (fun (X : Type (u + 1)) ↦ X) (X.obj.obj S)) → (fun (X : Type (u + 1)) ↦ X) (X.obj.obj T))
          x) :
      (fun (X : Type (u + 1)) ↦ X) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj T))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map g) :
          (a : (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj S)) → (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj T))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app S) :
            (a : (fun (X : Type (u + 1)) ↦ X) (X.obj.obj S)) → (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj S))
          x) :
      (fun (X : Type (u + 1)) ↦ X) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj T))

Tactic:
simp
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
h :
  (S : Profinite.{u}) →
    IsColimit
      ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone S.asLimitCone.op)
e : CondensedSet ≌ Sheaf (coherentTopology Profinite) (Type (u + 1)) :=
  CategoryTheory.Equivalence.symm (Condensed.ProfiniteCompHaus.equivalence (Type (u + 1)))
i : (e.functor.obj X).obj (P := Presheaf.IsSheaf (coherentTopology Profinite)) ≅
  (e.functor.obj
        (LocallyConstant.functor.obj
          ((e.functor.obj X).obj (P := Presheaf.IsSheaf (coherentTopology Profinite)).obj
            (toProfinite.op.obj (Opposite.op (of PUnit.{u + 1})))))).obj
    (P := Presheaf.IsSheaf (coherentTopology Profinite)) :=
  Condensed.isoLocallyConstantOfIsColimit ((e.functor.obj X).obj (P := Presheaf.IsSheaf (coherentTopology Profinite))) h
⊢ LocallyConstant.functor.essImage X

Tactic:
⟨_, ⟨e.functor.preimageIso ((sheafToPresheaf _ _).preimageIso i.symm)⟩⟩

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Functor.preimageIso, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
h :
  (S : Profinite.{u}) →
    IsColimit
      ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone S.asLimitCone.op)
e : CondensedSet ≌ Sheaf (coherentTopology Profinite) (Type (u + 1)) :=
  CategoryTheory.Equivalence.symm (Condensed.ProfiniteCompHaus.equivalence (Type (u + 1)))
i : (e.functor.obj X).obj (P := Presheaf.IsSheaf (coherentTopology Profinite)) ≅
  (e.functor.obj
        (LocallyConstant.functor.obj
          ((e.functor.obj X).obj (P := Presheaf.IsSheaf (coherentTopology Profinite)).obj
            (toProfinite.op.obj (Opposite.op (of PUnit.{u + 1})))))).obj
    (P := Presheaf.IsSheaf (coherentTopology Profinite)) :=
  Condensed.isoLocallyConstantOfIsColimit ((e.functor.obj X).obj (P := Presheaf.IsSheaf (coherentTopology Profinite))) h
⊢ LocallyConstant.functor.essImage X

Tactic:
exact ⟨_, ⟨e.functor.preimageIso ((sheafToPresheaf _ _).preimageIso i.symm)⟩⟩
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
⊢ Condensed.IsDiscrete X

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
⊢ IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
    (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
⊢ Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)

Tactic:
1 ↔ 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
⊢ Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)

Tactic:
tfae_have 1 ↔ 2 := Sheaf.isConstant_iff_isIso_counit_app _ _ _

Premises used: CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
⊢ Condensed.IsDiscrete X

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
⊢ essImage (discrete (Type (u + 1))) X

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
⊢ Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X

Tactic:
1 ↔ 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
⊢ Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X

Tactic:
tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
⊢ Condensed.IsDiscrete X

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
⊢ LocallyConstant.functor.essImage X

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
⊢ Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X

Tactic:
1 ↔ 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
⊢ Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X

Tactic:
tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _ CompHaus.isTerminalPUnit adjunction _

Premises used: CondensedSet.LocallyConstant.adjunction, CategoryTheory.Sheaf.isConstant_iff_mem_essImage, CompHaus.isTerminalPUnit
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
⊢ Condensed.IsDiscrete X

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
⊢ IsIso (LocallyConstant.adjunction.counit.app X)

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false