-- Mathlib/Geometry/Manifold/AnalyticManifold.lean
theorem analyticGroupoid_prod {E A : Type} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    [TopologicalSpace A] {F B : Type} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
    [TopologicalSpace B] {I : ModelWithCorners 𝕜 E A} {J : ModelWithCorners 𝕜 F B}
    {f : PartialHomeomorph A A} {g : PartialHomeomorph B B}
    (fa : f ∈ analyticGroupoid I) (ga : g ∈ analyticGroupoid J) :
    f.prod g ∈ analyticGroupoid (I.prod J)

Proof state:
𝕜 : Type u_1
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
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
pe : range ↑(I.prod J) = (range ↑I).prod (range ↑J)
⊢ f.prod g ∈ analyticGroupoid (I.prod J)

Tactic:
simp only [mem_analyticGroupoid, Function.comp, image_subset_iff] at fa ga ⊢

Result:
𝕜 : Type u_1
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
pe : range ↑(I.prod J) = (range ↑I).prod (range ↑J)
fa :
  AnalyticOn 𝕜 (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ range ↑I) ∧
    AnalyticOn 𝕜 (↑I ∘ ↑f.symm ∘ ↑I.symm) (↑I.symm ⁻¹' f.target ∩ range ↑I)
ga :
  AnalyticOn 𝕜 (↑J ∘ ↑g ∘ ↑J.symm) (↑J.symm ⁻¹' g.source ∩ range ↑J) ∧
    AnalyticOn 𝕜 (↑J ∘ ↑g.symm ∘ ↑J.symm) (↑J.symm ⁻¹' g.target ∩ range ↑J)
⊢ AnalyticOn 𝕜 (↑(I.prod J) ∘ ↑(f.prod g) ∘ ↑(I.prod J).symm)
      (↑(I.prod J).symm ⁻¹' (f.prod g).source ∩ range ↑(I.prod J)) ∧
    AnalyticOn 𝕜 (↑(I.prod J) ∘ ↑(f.prod g).symm ∘ ↑(I.prod J).symm)
      (↑(I.prod J).symm ⁻¹' (f.prod g).target ∩ range ↑(I.prod J))

Proof state:
𝕜 : Type u_1
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
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
⊢ f.prod g ∈ analyticGroupoid (I.prod J)

Tactic:
have pe : range (I.prod J) = (range I).prod (range J) := I.range_prod

Result:
𝕜 : Type u_1
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
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
pe : range ↑(I.prod J) = (range ↑I).prod (range ↑J)
⊢ f.prod g ∈ analyticGroupoid (I.prod J)

Proof state:
𝕜 : Type u_1
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
pe : range ↑(I.prod J) = (range ↑I).prod (range ↑J)
fa :
  AnalyticOn 𝕜 (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ range ↑I) ∧
    AnalyticOn 𝕜 (↑I ∘ ↑f.symm ∘ ↑I.symm) (↑I.symm ⁻¹' f.target ∩ range ↑I)
ga :
  AnalyticOn 𝕜 (↑J ∘ ↑g ∘ ↑J.symm) (↑J.symm ⁻¹' g.source ∩ range ↑J) ∧
    AnalyticOn 𝕜 (↑J ∘ ↑g.symm ∘ ↑J.symm) (↑J.symm ⁻¹' g.target ∩ range ↑J)
⊢ AnalyticOn 𝕜 (↑(I.prod J) ∘ ↑(f.prod g) ∘ ↑(I.prod J).symm)
      (↑(I.prod J).symm ⁻¹' (f.prod g).source ∩ range ↑(I.prod J)) ∧
    AnalyticOn 𝕜 (↑(I.prod J) ∘ ↑(f.prod g).symm ∘ ↑(I.prod J).symm)
      (↑(I.prod J).symm ⁻¹' (f.prod g).target ∩ range ↑(I.prod J))

Tactic:
exact ⟨AnalyticOn.prod
    (fa.1.comp analyticOn_fst fun _ m ↦ ⟨m.1.1, (pe ▸ m.2).1⟩)
    (ga.1.comp analyticOn_snd fun _ m ↦ ⟨m.1.2, (pe ▸ m.2).2⟩),
  AnalyticOn.prod
    (fa.2.comp analyticOn_fst fun _ m ↦ ⟨m.1.1, (pe ▸ m.2).1⟩)
    (ga.2.comp analyticOn_snd fun _ m ↦ ⟨m.1.2, (pe ▸ m.2).2⟩)⟩

Result:
no goals