harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_swap₁₂_sign (p₁ p₂ p₃ : P) : -(∡ p₁ p₂ p₃).sign = (∡ p₂ p₁ p₃).sign

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ (o.oangle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ + -1 • (p₃ -ᵥ p₂))).sign = -(o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign

Tactic:
nth_rw 2 [← one_smul ℝ (p₁ -ᵥ p₂)]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ (o.oangle (p₁ -ᵥ p₂) (1 • (p₁ -ᵥ p₂) + -1 • (p₃ -ᵥ p₂))).sign = -(o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ (o.oangle (p₁ -ᵥ p₂) (1 • (p₁ -ᵥ p₂) + -1 • (p₃ -ᵥ p₂))).sign = -(o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign

Tactic:
rw [o.oangle_sign_smul_add_smul_right]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ SignType.sign (-1) * (o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign = -(o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ SignType.sign (-1) * (o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign = -(o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ -(∡ p₁ p₂ p₃).sign = (∡ p₂ p₁ p₃).sign

Tactic:
rw [eq_comm, oangle, oangle, ← o.oangle_neg_neg, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev, ←
  vsub_sub_vsub_cancel_left p₁ p₃ p₂, ← neg_vsub_eq_vsub_rev p₃ p₂, sub_eq_add_neg,
  neg_vsub_eq_vsub_rev p₂ p₁, add_comm, ← @neg_one_smul ℝ]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ (o.oangle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ + -1 • (p₃ -ᵥ p₂))).sign = -(o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign
-- Mathlib/CategoryTheory/Limits/Cones.lean
theorem CoconeMorphism.ext {c c' : Cocone F} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g

Proof state:
case mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c c' : Cocone F
g : c ⟶ c'
hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), c.ι.app j ≫ hom✝ = c'.ι.app j
w : { hom := hom✝, w := w✝ }.hom = g.hom
⊢ { hom := hom✝, w := w✝ } = g

Tactic:
cases g

Result:
case mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c c' : Cocone F
hom✝¹ : c.pt ⟶ c'.pt
w✝¹ : ∀ (j : J), c.ι.app j ≫ hom✝¹ = c'.ι.app j
hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), c.ι.app j ≫ hom✝ = c'.ι.app j
w : { hom := hom✝¹, w := w✝¹ }.hom = { hom := hom✝, w := w✝ }.hom
⊢ { hom := hom✝¹, w := w✝¹ } = { hom := hom✝, w := w✝ }

Proof state:
case mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c c' : Cocone F
hom✝¹ : c.pt ⟶ c'.pt
w✝¹ : ∀ (j : J), c.ι.app j ≫ hom✝¹ = c'.ι.app j
hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), c.ι.app j ≫ hom✝ = c'.ι.app j
w : { hom := hom✝¹, w := w✝¹ }.hom = { hom := hom✝, w := w✝ }.hom
⊢ { hom := hom✝¹, w := w✝¹ } = { hom := hom✝, w := w✝ }

Tactic:
congr

Result:
no goals

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c c' : Cocone F
f g : c ⟶ c'
w : f.hom = g.hom
⊢ f = g

Tactic:
cases f

Result:
case mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c c' : Cocone F
g : c ⟶ c'
hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), c.ι.app j ≫ hom✝ = c'.ι.app j
w : { hom := hom✝, w := w✝ }.hom = g.hom
⊢ { hom := hom✝, w := w✝ } = g
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_iUnion [Finite ι] {t : ι → Set α} (h : Pairwise (Disjoint on t))
    (ht : ∀ i, (t i).Finite) : ∏ᶠ a ∈ ⋃ i : ι, t i, f a = ∏ᶠ i, ∏ᶠ a ∈ t i, f a

Proof state:
case intro.intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i, (fun i => ↑(t i)) i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i => ↑(t i)) i), f a

Tactic:
rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
  Finset.prod_biUnion]

Result:
case intro.intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ ∏ x : ι, ∏ i ∈ t x, f i = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i => ↑(t i)) i), f a

case intro.intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ (↑Finset.univ).PairwiseDisjoint t

Proof state:
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
t : ι → Set α
h : Pairwise (Disjoint on t)
ht : ∀ (i : ι), (t i).Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a

Tactic:
cases nonempty_fintype ι

Result:
case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
t : ι → Set α
h : Pairwise (Disjoint on t)
ht : ∀ (i : ι), (t i).Finite
val✝ : Fintype ι
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a

Proof state:
case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
t : ι → Set α
h : Pairwise (Disjoint on t)
ht : ∀ (i : ι), (t i).Finite
val✝ : Fintype ι
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a

Tactic:
lift t to ι → Finset α using ht

Result:
case intro.intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i, (fun i => ↑(t i)) i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i => ↑(t i)) i), f a

Proof state:
case intro.intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ ∏ x : ι, ∏ i ∈ t x, f i = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i => ↑(t i)) i), f a

Tactic:
simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i => ↑(t i))
⊢ (↑Finset.univ).PairwiseDisjoint t

Tactic:
exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma map_prodMkLeft (γ : Type*) [MeasurableSpace γ] (κ : Kernel α β) (f : β → δ) :
    map (prodMkLeft γ κ) f = prodMkLeft γ (map κ f)

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
γ : Type u_5
inst✝ : MeasurableSpace γ
κ : Kernel α β
f : β → δ
hf : ¬Measurable f
⊢ (prodMkLeft γ κ).map f = prodMkLeft γ (κ.map f)

Tactic:
simp [map_of_not_measurable _ hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
γ : Type u_5
inst✝ : MeasurableSpace γ
κ : Kernel α β
f : β → δ
⊢ (prodMkLeft γ κ).map f = prodMkLeft γ (κ.map f)

Tactic:
by_cases hf : Measurable f

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
γ : Type u_5
inst✝ : MeasurableSpace γ
κ : Kernel α β
f : β → δ
hf : Measurable f
⊢ (prodMkLeft γ κ).map f = prodMkLeft γ (κ.map f)

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
γ : Type u_5
inst✝ : MeasurableSpace γ
κ : Kernel α β
f : β → δ
hf : ¬Measurable f
⊢ (prodMkLeft γ κ).map f = prodMkLeft γ (κ.map f)

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
γ : Type u_5
inst✝ : MeasurableSpace γ
κ : Kernel α β
f : β → δ
hf : Measurable f
⊢ (prodMkLeft γ κ).map f = prodMkLeft γ (κ.map f)

Tactic:
simp only [map, hf, ↓reduceDIte]

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
γ : Type u_5
inst✝ : MeasurableSpace γ
κ : Kernel α β
f : β → δ
hf : Measurable f
⊢ (prodMkLeft γ κ).mapOfMeasurable f ⋯ = prodMkLeft γ (κ.mapOfMeasurable f ⋯)

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
δ : Type u_4
mδ : MeasurableSpace δ
γ : Type u_5
inst✝ : MeasurableSpace γ
κ : Kernel α β
f : β → δ
hf : Measurable f
⊢ (prodMkLeft γ κ).mapOfMeasurable f ⋯ = prodMkLeft γ (κ.mapOfMeasurable f ⋯)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem tendsto_setToFun_of_dominated_convergence (hT : DominatedFinMeasAdditive μ T C)
    {fs : ℕ → α → E} {f : α → E} (bound : α → ℝ)
    (fs_measurable : ∀ n, AEStronglyMeasurable (fs n) μ) (bound_integrable : Integrable bound μ)
    (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖fs n a‖ ≤ bound a)
    (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))) :
    Tendsto (fun n => setToFun μ T hT (fs n)) atTop (𝓝 <| setToFun μ T hT f)

Proof state:
case h.e'_3.h.e_a
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero : Tendsto (fun n => (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
x : α
hx : ↑↑(Integrable.toL1 (fs n - f) ⋯) x = (fs n - f) x
⊢ (fun a => ‖↑↑(Integrable.toL1 (fs n - f) ⋯) a‖ₑ) x = (fun a => ENNReal.ofReal ‖fs n a - f a‖) x

Tactic:
dsimp only

Result:
case h.e'_3.h.e_a
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero : Tendsto (fun n => (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
x : α
hx : ↑↑(Integrable.toL1 (fs n - f) ⋯) x = (fs n - f) x
⊢ ‖↑↑(Integrable.toL1 (fs n - f) ⋯) x‖ₑ = ENNReal.ofReal ‖fs n x - f x‖
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem setLIntegral_prod [SFinite μ] {s : Set α} (t : Set β) (f : α × β → ENNReal)
    (hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))) :
    ∫⁻ z in s ×ˢ t, f z ∂μ.prod ν = ∫⁻ x in s, ∫⁻ y in t, f (x, y) ∂ν ∂μ

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ ∫⁻ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂ν ∂μ

Tactic:
rw [← Measure.prod_restrict, lintegral_prod _ (by rwa [Measure.prod_restrict])]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ AEMeasurable f ((μ.restrict s).prod (ν.restrict t))

Tactic:
rwa [Measure.prod_restrict]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Units.lean
theorem inverse_add_norm_diff_first_order (x : Rˣ) :
    (fun t : R => inverse (↑x + t) - ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
⊢ (fun t => inverse (↑x + t) - ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖

Tactic:
simpa using inverse_add_norm_diff_nth_order x 1

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_range_le_of_locally_lipschitzOn [SecondCountableTopology X] {f : X → Y}
    (hf : ∀ x : X, ∃ C : ℝ≥0, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s) :
    dimH (range f) ≤ dimH (univ : Set X)

Proof state:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s
⊢ dimH (f '' univ) ≤ dimH univ

Tactic:
refine dimH_image_le_of_locally_lipschitzOn fun x _ => ?_

Result:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s
x : X
x✝ : x ∈ univ
⊢ ∃ C, ∃ t ∈ 𝓝[univ] x, LipschitzOnWith C f t

Proof state:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s
x : X
x✝ : x ∈ univ
⊢ ∃ C, ∃ t ∈ 𝓝[univ] x, LipschitzOnWith C f t

Tactic:
simpa only [exists_prop, nhdsWithin_univ] using hf x

Result:
no goals

Proof state:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s
⊢ dimH (range f) ≤ dimH univ

Tactic:
rw [← image_univ]

Result:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s
⊢ dimH (f '' univ) ≤ dimH univ
-- Mathlib/NumberTheory/LSeries/ZMod.lean
lemma LFunction_def_odd (hΦ : Φ.Odd) (s : ℂ) :
    LFunction Φ s = N ^ (-s) * ∑ j : ZMod N, Φ j * hurwitzZetaOdd (toAddCircle j) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ LFunction Φ s = ↑N ^ (-s) * ∑ j : ZMod N, Φ j * hurwitzZetaOdd (toAddCircle j) s

Tactic:
simp only [LFunction, hurwitzZeta, mul_add (Φ _), sum_add_distrib]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ ↑N ^ (-s) *
      (∑ x : ZMod N, Φ x * hurwitzZetaEven (toAddCircle x) s + ∑ x : ZMod N, Φ x * hurwitzZetaOdd (toAddCircle x) s) =
    ↑N ^ (-s) * ∑ j : ZMod N, Φ j * hurwitzZetaOdd (toAddCircle j) s

Proof state:
case e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ ∑ x : ZMod N, -(Φ x * hurwitzZetaEven (toAddCircle x) s) = ∑ x : ZMod N, Φ x * hurwitzZetaEven (toAddCircle x) s

Tactic:
refine Fintype.sum_equiv (.neg _) _ _ fun i ↦ ?_

Result:
case e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
i : ZMod N
⊢ -(Φ i * hurwitzZetaEven (toAddCircle i) s) =
    Φ ((Equiv.neg (ZMod N)) i) * hurwitzZetaEven (toAddCircle ((Equiv.neg (ZMod N)) i)) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ ↑N ^ (-s) *
      (∑ x : ZMod N, Φ x * hurwitzZetaEven (toAddCircle x) s + ∑ x : ZMod N, Φ x * hurwitzZetaOdd (toAddCircle x) s) =
    ↑N ^ (-s) * ∑ j : ZMod N, Φ j * hurwitzZetaOdd (toAddCircle j) s

Tactic:
congr 1

Result:
case e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ ∑ x : ZMod N, Φ x * hurwitzZetaEven (toAddCircle x) s + ∑ x : ZMod N, Φ x * hurwitzZetaOdd (toAddCircle x) s =
    ∑ j : ZMod N, Φ j * hurwitzZetaOdd (toAddCircle j) s

Proof state:
case e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
i : ZMod N
⊢ -(Φ i * hurwitzZetaEven (toAddCircle i) s) =
    Φ ((Equiv.neg (ZMod N)) i) * hurwitzZetaEven (toAddCircle ((Equiv.neg (ZMod N)) i)) s

Tactic:
simp only [Equiv.neg_apply, hΦ i, map_neg, hurwitzZetaEven_neg, neg_mul]

Result:
no goals

Proof state:
case e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ ∑ x : ZMod N, Φ x * hurwitzZetaEven (toAddCircle x) s + ∑ x : ZMod N, Φ x * hurwitzZetaOdd (toAddCircle x) s =
    ∑ j : ZMod N, Φ j * hurwitzZetaOdd (toAddCircle j) s

Tactic:
simp only [add_left_eq_self, ← neg_eq_self ℂ, ← sum_neg_distrib]

Result:
case e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ ∑ x : ZMod N, -(Φ x * hurwitzZetaEven (toAddCircle x) s) = ∑ x : ZMod N, Φ x * hurwitzZetaEven (toAddCircle x) s
-- Mathlib/Data/Set/Image.lean
theorem Injective.compl_image_eq (hf : Injective f) (s : Set α) :
    (f '' s)ᶜ = f '' sᶜ ∪ (range f)ᶜ

Proof state:
case h.inl.intro
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
x : α
⊢ f x ∈ (f '' s)ᶜ ↔ f x ∈ f '' sᶜ ∪ (range f)ᶜ

Tactic:
simp [hf.eq_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ (f '' s)ᶜ = f '' sᶜ ∪ (range f)ᶜ

Tactic:
ext y

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
y : β
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ (range f)ᶜ

Proof state:
case h.inr
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
y : β
hx : ∀ (x : α), ¬f x = y
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ (range f)ᶜ

Tactic:
simp [hx]

Result:
no goals

Proof state:
case h.inr
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
y : β
hx : y ∉ range f
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ (range f)ᶜ

Tactic:
rw [mem_range, not_exists] at hx

Result:
case h.inr
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
y : β
hx : ∀ (x : α), ¬f x = y
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ (range f)ᶜ

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
y : β
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ (range f)ᶜ

Tactic:
rcases em (y ∈ range f) with (⟨x, rfl⟩ | hx)

Result:
case h.inl.intro
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
x : α
⊢ f x ∈ (f '' s)ᶜ ↔ f x ∈ f '' sᶜ ∪ (range f)ᶜ

case h.inr
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
y : β
hx : y ∉ range f
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ (range f)ᶜ
-- Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean
theorem normSq_exp (q : ℍ[ℝ]) : normSq (exp ℝ q) = exp ℝ q.re ^ 2 :=
  calc
    normSq (exp ℝ q) =
        normSq (exp ℝ q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im))

Proof state:
q : ℍ
⊢ normSq (exp ℝ q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)) =
    exp ℝ q.re ^ 2 * normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)

Tactic:
rw [normSq_smul]

Result:
no goals

Proof state:
q : ℍ
⊢ exp ℝ q.re ^ 2 * (Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2) = exp ℝ q.re ^ 2

Tactic:
rw [Real.cos_sq_add_sin_sq, mul_one]

Result:
no goals

Proof state:
case e_a.inl
q : ℍ
hv : ‖q.im‖ = 0
⊢ normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2

Tactic:
simp [hv]

Result:
no goals

Proof state:
q : ℍ
⊢ normSq (exp ℝ q) = normSq (exp ℝ q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im))

Tactic:
rw [exp_eq]

Result:
no goals

Proof state:
case e_a.inr
q : ℍ
hv : ‖q.im‖ ≠ 0
⊢ normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2

Tactic:
rw [normSq_add, normSq_smul, star_smul, coe_mul_eq_smul, smul_re, smul_re, star_re, im_re,
  smul_zero, smul_zero, mul_zero, add_zero, div_pow, normSq_coe,
  normSq_eq_norm_mul_self, ← sq, div_mul_cancel₀ _ (pow_ne_zero _ hv)]

Result:
no goals

Proof state:
q : ℍ
⊢ exp ℝ q.re ^ 2 * normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) =
    exp ℝ q.re ^ 2 * (Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2)

Tactic:
congr 1

Result:
case e_a
q : ℍ
⊢ normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2

Proof state:
case e_a
q : ℍ
⊢ normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2

Tactic:
obtain hv | hv := eq_or_ne ‖q.im‖ 0

Result:
case e_a.inl
q : ℍ
hv : ‖q.im‖ = 0
⊢ normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2

case e_a.inr
q : ℍ
hv : ‖q.im‖ ≠ 0
⊢ normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2
-- Mathlib/Data/Set/Card.lean
theorem encard_eq_one : s.encard = 1 ↔ ∃ x, s = {x}

Proof state:
α : Type u_1
s : Set α
h : s.encard = 1
⊢ ∃ x, s = {x}

Tactic:
obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)

Result:
case intro
α : Type u_1
s : Set α
h : s.encard = 1
x : α
hx : x ∈ s
⊢ ∃ x, s = {x}

Proof state:
α : Type u_1
s : Set α
h : s.encard = 1
⊢ 1 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Set α
h : s.encard = 1
x : α
hx : x ∈ s
⊢ s.encard ≤ {x}.encard

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
h : s.encard = 1
⊢ s.encard ≠ 0

Tactic:
rw [h]

Result:
α : Type u_1
s : Set α
h : s.encard = 1
⊢ 1 ≠ 0

Proof state:
α : Type u_1
s : Set α
⊢ s.encard = 1 ↔ ∃ x, s = {x}

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨x, hx⟩ ↦ by rw [hx, encard_singleton]⟩

Result:
α : Type u_1
s : Set α
h : s.encard = 1
⊢ ∃ x, s = {x}

Proof state:
α : Type u_1
s : Set α
h : s.encard = 1
x : α
hx : x ∈ s
⊢ {x} ⊆ s

Tactic:
simpa

Result:
no goals

Proof state:
case intro
α : Type u_1
s : Set α
h : s.encard = 1
x : α
hx : x ∈ s
⊢ ∃ x, s = {x}

Tactic:
exact ⟨x, ((finite_singleton x).eq_of_subset_of_encard_le' (by simpa) (by simp [h])).symm⟩

Result:
no goals

Proof state:
α : Type u_1
s : Set α
x✝ : ∃ x, s = {x}
x : α
hx : s = {x}
⊢ s.encard = 1

Tactic:
rw [hx, encard_singleton]

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Hom.lean
theorem lift_unique (H : c ≤ ker f) (g : c.Quotient →* P) (Hg : g.comp c.mk' = f) :
    g = c.lift f H :=
  (lift_funext g (c.lift f H)) fun x => by
    subst f
    rfl

Proof state:
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
g : c.Quotient →* P
Hg : g.comp c.mk' = f
x : M
⊢ g ↑x = (c.lift f H) ↑x

Tactic:
subst f

Result:
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
g : c.Quotient →* P
x : M
H : c ≤ ker (g.comp c.mk')
⊢ g ↑x = (c.lift (g.comp c.mk') H) ↑x

Proof state:
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
g : c.Quotient →* P
x : M
H : c ≤ ker (g.comp c.mk')
⊢ g ↑x = (c.lift (g.comp c.mk') H) ↑x

Tactic:
rfl

Result:
no goals