Theorem: Tutorial.ContinuousProductTopIff (GlimpseOfLean/Solutions/Topics/GaloisAdjunctions.lean)

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

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

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

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

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

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

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