internlm/Lean-Github huggingface dataset:
Theorem: Tutorial.adjunction_of_Sup
Proof state before:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
a b : X
hab : a ≤ b
⊢ l a ≤ l b
Tactic:
have := h {a, b}
Proof state after:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
a b : X
hab : a ≤ b
this : l (Sup {a, b}) = Sup (l '' {a, b})
⊢ l a ≤ l b
Theorem: Tutorial.adjunction_of_Sup
Proof state before:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
a b : X
hab : a ≤ b
this : l (Sup {a, b}) = Sup (l '' {a, b})
⊢ l a ≤ l b
Tactic:
rw [Sup_pair.1 hab, Set.image_pair] at this
Proof state after:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
a b : X
hab : a ≤ b
this : l b = Sup {l a, l b}
⊢ l a ≤ l b
Theorem: Tutorial.adjunction_of_Sup
Proof state before:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
a b : X
hab : a ≤ b
this : l b = Sup {l a, l b}
⊢ l a ≤ l b
Tactic:
exact Sup_pair.2 this.symm
Proof state after:
no goals
Theorem: Tutorial.isOpen_empty
Proof state before:
X : Type
T : Topology X
⊢ Topology.isOpen T ∅
Tactic:
have : (∅ : Set X) = ⋃ i : Empty, i.rec
Proof state after:
case this
X : Type
T : Topology X
⊢ ∅ = ⋃ (i : Empty), Empty.rec (fun x => Set X) i

X : Type
T : Topology X
this : ∅ = ⋃ (i : Empty), Empty.rec (fun x => Set X) i
⊢ Topology.isOpen T ∅
Theorem: Tutorial.isOpen_empty
Proof state before:
X : Type
T : Topology X
this : ∅ = ⋃ (i : Empty), Empty.rec (fun x => Set X) i
⊢ Topology.isOpen T ∅
Tactic:
rw [this]
Proof state after:
X : Type
T : Topology X
this : ∅ = ⋃ (i : Empty), Empty.rec (fun x => Set X) i
⊢ Topology.isOpen T (⋃ (i : Empty), Empty.rec (fun x => Set X) i)
Theorem: Tutorial.isOpen_empty
Proof state before:
X : Type
T : Topology X
this : ∅ = ⋃ (i : Empty), Empty.rec (fun x => Set X) i
⊢ Topology.isOpen T (⋃ (i : Empty), Empty.rec (fun x => Set X) i)
Tactic:
exact T.isOpen_iUnion Empty.rec
Proof state after:
no goals
Theorem: Tutorial.isOpen_empty
Proof state before:
case this
X : Type
T : Topology X
⊢ ∅ = ⋃ (i : Empty), Empty.rec (fun x => Set X) i
Tactic:
rw [Set.iUnion_of_empty]
Proof state after:
no goals
Theorem: Tutorial.isOpen_univ
Proof state before:
X : Type
T : Topology X
⊢ Topology.isOpen T Set.univ
Tactic:
have : (Set.univ : Set X) = ⋂ i : Empty, i.rec
Proof state after:
case this
X : Type
T : Topology X
⊢ Set.univ = ⋂ (i : Empty), Empty.rec (fun x => Set X) i

X : Type
T : Topology X
this : Set.univ = ⋂ (i : Empty), Empty.rec (fun x => Set X) i
⊢ Topology.isOpen T Set.univ
Theorem: Tutorial.isOpen_univ
Proof state before:
X : Type
T : Topology X
this : Set.univ = ⋂ (i : Empty), Empty.rec (fun x => Set X) i
⊢ Topology.isOpen T Set.univ
Tactic:
rw [this]
Proof state after:
X : Type
T : Topology X
this : Set.univ = ⋂ (i : Empty), Empty.rec (fun x => Set X) i
⊢ Topology.isOpen T (⋂ (i : Empty), Empty.rec (fun x => Set X) i)
Theorem: Tutorial.isOpen_univ
Proof state before:
X : Type
T : Topology X
this : Set.univ = ⋂ (i : Empty), Empty.rec (fun x => Set X) i
⊢ Topology.isOpen T (⋂ (i : Empty), Empty.rec (fun x => Set X) i)
Tactic:
exact T.isOpen_iInter  Empty.rec (Finite.of_fintype Empty)
Proof state after:
no goals
Theorem: Tutorial.isOpen_univ
Proof state before:
case this
X : Type
T : Topology X
⊢ Set.univ = ⋂ (i : Empty), Empty.rec (fun x => Set X) i
Tactic:
rw [Set.iInter_of_empty]
Proof state after:
no goals
Theorem: Tutorial.push_push
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
T : Topology X
⊢ g⁎ (f⁎ T) = (g ∘ f)⁎ T
Tactic:
ext V
Proof state after:
case isOpen.h.a
X Y Z : Type
f : X → Y
g : Y → Z
T : Topology X
V : Set Z
⊢ Topology.isOpen (g⁎ (f⁎ T)) V ↔ Topology.isOpen ((g ∘ f)⁎ T) V
Theorem: Tutorial.push_push
Proof state before:
case isOpen.h.a
X Y Z : Type
f : X → Y
g : Y → Z
T : Topology X
V : Set Z
⊢ Topology.isOpen (g⁎ (f⁎ T)) V ↔ Topology.isOpen ((g ∘ f)⁎ T) V
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: Tutorial.push_Sup
Proof state before:
X Y : Type
f : X → Y
t : Set (Topology X)
⊢ f⁎ (Sup t) = Sup (f⁎ '' t)
Tactic:
ext V
Proof state after:
case isOpen.h.a
X Y : Type
f : X → Y
t : Set (Topology X)
V : Set Y
⊢ Topology.isOpen (f⁎ (Sup t)) V ↔ Topology.isOpen (Sup (f⁎ '' t)) V
Theorem: Tutorial.push_Sup
Proof state before:
case isOpen.h.a
X Y : Type
f : X → Y
t : Set (Topology X)
V : Set Y
⊢ Topology.isOpen (f⁎ (Sup t)) V ↔ Topology.isOpen (Sup (f⁎ '' t)) V
Tactic:
rw [isOpen_Sup, Set.ball_image_iff]
Proof state after:
case isOpen.h.a
X Y : Type
f : X → Y
t : Set (Topology X)
V : Set Y
⊢ Topology.isOpen (f⁎ (Sup t)) V ↔ ∀ x ∈ t, Topology.isOpen (f⁎ x) V
Theorem: Tutorial.push_Sup
Proof state before:
case isOpen.h.a
X Y : Type
f : X → Y
t : Set (Topology X)
V : Set Y
⊢ Topology.isOpen (f⁎ (Sup t)) V ↔ ∀ x ∈ t, Topology.isOpen (f⁎ x) V
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: Tutorial.ContinuousProductTopIff
Proof state before:
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
⊢ Continuous TZ (ProductTopology T) f ↔ ∀ (i : ι), Continuous TZ (T i) fun z => f z i
Tactic:
calc
  Continuous TZ (ProductTopology T) f
  _ ↔ f ⁎ TZ ∈ lowerBounds (Set.range (fun i ↦ (fun x ↦ x i) ^* (T i))) := by {
        rw [CompleteLattice.I_isInf]
        exact Iff.rfl
        }
  _ ↔ ∀ i, f ⁎ TZ ≤ (fun x ↦ x i) ^* (T i)        := by rw [lowerBounds_range]
  _ ↔ ∀ i, (fun x ↦ x i) ⁎ (f ⁎ TZ) ≤ T i        := by {
        apply forall_congr'
        intro i
        rw [pull, ← adjunction_of_Sup (fun s ↦ push_Sup _), push_push]
        }
  _ ↔ ∀ i,  Continuous TZ (T i) (fun z ↦ f z i)  := Iff.rfl
Proof state after:
no goals
Theorem: Tutorial.ContinuousProductTopIff
Proof state before:
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
⊢ Continuous TZ (ProductTopology T) f ↔ f⁎ TZ ∈ lowerBounds (Set.range fun i => (fun x => x i)^* (T i))
Tactic:
rw [CompleteLattice.I_isInf]
Proof state after:
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
⊢ Continuous TZ (ProductTopology T) f ↔ f⁎ TZ ≤ Inf (Set.range fun i => (fun x => x i)^* (T i))
Theorem: Tutorial.ContinuousProductTopIff
Proof state before:
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
⊢ Continuous TZ (ProductTopology T) f ↔ f⁎ TZ ≤ Inf (Set.range fun i => (fun x => x i)^* (T i))
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: Tutorial.ContinuousProductTopIff
Proof state before:
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
⊢ f⁎ TZ ∈ lowerBounds (Set.range fun i => (fun x => x i)^* (T i)) ↔ ∀ (i : ι), f⁎ TZ ≤ (fun x => x i)^* (T i)
Tactic:
rw [lowerBounds_range]
Proof state after:
no goals
Theorem: Tutorial.ContinuousProductTopIff
Proof state before:
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
⊢ (∀ (i : ι), f⁎ TZ ≤ (fun x => x i)^* (T i)) ↔ ∀ (i : ι), (fun x => x i)⁎ (f⁎ TZ) ≤ T i
Tactic:
apply forall_congr'
Proof state after:
case h
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
⊢ ∀ (a : ι), f⁎ TZ ≤ (fun x => x a)^* (T a) ↔ (fun x => x a)⁎ (f⁎ TZ) ≤ T a
Theorem: Tutorial.ContinuousProductTopIff
Proof state before:
case h
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
⊢ ∀ (a : ι), f⁎ TZ ≤ (fun x => x a)^* (T a) ↔ (fun x => x a)⁎ (f⁎ TZ) ≤ T a
Tactic:
intro i
Proof state after:
case h
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
i : ι
⊢ f⁎ TZ ≤ (fun x => x i)^* (T i) ↔ (fun x => x i)⁎ (f⁎ TZ) ≤ T i
Theorem: Tutorial.ContinuousProductTopIff
Proof state before:
case h
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
i : ι
⊢ f⁎ TZ ≤ (fun x => x i)^* (T i) ↔ (fun x => x i)⁎ (f⁎ TZ) ≤ T i
Tactic:
rw [pull, ← adjunction_of_Sup (fun s ↦ push_Sup _), push_push]
Proof state after:
no goals
Theorem: Tutorial.Subgroups.SubgroupInf_carrier
Proof state before:
G : Type
inst✝ : Group G
s : Set (Subgroup G)
⊢ (SubgroupInf s).carrier = ⋂₀ (Subgroup.carrier '' s)
Tactic:
simp [SubgroupInf]
Proof state after:
no goals
Theorem: Tutorial.Subgroups.isInf.lift
Proof state before:
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
⊢ isInf s y
Tactic:
intro y'
Proof state after:
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
⊢ y' ∈ lowerBounds s ↔ y' ≤ y
Theorem: Tutorial.Subgroups.isInf.lift
Proof state before:
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
⊢ y' ∈ lowerBounds s ↔ y' ≤ y
Tactic:
erw [← hy (f y')]
Proof state after:
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
⊢ y' ∈ lowerBounds s ↔ f y' ∈ lowerBounds (f '' s)
Theorem: Tutorial.Subgroups.isInf.lift
Proof state before:
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
⊢ y' ∈ lowerBounds s ↔ f y' ∈ lowerBounds (f '' s)
Tactic:
constructor
Proof state after:
case mp
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
⊢ y' ∈ lowerBounds s → f y' ∈ lowerBounds (f '' s)

case mpr
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
⊢ f y' ∈ lowerBounds (f '' s) → y' ∈ lowerBounds s
Theorem: Tutorial.Subgroups.isInf.lift
Proof state before:
case mp
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
⊢ y' ∈ lowerBounds s → f y' ∈ lowerBounds (f '' s)
Tactic:
intro hy' x hx
Proof state after:
case mp
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
hy' : y' ∈ lowerBounds s
x : X
hx : x ∈ f '' s
⊢ f y' ≤ x
Theorem: Tutorial.Subgroups.isInf.lift
Proof state before:
case mp
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
hy' : y' ∈ lowerBounds s
x : X
hx : x ∈ f '' s
⊢ f y' ≤ x
Tactic:
rcases hx with ⟨y'', hy'', H⟩
Proof state after:
case mp.intro.intro
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
hy' : y' ∈ lowerBounds s
x : X
y'' : Y
hy'' : y'' ∈ s
H : f y'' = x
⊢ f y' ≤ x
Theorem: Tutorial.Subgroups.isInf.lift
Proof state before:
case mp.intro.intro
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
hy' : y' ∈ lowerBounds s
x : X
y'' : Y
hy'' : y'' ∈ s
H : f y'' = x
⊢ f y' ≤ x
Tactic:
rw [← H]
Proof state after:
case mp.intro.intro
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
hy' : y' ∈ lowerBounds s
x : X
y'' : Y
hy'' : y'' ∈ s
H : f y'' = x
⊢ f y' ≤ f y''
Theorem: Tutorial.Subgroups.isInf.lift
Proof state before:
case mp.intro.intro
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
hy' : y' ∈ lowerBounds s
x : X
y'' : Y
hy'' : y'' ∈ s
H : f y'' = x
⊢ f y' ≤ f y''
Tactic:
exact hy' hy''
Proof state after:
no goals
Theorem: Tutorial.Subgroups.isInf.lift
Proof state before:
case mpr
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
⊢ f y' ∈ lowerBounds (f '' s) → y' ∈ lowerBounds s
Tactic:
intro hy' y'' hy''
Proof state after:
case mpr
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
hy' : f y' ∈ lowerBounds (f '' s)
y'' : Y
hy'' : y'' ∈ s
⊢ y' ≤ y''
Theorem: Tutorial.Subgroups.isInf.lift
Proof state before:
case mpr
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
hy' : f y' ∈ lowerBounds (f '' s)
y'' : Y
hy'' : y'' ∈ s
⊢ y' ≤ y''
Tactic:
apply hy'
Proof state after:
case mpr.a
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
hy' : f y' ∈ lowerBounds (f '' s)
y'' : Y
hy'' : y'' ∈ s
⊢ f y'' ∈ f '' s
Theorem: Tutorial.Subgroups.isInf.lift
Proof state before:
case mpr.a
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
hy' : f y' ∈ lowerBounds (f '' s)
y'' : Y
hy'' : y'' ∈ s
⊢ f y'' ∈ f '' s
Tactic:
exact Set.mem_image_of_mem f hy''
Proof state after:
no goals
Theorem: Tutorial.Subgroups.SubgroupInf_is_Inf
Proof state before:
G : Type
inst✝ : Group G
⊢ isInfFun SubgroupInf
Tactic:
intro s H
Proof state after:
G : Type
inst✝ : Group G
s : Set (Subgroup G)
H : Subgroup G
⊢ H ∈ lowerBounds s ↔ H ≤ SubgroupInf s
Theorem: Tutorial.Subgroups.SubgroupInf_is_Inf
Proof state before:
G : Type
inst✝ : Group G
s : Set (Subgroup G)
H : Subgroup G
⊢ H ∈ lowerBounds s ↔ H ≤ SubgroupInf s
Tactic:
apply isInf.lift (fun H H' ↦ (Subgroup.ext_iff H H').2)
Proof state after:
case hy
G : Type
inst✝ : Group G
s : Set (Subgroup G)
H : Subgroup G
⊢ isInf ((fun H => H.carrier) '' s) (SubgroupInf s).carrier
Theorem: Tutorial.Subgroups.SubgroupInf_is_Inf
Proof state before:
case hy
G : Type
inst✝ : Group G
s : Set (Subgroup G)
H : Subgroup G
⊢ isInf ((fun H => H.carrier) '' s) (SubgroupInf s).carrier
Tactic:
rw [SubgroupInf_carrier]
Proof state after:
case hy
G : Type
inst✝ : Group G
s : Set (Subgroup G)
H : Subgroup G
⊢ isInf ((fun H => H.carrier) '' s) (⋂₀ (Subgroup.carrier '' s))
Theorem: Tutorial.Subgroups.SubgroupInf_is_Inf
Proof state before:
case hy
G : Type
inst✝ : Group G
s : Set (Subgroup G)
H : Subgroup G
⊢ isInf ((fun H => H.carrier) '' s) (⋂₀ (Subgroup.carrier '' s))
Tactic:
apply isInfInter
Proof state after:
no goals
Theorem: Tutorial.Subgroups.generate_forget_adjunction
Proof state before:
G : Type
inst✝ : Group G
⊢ adjunction generate forget
Tactic:
exact adjunction_of_Inf SubgroupInf_carrier
Proof state after:
no goals
Theorem: Tutorial.Subgroups.push_pull_adjunction
Proof state before:
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (push f) (pull f)
Tactic:
apply adjunction_of_Inf
Proof state after:
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ∀ (s : Set (Subgroup G')), pull f (Inf s) = Inf (pull f '' s)
Theorem: Tutorial.Subgroups.push_pull_adjunction
Proof state before:
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ∀ (s : Set (Subgroup G')), pull f (Inf s) = Inf (pull f '' s)
Tactic:
intro S
Proof state after:
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
S : Set (Subgroup G')
⊢ pull f (Inf S) = Inf (pull f '' S)
Theorem: Tutorial.Subgroups.push_pull_adjunction
Proof state before:
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
S : Set (Subgroup G')
⊢ pull f (Inf S) = Inf (pull f '' S)
Tactic:
ext x
Proof state after:
case h.carrier.h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
S : Set (Subgroup G')
x : G
⊢ x ∈ (pull f (Inf S)).carrier ↔ x ∈ (Inf (pull f '' S)).carrier
Theorem: Tutorial.Subgroups.push_pull_adjunction
Proof state before:
case h.carrier.h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
S : Set (Subgroup G')
x : G
⊢ x ∈ (pull f (Inf S)).carrier ↔ x ∈ (Inf (pull f '' S)).carrier
Tactic:
simp [Inf_carrier, Set.image_image, pull, Set.preimage_iInter]
Proof state after:
no goals
Theorem: Tutorial.unique_left
Proof state before:
X : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
Y : Type
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l l' : X → Y
r : Y → X
h : adjunction l r
h' : adjunction l' r
⊢ l = l'
Tactic:
ext x
Proof state after:
case h
X : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
Y : Type
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l l' : X → Y
r : Y → X
h : adjunction l r
h' : adjunction l' r
x : X
⊢ l x = l' x
Theorem: Tutorial.unique_left
Proof state before:
case h
X : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
Y : Type
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l l' : X → Y
r : Y → X
h : adjunction l r
h' : adjunction l' r
x : X
⊢ l x = l' x
Tactic:
apply le_antisymm
Proof state after:
case h.a
X : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
Y : Type
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l l' : X → Y
r : Y → X
h : adjunction l r
h' : adjunction l' r
x : X
⊢ l x ≤ l' x

case h.a
X : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
Y : Type
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l l' : X → Y
r : Y → X
h : adjunction l r
h' : adjunction l' r
x : X
⊢ l' x ≤ l x
Theorem: Tutorial.unique_left
Proof state before:
case h.a
X : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
Y : Type
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l l' : X → Y
r : Y → X
h : adjunction l r
h' : adjunction l' r
x : X
⊢ l x ≤ l' x
Tactic:
rw [h, ← h']
Proof state after:
no goals
Theorem: Tutorial.unique_left
Proof state before:
case h.a
X : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
Y : Type
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l l' : X → Y
r : Y → X
h : adjunction l r
h' : adjunction l' r
x : X
⊢ l' x ≤ l x
Tactic:
rw [h', ← h]
Proof state after:
no goals
Theorem: Tutorial.unique_right
Proof state before:
X : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
Y : Type
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
r r' : Y → X
h : adjunction l r
h' : adjunction l r'
⊢ r = r'
Tactic:
exact (unique_left h'.dual h.dual).symm
Proof state after:
no goals
Theorem: Tutorial.adjunction.compose
Proof state before:
X : Type
inst✝⁵ : PartialOrder X
inst✝⁴ : CompleteLattice X
Y : Type
inst✝³ : PartialOrder Y
inst✝² : CompleteLattice Y
Z : Type
inst✝¹ : PartialOrder Z
inst✝ : CompleteLattice Z
l : X → Y
r : Y → X
h : adjunction l r
l' : Y → Z
r' : Z → Y
h' : adjunction l' r'
⊢ adjunction (l' ∘ l) (r ∘ r')
Tactic:
intro x z
Proof state after:
X : Type
inst✝⁵ : PartialOrder X
inst✝⁴ : CompleteLattice X
Y : Type
inst✝³ : PartialOrder Y
inst✝² : CompleteLattice Y
Z : Type
inst✝¹ : PartialOrder Z
inst✝ : CompleteLattice Z
l : X → Y
r : Y → X
h : adjunction l r
l' : Y → Z
r' : Z → Y
h' : adjunction l' r'
x : X
z : Z
⊢ (l' ∘ l) x ≤ z ↔ x ≤ (r ∘ r') z
Theorem: Tutorial.adjunction.compose
Proof state before:
X : Type
inst✝⁵ : PartialOrder X
inst✝⁴ : CompleteLattice X
Y : Type
inst✝³ : PartialOrder Y
inst✝² : CompleteLattice Y
Z : Type
inst✝¹ : PartialOrder Z
inst✝ : CompleteLattice Z
l : X → Y
r : Y → X
h : adjunction l r
l' : Y → Z
r' : Z → Y
h' : adjunction l' r'
x : X
z : Z
⊢ (l' ∘ l) x ≤ z ↔ x ≤ (r ∘ r') z
Tactic:
rw [Function.comp_apply, h', h]
Proof state after:
X : Type
inst✝⁵ : PartialOrder X
inst✝⁴ : CompleteLattice X
Y : Type
inst✝³ : PartialOrder Y
inst✝² : CompleteLattice Y
Z : Type
inst✝¹ : PartialOrder Z
inst✝ : CompleteLattice Z
l : X → Y
r : Y → X
h : adjunction l r
l' : Y → Z
r' : Z → Y
h' : adjunction l' r'
x : X
z : Z
⊢ x ≤ r (r' z) ↔ x ≤ (r ∘ r') z
Theorem: Tutorial.adjunction.compose
Proof state before:
X : Type
inst✝⁵ : PartialOrder X
inst✝⁴ : CompleteLattice X
Y : Type
inst✝³ : PartialOrder Y
inst✝² : CompleteLattice Y
Z : Type
inst✝¹ : PartialOrder Z
inst✝ : CompleteLattice Z
l : X → Y
r : Y → X
h : adjunction l r
l' : Y → Z
r' : Z → Y
h' : adjunction l' r'
x : X
z : Z
⊢ x ≤ r (r' z) ↔ x ≤ (r ∘ r') z
Tactic:
rfl
Proof state after:
no goals
Theorem: Tutorial.left_comm_of_right_comm
Proof state before:
X : Type
inst✝⁷ : PartialOrder X
inst✝⁶ : CompleteLattice X
Y : Type
inst✝⁵ : PartialOrder Y
inst✝⁴ : CompleteLattice Y
Z✝ : Type
inst✝³ : PartialOrder Z✝
inst✝² : CompleteLattice Z✝
W : Type
inst✝¹ : PartialOrder W
Z : Type
inst✝ : PartialOrder Z
lYX : X → Y
uXY : Y → X
hXY : adjunction lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : adjunction lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : adjunction lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : adjunction lZX uXZ
h : uXZ ∘ uZW = uXY ∘ uYW
⊢ lWZ ∘ lZX = lWY ∘ lYX
Tactic:
have A₁
Proof state after:
case A₁
X : Type
inst✝⁷ : PartialOrder X
inst✝⁶ : CompleteLattice X
Y : Type
inst✝⁵ : PartialOrder Y
inst✝⁴ : CompleteLattice Y
Z✝ : Type
inst✝³ : PartialOrder Z✝
inst✝² : CompleteLattice Z✝
W : Type
inst✝¹ : PartialOrder W
Z : Type
inst✝ : PartialOrder Z
lYX : X → Y
uXY : Y → X
hXY : adjunction lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : adjunction lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : adjunction lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : adjunction lZX uXZ
h : uXZ ∘ uZW = uXY ∘ uYW
⊢ ?m.150838

X : Type
inst✝⁷ : PartialOrder X
inst✝⁶ : CompleteLattice X
Y : Type
inst✝⁵ : PartialOrder Y
inst✝⁴ : CompleteLattice Y
Z✝ : Type
inst✝³ : PartialOrder Z✝
inst✝² : CompleteLattice Z✝
W : Type
inst✝¹ : PartialOrder W
Z : Type
inst✝ : PartialOrder Z
lYX : X → Y
uXY : Y → X
hXY : adjunction lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : adjunction lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : adjunction lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : adjunction lZX uXZ
h : uXZ ∘ uZW = uXY ∘ uYW
A₁ : ?m.150838
⊢ lWZ ∘ lZX = lWY ∘ lYX
Theorem: Tutorial.left_comm_of_right_comm
Proof state before:
X : Type
inst✝⁷ : PartialOrder X
inst✝⁶ : CompleteLattice X
Y : Type
inst✝⁵ : PartialOrder Y
inst✝⁴ : CompleteLattice Y
Z✝ : Type
inst✝³ : PartialOrder Z✝
inst✝² : CompleteLattice Z✝
W : Type
inst✝¹ : PartialOrder W
Z : Type
inst✝ : PartialOrder Z
lYX : X → Y
uXY : Y → X
hXY : adjunction lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : adjunction lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : adjunction lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : adjunction lZX uXZ
h : uXZ ∘ uZW = uXY ∘ uYW
A₁ : adjunction (lWZ ∘ lZX) (uXZ ∘ uZW)
⊢ lWZ ∘ lZX = lWY ∘ lYX
Tactic:
rw [h] at A₁
Proof state after:
X : Type
inst✝⁷ : PartialOrder X
inst✝⁶ : CompleteLattice X
Y : Type
inst✝⁵ : PartialOrder Y
inst✝⁴ : CompleteLattice Y
Z✝ : Type
inst✝³ : PartialOrder Z✝
inst✝² : CompleteLattice Z✝
W : Type
inst✝¹ : PartialOrder W
Z : Type
inst✝ : PartialOrder Z
lYX : X → Y
uXY : Y → X
hXY : adjunction lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : adjunction lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : adjunction lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : adjunction lZX uXZ
h : uXZ ∘ uZW = uXY ∘ uYW
A₁ : adjunction (lWZ ∘ lZX) (uXY ∘ uYW)
⊢ lWZ ∘ lZX = lWY ∘ lYX