Theorem: analyticGroupoid_prod
Proof state before:
case refine_3.hf
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
ei : interior (range fun x => (↑I x.1, ↑J x.2)) = interior (range ↑I) ×ˢ interior (range ↑J)
fa :
  f ∈ contDiffGroupoid ⊤ I ∧
    (AnalyticOn 𝕜 (fun x => ↑I (↑f (↑I.symm x))) (↑I.symm ⁻¹' f.source ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.source ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f (↑I.symm x))) ⁻¹' interior (range ↑I)) ∧
      AnalyticOn 𝕜 (fun x => ↑I (↑f.symm (↑I.symm x))) (↑I.symm ⁻¹' f.target ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.target ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f.symm (↑I.symm x))) ⁻¹' interior (range ↑I)
ga :
  g ∈ contDiffGroupoid ⊤ J ∧
    (AnalyticOn 𝕜 (fun x => ↑J (↑g (↑J.symm x))) (↑J.symm ⁻¹' g.source ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.source ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g (↑J.symm x))) ⁻¹' interior (range ↑J)) ∧
      AnalyticOn 𝕜 (fun x => ↑J (↑g.symm (↑J.symm x))) (↑J.symm ⁻¹' g.target ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.target ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g.symm (↑J.symm x))) ⁻¹' interior (range ↑J)
⊢ MapsTo (fun x => x.1)
    ((fun p => (↑I.symm p.1, ↑J.symm p.2)) ⁻¹' (f.prod g.toPartialEquiv).target ∩ interior (range ↑(I.prod J)))
    (↑I.symm ⁻¹' f.target ∩ interior (range ↑I))
Tactic:
intro x m
Proof state after:
case refine_3.hf
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
ei : interior (range fun x => (↑I x.1, ↑J x.2)) = interior (range ↑I) ×ˢ interior (range ↑J)
fa :
  f ∈ contDiffGroupoid ⊤ I ∧
    (AnalyticOn 𝕜 (fun x => ↑I (↑f (↑I.symm x))) (↑I.symm ⁻¹' f.source ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.source ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f (↑I.symm x))) ⁻¹' interior (range ↑I)) ∧
      AnalyticOn 𝕜 (fun x => ↑I (↑f.symm (↑I.symm x))) (↑I.symm ⁻¹' f.target ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.target ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f.symm (↑I.symm x))) ⁻¹' interior (range ↑I)
ga :
  g ∈ contDiffGroupoid ⊤ J ∧
    (AnalyticOn 𝕜 (fun x => ↑J (↑g (↑J.symm x))) (↑J.symm ⁻¹' g.source ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.source ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g (↑J.symm x))) ⁻¹' interior (range ↑J)) ∧
      AnalyticOn 𝕜 (fun x => ↑J (↑g.symm (↑J.symm x))) (↑J.symm ⁻¹' g.target ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.target ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g.symm (↑J.symm x))) ⁻¹' interior (range ↑J)
x : E × F
m : x ∈ (fun p => (↑I.symm p.1, ↑J.symm p.2)) ⁻¹' (f.prod g.toPartialEquiv).target ∩ interior (range ↑(I.prod J))
⊢ (fun x => x.1) x ∈ ↑I.symm ⁻¹' f.target ∩ interior (range ↑I)