internlm/Lean-Github huggingface dataset:
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof state before:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
this : ∀ (x : α), ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
i : ι
hi : i ∈ J
⊢ LowerSemicontinuousWithinAt (f i) s a
Tactic:
exact hf i (Set.mem_insert_of_mem j hi)
Proof state after:
no goals
Theorem: UpperSemicontinuousOn.exists_iSup_of_isCompact
Proof state before:
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : UpperSemicontinuousOn f s
⊢ ∃ a ∈ s, f a = ⨆ x ∈ s, f x
Tactic:
apply LowerSemicontinuousOn.exists_iInf_of_isCompact (β := βᵒᵈ) ne_s hs hf
Proof state after:
no goals
Theorem: lowerSemicontinuousWithinAt_iSup₂
Proof state before:
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
⊢ LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ I, f i x) s a
Tactic:
intro t ht
Proof state after:
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
ht : t < (fun x => ⨆ i ∈ I, f i x) a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Theorem: lowerSemicontinuousWithinAt_iSup₂
Proof state before:
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
ht : t < (fun x => ⨆ i ∈ I, f i x) a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Tactic:
dsimp at ht
Proof state after:
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
ht : t < ⨆ i ∈ I, f i a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Theorem: lowerSemicontinuousWithinAt_iSup₂
Proof state before:
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
ht : t < ⨆ i ∈ I, f i a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Tactic:
obtain ⟨i, hi, hi'⟩ := hf'.exists_iSup_of_isCompact ne_I hI
Proof state after:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
ht : t < ⨆ i ∈ I, f i a
i : ι
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Theorem: lowerSemicontinuousWithinAt_iSup₂
Proof state before:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
ht : t < ⨆ i ∈ I, f i a
i : ι
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Tactic:
rw [← hi'] at ht
Proof state after:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Theorem: lowerSemicontinuousWithinAt_iSup₂
Proof state before:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Tactic:
let h := hf i hi t ht
Proof state after:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Theorem: lowerSemicontinuousWithinAt_iSup₂
Proof state before:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
Tactic:
dsimp
Proof state after:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < ⨆ i ∈ I, f i x'
Theorem: lowerSemicontinuousWithinAt_iSup₂
Proof state before:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < ⨆ i ∈ I, f i x'
Tactic:
apply Filter.Eventually.mp h
Proof state after:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ᶠ (x : α) in 𝓝[s] a, t < f i x → t < ⨆ i ∈ I, f i x
Theorem: lowerSemicontinuousWithinAt_iSup₂
Proof state before:
case intro.intro
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ᶠ (x : α) in 𝓝[s] a, t < f i x → t < ⨆ i ∈ I, f i x
Tactic:
apply Filter.eventually_of_forall
Proof state after:
case intro.intro.hp
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ (x : α), t < f i x → t < ⨆ i ∈ I, f i x
Theorem: lowerSemicontinuousWithinAt_iSup₂
Proof state before:
case intro.intro.hp
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
⊢ ∀ (x : α), t < f i x → t < ⨆ i ∈ I, f i x
Tactic:
intro x hx
Proof state after:
case intro.intro.hp
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
x : α
hx : t < f i x
⊢ t < ⨆ i ∈ I, f i x
Theorem: lowerSemicontinuousWithinAt_iSup₂
Proof state before:
case intro.intro.hp
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
x : α
hx : t < f i x
⊢ t < ⨆ i ∈ I, f i x
Tactic:
apply lt_of_lt_of_le hx
Proof state after:
case intro.intro.hp
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
x : α
hx : t < f i x
⊢ f i x ≤ ⨆ i ∈ I, f i x
Theorem: lowerSemicontinuousWithinAt_iSup₂
Proof state before:
case intro.intro.hp
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
i : ι
ht : t < f i a
hi : i ∈ I
hi' : f i a = ⨆ x ∈ I, f x a
h : ∀ᶠ (x' : α) in 𝓝[s] a, t < f i x' := hf i hi t ht
x : α
hx : t < f i x
⊢ f i x ≤ ⨆ i ∈ I, f i x
Tactic:
apply le_iSup₂ i hi
Proof state after:
no goals
Theorem: Groupoid.left_inv_cancel
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
⊢ g ⁻¹ ≫ g ≫ h = h
Tactic:
rw [← comp_assoc]
Proof state after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
⊢ (g ⁻¹ ≫ g) ≫ h = h
Theorem: Groupoid.left_inv_cancel
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
⊢ (g ⁻¹ ≫ g) ≫ h = h
Tactic:
simp
Proof state after:
no goals
Theorem: Groupoid.id_inv
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
⊢ (𝟙 X) ⁻¹ = 𝟙 X
Tactic:
have := left_inv_cancel (𝟙 X) (𝟙 X)
Proof state after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : (𝟙 X) ⁻¹ ≫ 𝟙 X ≫ 𝟙 X = 𝟙 X
⊢ (𝟙 X) ⁻¹ = 𝟙 X
Theorem: Groupoid.id_inv
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : (𝟙 X) ⁻¹ ≫ 𝟙 X ≫ 𝟙 X = 𝟙 X
⊢ (𝟙 X) ⁻¹ = 𝟙 X
Tactic:
rw [comp_id, comp_id] at this
Proof state after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : (𝟙 X) ⁻¹ = 𝟙 X
⊢ (𝟙 X) ⁻¹ = 𝟙 X
Theorem: Groupoid.id_inv
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : (𝟙 X) ⁻¹ = 𝟙 X
⊢ (𝟙 X) ⁻¹ = 𝟙 X
Tactic:
assumption
Proof state after:
no goals
Theorem: Groupoid.inv_inv
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
⊢ g ⁻¹ ⁻¹ = g
Tactic:
have := left_inv_cancel (g⁻¹) g
Proof state after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : g ⁻¹ ⁻¹ ≫ g ⁻¹ ≫ g = g
⊢ g ⁻¹ ⁻¹ = g
Theorem: Groupoid.inv_inv
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : g ⁻¹ ⁻¹ ≫ g ⁻¹ ≫ g = g
⊢ g ⁻¹ ⁻¹ = g
Tactic:
rw [inv_comp_id, comp_id] at this
Proof state after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : g ⁻¹ ⁻¹ = g
⊢ g ⁻¹ ⁻¹ = g
Theorem: Groupoid.inv_inv
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : g ⁻¹ ⁻¹ = g
⊢ g ⁻¹ ⁻¹ = g
Tactic:
assumption
Proof state after:
no goals
Theorem: Groupoid.left_cancel_inv
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h✝ h' : Y ⟶ Z
h : X ⟶ Z
⊢ g ≫ g ⁻¹ ≫ h = h
Tactic:
have := left_inv_cancel g⁻¹ h
Proof state after:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h✝ h' : Y ⟶ Z
h : X ⟶ Z
this : g ⁻¹ ⁻¹ ≫ g ⁻¹ ≫ h = h
⊢ g ≫ g ⁻¹ ≫ h = h
Theorem: Groupoid.left_cancel_inv
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h✝ h' : Y ⟶ Z
h : X ⟶ Z
this : g ⁻¹ ⁻¹ ≫ g ⁻¹ ≫ h = h
⊢ g ≫ g ⁻¹ ≫ h = h
Tactic:
rw [inv_inv] at this
Proof state after:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h✝ h' : Y ⟶ Z
h : X ⟶ Z
this : g ≫ g ⁻¹ ≫ h = h
⊢ g ≫ g ⁻¹ ≫ h = h
Theorem: Groupoid.left_cancel_inv
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h✝ h' : Y ⟶ Z
h : X ⟶ Z
this : g ≫ g ⁻¹ ≫ h = h
⊢ g ≫ g ⁻¹ ≫ h = h
Tactic:
assumption
Proof state after:
no goals
Theorem: Groupoid.inv_comp
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
⊢ (g ≫ h) ⁻¹ = h ⁻¹ ≫ g ⁻¹
Tactic:
have := left_cancel_inv (g ≫ h)⁻¹ (h⁻¹ ≫ g⁻¹)
Proof state after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : (g ≫ h) ⁻¹ ≫ (g ≫ h) ⁻¹ ⁻¹ ≫ h ⁻¹ ≫ g ⁻¹ = h ⁻¹ ≫ g ⁻¹
⊢ (g ≫ h) ⁻¹ = h ⁻¹ ≫ g ⁻¹
Theorem: Groupoid.inv_comp
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : (g ≫ h) ⁻¹ ≫ (g ≫ h) ⁻¹ ⁻¹ ≫ h ⁻¹ ≫ g ⁻¹ = h ⁻¹ ≫ g ⁻¹
⊢ (g ≫ h) ⁻¹ = h ⁻¹ ≫ g ⁻¹
Tactic:
simp at this
Proof state after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : (g ≫ h) ⁻¹ = h ⁻¹ ≫ g ⁻¹
⊢ (g ≫ h) ⁻¹ = h ⁻¹ ≫ g ⁻¹
Theorem: Groupoid.inv_comp
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : (g ≫ h) ⁻¹ = h ⁻¹ ≫ g ⁻¹
⊢ (g ≫ h) ⁻¹ = h ⁻¹ ≫ g ⁻¹
Tactic:
assumption
Proof state after:
no goals
Theorem: Groupoid.left_cancel
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
⊢ g ≫ h = g ≫ h' → h = h'
Tactic:
intro hyp
Proof state after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
hyp : g ≫ h = g ≫ h'
⊢ h = h'
Theorem: Groupoid.left_cancel
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
hyp : g ≫ h = g ≫ h'
this : (fun x => g ⁻¹ ≫ x) (g ≫ h) = (fun x => g ⁻¹ ≫ x) (g ≫ h')
⊢ h = h'
Tactic:
simp at this
Proof state after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
hyp : g ≫ h = g ≫ h'
this : h = h'
⊢ h = h'
Theorem: Groupoid.left_cancel
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
hyp : g ≫ h = g ≫ h'
this : h = h'
⊢ h = h'
Tactic:
assumption
Proof state after:
no goals
Theorem: Groupoid.right_cancel
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
⊢ g ≫ h = g' ≫ h → g = g'
Tactic:
intro hyp
Proof state after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
hyp : g ≫ h = g' ≫ h
⊢ g = g'
Theorem: Groupoid.right_cancel
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
hyp : g ≫ h = g' ≫ h
this : (fun x => x ≫ h ⁻¹ ) (g ≫ h) = (fun x => x ≫ h ⁻¹ ) (g' ≫ h)
⊢ g = g'
Tactic:
simp at this
Proof state after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
hyp : g ≫ h = g' ≫ h
this : g = g'
⊢ g = g'
Theorem: Groupoid.right_cancel
Proof state before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
hyp : g ≫ h = g' ≫ h
this : g = g'
⊢ g = g'
Tactic:
assumption
Proof state after:
no goals
Theorem: Groupoid.left_cancel_id
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : Y ⟶ Y
⊢ g = g ≫ e ↔ 𝟙 Y = e
Tactic:
have := left_cancel g (𝟙 _) e
Proof state after:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : Y ⟶ Y
this : g ≫ 𝟙 Y = g ≫ e ↔ 𝟙 Y = e
⊢ g = g ≫ e ↔ 𝟙 Y = e
Theorem: Groupoid.left_cancel_id
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : Y ⟶ Y
this : g ≫ 𝟙 Y = g ≫ e ↔ 𝟙 Y = e
⊢ g = g ≫ e ↔ 𝟙 Y = e
Tactic:
simp at this
Proof state after:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : Y ⟶ Y
this : g = g ≫ e ↔ 𝟙 Y = e
⊢ g = g ≫ e ↔ 𝟙 Y = e
Theorem: Groupoid.left_cancel_id
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : Y ⟶ Y
this : g = g ≫ e ↔ 𝟙 Y = e
⊢ g = g ≫ e ↔ 𝟙 Y = e
Tactic:
assumption
Proof state after:
no goals
Theorem: Groupoid.left_cancel_id'
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : Y ⟶ Y
⊢ g ≫ e = g ↔ e = 𝟙 Y
Tactic:
have := left_cancel g e (𝟙 Y)
Proof state after:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : Y ⟶ Y
this : g ≫ e = g ≫ 𝟙 Y ↔ e = 𝟙 Y
⊢ g ≫ e = g ↔ e = 𝟙 Y
Theorem: Groupoid.left_cancel_id'
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : Y ⟶ Y
this : g ≫ e = g ≫ 𝟙 Y ↔ e = 𝟙 Y
⊢ g ≫ e = g ↔ e = 𝟙 Y
Tactic:
simp at this
Proof state after:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : Y ⟶ Y
this : g ≫ e = g ↔ e = 𝟙 Y
⊢ g ≫ e = g ↔ e = 𝟙 Y
Theorem: Groupoid.left_cancel_id'
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : Y ⟶ Y
this : g ≫ e = g ↔ e = 𝟙 Y
⊢ g ≫ e = g ↔ e = 𝟙 Y
Tactic:
assumption
Proof state after:
no goals
Theorem: Groupoid.right_cancel_id
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
⊢ g = e ≫ g ↔ 𝟙 X = e
Tactic:
have := right_cancel (𝟙 X) e g
Proof state after:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
this : 𝟙 X ≫ g = e ≫ g ↔ 𝟙 X = e
⊢ g = e ≫ g ↔ 𝟙 X = e
Theorem: Groupoid.right_cancel_id
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
this : 𝟙 X ≫ g = e ≫ g ↔ 𝟙 X = e
⊢ g = e ≫ g ↔ 𝟙 X = e
Tactic:
simp at this
Proof state after:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
this : g = e ≫ g ↔ 𝟙 X = e
⊢ g = e ≫ g ↔ 𝟙 X = e
Theorem: Groupoid.right_cancel_id
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
this : g = e ≫ g ↔ 𝟙 X = e
⊢ g = e ≫ g ↔ 𝟙 X = e
Tactic:
assumption
Proof state after:
no goals
Theorem: Groupoid.right_cancel_id'
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
⊢ e ≫ g = g ↔ e = 𝟙 X
Tactic:
have := right_cancel e (𝟙 X) g
Proof state after:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
this : e ≫ g = 𝟙 X ≫ g ↔ e = 𝟙 X
⊢ e ≫ g = g ↔ e = 𝟙 X
Theorem: Groupoid.right_cancel_id'
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
this : e ≫ g = 𝟙 X ≫ g ↔ e = 𝟙 X
⊢ e ≫ g = g ↔ e = 𝟙 X
Tactic:
simp at this
Proof state after:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
this : e ≫ g = g ↔ e = 𝟙 X
⊢ e ≫ g = g ↔ e = 𝟙 X
Theorem: Groupoid.right_cancel_id'
Proof state before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
this : e ≫ g = g ↔ e = 𝟙 X
⊢ e ≫ g = g ↔ e = 𝟙 X
Tactic:
assumption
Proof state after:
no goals
Theorem: Groupoid.Functor.map_id'
Proof state before:
R : Sort ?u.16460
S : Sort u_3
T : Sort u_2
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X : S
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X) = 𝟙 (Quiver.PreFunctor.obj Φ.toFunctor.toPreFunctor X)
Tactic:
have := Φ.map_comp (𝟙 X) (𝟙 X)
Proof state after:
R : Sort ?u.16460
S : Sort u_3
T : Sort u_2
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X : S
this :
  Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X ≫ 𝟙 X) =
    Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X) ≫ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X)
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X) = 𝟙 (Quiver.PreFunctor.obj Φ.toFunctor.toPreFunctor X)
Theorem: Groupoid.Functor.map_id'
Proof state before:
R : Sort ?u.16460
S : Sort u_3
T : Sort u_2
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X : S
this :
  Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X ≫ 𝟙 X) =
    Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X) ≫ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X)
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X) = 𝟙 (Quiver.PreFunctor.obj Φ.toFunctor.toPreFunctor X)
Tactic:
rw [Category.comp_id, right_cancel_id] at this
Proof state after:
R : Sort ?u.16460
S : Sort u_3
T : Sort u_2
F : Groupoid R
G : Groupoid S
H : Groupoid T
Ψ : Functor F G
Φ : Functor G H
X : S
this : 𝟙 (Quiver.PreFunctor.obj Φ.toFunctor.toPreFunctor X) = Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X)
⊢ Quiver.PreFunctor.map Φ.toFunctor.toPreFunctor (𝟙 X) = 𝟙 (Quiver.PreFunctor.obj Φ.toFunctor.toPreFunctor X)