harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Prod.lean
/-- If `s ×ˢ t` is a null measurable set and `μ s ≠ 0`, then `t` is a null measurable set. -/
lemma _root_.MeasureTheory.NullMeasurableSet.right_of_prod {s : Set α} {t : Set β}
    (h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)) (hs : μ s ≠ 0) : NullMeasurableSet t ν

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
hs : μ s ≠ 0
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u
⊢ NullMeasurableSet t ν

Tactic:
obtain ⟨x, hxs, hx⟩ : ∃ x ∈ s, (Prod.mk x ⁻¹' (s ×ˢ t)) =ᵐ[ν] (Prod.mk x ⁻¹' u) :=
  ((frequently_ae_iff.2 hs).and_eventually (ae_ae_eq_curry_of_prod hu)).exists

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
hs : μ s ≠ 0
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u
x : α
hxs : x ∈ s
hx : Prod.mk x ⁻¹' s ×ˢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u
⊢ NullMeasurableSet t ν

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
hs : μ s ≠ 0
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u
x : α
hxs : x ∈ s
hx : Prod.mk x ⁻¹' s ×ˢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u
⊢ NullMeasurableSet t ν

Tactic:
refine ⟨Prod.mk x ⁻¹' u, measurable_prod_mk_left hum, ?_⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
hs : μ s ≠ 0
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u
x : α
hxs : x ∈ s
hx : Prod.mk x ⁻¹' s ×ˢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u
⊢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
hs : μ s ≠ 0
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u
x : α
hxs : x ∈ s
hx : Prod.mk x ⁻¹' s ×ˢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u
⊢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u

Tactic:
rwa [mk_preimage_prod_right hxs] at hx

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
hs : μ s ≠ 0
⊢ NullMeasurableSet t ν

Tactic:
rcases h with ⟨u, hum, hu⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
hs : μ s ≠ 0
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u
⊢ NullMeasurableSet t ν
-- Mathlib/Data/Real/Cardinality.lean
theorem mk_real : #ℝ = 𝔠

Proof state:
case a

⊢ #(CauSeq ℚ abs) ≤ 𝔠

Tactic:
apply (mk_subtype_le _).trans_eq

Result:
case a

⊢ #(ℕ → ℚ) = 𝔠

Proof state:
⊢ #ℝ = 𝔠

Tactic:
apply le_antisymm

Result:
case a

⊢ #ℝ ≤ 𝔠

case a

⊢ 𝔠 ≤ #ℝ

Proof state:
case a

⊢ #(ℕ → ℚ) = 𝔠

Tactic:
rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]

Result:
no goals

Proof state:
case a.convert_3

⊢ 1 / 3 < 1 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
case a

⊢ #(CauSeq.Completion.Cauchy abs) ≤ 𝔠

Tactic:
apply mk_quotient_le.trans

Result:
case a

⊢ #(CauSeq ℚ abs) ≤ 𝔠

Proof state:
case a

⊢ 𝔠 ≤ #ℝ

Tactic:
convert mk_le_of_injective (cantorFunction_injective _ _)

Result:
case h.e'_3

⊢ 𝔠 = #(ℕ → Bool)

case a.convert_1

⊢ ℝ

case a.convert_2

⊢ 0 < ?a.convert_1✝

case a.convert_3

⊢ ?a.convert_1✝ < 1 / 2

Proof state:
case a.convert_2

⊢ 0 < 1 / 3

Tactic:
norm_num

Result:
no goals

Proof state:
case a

⊢ #ℝ ≤ 𝔠

Tactic:
rw [Real.equivCauchy.cardinal_eq]

Result:
case a

⊢ #(CauSeq.Completion.Cauchy abs) ≤ 𝔠

Proof state:
case a.convert_1

⊢ ℝ

Tactic:
exact 1 / 3

Result:
no goals

Proof state:
case h.e'_3

⊢ 𝔠 = #(ℕ → Bool)

Tactic:
rw [← power_def, mk_bool, mk_nat, two_power_aleph0]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean
theorem measure_compl_aeSeqSet_eq_zero [Countable ι] (hf : ∀ i, AEMeasurable (f i) μ)
    (hp : ∀ᵐ x ∂μ, p x fun n => f n x) : μ (aeSeqSet hf p)ᶜ = 0

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
hf_eq : ∀ (i : ι), f i =ᶠ[ae μ] AEMeasurable.mk (f i) ⋯
⊢ μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}ᶜ = 0

Tactic:
simp_rw [Filter.EventuallyEq, ← ae_all_iff] at hf_eq

Result:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
hf_eq : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), f i a = AEMeasurable.mk (f i) ⋯ a
⊢ μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}ᶜ = 0

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
hf_eq : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), f i a = AEMeasurable.mk (f i) ⋯ a
⊢ μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}ᶜ = 0

Tactic:
exact Filter.Eventually.and hf_eq hp

Result:
no goals

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}ᶜ = 0

Tactic:
have hf_eq := fun i => (hf i).ae_eq_mk

Result:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
hf_eq : ∀ (i : ι), f i =ᶠ[ae μ] AEMeasurable.mk (f i) ⋯
⊢ μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}ᶜ = 0

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ μ (aeSeqSet hf p)ᶜ = 0

Tactic:
rw [aeSeqSet, compl_compl, measure_toMeasurable]

Result:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}ᶜ = 0
-- Mathlib/LinearAlgebra/Determinant.lean
theorem LinearMap.associated_det_of_eq_comp (e : M ≃ₗ[R] M) (f f' : M →ₗ[R] M)
    (h : ∀ x, f x = f' (e x)) : Associated (LinearMap.det f) (LinearMap.det f')

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
⊢ Associated (LinearMap.det f) (LinearMap.det f')

Tactic:
suffices Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f') by
  convert this using 2
  ext x
  exact h x

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
⊢ Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f')

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
⊢ Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f')

Tactic:
rw [← mul_one (LinearMap.det f'), LinearMap.det_comp]

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
⊢ Associated (LinearMap.det f' * LinearMap.det ↑e) (LinearMap.det f' * 1)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
⊢ Associated (LinearMap.det f' * LinearMap.det ↑e) (LinearMap.det f' * 1)

Tactic:
exact Associated.mul_left _ (associated_one_iff_isUnit.mpr e.isUnit_det')

Result:
no goals

Proof state:
case h.e'_3.h.e'_6.h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
this : Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f')
x : M
⊢ f x = (f' ∘ₗ ↑e) x

Tactic:
exact h x

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
this : Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f')
⊢ Associated (LinearMap.det f) (LinearMap.det f')

Tactic:
convert this using 2

Result:
case h.e'_3.h.e'_6
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
this : Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f')
⊢ f = f' ∘ₗ ↑e

Proof state:
case h.e'_3.h.e'_6
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
this : Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f')
⊢ f = f' ∘ₗ ↑e

Tactic:
ext x

Result:
case h.e'_3.h.e'_6.h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
this : Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f')
x : M
⊢ f x = (f' ∘ₗ ↑e) x
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge'
    [CompleteSpace E] [IsMeasurablyGenerated l']
    [TendstoIxxClass Ioc l l'] (hfm : StronglyMeasurableAtFilter f l' μ)
    (hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)) (hl : μ.FiniteAtFilter l') (hu : Tendsto u lt l)
    (hv : Tendsto v lt l) (huv : v ≤ᶠ[lt] u) :
    (fun t => (∫ x in u t..v t, f x ∂μ) + (μ (Ioc (v t) (u t))).toReal • c) =o[lt] fun t =>
      (μ <| Ioc (v t) (u t)).toReal :=
  (measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le' hfm hf hl hv hu
          huv).neg_left.congr_left
    fun t => by simp [integral_symm (u t), add_comm]

Proof state:
ι : Type u_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝² : CompleteSpace E
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
huv : v ≤ᶠ[lt] u
t : ι
⊢ -(∫ (x : ℝ) in v t..u t, f x ∂μ - (μ (Ioc (v t) (u t))).toReal • c) =
    ∫ (x : ℝ) in u t..v t, f x ∂μ + (μ (Ioc (v t) (u t))).toReal • c

Tactic:
simp [integral_symm (u t), add_comm]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
lemma append_right_injective (h : x ++ₛ a = x ++ₛ b) : a = b

Proof state:
case a
α : Type u
x : List α
a b : Stream' α
h : x ++ₛ a = x ++ₛ b
n : ℕ
⊢ a.get n = b.get n

Tactic:
replace h := congr_arg (fun a ↦ a.get (x.length + n)) h

Result:
case a
α : Type u
x : List α
a b : Stream' α
n : ℕ
h : (fun a => a.get (x.length + n)) (x ++ₛ a) = (fun a => a.get (x.length + n)) (x ++ₛ b)
⊢ a.get n = b.get n

Proof state:
case a
α : Type u
x : List α
a b : Stream' α
n : ℕ
h : (fun a => a.get (x.length + n)) (x ++ₛ a) = (fun a => a.get (x.length + n)) (x ++ₛ b)
⊢ a.get n = b.get n

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u
x : List α
a b : Stream' α
h : x ++ₛ a = x ++ₛ b
⊢ a = b

Tactic:
ext n

Result:
case a
α : Type u
x : List α
a b : Stream' α
h : x ++ₛ a = x ++ₛ b
n : ℕ
⊢ a.get n = b.get n
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
theorem iteratedDerivWithin_congr (hfg : Set.EqOn f g s) :
    Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n g s) s

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
n : ℕ
IH : ∀ {f g : 𝕜 → F}, Set.EqOn f g s → Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n g s) s
f g : 𝕜 → F
hfg : Set.EqOn f g s
⊢ Set.EqOn (iteratedDerivWithin (n + 1) f s) (iteratedDerivWithin (n + 1) g s) s

Tactic:
intro y hy

Result:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
n : ℕ
IH : ∀ {f g : 𝕜 → F}, Set.EqOn f g s → Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n g s) s
f g : 𝕜 → F
hfg : Set.EqOn f g s
y : 𝕜
hy : y ∈ s
⊢ iteratedDerivWithin (n + 1) f s y = iteratedDerivWithin (n + 1) g s y

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
n : ℕ
IH : ∀ {f g : 𝕜 → F}, Set.EqOn f g s → Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n g s) s
f g : 𝕜 → F
hfg : Set.EqOn f g s
y : 𝕜
hy : y ∈ s
⊢ derivWithin (iteratedDerivWithin n f s) s y = derivWithin (iteratedDerivWithin n g s) s y

Tactic:
exact derivWithin_congr (IH hfg) (IH hfg hy)

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
n : ℕ
IH : ∀ {f g : 𝕜 → F}, Set.EqOn f g s → Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n g s) s
f g : 𝕜 → F
hfg : Set.EqOn f g s
y : 𝕜
hy : y ∈ s
⊢ iteratedDerivWithin (n + 1) f s y = iteratedDerivWithin (n + 1) g s y

Tactic:
rw [iteratedDerivWithin_succ, iteratedDerivWithin_succ]

Result:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
n : ℕ
IH : ∀ {f g : 𝕜 → F}, Set.EqOn f g s → Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n g s) s
f g : 𝕜 → F
hfg : Set.EqOn f g s
y : 𝕜
hy : y ∈ s
⊢ derivWithin (iteratedDerivWithin n f s) s y = derivWithin (iteratedDerivWithin n g s) s y

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
s : Set 𝕜
f g : 𝕜 → F
hfg : Set.EqOn f g s
⊢ Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n g s) s

Tactic:
induction n generalizing f g with
| zero => rwa [iteratedDerivWithin_zero]
| succ n IH =>
  intro y hy
  rw [iteratedDerivWithin_succ, iteratedDerivWithin_succ]
  exact derivWithin_congr (IH hfg) (IH hfg hy)

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : Set.EqOn f g s
⊢ Set.EqOn (iteratedDerivWithin 0 f s) (iteratedDerivWithin 0 g s) s

Tactic:
rwa [iteratedDerivWithin_zero]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
theorem Gamma_one_top : Gamma 1 = ⊤

Proof state:
⊢ Γ(1) = ⊤

Tactic:
ext

Result:
case h
x✝ : SL(2, ℤ)
⊢ x✝ ∈ Γ(1) ↔ x✝ ∈ ⊤

Proof state:
case h
x✝ : SL(2, ℤ)
⊢ x✝ ∈ Γ(1) ↔ x✝ ∈ ⊤

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem count_edges_takeUntil_le_one {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) (x : V) :
    (p.takeUntil u h).edges.count s(u, x) ≤ 1

Proof state:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ : V
h : u ∈ nil.support
⊢ List.count s(u, x) (nil.takeUntil u h).edges ≤ 1

Tactic:
rw [mem_support_nil_iff] at h

Result:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ : V
h✝ : u ∈ nil.support
h : u = u✝
⊢ List.count s(u, x) (nil.takeUntil u h✝).edges ≤ 1

Proof state:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ : V
h✝ : u ∈ nil.support
h : u = u✝
⊢ List.count s(u, x) (nil.takeUntil u h✝).edges ≤ 1

Tactic:
subst u

Result:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w x u✝ : V
h : u✝ ∈ nil.support
⊢ List.count s(u✝, x) (nil.takeUntil u✝ h).edges ≤ 1

Proof state:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : ¬u✝ = u
h'' : ¬(s(u✝, v✝) == s(u, x)) = true
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 0 ≤ 1

Tactic:
apply ih

Result:
no goals

Proof state:
case cons.head
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x v✝ w✝ : V
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
ha : G.Adj u v✝
⊢ List.count s(u, x) ((cons ha p').takeUntil u ⋯).edges ≤ 1

Tactic:
simp!

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_smul_add_right_eq_zero_or_eq_pi_iff {x y : V} (r : ℝ) :
    o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = π ↔
    o.oangle x y = 0 ∨ o.oangle x y = π

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
⊢ (∃ g, g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)) ↔
    ∃ g, g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ∃ g, g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
⊢ ∃ g, g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)

case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ∃ g, g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
⊢ ∃ g, g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
-- Mathlib/LinearAlgebra/Projection.lean
theorem ker_id_sub_eq_of_proj {f : E →ₗ[R] p} (hf : ∀ x : p, f x = x) :
    ker (id - p.subtype.comp f) = p

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
hx : x ∈ p
⊢ x = ↑(f x)

Tactic:
rw [hf ⟨x, hx⟩, Subtype.coe_mk]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ ker (id - p.subtype ∘ₗ f) = p

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
⊢ x ∈ ker (id - p.subtype ∘ₗ f) ↔ x ∈ p

Proof state:
case h
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
⊢ x ∈ ker (id - p.subtype ∘ₗ f) ↔ x ∈ p

Tactic:
simp only [comp_apply, mem_ker, subtype_apply, sub_apply, id_apply, sub_eq_zero]

Result:
case h
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
⊢ x = ↑(f x) ↔ x ∈ p

Proof state:
case h
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
⊢ x = ↑(f x) ↔ x ∈ p

Tactic:
exact ⟨fun h => h.symm ▸ Submodule.coe_mem _, fun hx => by rw [hf ⟨x, hx⟩, Subtype.coe_mk]⟩

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem cosh_half_dist (z w : ℍ) :
    cosh (dist z w / 2) = dist (z : ℂ) (conj (w : ℂ)) / (2 * √(z.im * w.im))

Proof state:
z w : ℍ
⊢ cosh (dist z w / 2) = dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))

Tactic:
rw [← sq_eq_sq₀, cosh_sq', sinh_half_dist, div_pow, div_pow, one_add_div, mul_pow, sq_sqrt]

Result:
z w : ℍ
⊢ (2 ^ 2 * (z.im * w.im) + dist ↑z ↑w ^ 2) / (2 ^ 2 * (z.im * w.im)) =
    dist (↑z) ((starRingEnd ℂ) ↑w) ^ 2 / (2 ^ 2 * (z.im * w.im))

z w : ℍ
⊢ 0 ≤ z.im * w.im

z w : ℍ
⊢ (2 * √(z.im * w.im)) ^ 2 ≠ 0

case ha
z w : ℍ
⊢ 0 ≤ cosh (dist z w / 2)

case hb
z w : ℍ
⊢ 0 ≤ dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))

Proof state:
z w : ℍ
⊢ (2 ^ 2 * (z.im * w.im) + dist ↑z ↑w ^ 2) / (2 ^ 2 * (z.im * w.im)) =
    dist (↑z) ((starRingEnd ℂ) ↑w) ^ 2 / (2 ^ 2 * (z.im * w.im))

Tactic:
congr 1

Result:
case e_a
z w : ℍ
⊢ 2 ^ 2 * (z.im * w.im) + dist ↑z ↑w ^ 2 = dist (↑z) ((starRingEnd ℂ) ↑w) ^ 2

Proof state:
z w : ℍ
⊢ 0 ≤ z.im * w.im

z w : ℍ
⊢ (2 * √(z.im * w.im)) ^ 2 ≠ 0

case ha
z w : ℍ
⊢ 0 ≤ cosh (dist z w / 2)

case hb
z w : ℍ
⊢ 0 ≤ dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))

Tactic:
all_goals positivity

Result:
no goals

Proof state:
case hb
z w : ℍ
⊢ 0 ≤ dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))

Tactic:
positivity

Result:
no goals

Proof state:
case e_a
z w : ℍ
⊢ 2 ^ 2 * (z.im * w.im) + dist ↑z ↑w ^ 2 = dist (↑z) ((starRingEnd ℂ) ↑w) ^ 2

Tactic:
simp only [Complex.dist_eq, Complex.sq_norm, Complex.normSq_sub, Complex.normSq_conj,
  Complex.conj_conj, Complex.mul_re, Complex.conj_re, Complex.conj_im, coe_im]

Result:
case e_a
z w : ℍ
⊢ 2 ^ 2 * (z.im * w.im) + (Complex.normSq ↑z + Complex.normSq ↑w - 2 * ((↑z).re * (↑w).re - z.im * -w.im)) =
    Complex.normSq ↑z + Complex.normSq ↑w - 2 * ((↑z).re * (↑w).re - z.im * w.im)

Proof state:
case e_a
z w : ℍ
⊢ 2 ^ 2 * (z.im * w.im) + (Complex.normSq ↑z + Complex.normSq ↑w - 2 * ((↑z).re * (↑w).re - z.im * -w.im)) =
    Complex.normSq ↑z + Complex.normSq ↑w - 2 * ((↑z).re * (↑w).re - z.im * w.im)

Tactic:
ring

Result:
no goals
-- Mathlib/Data/Int/LeastGreatest.lean
theorem coe_leastOfBdd_eq {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ} (Hb : ∀ z : ℤ, P z → b ≤ z)
    (Hb' : ∀ z : ℤ, P z → b' ≤ z) (Hinh : ∃ z : ℤ, P z) :
    (leastOfBdd b Hb Hinh : ℤ) = leastOfBdd b' Hb' Hinh

Proof state:
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ z, P z
⊢ ↑(b.leastOfBdd Hb Hinh) = ↑(b'.leastOfBdd Hb' Hinh)

Tactic:
rcases leastOfBdd b Hb Hinh with ⟨n, hn, h2n⟩

Result:
case mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → n ≤ z
⊢ ↑⟨n, ⋯⟩ = ↑(b'.leastOfBdd Hb' Hinh)

Proof state:
case mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → n ≤ z
⊢ ↑⟨n, ⋯⟩ = ↑(b'.leastOfBdd Hb' Hinh)

Tactic:
rcases leastOfBdd b' Hb' Hinh with ⟨n', hn', h2n'⟩

Result:
case mk.intro.mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → n ≤ z
n' : ℤ
hn' : P n'
h2n' : ∀ (z : ℤ), P z → n' ≤ z
⊢ ↑⟨n, ⋯⟩ = ↑⟨n', ⋯⟩

Proof state:
case mk.intro.mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → n ≤ z
n' : ℤ
hn' : P n'
h2n' : ∀ (z : ℤ), P z → n' ≤ z
⊢ ↑⟨n, ⋯⟩ = ↑⟨n', ⋯⟩

Tactic:
exact le_antisymm (h2n _ hn') (h2n' _ hn)

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem insert_inter_distrib (s t : Finset α) (a : α) :
    insert a (s ∩ t) = insert a s ∩ insert a t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ insert a (s ∩ t) = insert a s ∩ insert a t

Tactic:
simp_rw [insert_eq, union_inter_distrib_left]

Result:
no goals