awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
h :
  (¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x) ↔
    ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
⊢ x ∈ (fibres π σ)ᶜ ↔
    Membership.mem (γ := Set T) (⋃ (i : X), (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)}) x

Tactic:
simp only [Set.mem_compl_iff, mem_fibres_iff, not_or, not_exists, Set.mem_iUnion,
    Set.mem_inter_iff, Set.mem_range, Set.mem_preimage, Function.comp_apply,
    Set.mem_singleton_iff]

Premises used: Set.mem_range, Set.mem_inter_iff, Set.mem_iUnion, not_exists, not_or, Set.mem_singleton_iff, _private.0.InternalProjectivityProof.mem_fibres_iff, Function.comp_apply, Set.mem_compl_iff, Set.mem_preimage
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
⊢ (¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x) ↔
    ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)

Tactic:
⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun ⟨n, hn, hn'⟩ ↦ ?_⟩

Premises used: OnePoint.some, Exists, _private.0.InternalProjectivityProof.fibres_compl_eq_iUnion.match_9, Option.none, And, _private.0.InternalProjectivityProof.fibres_compl_eq_iUnion.match_8, Iff.intro, Eq, Prod.snd, Not
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
h :
  (¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x) →
    ∀ (h₁ : ¬(π x).2 = none) (h₂ : ∀ (x_2 : X) (x_3 : S), ¬σ (Option.some x_2) x_3 = x),
      ∃ (i : X), (∀ (x_2 : S), ¬σ (Option.some i) x_2 = x) ∧ (π x).2 = (↑i : OnePoint X)
h₁ :
  (∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)) →
    ∀ (n : X) (hn : ∀ (x_2 : S), ¬σ (Option.some n) x_2 = x) (hn' : (π x).2 = (↑n : OnePoint X)),
      ¬(π x).2 = none ∧ ∀ (x_2 : X) (x_3 : S), ¬σ (Option.some x_2) x_3 = x
⊢ (¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x) ↔
    ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun ⟨n, hn, hn'⟩ ↦ ?_⟩
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
h_1 : ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
h₁ : ¬(π x).2 = none
h₂ : ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
h :
  ∀ (n : X) (hn : (π x).2 = Option.some n),
    ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
⊢ ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)

Tactic:
obtain ⟨n, hn⟩ := Option.ne_none_iff_exists'.mp h₁

Premises used: Option.ne_none_iff_exists', Iff.mp
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
h : ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
h₁ : ¬(π x).2 = none
h₂ : ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
n : X
hn : (π x).2 = Option.some n
⊢ ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)

Tactic:
⟨n, h₂ n, hn⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
h : ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
h₁ : ¬(π x).2 = none
h₂ : ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
n : X
hn : (π x).2 = Option.some n
⊢ ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)

Tactic:
exact ⟨n, h₂ n, hn⟩
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
h : ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
hn' : (π x).2 = (↑n : OnePoint X)
⊢ ¬(π x).2 = none

Tactic:
simpa [hn'] using Option.isSome_iff_ne_none.mp rfl

Premises used: Iff.mp, Option.isSome_iff_ne_none
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
h_1 : ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
hn' : (π x).2 = (↑n : OnePoint X)
h : ∀ (i : X) (s : S) (h : σ (Option.some i) s = x), σ (Option.some n) s = x
⊢ ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x

Tactic:
refine ⟨by simpa [hn'] using Option.isSome_iff_ne_none.mp rfl, fun i s h ↦ hn s ?_⟩
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
h_1 : ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
hn' : (π x).2 = (↑n : OnePoint X)
i : X
s : S
h : σ (Option.some i) s = x
⊢ Option.some i = (↑n : OnePoint X)

Tactic:
rw [← h, hσ'] at hn'
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
h_1 : ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
hn' : (π x).2 = (↑n : OnePoint X)
i : X
s : S
h : σ (Option.some i) s = x
hn'₁ : Option.some i = (↑n : OnePoint X)
⊢ σ (Option.some i) s = x

Tactic:
rw [← h, hσ'] at hn'
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
h_1 : ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
i : X
s : S
hn' : Option.some i = (↑n : OnePoint X)
h : σ (Option.some i) s = x
h₁ : σ (Option.some n) s = σ (Option.some i) s
h₂ h₃ : σ (Option.some i) s = σ (Option.some i) s
⊢ σ (Option.some n) s = x

Tactic:
rw [← h, Option.some_injective _ hn'.symm]

Premises used: Option.some_injective, Eq.symm
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : TopologicalSpace T
inst_2 : TopologicalSpace X
inst_3 : DiscreteTopology X
inst_4 : T2Space T
inst_5 : CompactSpace S
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
rw : IsOpen.{u_2} (X := T) (⋃ (i : X), (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)})
⊢ IsOpen (fibres π σ)ᶜ

Tactic:
rw [fibres_compl_eq_iUnion π σ hσ']

Premises used: _private.0.InternalProjectivityProof.fibres_compl_eq_iUnion
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : TopologicalSpace T
inst_2 : TopologicalSpace X
inst_3 : DiscreteTopology X
inst_4 : T2Space T
inst_5 : CompactSpace S
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
⊢ IsOpen.{u_2} (X := T) (⋃ (i : X), (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)})

Tactic:
isOpen_iUnion fun i ↦ IsOpen.inter ?_ ?_

Premises used: isOpen_iUnion, IsOpen.inter
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : TopologicalSpace T
inst_2 : TopologicalSpace X
inst_3 : DiscreteTopology X
inst_4 : T2Space T
inst_5 : CompactSpace S
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
refine_1 : ∀ (i : X), IsOpen (Set.range (σ (Option.some i)))ᶜ
refine_2 : ∀ (i : X), IsOpen (Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)})
⊢ IsOpen.{u_2} (X := T) (⋃ (i : X), (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)})

Tactic:
refine isOpen_iUnion fun i ↦ IsOpen.inter ?_ ?_

Premises used: isOpen_iUnion, IsOpen.inter
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : TopologicalSpace T
inst_2 : TopologicalSpace X
inst_3 : DiscreteTopology X
inst_4 : T2Space T
inst_5 : CompactSpace S
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
⊢ IsOpen (Set.range (σ (Option.some i)))ᶜ

Tactic:
simpa using IsCompact.isClosed (isCompact_range (hσ i))

Premises used: Option.some, isCompact_range, IsCompact.isClosed
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : TopologicalSpace T
inst_2 : TopologicalSpace X
inst_3 : DiscreteTopology X
inst_4 : T2Space T
inst_5 : CompactSpace S
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
h : Membership.mem (γ := Set (OnePoint X)) {(↑i : OnePoint X)} ∞
⊢ IsCompact (X := X) (OnePoint.some ⁻¹' {(↑i : OnePoint X)})ᶜ

Tactic:
simp_all
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : TopologicalSpace T
inst_2 : TopologicalSpace X
inst_3 : DiscreteTopology X
inst_4 : T2Space T
inst_5 : CompactSpace S
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
⊢ IsOpen (X := X) (OnePoint.some ⁻¹' {(↑i : OnePoint X)})

Tactic:
simp
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : TopologicalSpace T
inst_2 : TopologicalSpace X
inst_3 : DiscreteTopology X
inst_4 : T2Space T
inst_5 : CompactSpace S
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
⊢ IsOpen (Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)})

Tactic:
exact .preimage (continuous_snd.comp hπ) ⟨fun h ↦ by simp_all, by simp⟩
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
x : (↑(fibres π σ) : Type u_2)
⊢ π_r π σ x = π (↑x : T)

Tactic:
rfl

Premises used: _private.0.InternalProjectivityProof.π_r, rfl
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
x : (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2)
⊢ fibreIncl π σ x = (↑x : (↑(fibres π σ) : Type u_2))

Tactic:
rfl

Premises used: _private.0.InternalProjectivityProof.fibreIncl, rfl
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
none :
  ∀ (y : T) (hy : π y = (s, Option.none)),
    ∃ (a : (↑(fibres π σ) : Type u_2)),
      Eq (α := Prod.{u_1, u_3} S (Option X)) ((fun (x : (↑(fibres π σ) : Type u_2)) ↦ π (↑x : T)) a) (s, Option.none)
⊢ ∃ (a : (↑(fibres π σ) : Type u_2)),
    Eq (α := Prod.{u_1, u_3} S (Option X)) ((fun (x : (↑(fibres π σ) : Type u_2)) ↦ π (↑x : T)) a) (s, Option.none)

Tactic:
obtain ⟨y, hy⟩ := hπ (s, none)

Premises used: Prod.mk, Option.none
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
y : T
hy : π y = (s, none)
⊢ y ∈ fibres π σ

Tactic:
grind
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
y : T
hy : π y = (s, none)
⊢ ∃ (a : (↑(fibres π σ) : Type u_2)),
    Eq (α := Prod.{u_1, u_3} S (Option X)) ((fun (x : (↑(fibres π σ) : Type u_2)) ↦ π (↑x : T)) a) (s, none)

Tactic:
exact ⟨⟨y, by grind⟩, hy⟩
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
x : X
⊢ σ (Option.some x) s ∈ fibres π σ

Tactic:
simp
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
x : X
⊢ ((fun (x : (↑(fibres π σ) : Type u_2)) ↦ π (↑x : T))
        (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) (σ (Option.some x) s) ⋯)).1 =
    (s, Option.some x).1

Tactic:
grind
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
x : X
⊢ ((fun (x : (↑(fibres π σ) : Type u_2)) ↦ π (↑x : T))
        (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) (σ (Option.some x) s) ⋯)).2 =
    (s, Option.some x).2

Tactic:
grind
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
x : X
⊢ ∃ (a : (↑(fibres π σ) : Type u_2)), (fun (x : (↑(fibres π σ) : Type u_2)) ↦ π (↑x : T)) a = (s, Option.some x)

Tactic:
exact ⟨⟨σ x s, by simp⟩, Prod.ext (by grind) (by grind)⟩
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_4
T : Type u_5
X : Type u_6
Y : Type u_7
i : Y → T
π : T → Prod.{u_4, u_6} S (Option X)
t : Sum.{u_5, u_7} T { xy : Y × Y // π (i xy.1) = π (i xy.2) }
⊢ coverToFun i π t =
    Sum.elim (fun (t : T) ↦ Subtype.mk (p := fun (xy : T × T) ↦ π xy.1 = π xy.2) (t, t) ⋯)
      (fun (xy : { xy : Y × Y // π (i xy.1) = π (i xy.2) }) ↦
        Subtype.mk (p := fun (xy : T × T) ↦ π xy.1 = π xy.2) (i (↑xy : Y × Y).1, i (↑xy : Y × Y).2) ⋯)
      t

Tactic:
rfl

Premises used: _private.0.InternalProjectivityProof.coverToFun, rfl
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property :
  π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').1 =
    π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').2
pos :
  ∀ (h : (π t).2 = none),
    ∃ (a :
      (↑(fibres π σ) : Type u_2) ⊕
        { xy : (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) × (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) //
          π_r π σ (fibreIncl π σ xy.1) = π_r π σ (fibreIncl π σ xy.2) }),
      coverToFun (fibreIncl π σ) (π_r π σ) a =
        Subtype.mk (p := fun (xy : (↑(fibres π σ) : Type u_2) × (↑(fibres π σ) : Type u_2)) ↦
          π_r π σ xy.1 = π_r π σ xy.2)
          (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht')
          property
neg :
  ∀ (h : ¬(π t).2 = none),
    ∃ (a :
      (↑(fibres π σ) : Type u_2) ⊕
        { xy : (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) × (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) //
          π_r π σ (fibreIncl π σ xy.1) = π_r π σ (fibreIncl π σ xy.2) }),
      coverToFun (fibreIncl π σ) (π_r π σ) a =
        Subtype.mk (p := fun (xy : (↑(fibres π σ) : Type u_2) × (↑(fibres π σ) : Type u_2)) ↦
          π_r π σ xy.1 = π_r π σ xy.2)
          (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht')
          property
⊢ ∃ (a :
    (↑(fibres π σ) : Type u_2) ⊕
      { xy : (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) × (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) //
        π_r π σ (fibreIncl π σ xy.1) = π_r π σ (fibreIncl π σ xy.2) }),
    coverToFun (fibreIncl π σ) (π_r π σ) a =
      Subtype.mk (p := fun (xy : (↑(fibres π σ) : Type u_2) × (↑(fibres π σ) : Type u_2)) ↦ π_r π σ xy.1 = π_r π σ xy.2)
        (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht')
        property

Tactic:
by_cases h : (π t).2 = none

Premises used: Option.none, Prod.snd
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property :
  π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').1 =
    π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').2
h : (π t).2 = none
⊢ Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht ∈ Prod.snd ∘ π_r π σ ⁻¹' {none}

Tactic:
grind
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property :
  π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').1 =
    π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').2
h : (π t).2 = none
⊢ Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht' ∈ Prod.snd ∘ π_r π σ ⁻¹' {none}

Tactic:
grind
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property :
  π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').1 =
    π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').2
h : (π t).2 = none
⊢ π_r π σ
      (fibreIncl π σ
        (Subtype.mk (p := fun (x : (↑(fibres π σ) : Type u_2)) ↦ x ∈ Prod.snd ∘ π_r π σ ⁻¹' {none})
              (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht) ⋯,
            Subtype.mk (p := fun (x : (↑(fibres π σ) : Type u_2)) ↦ x ∈ Prod.snd ∘ π_r π σ ⁻¹' {none})
              (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht') ⋯).1) =
    π_r π σ
      (fibreIncl π σ
        (Subtype.mk (p := fun (x : (↑(fibres π σ) : Type u_2)) ↦ x ∈ Prod.snd ∘ π_r π σ ⁻¹' {none})
              (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht) ⋯,
            Subtype.mk (p := fun (x : (↑(fibres π σ) : Type u_2)) ↦ x ∈ Prod.snd ∘ π_r π σ ⁻¹' {none})
              (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht') ⋯).2)

Tactic:
grind
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property :
  π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').1 =
    π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').2
h : (π t).2 = none
⊢ coverToFun (fibreIncl π σ) (π_r π σ)
      (Sum.inr
        (Subtype.mk (p :=
          fun (xy : (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) × (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2)) ↦
          π_r π σ (fibreIncl π σ xy.1) = π_r π σ (fibreIncl π σ xy.2))
          (Subtype.mk (p := fun (x : (↑(fibres π σ) : Type u_2)) ↦ x ∈ Prod.snd ∘ π_r π σ ⁻¹' {none})
              (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht) ⋯,
            Subtype.mk (p := fun (x : (↑(fibres π σ) : Type u_2)) ↦ x ∈ Prod.snd ∘ π_r π σ ⁻¹' {none})
              (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht') ⋯)
          ⋯)) =
    Subtype.mk (p := fun (xy : (↑(fibres π σ) : Type u_2) × (↑(fibres π σ) : Type u_2)) ↦ π_r π σ xy.1 = π_r π σ xy.2)
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht')
      property

Tactic:
grind
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property :
  π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').1 =
    π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').2
h : (π t).2 = none
⊢ ∃ (a :
    (↑(fibres π σ) : Type u_2) ⊕
      { xy : (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) × (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) //
        π_r π σ (fibreIncl π σ xy.1) = π_r π σ (fibreIncl π σ xy.2) }),
    coverToFun (fibreIncl π σ) (π_r π σ) a =
      Subtype.mk (p := fun (xy : (↑(fibres π σ) : Type u_2) × (↑(fibres π σ) : Type u_2)) ↦ π_r π σ xy.1 = π_r π σ xy.2)
        (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht')
        property

Tactic:
exact ⟨Sum.inr ⟨(⟨⟨t, ht⟩, by grind⟩, ⟨⟨t', ht'⟩, by grind⟩), by grind⟩, by grind⟩