[GOAL]
α : Type u_1
inst✝ : Primcodable α
p : α → Prop
⊢ ∀ (a : α), p a ↔ p (id a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ r ((g ∘ f) a)
[PROOFSTEP]
erw [← h₂, ← h₁]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ p a
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : r ((g ∘ f) a)
⊢ p a
[PROOFSTEP]
rwa [h₁, h₂]
[GOAL]
α : Type u_1
inst✝ : Primcodable α
p : α → Prop
⊢ ∀ (a : α), p a ↔ p (id a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ r ((g ∘ f) a)
[PROOFSTEP]
erw [← h₂, ← h₁]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ p a
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : r ((g ∘ f) a)
⊢ p a
[PROOFSTEP]
rwa [h₁, h₂]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ↑e.symm
⊢ q ≤₁ (q ∘ ↑e)
[PROOFSTEP]
convert OneOneReducible.of_equiv _ h
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ↑e.symm
⊢ q = (q ∘ ↑e) ∘ ↑e.symm
[PROOFSTEP]
funext
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ↑e.symm
x✝ : β
⊢ q x✝ = ((q ∘ ↑e) ∘ ↑e.symm) x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
q : β → Prop
h₁ : p ≤₀ q
h₂ : ComputablePred q
⊢ ComputablePred p
[PROOFSTEP]
rcases h₁ with ⟨f, c, hf⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred p
[PROOFSTEP]
rw [show p = fun a => q (f a) from Set.ext hf]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred fun a => q (f a)
[PROOFSTEP]
rcases computable_iff.1 h₂ with ⟨g, hg, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a => g a = true
hf : ∀ (a : α), p a ↔ (fun a => g a = true) (f a)
⊢ ComputablePred fun a => (fun a => g a = true) (f a)
[PROOFSTEP]
exact ⟨by infer_instance, by simpa using hg.comp c⟩
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a => g a = true
hf : ∀ (a : α), p a ↔ (fun a => g a = true) (f a)
⊢ DecidablePred fun a => (fun a => g a = true) (f a)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a => g a = true
hf : ∀ (a : α), p a ↔ (fun a => g a = true) (f a)
⊢ Computable fun a => decide ((fun a => (fun a => g a = true) (f a)) a)
[PROOFSTEP]
simpa using hg.comp c
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → γ
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ r (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
x : α ⊕ β
⊢ (p ⊕' q) x ↔ r ((f ⊕' g) x)
[PROOFSTEP]
cases x <;> [apply h₁; apply h₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → γ
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ r (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
x : α ⊕ β
⊢ (p ⊕' q) x ↔ r ((f ⊕' g) x)
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → γ
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ r (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
val✝ : α
⊢ (p ⊕' q) (Sum.inl val✝) ↔ r ((f ⊕' g) (Sum.inl val✝))
[PROOFSTEP]
apply h₁
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → γ
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ r (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
val✝ : β
⊢ (p ⊕' q) (Sum.inr val✝) ↔ r ((f ⊕' g) (Sum.inr val✝))
[PROOFSTEP]
apply h₂
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p : Set α
⊢ ∀ (a : α), p a ↔ toNat p (Encodable.encode a)
[PROOFSTEP]
simp [toNat, setOf]
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p : Set α
⊢ ManyOneEquiv (toNat p) p
[PROOFSTEP]
simp [ManyOneEquiv]
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p : Set α
q : Set β
⊢ ManyOneEquiv (toNat p) (toNat q) ↔ ManyOneEquiv p q
[PROOFSTEP]
simp [ManyOneEquiv]
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
φ : Sort ?u.72115
d₁ d₂ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p : Set ℕ
q₁ q₂ : ℕ → Prop
hq : ManyOneEquiv q₁ q₂
⊢ ManyOneEquiv p p
[PROOFSTEP]
rfl
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
φ : Sort ?u.72115
d₁ d₂ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
⊢ ∀ (p q : ℕ → Prop),
    ManyOneEquiv p q →
      (fun p => ManyOneDegree.liftOn d₂ (f p) (_ : ∀ (q₁ q₂ : ℕ → Prop), ManyOneEquiv q₁ q₂ → f p q₁ = f p q₂)) p =
        (fun p => ManyOneDegree.liftOn d₂ (f p) (_ : ∀ (q₁ q₂ : ℕ → Prop), ManyOneEquiv q₁ q₂ → f p q₁ = f p q₂)) q
[PROOFSTEP]
intro p₁ p₂ hp
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
φ : Sort ?u.72115
d₁ d₂ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
⊢ (fun p => ManyOneDegree.liftOn d₂ (f p) (_ : ∀ (q₁ q₂ : ℕ → Prop), ManyOneEquiv q₁ q₂ → f p q₁ = f p q₂)) p₁ =
    (fun p => ManyOneDegree.liftOn d₂ (f p) (_ : ∀ (q₁ q₂ : ℕ → Prop), ManyOneEquiv q₁ q₂ → f p q₁ = f p q₂)) p₂
[PROOFSTEP]
induction d₂ using ManyOneDegree.ind_on
[GOAL]
case h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
φ : Sort ?u.72115
d₁ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
p✝ : Set ℕ
⊢ (fun p => ManyOneDegree.liftOn (of p✝) (f p) (_ : ∀ (q₁ q₂ : ℕ → Prop), ManyOneEquiv q₁ q₂ → f p q₁ = f p q₂)) p₁ =
    (fun p => ManyOneDegree.liftOn (of p✝) (f p) (_ : ∀ (q₁ q₂ : ℕ → Prop), ManyOneEquiv q₁ q₂ → f p q₁ = f p q₂)) p₂
[PROOFSTEP]
apply h
[GOAL]
case h.a
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
φ : Sort ?u.72115
d₁ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
p✝ : Set ℕ
⊢ ManyOneEquiv p₁ p₂
case h.a
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
φ : Sort ?u.72115
d₁ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
p✝ : Set ℕ
⊢ ManyOneEquiv (toNat p✝) (toNat p✝)
[PROOFSTEP]
assumption
[GOAL]
case h.a
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
φ : Sort ?u.72115
d₁ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
p✝ : Set ℕ
⊢ ManyOneEquiv (toNat p✝) (toNat p✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p : α → Prop
q : β → Prop
⊢ of p = of q ↔ ManyOneEquiv p q
[PROOFSTEP]
rw [of, of, Quotient.eq'']
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p : α → Prop
q : β → Prop
⊢ Setoid.r (toNat p) (toNat q) ↔ ManyOneEquiv p q
[PROOFSTEP]
unfold Setoid.r
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p : α → Prop
q : β → Prop
⊢ { r := ManyOneEquiv, iseqv := proof_1 }.1 (toNat p) (toNat q) ↔ ManyOneEquiv p q
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d : ManyOneDegree
⊢ d ≤ d
[PROOFSTEP]
induction d using ManyOneDegree.ind_on
[GOAL]
case h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p✝ : Set ℕ
⊢ of p✝ ≤ of p✝
[PROOFSTEP]
simp
[GOAL]
case h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p✝ : Set ℕ
⊢ p✝ ≤₀ p✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₁ d₂ : ManyOneDegree
⊢ d₁ ≤ d₂ → d₂ ≤ d₁ → d₁ = d₂
[PROOFSTEP]
induction d₁ using ManyOneDegree.ind_on
[GOAL]
case h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₂ : ManyOneDegree
p✝ : Set ℕ
⊢ of p✝ ≤ d₂ → d₂ ≤ of p✝ → of p✝ = d₂
[PROOFSTEP]
induction d₂ using ManyOneDegree.ind_on
[GOAL]
case h.h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p✝¹ p✝ : Set ℕ
⊢ of p✝¹ ≤ of p✝ → of p✝ ≤ of p✝¹ → of p✝¹ = of p✝
[PROOFSTEP]
intro hp hq
[GOAL]
case h.h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p✝¹ p✝ : Set ℕ
hp : of p✝¹ ≤ of p✝
hq : of p✝ ≤ of p✝¹
⊢ of p✝¹ = of p✝
[PROOFSTEP]
simp_all only [ManyOneEquiv, of_le_of, of_eq_of, true_and_iff]
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₁ d₂ d₃ : ManyOneDegree
⊢ d₁ ≤ d₂ → d₂ ≤ d₃ → d₁ ≤ d₃
[PROOFSTEP]
induction d₁ using ManyOneDegree.ind_on
[GOAL]
case h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₂ d₃ : ManyOneDegree
p✝ : Set ℕ
⊢ of p✝ ≤ d₂ → d₂ ≤ d₃ → of p✝ ≤ d₃
[PROOFSTEP]
induction d₂ using ManyOneDegree.ind_on
[GOAL]
case h.h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₃ : ManyOneDegree
p✝¹ p✝ : Set ℕ
⊢ of p✝¹ ≤ of p✝ → of p✝ ≤ d₃ → of p✝¹ ≤ d₃
[PROOFSTEP]
induction d₃ using ManyOneDegree.ind_on
[GOAL]
case h.h.h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p✝² p✝¹ p✝ : Set ℕ
⊢ of p✝² ≤ of p✝¹ → of p✝¹ ≤ of p✝ → of p✝² ≤ of p✝
[PROOFSTEP]
apply ManyOneReducible.trans
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₁ d₂ : ManyOneDegree
⊢ ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop),
    ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → (fun a b => of (a ⊕' b)) p₁ q₁ = (fun a b => of (a ⊕' b)) p₂ q₂
[PROOFSTEP]
rintro a b c d ⟨hl₁, hr₁⟩ ⟨hl₂, hr₂⟩
[GOAL]
case intro.intro
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₁ d₂ : ManyOneDegree
a b c d : ℕ → Prop
hl₁ : a ≤₀ b
hr₁ : b ≤₀ a
hl₂ : c ≤₀ d
hr₂ : d ≤₀ c
⊢ (fun a b => of (a ⊕' b)) a c = (fun a b => of (a ⊕' b)) b d
[PROOFSTEP]
rw [of_eq_of]
[GOAL]
case intro.intro
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₁ d₂ : ManyOneDegree
a b c d : ℕ → Prop
hl₁ : a ≤₀ b
hr₁ : b ≤₀ a
hl₂ : c ≤₀ d
hr₂ : d ≤₀ c
⊢ ManyOneEquiv (a ⊕' c) (b ⊕' d)
[PROOFSTEP]
exact
  ⟨disjoin_manyOneReducible (hl₁.trans OneOneReducible.disjoin_left.to_many_one)
      (hl₂.trans OneOneReducible.disjoin_right.to_many_one),
    disjoin_manyOneReducible (hr₁.trans OneOneReducible.disjoin_left.to_many_one)
      (hr₂.trans OneOneReducible.disjoin_right.to_many_one)⟩
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₁ d₂ d₃ : ManyOneDegree
⊢ d₁ + d₂ ≤ d₃ ↔ d₁ ≤ d₃ ∧ d₂ ≤ d₃
[PROOFSTEP]
induction d₁ using ManyOneDegree.ind_on
[GOAL]
case h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₂ d₃ : ManyOneDegree
p✝ : Set ℕ
⊢ of p✝ + d₂ ≤ d₃ ↔ of p✝ ≤ d₃ ∧ d₂ ≤ d₃
[PROOFSTEP]
induction d₂ using ManyOneDegree.ind_on
[GOAL]
case h.h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₃ : ManyOneDegree
p✝¹ p✝ : Set ℕ
⊢ of p✝¹ + of p✝ ≤ d₃ ↔ of p✝¹ ≤ d₃ ∧ of p✝ ≤ d₃
[PROOFSTEP]
induction d₃ using ManyOneDegree.ind_on
[GOAL]
case h.h.h
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p✝² p✝¹ p✝ : Set ℕ
⊢ of p✝² + of p✝¹ ≤ of p✝ ↔ of p✝² ≤ of p✝ ∧ of p✝¹ ≤ of p✝
[PROOFSTEP]
simpa only [← add_of, of_le_of] using disjoin_le
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₁ d₂ : ManyOneDegree
⊢ d₁ + ?m.117648 d₁ d₂ ≤ d₁ + d₂
[PROOFSTEP]
rfl
[GOAL]
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
d₁ d₂ : ManyOneDegree
⊢ ?m.117829 d₁ d₂ + d₂ ≤ d₁ + d₂
[PROOFSTEP]
rfl


[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous reflTransSymmAux
[PROOFSTEP]
refine' continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _
[GOAL]
case refine'_1
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x.snd
[PROOFSTEP]
continuity
[GOAL]
case refine'_2
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 1 / 2
[PROOFSTEP]
continuity
[GOAL]
case refine'_3
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x.fst * 2 * ↑x.snd
[PROOFSTEP]
continuity
[GOAL]
case refine'_4
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x.fst * (2 - 2 * ↑x.snd)
[PROOFSTEP]
continuity
[GOAL]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I × ↑I), ↑x.snd = 1 / 2 → ↑x.fst * 2 * ↑x.snd = ↑x.fst * (2 - 2 * ↑x.snd)
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
hx : ↑x.snd = 1 / 2
⊢ ↑x.fst * 2 * ↑x.snd = ↑x.fst * (2 - 2 * ↑x.snd)
[PROOFSTEP]
rw [hx, mul_assoc]
[GOAL]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
hx : ↑x.snd = 1 / 2
⊢ ↑x.fst * (2 * (1 / 2)) = ↑x.fst * (2 - 2 * (1 / 2))
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
⊢ reflTransSymmAux x ∈ I
[PROOFSTEP]
dsimp only [reflTransSymmAux]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
⊢ (if ↑x.snd ≤ 1 / 2 then ↑x.fst * 2 * ↑x.snd else ↑x.fst * (2 - 2 * ↑x.snd)) ∈ I
[PROOFSTEP]
split_ifs
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst * 2 * ↑x.snd ∈ I
[PROOFSTEP]
constructor
[GOAL]
case pos.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst * 2 * ↑x.snd
[PROOFSTEP]
apply mul_nonneg
[GOAL]
case pos.left.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst * 2
[PROOFSTEP]
apply mul_nonneg
[GOAL]
case pos.left.ha.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst
[PROOFSTEP]
unit_interval
[GOAL]
case pos.left.ha.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
case pos.left.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.snd
[PROOFSTEP]
unit_interval
[GOAL]
case pos.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst * 2 * ↑x.snd ≤ 1
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case pos.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst * (2 * ↑x.snd) ≤ 1
[PROOFSTEP]
apply mul_le_one
[GOAL]
case pos.right.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst ≤ 1
[PROOFSTEP]
unit_interval
[GOAL]
case pos.right.hb'
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2 * ↑x.snd
[PROOFSTEP]
apply mul_nonneg
[GOAL]
case pos.right.hb'.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
case pos.right.hb'.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.snd
[PROOFSTEP]
unit_interval
[GOAL]
case pos.right.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 2 * ↑x.snd ≤ 1
[PROOFSTEP]
linarith
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ ↑x.fst * (2 - 2 * ↑x.snd) ∈ I
[PROOFSTEP]
constructor
[GOAL]
case neg.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst * (2 - 2 * ↑x.snd)
[PROOFSTEP]
apply mul_nonneg
[GOAL]
case neg.left.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst
[PROOFSTEP]
unit_interval
[GOAL]
case neg.left.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.snd
[PROOFSTEP]
linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]
[GOAL]
case neg.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ ↑x.fst * (2 - 2 * ↑x.snd) ≤ 1
[PROOFSTEP]
apply mul_le_one
[GOAL]
case neg.right.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ ↑x.fst ≤ 1
[PROOFSTEP]
unit_interval
[GOAL]
case neg.right.hb'
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.snd
[PROOFSTEP]
linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]
[GOAL]
case neg.right.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 2 - 2 * ↑x.snd ≤ 1
[PROOFSTEP]
linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Continuous fun x => ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) }
[PROOFSTEP]
continuity
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ ∀ (x : ↑I),
    ContinuousMap.toFun
        (ContinuousMap.mk fun x => ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) }) (0, x) =
      ↑(Path.refl x₀).toContinuousMap x
[PROOFSTEP]
simp [reflTransSymmAux]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
⊢ ContinuousMap.toFun
      (ContinuousMap.mk fun x => ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) }) (1, x) =
    ↑(Path.trans p (Path.symm p)).toContinuousMap x
[PROOFSTEP]
dsimp only [reflTransSymmAux, Path.coe_toContinuousMap, Path.trans]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
⊢ ↑p { val := if ↑x ≤ 1 / 2 then ↑1 * 2 * ↑x else ↑1 * (2 - 2 * ↑x), property := (_ : reflTransSymmAux (1, x) ∈ I) } =
    ↑(ContinuousMap.mk
          ((fun t => if t ≤ 1 / 2 then extend p (2 * t) else extend (Path.symm p) (2 * t - 1)) ∘ Subtype.val))
      x
[PROOFSTEP]
change _ = ite _ _ _
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
⊢ ↑p { val := if ↑x ≤ 1 / 2 then ↑1 * 2 * ↑x else ↑1 * (2 - 2 * ↑x), property := (_ : reflTransSymmAux (1, x) ∈ I) } =
    if ↑x ≤ 1 / 2 then extend p (2 * ↑x) else extend (Path.symm p) (2 * ↑x - 1)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ↑x ≤ 1 / 2
⊢ ↑p { val := ↑1 * 2 * ↑x, property := (_ : (fun x => x ∈ I) (↑1 * 2 * ↑x)) } = extend p (2 * ↑x)
[PROOFSTEP]
rw [Path.extend, Set.IccExtend_of_mem]
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ↑x ≤ 1 / 2
⊢ ↑p { val := ↑1 * 2 * ↑x, property := (_ : (fun x => x ∈ I) (↑1 * 2 * ↑x)) } =
    ↑p { val := 2 * ↑x, property := ?pos.hx✝ }
[PROOFSTEP]
norm_num
[GOAL]
case pos.hx
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ↑x ≤ 1 / 2
⊢ 2 * ↑x ∈ Set.Icc 0 1
[PROOFSTEP]
rw [unitInterval.mul_pos_mem_iff zero_lt_two]
[GOAL]
case pos.hx
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ↑x ≤ 1 / 2
⊢ ↑x ∈ Set.Icc 0 (1 / 2)
[PROOFSTEP]
exact ⟨unitInterval.nonneg x, h⟩
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ ↑p { val := ↑1 * (2 - 2 * ↑x), property := (_ : (fun x => x ∈ I) (↑1 * (2 - 2 * ↑x))) } =
    extend (Path.symm p) (2 * ↑x - 1)
[PROOFSTEP]
rw [Path.symm, Path.extend, Set.IccExtend_of_mem]
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ ↑p { val := ↑1 * (2 - 2 * ↑x), property := (_ : (fun x => x ∈ I) (↑1 * (2 - 2 * ↑x))) } =
    ↑{ toContinuousMap := ContinuousMap.mk (↑p ∘ σ),
          source' := (_ : ContinuousMap.toFun (ContinuousMap.mk (↑p ∘ σ)) 0 = x₁),
          target' := (_ : ContinuousMap.toFun (ContinuousMap.mk (↑p ∘ σ)) 1 = x₀) }
      { val := 2 * ↑x - 1, property := ?neg.hx✝ }
[PROOFSTEP]
simp only [Set.Icc.coe_one, one_mul, coe_mk_mk, Function.comp_apply]
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ ↑p { val := 2 - 2 * ↑x, property := (_ : (fun x => x ∈ I) (2 - 2 * ↑x)) } =
    ↑p (σ { val := 2 * ↑x - 1, property := ?neg.hx✝ })
[PROOFSTEP]
congr 1
[GOAL]
case neg.h.e_6.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ { val := 2 - 2 * ↑x, property := (_ : (fun x => x ∈ I) (2 - 2 * ↑x)) } = σ { val := 2 * ↑x - 1, property := ?neg.hx✝ }
[PROOFSTEP]
ext
  -- Porting note: norm_num ignores arguments.
[GOAL]
case neg.h.e_6.h.a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ ↑{ val := 2 - 2 * ↑x, property := (_ : (fun x => x ∈ I) (2 - 2 * ↑x)) } =
    ↑(σ { val := 2 * ↑x - 1, property := ?neg.hx✝ })
[PROOFSTEP]
simp [sub_sub_eq_add_sub]
[GOAL]
case neg.h.e_6.h.a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ 2 = 1 + 1
[PROOFSTEP]
norm_num
[GOAL]
case neg.hx
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ 2 * ↑x - 1 ∈ Set.Icc 0 1
[PROOFSTEP]
rw [unitInterval.two_mul_sub_one_mem_iff]
[GOAL]
case neg.hx
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ ↑x ∈ Set.Icc (1 / 2) 1
[PROOFSTEP]
exact ⟨(not_le.1 h).le, unitInterval.le_one x⟩
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x ∈ {0, 1}
⊢ ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              {
                  toContinuousMap :=
                    ContinuousMap.mk fun x =>
                      ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) },
                  map_zero_left :=
                    (_ :
                      ∀ (a : ↑I),
                        ↑p { val := reflTransSymmAux (0, a), property := (_ : reflTransSymmAux (0, a) ∈ I) } = x₀),
                  map_one_left :=
                    (_ :
                      ∀ (x : ↑I),
                        ContinuousMap.toFun
                            (ContinuousMap.mk fun x =>
                              ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) })
                            (1, x) =
                          ↑(Path.trans p (Path.symm p)).toContinuousMap x) }.toContinuousMap
              (t, x))
        x =
      ↑(Path.refl x₀).toContinuousMap x ∧
    ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              {
                  toContinuousMap :=
                    ContinuousMap.mk fun x =>
                      ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) },
                  map_zero_left :=
                    (_ :
                      ∀ (a : ↑I),
                        ↑p { val := reflTransSymmAux (0, a), property := (_ : reflTransSymmAux (0, a) ∈ I) } = x₀),
                  map_one_left :=
                    (_ :
                      ∀ (x : ↑I),
                        ContinuousMap.toFun
                            (ContinuousMap.mk fun x =>
                              ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) })
                            (1, x) =
                          ↑(Path.trans p (Path.symm p)).toContinuousMap x) }.toContinuousMap
              (t, x))
        x =
      ↑(Path.trans p (Path.symm p)).toContinuousMap x
[PROOFSTEP]
simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at hx
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0 ∨ x = 1
⊢ ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              {
                  toContinuousMap :=
                    ContinuousMap.mk fun x =>
                      ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) },
                  map_zero_left :=
                    (_ :
                      ∀ (a : ↑I),
                        ↑p { val := reflTransSymmAux (0, a), property := (_ : reflTransSymmAux (0, a) ∈ I) } = x₀),
                  map_one_left :=
                    (_ :
                      ∀ (x : ↑I),
                        ContinuousMap.toFun
                            (ContinuousMap.mk fun x =>
                              ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) })
                            (1, x) =
                          ↑(Path.trans p (Path.symm p)).toContinuousMap x) }.toContinuousMap
              (t, x))
        x =
      ↑(Path.refl x₀).toContinuousMap x ∧
    ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              {
                  toContinuousMap :=
                    ContinuousMap.mk fun x =>
                      ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) },
                  map_zero_left :=
                    (_ :
                      ∀ (a : ↑I),
                        ↑p { val := reflTransSymmAux (0, a), property := (_ : reflTransSymmAux (0, a) ∈ I) } = x₀),
                  map_one_left :=
                    (_ :
                      ∀ (x : ↑I),
                        ContinuousMap.toFun
                            (ContinuousMap.mk fun x =>
                              ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) })
                            (1, x) =
                          ↑(Path.trans p (Path.symm p)).toContinuousMap x) }.toContinuousMap
              (t, x))
        x =
      ↑(Path.trans p (Path.symm p)).toContinuousMap x
[PROOFSTEP]
simp only [ContinuousMap.coe_mk, coe_toContinuousMap, Path.refl_apply]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0 ∨ x = 1
⊢ ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) x
[PROOFSTEP]
cases hx with
| inl hx| inr hx =>
  rw [hx]
  simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
    sub_self, Path.source, Path.target, and_self]
  norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0 ∨ x = 1
⊢ ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) x
[PROOFSTEP]
cases hx with
| inl hx =>
  rw [hx]
  simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
    sub_self, Path.source, Path.target, and_self]
  norm_num
| inr hx =>
  rw [hx]
  simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
    sub_self, Path.source, Path.target, and_self]
  norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0 ∨ x = 1
⊢ ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) x
[PROOFSTEP]
cases hx with
| inl hx =>
  rw [hx]
  simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
    sub_self, Path.source, Path.target, and_self]
  norm_num
| inr hx =>
  rw [hx]
  simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
    sub_self, Path.source, Path.target, and_self]
  norm_num
[GOAL]
case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0
⊢ ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) x
[PROOFSTEP]

| inl hx =>
  rw [hx]
  simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
    sub_self, Path.source, Path.target, and_self]
  norm_num
[GOAL]
case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0
⊢ ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) x
[PROOFSTEP]
rw [hx]
[GOAL]
case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0
⊢ ↑p { val := reflTransSymmAux (t, 0), property := (_ : reflTransSymmAux (t, 0) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, 0), property := (_ : reflTransSymmAux (t, 0) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) 0
[PROOFSTEP]
simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
  sub_self, Path.source, Path.target, and_self]
[GOAL]
case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0
⊢ ↑p { val := if 0 ≤ 2 then 0 else ↑t * 2, property := (_ : (fun x => x ∈ I) (if 0 ≤ 2 then 0 else ↑t * 2)) } = x₀
[PROOFSTEP]
norm_num
[GOAL]
case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 1
⊢ ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) x
[PROOFSTEP]

| inr hx =>
  rw [hx]
  simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
    sub_self, Path.source, Path.target, and_self]
  norm_num
[GOAL]
case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 1
⊢ ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) x
[PROOFSTEP]
rw [hx]
[GOAL]
case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 1
⊢ ↑p { val := reflTransSymmAux (t, 1), property := (_ : reflTransSymmAux (t, 1) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, 1), property := (_ : reflTransSymmAux (t, 1) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) 1
[PROOFSTEP]
simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
  sub_self, Path.source, Path.target, and_self]
[GOAL]
case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 1
⊢ ↑p { val := if 1 ≤ 2⁻¹ then ↑t * 2 else 0, property := (_ : (fun x => x ∈ I) (if 1 ≤ 2⁻¹ then ↑t * 2 else 0)) } = x₀
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous transReflReparamAux
[PROOFSTEP]
refine' continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _ <;> [continuity; continuity;
  continuity; continuity; skip]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous transReflReparamAux
[PROOFSTEP]
refine' continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _
[GOAL]
case refine'_1
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x
[PROOFSTEP]
continuity
[GOAL]
case refine'_2
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 1 / 2
[PROOFSTEP]
continuity
[GOAL]
case refine'_3
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 2 * ↑x
[PROOFSTEP]
continuity
[GOAL]
case refine'_4
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 1
[PROOFSTEP]
continuity
[GOAL]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 2 → 2 * ↑x = 1
[PROOFSTEP]
skip
[GOAL]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 2 → 2 * ↑x = 1
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 2
⊢ 2 * ↑x = 1
[PROOFSTEP]
simp [hx]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
⊢ transReflReparamAux t ∈ I
[PROOFSTEP]
unfold transReflReparamAux
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) ∈ I
[PROOFSTEP]
split_ifs
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 2 * ↑t ∈ I
[PROOFSTEP]
constructor
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ∈ I
[PROOFSTEP]
constructor
[GOAL]
case pos.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 0 ≤ 2 * ↑t
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case pos.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 2 * ↑t ≤ 1
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case neg.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 ≤ 1
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case neg.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 1
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ transReflReparamAux 0 = 0
[PROOFSTEP]
simp [transReflReparamAux]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ 2 < 0 → False
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ transReflReparamAux 1 = 1
[PROOFSTEP]
simp [transReflReparamAux]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ 1 ≤ 2⁻¹ → False
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Continuous fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) }
[PROOFSTEP]
continuity
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Path.trans p (Path.refl x₁) =
    Path.reparam p (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) })
      (_ : Continuous fun x => { val := transReflReparamAux x, property := (_ : transReflReparamAux x ∈ I) })
      (_ : (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) }) 0 = 0)
      (_ : (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) }) 1 = 1)
[PROOFSTEP]
ext
[GOAL]
case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ ↑(Path.trans p (Path.refl x₁)) x✝ =
    ↑(Path.reparam p (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) })
          (_ : Continuous fun x => { val := transReflReparamAux x, property := (_ : transReflReparamAux x ∈ I) })
          (_ : (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) }) 0 = 0)
          (_ : (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) }) 1 = 1))
      x✝
[PROOFSTEP]
unfold transReflReparamAux
[GOAL]
case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ ↑(Path.trans p (Path.refl x₁)) x✝ =
    ↑(Path.reparam p (fun t => { val := if ↑t ≤ 1 / 2 then 2 * ↑t else 1, property := (_ : transReflReparamAux t ∈ I) })
          (_ :
            Continuous fun x =>
              { val := if ↑x ≤ 1 / 2 then 2 * ↑x else 1, property := (_ : transReflReparamAux x ∈ I) })
          (_ :
            (fun t => { val := if ↑t ≤ 1 / 2 then 2 * ↑t else 1, property := (_ : transReflReparamAux t ∈ I) }) 0 = 0)
          (_ :
            (fun t => { val := if ↑t ≤ 1 / 2 then 2 * ↑t else 1, property := (_ : transReflReparamAux t ∈ I) }) 1 = 1))
      x✝
[PROOFSTEP]
simp only [Path.trans_apply, not_le, coe_reparam, Function.comp_apply, one_div, Path.refl_apply]
[GOAL]
case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (if h : ↑x✝ ≤ 2⁻¹ then ↑p { val := 2 * ↑x✝, property := (_ : 2 * ↑x✝ ∈ I) } else x₁) =
    ↑p
      { val := if ↑x✝ ≤ 2⁻¹ then 2 * ↑x✝ else 1, property := (_ : (fun x => x ∈ I) (if ↑x✝ ≤ 2⁻¹ then 2 * ↑x✝ else 1)) }
[PROOFSTEP]
split_ifs
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ↑x✝ ≤ 2⁻¹
h✝ : ↑x✝ ≤ 2⁻¹
⊢ ↑p { val := 2 * ↑x✝, property := (_ : 2 * ↑x✝ ∈ I) } =
    ↑p { val := 2 * ↑x✝, property := (_ : (fun x => x ∈ I) (2 * ↑x✝)) }
[PROOFSTEP]
rfl
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ↑x✝ ≤ 2⁻¹
h✝ : ¬↑x✝ ≤ 2⁻¹
⊢ ↑p { val := 2 * ↑x✝, property := (_ : 2 * ↑x✝ ∈ I) } =
    ↑p { val := 2 * ↑x✝, property := (_ : (fun x => x ∈ I) (2 * ↑x✝)) }
[PROOFSTEP]
rfl
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ¬↑x✝ ≤ 2⁻¹
h✝ : ↑x✝ ≤ 2⁻¹
⊢ x₁ = ↑p { val := 1, property := (_ : (fun x => x ∈ I) 1) }
[PROOFSTEP]
simp
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ¬↑x✝ ≤ 2⁻¹
h✝ : ¬↑x✝ ≤ 2⁻¹
⊢ x₁ = ↑p { val := 1, property := (_ : (fun x => x ∈ I) 1) }
[PROOFSTEP]
simp
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Continuous fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) }
[PROOFSTEP]
continuity
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Path.symm (Path.trans (Path.symm p) (Path.refl x₀)) = Path.trans (Path.refl x₀) p
[PROOFSTEP]
simp
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Path.symm (Path.symm p) = p
[PROOFSTEP]
simp
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous transAssocReparamAux
[PROOFSTEP]
refine'
    continuous_if_le _ _ (Continuous.continuousOn _)
      (continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _).continuousOn _ <;>
  [continuity; continuity; continuity; continuity; continuity; continuity; continuity; skip; skip]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous transAssocReparamAux
[PROOFSTEP]
refine'
  continuous_if_le _ _ (Continuous.continuousOn _)
    (continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _).continuousOn _
[GOAL]
case refine'_1
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x
[PROOFSTEP]
continuity
[GOAL]
case refine'_2
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 1 / 4
[PROOFSTEP]
continuity
[GOAL]
case refine'_3
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 2 * ↑x
[PROOFSTEP]
continuity
[GOAL]
case refine'_4
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x
[PROOFSTEP]
continuity
[GOAL]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 1 / 2
[PROOFSTEP]
continuity
[GOAL]
case refine'_6
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x + 1 / 4
[PROOFSTEP]
continuity
[GOAL]
case refine'_7
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 1 / 2 * (↑x + 1)
[PROOFSTEP]
continuity
[GOAL]
case refine'_8
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 2 → ↑x + 1 / 4 = 1 / 2 * (↑x + 1)
[PROOFSTEP]
skip
[GOAL]
case refine'_9
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 4 → 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)
[PROOFSTEP]
skip
[GOAL]
case refine'_8
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 2 → ↑x + 1 / 4 = 1 / 2 * (↑x + 1)
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_8
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 2
⊢ ↑x + 1 / 4 = 1 / 2 * (↑x + 1)
[PROOFSTEP]
simp [hx]
[GOAL]
case refine'_8
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 2
⊢ 2⁻¹ + 4⁻¹ = 2⁻¹ * (2⁻¹ + 1)
[PROOFSTEP]
norm_num
[GOAL]
case refine'_9
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 4 → 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_9
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 4
⊢ 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)
[PROOFSTEP]
simp [hx]
[GOAL]
case refine'_9
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 4
⊢ 2 * 4⁻¹ = if 4⁻¹ ≤ 2⁻¹ then 4⁻¹ + 4⁻¹ else 2⁻¹ * (4⁻¹ + 1)
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
⊢ transAssocReparamAux t ∈ I
[PROOFSTEP]
unfold transAssocReparamAux
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
⊢ (if ↑t ≤ 1 / 4 then 2 * ↑t else if ↑t ≤ 1 / 2 then ↑t + 1 / 4 else 1 / 2 * (↑t + 1)) ∈ I
[PROOFSTEP]
split_ifs
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 2 * ↑t ∈ I
[PROOFSTEP]
constructor
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ ↑t + 1 / 4 ∈ I
[PROOFSTEP]
constructor
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 / 2 * (↑t + 1) ∈ I
[PROOFSTEP]
constructor
[GOAL]
case pos.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 0 ≤ 2 * ↑t
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case pos.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 2 * ↑t ≤ 1
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case pos.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ 0 ≤ ↑t + 1 / 4
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case pos.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ ↑t + 1 / 4 ≤ 1
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case neg.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 ≤ 1 / 2 * (↑t + 1)
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case neg.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 / 2 * (↑t + 1) ≤ 1
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ transAssocReparamAux 0 = 0
[PROOFSTEP]
simp [transAssocReparamAux]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ 4 < 0 → (if 0 ≤ 2 then 4⁻¹ else 2⁻¹) = 0
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ transAssocReparamAux 1 = 1
[PROOFSTEP]
simp [transAssocReparamAux]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ (if 1 ≤ 4⁻¹ then 2 else if 1 ≤ 2⁻¹ then 1 + 4⁻¹ else 2⁻¹ * (1 + 1)) = 1
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
⊢ Continuous fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) }
[PROOFSTEP]
continuity
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
⊢ Path.trans (Path.trans p q) r =
    Path.reparam (Path.trans p (Path.trans q r))
      (fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) })
      (_ : Continuous fun x => { val := transAssocReparamAux x, property := (_ : transAssocReparamAux x ∈ I) })
      (_ : (fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) }) 0 = 0)
      (_ : (fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) }) 1 = 1)
[PROOFSTEP]
ext x
[GOAL]
case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
⊢ ↑(Path.trans (Path.trans p q) r) x =
    ↑(Path.reparam (Path.trans p (Path.trans q r))
          (fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) })
          (_ : Continuous fun x => { val := transAssocReparamAux x, property := (_ : transAssocReparamAux x ∈ I) })
          (_ : (fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) }) 0 = 0)
          (_ : (fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) }) 1 = 1))
      x
[PROOFSTEP]
simp only [transAssocReparamAux, Path.trans_apply, mul_inv_cancel_left₀, not_le, Function.comp_apply, Ne.def,
  not_false_iff, bit0_eq_zero, one_ne_zero, mul_ite, Subtype.coe_mk, Path.coe_reparam]
  -- TODO: why does split_ifs not reduce the ifs??????
[GOAL]
case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
⊢ (if h : ↑x ≤ 1 / 2 then
      if h_1 : 2 * ↑x ≤ 1 / 2 then
        ↑p { val := 2 * (2 * ↑x), property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } ∈ I) }
      else
        ↑q { val := 2 * (2 * ↑x) - 1, property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } - 1 ∈ I) }
    else ↑r { val := 2 * ↑x - 1, property := (_ : 2 * ↑x - 1 ∈ I) }) =
    if h : (if ↑x ≤ 1 / 4 then 2 * ↑x else if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)) ≤ 1 / 2 then
      ↑p
        { val := if ↑x ≤ 1 / 4 then 2 * (2 * ↑x) else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1)),
          property :=
            (_ :
              (fun x => x ∈ I)
                (if ↑x ≤ 1 / 4 then 2 * (2 * ↑x)
                else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1)))) }
    else
      if h_1 :
          (if ↑x ≤ 1 / 4 then 2 * (2 * ↑x) else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) - 1 ≤
            1 / 2 then
        ↑q
          {
            val :=
              2 *
                ((if ↑x ≤ 1 / 4 then 2 * (2 * ↑x)
                  else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) -
                  1),
            property :=
              (_ :
                2 *
                    ↑{
                        val :=
                          (if ↑x ≤ 1 / 4 then 2 * (2 * ↑x)
                            else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) -
                            1,
                        property :=
                          (_ :
                            (fun x => x ∈ I)
                              ((if ↑x ≤ 1 / 4 then 2 * (2 * ↑x)
                                else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) -
                                1)) } ∈
                  I) }
      else
        ↑r
          {
            val :=
              2 *
                  ((if ↑x ≤ 1 / 4 then 2 * (2 * ↑x)
                    else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) -
                    1) -
                1,
            property :=
              (_ :
                2 *
                      ↑{
                          val :=
                            (if ↑x ≤ 1 / 4 then 2 * (2 * ↑x)
                              else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) -
                              1,
                          property :=
                            (_ :
                              (fun x => x ∈ I)
                                ((if ↑x ≤ 1 / 4 then 2 * (2 * ↑x)
                                  else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) -
                                  1)) } -
                    1 ∈
                  I) }
[PROOFSTEP]
split_ifs with h₁ h₂ h₃ h₄ h₅
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : 2 * ↑x ≤ 1 / 2
h₃ : ↑x ≤ 1 / 4
⊢ ↑p { val := 2 * (2 * ↑x), property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } ∈ I) } =
    ↑p { val := 2 * (2 * ↑x), property := (_ : (fun x => x ∈ I) (2 * (2 * ↑x))) }
[PROOFSTEP]
rfl
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : 2 * ↑x ≤ 1 / 2
h₃ : ¬↑x ≤ 1 / 4
h₄ : ↑x + 1 / 4 ≤ 1 / 2
⊢ ↑p { val := 2 * (2 * ↑x), property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } ∈ I) } =
    ↑p { val := 2 * (↑x + 1 / 4), property := (_ : (fun x => x ∈ I) (2 * (↑x + 1 / 4))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : 2 * ↑x ≤ 1 / 2
h₃ : ¬↑x ≤ 1 / 4
h₄ : ↑x + 1 / 4 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : 2 * ↑x ≤ 1 / 2
h₃ : ¬↑x ≤ 1 / 4
h₄ : ¬↑x + 1 / 4 ≤ 1 / 2
h₅ : 2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ ↑p { val := 2 * (2 * ↑x), property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } ∈ I) } =
    ↑q { val := 2 * (2 * (↑x + 1 / 4) - 1), property := (_ : (fun x => x ∈ I) (2 * (2 * (↑x + 1 / 4) - 1))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : 2 * ↑x ≤ 1 / 2
h₃ : ¬↑x ≤ 1 / 4
h₄ : ¬↑x + 1 / 4 ≤ 1 / 2
h₅ : 2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : 2 * ↑x ≤ 1 / 2
h₃ : ¬↑x ≤ 1 / 4
h₄ : ¬↑x + 1 / 4 ≤ 1 / 2
h₅ : ¬2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ ↑p { val := 2 * (2 * ↑x), property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } ∈ I) } =
    ↑r { val := 2 * (2 * (↑x + 1 / 4) - 1) - 1, property := (_ : (fun x => x ∈ I) (2 * (2 * (↑x + 1 / 4) - 1) - 1)) }
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : 2 * ↑x ≤ 1 / 2
h₃ : ¬↑x ≤ 1 / 4
h₄ : ¬↑x + 1 / 4 ≤ 1 / 2
h₅ : ¬2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : 2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ ↑q { val := 2 * (2 * ↑x) - 1, property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } - 1 ∈ I) } =
    ↑q { val := 2 * (2 * (2 * ↑x) - 1), property := (_ : (fun x => x ∈ I) (2 * (2 * (2 * ↑x) - 1))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : 2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ ↑q { val := 2 * (2 * ↑x) - 1, property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } - 1 ∈ I) } =
    ↑r { val := 2 * (2 * (2 * ↑x) - 1) - 1, property := (_ : (fun x => x ∈ I) (2 * (2 * (2 * ↑x) - 1) - 1)) }
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : ↑x + 1 / 4 ≤ 1 / 2
⊢ ↑q { val := 2 * (2 * ↑x) - 1, property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } - 1 ∈ I) } =
    ↑p { val := 2 * (↑x + 1 / 4), property := (_ : (fun x => x ∈ I) (2 * (↑x + 1 / 4))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : ↑x + 1 / 4 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬↑x + 1 / 4 ≤ 1 / 2
h✝ : 2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ ↑q { val := 2 * (2 * ↑x) - 1, property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } - 1 ∈ I) } =
    ↑q { val := 2 * (2 * (↑x + 1 / 4) - 1), property := (_ : (fun x => x ∈ I) (2 * (2 * (↑x + 1 / 4) - 1))) }
[PROOFSTEP]
have h : 2 * (2 * (x : ℝ)) - 1 = 2 * (2 * (↑x + 1 / 4) - 1) := by linarith
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬↑x + 1 / 4 ≤ 1 / 2
h✝ : 2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ 2 * (2 * ↑x) - 1 = 2 * (2 * (↑x + 1 / 4) - 1)
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬↑x + 1 / 4 ≤ 1 / 2
h✝ : 2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
h : 2 * (2 * ↑x) - 1 = 2 * (2 * (↑x + 1 / 4) - 1)
⊢ ↑q { val := 2 * (2 * ↑x) - 1, property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } - 1 ∈ I) } =
    ↑q { val := 2 * (2 * (↑x + 1 / 4) - 1), property := (_ : (fun x => x ∈ I) (2 * (2 * (↑x + 1 / 4) - 1))) }
[PROOFSTEP]
simp [h₂, h₁, h, dif_neg (show ¬False from id), dif_pos True.intro, if_false, if_true]
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬↑x + 1 / 4 ≤ 1 / 2
h✝ : ¬2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ ↑q { val := 2 * (2 * ↑x) - 1, property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } - 1 ∈ I) } =
    ↑r { val := 2 * (2 * (↑x + 1 / 4) - 1) - 1, property := (_ : (fun x => x ∈ I) (2 * (2 * (↑x + 1 / 4) - 1) - 1)) }
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬↑x + 1 / 4 ≤ 1 / 2
h✝ : ¬2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : 2 * ↑x ≤ 1 / 2
⊢ ↑r { val := 2 * ↑x - 1, property := (_ : 2 * ↑x - 1 ∈ I) } =
    ↑p { val := 2 * (2 * ↑x), property := (_ : (fun x => x ∈ I) (2 * (2 * ↑x))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : 2 * ↑x ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : 2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ ↑r { val := 2 * ↑x - 1, property := (_ : 2 * ↑x - 1 ∈ I) } =
    ↑q { val := 2 * (2 * (2 * ↑x) - 1), property := (_ : (fun x => x ∈ I) (2 * (2 * (2 * ↑x) - 1))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : 2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ ↑r { val := 2 * ↑x - 1, property := (_ : 2 * ↑x - 1 ∈ I) } =
    ↑r { val := 2 * (2 * (2 * ↑x) - 1) - 1, property := (_ : (fun x => x ∈ I) (2 * (2 * (2 * ↑x) - 1) - 1)) }
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : 1 / 2 * (↑x + 1) ≤ 1 / 2
⊢ ↑r { val := 2 * ↑x - 1, property := (_ : 2 * ↑x - 1 ∈ I) } =
    ↑p { val := 2 * (1 / 2 * (↑x + 1)), property := (_ : (fun x => x ∈ I) (2 * (1 / 2 * (↑x + 1)))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : 1 / 2 * (↑x + 1) ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : 2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ ↑r { val := 2 * ↑x - 1, property := (_ : 2 * ↑x - 1 ∈ I) } =
    ↑q
      { val := 2 * (2 * (1 / 2 * (↑x + 1)) - 1), property := (_ : (fun x => x ∈ I) (2 * (2 * (1 / 2 * (↑x + 1)) - 1))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : 2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : ¬2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ ↑r { val := 2 * ↑x - 1, property := (_ : 2 * ↑x - 1 ∈ I) } =
    ↑r
      { val := 2 * (2 * (1 / 2 * (↑x + 1)) - 1) - 1,
        property := (_ : (fun x => x ∈ I) (2 * (2 * (1 / 2 * (↑x + 1)) - 1) - 1)) }
[PROOFSTEP]
congr
[GOAL]
case neg.h.e_6.h.e_val.e_a.e_a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : ¬2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ ↑x = 2 * (1 / 2 * (↑x + 1)) - 1
[PROOFSTEP]
ring
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
⊢ Continuous fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) }
[PROOFSTEP]
continuity
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x y : FundamentalGroupoid X
p : x ⟶ y
⊢ ∀ (a b : Path x y),
    a ≈ b →
      (fun l => Quotient.mk (Path.Homotopic.setoid y x) (Path.symm l)) a =
        (fun l => Quotient.mk (Path.Homotopic.setoid y x) (Path.symm l)) b
[PROOFSTEP]
rintro a b ⟨h⟩
[GOAL]
case intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x y : FundamentalGroupoid X
p : x ⟶ y
a b : Path x y
h : Path.Homotopy a b
⊢ (fun l => Quotient.mk (Path.Homotopic.setoid y x) (Path.symm l)) a =
    (fun l => Quotient.mk (Path.Homotopic.setoid y x) (Path.symm l)) b
[PROOFSTEP]
simp only
[GOAL]
case intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x y : FundamentalGroupoid X
p : x ⟶ y
a b : Path x y
h : Path.Homotopy a b
⊢ Quotient.mk (Path.Homotopic.setoid y x) (Path.symm a) = Quotient.mk (Path.Homotopic.setoid y x) (Path.symm b)
[PROOFSTEP]
rw [Quotient.eq]
[GOAL]
case intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x y : FundamentalGroupoid X
p : x ⟶ y
a b : Path x y
h : Path.Homotopy a b
⊢ Path.symm a ≈ Path.symm b
[PROOFSTEP]
exact ⟨h.symm₂⟩
[GOAL]
X✝¹ : Type u
Y✝¹ : Type v
inst✝¹ : TopologicalSpace X✝¹
inst✝ : TopologicalSpace Y✝¹
x₀ x₁ : X✝¹
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
X Y : ↑((fun X => Bundled.mk (FundamentalGroupoid ↑X)) X✝)
p : X ⟶ Y
⊢ ↑f X ⟶ ↑f Y
[PROOFSTEP]
exact Path.Homotopic.Quotient.mapFn p f
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
x y z : ↑((fun X => Bundled.mk (FundamentalGroupoid ↑X)) X✝)
p : x ⟶ y
q : y ⟶ z
⊢ { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }.map (p ≫ q) =
    { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }.map p ≫
      { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }.map q
[PROOFSTEP]
refine' Quotient.inductionOn₂ p q fun a b => _
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
x y z : ↑((fun X => Bundled.mk (FundamentalGroupoid ↑X)) X✝)
p : x ⟶ y
q : y ⟶ z
a : Path x y
b : Path y z
⊢ { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }.map
      (Quotient.mk (Path.Homotopic.setoid x y) a ≫ Quotient.mk (Path.Homotopic.setoid y z) b) =
    { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }.map
        (Quotient.mk (Path.Homotopic.setoid x y) a) ≫
      { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }.map
        (Quotient.mk (Path.Homotopic.setoid y z) b)
[PROOFSTEP]
simp only [comp_eq, ← Path.Homotopic.map_lift, ← Path.Homotopic.comp_lift, Path.map_trans]
[GOAL]
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
⊢ { obj := fun X => Bundled.mk (FundamentalGroupoid ↑X),
          map := fun {X Y} f =>
            CategoryTheory.Functor.mk { obj := ↑f, map := fun {X_1 Y_1} p => Path.Homotopic.Quotient.mapFn p f } }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun X => Bundled.mk (FundamentalGroupoid ↑X),
            map := fun {X Y} f =>
              CategoryTheory.Functor.mk { obj := ↑f, map := fun {X_1 Y_1} p => Path.Homotopic.Quotient.mapFn p f } }.obj
        X)
[PROOFSTEP]
simp only
[GOAL]
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
⊢ CategoryTheory.Functor.mk { obj := ↑(𝟙 X), map := fun {X_1 Y} p => Path.Homotopic.Quotient.mapFn p (𝟙 X) } =
    𝟙 (Bundled.mk (FundamentalGroupoid ↑X))
[PROOFSTEP]
change _ = (⟨_, _, _⟩ : FundamentalGroupoid X ⥤ FundamentalGroupoid X)
[GOAL]
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
⊢ CategoryTheory.Functor.mk { obj := ↑(𝟙 X), map := fun {X_1 Y} p => Path.Homotopic.Quotient.mapFn p (𝟙 X) } =
    CategoryTheory.Functor.mk { obj := fun X => X, map := fun {X_1 Y} f => f }
[PROOFSTEP]
congr
[GOAL]
case e_toPrefunctor.e_map
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
⊢ (fun {X_1 Y} p => Path.Homotopic.Quotient.mapFn p (𝟙 X)) = fun {X_1 Y} f => f
[PROOFSTEP]
ext x y p
[GOAL]
case e_toPrefunctor.e_map.h.h.h
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
x y : FundamentalGroupoid ↑X
p : x ⟶ y
⊢ Path.Homotopic.Quotient.mapFn p (𝟙 X) = p
[PROOFSTEP]
refine' Quotient.inductionOn p fun q => _
[GOAL]
case e_toPrefunctor.e_map.h.h.h
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
x y : FundamentalGroupoid ↑X
p : x ⟶ y
q : Path x y
⊢ Path.Homotopic.Quotient.mapFn (Quotient.mk (Path.Homotopic.setoid x y) q) (𝟙 X) =
    Quotient.mk (Path.Homotopic.setoid x y) q
[PROOFSTEP]
rw [← Path.Homotopic.map_lift]
[GOAL]
case e_toPrefunctor.e_map.h.h.h
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
x y : FundamentalGroupoid ↑X
p : x ⟶ y
q : Path x y
⊢ Quotient.mk (Path.Homotopic.setoid (↑(𝟙 X) x) (↑(𝟙 X) y)) (Path.map q (_ : Continuous ↑(𝟙 X))) =
    Quotient.mk (Path.Homotopic.setoid x y) q
[PROOFSTEP]
conv_rhs => rw [← q.map_id]
[GOAL]
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
x y : FundamentalGroupoid ↑X
p : x ⟶ y
q : Path x y
| Quotient.mk (Path.Homotopic.setoid x y) q
[PROOFSTEP]
rw [← q.map_id]
[GOAL]
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
x y : FundamentalGroupoid ↑X
p : x ⟶ y
q : Path x y
| Quotient.mk (Path.Homotopic.setoid x y) q
[PROOFSTEP]
rw [← q.map_id]
[GOAL]
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
x y : FundamentalGroupoid ↑X
p : x ⟶ y
q : Path x y
| Quotient.mk (Path.Homotopic.setoid x y) q
[PROOFSTEP]
rw [← q.map_id]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => Bundled.mk (FundamentalGroupoid ↑X),
          map := fun {X Y} f =>
            CategoryTheory.Functor.mk { obj := ↑f, map := fun {X_1 Y_1} p => Path.Homotopic.Quotient.mapFn p f } }.map
      (f ≫ g) =
    { obj := fun X => Bundled.mk (FundamentalGroupoid ↑X),
            map := fun {X Y} f =>
              CategoryTheory.Functor.mk { obj := ↑f, map := fun {X_1 Y_1} p => Path.Homotopic.Quotient.mapFn p f } }.map
        f ≫
      { obj := fun X => Bundled.mk (FundamentalGroupoid ↑X),
            map := fun {X Y} f =>
              CategoryTheory.Functor.mk { obj := ↑f, map := fun {X_1 Y_1} p => Path.Homotopic.Quotient.mapFn p f } }.map
        g
[PROOFSTEP]
simp only
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ CategoryTheory.Functor.mk { obj := ↑(f ≫ g), map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p (f ≫ g) } =
    CategoryTheory.Functor.mk { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f } ≫
      CategoryTheory.Functor.mk { obj := ↑g, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p g }
[PROOFSTEP]
congr
[GOAL]
case e_toPrefunctor.e_map
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (fun {X Y} p => Path.Homotopic.Quotient.mapFn p (f ≫ g)) = fun {X Y} f_1 =>
    (CategoryTheory.Functor.mk { obj := ↑g, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p g }).map
      ((CategoryTheory.Functor.mk { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }).map f_1)
[PROOFSTEP]
ext x y p
[GOAL]
case e_toPrefunctor.e_map.h.h.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x y : FundamentalGroupoid ↑X✝
p : x ⟶ y
⊢ Path.Homotopic.Quotient.mapFn p (f ≫ g) =
    (CategoryTheory.Functor.mk { obj := ↑g, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p g }).map
      ((CategoryTheory.Functor.mk { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }).map p)
[PROOFSTEP]
refine' Quotient.inductionOn p fun q => _
[GOAL]
case e_toPrefunctor.e_map.h.h.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x y : FundamentalGroupoid ↑X✝
p : x ⟶ y
q : Path x y
⊢ Path.Homotopic.Quotient.mapFn (Quotient.mk (Path.Homotopic.setoid x y) q) (f ≫ g) =
    (CategoryTheory.Functor.mk { obj := ↑g, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p g }).map
      ((CategoryTheory.Functor.mk { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }).map
        (Quotient.mk (Path.Homotopic.setoid x y) q))
[PROOFSTEP]
simp only [Quotient.map_mk, Path.map_map, Quotient.eq']
[GOAL]
case e_toPrefunctor.e_map.h.h.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x y : FundamentalGroupoid ↑X✝
p : x ⟶ y
q : Path x y
⊢ Path.Homotopic.Quotient.mapFn (Quotient.mk (Path.Homotopic.setoid x y) q) (f ≫ g) =
    Path.Homotopic.Quotient.mapFn (Path.Homotopic.Quotient.mapFn (Quotient.mk (Path.Homotopic.setoid x y) q) f) g
[PROOFSTEP]
rfl


[GOAL]
α : Type u
σ σ' : Type v
M : NFA α σ
s : σ
S : Set σ
a : α
⊢ s ∈ stepSet M S a ↔ ∃ t, t ∈ S ∧ s ∈ step M t a
[PROOFSTEP]
simp [stepSet]
[GOAL]
α : Type u
σ σ' : Type v
M : NFA α σ
a : α
⊢ stepSet M ∅ a = ∅
[PROOFSTEP]
simp [stepSet]
[GOAL]
α : Type u
σ σ' : Type v
M : NFA α σ
S : Set σ
x : List α
a : α
⊢ evalFrom M S (x ++ [a]) = stepSet M (evalFrom M S x) a
[PROOFSTEP]
simp only [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]
[GOAL]
α : Type u
σ σ' : Type v
M : NFA α σ
x : List α
⊢ x ∈ accepts M ↔ ∃ S, S ∈ M.accept ∧ S ∈ evalFrom M M.start x
[PROOFSTEP]
rfl
[GOAL]
α : Type u
σ σ' : Type v
M : NFA α σ
⊢ DFA.accepts (toDFA M) = accepts M
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
σ σ' : Type v
M : NFA α σ
x : List α
⊢ x ∈ DFA.accepts (toDFA M) ↔ x ∈ accepts M
[PROOFSTEP]
rw [mem_accepts, DFA.mem_accepts]
[GOAL]
case h
α : Type u
σ σ' : Type v
M : NFA α σ
x : List α
⊢ DFA.evalFrom (toDFA M) (toDFA M).start x ∈ (toDFA M).accept ↔ ∃ S, S ∈ M.accept ∧ S ∈ evalFrom M M.start x
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u
σ σ' : Type v
M : NFA α σ
x : List α
⊢ DFA.evalFrom (toDFA M) (toDFA M).start x ∈ (toDFA M).accept → ∃ S, S ∈ M.accept ∧ S ∈ evalFrom M M.start x
[PROOFSTEP]
exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩
[GOAL]
case h.mpr
α : Type u
σ σ' : Type v
M : NFA α σ
x : List α
⊢ (∃ S, S ∈ M.accept ∧ S ∈ evalFrom M M.start x) → DFA.evalFrom (toDFA M) (toDFA M).start x ∈ (toDFA M).accept
[PROOFSTEP]
exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩
[GOAL]
α : Type u
σ σ' : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ accepts M
hlen : Fintype.card (Set σ) ≤ List.length x
⊢ ∃ a b c,
    x = a ++ b ++ c ∧ List.length a + List.length b ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ accepts M
[PROOFSTEP]
rw [← toDFA_correct] at hx ⊢
[GOAL]
α : Type u
σ σ' : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ DFA.accepts (toDFA M)
hlen : Fintype.card (Set σ) ≤ List.length x
⊢ ∃ a b c,
    x = a ++ b ++ c ∧
      List.length a + List.length b ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ DFA.accepts (toDFA M)
[PROOFSTEP]
exact M.toDFA.pumping_lemma hx hlen
[GOAL]
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start : σ
s : List α
⊢ NFA.evalFrom (toNFA M) {start} s = {evalFrom M start s}
[PROOFSTEP]
change List.foldl M.toNFA.stepSet { start } s = {List.foldl M.step start s}
[GOAL]
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start : σ
s : List α
⊢ List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
[PROOFSTEP]
induction' s with a s ih generalizing start
[GOAL]
case nil
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ start : σ
⊢ List.foldl (NFA.stepSet (toNFA M)) {start} [] = {List.foldl M.step start []}
[PROOFSTEP]
tauto
[GOAL]
case cons
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ : σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl (NFA.stepSet (toNFA M)) {start} (a :: s) = {List.foldl M.step start (a :: s)}
[PROOFSTEP]
rw [List.foldl, List.foldl, show M.toNFA.stepSet { start } a = {M.step start a} by simp [NFA.stepSet]]
[GOAL]
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ : σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
start : σ
⊢ NFA.stepSet (toNFA M) {start} a = {step M start a}
[PROOFSTEP]
simp [NFA.stepSet]
[GOAL]
case cons
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ : σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl (NFA.stepSet (toNFA M)) {step M start a} s = {List.foldl M.step (step M start a) s}
[PROOFSTEP]
tauto
[GOAL]
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
⊢ NFA.accepts (toNFA M) = accepts M
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ x ∈ NFA.accepts (toNFA M) ↔ x ∈ accepts M
[PROOFSTEP]
rw [NFA.mem_accepts, toNFA_start, toNFA_evalFrom_match]
[GOAL]
case h
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ (∃ S, S ∈ (toNFA M).accept ∧ S ∈ {evalFrom M M.start x}) ↔ x ∈ accepts M
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ (∃ S, S ∈ (toNFA M).accept ∧ S ∈ {evalFrom M M.start x}) → x ∈ accepts M
[PROOFSTEP]
rintro ⟨S, hS₁, hS₂⟩
[GOAL]
case h.mp.intro.intro
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
S : σ
hS₁ : S ∈ (toNFA M).accept
hS₂ : S ∈ {evalFrom M M.start x}
⊢ x ∈ accepts M
[PROOFSTEP]
rwa [Set.mem_singleton_iff.mp hS₂] at hS₁
[GOAL]
case h.mpr
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
x : List α
⊢ x ∈ accepts M → ∃ S, S ∈ (toNFA M).accept ∧ S ∈ {evalFrom M M.start x}
[PROOFSTEP]
exact fun h => ⟨M.eval x, h, rfl⟩