awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : Circle → ℂ := Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
⊢ ContMDiff (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (z : ℂ × ℂ) ↦ z.1 * z.2

Tactic:
have h₂ : ContMDiff (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) ω fun z : ℂ × ℂ => z.fst * z.snd := by
      rw [contMDiff_iff]
      exact ⟨continuous_mul, fun x y => contDiff_mul.contDiffOn⟩
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : Circle → ℂ := Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
h₂ : ContMDiff (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (z : ℂ × ℂ) ↦ z.1 * z.2
hf :
  ContMDiff (E := EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) (ModelWithCorners.prod (𝓡 1) (𝓡 1))
    (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) ω (Prod.map c c)
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) (ModelWithCorners.prod (𝓡 1) (𝓡 1)) 𝓘(ℝ, ℂ)
    (M' := ℂ) ω fun (p : Circle × Circle) ↦ (↑p.1 : ℂ) * (↑p.2 : ℂ)

Tactic:
suffices h₁ : ContMDiff _ _ _ (Prod.map c c) from
      h₂.comp h₁
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : Circle → ℂ := Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
h₂ : ContMDiff (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (z : ℂ × ℂ) ↦ z.1 * z.2
hf hf₁ : ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) 𝓘(ℝ, ℂ) ω c
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) (ModelWithCorners.prod (𝓡 1) (𝓡 1))
    (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) ω (Prod.map c c)

Tactic:
apply ContMDiff.prodMap

Premises used: ContMDiff.prodMap
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : Circle → ℂ := Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
h₂ : ContMDiff (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (z : ℂ × ℂ) ↦ z.1 * z.2
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) 𝓘(ℝ, ℂ) ω c

Tactic:
contMDiff_coe_sphere

Premises used: Set.Mem, contMDiff_coe_sphere, setOf, Circle, Metric.sphere
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : Circle → ℂ := Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
h₂ : ContMDiff (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (z : ℂ × ℂ) ↦ z.1 * z.2
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) 𝓘(ℝ, ℂ) ω c

Tactic:
exact contMDiff_coe_sphere

Premises used: contMDiff_coe_sphere
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
hf : ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (a : Circle) ↦ (↑a : ℂ)⁻¹
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) (E' := EuclideanSpace ℝ (Fin 1)) (𝓡 1) (M' := Circle) ω
    fun (a : Circle) ↦ a⁻¹

Tactic:
apply ContMDiff.codRestrict_sphere

Premises used: ContMDiff.codRestrict_sphere
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
hf :
  ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (a : Circle) ↦
    (starRingEnd ℂ : (a : ℂ) → ℂ) (↑a : ℂ)
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (a : Circle) ↦ (↑a : ℂ)⁻¹

Tactic:
simp only [← Circle.coe_inv, Circle.coe_inv_eq_conj]

Premises used: Circle.coe_inv_eq_conj, Circle.coe_inv
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (a : Circle) ↦
    (starRingEnd ℂ : (a : ℂ) → ℂ) (↑a : ℂ)

Tactic:
Complex.conjCLE.contDiff.contMDiff.comp contMDiff_coe_sphere

Premises used: ContMDiff.comp, contMDiff_coe_sphere, ContDiff.contMDiff, Complex.conjCLE, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (a : Circle) ↦
    (starRingEnd ℂ : (a : ℂ) → ℂ) (↑a : ℂ)

Tactic:
exact Complex.conjCLE.contDiff.contMDiff.comp contMDiff_coe_sphere

Premises used: ContMDiff.comp, contMDiff_coe_sphere, ContDiff.contMDiff, Complex.conjCLE, ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
m : ℕ∞ω
⊢ ContMDiff 𝓘(ℝ, ℝ) (M := ℝ) (E' := EuclideanSpace ℝ (Fin 1)) (𝓡 1) (M' := Circle) m (⇑Circle.exp : (a : ℝ) → Circle)

Tactic:
(contDiff_exp.comp (contDiff_id.smul contDiff_const)).contMDiff.codRestrict_sphere _

Premises used: contDiff_id, Set.Mem, setOf, contDiff_const, Complex.contDiff_exp, ContDiff.contMDiff, ContDiff.comp, ContDiff.smul, Circle, Set.codRestrict, ContMDiff.codRestrict_sphere, Metric.sphere
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
a b : Rˣ
⊢ (↑(chartAt R a) : Rˣ → R) b = (↑b : R)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
a : Rˣ
⊢ (OpenPartialHomeomorph.toPartialEquiv (chartAt R a)).source = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
⊢ IsManifold 𝓘(𝕜, R) n Rˣ

Tactic:
isOpenEmbedding_val.isManifold_singleton

Premises used: Topology.IsOpenEmbedding.isManifold_singleton, Units.isOpenEmbedding_val
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
⊢ ContMDiff 𝓘(𝕜, R) (M := Rˣ) 𝓘(𝕜, R) n val

Tactic:
contMDiff_isOpenEmbedding Units.isOpenEmbedding_val

Premises used: contMDiff_isOpenEmbedding, Units.isOpenEmbedding_val
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
apply :
  ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (M := Rˣ × Rˣ) 𝓘(𝕜, R) (M' := R) n
    (Function.comp (β := Rˣ) val fun (p : Rˣ × Rˣ) ↦ p.1 * p.2)
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) 𝓘(𝕜, R) (M' := Rˣ) n fun (p : Rˣ × Rˣ) ↦ p.1 * p.2

Tactic:
apply ContMDiff.of_comp_isOpenEmbedding Units.isOpenEmbedding_val

Premises used: ContMDiff.of_comp_isOpenEmbedding, Units.isOpenEmbedding_val
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
h :
  ∀ (x : Rˣ × Rˣ),
    Eq (α := R) (Function.comp (β := Rˣ) val (fun (x : Rˣ × Rˣ) ↦ x.1 * x.2) x)
      (((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R))) x)
⊢ Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
x : Rˣ × Rˣ
⊢ Eq (α := R) (Function.comp (β := Rˣ) val (fun (x : Rˣ × Rˣ) ↦ x.1 * x.2) x)
    (((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R))) x)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
⊢ Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))

Tactic:
have : (val : Rˣ → R) ∘ (fun x : Rˣ × Rˣ => x.1 * x.2) =
      (fun x : R × R => x.1 * x.2) ∘ (fun x : Rˣ × Rˣ => (x.1, x.2)) := by ext; simp
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this :
  Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
rw :
  ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (M := Rˣ × Rˣ) 𝓘(𝕜, R) (M' := R) n
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (M := Rˣ × Rˣ) 𝓘(𝕜, R) (M' := R) n
    (Function.comp (β := Rˣ) val fun (p : Rˣ × Rˣ) ↦ p.1 * p.2)

Tactic:
rw [this]
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this :
  Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (E' := R × R) 𝓘(𝕜, R × R) (M' := R × R) n fun (x : Rˣ × Rˣ) ↦
    ((↑x.1 : R), (↑x.2 : R))

Tactic:
have : ContMDiff (𝓘(𝕜, R).prod 𝓘(𝕜, R)) 𝓘(𝕜, R × R) n
      (fun x : Rˣ × Rˣ => ((x.1 : R), (x.2 : R))) :=
      (contMDiff_val.comp contMDiff_fst).prodMk_space (contMDiff_val.comp contMDiff_snd)
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this_1 :
  Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
this :
  ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (E' := R × R) 𝓘(𝕜, R × R) (M' := R × R) n fun (x : Rˣ × Rˣ) ↦
    ((↑x.1 : R), (↑x.2 : R))
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (M := Rˣ × Rˣ) 𝓘(𝕜, R) (M' := R) n
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))

Tactic:
ContMDiff.comp ?_ this

Premises used: ContMDiff.comp
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this_1 :
  Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
this :
  ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (E' := R × R) 𝓘(𝕜, R × R) (M' := R × R) n fun (x : Rˣ × Rˣ) ↦
    ((↑x.1 : R), (↑x.2 : R))
refine : ContMDiff (E := R × R) 𝓘(𝕜, R × R) 𝓘(𝕜, R) (M' := R) n fun (x : R × R) ↦ x.1 * x.2
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (M := Rˣ × Rˣ) 𝓘(𝕜, R) (M' := R) n
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))

Tactic:
refine ContMDiff.comp ?_ this

Premises used: ContMDiff.comp
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this_1 :
  Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
this :
  ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (E' := R × R) 𝓘(𝕜, R × R) (M' := R × R) n fun (x : Rˣ × Rˣ) ↦
    ((↑x.1 : R), (↑x.2 : R))
rw : ContDiff 𝕜 (F := R) n fun (x : R × R) ↦ x.1 * x.2
⊢ ContMDiff (E := R × R) 𝓘(𝕜, R × R) 𝓘(𝕜, R) (M' := R) n fun (x : R × R) ↦ x.1 * x.2

Tactic:
rw [contMDiff_iff_contDiff]

Premises used: contMDiff_iff_contDiff
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this_1 :
  Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
this :
  ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (E' := R × R) 𝓘(𝕜, R × R) (M' := R × R) n fun (x : Rˣ × Rˣ) ↦
    ((↑x.1 : R), (↑x.2 : R))
⊢ ContDiff 𝕜 (F := R) n fun (x : R × R) ↦ x.1 * x.2

Tactic:
contDiff_mul

Premises used: contDiff_mul
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this_1 :
  Eq.{u_1 + 1} (α := Rˣ × Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ × Rˣ) ↦ x.1 * x.2)
    ((fun (x : R × R) ↦ x.1 * x.2) ∘ fun (x : Rˣ × Rˣ) ↦ ((↑x.1 : R), (↑x.2 : R)))
this :
  ContMDiff (ModelWithCorners.prod 𝓘(𝕜, R) 𝓘(𝕜, R)) (E' := R × R) 𝓘(𝕜, R × R) (M' := R × R) n fun (x : Rˣ × Rˣ) ↦
    ((↑x.1 : R), (↑x.2 : R))
⊢ ContDiff 𝕜 (F := R) n fun (x : R × R) ↦ x.1 * x.2

Tactic:
exact contDiff_mul

Premises used: contDiff_mul
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
apply : ContMDiff 𝓘(𝕜, R) (M := Rˣ) 𝓘(𝕜, R) (M' := R) n (Function.comp (β := Rˣ) val fun (a : Rˣ) ↦ a⁻¹)
⊢ ContMDiff 𝓘(𝕜, R) 𝓘(𝕜, R) (M' := Rˣ) n fun (a : Rˣ) ↦ a⁻¹

Tactic:
apply ContMDiff.of_comp_isOpenEmbedding Units.isOpenEmbedding_val

Premises used: ContMDiff.of_comp_isOpenEmbedding, Units.isOpenEmbedding_val
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
h : ∀ (x : Rˣ), Function.comp (β := Rˣ) val (fun (x : Rˣ) ↦ x⁻¹) x = (Ring.inverse ∘ val) x
⊢ Eq.{u_1 + 1} (α := Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ) ↦ x⁻¹) (Ring.inverse ∘ val)

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
x : Rˣ
⊢ Function.comp (β := Rˣ) val (fun (x : Rˣ) ↦ x⁻¹) x = (Ring.inverse ∘ val) x

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
⊢ Eq.{u_1 + 1} (α := Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ) ↦ x⁻¹) (Ring.inverse ∘ val)

Tactic:
have : (val : Rˣ → R) ∘ (fun x : Rˣ => x⁻¹) = Ring.inverse ∘ val := by ext; simp
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this : Eq.{u_1 + 1} (α := Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ) ↦ x⁻¹) (Ring.inverse ∘ val)
rw : ∀ (x : Rˣ), ContMDiffAt 𝓘(𝕜, R) 𝓘(𝕜, R) n (Ring.inverse ∘ val) x
⊢ ContMDiff 𝓘(𝕜, R) (M := Rˣ) 𝓘(𝕜, R) (M' := R) n (Function.comp (β := Rˣ) val fun (a : Rˣ) ↦ a⁻¹)

Tactic:
rw [this, ContMDiff]

Premises used: ContMDiff
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this : Eq.{u_1 + 1} (α := Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ) ↦ x⁻¹) (Ring.inverse ∘ val)
⊢ ∀ (x : Rˣ), ContMDiffAt 𝓘(𝕜, R) 𝓘(𝕜, R) n (Ring.inverse ∘ val) x

Tactic:
fun x => ContMDiffAt.comp x ?_ (contMDiff_val x)

Premises used: Units.contMDiff_val, ContMDiffAt.comp
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this : Eq.{u_1 + 1} (α := Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ) ↦ x⁻¹) (Ring.inverse ∘ val)
refine : ∀ (x : Rˣ), ContMDiffAt 𝓘(𝕜, R) 𝓘(𝕜, R) n Ring.inverse (↑x : R)
⊢ ∀ (x : Rˣ), ContMDiffAt 𝓘(𝕜, R) 𝓘(𝕜, R) n (Ring.inverse ∘ val) x

Tactic:
refine fun x => ContMDiffAt.comp x ?_ (contMDiff_val x)

Premises used: Units.contMDiff_val, ContMDiffAt.comp
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this : Eq.{u_1 + 1} (α := Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ) ↦ x⁻¹) (Ring.inverse ∘ val)
x : Rˣ
rw : ContDiffAt 𝕜 n Ring.inverse (↑x : R)
⊢ ContMDiffAt 𝓘(𝕜, R) 𝓘(𝕜, R) n Ring.inverse (↑x : R)

Tactic:
rw [contMDiffAt_iff_contDiffAt]

Premises used: contMDiffAt_iff_contDiffAt
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this : Eq.{u_1 + 1} (α := Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ) ↦ x⁻¹) (Ring.inverse ∘ val)
x : Rˣ
⊢ ContDiffAt 𝕜 n Ring.inverse (↑x : R)

Tactic:
contDiffAt_ringInverse _ _

Premises used: contDiffAt_ringInverse
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
this : Eq.{u_1 + 1} (α := Rˣ → R) (Function.comp (β := Rˣ) val fun (x : Rˣ) ↦ x⁻¹) (Ring.inverse ∘ val)
x : Rˣ
⊢ ContDiffAt 𝕜 n Ring.inverse (↑x : R)

Tactic:
exact contDiffAt_ringInverse _ _

Premises used: contDiffAt_ringInverse
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : MulAction R M
inst_10 : ContMDiffSMul 𝓘(𝕜, R) I n R M
⊢ ContMDiffSMul 𝓘(𝕜, R) I n Rˣ M

Tactic:
MulAction.contMDiffSMul_compHom (f := coeHom R) contMDiff_val

Premises used: MulAction.contMDiffSMul_compHom, SMul.comp.smul, Units.contMDiff_val
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n_1 : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
V : Type u_6
inst_9 : NormedAddCommGroup V
inst_10 : NormedSpace 𝕜 V
inst_11 : CompleteSpace V
n : ℕ∞ω
⊢ LieGroup.{u_2, u_6, u_6, u_6} (H := V →L[𝕜] V) 𝓘(𝕜, V →L[𝕜] V) n (V →L[𝕜] V)ˣ

Tactic:
inferInstance

Premises used: inferInstance