mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : g ∈ T
⊢ ↑(hST.equiv g).2 = g

Tactic:
hST.equiv_snd_eq_self_of_mem_of_one_mem h1 h

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
h : g ∈ T
⊢ ↑⟨g, h⟩ = g
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
hS : IsComplement S ↑H
g : G
⊢ g⁻¹ * (↑(hS.toLeftFun g))⁻¹⁻¹ = g⁻¹ * ↑(hS.toLeftFun g)

Tactic:
inv_inv

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
hS : IsComplement S ↑H
g : G
⊢ g⁻¹ * ↑(hS.toLeftFun g) = g⁻¹ * ↑(hS.toLeftFun g)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hT : IsComplement (↑H) T
g : G
⊢ (↑(hT.toRightFun g))⁻¹⁻¹ * g⁻¹ = ↑(hT.toRightFun g) * g⁻¹

Tactic:
inv_inv

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hT : IsComplement (↑H) T
g : G
⊢ ↑(hT.toRightFun g) * g⁻¹ = ↑(hT.toRightFun g) * g⁻¹
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 (β × α)
hs : MeasurableSet s
⊢ (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) s =
    (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) s

Tactic:
sum_apply _ hs,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set (β × α)
hs : MeasurableSet s
⊢ ∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) s =
    (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst✝² : SFinite ν
inst✝¹ : SFinite μ
inst✝ : SFinite τ
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ (sum fun p ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2))) s =
    (sum fun p ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))) s

Tactic:
sum_apply _ hs,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst✝² : SFinite ν
inst✝¹ : SFinite μ
inst✝ : SFinite τ
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ ∑' (i : ℕ × ℕ × ℕ), ((sfiniteSeq μ i.1).prod ((sfiniteSeq ν i.2.1).prod (sfiniteSeq τ i.2.2))) s =
    (sum fun p ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))) s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst✝² : SFinite ν
inst✝¹ : SFinite μ
inst✝ : SFinite τ
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ ∑' (i : ℕ × ℕ × ℕ), ((sfiniteSeq μ i.1).prod ((sfiniteSeq ν i.2.1).prod (sfiniteSeq τ i.2.2))) s =
    (sum fun p ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))) s

Tactic:
sum_apply _ hs,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst✝² : SFinite ν
inst✝¹ : SFinite μ
inst✝ : SFinite τ
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ ∑' (i : ℕ × ℕ × ℕ), ((sfiniteSeq μ i.1).prod ((sfiniteSeq ν i.2.1).prod (sfiniteSeq τ i.2.2))) s =
    ∑' (i : (ℕ × ℕ) × ℕ), ((sfiniteSeq μ i.1.1).prod ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2))) s
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left✝ : IsClosed[t'] s
s_open : IsOpen[t'] s
⊢ MeasurableSet s

Tactic:
← borel_eq_borel_of_le t'_polish _ t't

Goal state after:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left✝ : IsClosed[t'] s
s_open : IsOpen[t'] s
⊢ MeasurableSet s

γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left✝ : IsClosed[t'] s
s_open : IsOpen[t'] s
⊢ PolishSpace γ
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ MeasurePreserving (fun x ↦ x / g) μ μ

Tactic:
by simp_rw [div_eq_mul_inv, measurePreserving_mul_right μ g⁻¹]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSpace H
inst✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ map (fun x ↦ x⁻¹ * g) μ = map (fun x ↦ x⁻¹ * g⁻¹⁻¹) μ

Tactic:
inv_inv

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSpace H
inst✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ map (fun x ↦ g * x⁻¹) μ = map (fun x ↦ g⁻¹⁻¹ * x⁻¹) μ

Tactic:
inv_inv

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
y : G
⊢ μ ((fun x ↦ x * y) ⁻¹' s) = 0 ↔ μ ((fun x ↦ x⁻¹⁻¹ * y⁻¹⁻¹) ⁻¹' s) = 0

Tactic:
inv_inv

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ μ ((fun x ↦ x * g) ⁻¹' s) = 0 → μ s = 0

Tactic:
measure_mul_right_null

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ μ s = 0 → μ s = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : ι → Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ((sum μ).withDensity f) s = (sum fun n ↦ (μ n).withDensity f) s

Tactic:
sum_apply _ hs,

Goal state after:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : ι → Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ((sum μ).withDensity f) s = ∑' (i : ι), ((μ i).withDensity f) s
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (∑' (n : ι), f n)) s = (sum fun n ↦ μ.withDensity (f n)) s

Tactic:
sum_apply _ hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (∑' (n : ι), f n)) s = ∑' (i : ι), (μ.withDensity (f i)) s
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
r : ℝ≥0∞
hr : μ K < r
⊢ ∃ U, K ⊆ U ∧ IsOpen[inst✝⁴] U ∧ μ U < r

Tactic:
by
  rcases hK.exists_open_superset_measure_lt_top μ with ⟨V, hKV, hVo, hμV⟩
  have := Fact.mk hμV
  obtain ⟨U, hKU, hUo, hμU⟩ : ∃ U, K ⊆ U ∧ IsOpen U ∧ μ.restrict V U < r :=
    exists_isOpen_lt_of_lt K r <| (restrict_apply_le _ _).trans_lt hr
  refine ⟨U ∩ V, subset_inter hKU hKV, hUo.inter hVo, ?_⟩
  rwa [restrict_apply hUo.measurableSet] at hμU

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y ↦ f y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ ∫⁻ (x : G), ν' ((fun z ↦ z * x) ⁻¹' s) * (f x⁻¹⁻¹ / ν' ((fun x_1 ↦ x_1 * x⁻¹⁻¹) ⁻¹' s)) ∂μ' = ∫⁻ (x : G), f x ∂μ'

Tactic:
inv_inv

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y ↦ f y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ ∫⁻ (x : G), ν' ((fun z ↦ z * x) ⁻¹' s) * (f x / ν' ((fun z ↦ z * x) ⁻¹' s)) ∂μ' = ∫⁻ (x : G), f x ∂μ'
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ μ s = 0 → μ ((fun x ↦ x * g) ⁻¹' s) = 0

Tactic:
measure_mul_right_null

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ μ s = 0 → μ s = 0
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this✝ : QuasiMeasurePreserving (fun h ↦ h * g⁻¹) μ μ
this : QuasiMeasurePreserving (fun x ↦ g⁻¹⁻¹ * x⁻¹⁻¹) μ μ
⊢ QuasiMeasurePreserving (fun h ↦ g * h) μ μ

Tactic:
inv_inv

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this✝ : QuasiMeasurePreserving (fun h ↦ h * g⁻¹) μ μ
this : QuasiMeasurePreserving (fun x ↦ g * x) μ μ
⊢ QuasiMeasurePreserving (fun h ↦ g * h) μ μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂μ.withDensity f', g x = AEMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (f' * g') x = (f' * g) x

Tactic:
ae_withDensity_iff_ae_restrict hf.measurable_mk

Goal state after:
case ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂μ.restrict {x | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (f' * g') x = (f' * g) x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ √x ≤ y ↔ x ≤ y ^ 2

Tactic:
by
  rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff_le_sq, sq, ← Real.toNNReal_mul hy,
    Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]

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

Goal state before:
pp: x y : ℝ
⊢ 0 ≤ y ∧ √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2

Tactic:
and_congr_right_iff

Goal state after:
x y : ℝ
⊢ 0 ≤ y → (√x ≤ y ↔ x ≤ y ^ 2)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
⊢ i x = f x * ((f x)⁻¹ * i x)

Tactic:
rw [← mul_assoc, ENNReal.mul_inv_cancel hx h'x.ne, one_mul]

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

Goal state before:
pp: z : ℂ
⊢ ‖z‖ ≤ √2 * max |z.re| |z.im|

Tactic:
by
  obtain ⟨x, y⟩ := z
  simp only [norm_def, normSq_mk, norm_def, ← sq]
  set m := max |x| |y|
  have hm₀ : 0 ≤ m := by positivity
  calc
    √(x ^ 2 + y ^ 2) ≤ √(m ^ 2 + m ^ 2) := by
      gcongr √(?_ + ?_) <;> rw [sq_le_sq, abs_of_nonneg hm₀]
      exacts [le_max_left _ _, le_max_right _ _]
    _ = √2 * m := by
      rw [← two_mul, Real.sqrt_mul, Real.sqrt_sq] <;> positivity

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

Goal state before:
pp: z : ℂ
⊢ ↑(nndist ((starRingEnd ℂ) z) z) = ↑(2 * Real.nnabs z.im)

Tactic:
by rw [← dist_nndist, NNReal.coe_mul, NNReal.coe_two, Real.coe_nnabs, dist_conj_self]

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a b c : ℂ), a + b + c = a + (b + c)

Tactic:
intros

Goal state after:
a✝ b✝ c✝ : ℂ
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a : ℂ), 0 + a = a

Tactic:
intros

Goal state after:
a✝ : ℂ
⊢ 0 + a✝ = a✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a : ℂ), a + 0 = a

Tactic:
intros

Goal state after:
a✝ : ℂ
⊢ a✝ + 0 = a✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (x : ℂ), 0 • x = 0

Tactic:
intros

Goal state after:
x✝ : ℂ
⊢ 0 • x✝ = 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (n : ℕ) (x : ℂ), (n + 1) • x = n • x + x

Tactic:
intros

Goal state after:
n✝ : ℕ
x✝ : ℂ
⊢ (n✝ + 1) • x✝ = n✝ • x✝ + x✝
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ 0 ≤ 1 - x ^ 2

Tactic:
nlinarith [abs_le.mp hx]

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a : ℂ), 0 • a = 0

Tactic:
intros

Goal state after:
a✝ : ℂ
⊢ 0 • a✝ = 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (n : ℕ) (a : ℂ), ↑n.succ • a = ↑n • a + a

Tactic:
intros

Goal state after:
n✝ : ℕ
a✝ : ℂ
⊢ ↑n✝.succ • a✝ = ↑n✝ • a✝ + a✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (n : ℕ) (a : ℂ), Int.negSucc n • a = -(↑n.succ • a)

Tactic:
intros

Goal state after:
n✝ : ℕ
a✝ : ℂ
⊢ Int.negSucc n✝ • a✝ = -(↑n✝.succ • a✝)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a : ℂ), -a + a = 0

Tactic:
intros

Goal state after:
a✝ : ℂ
⊢ -a✝ + a✝ = 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a b : ℂ), a + b = b + a

Tactic:
intros

Goal state after:
a✝ b✝ : ℂ
⊢ a✝ + b✝ = b✝ + a✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a b c : ℂ), a * b * c = a * (b * c)

Tactic:
intros

Goal state after:
a✝ b✝ c✝ : ℂ
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a : ℂ), 1 * a = a

Tactic:
intros

Goal state after:
a✝ : ℂ
⊢ 1 * a✝ = a✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a : ℂ), a * 1 = a

Tactic:
intros

Goal state after:
a✝ : ℂ
⊢ a✝ * 1 = a✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a : ℂ), 0 * a = 0

Tactic:
intros

Goal state after:
a✝ : ℂ
⊢ 0 * a✝ = 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a : ℂ), a * 0 = 0

Tactic:
intros

Goal state after:
a✝ : ℂ
⊢ a✝ * 0 = 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a b c : ℂ), a * (b + c) = a * b + a * c

Tactic:
intros

Goal state after:
a✝ b✝ c✝ : ℂ
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a b c : ℂ), (a + b) * c = a * c + b * c

Tactic:
intros

Goal state after:
a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a b : ℂ), a * b = b * a

Tactic:
intros

Goal state after:
a✝ b✝ : ℂ
⊢ a✝ * b✝ = b✝ * a✝
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ I ^ 2 = -1

Tactic:
by rw [sq, I_mul_I]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case hbc
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖f v‖ ≤ b * ‖v‖

Tactic:
apply hb

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case hbc
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖f v‖ ≤ b * ‖v‖

Tactic:
apply hb

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g✝ : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
⊢ ∀ (a b : NormedAddGroupHom V₁ V₂), g.comp (a + b) = g.comp a + g.comp b

Tactic:
intros

Goal state after:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g✝ : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
a✝ b✝ : NormedAddGroupHom V₁ V₂
⊢ g.comp (a✝ + b✝) = g.comp a✝ + g.comp b✝
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
⊢ ∀ (a b : NormedAddGroupHom V₂ V₃),
    AddMonoidHom.mk' (fun f ↦ (a + b).comp f) ⋯ =
      AddMonoidHom.mk' (fun f ↦ a.comp f) ⋯ + AddMonoidHom.mk' (fun f ↦ b.comp f) ⋯

Tactic:
intros

Goal state after:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
a✝ b✝ : NormedAddGroupHom V₂ V₃
⊢ AddMonoidHom.mk' (fun f ↦ (a✝ + b✝).comp f) ⋯ =
    AddMonoidHom.mk' (fun f ↦ a✝.comp f) ⋯ + AddMonoidHom.mk' (fun f ↦ b✝.comp f) ⋯
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
α : Type u_3
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
obtain (hx | hx) := eq_zero_or_norm_pos x⋆
    · simp [hx]
    · refine le_of_mul_le_mul_right ?_ hx
      simpa using norm_mul_self_le (x := x⋆) |>.trans <| norm_mul_le _ _

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * star (U * B) = U * B * (star B * star U)

Tactic:
by rw [star_mul]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
⊢ ‖x * x‖ = ‖x‖ ^ 2

Tactic:
by
  simpa [sq, hx.star_eq] using CStarRing.norm_star_mul_self (x := x)

Goal state after:
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₂ + -((y₁ * y₂) • 1)

Tactic:
← algebraMap_eq_smul_one,

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₁ * (algebraMap ℝ A) x₂ + -(algebraMap ℝ A) (y₁ * y₂)
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ x.re = y ↔ x = ↑y

Tactic:
by
  rw [← RCLike.re_eq_complex_re]
  exact RCLike.re_eq_ofReal_of_isSelfAdjoint hx

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
a : A
a_eq : a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ star (↑(ℜ a) + I • ↑(ℑ a)) * (↑(ℜ a) + I • ↑(ℑ a)) + (↑(ℜ a) + I • ↑(ℑ a)) * star (↑(ℜ a) + I • ↑(ℑ a)) =
    2 • (↑(ℜ a) * ↑(ℜ a) + ↑(ℑ a) * ↑(ℑ a))

Tactic:
by
      simp [mul_add, add_mul, smul_smul, mul_smul_comm,
        smul_mul_assoc]
      abel

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ |re z| / ‖z‖ ≤ 1

Tactic:
exact div_le_one_of_le₀ (abs_re_le_norm _) (norm_nonneg _)

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : { x // x ∈ e.source }
⊢ map Subtype.val (𝓝 x) = comap (↑e) (𝓝 (↑e ↑x)) ⊓ 𝓟 e.source

Tactic:
← map_comap_setCoe_val,

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : { x // x ∈ e.source }
⊢ map Subtype.val (𝓝 x) = map Subtype.val (comap Subtype.val (comap (↑e) (𝓝 (↑e ↑x))))
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Y → Z
x : Y
h : x ∈ e.target
⊢ ContinuousAt f x ↔ ContinuousAt (f ∘ ↑e) (↑e.symm x)

Tactic:
rw [← continuousWithinAt_univ, e.continuousWithinAt_iff_continuousWithinAt_comp_right h,
    preimage_univ, continuousWithinAt_univ]

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝² : RCLike K
𝕜 : Type u_3
𝕜' : Type u_4
inst✝¹ : RCLike 𝕜
inst✝ : RCLike 𝕜'
x✝¹ : ℝ
x✝ : 𝕜
⊢ ↑(re (x✝¹ • x✝)) + ↑(im (x✝¹ • x✝)) * I = (RingHom.id ℝ) x✝¹ • (↑(re x✝) + ↑(im x✝) * I)

Tactic:
by simp [real_smul_eq_coe_mul, mul_assoc]

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

Goal state before:
pp: case hbc
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ c ≤ max c 1

Tactic:
exact le_max_left _ _

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
x : α
hle : ‖f' x‖ ≤ 2⁻¹ * ‖f' x‖
hne : ‖f' x‖ ≠ 0
⊢ False

Tactic:
← div_eq_inv_mul

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
x : α
hle : ‖f' x‖ ≤ ‖f' x‖ / 2
hne : ‖f' x‖ ≠ 0
⊢ False