harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiable_iff_target :
    MDifferentiable I I' f ↔
      Continuous f ∧ ∀ y : M',
        MDifferentiableOn I 𝓘(𝕜, E') (extChartAt I' y ∘ f) (f ⁻¹' (extChartAt I' y).source)

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
⊢ (ContinuousOn f univ ∧
      ∀ (y : M'), MDifferentiableOn I 𝓘(𝕜, E') (↑(extChartAt I' y) ∘ f) (univ ∩ f ⁻¹' (extChartAt I' y).source)) ↔
    Continuous f ∧ ∀ (y : M'), MDifferentiableOn I 𝓘(𝕜, E') (↑(extChartAt I' y) ∘ f) (f ⁻¹' (extChartAt I' y).source)

Tactic:
simp [continuous_iff_continuousOn_univ]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
⊢ MDifferentiable I I' f ↔
    Continuous f ∧ ∀ (y : M'), MDifferentiableOn I 𝓘(𝕜, E') (↑(extChartAt I' y) ∘ f) (f ⁻¹' (extChartAt I' y).source)

Tactic:
rw [← mdifferentiableOn_univ, mdifferentiableOn_iff_target]

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
⊢ (ContinuousOn f univ ∧
      ∀ (y : M'), MDifferentiableOn I 𝓘(𝕜, E') (↑(extChartAt I' y) ∘ f) (univ ∩ f ⁻¹' (extChartAt I' y).source)) ↔
    Continuous f ∧ ∀ (y : M'), MDifferentiableOn I 𝓘(𝕜, E') (↑(extChartAt I' y) ∘ f) (f ⁻¹' (extChartAt I' y).source)
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
@[simp]
lemma infinitePlace_apply (v : InfinitePlace ℚ) (x : ℚ) : v x = |x|

Proof state:
v : InfinitePlace ℚ
x : ℚ
⊢ v x = ↑|x|

Tactic:
rw [NumberField.InfinitePlace.coe_apply]

Result:
v : InfinitePlace ℚ
x : ℚ
⊢ ↑v x = ↑|x|

Proof state:
case mk.intro
x : ℚ
w✝ : ℚ →+* ℂ
⊢ ↑⟨place w✝, ⋯⟩ x = ↑|x|

Tactic:
simp

Result:
no goals

Proof state:
v : InfinitePlace ℚ
x : ℚ
⊢ ↑v x = ↑|x|

Tactic:
obtain ⟨_, _, rfl⟩ := v

Result:
case mk.intro
x : ℚ
w✝ : ℚ →+* ℂ
⊢ ↑⟨place w✝, ⋯⟩ x = ↑|x|
-- Mathlib/CategoryTheory/EqToHom.lean
theorem map_comp_heq' (hobj : ∀ X : C, F.obj X = G.obj X)
    (hmap : ∀ {X Y} (f : X ⟶ Y), HEq (F.map f) (G.map f)) :
    HEq (F.map (f ≫ g)) (G.map (f ≫ g))

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hobj : ∀ (X : C), F.obj X = G.obj X
hmap : ∀ {X Y : C} (f : X ⟶ Y), HEq (F.map f) (G.map f)
⊢ HEq (F.map (f ≫ g)) (G.map (f ≫ g))

Tactic:
rw [Functor.hext hobj fun _ _ => hmap]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Localization.lean
lemma W_sheafToPreheaf_map_iff_isIso {F₁ F₂ : Sheaf J A} (φ : F₁ ⟶ F₂) :
    J.W ((sheafToPresheaf J A).map φ) ↔ IsIso φ

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_4, u_2} A
F₁ F₂ : Sheaf J A
φ : F₁ ⟶ F₂
⊢ J.W ((sheafToPresheaf J A).map φ) ↔ IsIso φ

Tactic:
rw [W_eq_W_range_sheafToPresheaf_obj, LeftBousfield.W_iff_isIso _ _ ⟨_, rfl⟩ ⟨_, rfl⟩,
  isIso_iff_of_reflects_iso]

Result:
no goals
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ X ω ^ p` is
integrable for all nonnegative `p : ℝ`. -/
lemma integrable_rpow_of_integrable_exp_mul (ht : t ≠ 0)
    (ht_int_pos : Integrable (fun ω ↦ exp (t * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp (- t * X ω)) μ) {p : ℝ} (hp : 0 ≤ p) :
    Integrable (fun ω ↦ X ω ^ p) μ

Proof state:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω => rexp ((0 - t) * X ω)) μ

Tactic:
simpa using ht_int_neg

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω => X ω ^ p) μ

Tactic:
have h := integrable_rpow_mul_exp_of_integrable_exp_mul (μ := μ) (X := X) ht (v := 0) ?_ ?_ hp

Result:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
h : Integrable (fun ω => X ω ^ p * rexp (0 * X ω)) μ
⊢ Integrable (fun ω => X ω ^ p) μ

case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω => rexp ((0 + t) * X ω)) μ

case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω => rexp ((0 - t) * X ω)) μ

Proof state:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω => rexp ((0 + t) * X ω)) μ

Tactic:
simpa using ht_int_pos

Result:
no goals

Proof state:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
h : Integrable (fun ω => X ω ^ p * rexp (0 * X ω)) μ
⊢ Integrable (fun ω => X ω ^ p) μ

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Order/SuccPred/Archimedean.lean
lemma strictMonoOn_of_lt_succ (hs : s.OrdConnected)
    (hf : ∀ a, ¬ IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)) : StrictMonoOn f s

Proof state:
case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : succ^[n + 1] a ∈ s → f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
this : succ^[n + 1] a ∈ s
hb' : IsMax (succ^[n + 1] a)
⊢ f a < f (succ^[n + 1] a)

Tactic:
exact hn this

Result:
no goals

Proof state:
case intro.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
n : ℕ
hb : succ^[n + 1] a ∈ s
hab : ¬IsMax a
⊢ f a < f (succ^[n + 1] a)

Tactic:
induction' n with n hn

Result:
case intro.succ.zero
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
hb : succ^[0 + 1] a ∈ s
⊢ f a < f (succ^[0 + 1] a)

case intro.succ.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : succ^[n + 1] a ∈ s → f a < f (succ^[n + 1] a)
hb : succ^[n + 1 + 1] a ∈ s
⊢ f a < f (succ^[n + 1 + 1] a)

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f a < f b

Tactic:
obtain ⟨n, rfl⟩ := exists_succ_iterate_of_le hab.le

Result:
case intro
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
n : ℕ
hb : succ^[n] a ∈ s
hab : a < succ^[n] a
⊢ f a < f (succ^[n] a)
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem hasFDerivAt [DecidableEq ι] : HasFDerivAt f (f.linearDeriv x) x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
⊢ HasFDerivAt (⇑f) ((continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F) (f.toFormalMultilinearSeries.changeOrigin x 1))
    x

Tactic:
convert f.hasFiniteFPowerSeriesOnBall.hasFDerivAt (y := x) ENNReal.coe_lt_top

Result:
case h.e'_13
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
⊢ x = 0 + x

Proof state:
case h.e'_13
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
⊢ x = 0 + x

Tactic:
rw [zero_add]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
⊢ HasFDerivAt (⇑f) (f.linearDeriv x) x

Tactic:
rw [← changeOrigin_toFormalMultilinearSeries]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
⊢ HasFDerivAt (⇑f) ((continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F) (f.toFormalMultilinearSeries.changeOrigin x 1))
    x
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_affineCombinationSingleWeights [DecidableEq ι] {i : ι} (h : i ∈ s) :
    ∑ j ∈ s, affineCombinationSingleWeights k i j = 1

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i : ι
h : i ∈ s
⊢ ∑ j ∈ s, affineCombinationSingleWeights k i j = affineCombinationSingleWeights k i i

Tactic:
exact sum_eq_single_of_mem i h fun j _ hj => affineCombinationSingleWeights_apply_of_ne k hj

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i : ι
h : i ∈ s
⊢ ∑ j ∈ s, affineCombinationSingleWeights k i j = 1

Tactic:
rw [← affineCombinationSingleWeights_apply_self k i]

Result:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i : ι
h : i ∈ s
⊢ ∑ j ∈ s, affineCombinationSingleWeights k i j = affineCombinationSingleWeights k i i
-- Mathlib/Order/Interval/Set/SurjOn.lean
theorem surjOn_Ioc_of_monotone_surjective (h_mono : Monotone f) (h_surj : Function.Surjective f)
    (a b : α) : SurjOn f (Ioc a b) (Ioc (f a) (f b))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
⊢ SurjOn f (Ioc a b) (Ioc (f a) (f b))

Tactic:
simpa using surjOn_Ico_of_monotone_surjective h_mono.dual h_surj (toDual b) (toDual a)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem invOf_diagonal_eq {α} [Semiring α] (v : n → α) [Invertible v] [Invertible (diagonal v)] :
    ⅟ (diagonal v) = diagonal (⅟ v)

Proof state:
n : Type u'
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
α : Type u_2
inst✝² : Semiring α
v : n → α
inst✝¹ : Invertible v
inst✝ : Invertible (diagonal v)
⊢ ⅟(diagonal v) = diagonal ⅟v

Tactic:
letI := diagonalInvertible v

Result:
n : Type u'
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
α : Type u_2
inst✝² : Semiring α
v : n → α
inst✝¹ : Invertible v
inst✝ : Invertible (diagonal v)
this : Invertible (diagonal v) := diagonalInvertible v
⊢ ⅟(diagonal v) = diagonal ⅟v

Proof state:
n : Type u'
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
α : Type u_2
inst✝² : Semiring α
v : n → α
inst✝¹ : Invertible v
inst✝ : Invertible (diagonal v)
this : Invertible (diagonal v) := diagonalInvertible v
⊢ ⅟(diagonal v) = diagonal ⅟v

Tactic:
convert (rfl : ⅟ (diagonal v) = _)

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma zpow_neg_mul_zpow_self (n : ℤ) (ha : a ≠ 0) : a ^ (-n) * a ^ n = 1

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
ha : a ≠ 0
⊢ a ^ (-n) * a ^ n = 1

Tactic:
rw [zpow_neg]

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
ha : a ≠ 0
⊢ (a ^ n)⁻¹ * a ^ n = 1

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
ha : a ≠ 0
⊢ (a ^ n)⁻¹ * a ^ n = 1

Tactic:
exact inv_mul_cancel₀ (zpow_ne_zero n ha)

Result:
no goals
-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem ae_tendsto_limRatioMeas :
    ∀ᵐ x ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))

Proof state:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
hx : Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
h'x : v.limRatio ρ x = AEMeasurable.mk (v.limRatio ρ) ⋯ x
⊢ Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))

Tactic:
rwa [h'x] at hx

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))

Tactic:
filter_upwards [v.ae_tendsto_limRatio hρ, AEMeasurable.ae_eq_mk (v.aemeasurable_limRatio hρ)]

Result:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ (a : α),
    Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 (v.limRatio ρ a)) →
      v.limRatio ρ a = AEMeasurable.mk (v.limRatio ρ) ⋯ a →
        Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 (v.limRatioMeas hρ a))

Proof state:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ (a : α),
    Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 (v.limRatio ρ a)) →
      v.limRatio ρ a = AEMeasurable.mk (v.limRatio ρ) ⋯ a →
        Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 (v.limRatioMeas hρ a))

Tactic:
intro x hx h'x

Result:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
hx : Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
h'x : v.limRatio ρ x = AEMeasurable.mk (v.limRatio ρ) ⋯ x
⊢ Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))
-- Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean
theorem convs'Aux_stable_of_terminated {s : Stream'.Seq <| Pair K} (n_le_m : n ≤ m)
    (terminatedAt_n : s.TerminatedAt n) : convs'Aux s m = convs'Aux s n

Proof state:
K : Type u_1
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
n_le_m : n ≤ m
terminatedAt_n : s.TerminatedAt n
⊢ convs'Aux s m = convs'Aux s n

Tactic:
induction n_le_m with
| refl => rfl
| step n_le_m IH =>
  refine (convs'Aux_stable_step_of_terminated (?_)).trans IH
  exact s.terminated_stable n_le_m terminatedAt_n

Result:
no goals

Proof state:
case refl
K : Type u_1
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
⊢ convs'Aux s n = convs'Aux s n

Tactic:
rfl

Result:
no goals

Proof state:
case step
K : Type u_1
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
m✝ : ℕ
n_le_m : n.le m✝
IH : convs'Aux s m✝ = convs'Aux s n
⊢ convs'Aux s m✝.succ = convs'Aux s n

Tactic:
refine (convs'Aux_stable_step_of_terminated (?_)).trans IH

Result:
case step
K : Type u_1
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
m✝ : ℕ
n_le_m : n.le m✝
IH : convs'Aux s m✝ = convs'Aux s n
⊢ s.TerminatedAt m✝

Proof state:
case step
K : Type u_1
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
m✝ : ℕ
n_le_m : n.le m✝
IH : convs'Aux s m✝ = convs'Aux s n
⊢ s.TerminatedAt m✝

Tactic:
exact s.terminated_stable n_le_m terminatedAt_n

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem fromEdgeSet_edgeSet : fromEdgeSet G.edgeSet = G

Proof state:
V : Type u
G : SimpleGraph V
⊢ fromEdgeSet G.edgeSet = G

Tactic:
ext v w

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
v w : V
⊢ (fromEdgeSet G.edgeSet).Adj v w ↔ G.Adj v w

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
v w : V
⊢ (fromEdgeSet G.edgeSet).Adj v w ↔ G.Adj v w

Tactic:
exact ⟨fun h => h.1, fun h => ⟨h, G.ne_of_adj h⟩⟩

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc (attr := simp)]
lemma inlX_sndX (i j : ι) (hij : c.Rel j i) :
    inlX φ i j hij ≫ sndX φ j = 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
⊢ inlX φ i j hij ≫ sndX φ j = 0

Tactic:
obtain rfl := c.next_eq' hij

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
j : ι
hij : c.Rel j (c.next j)
⊢ inlX φ (c.next j) j hij ≫ sndX φ j = 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
j : ι
hij : c.Rel j (c.next j)
⊢ inlX φ (c.next j) j hij ≫ sndX φ j = 0

Tactic:
simp [inlX, sndX, dif_pos hij]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
theorem hasCoequalizer_of_common_section [HasReflexiveCoequalizers C] {A B : C} {f g : A ⟶ B}
    (r : B ⟶ A) (rf : r ≫ f = 𝟙 _) (rg : r ≫ g = 𝟙 _) : HasCoequalizer f g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasReflexiveCoequalizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
rf : r ≫ f = 𝟙 B
rg : r ≫ g = 𝟙 B
this : IsReflexivePair f g := IsReflexivePair.mk' r rf rg
⊢ HasCoequalizer f g

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasReflexiveCoequalizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
rf : r ≫ f = 𝟙 B
rg : r ≫ g = 𝟙 B
⊢ HasCoequalizer f g

Tactic:
letI := IsReflexivePair.mk' r rf rg

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasReflexiveCoequalizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
rf : r ≫ f = 𝟙 B
rg : r ≫ g = 𝟙 B
this : IsReflexivePair f g := IsReflexivePair.mk' r rf rg
⊢ HasCoequalizer f g
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourierCoeffOn.const_smul {a b : ℝ} (f : ℝ → E) (c : ℂ) (n : ℤ) (hab : a < b) :
    fourierCoeffOn hab (c • f) n = c • fourierCoeffOn hab f n

Proof state:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
c : ℂ
n : ℤ
hab : a < b
⊢ 0 < b - a

Tactic:
linarith

Result:
no goals

Proof state:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
c : ℂ
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ fourierCoeffOn hab (c • f) n = c • fourierCoeffOn hab f n

Tactic:
apply fourierCoeff.const_smul

Result:
no goals

Proof state:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
c : ℂ
n : ℤ
hab : a < b
⊢ fourierCoeffOn hab (c • f) n = c • fourierCoeffOn hab f n

Tactic:
haveI := Fact.mk (by linarith : 0 < b - a)

Result:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
c : ℂ
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ fourierCoeffOn hab (c • f) n = c • fourierCoeffOn hab f n
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma lift_fst {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) : lift f g ≫ fst _ _ = f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
T X Y : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g ≫ fst X Y = f

Tactic:
simp [lift, fst]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
lemma unitClosedBall_eq_univ_of_discrete : (Metric.closedBall 0 1 : Set 𝕜) = Set.univ

Proof state:
case h
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x✝ : 𝕜
⊢ x✝ ∈ Metric.closedBall 0 1 ↔ x✝ ∈ Set.univ

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
⊢ Metric.closedBall 0 1 = Set.univ

Tactic:
ext

Result:
case h
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x✝ : 𝕜
⊢ x✝ ∈ Metric.closedBall 0 1 ↔ x✝ ∈ Set.univ