mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε : ∀ (y : s.CompleteCopy), dist ↑x ↑y + |(infDist (↑x) (↑s)ᶜ)⁻¹ - (infDist (↑y) (↑s)ᶜ)⁻¹| < ε → y ∈ t
⊢ ↑x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s)ᶜ

Tactic:
s.isOpen.isClosed_compl.closure_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε : ∀ (y : s.CompleteCopy), dist ↑x ↑y + |(infDist (↑x) (↑s)ᶜ)⁻¹ - (infDist (↑y) (↑s)ᶜ)⁻¹| < ε → y ∈ t
⊢ ↑x ∉ (↑s)ᶜ
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case inr.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : Y
h : Sum.dist (Sum.inr p) (Sum.inr q) = 0
⊢ Sum.inr p = Sum.inr q

Tactic:
rw [eq_of_dist_eq_zero h]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopenable s
⊢ IsClopenable sᶜ

Tactic:
rcases hs with ⟨t, t_le, t_polish, h, h'⟩
  exact ⟨t, t_le, t_polish, @IsOpen.isClosed_compl α t s h', @IsClosed.isOpen_compl α t s h⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ CompleteSpace ((n : ℕ) → E n)

Tactic:
by
  refine Metric.complete_of_convergent_controlled_sequences (fun n => (1 / 2) ^ n) (by simp) ?_
  intro u hu
  refine ⟨fun n => u n n, tendsto_pi_nhds.2 fun i => ?_⟩
  refine tendsto_const_nhds.congr' ?_
  filter_upwards [Filter.Ici_mem_atTop i] with n hn
  exact apply_eq_of_dist_lt (hu i i n le_rfl hn) le_rfl

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous[inst✝¹, inst✝²] f
h✝ : IsEmpty β
⊢ AnalyticSet (range f)

Tactic:
range_eq_empty

Goal state after:
case inl
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : β → α
f_cont : Continuous[inst✝¹, inst✝²] f
h✝ : IsEmpty β
⊢ AnalyticSet ∅
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
s : ↑measurableAtoms
y : α
left✝ : y ∈ univ
hy : measurableAtom y = ↑s
⊢ (measurableAtom y).Nonempty

Tactic:
exact ⟨y, mem_measurableAtom_self y⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ (SimpleFunc.eapprox f n).range
⊢ Measurable fun μ ↦ i * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {i})

Tactic:
refine Measurable.const_mul ?_ _

Goal state after:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ (SimpleFunc.eapprox f n).range
⊢ Measurable fun μ ↦ μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {i})
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, ∀ x, ψ x ≤ n := by
    rcases ψ.range.bddAbove with ⟨C, hC⟩
    exact ⟨⌈C⌉₊, fun x ↦ (hC <| ψ.mem_range_self x).trans (Nat.le_ceil _)⟩

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
n : ℕ
hn : ∀ (x : α), ψ x ≤ ↑n
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ ((m.bind f).bind g) s = (m.bind fun a ↦ (f a).bind g) s

Tactic:
bind_apply hs hg,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : β), (g a) s ∂m.bind f = (m.bind fun a ↦ (f a).bind g) s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x y : X
hxy : x ≠ y
n : ℕ
hn : {y}ᶜ ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
e : distDenseSeq X n x = distDenseSeq X n y
⊢ False

Tactic:
by simp +contextual [e, ← exists_prop, mem_of_mem_nhds] at hn

Goal state after:
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : ρ.IsMulLeftInvariant
inst✝ : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : ρ s = 0
x : M
⊢ MeasurableSet (HMul.hMul x ⁻¹' s)

Tactic:
apply MeasurableSet.preimage hs (by fun_prop)

Goal state after:
Module: Mathlib.Dynamics.Minimal

Goal state before:
pp: case mp
M : Type u_1
α : Type u_3
inst✝³ : Monoid M
inst✝² : TopologicalSpace α
inst✝¹ : MulAction M α
inst✝ : ContinuousConstSMul M α
⊢ IsMinimal M α → ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ

Tactic:
intro _ _
    exact eq_empty_or_univ_of_smul_invariant_closed M

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
x : G
x✝ : x ∈ ⊤
z : G
h : IsComplement {z} S
y : G
property✝ : y ∈ S
hy : (fun x ↦ ↑x.1 * ↑x.2) (⟨z, ⋯⟩, ⟨y, property✝⟩) = z * x
⊢ x ∈ S

Tactic:
← mul_left_cancel hy

Goal state after:
G : Type u_1
inst✝ : Group G
S : Set G
x : G
x✝ : x ∈ ⊤
z : G
h : IsComplement {z} S
y : G
property✝ : y ∈ S
hy : (fun x ↦ ↑x.1 * ↑x.2) (⟨z, ⋯⟩, ⟨y, property✝⟩) = z * x
⊢ ↑(⟨z, ⋯⟩, ⟨y, property✝⟩).2 ∈ S
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
ν : Measure α
inst✝¹ : μ.OuterRegular
inst✝ : ν.OuterRegular
hμν : ∀ (U : Set α), IsOpen[inst✝²] U → μ U = ν U
s : Set α
ms : MeasurableSet s
⊢ μ s = ν s

Tactic:
Set.measure_eq_iInf_isOpen,

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
ν : Measure α
inst✝¹ : μ.OuterRegular
inst✝ : ν.OuterRegular
hμν : ∀ (U : Set α), IsOpen[inst✝²] U → μ U = ν U
s : Set α
ms : MeasurableSet s
⊢ ⨅ U, ⨅ (_ : s ⊆ U), ⨅ (_ : IsOpen[inst✝²] U), μ U = ν s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
p : α → β → Prop
h : MeasurableSet {x | p x.1 x.2}
⊢ (∀ᵐ (x : α × β) ∂μ.prod ν, p x.1 x.2) ↔ ∀ᵐ (x : β × α) ∂ν.prod μ, p x.2 x.1

Tactic:
rw [← prod_swap, ae_map_iff (by fun_prop) h]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
p : α → β → Prop
h : MeasurableSet {x | p x.1 x.2}
⊢ (∀ᵐ (x : β × α) ∂ν.prod μ, p x.swap.1 x.swap.2) ↔ ∀ᵐ (x : β × α) ∂ν.prod μ, p x.2 x.1
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
⊢ (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)

Tactic:
by
  rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, restrict_sum_of_countable, restrict_sum_of_countable,
    prod_sum, prod_sum, restrict_sum_of_countable]
  congr 1
  ext1 i
  refine prod_eq fun s' t' hs' ht' => ?_
  rw [restrict_apply (hs'.prod ht'), prod_inter_prod, prod_prod, restrict_apply hs',
    restrict_apply ht']

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
⊢ (dirac x).prod ν = map (Prod.mk x) ν

Tactic:
rw [← sum_sfiniteSeq ν, prod_sum_right, map_sum measurable_prodMk_left.aemeasurable]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
x : α
⊢ (sum fun p ↦ (dirac x).prod (sfiniteSeq ν p)) = sum fun i ↦ map (Prod.mk x) (sfiniteSeq ν i)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
⊢ (map (fun a ↦ (X a, Y a)) μ).fst = map X μ

Tactic:
by_cases hX : AEMeasurable X μ

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : AEMeasurable X μ
⊢ (map (fun a ↦ (X a, Y a)) μ).fst = map X μ

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hY : AEMeasurable Y μ
hX : ¬AEMeasurable X μ
⊢ (map (fun a ↦ (X a, Y a)) μ).fst = map X μ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: X : Type u_6
E : Type u_7
ι : Type u_8
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : CommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : IsCompletelyPseudoMetrizableSpace E
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableMul₂ E
inst✝² : Countable ι
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x ↦ ∏'[L] (i : ι), f i x) μ

Tactic:
by
  choose g hg_meas hg_eq_f using h
  use (fun x => ∏'[L] i, g i x), Measurable.tprod hg_meas
  filter_upwards [ae_all_iff.mpr hg_eq_f] with x h_eq using tprod_congr h_eq

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᵐ[μ] 0

Tactic:
lintegral_eq_zero_iff' hf

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ f =ᵐ[μ] 0 ↔ f =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : PseudoEMetricSpace β
n : ℕ
j : ι
f : ι → α → β
g : α → β
inst✝ : Preorder ι
x : α
⊢ x ∈ notConvergentSeq f g n j ↔ ∃ k ≥ j, (↑n)⁻¹ < edist (f k x) (g x)

Tactic:
simp_rw [notConvergentSeq, Set.mem_iUnion, exists_prop, mem_ofPred]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case mp
x y : ℝ
⊢ √x = y → y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0

pp: case mpr
x y : ℝ
⊢ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → √x = y

Tactic:
· rintro rfl
    rcases le_or_gt 0 x with hle | hlt
    · exact Or.inl ⟨mul_self_sqrt hle, sqrt_nonneg x⟩
    · exact Or.inr ⟨hlt, sqrt_eq_zero_of_nonpos hlt.le⟩

Goal state after:
case mpr
x y : ℝ
⊢ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → √x = y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hx : 0 < x
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
by
  obtain hy | hy := le_total y 0
  · exact iff_of_false ((sqrt_eq_zero_of_nonpos hy).trans_lt <| sqrt_pos.2 hx).not_ge
      (hy.trans_lt hx).not_ge
  · exact sqrt_le_sqrt_iff hy

Goal state after:
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ (↑r).im = 0

Tactic:
Complex.ofReal_im

Goal state after:
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ 0 = 0
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ ‖∑ i ∈ s, f i‖ ≤ b

Tactic:
hb

Goal state after:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) = (algebraMap ℝ A) x₁ * (algebraMap ℝ A) x₂ - (algebraMap ℝ A) (y₁ * y₂)

Tactic:
← map_mul,

Goal state after:
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) = (algebraMap ℝ A) (x₁ * x₂) - (algebraMap ℝ A) (y₁ * y₂)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * y₂ + y₁ * x₂) * I' =
    ((algebraMap ℝ A) x₁ * (algebraMap ℝ A) y₂ + (algebraMap ℝ A) y₁ * (algebraMap ℝ A) x₂) * I'

Tactic:
← map_mul,

Goal state after:
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * y₂ + y₁ * x₂) * I' =
    ((algebraMap ℝ A) (x₁ * y₂) + (algebraMap ℝ A) y₁ * (algebraMap ℝ A) x₂) * I'
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * y₂ + y₁ * x₂) * I' =
    ((algebraMap ℝ A) (x₁ * y₂) + (algebraMap ℝ A) y₁ * (algebraMap ℝ A) x₂) * I'

Tactic:
← map_mul,

Goal state after:
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * y₂ + y₁ * x₂) * I' = ((algebraMap ℝ A) (x₁ * y₂) + (algebraMap ℝ A) (y₁ * x₂)) * I'
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
F : ℂ →ₐ[ℝ] A
⊢ F I * F I = -1

Tactic:
← map_mul,

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
F : ℂ →ₐ[ℝ] A
⊢ F (I * I) = -1
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: n : ℕ
⊢ ↑n ∈ slitPlane ↔ n ≠ 0

Tactic:
simpa [pos_iff_ne_zero] using @ofReal_mem_slitPlane n

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : X
⊢ ↑(toPartialHomeomorph f h).symm (f x) = x

Tactic:
← congr_fun (h.toPartialHomeomorph_apply f),

Goal state after:
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : X
⊢ ↑(toPartialHomeomorph f h).symm (↑(toPartialHomeomorph f h) x) = x
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ f (↑(toPartialHomeomorph f h).symm x) = x

Tactic:
← congr_fun (h.toPartialHomeomorph_apply f),

Goal state after:
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ ↑(toPartialHomeomorph f h) (↑(toPartialHomeomorph f h).symm x) = x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ 𝕜 →+ ℝ

Tactic:
by subst h''; exact h.im

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: case ofNat
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x ↦ f x ^ Int.ofNat a✝) =Θ[l] fun x ↦ g x ^ Int.ofNat a✝

pp: case negSucc
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x ↦ f x ^ Int.negSucc a✝) =Θ[l] fun x ↦ g x ^ Int.negSucc a✝

Tactic:
· simpa only [Int.ofNat_eq_natCast, zpow_natCast] using h.pow _

Goal state after:
case negSucc
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x ↦ f x ^ Int.negSucc a✝) =Θ[l] fun x ↦ g x ^ Int.negSucc a✝
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =Θ[l] g → (f ∘ Prod.fst) =Θ[l ×ˢ l'] (g ∘ Prod.fst)

Tactic:
simp only [IsTheta]

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g ∧ g =O[l] f → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst) ∧ (g ∘ Prod.fst) =O[l ×ˢ l'] (f ∘ Prod.fst)
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =Θ[l] g → (f ∘ Prod.snd) =Θ[l' ×ˢ l] (g ∘ Prod.snd)

Tactic:
simp only [IsTheta]

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g ∧ g =O[l] f → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd) ∧ (g ∘ Prod.snd) =O[l' ×ˢ l] (f ∘ Prod.snd)
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hgk : g =o[l] k
hc : 0 < c
⊢ f =o[l] k

Tactic:
simp only [IsLittleO_def] at *
  intro c' c'pos
  have : 0 < c' / c := div_pos c'pos hc
  exact (hfg.trans (hgk this) hc.le).congr_const (mul_div_cancel₀ _ hc.ne')

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
c : ℝ
hc : 0 < c
x : α
⊢ x ∈ {x | (fun x ↦ ‖0‖ ≤ c * ‖g' x‖) x}

Tactic:
by simpa using mul_nonneg hc.le (norm_nonneg <| g' x)

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (fun c ↦ c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
c : ℝ
hc : c ∈ Ioi 0
⊢ (fun x_1 ↦ ‖f'' x‖) c ≤ (fun c ↦ c * ‖g' x‖) c

Tactic:
exact eventually_principal.1 (h hc) x hx

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Norm E
inst✝³ : Norm F
f : α → E
inst✝² : One F
inst✝¹ : NormOneClass F
inst✝ : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
b : α
⊢ (b ∈ {a}ᶜ → ‖f b‖ ≤ c) → ‖f b‖ ≤ max c ‖f a‖

Tactic:
hb

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Norm E
inst✝³ : Norm F
f : α → E
inst✝² : One F
inst✝¹ : NormOneClass F
inst✝ : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
b : α
hb : b ∈ {a}ᶜ → ‖f b‖ ≤ c
⊢ ‖f b‖ ≤ max c ‖f a‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ x + 1 ≤ rexp x

Tactic:
rcases eq_or_lt_of_le hx with (rfl | h)

Goal state after:
case inl
hx : 0 ≤ 0
⊢ 0 + 1 ≤ rexp 0

case inr
x : ℝ
hx : 0 ≤ x
h : 0 < x
⊢ x + 1 ≤ rexp x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sinh ((starRingEnd ℂ) x) / cosh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tanh x)

Tactic:
sinh_conj,

Goal state after:
x : ℂ
⊢ (starRingEnd ℂ) (sinh x) / cosh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tanh x)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case neg
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
x : α
hx₁ : g x = 0 → f x = 0
hx₂ : ‖f x‖ / ‖g x‖ ≤ c
hgx : ¬g x = 0
⊢ ‖f x‖ ≤ c * ‖g x‖

Tactic:
exact (div_le_iff₀ (norm_pos_iff.2 hgx)).mp hx₂

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2

Tactic:
by rw [two_mul, cosh_add, sq, sq]

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sinh x * I / cos (x * I) = tanh x * I

Tactic:
cos_mul_I,

Goal state after:
x : ℂ
⊢ sinh x * I / cosh x = tanh x * I
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ sin x * cos (y * I) + cos x * sin (y * I) = sin x * cosh y + cos x * sinh y * I

Tactic:
cos_mul_I,

Goal state after:
x y : ℂ
⊢ sin x * cosh y + cos x * sin (y * I) = sin x * cosh y + cos x * sinh y * I
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ cos x * cos (y * I) - sin x * sin (y * I) = cos x * cosh y - sin x * sinh y * I

Tactic:
cos_mul_I,

Goal state after:
x y : ℂ
⊢ cos x * cosh y - sin x * sin (y * I) = cos x * cosh y - sin x * sinh y * I
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sinh ((starRingEnd ℂ) x * (starRingEnd ℂ) (-I)) = (starRingEnd ℂ) (sin x) * (starRingEnd ℂ) (-I)

Tactic:
← map_mul,

Goal state after:
x : ℂ
⊢ sinh ((starRingEnd ℂ) (x * -I)) = (starRingEnd ℂ) (sin x) * (starRingEnd ℂ) (-I)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sinh ((starRingEnd ℂ) (x * -I)) = (starRingEnd ℂ) (sin x) * (starRingEnd ℂ) (-I)

Tactic:
← map_mul,

Goal state after:
x : ℂ
⊢ sinh ((starRingEnd ℂ) (x * -I)) = (starRingEnd ℂ) (sin x * -I)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sinh ((starRingEnd ℂ) (x * -I)) = (starRingEnd ℂ) (sin x * -I)

Tactic:
sinh_conj,

Goal state after:
x : ℂ
⊢ (starRingEnd ℂ) (sinh (x * -I)) = (starRingEnd ℂ) (sin x * -I)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (sin ↑x).im = 0

Tactic:
rw [← ofReal_sin_ofReal_re, ofReal_im]

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cosh ((starRingEnd ℂ) x * (starRingEnd ℂ) (-I)) = (starRingEnd ℂ) (cos x)

Tactic:
← map_mul,

Goal state after:
x : ℂ
⊢ cosh ((starRingEnd ℂ) (x * -I)) = (starRingEnd ℂ) (cos x)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case calc_3
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i ∈ range k, ‖x‖ ^ n / ↑n.factorial * (‖x‖ ^ i / ↑n.succ ^ i) ≤ ‖x‖ ^ n / ↑n.factorial * 2

Tactic:
← mul_sum

Goal state after:
case calc_3
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖x‖ ^ n / ↑n.factorial * ∑ i ∈ range k, ‖x‖ ^ i / ↑n.succ ^ i ≤ ‖x‖ ^ n / ↑n.factorial * 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos x + sin x * I = cexp (x * I)

Tactic:
rw [← cosh_add_sinh, sinh_mul_I, cosh_mul_I]

Goal state after: