internlm/Lean-Github huggingface dataset:
Theorem: BishopFin.count_eq_count_invimage_of_inv
Proof state before:
case refine_1
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
g : α → β
hgf : ∀ (b : β), g (f b) = b
hfg : ∀ (a : α), f (g a) = a
⊢ ∀ (a : α), ∃ b, f b = a

case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
g : α → β
hgf : ∀ (b : β), g (f b) = b
hfg : ∀ (a : α), f (g a) = a
⊢ ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
Tactic:
. exact fun a => ⟨g a, hfg a⟩
Proof state after:
case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
g : α → β
hgf : ∀ (b : β), g (f b) = b
hfg : ∀ (a : α), f (g a) = a
⊢ ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
Theorem: BishopFin.count_eq_count_invimage_of_inv
Proof state before:
case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
g : α → β
hgf : ∀ (b : β), g (f b) = b
hfg : ∀ (a : α), f (g a) = a
⊢ ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
Tactic:
. intro b₁ b₂ hb
  rw [← hgf b₁, ← hgf b₂, hb]
Proof state after:
no goals
Theorem: BishopFin.count_eq_count_invimage_of_inv
Proof state before:
case refine_1
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
g : α → β
hgf : ∀ (b : β), g (f b) = b
hfg : ∀ (a : α), f (g a) = a
⊢ ∀ (a : α), ∃ b, f b = a
Tactic:
exact fun a => ⟨g a, hfg a⟩
Proof state after:
no goals
Theorem: BishopFin.count_eq_count_invimage_of_inv
Proof state before:
case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
g : α → β
hgf : ∀ (b : β), g (f b) = b
hfg : ∀ (a : α), f (g a) = a
⊢ ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
Tactic:
intro b₁ b₂ hb
Proof state after:
case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
g : α → β
hgf : ∀ (b : β), g (f b) = b
hfg : ∀ (a : α), f (g a) = a
b₁ b₂ : β
hb : f b₁ = f b₂
⊢ b₁ = b₂
Theorem: BishopFin.count_eq_count_invimage_of_inv
Proof state before:
case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
g : α → β
hgf : ∀ (b : β), g (f b) = b
hfg : ∀ (a : α), f (g a) = a
b₁ b₂ : β
hb : f b₁ = f b₂
⊢ b₁ = b₂
Tactic:
rw [← hgf b₁, ← hgf b₂, hb]
Proof state after:
no goals
Theorem: barber_paradox
Proof state before:
person : Type
shaves : person → person → Prop
h : ∃ b, ∀ (p : person), shaves b p ↔ ¬shaves p p
⊢ False
Tactic:
duper [*] {preprocessing := no_preprocessing, inhabitationReasoning := true}
Proof state after:
no goals
Theorem: Tutorial.isInf.lowerBound
Proof state before:
X : Type u_1
inst✝ : PartialOrder X
s : Set X
x₀ : X
h : isInf s x₀
⊢ x₀ ∈ lowerBounds s
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Tutorial.isSup_of_isInf
Proof state before:
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
⊢ isSupFun fun s => I (upperBounds s)
Tactic:
intro s x
Proof state after:
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ x ∈ upperBounds s ↔ (fun s => I (upperBounds s)) s ≤ x
Theorem: Tutorial.isSup_of_isInf
Proof state before:
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ x ∈ upperBounds s ↔ (fun s => I (upperBounds s)) s ≤ x
Tactic:
constructor
Proof state after:
case mp
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ x ∈ upperBounds s → (fun s => I (upperBounds s)) s ≤ x

case mpr
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ (fun s => I (upperBounds s)) s ≤ x → x ∈ upperBounds s
Theorem: Tutorial.isSup_of_isInf
Proof state before:
case mp
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ x ∈ upperBounds s → (fun s => I (upperBounds s)) s ≤ x
Tactic:
intro hx
Proof state after:
case mp
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
hx : x ∈ upperBounds s
⊢ (fun s => I (upperBounds s)) s ≤ x
Theorem: Tutorial.isSup_of_isInf
Proof state before:
case mp
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
hx : x ∈ upperBounds s
⊢ (fun s => I (upperBounds s)) s ≤ x
Tactic:
exact (h _).lowerBound hx
Proof state after:
no goals
Theorem: Tutorial.isSup_of_isInf
Proof state before:
case mpr
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ (fun s => I (upperBounds s)) s ≤ x → x ∈ upperBounds s
Tactic:
intros hx y hy
Proof state after:
case mpr
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
hx : (fun s => I (upperBounds s)) s ≤ x
y : X
hy : y ∈ s
⊢ y ≤ x
Theorem: Tutorial.isSup_of_isInf
Proof state before:
case mpr
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
hx : (fun s => I (upperBounds s)) s ≤ x
y : X
hy : y ∈ s
⊢ y ≤ x
Tactic:
calc
  y ≤ I (upperBounds s) := (h _ y).mp (fun z hz ↦ hz hy)
  _ ≤ x                 := hx
Proof state after:
no goals
Theorem: Tutorial.Inf_subset
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ≤ Inf s
Tactic:
apply (CompleteLattice.I_isInf s _).1
Proof state after:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ∈ lowerBounds s
Theorem: Tutorial.Inf_subset
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ∈ lowerBounds s
Tactic:
apply lowerBounds_mono_set h
Proof state after:
case a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ∈ lowerBounds t
Theorem: Tutorial.Inf_subset
Proof state before:
case a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ∈ lowerBounds t
Tactic:
exact lowerBound_Inf t
Proof state after:
no goals
Theorem: Tutorial.Inf_pair
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' ↔ Inf {x, x'} = x
Tactic:
constructor
Proof state after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' → Inf {x, x'} = x

case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ Inf {x, x'} = x → x ≤ x'
Theorem: Tutorial.Inf_pair
Proof state before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' → Inf {x, x'} = x
Tactic:
intro h
Proof state after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
⊢ Inf {x, x'} = x
Theorem: Tutorial.Inf_pair
Proof state before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
⊢ Inf {x, x'} = x
Tactic:
apply (CompleteLattice.I_isInf _).eq
Proof state after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
⊢ isInf {x, x'} x
Theorem: Tutorial.Inf_pair
Proof state before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
⊢ isInf {x, x'} x
Tactic:
intro z
Proof state after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
⊢ z ∈ lowerBounds {x, x'} ↔ z ≤ x
Theorem: Tutorial.Inf_pair
Proof state before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
⊢ z ∈ lowerBounds {x, x'} ↔ z ≤ x
Tactic:
constructor
Proof state after:
case mp.mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
⊢ z ∈ lowerBounds {x, x'} → z ≤ x

case mp.mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
⊢ z ≤ x → z ∈ lowerBounds {x, x'}
Theorem: Tutorial.Inf_pair
Proof state before:
case mp.mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
⊢ z ∈ lowerBounds {x, x'} → z ≤ x
Tactic:
intro hz
Proof state after:
case mp.mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
hz : z ∈ lowerBounds {x, x'}
⊢ z ≤ x
Theorem: Tutorial.Inf_pair
Proof state before:
case mp.mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
hz : z ∈ lowerBounds {x, x'}
⊢ z ≤ x
Tactic:
apply hz
Proof state after:
case mp.mp.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
hz : z ∈ lowerBounds {x, x'}
⊢ x ∈ {x, x'}
Theorem: Tutorial.Inf_pair
Proof state before:
case mp.mp.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
hz : z ∈ lowerBounds {x, x'}
⊢ x ∈ {x, x'}
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.Inf_pair
Proof state before:
case mp.mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
⊢ z ≤ x → z ∈ lowerBounds {x, x'}
Tactic:
intro hz
Proof state after:
case mp.mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
hz : z ≤ x
⊢ z ∈ lowerBounds {x, x'}
Theorem: Tutorial.Inf_pair
Proof state before:
case mp.mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
hz : z ≤ x
⊢ z ∈ lowerBounds {x, x'}
Tactic:
simp [hz, hz.trans h]
Proof state after:
no goals
Theorem: Tutorial.Inf_pair
Proof state before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ Inf {x, x'} = x → x ≤ x'
Tactic:
intro h
Proof state after:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : Inf {x, x'} = x
⊢ x ≤ x'
Theorem: Tutorial.Inf_pair
Proof state before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : Inf {x, x'} = x
⊢ x ≤ x'
Tactic:
rw [← h]
Proof state after:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : Inf {x, x'} = x
⊢ Inf {x, x'} ≤ x'
Theorem: Tutorial.Inf_pair
Proof state before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : Inf {x, x'} = x
⊢ Inf {x, x'} ≤ x'
Tactic:
apply lowerBound_Inf
Proof state after:
case mpr.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : Inf {x, x'} = x
⊢ x' ∈ {x, x'}
Theorem: Tutorial.Inf_pair
Proof state before:
case mpr.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : Inf {x, x'} = x
⊢ x' ∈ {x, x'}
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.Sup_pair
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' ↔ Sup {x, x'} = x'
Tactic:
rw [Set.pair_comm x x']
Proof state after:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' ↔ Sup {x', x} = x'
Theorem: Tutorial.Sup_pair
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' ↔ Sup {x', x} = x'
Tactic:
exact Inf_pair (X := OrderDual X)
Proof state after:
no goals
Theorem: Tutorial.Inf_self_le
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x : X
⊢ Inf {x' | x ≤ x'} = x
Tactic:
apply (CompleteLattice.I_isInf _).eq
Proof state after:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x : X
⊢ isInf {x' | x ≤ x'} x
Theorem: Tutorial.Inf_self_le
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x : X
⊢ isInf {x' | x ≤ x'} x
Tactic:
intro x'
Proof state after:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ∈ lowerBounds {x' | x ≤ x'} ↔ x' ≤ x
Theorem: Tutorial.Inf_self_le
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ∈ lowerBounds {x' | x ≤ x'} ↔ x' ≤ x
Tactic:
constructor
Proof state after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ∈ lowerBounds {x' | x ≤ x'} → x' ≤ x

case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ≤ x → x' ∈ lowerBounds {x' | x ≤ x'}
Theorem: Tutorial.Inf_self_le
Proof state before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ∈ lowerBounds {x' | x ≤ x'} → x' ≤ x
Tactic:
intro h
Proof state after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x' ∈ lowerBounds {x' | x ≤ x'}
⊢ x' ≤ x
Theorem: Tutorial.Inf_self_le
Proof state before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x' ∈ lowerBounds {x' | x ≤ x'}
⊢ x' ≤ x
Tactic:
exact h le_rfl
Proof state after:
no goals
Theorem: Tutorial.Inf_self_le
Proof state before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ≤ x → x' ∈ lowerBounds {x' | x ≤ x'}
Tactic:
intro h x'' hx''
Proof state after:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x' ≤ x
x'' : X
hx'' : x'' ∈ {x' | x ≤ x'}
⊢ x' ≤ x''
Theorem: Tutorial.Inf_self_le
Proof state before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x' ≤ x
x'' : X
hx'' : x'' ∈ {x' | x ≤ x'}
⊢ x' ≤ x''
Tactic:
exact h.trans hx''
Proof state after:
no goals
Theorem: Tutorial.isInfInter
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
⊢ isInf S (⋂₀ S)
Tactic:
intro t
Proof state after:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ lowerBounds S ↔ t ≤ ⋂₀ S
Theorem: Tutorial.isInfInter
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ lowerBounds S ↔ t ≤ ⋂₀ S
Tactic:
constructor
Proof state after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ lowerBounds S → t ≤ ⋂₀ S

case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ≤ ⋂₀ S → t ∈ lowerBounds S
Theorem: Tutorial.isInfInter
Proof state before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ lowerBounds S → t ≤ ⋂₀ S
Tactic:
intro ht x hx u hu
Proof state after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ∈ lowerBounds S
x : Y
hx : x ∈ t
u : Set Y
hu : u ∈ S
⊢ x ∈ u
Theorem: Tutorial.isInfInter
Proof state before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ∈ lowerBounds S
x : Y
hx : x ∈ t
u : Set Y
hu : u ∈ S
⊢ x ∈ u
Tactic:
exact ht hu hx
Proof state after:
no goals
Theorem: Tutorial.isInfInter
Proof state before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ≤ ⋂₀ S → t ∈ lowerBounds S
Tactic:
intro ht u hu x hx
Proof state after:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ≤ ⋂₀ S
u : Set Y
hu : u ∈ S
x : Y
hx : x ∈ t
⊢ x ∈ u
Theorem: Tutorial.isInfInter
Proof state before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ≤ ⋂₀ S
u : Set Y
hu : u ∈ S
x : Y
hx : x ∈ t
⊢ x ∈ u
Tactic:
exact ht hx _ hu
Proof state after:
no goals
Theorem: Tutorial.isSupUnion
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
⊢ isSup S (⋃₀ S)
Tactic:
intro t
Proof state after:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ upperBounds S ↔ ⋃₀ S ≤ t
Theorem: Tutorial.isSupUnion
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ upperBounds S ↔ ⋃₀ S ≤ t
Tactic:
constructor
Proof state after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ upperBounds S → ⋃₀ S ≤ t

case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ ⋃₀ S ≤ t → t ∈ upperBounds S
Theorem: Tutorial.isSupUnion
Proof state before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ upperBounds S → ⋃₀ S ≤ t
Tactic:
intro ht x hx
Proof state after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ∈ upperBounds S
x : Y
hx : x ∈ ⋃₀ S
⊢ x ∈ t
Theorem: Tutorial.isSupUnion
Proof state before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ∈ upperBounds S
x : Y
hx : x ∈ ⋃₀ S
⊢ x ∈ t
Tactic:
rcases hx with ⟨s, hs, hx⟩
Proof state after:
case mp.intro.intro
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ∈ upperBounds S
x : Y
s : Set Y
hs : s ∈ S
hx : x ∈ s
⊢ x ∈ t
Theorem: Tutorial.isSupUnion
Proof state before:
case mp.intro.intro
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ∈ upperBounds S
x : Y
s : Set Y
hs : s ∈ S
hx : x ∈ s
⊢ x ∈ t
Tactic:
exact ht hs hx
Proof state after:
no goals
Theorem: Tutorial.isSupUnion
Proof state before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ ⋃₀ S ≤ t → t ∈ upperBounds S
Tactic:
intro ht u hu x hx
Proof state after:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : ⋃₀ S ≤ t
u : Set Y
hu : u ∈ S
x : Y
hx : x ∈ u
⊢ x ∈ t
Theorem: Tutorial.isSupUnion
Proof state before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : ⋃₀ S ≤ t
u : Set Y
hu : u ∈ S
x : Y
hx : x ∈ u
⊢ x ∈ t
Tactic:
apply ht
Proof state after:
case mpr.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : ⋃₀ S ≤ t
u : Set Y
hu : u ∈ S
x : Y
hx : x ∈ u
⊢ x ∈ ⋃₀ S
Theorem: Tutorial.isSupUnion
Proof state before:
case mpr.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : ⋃₀ S ≤ t
u : Set Y
hu : u ∈ S
x : Y
hx : x ∈ u
⊢ x ∈ ⋃₀ S
Tactic:
use u
Proof state after:
case mpr.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : ⋃₀ S ≤ t
u : Set Y
hu : u ∈ S
x : Y
hx : x ∈ u
⊢ u ∈ S ∧ x ∈ u
Theorem: Tutorial.isSupUnion
Proof state before:
case mpr.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : ⋃₀ S ≤ t
u : Set Y
hu : u ∈ S
x : Y
hx : x ∈ u
⊢ u ∈ S ∧ x ∈ u
Tactic:
tauto
Proof state after:
no goals
Theorem: Tutorial.image_preimage_adjunction
Proof state before:
α β : Type
f : α → β
⊢ adjunction (Set.image f) (Set.preimage f)
Tactic:
intros s t
Proof state after:
α β : Type
f : α → β
s : Set α
t : Set β
⊢ f '' s ≤ t ↔ s ≤ f ⁻¹' t
Theorem: Tutorial.image_preimage_adjunction
Proof state before:
α β : Type
f : α → β
s : Set α
t : Set β
⊢ f '' s ≤ t ↔ s ≤ f ⁻¹' t
Tactic:
exact Set.image_subset_iff
Proof state after:
no goals
Theorem: Tutorial.adjunction.dual
Proof state before:
X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
l : X → Y
r : Y → X
h : adjunction l r
⊢ adjunction r l
Tactic:
intros y x
Proof state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
l : X → Y
r : Y → X
h : adjunction l r
y : Yᵒᵈ
x : Xᵒᵈ
⊢ r y ≤ x ↔ y ≤ l x
Theorem: Tutorial.adjunction.dual
Proof state before:
X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
l : X → Y
r : Y → X
h : adjunction l r
y : Yᵒᵈ
x : Xᵒᵈ
⊢ r y ≤ x ↔ y ≤ l x
Tactic:
exact (h x y).symm
Proof state after:
no goals
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)
⊢ adjunction l (mk_right l)
Tactic:
intro x y
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
⊢ l x ≤ y ↔ x ≤ mk_right l y
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
⊢ l x ≤ y ↔ x ≤ mk_right l y
Tactic:
constructor
Proof state after:
case mp
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
⊢ l x ≤ y → x ≤ mk_right l y

case mpr
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
⊢ x ≤ mk_right l y → l x ≤ y
Theorem: Tutorial.adjunction_of_Sup
Proof state before:
case mp
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
⊢ l x ≤ y → x ≤ mk_right l y
Tactic:
intro h'
Proof state after:
case mp
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' : l x ≤ y
⊢ x ≤ mk_right l y
Theorem: Tutorial.adjunction_of_Sup
Proof state before:
case mp
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' : l x ≤ y
⊢ x ≤ mk_right l y
Tactic:
exact (CompleteLattice.S_isSup {x | l x ≤ y}).upperBound h'
Proof state after:
no goals
Theorem: Tutorial.adjunction_of_Sup
Proof state before:
case mpr
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
⊢ x ≤ mk_right l y → l x ≤ y
Tactic:
intro h'
Proof state after:
case mpr
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
⊢ l x ≤ y
Theorem: Tutorial.adjunction_of_Sup
Proof state before:
case mpr
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
⊢ l x ≤ y
Tactic:
have l_mono : Monotone l := by {
  intro a b hab
  have := h {a, b}
  rw [Sup_pair.1 hab, Set.image_pair] at this
  exact Sup_pair.2 this.symm
}
Proof state after:
case mpr
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
l_mono : Monotone l
⊢ l x ≤ y
Theorem: Tutorial.adjunction_of_Sup
Proof state before:
case mpr
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
l_mono : Monotone l
⊢ l x ≤ y
Tactic:
calc
  l x ≤ l (mk_right l y) := l_mono h'
  _   = Sup (l '' { x | l x ≤ y }) := h {x | l x ≤ y}
  _   ≤ Sup { y' | y' ≤ y } := Sup_subset (Set.image_preimage_subset l { y' | y' ≤ y })
  _   = y := Sup_le_self y
Proof state after:
no goals
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
⊢ Monotone l
Tactic:
intro a b hab
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
⊢ l a ≤ l b