Theorem: analyticGroupoid_prod
Proof state before:
𝕜 : 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)
⊢ f.prod g ∈ contDiffGroupoid ⊤ (I.prod J) ∧
    (AnalyticOn 𝕜 (fun x => ↑(I.prod J) (↑(f.prod g) (↑(I.prod J).symm x)))
          (↑(I.prod J).symm ⁻¹' (f.prod g).source ∩ interior (range ↑(I.prod J))) ∧
        ↑(I.prod J).symm ⁻¹' (f.prod g).source ∩ interior (range ↑(I.prod J)) ⊆
          (fun x => ↑(I.prod J) (↑(f.prod g) (↑(I.prod J).symm x))) ⁻¹' interior (range ↑(I.prod J))) ∧
      AnalyticOn 𝕜 (fun x => ↑(I.prod J) (↑(f.prod g).symm (↑(I.prod J).symm x)))
          (↑(I.prod J).symm ⁻¹' (f.prod g).target ∩ interior (range ↑(I.prod 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:
refine ⟨contDiffGroupoid_prod fa.1 ga.1, ⟨?_, ?_⟩, ⟨?_, ?_⟩⟩
Proof state after:
case refine_1
𝕜 : 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)
⊢ AnalyticOn 𝕜 (fun x => ↑(I.prod J) (↑(f.prod g) (↑(I.prod J).symm x)))
    (↑(I.prod J).symm ⁻¹' (f.prod g).source ∩ interior (range ↑(I.prod J)))

case refine_2
𝕜 : 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).source ∩ interior (range ↑(I.prod J)) ⊆
    (fun x => ↑(I.prod J) (↑(f.prod g) (↑(I.prod J).symm x))) ⁻¹' interior (range ↑(I.prod J))

case refine_3
𝕜 : 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)
⊢ AnalyticOn 𝕜 (fun x => ↑(I.prod J) (↑(f.prod g).symm (↑(I.prod J).symm x)))
    (↑(I.prod J).symm ⁻¹' (f.prod g).target ∩ interior (range ↑(I.prod J)))

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