Theorem: analyticGroupoid_prod (Ray/AnalyticManifold/AnalyticManifold.lean)

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
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
⊢ f.prod g ∈ analyticGroupoid (I.prod J)
Tactic:
have er : (range fun x : A × B ↦ (I x.1, J x.2)) = range I ×ˢ range J := range_prod_map
State after:
𝕜 : 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
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
⊢ f.prod g ∈ analyticGroupoid (I.prod J)

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
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
⊢ f.prod g ∈ analyticGroupoid (I.prod J)
Tactic:
have ei : interior (range fun x : A × B ↦ (I x.1, J x.2)) =
    interior (range I) ×ˢ interior (range J) := by rw [er, interior_prod_eq]
State after:
𝕜 : 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
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
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)
⊢ f.prod g ∈ analyticGroupoid (I.prod J)

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
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
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)
⊢ f.prod g ∈ analyticGroupoid (I.prod J)
Tactic:
simp only [mem_analyticGroupoid, Function.comp, image_subset_iff] at fa ga ⊢
State after:
𝕜 : 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))

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, ⟨?_, ?_⟩, ⟨?_, ?_⟩⟩
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))

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
fa : f ∈ analyticGroupoid I
ga : g ∈ analyticGroupoid J
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
⊢ interior (range fun x => (↑I x.1, ↑J x.2)) = interior (range ↑I) ×ˢ interior (range ↑J)
Tactic:
rw [er, interior_prod_eq]
State after:
no goals

State before:
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)))
Tactic:
apply AnalyticOn.prod
State after:
case refine_1.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)
⊢ AnalyticOn 𝕜 (fun x => ↑I (↑(f.prod g) (↑(I.prod J).symm x)).1)
    (↑(I.prod J).symm ⁻¹' (f.prod g).source ∩ interior (range ↑(I.prod J)))

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

State before:
case refine_1.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)
⊢ AnalyticOn 𝕜 (fun x => ↑I (↑(f.prod g) (↑(I.prod J).symm x)).1)
    (↑(I.prod J).symm ⁻¹' (f.prod g).source ∩ interior (range ↑(I.prod J)))
Tactic:
simp only [ModelWithCorners.symm, modelWithCorners_prod_toPartialEquiv,
  PartialEquiv.prod_symm, PartialEquiv.prod_coe, ModelWithCorners.toPartialEquiv_coe_symm,
  PartialHomeomorph.prod_apply, PartialHomeomorph.prod_toPartialEquiv,
  PartialEquiv.prod_source]
State after:
case refine_1.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)
⊢ AnalyticOn 𝕜 (fun x => ↑I (↑f (↑I.symm x.1)))
    ((fun p => (↑I.symm p.1, ↑J.symm p.2)) ⁻¹' f.source ×ˢ g.source ∩ interior (range ↑(I.prod J)))

State before:
case refine_1.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)
⊢ AnalyticOn 𝕜 (fun x => ↑I (↑f (↑I.symm x.1)))
    ((fun p => (↑I.symm p.1, ↑J.symm p.2)) ⁻¹' f.source ×ˢ g.source ∩ interior (range ↑(I.prod J)))
Tactic:
refine fa.2.1.1.comp (analyticOn_fst _) ?_
State after:
case refine_1.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.source ×ˢ g.source ∩ interior (range ↑(I.prod J)))
    (↑I.symm ⁻¹' f.source ∩ interior (range ↑I))

State before:
case refine_1.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.source ×ˢ g.source ∩ interior (range ↑(I.prod J)))
    (↑I.symm ⁻¹' f.source ∩ interior (range ↑I))
Tactic:
intro x m
State after:
case refine_1.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.source ×ˢ g.source ∩ interior (range ↑(I.prod J))
⊢ (fun x => x.1) x ∈ ↑I.symm ⁻¹' f.source ∩ interior (range ↑I)

State before:
case refine_1.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.source ×ˢ g.source ∩ interior (range ↑(I.prod J))
⊢ (fun x => x.1) x ∈ ↑I.symm ⁻¹' f.source ∩ interior (range ↑I)
Tactic:
simp only [ModelWithCorners.prod, ModelWithCorners.source_eq, mem_univ, and_self, setOf_true,
  PartialEquiv.prod_target, ModelWithCorners.target_eq, ModelWithCorners.mk_coe,
  mem_inter_iff, mem_preimage, mem_prod] at m ⊢
State after:
case refine_1.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 : (↑I.symm x.1 ∈ f.source ∧ ↑J.symm x.2 ∈ g.source) ∧ x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ ↑I.symm x.1 ∈ f.source ∧ x.1 ∈ interior (range ↑I)

State before:
case refine_1.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 : (↑I.symm x.1 ∈ f.source ∧ ↑J.symm x.2 ∈ g.source) ∧ x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ ↑I.symm x.1 ∈ f.source ∧ x.1 ∈ interior (range ↑I)
Tactic:
exact ⟨m.1.1, (subset_of_eq ei m.2).1⟩
State after:
no goals

State before:
case refine_1.hg
𝕜 : 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 => ↑J (↑(f.prod g) (↑(I.prod J).symm x)).2)
    (↑(I.prod J).symm ⁻¹' (f.prod g).source ∩ interior (range ↑(I.prod J)))
Tactic:
simp only [ModelWithCorners.symm, modelWithCorners_prod_toPartialEquiv,
  PartialEquiv.prod_symm, PartialEquiv.prod_coe, ModelWithCorners.toPartialEquiv_coe_symm,
  PartialHomeomorph.prod_apply, PartialHomeomorph.prod_toPartialEquiv,
  PartialEquiv.prod_source]
State after:
case refine_1.hg
𝕜 : 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 => ↑J (↑g (↑J.symm x.2)))
    ((fun p => (↑I.symm p.1, ↑J.symm p.2)) ⁻¹' f.source ×ˢ g.source ∩ interior (range ↑(I.prod J)))

State before:
case refine_1.hg
𝕜 : 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 => ↑J (↑g (↑J.symm x.2)))
    ((fun p => (↑I.symm p.1, ↑J.symm p.2)) ⁻¹' f.source ×ˢ g.source ∩ interior (range ↑(I.prod J)))
Tactic:
refine ga.2.1.1.comp (analyticOn_snd _) ?_
State after:
case refine_1.hg
𝕜 : 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.2) ((fun p => (↑I.symm p.1, ↑J.symm p.2)) ⁻¹' f.source ×ˢ g.source ∩ interior (range ↑(I.prod J)))
    (↑J.symm ⁻¹' g.source ∩ interior (range ↑J))

State before:
case refine_1.hg
𝕜 : 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.2) ((fun p => (↑I.symm p.1, ↑J.symm p.2)) ⁻¹' f.source ×ˢ g.source ∩ interior (range ↑(I.prod J)))
    (↑J.symm ⁻¹' g.source ∩ interior (range ↑J))
Tactic:
intro x m
State after:
case refine_1.hg
𝕜 : 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.source ×ˢ g.source ∩ interior (range ↑(I.prod J))
⊢ (fun x => x.2) x ∈ ↑J.symm ⁻¹' g.source ∩ interior (range ↑J)

State before:
case refine_1.hg
𝕜 : 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.source ×ˢ g.source ∩ interior (range ↑(I.prod J))
⊢ (fun x => x.2) x ∈ ↑J.symm ⁻¹' g.source ∩ interior (range ↑J)
Tactic:
simp only [ModelWithCorners.prod, ModelWithCorners.source_eq, mem_univ, and_self, setOf_true,
  PartialEquiv.prod_target, ModelWithCorners.target_eq, ModelWithCorners.mk_coe,
  mem_inter_iff, mem_preimage, mem_prod] at m ⊢
State after:
case refine_1.hg
𝕜 : 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 : (↑I.symm x.1 ∈ f.source ∧ ↑J.symm x.2 ∈ g.source) ∧ x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ ↑J.symm x.2 ∈ g.source ∧ x.2 ∈ interior (range ↑J)

State before:
case refine_1.hg
𝕜 : 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 : (↑I.symm x.1 ∈ f.source ∧ ↑J.symm x.2 ∈ g.source) ∧ x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ ↑J.symm x.2 ∈ g.source ∧ x.2 ∈ interior (range ↑J)
Tactic:
exact ⟨m.1.2, (subset_of_eq ei m.2).2⟩
State after:
no goals

State before:
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))
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]
State after:
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)
⊢ (fun x => ↑I.symm x.1) ⁻¹' f.source ∩ (fun x => ↑J.symm x.2) ⁻¹' g.source ∩
      interior (range fun x => (↑I x.1, ↑J x.2)) ⊆
    (fun x => (↑I (↑f (↑I.symm x.1)), ↑J (↑g (↑J.symm x.2)))) ⁻¹' interior (range fun x => (↑I x.1, ↑J x.2))

State before:
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)
⊢ (fun x => ↑I.symm x.1) ⁻¹' f.source ∩ (fun x => ↑J.symm x.2) ⁻¹' g.source ∩
      interior (range fun x => (↑I x.1, ↑J x.2)) ⊆
    (fun x => (↑I (↑f (↑I.symm x.1)), ↑J (↑g (↑J.symm x.2)))) ⁻¹' interior (range fun x => (↑I x.1, ↑J x.2))
Tactic:
intro x ⟨⟨m0,m1⟩,m2⟩
State after:
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)
x : E × F
m0 : x ∈ (fun x => ↑I.symm x.1) ⁻¹' f.source
m1 : x ∈ (fun x => ↑J.symm x.2) ⁻¹' g.source
m2 : x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ x ∈ (fun x => (↑I (↑f (↑I.symm x.1)), ↑J (↑g (↑J.symm x.2)))) ⁻¹' interior (range fun x => (↑I x.1, ↑J x.2))

State before:
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)
x : E × F
m0 : x ∈ (fun x => ↑I.symm x.1) ⁻¹' f.source
m1 : x ∈ (fun x => ↑J.symm x.2) ⁻¹' g.source
m2 : x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ x ∈ (fun x => (↑I (↑f (↑I.symm x.1)), ↑J (↑g (↑J.symm x.2)))) ⁻¹' interior (range fun x => (↑I x.1, ↑J x.2))
Tactic:
replace m2 := subset_of_eq ei m2
State after:
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)
x : E × F
m0 : x ∈ (fun x => ↑I.symm x.1) ⁻¹' f.source
m1 : x ∈ (fun x => ↑J.symm x.2) ⁻¹' g.source
m2 : x ∈ interior (range ↑I) ×ˢ interior (range ↑J)
⊢ x ∈ (fun x => (↑I (↑f (↑I.symm x.1)), ↑J (↑g (↑J.symm x.2)))) ⁻¹' interior (range fun x => (↑I x.1, ↑J x.2))

State before:
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)
x : E × F
m0 : x ∈ (fun x => ↑I.symm x.1) ⁻¹' f.source
m1 : x ∈ (fun x => ↑J.symm x.2) ⁻¹' g.source
m2 : x ∈ interior (range ↑I) ×ˢ interior (range ↑J)
⊢ x ∈ (fun x => (↑I (↑f (↑I.symm x.1)), ↑J (↑g (↑J.symm x.2)))) ⁻¹' interior (range fun x => (↑I x.1, ↑J x.2))
Tactic:
exact subset_of_eq ei.symm ⟨fa.2.1.2 ⟨m0,m2.1⟩, ga.2.1.2 ⟨m1,m2.2⟩⟩
State after:
no goals

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

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

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)
⊢ AnalyticOn 𝕜 (fun x => ↑I (↑(f.prod g).symm (↑(I.prod J).symm x)).1)
    (↑(I.prod J).symm ⁻¹' (f.prod g).target ∩ interior (range ↑(I.prod J)))
Tactic:
simp only [ModelWithCorners.symm, modelWithCorners_prod_toPartialEquiv,
  PartialEquiv.prod_symm, PartialEquiv.prod_coe, ModelWithCorners.toPartialEquiv_coe_symm,
  PartialHomeomorph.prod_apply, PartialHomeomorph.prod_toPartialEquiv,
  PartialEquiv.prod_source]
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)
⊢ AnalyticOn 𝕜 (fun x => ↑I (↑(f.prod g).symm (↑I.symm x.1, ↑J.symm x.2)).1)
    ((fun p => (↑I.symm p.1, ↑J.symm p.2)) ⁻¹' (f.prod g.toPartialEquiv).target ∩ interior (range ↑(I.prod J)))

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)
⊢ AnalyticOn 𝕜 (fun x => ↑I (↑(f.prod g).symm (↑I.symm x.1, ↑J.symm x.2)).1)
    ((fun p => (↑I.symm p.1, ↑J.symm p.2)) ⁻¹' (f.prod g.toPartialEquiv).target ∩ interior (range ↑(I.prod J)))
Tactic:
refine fa.2.2.1.comp (analyticOn_fst _) ?_
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)
⊢ 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))

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

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)
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)
Tactic:
simp only [ModelWithCorners.prod, ModelWithCorners.source_eq, mem_univ, and_self, setOf_true,
  PartialEquiv.prod_target, ModelWithCorners.target_eq, ModelWithCorners.mk_coe,
  mem_inter_iff, mem_preimage, mem_prod] at m ⊢
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 : (↑I.symm x.1 ∈ f.target ∧ ↑J.symm x.2 ∈ g.target) ∧ x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ ↑I.symm x.1 ∈ f.target ∧ x.1 ∈ interior (range ↑I)

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)
x : E × F
m : (↑I.symm x.1 ∈ f.target ∧ ↑J.symm x.2 ∈ g.target) ∧ x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ ↑I.symm x.1 ∈ f.target ∧ x.1 ∈ interior (range ↑I)
Tactic:
exact ⟨m.1.1, (subset_of_eq ei m.2).1⟩
State after:
no goals

State before:
case refine_3.hg
𝕜 : 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 => ↑J (↑(f.prod g).symm (↑(I.prod J).symm x)).2)
    (↑(I.prod J).symm ⁻¹' (f.prod g).target ∩ interior (range ↑(I.prod J)))
Tactic:
simp only [ModelWithCorners.symm, modelWithCorners_prod_toPartialEquiv,
  PartialEquiv.prod_symm, PartialEquiv.prod_coe, ModelWithCorners.toPartialEquiv_coe_symm,
  PartialHomeomorph.prod_apply, PartialHomeomorph.prod_toPartialEquiv,
  PartialEquiv.prod_source]
State after:
case refine_3.hg
𝕜 : 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 => ↑J (↑(f.prod g).symm (↑I.symm x.1, ↑J.symm x.2)).2)
    ((fun p => (↑I.symm p.1, ↑J.symm p.2)) ⁻¹' (f.prod g.toPartialEquiv).target ∩ interior (range ↑(I.prod J)))

State before:
case refine_3.hg
𝕜 : 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 => ↑J (↑(f.prod g).symm (↑I.symm x.1, ↑J.symm x.2)).2)
    ((fun p => (↑I.symm p.1, ↑J.symm p.2)) ⁻¹' (f.prod g.toPartialEquiv).target ∩ interior (range ↑(I.prod J)))
Tactic:
refine ga.2.2.1.comp (analyticOn_snd _) ?_
State after:
case refine_3.hg
𝕜 : 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.2)
    ((fun p => (↑I.symm p.1, ↑J.symm p.2)) ⁻¹' (f.prod g.toPartialEquiv).target ∩ interior (range ↑(I.prod J)))
    (↑J.symm ⁻¹' g.target ∩ interior (range ↑J))

State before:
case refine_3.hg
𝕜 : 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.2)
    ((fun p => (↑I.symm p.1, ↑J.symm p.2)) ⁻¹' (f.prod g.toPartialEquiv).target ∩ interior (range ↑(I.prod J)))
    (↑J.symm ⁻¹' g.target ∩ interior (range ↑J))
Tactic:
intro x m
State after:
case refine_3.hg
𝕜 : 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.2) x ∈ ↑J.symm ⁻¹' g.target ∩ interior (range ↑J)

State before:
case refine_3.hg
𝕜 : 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.2) x ∈ ↑J.symm ⁻¹' g.target ∩ interior (range ↑J)
Tactic:
simp only [ModelWithCorners.prod, ModelWithCorners.source_eq, mem_univ, and_self, setOf_true,
  PartialEquiv.prod_target, ModelWithCorners.target_eq, ModelWithCorners.mk_coe,
  mem_inter_iff, mem_preimage, mem_prod] at m ⊢
State after:
case refine_3.hg
𝕜 : 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 : (↑I.symm x.1 ∈ f.target ∧ ↑J.symm x.2 ∈ g.target) ∧ x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ ↑J.symm x.2 ∈ g.target ∧ x.2 ∈ interior (range ↑J)

State before:
case refine_3.hg
𝕜 : 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 : (↑I.symm x.1 ∈ f.target ∧ ↑J.symm x.2 ∈ g.target) ∧ x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ ↑J.symm x.2 ∈ g.target ∧ x.2 ∈ interior (range ↑J)
Tactic:
exact ⟨m.1.2, (subset_of_eq ei m.2).2⟩
State after:
no goals

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

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)
⊢ (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))
Tactic:
intro x ⟨⟨m0,m1⟩,m2⟩
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)
x : E × F
m0 : x ∈ (fun x => ↑I.symm x.1) ⁻¹' f.target
m1 : x ∈ (fun x => ↑J.symm x.2) ⁻¹' g.target
m2 : x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ x ∈
    (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))

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)
x : E × F
m0 : x ∈ (fun x => ↑I.symm x.1) ⁻¹' f.target
m1 : x ∈ (fun x => ↑J.symm x.2) ⁻¹' g.target
m2 : x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ x ∈
    (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))
Tactic:
replace m2 := subset_of_eq ei m2
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)
x : E × F
m0 : x ∈ (fun x => ↑I.symm x.1) ⁻¹' f.target
m1 : x ∈ (fun x => ↑J.symm x.2) ⁻¹' g.target
m2 : x ∈ interior (range ↑I) ×ˢ interior (range ↑J)
⊢ x ∈
    (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))

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)
x : E × F
m0 : x ∈ (fun x => ↑I.symm x.1) ⁻¹' f.target
m1 : x ∈ (fun x => ↑J.symm x.2) ⁻¹' g.target
m2 : x ∈ interior (range ↑I) ×ˢ interior (range ↑J)
⊢ x ∈
    (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))
Tactic:
exact subset_of_eq ei.symm ⟨fa.2.2.2 ⟨m0,m2.1⟩, ga.2.2.2 ⟨m1,m2.2⟩⟩
State after:
no goals