awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_3
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
F' : Type u_4
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
s : Set E
t : Set E'
f : E → F
g : E' → F'
p : E × E'
hf : ContDiffWithinAt 𝕜 n f s p.1
hg : ContDiffWithinAt 𝕜 n g t p.2
⊢ ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) p

Tactic:
(hf.comp p contDiffWithinAt_fst (prod_subset_preimage_fst _ _)).prodMk
    (hg.comp p contDiffWithinAt_snd (prod_subset_preimage_snd _ _))

Premises used: contDiffWithinAt_fst, Set.prod_subset_preimage_fst, ContDiffWithinAt.comp, Prod.map, Set.prod_subset_preimage_snd, contDiffWithinAt_snd, ContDiffWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_3
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
F' : Type u_4
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
s : Set E
t : Set E'
f : E → F
g : E' → F'
x : E
y : E'
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g t y
⊢ ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) (x, y)

Tactic:
ContDiffWithinAt.prodMap' hf hg

Premises used: ContDiffWithinAt.prodMap'
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
F' : Type u_6
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
s : Set E
t : Set E'
f : E → F
g : E' → F'
hf : ContDiffOn 𝕜 n f s
hg : ContDiffOn 𝕜 n g t
⊢ ContDiffOn 𝕜 n (Prod.map f g) (s ×ˢ t)

Tactic:
(hf.comp contDiffOn_fst (prod_subset_preimage_fst _ _)).prodMk
    (hg.comp contDiffOn_snd (prod_subset_preimage_snd _ _))

Premises used: ContDiffOn.comp, contDiffOn_fst, Set.prod_subset_preimage_fst, Prod.map, Set.prod_subset_preimage_snd, contDiffOn_snd, ContDiffOn.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_3
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
F' : Type u_4
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
x : E
y : E'
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g y
⊢ ContDiffWithinAt 𝕜 n f univ x

Tactic:
rw [ContDiffAt] at *

Premises used: ContDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_3
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
F' : Type u_4
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
x : E
y : E'
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g y
hf₁ : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt 𝕜 n g univ y

Tactic:
rw [ContDiffAt] at *

Premises used: ContDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_3
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
F' : Type u_4
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
x : E
y : E'
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ y
⊢ ContDiffWithinAt 𝕜 n (Prod.map f g) univ (x, y)

Tactic:
simpa only [univ_prod_univ] using hf.prodMap hg

Premises used: ContDiffWithinAt.prodMap, Set.univ_prod_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_3
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
F' : Type u_4
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
p : E × E'
hf : ContDiffAt 𝕜 n f p.1
hg : ContDiffAt 𝕜 n g p.2
⊢ ContDiffAt 𝕜 n (Prod.map f g) p

Tactic:
hf.prodMap hg

Premises used: ContDiffAt.prodMap
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_3
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
F' : Type u_4
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
rw :
  ∀ (hf : ∀ (x : E), ContDiffAt 𝕜 n f x) (hg : ∀ (x : E'), ContDiffAt 𝕜 n g x) (x : E × E'),
    ContDiffAt 𝕜 n (Prod.map f g) x
⊢ ContDiff 𝕜 n (Prod.map f g)

Tactic:
rw [contDiff_iff_contDiffAt] at *

Premises used: contDiff_iff_contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_3
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
F' : Type u_4
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
hf : ∀ (x : E), ContDiffAt 𝕜 n f x
hg : ∀ (x : E'), ContDiffAt 𝕜 n g x
⊢ ∀ (x : E × E'), ContDiffAt 𝕜 n (Prod.map f g) x

Tactic:
fun ⟨x, y⟩ => (hf x).prodMap (hg y)

Premises used: ContDiffAt, ContDiffAt.prodMap, Prod.map, _private.0.ContDiff.prodMap.match_1
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_3
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
F' : Type u_4
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
hf : ∀ (x : E), ContDiffAt 𝕜 n f x
hg : ∀ (x : E'), ContDiffAt 𝕜 n g x
⊢ ∀ (x : E × E'), ContDiffAt 𝕜 n (Prod.map f g) x

Tactic:
exact fun ⟨x, y⟩ => (hf x).prodMap (hg y)
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
f₀ : F
⊢ ContDiff 𝕜 (F := E × F) n fun (e : E) ↦ (e, f₀)

Tactic:
contDiff_id.prodMk contDiff_const

Premises used: contDiff_id, ContDiff.prodMk, contDiff_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
e₀ : E
⊢ ContDiff 𝕜 (F := E × F) n fun (f : F) ↦ (e₀, f)

Tactic:
contDiff_const.prodMk contDiff_id

Premises used: contDiff_id, ContDiff.prodMk, contDiff_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
R : Type u_3
inst_1 : NormedRing R
inst_2 : NormedAlgebra 𝕜 R
inst_3 : HasSummableGeomSeries R
x : Rˣ
⊢ ContDiffWithinAt 𝕜 n Ring.inverse {x : R | IsUnit x} (↑x : R)

Tactic:
have := AnalyticOnNhd.contDiffOn (analyticOnNhd_inverse (𝕜 := 𝕜) (A := R)) (n := n)
    Units.isOpen.uniqueDiffOn x x.isUnit
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
R : Type u_3
inst_1 : NormedRing R
inst_2 : NormedAlgebra 𝕜 R
inst_3 : HasSummableGeomSeries R
x : Rˣ
this : ContDiffWithinAt 𝕜 n Ring.inverse {x : R | IsUnit x} (↑x : R)
⊢ ContDiffAt 𝕜 n Ring.inverse (↑x : R)

Tactic:
this.contDiffAt (Units.isOpen.mem_nhds x.isUnit)

Premises used: ContDiffWithinAt.contDiffAt, Units.isOpen, IsOpen.mem_nhds, Units.isUnit
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
R : Type u_3
inst_1 : NormedRing R
inst_2 : NormedAlgebra 𝕜 R
inst_3 : HasSummableGeomSeries R
x : Rˣ
this : ContDiffWithinAt 𝕜 n Ring.inverse {x : R | IsUnit x} (↑x : R)
⊢ ContDiffAt 𝕜 n Ring.inverse (↑x : R)

Tactic:
exact this.contDiffAt (Units.isOpen.mem_nhds x.isUnit)

Premises used: ContDiffWithinAt.contDiffAt, Units.isOpen, IsOpen.mem_nhds, Units.isUnit
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst_1 : NormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜'
hx : x ≠ 0
n : ℕ∞ω
⊢ ContDiffAt 𝕜 n Inv.inv x

Tactic:
simpa only [Ring.inverse_eq_inv'] using contDiffAt_ringInverse 𝕜 (Units.mk0 x hx)

Premises used: Ring.inverse_eq_inv', Units.mk0, contDiffAt_ringInverse
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst_1 : NormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
n : ℕ∞ω
⊢ ContDiffOn 𝕜 (E := 𝕜') n Inv.inv {0}ᶜ

Tactic:
fun _ hx =>
  (contDiffAt_inv 𝕜 hx).contDiffWithinAt

Premises used: ContDiffOn, contDiffAt_inv, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
𝕜' : Type u_4
inst_3 : NormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hx : f x ≠ 0
⊢ ContDiffWithinAt.{u_1, uE, u_4} 𝕜 (F := 𝕜') n (fun (x : E) ↦ (f x)⁻¹) s x

Tactic:
(contDiffAt_inv 𝕜 hx).comp_contDiffWithinAt x hf

Premises used: contDiffAt_inv, ContDiffAt.comp_contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
n : ℕ∞ω
𝕜' : Type u_4
inst_3 : NormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
hf : ContDiffOn 𝕜 n f s
h : ∀ x ∈ s, f x ≠ 0
⊢ ContDiffOn.{u_1, uE, u_4} 𝕜 (F := 𝕜') n (fun (x : E) ↦ (f x)⁻¹) s

Tactic:
fun x hx => (hf.contDiffWithinAt hx).inv (h x hx)

Premises used: ContDiffOn, ContDiffWithinAt.inv, ContDiffOn.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ∞ω
𝕜' : Type u_4
inst_3 : NormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
hf : ContDiffAt 𝕜 n f x
hx : f x ≠ 0
⊢ ContDiffAt.{u_1, uE, u_4} 𝕜 (F := 𝕜') n (fun (x : E) ↦ (f x)⁻¹) x

Tactic:
hf.inv hx

Premises used: ContDiffAt, ContDiffWithinAt.inv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
𝕜' : Type u_4
inst_3 : NormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
hf : ContDiff 𝕜 n f
h : ∀ (x : E), f x ≠ 0
rw : ∀ (x : E), ContDiffAt.{u_1, uE, u_4} 𝕜 (F := 𝕜') n (fun (x : E) ↦ (f x)⁻¹) x
⊢ ContDiff.{u_1, uE, u_4} 𝕜 (F := 𝕜') n fun (x : E) ↦ (f x)⁻¹

Tactic:
rw [contDiff_iff_contDiffAt]

Premises used: contDiff_iff_contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
𝕜' : Type u_4
inst_3 : NormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
hf : ContDiff 𝕜 n f
h : ∀ (x : E), f x ≠ 0
⊢ ∀ (x : E), ContDiffAt.{u_1, uE, u_4} 𝕜 (F := 𝕜') n (fun (x : E) ↦ (f x)⁻¹) x

Tactic:
fun x => hf.contDiffAt.inv (h x)

Premises used: ContDiffAt.inv, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
𝕜' : Type u_4
inst_3 : NormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
hf : ContDiff 𝕜 n f
h : ∀ (x : E), f x ≠ 0
⊢ ∀ (x : E), ContDiffAt.{u_1, uE, u_4} 𝕜 (F := 𝕜') n (fun (x : E) ↦ (f x)⁻¹) x

Tactic:
exact fun x => hf.contDiffAt.inv (h x)

Premises used: ContDiffAt.inv, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
f g : E → 𝕜
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hx : g x ≠ 0
⊢ ContDiffWithinAt 𝕜 (F := 𝕜) n (fun (x : E) ↦ f x / g x) s x

Tactic:
simpa only [div_eq_mul_inv] using hf.mul (hg.inv hx)

Premises used: ContDiffWithinAt.mul, ContDiffWithinAt.inv, div_eq_mul_inv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
f g : E → 𝕜
n : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
hg : ContDiffOn 𝕜 n g s
h₀ : ∀ x ∈ s, g x ≠ 0
⊢ ContDiffOn 𝕜 n (f / g) s

Tactic:
fun x hx =>
  (hf x hx).div (hg x hx) (h₀ x hx)

Premises used: ContDiffOn, ContDiffWithinAt.div
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
f g : E → 𝕜
n : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
hg : ContDiffOn 𝕜 n g s
h₀ : ∀ x ∈ s, g x ≠ 0
⊢ ContDiffOn 𝕜 (F := 𝕜) n (fun (x : E) ↦ f x / g x) s

Tactic:
ContDiffOn.div hf hg h₀

Premises used: ContDiffOn.div
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
f g : E → 𝕜
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
hx : g x ≠ 0
⊢ ContDiffAt 𝕜 (F := 𝕜) n (fun (x : E) ↦ f x / g x) x

Tactic:
hf.div hg hx

Premises used: ContDiffAt, ContDiffWithinAt.div
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : E → 𝕜
n : ℕ∞ω
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
h0 : ∀ (x : E), g x ≠ 0
simp :
  ∀ (hf : ∀ (x : E), ContDiffAt 𝕜 n f x) (hg : ∀ (x : E), ContDiffAt 𝕜 n g x) (x : E),
    ContDiffAt 𝕜 (F := 𝕜) n (fun (x : E) ↦ f x / g x) x
⊢ ContDiff 𝕜 (F := 𝕜) n fun (x : E) ↦ f x / g x

Tactic:
simp only [contDiff_iff_contDiffAt] at *

Premises used: contDiff_iff_contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : E → 𝕜
n : ℕ∞ω
h0 : ∀ (x : E), g x ≠ 0
hf : ∀ (x : E), ContDiffAt 𝕜 n f x
hg : ∀ (x : E), ContDiffAt 𝕜 n g x
⊢ ∀ (x : E), ContDiffAt 𝕜 (F := 𝕜) n (fun (x : E) ↦ f x / g x) x

Tactic:
fun x => (hf x).div (hg x) (h0 x)

Premises used: ContDiffAt.div
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : E → 𝕜
n : ℕ∞ω
h0 : ∀ (x : E), g x ≠ 0
hf : ∀ (x : E), ContDiffAt 𝕜 n f x
hg : ∀ (x : E), ContDiffAt 𝕜 n g x
⊢ ∀ (x : E), ContDiffAt 𝕜 (F := 𝕜) n (fun (x : E) ↦ f x / g x) x

Tactic:
exact fun x => (hf x).div (hg x) (h0 x)

Premises used: ContDiffAt.div
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
⊢ Nontrivial E

Tactic:
nontriviality E
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
⊢ inverse = O₁ ∘ Ring.inverse ∘ O₂

Tactic:
have : ContinuousLinearMap.inverse = O₁ ∘ Ring.inverse ∘ O₂ := funext (inverse_eq_ringInverse e)
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
rw : ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) (↑e : E →L[𝕜] F)
⊢ ContDiffAt 𝕜 n inverse (↑e : E →L[𝕜] F)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
⊢ ContDiff 𝕜 n O₁

Tactic:
have h₁ : ContDiff 𝕜 n O₁ := contDiff_id.clm_comp contDiff_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
⊢ ContDiff 𝕜 n O₂

Tactic:
have h₂ : ContDiff 𝕜 n O₂ := contDiff_const.clm_comp contDiff_id
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
h₂ : ContDiff 𝕜 n O₂
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) (↑e : E →L[𝕜] F)

Tactic:
h₁.contDiffAt.comp _ (ContDiffAt.comp _ ?_ h₂.contDiffAt)

Premises used: ContDiffAt.comp, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
h₂ : ContDiff 𝕜 n O₂
refine : ContDiffAt 𝕜 n Ring.inverse (O₂ (↑e : E →L[𝕜] F))
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) (↑e : E →L[𝕜] F)

Tactic:
refine h₁.contDiffAt.comp _ (ContDiffAt.comp _ ?_ h₂.contDiffAt)

Premises used: ContDiffAt.comp, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
h₂ : ContDiff 𝕜 n O₂
⊢ ContDiffAt.{u_1, uE, uE} 𝕜 (E := E →L[𝕜] E) n Ring.inverse (↑1 : E →L[𝕜] E)

Tactic:
contDiffAt_ringInverse 𝕜 (1 : (E →L[𝕜] E)ˣ)

Premises used: contDiffAt_ringInverse, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h_1 : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
h₂ : ContDiff 𝕜 n O₂
h : O₂ (↑e : E →L[𝕜] F) = (↑1 : E →L[𝕜] E)
⊢ ContDiffAt 𝕜 n Ring.inverse (O₂ (↑e : E →L[𝕜] F))

Tactic:
convert! contDiffAt_ringInverse 𝕜 (1 : (E →L[𝕜] E)ˣ)

Premises used: contDiffAt_ringInverse, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
h₂ : ContDiff 𝕜 n O₂
⊢ O₂ (↑e : E →L[𝕜] F) = (↑1 : E →L[𝕜] E)

Tactic:
simp [O₂, one_def]

Premises used: ContinuousLinearMap.one_def
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E →L[𝕜] F
he : e.IsInvertible
rcases : ∀ (M : E ≃L[𝕜] F), ContDiffAt 𝕜 n inverse (↑M : E →L[𝕜] F)
⊢ ContDiffAt 𝕜 n inverse e

Tactic:
rcases he with ⟨M, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
M : E ≃L[𝕜] F
⊢ ContDiffAt 𝕜 n inverse (↑M : E →L[𝕜] F)

Tactic:
_root_.contDiffAt_map_inverse M

Premises used: contDiffAt_map_inverse
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
M : E ≃L[𝕜] F
⊢ ContDiffAt 𝕜 n inverse (↑M : E →L[𝕜] F)

Tactic:
exact _root_.contDiffAt_map_inverse M

Premises used: contDiffAt_map_inverse
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
hf : ContDiffAt 𝕜 ω (↑f : E → F) ((↑f.symm : F → E) a)
h : AnalyticAt 𝕜 (↑f.symm : F → E) a
⊢ ContDiffAt 𝕜 ω (↑f.symm : F → E) a

Tactic:
apply AnalyticAt.contDiffAt

Premises used: AnalyticAt.contDiffAt