Theorem: analyticGroupoid_prod
Proof state before:
case refine_4
𝕜 : 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)
⊢ ↑(I.prod J).symm ⁻¹' (f.prod g).target ∩ interior (range ↑(I.prod J)) ⊆
    (fun x => ↑(I.prod J) (↑(f.prod g).symm (↑(I.prod J).symm x))) ⁻¹' interior (range ↑(I.prod J))
Tactic:
simp only [ModelWithCorners.prod, ModelWithCorners.source_eq, mem_univ, and_self, setOf_true,
  PartialEquiv.prod_target, ModelWithCorners.target_eq, ModelWithCorners.mk_symm,
  PartialEquiv.coe_symm_mk, PartialHomeomorph.prod_apply, ModelWithCorners.mk_coe,
  PartialHomeomorph.prod_toPartialEquiv, PartialEquiv.prod_source, mk_preimage_prod,
  image_subset_iff]
Proof state after:
case refine_4
𝕜 : 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)
⊢ (fun x => ↑I.symm x.1) ⁻¹' f.target ∩ (fun x => ↑J.symm x.2) ⁻¹' g.target ∩
      interior (range fun x => (↑I x.1, ↑J x.2)) ⊆
    (fun x =>
        (↑I (↑(f.prod g).symm (↑I.symm x.1, ↑J.symm x.2)).1, ↑J (↑(f.prod g).symm (↑I.symm x.1, ↑J.symm x.2)).2)) ⁻¹'
      interior (range fun x => (↑I x.1, ↑J x.2))