awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
hf' : ContinuousOn f (ball c r)
hf : IsConservativeOn f (ball c r)
⊢ IsExactOn f (ball c r)

Tactic:
⟨fun z ↦ wedgeIntegral c z f, fun _ ↦ hf.hasDerivAt_wedgeIntegral hf'⟩

Premises used: Complex.wedgeIntegral, Complex.IsExactOn, Exists.intro, Complex.IsConservativeOn.hasDerivAt_wedgeIntegral
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
⊢ IsConservativeOn f U ∧ ContinuousOn f U ↔ DifferentiableOn ℂ f U

Tactic:
⟨fun ⟨hf, hf'⟩ z hz ↦ ?_, fun hf ↦ ⟨hf.isConservativeOn, hf.continuousOn⟩⟩

Premises used: DifferentiableOn.continuousOn, And.intro, _private.0.Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn.match_1, Iff.intro, DifferentiableWithinAt, Complex, DifferentiableOn.isConservativeOn
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
refine :
  IsConservativeOn f U ∧ ContinuousOn f U →
    ∀ (z : ℂ) (hz : z ∈ U) (hf : IsConservativeOn f U) (hf' : ContinuousOn f U), DifferentiableWithinAt ℂ f U z
⊢ IsConservativeOn f U ∧ ContinuousOn f U ↔ DifferentiableOn ℂ f U

Tactic:
refine ⟨fun ⟨hf, hf'⟩ z hz ↦ ?_, fun hf ↦ ⟨hf.isConservativeOn, hf.continuousOn⟩⟩
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
h : IsConservativeOn f U ∧ ContinuousOn f U
z : ℂ
hz : z ∈ U
hf : IsConservativeOn f U
hf' : ContinuousOn f U
⊢ ∃ r > 0, ball z r ⊆ U

Tactic:
Metric.isOpen_iff.mp hU z hz

Premises used: Metric.isOpen_iff, Iff.mp
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
h : IsConservativeOn f U ∧ ContinuousOn f U
z : ℂ
hz : z ∈ U
hf : IsConservativeOn f U
hf' : ContinuousOn f U
obtain : ∀ (r : ℝ) (h₀ : r > 0) (h₁ : ball z r ⊆ U), DifferentiableWithinAt ℂ f U z
⊢ DifferentiableWithinAt ℂ f U z

Tactic:
obtain ⟨r, h₀, h₁⟩ : ∃ r > 0, ball z r ⊆ U := Metric.isOpen_iff.mp hU z hz

Premises used: Metric.isOpen_iff, Iff.mp
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
h : IsConservativeOn f U ∧ ContinuousOn f U
z : ℂ
hz : z ∈ U
hf : IsConservativeOn f U
hf' : ContinuousOn f U
r : ℝ
h₀ : r > 0
h₁ : ball z r ⊆ U
⊢ DifferentiableOn ℂ f (ball z r)

Tactic:
have : DifferentiableOn ℂ f (ball z r) :=
    (IsConservativeOn.isExactOn_ball (hf'.mono h₁) (hf.mono h₁)).differentiableOn isOpen_ball
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
h : IsConservativeOn f U ∧ ContinuousOn f U
z : ℂ
hz : z ∈ U
hf : IsConservativeOn f U
hf' : ContinuousOn f U
r : ℝ
h₀ : r > 0
h₁ : ball z r ⊆ U
this : DifferentiableOn ℂ f (ball z r)
apply : ball z r ∈ 𝓝[U] z
⊢ DifferentiableWithinAt ℂ f U z

Tactic:
apply (this z (mem_ball_self h₀)).mono_of_mem_nhdsWithin

Premises used: Metric.mem_ball_self, DifferentiableWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
h : IsConservativeOn f U ∧ ContinuousOn f U
z : ℂ
hz : z ∈ U
hf : IsConservativeOn f U
hf' : ContinuousOn f U
r : ℝ
h₀ : r > 0
h₁ : ball z r ⊆ U
this : DifferentiableOn ℂ f (ball z r)
⊢ ball z r ∈ 𝓝[U] z

Tactic:
mem_nhdsWithin.mpr ⟨ball z r, isOpen_ball, mem_ball_self h₀, inter_subset_left⟩

Premises used: Iff.mpr, Metric.mem_ball_self, Metric.ball, Set.inter_subset_left, mem_nhdsWithin, Metric.isOpen_ball, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
h : IsConservativeOn f U ∧ ContinuousOn f U
z : ℂ
hz : z ∈ U
hf : IsConservativeOn f U
hf' : ContinuousOn f U
r : ℝ
h₀ : r > 0
h₁ : ball z r ⊆ U
this : DifferentiableOn ℂ f (ball z r)
⊢ ball z r ∈ 𝓝[U] z

Tactic:
exact mem_nhdsWithin.mpr ⟨ball z r, isOpen_ball, mem_ball_self h₀, inter_subset_left⟩

Premises used: Iff.mpr, Metric.mem_ball_self, Metric.ball, Set.inter_subset_left, mem_nhdsWithin, Metric.isOpen_ball, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
hf : DifferentiableOn ℂ f (ball c r)
⊢ IsExactOn f (ball c r)

Tactic:
hf.isConservativeOn.isExactOn_ball hf.continuousOn

Premises used: DifferentiableOn.continuousOn, Complex.IsConservativeOn.isExactOn_ball, DifferentiableOn.isConservativeOn
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
h : ∀ (z : ℂ), Membership.mem (γ := Set ℂ) univ z → HasDerivAt (fun (x : ℂ) ↦ wedgeIntegral 0 x f) (f z) z
⊢ IsExactOn f univ

Tactic:
use (wedgeIntegral 0 · f)

Premises used: Complex.wedgeIntegral, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
z : ℂ
h : Membership.mem (γ := Set ℂ) univ z → HasDerivAt (fun (x : ℂ) ↦ wedgeIntegral 0 x f) (f z) z
⊢ Membership.mem (γ := Set ℂ) univ z → HasDerivAt (fun (x : ℂ) ↦ wedgeIntegral 0 x f) (f z) z

Tactic:
_
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
z : ℂ
h : Membership.mem (γ := Set ℂ) univ z
⊢ IsConservativeOn f (ball 0 (‖z‖ + 1))

Tactic:
have h₃ : IsConservativeOn f (ball 0 (‖z‖ + 1)) := h₂.mono (subset_univ _)
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
z : ℂ
h : Membership.mem (γ := Set ℂ) univ z
h₃ : IsConservativeOn f (ball 0 (‖z‖ + 1))
⊢ ContinuousOn f (ball 0 (‖z‖ + 1))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
z : ℂ
h : Membership.mem (γ := Set ℂ) univ z
h₃ : IsConservativeOn f (ball 0 (‖z‖ + 1))
⊢ Membership.mem (γ := Set ℂ) (ball 0 (‖z‖ + 1)) z

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
z : ℂ
h : Membership.mem (γ := Set ℂ) univ z
h₃ : IsConservativeOn f (ball 0 (‖z‖ + 1))
⊢ HasDerivAt (fun (x : ℂ) ↦ wedgeIntegral 0 x f) (f z) z

Tactic:
exact h₃.hasDerivAt_wedgeIntegral (by fun_prop) (by aesop)

Premises used: Complex.IsConservativeOn.hasDerivAt_wedgeIntegral
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
hf : Differentiable ℂ f
⊢ IsExactOn f univ

Tactic:
apply IsConservativeOn.isExactOn_univ hf.continuous
    ((isConservativeOn_and_continuousOn_iff_isDifferentiableOn isOpen_univ).2 hf.differentiableOn).1

Premises used: Iff.mpr, Complex.IsConservativeOn.isExactOn_univ, isOpen_univ, And.left, Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn, Differentiable.differentiableOn, Differentiable.continuous
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
⊢ ℂ_ℤ = {z : ℂ | ¬∃ (n : ℤ), (↑n : ℂ) = z}

Tactic:
rfl

Premises used: Set.Mem, setOf, Complex.integerComplement, Set.range, rfl
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
x : ℂ
⊢ x ∈ ℂ_ℤ ↔ ¬∃ (n : ℤ), (↑n : ℂ) = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Complex.integerComplement, Set.range, Not
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
z : ℍ
⊢ (↑z : ℂ) ∈ ℂ_ℤ

Tactic:
not_exists.mpr fun x hx ↦ ne_intCast z x hx.symm

Premises used: Iff.mpr, Set.Mem, setOf, not_exists, Complex.integerComplement, Set.range, Eq.symm, UpperHalfPlane.ne_intCast, Not
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
x : ℂ
a : ℤ
simp : (∃ (n : ℤ), (↑n : ℂ) = x + (↑a : ℂ)) ↔ ∃ (n : ℤ), (↑n : ℂ) = x
⊢ x + (↑a : ℂ) ∈ ℂ_ℤ ↔ x ∈ ℂ_ℤ

Tactic:
simp only [mem_integerComplement_iff, not_iff_not]

Premises used: not_iff_not, Complex.mem_integerComplement_iff
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
x : ℂ
a : ℤ
⊢ (∃ (n : ℤ), (↑n : ℂ) = x + (↑a : ℂ)) ↔ ∃ (n : ℤ), (↑n : ℂ) = x

Tactic:
exact ⟨(Exists.elim · fun n hn ↦ ⟨n - a, by simp [hn]⟩),
    (Exists.elim · fun n hn ↦ ⟨n + a, by simp [hn]⟩)⟩
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
hx' : x = 0
⊢ (↑0 : ℂ) = x

Tactic:
exact_mod_cast hx'.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
a : ℤ
⊢ x + (↑a : ℂ) ≠ 0

Tactic:
integerComplement.ne_zero ((add_intCast_mem_integerComplement a).mpr hx)

Premises used: Iff.mpr, Complex.integerComplement.ne_zero, Complex.add_intCast_mem_integerComplement
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
hx' : x = 1
⊢ (↑1 : ℂ) = x

Tactic:
exact_mod_cast hx'.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℤ
⊢ ¬(↑n : ℂ) = x

Tactic:
have := not_exists.mp hx n
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℤ
this : ¬(↑n : ℂ) = x
⊢ ¬(↑(-n) : ℂ) = x

Tactic:
have := not_exists.mp hx (-n)
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℤ
this_1 : ¬(↑n : ℂ) = x
this : ¬(↑(-n) : ℂ) = x
⊢ HPow.hPow (β := ℕ) x 2 ≠ HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2

Tactic:
simp_all [sq_eq_sq_iff_eq_or_eq_neg, eq_comm]

Premises used: eq_comm, sq_eq_sq_iff_eq_or_eq_neg
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
a : {z : ℂ | 0 < z.im} ⊆ ℂ_ℤ
⊢ {z : ℂ | 0 < z.im} ∩ ℂ_ℤ = {z : ℂ | 0 < z.im}

Tactic:
apply Set.inter_eq_self_of_subset_left

Premises used: Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
⊢ {z : ℂ | 0 < z.im} ⊆ ℂ_ℤ

Tactic:
fun z hz ↦ UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩

Premises used: Set.Mem, UpperHalfPlane.mk, UpperHalfPlane.coe_mem_integerComplement, Set.Subset
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
⊢ {z : ℂ | 0 < z.im} ⊆ ℂ_ℤ

Tactic:
exact fun z hz ↦ UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩

Premises used: UpperHalfPlane.mk, UpperHalfPlane.coe_mem_integerComplement
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
z : ℍ
n : ℤ
hn : n ≠ 0
w : ℤ
hm : (↑w : ℂ) = (↑n : ℂ) / (↑z : ℂ)
⊢ ((↑n : ℂ) / (↑z : ℂ)).im ≠ 0

Tactic:
simp [div_im, z.ne_zero, hn, z.im_ne_zero]

Premises used: UpperHalfPlane.im_ne_zero, Complex.div_im, UpperHalfPlane.ne_zero
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
z : ℍ
n : ℤ
hn : n ≠ 0
w : ℤ
hm : (↑w : ℂ) = (↑n : ℂ) / (↑z : ℂ)
⊢ ((↑n : ℂ) / (↑z : ℂ)).im ≠ 0

Tactic:
have : (n / (z : ℂ)).im ≠ 0 := by simp [div_im, z.ne_zero, hn, z.im_ne_zero]
-- Module: Mathlib.Analysis.Complex.IntegerCompl
Goal:
z : ℍ
n : ℤ
hn : n ≠ 0
w : ℤ
hm : (↑w : ℂ) = (↑n : ℂ) / (↑z : ℂ)
this : ((↑n : ℂ) / (↑z : ℂ)).im ≠ 0
⊢ False

Tactic:
simpa [← hm]
-- Module: Mathlib.Analysis.Complex.IsIntegral
Goal:
⊢ IsIntegral ℤ I

Tactic:
⟨X ^ 2 + C 1, monic_X_pow_add_C _ two_ne_zero, ?_⟩

Premises used: Polynomial.C, Polynomial.monic_X_pow_add_C, RingHom.IsIntegralElem, two_ne_zero, IsIntegral, HPow.hPow, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.IsIntegral
Goal:
refine : eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 + (C : (a : ℤ) → ℤ[X]) 1) = 0
⊢ IsIntegral ℤ I

Tactic:
refine ⟨X ^ 2 + C 1, monic_X_pow_add_C _ two_ne_zero, ?_⟩
-- Module: Mathlib.Analysis.Complex.IsIntegral
Goal:
rw :
  eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
rw₁ : HPow.hPow (β := ℕ) I 2 + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
rw₂ : HAdd.hAdd (β := ℂ) (HPow.hPow (β := ℕ) I 2) ((algebraMap ℤ ℂ : (a : ℤ) → ℂ) 1 : ℂ) = 0
rw₃ : HAdd.hAdd (α := ℂ) (β := ℂ) (-1 : ℂ) ((algebraMap ℤ ℂ : (a : ℤ) → ℂ) 1 : ℂ) = 0
rw₄ : HAdd.hAdd (α := ℂ) (-1) (↑1 : ℂ) = 0
rw₅ : HAdd.hAdd (α := ℂ) (-1) 1 = 0
rw₆ rw₇ : Eq (α := ℂ) 0 0
⊢ eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 + (C : (a : ℤ) → ℤ[X]) 1) = 0

Tactic:
rw [eval₂_add, eval₂_X_pow, eval₂_C, I_sq, eq_intCast, Int.cast_one, neg_add_cancel]

Premises used: Polynomial.eval₂_X_pow, eq_intCast, neg_add_cancel, Complex.I_sq, Polynomial.eval₂_C, Int.cast_one, Polynomial.eval₂_add
-- Module: Mathlib.Analysis.Complex.IsIntegral
Goal:
⊢ IsIntegral ℚ I

Tactic:
isIntegral_int_I.tower_top

Premises used: IsIntegral.tower_top, Complex.isIntegral_int_I
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
x : ℂ
rw : ‖(↑a : ℂ)‖ * ‖x‖ = ‖x‖
rw₁ : 1 * ‖x‖ = ‖x‖
rw₂ rw₃ : ‖x‖ = ‖x‖
⊢ ‖(↑a : ℂ) * x‖ = ‖x‖

Tactic:
rw [norm_mul, Circle.norm_coe, one_mul]

Premises used: norm_mul, Circle.norm_coe, one_mul
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
⊢ ∀ (x : ℂ),
    Eq (α := ℂ)
      ((let __src : ℂ ≃ₗ[ℝ] ℂ := DistribMulAction.toLinearEquiv ℝ (S := Circle) ℂ 1;
            { toLinearEquiv := __src, norm_map' := ⋯ } :
            (a : ℂ) → ℂ)
          x :
        ℂ)
      ((1 : (a : ℂ) → ℂ) x : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
z : ℂ
⊢ (((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) z = (↑a : ℂ) * z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
⊢ Eq (α := ℂ ≃ₗᵢ[ℝ] ℂ) (LinearIsometryEquiv.symm ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))
    ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a⁻¹)

Tactic:
LinearIsometryEquiv.ext fun _ => rfl

Premises used: LinearIsometryEquiv.ext, rfl
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a b : Circle
h :
  ∀ (x : ℂ),
    Eq (α := ℂ)
      ((LinearIsometryEquiv.trans (E₂ := ℂ) ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)
              ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) b) :
            (a : ℂ) → ℂ)
          x :
        ℂ)
      ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) (b * a) : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) x : ℂ)
⊢ Eq (α := ℂ ≃ₗᵢ[ℝ] ℂ)
    (LinearIsometryEquiv.trans (E₂ := ℂ) ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)
      ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) b))
    ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) (b * a))

Tactic:
ext1
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a b : Circle
x : ℂ
⊢ Eq (α := ℂ)
    ((LinearIsometryEquiv.trans (E₂ := ℂ) ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)
            ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) b) :
          (a : ℂ) → ℂ)
        x :
      ℂ)
    ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) (b * a) : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) x : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
h : (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a = conjLIE
⊢ Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) 1 : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)

Tactic:
have h1 : rotation a 1 = conj 1 := LinearIsometryEquiv.congr_fun h 1
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
h : (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a = conjLIE
h1 :
  Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) 1 : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
⊢ Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) I : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)

Tactic:
have hI : rotation a I = conj I := LinearIsometryEquiv.congr_fun h I
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
h : (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a = conjLIE
h1 :
  Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) 1 : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
hI :
  Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) I : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
⊢ (↑a : ℂ) = 1

Tactic:
rw [rotation_apply, map_one, mul_one] at h1

Premises used: rotation_apply, map_one, mul_one
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
h : (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a = conjLIE
h1 :
  Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) 1 : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
hI :
  Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) I : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
h1₁ : (↑a : ℂ) = 1
⊢ Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) I : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)

Tactic:
rw [rotation_apply, map_one, mul_one] at h1

Premises used: rotation_apply, map_one, mul_one
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
h : (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a = conjLIE
h1 : (↑a : ℂ) = 1
hI :
  Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) I : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
⊢ Eq (α := ℂ) 1 0

Tactic:
rw [rotation_apply, conj_I, ← neg_one_mul, mul_left_inj' I_ne_zero, h1, eq_neg_self_iff] at hI

Premises used: rotation_apply, neg_one_mul, Complex.I_ne_zero, CharZero.eq_neg_self_iff, mul_left_inj', Complex.conj_I
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
h : (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a = conjLIE
h1 : (↑a : ℂ) = 1
hI : Eq (α := ℂ) 1 0
⊢ False

Tactic:
one_ne_zero hI

Premises used: one_ne_zero
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
h : (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a = conjLIE
h1 : (↑a : ℂ) = 1
hI : Eq (α := ℂ) 1 0
⊢ False

Tactic:
exact one_ne_zero hI

Premises used: one_ne_zero
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
e : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ)
    (HDiv.hDiv (α := ℂ) ((e : (a : ℂ) → ℂ) 1 : ℂ) (↑(norm (E := ℂ) ((e : (a : ℂ) → ℂ) 1 : ℂ)) : ℂ))

Tactic:
simp [Submonoid.unitSphere]

Premises used: Submonoid.unitSphere
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
⊢ (↑(rotationOf ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : ℂ) = (↑a : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
⊢ Function.Injective (α := Circle) (β := ℂ ≃ₗᵢ[ℝ] ℂ) (⇑rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ)

Tactic:
Function.LeftInverse.injective rotationOf_rotation

Premises used: Function.LeftInverse.injective, rotationOf_rotation
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h₃ :
  ∀ (z : ℂ),
    HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) =
      HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
z : ℂ
⊢ Ne (α := ℝ) 2 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h₃ :
  ∀ (z : ℂ),
    HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) =
      HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
z : ℂ
⊢ re ((f : (a : ℂ) → ℂ) z) = z.re

Tactic:
simpa [Complex.ext_iff, add_re, add_im, conj_re, conj_im, ← two_mul,
    show (2 : ℝ) ≠ 0 by simp] using (h₃ z).symm

Premises used: Complex.add_im, two_mul, Complex.add_re, Complex.conj_im, Complex.ext_iff, Complex.conj_re, Eq.symm
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), re ((f : (a : ℂ) → ℂ) z) = z.re
z : ℂ
⊢ norm (E := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) = ‖z‖

Tactic:
have h₁ := f.norm_map z
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), re ((f : (a : ℂ) → ℂ) z) = z.re
z : ℂ
h₁ : norm (E := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) = ‖z‖
⊢ √((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ)) = √((normSq : (a : ℂ) → ℝ) z)

Tactic:
simp only [norm_def] at h₁

Premises used: Complex.norm_def
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), re ((f : (a : ℂ) → ℂ) z) = z.re
z : ℂ
h₁ : √((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ)) = √((normSq : (a : ℂ) → ℝ) z)
rwa :
  ∀ (h₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₁ :
  ∀
    (h₁ :
      re ((f : (a : ℂ) → ℂ) z) * re ((f : (a : ℂ) → ℂ) z) + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) =
        (normSq : (a : ℂ) → ℝ) z),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₂ :
  ∀
    (h₁ :
      re ((f : (a : ℂ) → ℂ) z) * re ((f : (a : ℂ) → ℂ) z) + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) =
        z.re * z.re + z.im * z.im),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₃ :
  ∀ (h₁ : z.re * z.re + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) = z.re * z.re + z.im * z.im),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₄ :
  ∀ (h₁ : im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) = z.im * z.im),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀ (h₁ : im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
⊢ im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im

Tactic:
rwa [Real.sqrt_inj (normSq_nonneg _) (normSq_nonneg _), normSq_apply (f z), normSq_apply z,
    h₂, add_left_cancel_iff, mul_self_eq_mul_self_iff] at h₁

Premises used: mul_self_eq_mul_self_iff, add_left_cancel_iff, Complex.normSq_nonneg, Complex.normSq_apply, DFunLike.coe, Real.sqrt_inj
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
rw : ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ = norm (E := ℂ) ((f : (a : ℂ) → ℂ) (z - 1) : ℂ)
rw₁ :
  ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ =
    ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ)‖
rw₂ rw₃ :
  ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ =
    ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖
⊢ ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ = ‖z - 1‖

Tactic:
rw [← f.norm_map (z - 1), f.map_sub, h]

Premises used: LinearIsometry.norm_map, LinearIsometry.map_sub, HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
⊢ ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ = ‖z - 1‖

Tactic:
have : ‖f z - 1‖ = ‖z - 1‖ := by rw [← f.norm_map (z - 1), f.map_sub, h]
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
this : ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ = ‖z - 1‖
⊢ HPow.hPow (β := ℕ) ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ 2 = HPow.hPow (β := ℕ) ‖z - 1‖ 2

Tactic:
apply_fun fun x => x ^ 2 at this

Premises used: HPow.hPow, OfNat.ofNat