harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem gcd_val (a b : R) : gcd a b = gcd (b % a) a

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ gcd a b = gcd (b % a) a

Tactic:
rw [gcd]

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ (if a0 : a = 0 then b
    else
      let_fun x := ⋯;
      gcd (b % a) a) =
    gcd (b % a) a

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ (if a0 : a = 0 then b
    else
      let_fun x := ⋯;
      gcd (b % a) a) =
    gcd (b % a) a

Tactic:
split_ifs with h <;> [simp only [h, mod_zero, gcd_zero_right]; rfl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem exists_mem_cons {p : α → Prop} {a : α} {l : List α} :
    (∃ x, ∃ _ : x ∈ a :: l, p x) ↔ p a ∨ ∃ x, ∃ _ : x ∈ l, p x

Proof state:
α : Type u_1
p : α → Prop
a : α
l : List α
⊢ (∃ x x_1, p x) ↔ p a ∨ ∃ x x_1, p x

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_le_pi_div_four {x} : arccos x ≤ π / 4 ↔ √2 / 2 ≤ x

Proof state:
case mpr
x : ℝ
a✝ : π / 4 ≤ arcsin x
⊢ π / 2 - arcsin x ≤ π / 4

Tactic:
linarith

Result:
no goals

Proof state:
case mpr
x : ℝ
⊢ π / 4 ≤ arcsin x → π / 2 - arcsin x ≤ π / 4

Tactic:
intro

Result:
case mpr
x : ℝ
a✝ : π / 4 ≤ arcsin x
⊢ π / 2 - arcsin x ≤ π / 4

Proof state:
x : ℝ
⊢ arccos x ≤ π / 4 ↔ √2 / 2 ≤ x

Tactic:
rw [arccos, ← pi_div_four_le_arcsin]

Result:
x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 ↔ π / 4 ≤ arcsin x
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem map_C (f : R →+* R') (n : ℤ) : map f (C R n) = C R' n

Proof state:
case one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (C R 1) = C R' 1

Tactic:
simp

Result:
no goals

Proof state:
case zero
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
⊢ map f (C R 0) = C R' 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℤ
⊢ map f (C R n) = C R' n

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1 ih2 =>
  simp_rw [C_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]
| neg_add_one n ih1 ih2 =>
  simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (C R (-↑n)) = C R' (-↑n)
ih2 : map f (C R (-↑n + 1)) = C R' (-↑n + 1)
⊢ map f (C R (-↑n - 1)) = C R' (-↑n - 1)

Tactic:
simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

Result:
no goals

Proof state:
case add_two
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (C R (↑n + 1)) = C R' (↑n + 1)
ih2 : map f (C R ↑n) = C R' ↑n
⊢ map f (C R (↑n + 2)) = C R' (↑n + 2)

Tactic:
simp_rw [C_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mfderiv_prod_left {x₀ : M} {y₀ : M'} :
    mfderiv I (I.prod I') (fun x => (x, y₀)) x₀ =
      ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)

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'
x₀ : M
y₀ : M'
⊢ mfderiv I (I.prod I') (fun x => (x, y₀)) x₀ = ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)

Tactic:
refine (mdifferentiableAt_id.mfderiv_prod mdifferentiableAt_const).trans ?_

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'
x₀ : M
y₀ : M'
⊢ (mfderiv I I id x₀).prod (mfderiv I I' (fun x => y₀) x₀) =
    ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)

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'
x₀ : M
y₀ : M'
⊢ (mfderiv I I id x₀).prod (mfderiv I I' (fun x => y₀) x₀) =
    ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)

Tactic:
rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inl]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem zpowers_eq {k : ℕ} [NeZero k] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) :
    Subgroup.zpowers ζ = rootsOfUnity k R

Proof state:
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
⊢ Subgroup.zpowers ζ = rootsOfUnity k R

Tactic:
apply SetLike.coe_injective

Result:
case a
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
⊢ ↑(Subgroup.zpowers ζ) = ↑(rootsOfUnity k R)

Proof state:
case a
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
⊢ ↑(Subgroup.zpowers ζ) = ↑(rootsOfUnity k R)

Tactic:
have F : Fintype (Subgroup.zpowers ζ) := Fintype.ofEquiv _ h.zmodEquivZPowers.toEquiv

Result:
case a
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
F : Fintype ↥(Subgroup.zpowers ζ)
⊢ ↑(Subgroup.zpowers ζ) = ↑(rootsOfUnity k R)

Proof state:
case a
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
F : Fintype ↥(Subgroup.zpowers ζ)
⊢ ↑(Subgroup.zpowers ζ) = ↑(rootsOfUnity k R)

Tactic:
refine
  @Set.eq_of_subset_of_card_le Rˣ _ _ F (rootsOfUnity.fintype R k)
    (Subgroup.zpowers_le_of_mem <| show ζ ∈ rootsOfUnity k R from h.pow_eq_one) ?_

Result:
case a
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
F : Fintype ↥(Subgroup.zpowers ζ)
⊢ Fintype.card ↑↑(rootsOfUnity k R) ≤ Fintype.card ↑↑(Subgroup.zpowers ζ)

Proof state:
case a
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
F : Fintype ↥(Subgroup.zpowers ζ)
⊢ Fintype.card ↑↑(rootsOfUnity k R) ≤ Fintype.card ↑↑(Subgroup.zpowers ζ)

Tactic:
calc
  Fintype.card (rootsOfUnity k R) ≤ k := card_rootsOfUnity R k
  _ = Fintype.card (ZMod k) := (ZMod.card k).symm
  _ = Fintype.card (Subgroup.zpowers ζ) := Fintype.card_congr h.zmodEquivZPowers.toEquiv

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Induction.lean
lemma _root_.induction_on_primes {P : ℕ → Prop} (h₀ : P 0) (h₁ : P 1)
    (h : ∀ p a : ℕ, p.Prime → P a → P (p * a)) : ∀ n, P n

Proof state:
case zero
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Prime p → P a → P (p * a)
a p : ℕ
hp : Prime p
ha : P a
⊢ P (p ^ 0 * a)

Tactic:
simpa using ha

Result:
no goals

Proof state:
case succ
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Prime p → P a → P (p * a)
a p : ℕ
hp : Prime p
ha : P a
n : ℕ
ih : P (p ^ n * a)
⊢ P (p * (p ^ n * a))

Tactic:
exact h _ _ hp ih

Result:
no goals

Proof state:
case succ
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Prime p → P a → P (p * a)
a p : ℕ
hp : Prime p
ha : P a
n : ℕ
ih : P (p ^ n * a)
⊢ P (p ^ (n + 1) * a)

Tactic:
rw [pow_succ', mul_assoc]

Result:
case succ
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Prime p → P a → P (p * a)
a p : ℕ
hp : Prime p
ha : P a
n : ℕ
ih : P (p ^ n * a)
⊢ P (p * (p ^ n * a))

Proof state:
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Prime p → P a → P (p * a)
⊢ ∀ (a p n : ℕ), Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)

Tactic:
rintro a p n hp - - ha

Result:
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Prime p → P a → P (p * a)
a p n : ℕ
hp : Prime p
ha : P a
⊢ P (p ^ n * a)

Proof state:
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Prime p → P a → P (p * a)
a p n : ℕ
hp : Prime p
ha : P a
⊢ P (p ^ n * a)

Tactic:
induction' n with n ih

Result:
case zero
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Prime p → P a → P (p * a)
a p : ℕ
hp : Prime p
ha : P a
⊢ P (p ^ 0 * a)

case succ
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Prime p → P a → P (p * a)
a p : ℕ
hp : Prime p
ha : P a
n : ℕ
ih : P (p ^ n * a)
⊢ P (p ^ (n + 1) * a)

Proof state:
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Prime p → P a → P (p * a)
⊢ ∀ (n : ℕ), P n

Tactic:
refine recOnPrimePow h₀ h₁ ?_

Result:
P : ℕ → Prop
h₀ : P 0
h₁ : P 1
h : ∀ (p a : ℕ), Prime p → P a → P (p * a)
⊢ ∀ (a p n : ℕ), Prime p → ¬p ∣ a → 0 < n → P a → P (p ^ n * a)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
private lemma toAffine_negAddY_of_eq {P : Fin 3 → F} (hPz : P z ≠ 0) {n d : F} (hd : d ≠ 0) :
    W.toAffine.negAddY (P x / P z ^ 2) (P x / P z ^ 2) (P y / P z ^ 3) (-n / (P z * d)) =
      (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2 - P x * d ^ 2)
        + P y * d ^ 3) / (P z * d) ^ 3

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ (toAffine W).negAddY (P x / P z ^ 2) (P x / P z ^ 2) (P y / P z ^ 3) (-n / (P z * d)) =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2 - P x * d ^ 2) + P y * d ^ 3) /
      (P z * d) ^ 3

Tactic:
rw [Affine.negAddY, toAffine_addX_of_eq hPz hd]

Result:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ -n / (P z * d) *
        ((n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2) / (P z * d) ^ 2 - P x / P z ^ 2) +
      P y / P z ^ 3 =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2 - P x * d ^ 2) + P y * d ^ 3) /
      (P z * d) ^ 3

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ (-(n * ((n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2) * P z ^ 2 - (P z * d) ^ 2 * P x) *
            P z ^ 3) +
        P y * (P z * d * ((P z * d) ^ 2 * P z ^ 2))) *
      (P z * d) ^ 3 =
    (-(n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2 - P x * d ^ 2)) + P y * d ^ 3) *
      (P z * d * ((P z * d) ^ 2 * P z ^ 2) * P z ^ 3)

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ -n / (P z * d) *
        ((n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2) / (P z * d) ^ 2 - P x / P z ^ 2) +
      P y / P z ^ 3 =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2 - P x * d ^ 2) + P y * d ^ 3) /
      (P z * d) ^ 3

Tactic:
field_simp [mul_ne_zero (pow_ne_zero 2 <| mul_ne_zero hPz hd) <| pow_ne_zero 2 hPz]

Result:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ (-(n * ((n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2) * P z ^ 2 - (P z * d) ^ 2 * P x) *
            P z ^ 3) +
        P y * (P z * d * ((P z * d) ^ 2 * P z ^ 2))) *
      (P z * d) ^ 3 =
    (-(n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2 - P x * d ^ 2)) + P y * d ^ 3) *
      (P z * d * ((P z * d) ^ 2 * P z ^ 2) * P z ^ 3)
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem stronglyMeasurable_in_set {m : MeasurableSpace α} [TopologicalSpace β] [Zero β] {s : Set α}
    {f : α → β} (hs : MeasurableSet s) (hf : StronglyMeasurable f)
    (hf_zero : ∀ x, x ∉ s → f x = 0) :
    ∃ fs : ℕ → α →ₛ β,
      (∀ x, Tendsto (fun n => fs n x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ n, fs n x = 0

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
x : α
hx : x ∈ s
n : ℕ
⊢ (g_seq_s n) x = (hf.approx n) x

Tactic:
rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_mem hx]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
x : α
hx : x ∉ s
n : ℕ
⊢ (g_seq_s n) x = 0

Tactic:
rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_not_mem hx]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
x : α
hx : x ∈ s
⊢ Tendsto (fun n => (g_seq_s n) x) atTop (𝓝 (f x))

Tactic:
simp_rw [hg_eq x hx]

Result:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
x : α
hx : x ∈ s
⊢ Tendsto (fun n => (hf.approx n) x) atTop (𝓝 (f x))

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), (fs n) x = 0

Tactic:
let g_seq_s : ℕ → @SimpleFunc α m β := fun n => (hf.approx n).restrict s

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), (fs n) x = 0
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem Set.Countable.exists_pos_forall_sum_le {ι : Type*} {s : Set ι} (hs : s.Countable) {ε : ℝ}
    (hε : 0 < ε) : ∃ ε' : ι → ℝ,
    (∀ i, 0 < ε' i) ∧ ∀ t : Finset ι, ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε

Proof state:
case intro.intro.intro.intro
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∑ i ∈ t, ε' i ≤ ε

Tactic:
rw [← sum_subtype_of_mem _ ht]

Result:
case intro.intro.intro.intro
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∑ x ∈ Finset.subtype (Membership.mem s) t, ε' ↑x ≤ ε

Proof state:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε

Tactic:
rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩

Result:
case intro.intro.intro.intro
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε

Proof state:
case intro.intro.intro.intro
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∑ x ∈ Finset.subtype (Membership.mem s) t, ε' ↑x ≤ ε

Tactic:
refine (sum_le_hasSum _ ?_ hε'c).trans hcε

Result:
case intro.intro.intro.intro
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∀ i ∉ Finset.subtype (Membership.mem s) t, 0 ≤ ε' ↑i

Proof state:
case intro.intro.intro.intro
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε

Tactic:
refine ⟨ε', hpos, fun t ht ↦ ?_⟩

Result:
case intro.intro.intro.intro
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∑ i ∈ t, ε' i ≤ ε

Proof state:
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε

Tactic:
classical
rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩
refine ⟨ε', hpos, fun t ht ↦ ?_⟩
rw [← sum_subtype_of_mem _ ht]
refine (sum_le_hasSum _ ?_ hε'c).trans hcε
exact fun _ _ ↦ (hpos _).le

Result:
no goals

Proof state:
case intro.intro.intro.intro
ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∀ i ∉ Finset.subtype (Membership.mem s) t, 0 ≤ ε' ↑i

Tactic:
exact fun _ _ ↦ (hpos _).le

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem restrict_le_restrict_union (hi₁ : MeasurableSet i) (hi₂ : v ≤[i] w) (hj₁ : MeasurableSet j)
    (hj₂ : v ≤[j] w) : v ≤[i ∪ j] w

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ v ≤[⋃ b, bif b then i else j] w

Tactic:
refine restrict_le_restrict_countable_iUnion v w ?_ ?_

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ ∀ (b : Bool), MeasurableSet (bif b then i else j)

case refine_2
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ ∀ (b : Bool), v ≤[bif b then i else j] w

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ v ≤[i ∪ j] w

Tactic:
rw [Set.union_eq_iUnion]

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ v ≤[⋃ b, bif b then i else j] w

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ ∀ (b : Bool), MeasurableSet (bif b then i else j)

Tactic:
measurability

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ ∀ (b : Bool), v ≤[bif b then i else j] w

Tactic:
rintro (_ | _) <;> simpa

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/IsDiag.lean
theorem IsDiag.neg [AddGroup α] {A : Matrix n n α} (ha : A.IsDiag) : (-A).IsDiag

Proof state:
α : Type u_1
n : Type u_4
inst✝ : AddGroup α
A : Matrix n n α
ha : A.IsDiag
⊢ (-A).IsDiag

Tactic:
intro i j h

Result:
α : Type u_1
n : Type u_4
inst✝ : AddGroup α
A : Matrix n n α
ha : A.IsDiag
i j : n
h : i ≠ j
⊢ (-A) i j = 0

Proof state:
α : Type u_1
n : Type u_4
inst✝ : AddGroup α
A : Matrix n n α
ha : A.IsDiag
i j : n
h : i ≠ j
⊢ (-A) i j = 0

Tactic:
simp [ha h]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem prodComparison_natural_whiskerLeft (g : B ⟶ B') :
    F.map (A ◁ g) ≫ prodComparison F A B' =
      prodComparison F A B ≫ (F.obj A ◁ F.map g)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ChosenFiniteProducts C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : ChosenFiniteProducts D
F : C ⥤ D
A B B' : C
g : B ⟶ B'
⊢ prodComparison F A B ≫ (𝟙 (F.obj A) ⊗ F.map g) = prodComparison F A B ≫ F.obj A ◁ F.map g

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ChosenFiniteProducts C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : ChosenFiniteProducts D
F : C ⥤ D
A B B' : C
g : B ⟶ B'
⊢ F.map (A ◁ g) ≫ prodComparison F A B' = prodComparison F A B ≫ F.obj A ◁ F.map g

Tactic:
rw [← id_tensorHom, prodComparison_natural, Functor.map_id]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ChosenFiniteProducts C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : ChosenFiniteProducts D
F : C ⥤ D
A B B' : C
g : B ⟶ B'
⊢ prodComparison F A B ≫ (𝟙 (F.obj A) ⊗ F.map g) = prodComparison F A B ≫ F.obj A ◁ F.map g
-- Mathlib/Analysis/Calculus/BumpFunction/Normed.lean
theorem normed_neg (f : ContDiffBump (0 : E)) (x : E) : f.normed μ (-x) = f.normed μ x

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : HasContDiffBump E
inst✝ : MeasurableSpace E
μ : Measure E
f : ContDiffBump 0
x : E
⊢ f.normed μ (-x) = f.normed μ x

Tactic:
simp_rw [f.normed_def, f.neg]

Result:
no goals