awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
S : Finset Λ'
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
have H₁ : codeSupp' f.fix k ∪ contSupp k ⊆ S
Tactic: rw [contSupp] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
k : Cont'
H : contSupp k ⊆ S
⊢ Supports (contSupp k) S
have halt : ∀ (H : contSupp Cont'.halt ⊆ S), Supports (contSupp Cont'.halt) 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)⟩
Cleared hypotheses: k, H
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
S : Finset Λ'
k : Cont'
H : contSupp k ⊆ S
halt : ∀ (H : contSupp Cont'.halt ⊆ S), Supports (contSupp Cont'.halt) S
⊢ Supports (contSupp k) S
have 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
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)⟩
Cleared hypotheses: k, H
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ Supports (contSupp k) S
have cons₂ : ∀ (k : Cont') (IH : ∀ (H : contSupp k ⊆ S), Supports (contSupp k) S) (H : contSupp k.cons₂ ⊆ S),
  Supports (contSupp k.cons₂) 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)⟩
Cleared hypotheses: k, H
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ Supports (contSupp k) S
have 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
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)⟩
Cleared hypotheses: k, H
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ Supports (contSupp k) S
have 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
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)⟩
Cleared hypotheses: k, H
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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),
      essImage (discrete (Type (u + 1))) X, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite)
        (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X),
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))].TFAE
have 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)
Tactic: tfae_have 1 ↔ 2 := Sheaf.isConstant_iff_isIso_counit_app _ _ _
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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,
      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, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite)
        (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X),
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))].TFAE
have tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
Tactic: tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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,
      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, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite)
        (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X),
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))].TFAE
have tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
Tactic: tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _ CompHaus.isTerminalPUnit adjunction _
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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,
      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, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite)
        (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X),
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))].TFAE
have tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
Tactic: tfae_have 1 ↔ 5 :=
    have : functor.Faithful := inferInstance
    have : functor.Full := inferInstance
    -- These `have` statements above shouldn't be needed, but they are.
    Sheaf.isConstant_iff_isIso_counit_app' _ CompHaus.isTerminalPUnit adjunction _
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
⊢ [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, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite)
        (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X),
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))].TFAE
have tfae_1_iff_6 : Condensed.IsDiscrete X ↔
  Sheaf.IsConstant (coherentTopology Profinite)
    (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X)
Tactic: tfae_have 1 ↔ 6 :=
    (Sheaf.isConstant_iff_of_equivalence (coherentTopology Profinite)
      (coherentTopology CompHaus) profiniteToCompHaus Profinite.isTerminalPUnit
      CompHaus.isTerminalPUnit _).symm
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X)
⊢ [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, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite)
        (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X),
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))].TFAE
have tfae_7_to_4 : ∀
  (a :
    ∀ (S : Profinite.{u}),
      Nonempty.{u + 3}
        (IsColimit
          ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
            S.asLimitCone.op))),
  LocallyConstant.functor.essImage X
Tactic: tfae_have 7 → 4 := fun h ↦
    mem_locallyConstant_essImage_of_isColimit_mapCocone X (fun S ↦ (h S).some)
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X)
tfae_7_to_4 :
  ∀
    (a :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))),
    LocallyConstant.functor.essImage X
⊢ [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, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite)
        (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X),
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))].TFAE
have tfae_4_to_7 : ∀ (a : LocallyConstant.functor.essImage X) (S : Profinite.{u}),
  Nonempty.{u + 3}
    (IsColimit
      ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone S.asLimitCone.op))
Tactic: tfae_have 4 → 7 := fun ⟨Y, ⟨i⟩⟩ S ↦
    ⟨IsColimit.mapCoconeEquiv (isoWhiskerLeft profiniteToCompHaus.op
      ((sheafToPresheaf _ _).mapIso i))
      (Condensed.isColimitLocallyConstantPresheafDiagram Y S)⟩
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
⊢ [Condensed.IsDiscrete M,
      IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
        (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M),
      essImage (Condensed.discrete (ModuleCat R)) M, essImage (functor R) M,
      IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M),
      Sheaf.IsConstant (coherentTopology Profinite)
        (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M),
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))].TFAE
have tfae_1_iff_2 : Condensed.IsDiscrete M ↔
  IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
    (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
Tactic: tfae_have 1 ↔ 2 := Sheaf.isConstant_iff_isIso_counit_app _ _ _
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
⊢ [Condensed.IsDiscrete M,
      IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
        (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M),
      essImage (Condensed.discrete (ModuleCat R)) M, essImage (functor R) M,
      IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M),
      Sheaf.IsConstant (coherentTopology Profinite)
        (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M),
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))].TFAE
have tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
Tactic: tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
⊢ [Condensed.IsDiscrete M,
      IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
        (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M),
      essImage (Condensed.discrete (ModuleCat R)) M, essImage (functor R) M,
      IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M),
      Sheaf.IsConstant (coherentTopology Profinite)
        (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M),
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))].TFAE
have tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
Tactic: tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _ CompHaus.isTerminalPUnit (adjunction R) _
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
⊢ [Condensed.IsDiscrete M,
      IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
        (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M),
      essImage (Condensed.discrete (ModuleCat R)) M, essImage (functor R) M,
      IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M),
      Sheaf.IsConstant (coherentTopology Profinite)
        (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M),
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))].TFAE
have tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
Tactic: tfae_have 1 ↔ 5 :=
    have : (functor R).Faithful := inferInstance
    have : (functor R).Full := inferInstance
    -- These `have` statements above shouldn't be needed, but they are.
    Sheaf.isConstant_iff_isIso_counit_app' _ CompHaus.isTerminalPUnit (adjunction R) _