Theorem: Tutorial.Subgroups.isInf.lift (GlimpseOfLean/Solutions/Topics/GaloisAdjunctions.lean)

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'
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

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')]
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)

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
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

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
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

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⟩
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

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]
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''

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''
State after:
no goals

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''
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''

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'
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

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''
State after:
no goals