[GOAL]
B : Type u_1
F : Type u_2
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
⊢ topologicalSpace B F = induced (↑(TotalSpace.toProd B F)) instTopologicalSpaceProd
[PROOFSTEP]
simp only [instTopologicalSpaceProd, induced_inf, induced_compose]
[GOAL]
B : Type u_1
F : Type u_2
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
⊢ topologicalSpace B F =
    induced (Prod.fst ∘ ↑(TotalSpace.toProd B F)) inst✝¹ ⊓ induced (Prod.snd ∘ ↑(TotalSpace.toProd B F)) inst✝
[PROOFSTEP]
rfl
[GOAL]
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
⊢ ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
let f₁ : TotalSpace (F₁ × F₂) (E₁ ×ᵇ E₂) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ := fun p ↦
  ((⟨p.1, p.2.1⟩ : TotalSpace F₁ E₁), (⟨p.1, p.2.2⟩ : TotalSpace F₂ E₂))
[GOAL]
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
⊢ ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
let f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p ↦ ⟨e₁ p.1, e₂ p.2⟩
[GOAL]
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
⊢ ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
let f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p ↦ ⟨p.1.1, p.1.2, p.2.2⟩
[GOAL]
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
⊢ ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
have hf₁ : Continuous f₁ := (Prod.inducing_diag F₁ E₁ F₂ E₂).continuous
[GOAL]
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
⊢ ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
have hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source) :=
  e₁.toLocalHomeomorph.continuousOn.prod_map e₂.toLocalHomeomorph.continuousOn
[GOAL]
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
⊢ ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
have hf₃ : Continuous f₃ := (continuous_fst.comp continuous_fst).prod_mk (continuous_snd.prod_map continuous_snd)
[GOAL]
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
⊢ ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
refine' ((hf₃.comp_continuousOn hf₂).comp hf₁.continuousOn _).congr _
[GOAL]
case refine'_1
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
⊢ MapsTo f₁ (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet)) (e₁.source ×ˢ e₂.source)
[PROOFSTEP]
rw [e₁.source_eq, e₂.source_eq]
[GOAL]
case refine'_1
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
⊢ MapsTo f₁ (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
    ((TotalSpace.proj ⁻¹' e₁.baseSet) ×ˢ (TotalSpace.proj ⁻¹' e₂.baseSet))
[PROOFSTEP]
exact mapsTo_preimage _ _
[GOAL]
case refine'_2
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
⊢ EqOn (toFun' e₁ e₂) ((f₃ ∘ f₂) ∘ f₁) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
[PROOFSTEP]
rintro ⟨b, v₁, v₂⟩ ⟨hb₁, _⟩
[GOAL]
case refine'_2.mk.mk.intro
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet
right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet
⊢ toFun' e₁ e₂ { proj := b, snd := (v₁, v₂) } = ((f₃ ∘ f₂) ∘ f₁) { proj := b, snd := (v₁, v₂) }
[PROOFSTEP]
simp only [Prod.toFun', Prod.mk.inj_iff, Function.comp_apply, and_true_iff]
[GOAL]
case refine'_2.mk.mk.intro
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet
right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet
⊢ b = (↑e₁ { proj := b, snd := v₁ }).fst
[PROOFSTEP]
rw [e₁.coe_fst]
[GOAL]
case refine'_2.mk.mk.intro
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet
right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet
⊢ { proj := b, snd := v₁ } ∈ e₁.source
[PROOFSTEP]
rw [e₁.source_eq, mem_preimage]
[GOAL]
case refine'_2.mk.mk.intro
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.fst, ↑e₂ p.snd)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.fst.fst, p.fst.snd, p.snd.snd)
hf₁ : Continuous f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous f₃
b : B
v₁ : E₁ b
v₂ : E₂ b
hb₁ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₁.baseSet
right✝ : { proj := b, snd := (v₁, v₂) }.proj ∈ e₂.baseSet
⊢ { proj := b, snd := v₁ }.proj ∈ e₁.baseSet
[PROOFSTEP]
exact hb₁
[GOAL]
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x
h : x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet)
⊢ invFun' e₁ e₂ (toFun' e₁ e₂ x) = x
[PROOFSTEP]
obtain ⟨x, v₁, v₂⟩ := x
[GOAL]
case mk.mk
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B
v₁ : E₁ x
v₂ : E₂ x
h : { proj := x, snd := (v₁, v₂) } ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet)
⊢ invFun' e₁ e₂ (toFun' e₁ e₂ { proj := x, snd := (v₁, v₂) }) = { proj := x, snd := (v₁, v₂) }
[PROOFSTEP]
obtain ⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩ := h
[GOAL]
case mk.mk.intro
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B
v₁ : E₁ x
v₂ : E₂ x
h₁ : x ∈ e₁.baseSet
h₂ : x ∈ e₂.baseSet
⊢ invFun' e₁ e₂ (toFun' e₁ e₂ { proj := x, snd := (v₁, v₂) }) = { proj := x, snd := (v₁, v₂) }
[PROOFSTEP]
simp only [Prod.toFun', Prod.invFun', symm_apply_apply_mk, h₁, h₂]
[GOAL]
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B × F₁ × F₂
h : x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ x) = x
[PROOFSTEP]
obtain ⟨x, w₁, w₂⟩ := x
[GOAL]
case mk.mk
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B
w₁ : F₁
w₂ : F₂
h : (x, w₁, w₂) ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)
[PROOFSTEP]
obtain ⟨⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩, -⟩ := h
[GOAL]
case mk.mk.intro.intro
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B
w₁ : F₁
w₂ : F₂
h₁ : x ∈ e₁.baseSet
h₂ : x ∈ e₂.baseSet
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)
[PROOFSTEP]
simp only [Prod.toFun', Prod.invFun', apply_mk_symm, h₁, h₂]
[GOAL]
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
⊢ ContinuousOn (invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
[PROOFSTEP]
rw [(Prod.inducing_diag F₁ E₁ F₂ E₂).continuousOn_iff]
[GOAL]
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
⊢ ContinuousOn ((fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })) ∘ invFun' e₁ e₂)
    ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
[PROOFSTEP]
have H₁ : Continuous fun p : B × F₁ × F₂ ↦ ((p.1, p.2.1), (p.1, p.2.2)) :=
  (continuous_id.prod_map continuous_fst).prod_mk (continuous_id.prod_map continuous_snd)
[GOAL]
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
H₁ : Continuous fun p => ((p.fst, p.snd.fst), p.fst, p.snd.snd)
⊢ ContinuousOn ((fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })) ∘ invFun' e₁ e₂)
    ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
[PROOFSTEP]
refine' (e₁.continuousOn_symm.prod_map e₂.continuousOn_symm).comp H₁.continuousOn _
[GOAL]
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
H₁ : Continuous fun p => ((p.fst, p.snd.fst), p.fst, p.snd.snd)
⊢ MapsTo (fun p => ((p.fst, p.snd.fst), p.fst, p.snd.snd)) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
    ((e₁.baseSet ×ˢ univ) ×ˢ e₂.baseSet ×ˢ univ)
[PROOFSTEP]
exact fun x h ↦ ⟨⟨h.1.1, mem_univ _⟩, ⟨h.1.2, mem_univ _⟩⟩
[GOAL]
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
⊢ IsOpen
    { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂, source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
        target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
        map_source' :=
          (_ :
            ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
              x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧ (Prod.toFun' e₁ e₂ x).snd ∈ univ),
        map_target' :=
          (_ : ∀ (x : B × F₁ × F₂), x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
        left_inv' :=
          (_ :
            ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
              x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) → Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
        right_inv' :=
          (_ :
            ∀ (x : B × F₁ × F₂),
              x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) }.source
[PROOFSTEP]
convert (e₁.open_source.prod e₂.open_source).preimage (FiberBundle.Prod.inducing_diag F₁ E₁ F₂ E₂).continuous
[GOAL]
case h.e'_3
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
⊢ { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂, source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
        target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
        map_source' :=
          (_ :
            ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
              x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧ (Prod.toFun' e₁ e₂ x).snd ∈ univ),
        map_target' :=
          (_ : ∀ (x : B × F₁ × F₂), x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
        left_inv' :=
          (_ :
            ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
              x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) → Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
        right_inv' :=
          (_ :
            ∀ (x : B × F₁ × F₂),
              x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) }.source =
    (fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })) ⁻¹' e₁.source ×ˢ e₂.source
[PROOFSTEP]
ext x
[GOAL]
case h.e'_3.h
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x
⊢ x ∈
      { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
          source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet), target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
          map_source' :=
            (_ :
              ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                  (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧ (Prod.toFun' e₁ e₂ x).snd ∈ univ),
          map_target' :=
            (_ : ∀ (x : B × F₁ × F₂), x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
          left_inv' :=
            (_ :
              ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) → Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
          right_inv' :=
            (_ :
              ∀ (x : B × F₁ × F₂),
                x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) }.source ↔
    x ∈
      (fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })) ⁻¹' e₁.source ×ˢ e₂.source
[PROOFSTEP]
simp only [Trivialization.source_eq, mfld_simps]
[GOAL]
B : Type u_1
inst✝¹⁰ : TopologicalSpace B
F₁ : Type u_2
inst✝⁹ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁸ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝⁷ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝⁶ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁵ : (x : B) → Zero (E₁ x)
inst✝⁴ : (x : B) → Zero (E₂ x)
inst✝³ : (x : B) → TopologicalSpace (E₁ x)
inst✝² : (x : B) → TopologicalSpace (E₂ x)
inst✝¹ : FiberBundle F₁ E₁
inst✝ : FiberBundle F₂ E₂
b : B
⊢ Inducing (TotalSpace.mk b)
[PROOFSTEP]
rw [(Prod.inducing_diag F₁ E₁ F₂ E₂).inducing_iff]
[GOAL]
B : Type u_1
inst✝¹⁰ : TopologicalSpace B
F₁ : Type u_2
inst✝⁹ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁸ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝⁷ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝⁶ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁵ : (x : B) → Zero (E₁ x)
inst✝⁴ : (x : B) → Zero (E₂ x)
inst✝³ : (x : B) → TopologicalSpace (E₁ x)
inst✝² : (x : B) → TopologicalSpace (E₂ x)
inst✝¹ : FiberBundle F₁ E₁
inst✝ : FiberBundle F₂ E₂
b : B
⊢ Inducing ((fun p => ({ proj := p.proj, snd := p.snd.fst }, { proj := p.proj, snd := p.snd.snd })) ∘ TotalSpace.mk b)
[PROOFSTEP]
exact (totalSpaceMk_inducing F₁ E₁ b).prod_map (totalSpaceMk_inducing F₂ E₂ b)
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f : B' → B
inst✝ : (x : B) → TopologicalSpace (E x)
⊢ (x : B') → TopologicalSpace ((f *ᵖ E) x)
[PROOFSTEP]
intro x
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f : B' → B
inst✝ : (x : B) → TopologicalSpace (E x)
x : B'
⊢ TopologicalSpace ((f *ᵖ E) x)
[PROOFSTEP]
rw [Bundle.Pullback]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f : B' → B
inst✝ : (x : B) → TopologicalSpace (E x)
x : B'
⊢ TopologicalSpace (E (f x))
[PROOFSTEP]
infer_instance
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Continuous TotalSpace.proj
[PROOFSTEP]
rw [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ ≤ induced TotalSpace.proj inst✝¹
[PROOFSTEP]
exact inf_le_left
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Continuous (Pullback.lift f)
[PROOFSTEP]
rw [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ ≤ induced (Pullback.lift f) inst✝
[PROOFSTEP]
exact inf_le_right
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Inducing (pullbackTotalSpaceEmbedding f)
[PROOFSTEP]
constructor
[GOAL]
case induced
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Pullback.TotalSpace.topologicalSpace F E f = induced (pullbackTotalSpaceEmbedding f) instTopologicalSpaceProd
[PROOFSTEP]
simp_rw [instTopologicalSpaceProd, induced_inf, induced_compose, Pullback.TotalSpace.topologicalSpace,
  pullbackTopology_def]
[GOAL]
case induced
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ =
    induced (Prod.fst ∘ pullbackTotalSpaceEmbedding f) inst✝¹ ⊓ induced (Prod.snd ∘ pullbackTotalSpaceEmbedding f) inst✝
[PROOFSTEP]
rfl
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
f : B' → B
x : B'
⊢ Continuous (TotalSpace.mk x)
[PROOFSTEP]
simp only [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, induced_compose, induced_inf, Function.comp,
  induced_const, top_inf_eq, pullbackTopology_def]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
f : B' → B
x : B'
⊢ instForAllTopologicalSpacePullback E f x ≤ induced (fun x_1 => Pullback.lift f { proj := x, snd := x_1 }) inst✝⁴
[PROOFSTEP]
exact le_of_eq (FiberBundle.totalSpaceMk_inducing F E (f x)).induced
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : TotalSpace F (↑f *ᵖ E)
h : x ∈ Pullback.lift ↑f ⁻¹' e.source
⊢ (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ
[PROOFSTEP]
simp_rw [e.source_eq, mem_preimage, Pullback.lift_proj] at h
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : TotalSpace F (↑f *ᵖ E)
h : ↑f x.proj ∈ e.baseSet
⊢ (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ
[PROOFSTEP]
simp_rw [prod_mk_mem_set_prod_eq, mem_univ, and_true_iff, mem_preimage, h]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
y : B' × F
h : y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ
⊢ (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈ Pullback.lift ↑f ⁻¹' e.source
[PROOFSTEP]
rw [mem_prod, mem_preimage] at h
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
y : B' × F
h : ↑f y.fst ∈ e.baseSet ∧ y.snd ∈ univ
⊢ (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈ Pullback.lift ↑f ⁻¹' e.source
[PROOFSTEP]
simp_rw [e.source_eq, mem_preimage, Pullback.lift_proj, h.1]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : TotalSpace F (↑f *ᵖ E)
h : x ∈ Pullback.lift ↑f ⁻¹' e.source
⊢ (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
      ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
    x
[PROOFSTEP]
simp_rw [mem_preimage, e.mem_source, Pullback.lift_proj] at h
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : TotalSpace F (↑f *ᵖ E)
h : ↑f x.proj ∈ e.baseSet
⊢ (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
      ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
    x
[PROOFSTEP]
simp_rw [Pullback.lift, e.symm_apply_apply_mk h]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : B' × F
h : x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ
⊢ (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
      ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
    x
[PROOFSTEP]
simp_rw [mem_prod, mem_preimage, mem_univ, and_true_iff] at h
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : B' × F
h : ↑f x.fst ∈ e.baseSet
⊢ (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
      ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
    x
[PROOFSTEP]
simp_rw [Pullback.lift_mk, e.apply_mk_symm h]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ IsOpen
    { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
        invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
        source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
        map_source' :=
          (_ :
            ∀ (x : TotalSpace F (↑f *ᵖ E)),
              x ∈ Pullback.lift ↑f ⁻¹' e.source →
                (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
        map_target' :=
          (_ :
            ∀ (y : B' × F),
              y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                  Pullback.lift ↑f ⁻¹' e.source),
        left_inv' :=
          (_ :
            ∀ (x : TotalSpace F (↑f *ᵖ E)),
              x ∈ Pullback.lift ↑f ⁻¹' e.source →
                (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                    ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ (x : B' × F),
              x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                    ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                  x) }.source
[PROOFSTEP]
simp_rw [e.source_eq, ← preimage_comp]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ IsOpen (TotalSpace.proj ∘ Pullback.lift ↑f ⁻¹' e.baseSet)
[PROOFSTEP]
exact e.open_baseSet.preimage ((map_continuous f).comp <| Pullback.continuous_proj F E f)
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ ContinuousOn
    { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
        invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
        source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
        map_source' :=
          (_ :
            ∀ (x : TotalSpace F (↑f *ᵖ E)),
              x ∈ Pullback.lift ↑f ⁻¹' e.source →
                (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
        map_target' :=
          (_ :
            ∀ (y : B' × F),
              y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                  Pullback.lift ↑f ⁻¹' e.source),
        left_inv' :=
          (_ :
            ∀ (x : TotalSpace F (↑f *ᵖ E)),
              x ∈ Pullback.lift ↑f ⁻¹' e.source →
                (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                    ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ (x : B' × F),
              x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                    ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                  x) }.invFun
    { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
        invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
        source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
        map_source' :=
          (_ :
            ∀ (x : TotalSpace F (↑f *ᵖ E)),
              x ∈ Pullback.lift ↑f ⁻¹' e.source →
                (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
        map_target' :=
          (_ :
            ∀ (y : B' × F),
              y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                  Pullback.lift ↑f ⁻¹' e.source),
        left_inv' :=
          (_ :
            ∀ (x : TotalSpace F (↑f *ᵖ E)),
              x ∈ Pullback.lift ↑f ⁻¹' e.source →
                (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                    ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                  x),
        right_inv' :=
          (_ :
            ∀ (x : B' × F),
              x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                    ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                  x) }.target
[PROOFSTEP]
dsimp only
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ ContinuousOn (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) ((↑f ⁻¹' e.baseSet) ×ˢ univ)
[PROOFSTEP]
simp_rw [(inducing_pullbackTotalSpaceEmbedding F E f).continuousOn_iff, Function.comp, pullbackTotalSpaceEmbedding]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ ContinuousOn (fun x => (x.fst, { proj := ↑f x.fst, snd := Trivialization.symm e (↑f x.fst) x.snd }))
    ((↑f ⁻¹' e.baseSet) ×ˢ univ)
[PROOFSTEP]
refine'
  continuousOn_fst.prod (e.continuousOn_symm.comp ((map_continuous f).prod_map continuous_id).continuousOn Subset.rfl)
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ {
          toLocalEquiv :=
            { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
              invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
              source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
              map_source' :=
                (_ :
                  ∀ (x : TotalSpace F (↑f *ᵖ E)),
                    x ∈ Pullback.lift ↑f ⁻¹' e.source →
                      (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
              map_target' :=
                (_ :
                  ∀ (y : B' × F),
                    y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                      (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                        Pullback.lift ↑f ⁻¹' e.source),
              left_inv' :=
                (_ :
                  ∀ (x : TotalSpace F (↑f *ᵖ E)),
                    x ∈ Pullback.lift ↑f ⁻¹' e.source →
                      (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                          ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                        x),
              right_inv' :=
                (_ :
                  ∀ (x : B' × F),
                    x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                      (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                          ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                        x) },
          open_source :=
            (_ :
              IsOpen
                { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
                    invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
                    source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
                    map_source' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
                    map_target' :=
                      (_ :
                        ∀ (y : B' × F),
                          y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                              Pullback.lift ↑f ⁻¹' e.source),
                    left_inv' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                                ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                              x),
                    right_inv' :=
                      (_ :
                        ∀ (x : B' × F),
                          x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                                ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                              x) }.source),
          open_target := (_ : IsOpen ((↑f ⁻¹' e.baseSet) ×ˢ univ)),
          continuous_toFun :=
            (_ :
              ContinuousOn (fun x => (x.proj, (↑e (Pullback.lift (↑f) x)).snd))
                { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
                    invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
                    source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
                    map_source' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
                    map_target' :=
                      (_ :
                        ∀ (y : B' × F),
                          y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                              Pullback.lift ↑f ⁻¹' e.source),
                    left_inv' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                                ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                              x),
                    right_inv' :=
                      (_ :
                        ∀ (x : B' × F),
                          x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                                ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                              x) }.source),
          continuous_invFun :=
            (_ :
              ContinuousOn
                { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
                    invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
                    source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
                    map_source' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
                    map_target' :=
                      (_ :
                        ∀ (y : B' × F),
                          y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                              Pullback.lift ↑f ⁻¹' e.source),
                    left_inv' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                                ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                              x),
                    right_inv' :=
                      (_ :
                        ∀ (x : B' × F),
                          x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                                ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                              x) }.invFun
                { toFun := fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd),
                    invFun := fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd },
                    source := Pullback.lift ↑f ⁻¹' e.source, target := (↑f ⁻¹' e.baseSet) ×ˢ univ,
                    map_source' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ),
                    map_target' :=
                      (_ :
                        ∀ (y : B' × F),
                          y ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) y ∈
                              Pullback.lift ↑f ⁻¹' e.source),
                    left_inv' :=
                      (_ :
                        ∀ (x : TotalSpace F (↑f *ᵖ E)),
                          x ∈ Pullback.lift ↑f ⁻¹' e.source →
                            (fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd })
                                ((fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd)) x) =
                              x),
                    right_inv' :=
                      (_ :
                        ∀ (x : B' × F),
                          x ∈ (↑f ⁻¹' e.baseSet) ×ˢ univ →
                            (fun z => (z.proj, (↑e (Pullback.lift (↑f) z)).snd))
                                ((fun y => { proj := y.fst, snd := Trivialization.symm e (↑f y.fst) y.snd }) x) =
                              x) }.target) }.toLocalEquiv.source =
    TotalSpace.proj ⁻¹' (↑f ⁻¹' e.baseSet)
[PROOFSTEP]
dsimp only
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ Pullback.lift ↑f ⁻¹' e.source = TotalSpace.proj ⁻¹' (↑f ⁻¹' e.baseSet)
[PROOFSTEP]
rw [e.source_eq]
[GOAL]
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (_b : B) → Zero (E _b)
K : Type U
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
⊢ Pullback.lift ↑f ⁻¹' (TotalSpace.proj ⁻¹' e.baseSet) = TotalSpace.proj ⁻¹' (↑f ⁻¹' e.baseSet)
[PROOFSTEP]
rfl


[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
X Y : J
f : X ⟶ Y
⊢ ((Functor.const J).obj (of ↑{u | ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (u i) = u j})).map f ≫
      (fun j => ContinuousMap.mk fun u => ↑u j) Y =
    (fun j => ContinuousMap.mk fun u => ↑u j) X ≫ F.map f
[PROOFSTEP]
dsimp
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
X Y : J
f : X ⟶ Y
⊢ (𝟙 (of { x // ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (x i) = x j }) ≫ ContinuousMap.mk fun u => ↑u Y) =
    (ContinuousMap.mk fun u => ↑u X) ≫ F.map f
[PROOFSTEP]
rw [Category.id_comp]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
X Y : J
f : X ⟶ Y
⊢ (ContinuousMap.mk fun u => ↑u Y) = (ContinuousMap.mk fun u => ↑u X) ≫ F.map f
[PROOFSTEP]
apply ContinuousMap.ext
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
X Y : J
f : X ⟶ Y
⊢ ∀ (a : { x // ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (x i) = x j }),
    ↑(ContinuousMap.mk fun u => ↑u Y) a = ↑((ContinuousMap.mk fun u => ↑u X) ≫ F.map f) a
[PROOFSTEP]
intro a
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
X Y : J
f : X ⟶ Y
a : { x // ∀ {i j : J} (f : i ⟶ j), ↑(F.map f) (x i) = x j }
⊢ ↑(ContinuousMap.mk fun u => ↑u Y) a = ↑((ContinuousMap.mk fun u => ↑u X) ≫ F.map f) a
[PROOFSTEP]
exact (a.2 f).symm
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
S : Cone F
x : ↑S.pt
i✝ j✝ : J
f : i✝ ⟶ j✝
⊢ ↑(F.map f) ((fun j => ↑(NatTrans.app S.π j) x) i✝) = (fun j => ↑(NatTrans.app S.π j) x) j✝
[PROOFSTEP]
dsimp
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
S : Cone F
x : ↑S.pt
i✝ j✝ : J
f : i✝ ⟶ j✝
⊢ ↑(F.map f) (↑(NatTrans.app S.π i✝) x) = ↑(NatTrans.app S.π j✝) x
[PROOFSTEP]
erw [← S.w f]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
S : Cone F
x : ↑S.pt
i✝ j✝ : J
f : i✝ ⟶ j✝
⊢ ↑(F.map f) (↑(NatTrans.app S.π i✝) x) = ↑(NatTrans.app S.π i✝ ≫ F.map f) x
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
S : Cone F
x : ↑S.pt
i j : J
f : i ⟶ j
⊢ ↑(F.map f) ((fun j => ↑(NatTrans.app S.π j) x) i) = (fun j => ↑(NatTrans.app S.π j) x) j
[PROOFSTEP]
dsimp
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
S : Cone F
x : ↑S.pt
i j : J
f : i ⟶ j
⊢ ↑(F.map f) (↑(NatTrans.app S.π i) x) = ↑(NatTrans.app S.π j) x
[PROOFSTEP]
rw [← S.w f]
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
S : Cone F
x : ↑S.pt
i j : J
f : i ⟶ j
⊢ ↑(F.map f) (↑(NatTrans.app S.π i) x) = ↑(NatTrans.app S.π i ≫ F.map f) x
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
S : Cone F
m : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app S.π j
⊢ m =
    (fun S =>
        ContinuousMap.mk fun x =>
          { val := fun j => ↑(NatTrans.app S.π j) x,
            property :=
              (_ :
                ∀ {i j : J} (f : i ⟶ j),
                  ↑(F.map f) ((fun j => ↑(NatTrans.app S.π j) x) i) = (fun j => ↑(NatTrans.app S.π j) x) j) })
      S
[PROOFSTEP]
apply ContinuousMap.ext
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
S : Cone F
m : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app S.π j
⊢ ∀ (a : ↑S.pt),
    ↑m a =
      ↑((fun S =>
              ContinuousMap.mk fun x =>
                { val := fun j => ↑(NatTrans.app S.π j) x,
                  property :=
                    (_ :
                      ∀ {i j : J} (f : i ⟶ j),
                        ↑(F.map f) ((fun j => ↑(NatTrans.app S.π j) x) i) = (fun j => ↑(NatTrans.app S.π j) x) j) })
            S)
        a
[PROOFSTEP]
intros a
[GOAL]
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
S : Cone F
m : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app S.π j
a : ↑S.pt
⊢ ↑m a =
    ↑((fun S =>
            ContinuousMap.mk fun x =>
              { val := fun j => ↑(NatTrans.app S.π j) x,
                property :=
                  (_ :
                    ∀ {i j : J} (f : i ⟶ j),
                      ↑(F.map f) ((fun j => ↑(NatTrans.app S.π j) x) i) = (fun j => ↑(NatTrans.app S.π j) x) j) })
          S)
      a
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case h.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
S : Cone F
m : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app S.π j
a : ↑S.pt
⊢ ↑(↑m a) =
    ↑(↑((fun S =>
              ContinuousMap.mk fun x =>
                { val := fun j => ↑(NatTrans.app S.π j) x,
                  property :=
                    (_ :
                      ∀ {i j : J} (f : i ⟶ j),
                        ↑(F.map f) ((fun j => ↑(NatTrans.app S.π j) x) i) = (fun j => ↑(NatTrans.app S.π j) x) j) })
            S)
        a)
[PROOFSTEP]
funext j
[GOAL]
case h.a.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
S : Cone F
m : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app S.π j
a : ↑S.pt
j : J
⊢ ↑(↑m a) j =
    ↑(↑((fun S =>
                ContinuousMap.mk fun x =>
                  { val := fun j => ↑(NatTrans.app S.π j) x,
                    property :=
                      (_ :
                        ∀ {i j : J} (f : i ⟶ j),
                          ↑(F.map f) ((fun j => ↑(NatTrans.app S.π j) x) i) = (fun j => ↑(NatTrans.app S.π j) x) j) })
              S)
          a)
      j
[PROOFSTEP]
dsimp
[GOAL]
case h.a.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
S : Cone F
m : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app S.π j
a : ↑S.pt
j : J
⊢ ↑(↑m a) j = ↑(NatTrans.app S.π j) a
[PROOFSTEP]
rw [← h]
[GOAL]
case h.a.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
S : Cone F
m : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ NatTrans.app (limitCone F).π j = NatTrans.app S.π j
a : ↑S.pt
j : J
⊢ ↑(↑m a) j = ↑(m ≫ NatTrans.app (limitCone F).π j) a
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
⊢ IsLimit (limitConeInfi F)
[PROOFSTEP]
refine
  IsLimit.ofFaithful forget
    (Types.limitConeIsLimit.{v, u} (F ⋙ forget))
      -- Porting note: previously could infer all ?_ except continuity
    (fun s => ⟨fun v => ⟨fun j => (Functor.mapCone forget s).π.app j v, ?_⟩, ?_⟩) fun s => ?_
[GOAL]
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
s : Cone F
v : ↑s.pt
⊢ (fun j => NatTrans.app (forget.mapCone s).π j v) ∈ Functor.sections (F ⋙ forget)
[PROOFSTEP]
dsimp [Functor.sections]
[GOAL]
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
s : Cone F
v : ↑s.pt
⊢ ∀ {j j' : J} (f : j ⟶ j'),
    forget.map (F.map f) (forget.map (NatTrans.app s.π j) v) = forget.map (NatTrans.app s.π j') v
[PROOFSTEP]
intro _ _ _
[GOAL]
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
s : Cone F
v : ↑s.pt
j✝ j'✝ : J
f✝ : j✝ ⟶ j'✝
⊢ forget.map (F.map f✝) (forget.map (NatTrans.app s.π j✝) v) = forget.map (NatTrans.app s.π j'✝) v
[PROOFSTEP]
rw [← comp_apply', forget_map_eq_coe, ← s.π.naturality, forget_map_eq_coe]
[GOAL]
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
s : Cone F
v : ↑s.pt
j✝ j'✝ : J
f✝ : j✝ ⟶ j'✝
⊢ ↑(((Functor.const J).obj s.pt).map f✝ ≫ NatTrans.app s.π j'✝) v = ↑(NatTrans.app s.π j'✝) v
[PROOFSTEP]
dsimp
[GOAL]
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
s : Cone F
v : ↑s.pt
j✝ j'✝ : J
f✝ : j✝ ⟶ j'✝
⊢ ↑(𝟙 s.pt ≫ NatTrans.app s.π j'✝) v = ↑(NatTrans.app s.π j'✝) v
[PROOFSTEP]
rw [Category.id_comp]
[GOAL]
case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
s : Cone F
⊢ Continuous fun v =>
    { val := fun j => NatTrans.app (forget.mapCone s).π j v,
      property := (_ : (fun j => NatTrans.app (forget.mapCone s).π j v) ∈ Functor.sections (F ⋙ forget)) }
[PROOFSTEP]
exact
  continuous_iff_coinduced_le.mpr
    (le_iInf fun j => coinduced_le_iff_le_induced.mp <| (continuous_iff_coinduced_le.mp (s.π.app j).continuous : _))
[GOAL]
case refine_3
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
s : Cone F
⊢ forget.map
      ((fun s =>
          ContinuousMap.mk fun v =>
            { val := fun j => NatTrans.app (forget.mapCone s).π j v,
              property := (_ : (fun j => NatTrans.app (forget.mapCone s).π j v) ∈ Functor.sections (F ⋙ forget)) })
        s) =
    IsLimit.lift (Types.limitConeIsLimit (F ⋙ forget)) (forget.mapCone s)
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
⊢ IsColimit (colimitCocone F)
[PROOFSTEP]
refine
  IsColimit.ofFaithful forget (Types.colimitCoconeIsColimit _)
    (fun s =>
        -- Porting note: it appears notation for forget breaks dot notation (also above)
            -- Porting note: previously function was inferred
      ⟨Quot.lift (fun p => (Functor.mapCocone forget s).ι.app p.fst p.snd) ?_, ?_⟩)
    fun s => ?_
[GOAL]
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
s : Cocone F
⊢ ∀ (a b : (j : J) × (F ⋙ forget).obj j),
    Types.Quot.Rel (F ⋙ forget) a b →
      (fun p => NatTrans.app (forget.mapCocone s).ι p.fst p.snd) a =
        (fun p => NatTrans.app (forget.mapCocone s).ι p.fst p.snd) b
[PROOFSTEP]
intro _ _ ⟨_, h⟩
[GOAL]
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
s : Cocone F
a✝ b✝ : (j : J) × (F ⋙ forget).obj j
w✝ : a✝.fst ⟶ b✝.fst
h : b✝.snd = (F ⋙ forget).map w✝ a✝.snd
⊢ (fun p => NatTrans.app (forget.mapCocone s).ι p.fst p.snd) a✝ =
    (fun p => NatTrans.app (forget.mapCocone s).ι p.fst p.snd) b✝
[PROOFSTEP]
dsimp
[GOAL]
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
s : Cocone F
a✝ b✝ : (j : J) × (F ⋙ forget).obj j
w✝ : a✝.fst ⟶ b✝.fst
h : b✝.snd = (F ⋙ forget).map w✝ a✝.snd
⊢ forget.map (NatTrans.app s.ι a✝.fst) a✝.snd = forget.map (NatTrans.app s.ι b✝.fst) b✝.snd
[PROOFSTEP]
rw [h, Functor.comp_map, ← comp_apply', s.ι.naturality]
[GOAL]
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
s : Cocone F
a✝ b✝ : (j : J) × (F ⋙ forget).obj j
w✝ : a✝.fst ⟶ b✝.fst
h : b✝.snd = (F ⋙ forget).map w✝ a✝.snd
⊢ forget.map (NatTrans.app s.ι a✝.fst) a✝.snd =
    forget.map (NatTrans.app s.ι a✝.fst ≫ ((Functor.const J).obj s.pt).map w✝) a✝.snd
[PROOFSTEP]
dsimp
[GOAL]
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
s : Cocone F
a✝ b✝ : (j : J) × (F ⋙ forget).obj j
w✝ : a✝.fst ⟶ b✝.fst
h : b✝.snd = (F ⋙ forget).map w✝ a✝.snd
⊢ forget.map (NatTrans.app s.ι a✝.fst) a✝.snd = forget.map (NatTrans.app s.ι a✝.fst ≫ 𝟙 s.pt) a✝.snd
[PROOFSTEP]
rw [Category.comp_id]
[GOAL]
case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
s : Cocone F
⊢ Continuous
    (Quot.lift (fun p => NatTrans.app (forget.mapCocone s).ι p.fst p.snd)
      (_ :
        ∀ (a b : (j : J) × (F ⋙ forget).obj j),
          Types.Quot.Rel (F ⋙ forget) a b →
            (fun p => NatTrans.app (forget.mapCocone s).ι p.fst p.snd) a =
              (fun p => NatTrans.app (forget.mapCocone s).ι p.fst p.snd) b))
[PROOFSTEP]
exact
  continuous_iff_le_induced.mpr
    (iSup_le fun j => coinduced_le_iff_le_induced.mp <| (continuous_iff_coinduced_le.mp (s.ι.app j).continuous : _))
[GOAL]
case refine_3
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
s : Cocone F
⊢ forget.map
      ((fun s =>
          ContinuousMap.mk
            (Quot.lift (fun p => NatTrans.app (forget.mapCocone s).ι p.fst p.snd)
              (_ :
                ∀ (a b : (j : J) × (F ⋙ forget).obj j),
                  Types.Quot.Rel (F ⋙ forget) a b →
                    (fun p => NatTrans.app (forget.mapCocone s).ι p.fst p.snd) a =
                      (fun p => NatTrans.app (forget.mapCocone s).ι p.fst p.snd) b)))
        s) =
    IsColimit.desc (Types.colimitCoconeIsColimit (F ⋙ forget)) (forget.mapCocone s)
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
X : TopCat
⊢ Continuous fun x => PUnit.unit
[PROOFSTEP]
continuity
[GOAL]
J : Type v
inst✝ : SmallCategory J
X : TopCat
f : X ⟶ of PUnit
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case w
J : Type v
inst✝ : SmallCategory J
X : TopCat
f : X ⟶ of PUnit
x✝ : forget.obj X
⊢ ↑f x✝ = ↑default x✝
[PROOFSTEP]
aesop
[GOAL]
J : Type v
inst✝ : SmallCategory J
X : TopCat
⊢ Continuous fun x => PEmpty.elim x
[PROOFSTEP]
continuity
[GOAL]
J : Type v
inst✝ : SmallCategory J
X : TopCat
f : of PEmpty ⟶ X
⊢ f = default
[PROOFSTEP]
ext ⟨⟩


[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
a : R
h : a ∈ closure s
b : R
ih : ∃ L, (∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) ∧ List.sum (List.map List.prod L) = b
L1 : List (List R)
h1 : ∀ (l : List R), l ∈ L1 → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
x✝ : AddGroup.InClosure (Monoid.Closure s) (List.sum (List.map List.prod L1))
⊢ List.sum (List.map List.prod (List.map (List.cons (-1)) L1)) = -List.sum (List.map List.prod L1)
[PROOFSTEP]
simp only [List.map_map, (· ∘ ·), List.prod_cons, neg_one_mul]
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
a : R
h : a ∈ closure s
b : R
ih : ∃ L, (∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) ∧ List.sum (List.map List.prod L) = b
L1 : List (List R)
h1 : ∀ (l : List R), l ∈ L1 → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
x✝ : AddGroup.InClosure (Monoid.Closure s) (List.sum (List.map List.prod L1))
⊢ List.sum (List.map (fun x => -List.prod x) L1) = -List.sum (List.map List.prod L1)
[PROOFSTEP]
refine' List.recOn L1 neg_zero.symm fun hd tl ih ↦ _
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
a : R
h : a ∈ closure s
b : R
ih✝ : ∃ L, (∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) ∧ List.sum (List.map List.prod L) = b
L1 : List (List R)
h1 : ∀ (l : List R), l ∈ L1 → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
x✝ : AddGroup.InClosure (Monoid.Closure s) (List.sum (List.map List.prod L1))
hd : List R
tl : List (List R)
ih : List.sum (List.map (fun x => -List.prod x) tl) = -List.sum (List.map List.prod tl)
⊢ List.sum (List.map (fun x => -List.prod x) (hd :: tl)) = -List.sum (List.map List.prod (hd :: tl))
[PROOFSTEP]
rw [List.map_cons, List.sum_cons, ih, List.map_cons, List.sum_cons, neg_add]
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
a : R
h : a ∈ closure s
r1 r2 : R
ih1 : ∃ L, (∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) ∧ List.sum (List.map List.prod L) = r1
ih2 : ∃ L, (∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) ∧ List.sum (List.map List.prod L) = r2
L1 : List (List R)
h1 : ∀ (l : List R), l ∈ L1 → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
L2 : List (List R)
h2 : ∀ (l : List R), l ∈ L2 → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
x✝¹ : AddGroup.InClosure (Monoid.Closure s) (List.sum (List.map List.prod L1))
x✝ : AddGroup.InClosure (Monoid.Closure s) (List.sum (List.map List.prod L2))
⊢ List.sum (List.map List.prod (L1 ++ L2)) = List.sum (List.map List.prod L1) + List.sum (List.map List.prod L2)
[PROOFSTEP]
rw [List.map_append, List.sum_append]
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
x : R
hx : x ∈ closure s
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
⊢ C x
[PROOFSTEP]
have h0 : C 0 := add_neg_self (1 : R) ▸ ha h1 hneg1
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
x : R
hx : x ∈ closure s
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
⊢ C x
[PROOFSTEP]
rcases exists_list_of_mem_closure hx with ⟨L, HL, rfl⟩
[GOAL]
case intro.intro
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hx : List.sum (List.map List.prod L) ∈ closure s
⊢ C (List.sum (List.map List.prod L))
[PROOFSTEP]
clear hx
[GOAL]
case intro.intro
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
⊢ C (List.sum (List.map List.prod L))
[PROOFSTEP]
induction' L with hd tl ih
[GOAL]
case intro.intro.nil
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
HL : ∀ (l : List R), l ∈ [] → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
⊢ C (List.sum (List.map List.prod []))
[PROOFSTEP]
exact h0
[GOAL]
case intro.intro.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
tl : List (List R)
ih : (∀ (l : List R), l ∈ tl → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) → C (List.sum (List.map List.prod tl))
HL : ∀ (l : List R), l ∈ hd :: tl → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
⊢ C (List.sum (List.map List.prod (hd :: tl)))
[PROOFSTEP]
rw [List.forall_mem_cons] at HL
[GOAL]
case intro.intro.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
tl : List (List R)
ih : (∀ (l : List R), l ∈ tl → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (x_1 : R), x_1 ∈ x → x_1 ∈ s ∨ x_1 = -1
⊢ C (List.sum (List.map List.prod (hd :: tl)))
[PROOFSTEP]
suffices C (List.prod hd) by
  rw [List.map_cons, List.sum_cons]
  exact ha this (ih HL.2)
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
tl : List (List R)
ih : (∀ (l : List R), l ∈ tl → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (x_1 : R), x_1 ∈ x → x_1 ∈ s ∨ x_1 = -1
this : C (List.prod hd)
⊢ C (List.sum (List.map List.prod (hd :: tl)))
[PROOFSTEP]
rw [List.map_cons, List.sum_cons]
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
tl : List (List R)
ih : (∀ (l : List R), l ∈ tl → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (x_1 : R), x_1 ∈ x → x_1 ∈ s ∨ x_1 = -1
this : C (List.prod hd)
⊢ C (List.prod hd + List.sum (List.map List.prod tl))
[PROOFSTEP]
exact ha this (ih HL.2)
[GOAL]
case intro.intro.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
tl : List (List R)
ih : (∀ (l : List R), l ∈ tl → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (x_1 : R), x_1 ∈ x → x_1 ∈ s ∨ x_1 = -1
⊢ C (List.prod hd)
[PROOFSTEP]
replace HL := HL.1
[GOAL]
case intro.intro.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
tl : List (List R)
ih : (∀ (l : List R), l ∈ tl → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) → C (List.sum (List.map List.prod tl))
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
⊢ C (List.prod hd)
[PROOFSTEP]
clear ih tl
[GOAL]
case intro.intro.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
⊢ C (List.prod hd)
[PROOFSTEP]
suffices ∃ L, (∀ x ∈ L, x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
  by
  rcases this with ⟨L, HL', HP | HP⟩ <;> rw [HP] <;> clear HP HL
  · induction' L with hd tl ih
    · exact h1
    rw [List.forall_mem_cons] at HL'
    rw [List.prod_cons]
    exact hs _ HL'.1 _ (ih HL'.2)
  · induction' L with hd tl ih
    · exact hneg1
    rw [List.prod_cons, neg_mul_eq_mul_neg]
    rw [List.forall_mem_cons] at HL'
    exact hs _ HL'.1 _ (ih HL'.2)
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
this : ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
⊢ C (List.prod hd)
[PROOFSTEP]
rcases this with ⟨L, HL', HP | HP⟩
[GOAL]
case intro.intro.inl
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = List.prod L
⊢ C (List.prod hd)
[PROOFSTEP]
rw [HP]
[GOAL]
case intro.intro.inr
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = -List.prod L
⊢ C (List.prod hd)
[PROOFSTEP]
rw [HP]
[GOAL]
case intro.intro.inl
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = List.prod L
⊢ C (List.prod L)
[PROOFSTEP]
clear HP HL
[GOAL]
case intro.intro.inr
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = -List.prod L
⊢ C (-List.prod L)
[PROOFSTEP]
clear HP HL
[GOAL]
case intro.intro.inl
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
⊢ C (List.prod L)
[PROOFSTEP]
induction' L with hd tl ih
[GOAL]
case intro.intro.inl.nil
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
HL' : ∀ (x : R), x ∈ [] → x ∈ s
⊢ C (List.prod [])
[PROOFSTEP]
exact h1
[GOAL]
case intro.intro.inl.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (List.prod tl)
HL' : ∀ (x : R), x ∈ hd :: tl → x ∈ s
⊢ C (List.prod (hd :: tl))
[PROOFSTEP]
rw [List.forall_mem_cons] at HL'
[GOAL]
case intro.intro.inl.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (List.prod tl)
HL' : hd ∈ s ∧ ∀ (x : R), x ∈ tl → x ∈ s
⊢ C (List.prod (hd :: tl))
[PROOFSTEP]
rw [List.prod_cons]
[GOAL]
case intro.intro.inl.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (List.prod tl)
HL' : hd ∈ s ∧ ∀ (x : R), x ∈ tl → x ∈ s
⊢ C (hd * List.prod tl)
[PROOFSTEP]
exact hs _ HL'.1 _ (ih HL'.2)
[GOAL]
case intro.intro.inr
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
⊢ C (-List.prod L)
[PROOFSTEP]
induction' L with hd tl ih
[GOAL]
case intro.intro.inr.nil
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
HL' : ∀ (x : R), x ∈ [] → x ∈ s
⊢ C (-List.prod [])
[PROOFSTEP]
exact hneg1
[GOAL]
case intro.intro.inr.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (-List.prod tl)
HL' : ∀ (x : R), x ∈ hd :: tl → x ∈ s
⊢ C (-List.prod (hd :: tl))
[PROOFSTEP]
rw [List.prod_cons, neg_mul_eq_mul_neg]
[GOAL]
case intro.intro.inr.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (-List.prod tl)
HL' : ∀ (x : R), x ∈ hd :: tl → x ∈ s
⊢ C (hd * -List.prod tl)
[PROOFSTEP]
rw [List.forall_mem_cons] at HL'
[GOAL]
case intro.intro.inr.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (-List.prod tl)
HL' : hd ∈ s ∧ ∀ (x : R), x ∈ tl → x ∈ s
⊢ C (hd * -List.prod tl)
[PROOFSTEP]
exact hs _ HL'.1 _ (ih HL'.2)
[GOAL]
case intro.intro.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
[PROOFSTEP]
induction' hd with hd tl ih
[GOAL]
case intro.intro.cons.nil
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL✝ : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
HL : ∀ (x : R), x ∈ [] → x ∈ s ∨ x = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod [] = List.prod L ∨ List.prod [] = -List.prod L)
[PROOFSTEP]
exact ⟨[], List.forall_mem_nil _, Or.inl rfl⟩
[GOAL]
case intro.intro.cons.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : ∀ (x : R), x ∈ hd :: tl → x ∈ s ∨ x = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
rw [List.forall_mem_cons] at HL
[GOAL]
case intro.intro.cons.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
rcases ih HL.2 with ⟨L, HL', HP | HP⟩
[GOAL]
case intro.intro.cons.cons.intro.intro.inl
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
cases' HL.1 with hhd hhd
[GOAL]
case intro.intro.cons.cons.intro.intro.inr
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
cases' HL.1 with hhd hhd
[GOAL]
case intro.intro.cons.cons.intro.intro.inl.inl
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd ∈ s
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact ⟨hd :: L, List.forall_mem_cons.2 ⟨hhd, HL'⟩, Or.inl <| by rw [List.prod_cons, List.prod_cons, HP]⟩
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd ∈ s
⊢ List.prod (hd :: tl) = List.prod (hd :: L)
[PROOFSTEP]
rw [List.prod_cons, List.prod_cons, HP]
[GOAL]
case intro.intro.cons.cons.intro.intro.inl.inr
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact ⟨L, HL', Or.inr <| by rw [List.prod_cons, hhd, neg_one_mul, HP]⟩
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd = -1
⊢ List.prod (hd :: tl) = -List.prod L
[PROOFSTEP]
rw [List.prod_cons, hhd, neg_one_mul, HP]
[GOAL]
case intro.intro.cons.cons.intro.intro.inr.inl
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd ∈ s
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact
  ⟨hd :: L, List.forall_mem_cons.2 ⟨hhd, HL'⟩, Or.inr <| by rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]⟩
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd ∈ s
⊢ List.prod (hd :: tl) = -List.prod (hd :: L)
[PROOFSTEP]
rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]
[GOAL]
case intro.intro.cons.cons.intro.intro.inr.inr
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact ⟨L, HL', Or.inl <| by rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]⟩
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd = -1
⊢ List.prod (hd :: tl) = List.prod L
[PROOFSTEP]
rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]
[GOAL]
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
⊢ ↑f '' closure s = closure (↑f '' s)
[PROOFSTEP]
refine'
  le_antisymm _ (closure_subset (RingHom.isSubring_image _ closure.isSubring) <| Set.image_subset _ subset_closure)
[GOAL]
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
⊢ ↑f '' closure s ≤ closure (↑f '' s)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ ↑f x ∈ closure (↑f '' s)
[PROOFSTEP]
apply AddGroup.InClosure.recOn (motive := fun {x} _ ↦ f x ∈ closure (f '' s)) hx _
[GOAL]
case intro.intro.zero
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ ↑f 0 ∈ closure (↑f '' s)
[PROOFSTEP]
intros
[GOAL]
case intro.intro.neg
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ ∀ {a : R}, AddGroup.InClosure (Monoid.Closure s) a → ↑f a ∈ closure (↑f '' s) → ↑f (-a) ∈ closure (↑f '' s)
[PROOFSTEP]
intros
[GOAL]
case intro.intro.add
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ ∀ {a b : R},
    AddGroup.InClosure (Monoid.Closure s) a →
      AddGroup.InClosure (Monoid.Closure s) b →
        ↑f a ∈ closure (↑f '' s) → ↑f b ∈ closure (↑f '' s) → ↑f (a + b) ∈ closure (↑f '' s)
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ ∀ {a : R} (a_1 : a ∈ Monoid.Closure s),
    (fun {x} x_1 => ↑f x ∈ closure (↑f '' s)) (_ : AddGroup.InClosure (Monoid.Closure s) a)
[PROOFSTEP]
intros
[GOAL]
case intro.intro.zero
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ ↑f 0 ∈ closure (↑f '' s)
[PROOFSTEP]
rw [f.map_zero]
[GOAL]
case intro.intro.zero
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ 0 ∈ closure (↑f '' s)
[PROOFSTEP]
apply closure.isSubring.zero_mem
[GOAL]
case intro.intro.neg
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝¹ : R
a✝ : AddGroup.InClosure (Monoid.Closure s) a✝¹
a_ih✝ : ↑f a✝¹ ∈ closure (↑f '' s)
⊢ ↑f (-a✝¹) ∈ closure (↑f '' s)
[PROOFSTEP]
rw [f.map_neg]
[GOAL]
case intro.intro.neg
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝¹ : R
a✝ : AddGroup.InClosure (Monoid.Closure s) a✝¹
a_ih✝ : ↑f a✝¹ ∈ closure (↑f '' s)
⊢ -↑f a✝¹ ∈ closure (↑f '' s)
[PROOFSTEP]
apply closure.isSubring.neg_mem
[GOAL]
case intro.intro.neg
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝¹ : R
a✝ : AddGroup.InClosure (Monoid.Closure s) a✝¹
a_ih✝ : ↑f a✝¹ ∈ closure (↑f '' s)
⊢ ↑f a✝¹ ∈ closure (↑f '' s)
[PROOFSTEP]
assumption
[GOAL]
case intro.intro.add
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝² b✝ : R
a✝¹ : AddGroup.InClosure (Monoid.Closure s) a✝²
a✝ : AddGroup.InClosure (Monoid.Closure s) b✝
a_ih✝¹ : ↑f a✝² ∈ closure (↑f '' s)
a_ih✝ : ↑f b✝ ∈ closure (↑f '' s)
⊢ ↑f (a✝² + b✝) ∈ closure (↑f '' s)
[PROOFSTEP]
rw [f.map_add]
[GOAL]
case intro.intro.add
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝² b✝ : R
a✝¹ : AddGroup.InClosure (Monoid.Closure s) a✝²
a✝ : AddGroup.InClosure (Monoid.Closure s) b✝
a_ih✝¹ : ↑f a✝² ∈ closure (↑f '' s)
a_ih✝ : ↑f b✝ ∈ closure (↑f '' s)
⊢ ↑f a✝² + ↑f b✝ ∈ closure (↑f '' s)
[PROOFSTEP]
apply closure.isSubring.add_mem
[GOAL]
case intro.intro.add.a
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝² b✝ : R
a✝¹ : AddGroup.InClosure (Monoid.Closure s) a✝²
a✝ : AddGroup.InClosure (Monoid.Closure s) b✝
a_ih✝¹ : ↑f a✝² ∈ closure (↑f '' s)
a_ih✝ : ↑f b✝ ∈ closure (↑f '' s)
⊢ ↑f a✝² ∈ closure (↑f '' s)
case intro.intro.add.a
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝² b✝ : R
a✝¹ : AddGroup.InClosure (Monoid.Closure s) a✝²
a✝ : AddGroup.InClosure (Monoid.Closure s) b✝
a_ih✝¹ : ↑f a✝² ∈ closure (↑f '' s)
a_ih✝ : ↑f b✝ ∈ closure (↑f '' s)
⊢ ↑f b✝ ∈ closure (↑f '' s)
[PROOFSTEP]
assumption'
[GOAL]
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝¹ : R
a✝ : a✝¹ ∈ Monoid.Closure s
⊢ ↑f a✝¹ ∈ closure (↑f '' s)
[PROOFSTEP]
apply AddGroup.mem_closure
[GOAL]
case a
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝¹ : R
a✝ : a✝¹ ∈ Monoid.Closure s
⊢ ↑f a✝¹ ∈ Monoid.Closure (↑f '' s)
[PROOFSTEP]
rw [← Monoid.image_closure f.to_isMonoidHom]
[GOAL]
case a
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝¹ : R
a✝ : a✝¹ ∈ Monoid.Closure s
⊢ ↑f a✝¹ ∈ ↑f '' Monoid.Closure s
[PROOFSTEP]
apply Set.mem_image_of_mem
[GOAL]
case a.h
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝¹ : R
a✝ : a✝¹ ∈ Monoid.Closure s
⊢ a✝¹ ∈ Monoid.Closure s
[PROOFSTEP]
assumption