harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
theorem restrictNonposSeq_subset (n : ℕ) : restrictNonposSeq s i n ⊆ i

Proof state:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ MeasureTheory.SignedMeasure.someExistsOneDivLT s
      (i \
        ⋃ k,
          ⋃ (H : k ≤ n✝),
            let_fun this := ⋯;
            MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ⊆
    i

Tactic:
exact someExistsOneDivLT_subset'

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i (n✝ + 1) ⊆ i

Tactic:
rw [restrictNonposSeq]

Result:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ MeasureTheory.SignedMeasure.someExistsOneDivLT s
      (i \
        ⋃ k,
          ⋃ (H : k ≤ n✝),
            let_fun this := ⋯;
            MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ⊆
    i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem or_comm (x y : Nat) : x ||| y = y ||| x

Proof state:
case pred
x y : Nat
⊢ ∀ (i : Nat), (x ||| y).testBit i = (y ||| x).testBit i

Tactic:
simp [Bool.or_comm]

Result:
no goals

Proof state:
x y : Nat
⊢ x ||| y = y ||| x

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x y : Nat
⊢ ∀ (i : Nat), (x ||| y).testBit i = (y ||| x).testBit i
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem append_right_nil (u : Fin m → α) (v : Fin n → α) (hv : n = 0) :
    append u v = u ∘ Fin.cast (by rw [hv, Nat.add_zero])

Proof state:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ append u v (castAdd n l) = (u ∘ Fin.cast ⋯) (castAdd n l)

Tactic:
rw [append_left, Function.comp_apply]

Result:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ u l = u (Fin.cast ⋯ (castAdd n l))

Proof state:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ ↑l = ↑(Fin.cast ⋯ (castAdd n l))

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
r : Fin n
⊢ append u v (natAdd m r) = (u ∘ Fin.cast ⋯) (natAdd m r)

Tactic:
exact (Fin.cast hv r).elim0

Result:
no goals

Proof state:
m n : ℕ
α✝ : Fin (n + 1) → Sort u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.succ
i : Fin n
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ m + n = m

Tactic:
rw [hv, Nat.add_zero]

Result:
no goals

Proof state:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ u l = u (Fin.cast ⋯ (castAdd n l))

Tactic:
refine congr_arg u (Fin.ext ?_)

Result:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ ↑l = ↑(Fin.cast ⋯ (castAdd n l))

Proof state:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ append u v = u ∘ Fin.cast ⋯

Tactic:
refine funext (Fin.addCases (fun l => ?_) fun r => ?_)

Result:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ append u v (castAdd n l) = (u ∘ Fin.cast ⋯) (castAdd n l)

case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
r : Fin n
⊢ append u v (natAdd m r) = (u ∘ Fin.cast ⋯) (natAdd m r)
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_image (h : Isometry Φ) :
    hausdorffEdist (Φ '' s) (Φ '' t) = hausdorffEdist s t

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s t : Set α
Φ : α → β
h : Isometry Φ
⊢ hausdorffEdist (Φ '' s) (Φ '' t) = hausdorffEdist s t

Tactic:
simp only [hausdorffEdist_def, iSup_image, infEdist_image h]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem nonsquare_of_jacobiSym_eq_neg_one {a : ℤ} {b : ℕ} (h : J(a | b) = -1) :
    ¬IsSquare (a : ZMod b) := fun ⟨r, ha⟩ => by
  rw [← r.coe_valMinAbs, ← Int.cast_mul, intCast_eq_intCast_iff', ← sq] at ha
  apply (by norm_num : ¬(0 : ℤ) ≤ -1)
  rw [← h, mod_left, ha, ← mod_left, pow_left]
  apply sq_nonneg

Proof state:
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = r.valMinAbs ^ 2 % ↑b
⊢ 0 ≤ J(r.valMinAbs | b) ^ 2

Tactic:
apply sq_nonneg

Result:
no goals

Proof state:
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = r.valMinAbs ^ 2 % ↑b
⊢ 0 ≤ -1

Tactic:
rw [← h, mod_left, ha, ← mod_left, pow_left]

Result:
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = r.valMinAbs ^ 2 % ↑b
⊢ 0 ≤ J(r.valMinAbs | b) ^ 2

Proof state:
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : ↑a = r * r
⊢ False

Tactic:
rw [← r.coe_valMinAbs, ← Int.cast_mul, intCast_eq_intCast_iff', ← sq] at ha

Result:
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = r.valMinAbs ^ 2 % ↑b
⊢ False

Proof state:
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = r.valMinAbs ^ 2 % ↑b
⊢ ¬0 ≤ -1

Tactic:
norm_num

Result:
no goals

Proof state:
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = r.valMinAbs ^ 2 % ↑b
⊢ False

Tactic:
apply (by norm_num : ¬(0 : ℤ) ≤ -1)

Result:
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = r.valMinAbs ^ 2 % ↑b
⊢ 0 ≤ -1
-- Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
theorem lineMap_strict_mono_endpoints (ha : a < a') (hb : b < b') (h₀ : 0 ≤ r) (h₁ : r ≤ 1) :
    lineMap a b r < lineMap a' b' r

Proof state:
case inr
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r : k
ha : a < a'
hb : b < b'
h₀✝ : 0 ≤ r
h₁ : r ≤ 1
h₀ : 0 < r
⊢ (lineMap a b) r < (lineMap a' b') r

Tactic:
exact (lineMap_mono_left ha.le h₁).trans_lt (lineMap_strict_mono_right hb h₀)

Result:
no goals

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r : k
ha : a < a'
hb : b < b'
h₀ : 0 ≤ r
h₁ : r ≤ 1
⊢ (lineMap a b) r < (lineMap a' b') r

Tactic:
rcases h₀.eq_or_lt with (rfl | h₀)

Result:
case inl
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
ha : a < a'
hb : b < b'
h₀ : 0 ≤ 0
h₁ : 0 ≤ 1
⊢ (lineMap a b) 0 < (lineMap a' b') 0

case inr
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r : k
ha : a < a'
hb : b < b'
h₀✝ : 0 ≤ r
h₁ : r ≤ 1
h₀ : 0 < r
⊢ (lineMap a b) r < (lineMap a' b') r

Proof state:
case inl
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
ha : a < a'
hb : b < b'
h₀ : 0 ≤ 0
h₁ : 0 ≤ 1
⊢ (lineMap a b) 0 < (lineMap a' b') 0

Tactic:
simpa

Result:
no goals
-- Mathlib/Analysis/Quaternion.lean
theorem continuous_im : Continuous fun q : ℍ => q.im

Proof state:
⊢ Continuous fun q => q.im

Tactic:
simpa only [← sub_self_re] using continuous_id.sub (continuous_coe.comp continuous_re)

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem isMultiplicative_sigma {k : ℕ} : IsMultiplicative (σ k)

Proof state:
k : ℕ
⊢ (ζ * pow k).IsMultiplicative

Tactic:
apply isMultiplicative_zeta.mul isMultiplicative_pow

Result:
no goals

Proof state:
k : ℕ
⊢ (σ k).IsMultiplicative

Tactic:
rw [← zeta_mul_pow_eq_sigma]

Result:
k : ℕ
⊢ (ζ * pow k).IsMultiplicative
-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem norm_torusIntegral_le_of_norm_le_const {C : ℝ} (hf : ∀ θ, ‖f (torusMap c R θ)‖ ≤ C) :
    ‖∯ x in T(c, R), f x‖ ≤ ((2 * π) ^ (n : ℕ) * ∏ i, |R i|) * C :=
  calc
    ‖∯ x in T(c, R), f x‖ ≤ (∏ i, |R i|) * C * (volume (Icc (0 : ℝⁿ) fun _ => 2 * π)).toReal :=
      norm_setIntegral_le_of_norm_le_const' measure_Icc_lt_top measurableSet_Icc fun θ _ =>
        calc
          ‖(∏ i : Fin n, R i * exp (θ i * I) * I : ℂ) • f (torusMap c R θ)‖ =
              (∏ i : Fin n, |R i|) * ‖f (torusMap c R θ)‖

Proof state:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
C : ℝ
hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C
θ : Fin n → ℝ
x✝ : θ ∈ Icc 0 fun x => 2 * π
⊢ 0 ≤ ∏ i : Fin n, |R i|

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
C : ℝ
hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C
θ : Fin n → ℝ
x✝ : θ ∈ Icc 0 fun x => 2 * π
⊢ ‖(∏ i : Fin n, ↑(R i) * cexp (↑(θ i) * I) * I) • f (torusMap c R θ)‖ = (∏ i : Fin n, |R i|) * ‖f (torusMap c R θ)‖

Tactic:
simp [norm_smul]

Result:
no goals

Proof state:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
C : ℝ
hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C
⊢ (∏ i : Fin n, |R i|) * C * (volume (Icc 0 fun x => 2 * π)).toReal = ((2 * π) ^ n * ∏ i : Fin n, |R i|) * C

Tactic:
simp only [Pi.zero_def, Real.volume_Icc_pi_toReal fun _ => Real.two_pi_pos.le, sub_zero,
  Fin.prod_const, mul_assoc, mul_comm ((2 * π) ^ (n : ℕ))]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem coe_neg : ((-x : R) : ℍ[R,c₁,c₂,c₃]) = -x

Proof state:
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : AddGroup R
⊢ ↑(-x) = -↑x

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem _root_.MeasurableEmbedding.integrableAtFilter_iff_comap [MeasurableSpace β] {e : α → β}
    (he : MeasurableEmbedding e) {f : β → E} {μ : Measure β} :
    IntegrableAtFilter f (l.map e) μ ↔ IntegrableAtFilter (f ∘ e) l (μ.comap e)

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
μ : Measure β
s : Set β
hs : s ∈ map e l
int : IntegrableOn f s (μ.restrict (range e))
⊢ ∃ s ∈ map e l, IntegrableOn f s μ

Tactic:
exact ⟨_, inter_mem hs range_mem_map, int.inter_of_restrict⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
μ : Measure β
⊢ (∃ s ∈ map e l, IntegrableOn f s μ) ↔ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))

Tactic:
constructor <;> rintro ⟨s, hs, int⟩

Result:
case mp.intro.intro
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
μ : Measure β
s : Set β
hs : s ∈ map e l
int : IntegrableOn f s μ
⊢ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))

case mpr.intro.intro
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
μ : Measure β
s : Set β
hs : s ∈ map e l
int : IntegrableOn f s (μ.restrict (range e))
⊢ ∃ s ∈ map e l, IntegrableOn f s μ

Proof state:
case mp.intro.intro
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
μ : Measure β
s : Set β
hs : s ∈ map e l
int : IntegrableOn f s μ
⊢ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))

Tactic:
exact ⟨s, hs, int.mono_measure <| μ.restrict_le_self⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
μ : Measure β
⊢ IntegrableAtFilter f (map e l) μ ↔ IntegrableAtFilter (f ∘ e) l (Measure.comap e μ)

Tactic:
simp_rw [← he.integrableAtFilter_map_iff, IntegrableAtFilter, he.map_comap]

Result:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
μ : Measure β
⊢ (∃ s ∈ map e l, IntegrableOn f s μ) ↔ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))
-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuousAt_sum {f : ι → α → γ} {a : Finset ι}
    (ha : ∀ i ∈ a, LowerSemicontinuousAt (f i) x) :
    LowerSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
x : α
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x

Tactic:
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *

Result:
α : Type u_1
inst✝⁴ : TopologicalSpace α
x : α
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) univ x

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
x : α
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) univ x

Tactic:
exact lowerSemicontinuousWithinAt_sum ha

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean
theorem transcendental_adjoin_iff [Nontrivial A] {s : Set ι} {i : ι} :
    Transcendental (adjoin R (x '' s)) (x i) ↔ i ∉ s

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s : Set ι
i : ι
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ Disjoint s {i}

Tactic:
convert ← hx.adjoin_iff_disjoint (t := {i})

Result:
case h.e'_1.a
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s : Set ι
i : ι
⊢ (AlgebraicIndependent ↥(adjoin R (x '' s)) fun i_1 => x ↑i_1) ↔ Transcendental (↥(adjoin R (x '' s))) (x i)

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s : Set ι
i : ι
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ i ∉ s

Tactic:
rw [← Set.disjoint_singleton_right]

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s : Set ι
i : ι
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ Disjoint s {i}

Proof state:
case h.e'_1.a
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s : Set ι
i : ι
⊢ (AlgebraicIndependent ↥(adjoin R (x '' s)) fun i_1 => x ↑i_1) ↔ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
rw [algebraicIndependent_singleton_iff ⟨i, rfl⟩]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffAt.congr_of_eventuallyEq (h : ContDiffAt 𝕜 n f x) (hg : f₁ =ᶠ[𝓝 x] f) :
    ContDiffAt 𝕜 n f₁ x :=
  h.congr_of_eventuallyEq_of_mem (by rwa [nhdsWithin_univ]) (mem_univ x)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : E → F
x : E
n : WithTop ℕ∞
h : ContDiffAt 𝕜 n f x
hg : f₁ =ᶠ[𝓝 x] f
⊢ f₁ =ᶠ[𝓝[univ] x] f

Tactic:
rwa [nhdsWithin_univ]

Result:
no goals
-- Mathlib/Probability/Process/HittingTime.lean
theorem le_hitting_of_exists {m : ι} (h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s) :
    n ≤ hitting u s n m ω

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ hitting u s n m ω

Tactic:
refine le_hitting ?_ ω

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ m

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h_exists : ∃ j ∈ ∅, u j ω ∈ s
h : ¬n ≤ m
⊢ False

Tactic:
simp at h_exists

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h : ¬n ≤ m
⊢ False

Tactic:
rw [Set.Icc_eq_empty_of_lt (not_le.mp h)] at h_exists

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h_exists : ∃ j ∈ ∅, u j ω ∈ s
h : ¬n ≤ m
⊢ False

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ m

Tactic:
by_contra h

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h : ¬n ≤ m
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem Const.toListModel_getThenInsertIfNew? {β : Type v} [BEq α] [Hashable α] [EquivBEq α]
    [LawfulHashable α] {m : Raw₀ α (fun _ => β)} {a : α} {b : β} (h : Raw.WFImp m.1) :
    Perm (toListModel (Const.getThenInsertIfNew? m a b).2.1.buckets)
      (insertEntryIfNew a b (toListModel m.1.buckets))

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
a : α
b : β
h : Raw.WFImp m.val
⊢ toListModel (m.insertIfNewₘ a b).val.buckets ~ insertEntryIfNew a b (toListModel m.val.buckets)

Tactic:
exact toListModel_insertIfNewₘ h

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
a : α
b : β
h : Raw.WFImp m.val
⊢ toListModel (getThenInsertIfNew? m a b).snd.val.buckets ~ insertEntryIfNew a b (toListModel m.val.buckets)

Tactic:
rw [getThenInsertIfNew?_eq_insertIfNewₘ]

Result:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
a : α
b : β
h : Raw.WFImp m.val
⊢ toListModel (m.insertIfNewₘ a b).val.buckets ~ insertEntryIfNew a b (toListModel m.val.buckets)
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
@[ext]
lemma hom_ext {X Y : SimplicialObject C} (f g : X ⟶ Y)
    (h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n) : f = g :=
  NatTrans.ext (by ext; apply h)

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n
x✝ : SimplexCategoryᵒᵖ
⊢ f.app x✝ = g.app x✝

Tactic:
apply h

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n
⊢ f.app = g.app

Tactic:
ext

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n
x✝ : SimplexCategoryᵒᵖ
⊢ f.app x✝ = g.app x✝
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_le_rpow_left_iff (hx : 1 < x) : x ^ y ≤ x ^ z ↔ y ≤ z

Proof state:
x y z : ℝ
hx : 1 < x
⊢ x ^ y ≤ x ^ z ↔ y ≤ z

Tactic:
have x_pos : 0 < x := lt_trans zero_lt_one hx

Result:
x y z : ℝ
hx : 1 < x
x_pos : 0 < x
⊢ x ^ y ≤ x ^ z ↔ y ≤ z

Proof state:
x y z : ℝ
hx : 1 < x
x_pos : 0 < x
⊢ x ^ y ≤ x ^ z ↔ y ≤ z

Tactic:
rw [← log_le_log_iff (rpow_pos_of_pos x_pos y) (rpow_pos_of_pos x_pos z), log_rpow x_pos,
  log_rpow x_pos, mul_le_mul_right (log_pos hx)]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem mul_right_surjective₀ {a : G₀} (h : a ≠ 0) : Surjective fun g => g * a := fun g =>
  ⟨g * a⁻¹, by simp [mul_assoc, inv_mul_cancel₀ h]⟩

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
g : G₀
⊢ (fun g => g * a) (g * a⁻¹) = g

Tactic:
simp [mul_assoc, inv_mul_cancel₀ h]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
lemma strictMono_semilength : StrictMono semilength := fun p q pq ↦ by
  obtain ⟨plq, pnq⟩ := lt_iff_le_and_ne.mp pq
  apply lt_of_le_of_ne (monotone_semilength plq)
  contrapose! pnq
  replace pnq := congr(2 * $(pnq))
  simp_rw [two_mul_semilength_eq_length] at pnq
  exact DyckWord.ext ((infix_of_le plq).eq_of_length pnq)

Proof state:
case intro
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : 2 * p.semilength = 2 * q.semilength
⊢ p = q

Tactic:
simp_rw [two_mul_semilength_eq_length] at pnq

Result:
case intro
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : (↑p).length = (↑q).length
⊢ p = q

Proof state:
case intro
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : (↑p).length = (↑q).length
⊢ p = q

Tactic:
exact DyckWord.ext ((infix_of_le plq).eq_of_length pnq)

Result:
no goals

Proof state:
case intro
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p.semilength = q.semilength
⊢ p = q

Tactic:
replace pnq := congr(2 * $(pnq))

Result:
case intro
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : 2 * p.semilength = 2 * q.semilength
⊢ p = q

Proof state:
case intro
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p ≠ q
⊢ p.semilength < q.semilength

Tactic:
apply lt_of_le_of_ne (monotone_semilength plq)

Result:
case intro
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p ≠ q
⊢ p.semilength ≠ q.semilength

Proof state:
case intro
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p ≠ q
⊢ p.semilength ≠ q.semilength

Tactic:
contrapose! pnq

Result:
case intro
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p.semilength = q.semilength
⊢ p = q

Proof state:
p q : DyckWord
pq : p < q
⊢ p.semilength < q.semilength

Tactic:
obtain ⟨plq, pnq⟩ := lt_iff_le_and_ne.mp pq

Result:
case intro
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p ≠ q
⊢ p.semilength < q.semilength
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.le_offset (a k : Nat) : k ≤ a + k

Proof state:
a k : Nat
⊢ k ≤ a + k

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma subset_closure_of_subset' (M : Matroid α) (hXY : X ⊆ Y) (hX : X ⊆ M.E

Proof state:
α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : autoParam (X ⊆ M.E) _auto✝
⊢ X ⊆ M.closure (Y ∩ M.E)

Tactic:
exact M.subset_closure_of_subset (subset_inter hXY hX)

Result:
no goals

Proof state:
α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : autoParam (X ⊆ M.E) _auto✝
⊢ X ⊆ M.closure Y

Tactic:
rw [← closure_inter_ground]

Result:
α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : autoParam (X ⊆ M.E) _auto✝
⊢ X ⊆ M.closure (Y ∩ M.E)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF)
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) :
    get! (insertMany m l).1 k' = v

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
⊢ get! (insertMany m l).val k' = v

Tactic:
simp_to_model [Const.insertMany] using List.getValue!_insertListConst_of_mem

Result:
no goals