harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Forall2.lean
theorem forall₂_zip : ∀ {l₁ l₂}, Forall₂ R l₁ l₂ → ∀ {a b}, (a, b) ∈ zip l₁ l₂ → R a b
  | _, _, Forall₂.cons h₁ h₂, x, y, hx => by
    rw [zip, zipWith, mem_cons] at hx
    match hx with
    | Or.inl rfl => exact h₁
    | Or.inr h₃ => exact forall₂_zip h₂ h₃

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
h₁ : R x y
⊢ R x y

Tactic:
exact h₁

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) ∈ (a✝ :: l₁✝).zip (b✝ :: l₂✝)
⊢ R x y

Tactic:
rw [zip, zipWith, mem_cons] at hx

Result:
α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
⊢ R x y

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
x✝¹ : β
x✝ : α
h₃ : (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
h₁ : R x✝ x✝¹
⊢ R x y

Tactic:
exact forall₂_zip h₂ h₃

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
⊢ R x y

Tactic:
match hx with
| Or.inl rfl => exact h₁
| Or.inr h₃ => exact forall₂_zip h₂ h₃

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem zeroIsoTerminal_inv [HasTerminal C] : zeroIsoTerminal.inv = (0 : ⊤_ C ⟶ 0)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
⊢ zeroIsoTerminal.inv = 0

Tactic:
ext

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_shiftLeft : eval assign (.shiftLeft lhs rhs) = (eval assign lhs) <<< (eval assign rhs)

Proof state:
assign : Assignment
a✝¹ : Nat
lhs : BVExpr a✝¹
a✝ : Nat
rhs : BVExpr a✝
⊢ eval assign (lhs.shiftLeft rhs) = eval assign lhs <<< eval assign rhs

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x

Proof state:
case mk
α : Type u_1
x : α
data : Array α
⊢ ({ toArray := data, size_toArray := ⋯ }.push x)[data.size] = x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v : Vector α n
x : α
⊢ (v.push x)[n] = x

Tactic:
rcases v with ⟨data, rfl⟩

Result:
case mk
α : Type u_1
x : α
data : Array α
⊢ ({ toArray := data, size_toArray := ⋯ }.push x)[data.size] = x
-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Module.eq_zero_of_localization_maximal (m : M)
    (h : ∀ (P : Ideal R) [P.IsMaximal], f P m = 0) :
    m = 0 :=
  eq_of_localization_maximal _ f _ _ fun P _ ↦ by rw [h, map_zero]

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
m : M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m = 0
P : Ideal R
x✝ : P.IsMaximal
⊢ (f P) m = (f P) 0

Tactic:
rw [h, map_zero]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiffOn.sub {s : Set E} {f g : E → F} (hf : ContDiffOn 𝕜 n f s)
    (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x => f x - g x) s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
s : Set E
f g : E → F
hf : ContDiffOn 𝕜 n f s
hg : ContDiffOn 𝕜 n g s
⊢ ContDiffOn 𝕜 n (fun x => f x - g x) s

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/Data/Multiset/Nodup.lean
theorem nodup_iff_ne_cons_cons {s : Multiset α} : s.Nodup ↔ ∀ a t, s ≠ a ::ₘ a ::ₘ t :=
  nodup_iff_le.trans
    ⟨fun h a _ s_eq => h a (s_eq.symm ▸ cons_le_cons a (cons_le_cons a (zero_le _))), fun h a le =>
      let ⟨t, s_eq⟩ := le_iff_exists_add.mp le
      h a t (by rwa [cons_add, cons_add, Multiset.zero_add] at s_eq)⟩

Proof state:
α : Type u_1
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ a ::ₘ 0 + t
⊢ s = a ::ₘ a ::ₘ t

Tactic:
rwa [cons_add, cons_add, Multiset.zero_add] at s_eq

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem zmodEquivZPowers_symm_apply_zpow (i : ℤ) :
    h.zmodEquivZPowers.symm (Additive.ofMul (⟨ζ ^ i, i, rfl⟩ : Subgroup.zpowers ζ)) = i

Proof state:
R : Type u_4
k : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℤ
⊢ h.zmodEquivZPowers.symm (Additive.ofMul ⟨ζ ^ i, ⋯⟩) = ↑i

Tactic:
rw [← h.zmodEquivZPowers.symm_apply_apply i, zmodEquivZPowers_apply_coe_int]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_apply_left (a : α) : toIocDiv hp a a = -1 :=
  toIocDiv_eq_of_sub_zsmul_mem_Ioc hp <| by simp [hp]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a - -1 • p ∈ Set.Ioc a (a + p)

Tactic:
simp [hp]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem mk_pow (a : M) (n : ℕ) : Associates.mk (a ^ n) = Associates.mk a ^ n

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a : M
n : ℕ
⊢ Associates.mk (a ^ n) = Associates.mk a ^ n

Tactic:
induction n <;> simp [*, pow_succ, Associates.mk_mul_mk.symm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem is_left_invariant_prehaar {K₀ : PositiveCompacts G} {U : Set G} (hU : (interior U).Nonempty)
    (g : G) (K : Compacts G) :
    prehaar (K₀ : Set G) U (K.map _ <| continuous_mul_left g) = prehaar (K₀ : Set G) U K

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
g : G
K : Compacts G
⊢ prehaar (↑K₀) U (Compacts.map (fun b => g * b) ⋯ K) = prehaar (↑K₀) U K

Tactic:
simp only [prehaar, Compacts.coe_map, is_left_invariant_index K.isCompact _ hU]

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem lineDifferentiableWithinAt_univ :
    LineDifferentiableWithinAt 𝕜 f univ x v ↔ LineDifferentiableAt 𝕜 f x v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
⊢ LineDifferentiableWithinAt 𝕜 f univ x v ↔ LineDifferentiableAt 𝕜 f x v

Tactic:
simp only [LineDifferentiableWithinAt, LineDifferentiableAt, preimage_univ,
  differentiableWithinAt_univ]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/ProductFormula.lean
theorem prod_abs_eq_one {x : K} (h_x_nezero : x ≠ 0) :
    (∏ w : InfinitePlace K, w x ^ w.mult) * ∏ᶠ w : FinitePlace K, w x = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
h_x_nezero : x ≠ 0
⊢ (∏ w : InfinitePlace K, w x ^ w.mult) * ∏ᶠ (w : FinitePlace K), w x = 1

Tactic:
simp [prod_eq_inv_abs_norm, InfinitePlace.prod_eq_abs_norm, h_x_nezero]

Result:
no goals
-- Mathlib/RingTheory/HopfAlgebra/MonoidAlgebra.lean
@[simp]
lemma antipode_single (g : G) (a : A) :
    antipode (R := R) (single g a) = single g⁻¹ (antipode (R := R) a)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : HopfAlgebra R A
G : Type u_3
inst✝ : Group G
g : G
a : A
⊢ antipode (single g a) = single g⁻¹ (antipode a)

Tactic:
simp [MonoidAlgebra, antipode]

Result:
no goals
-- Mathlib/Topology/Separation/SeparatedNhds.lean
theorem HasSeparatingCover.mono {s₁ s₂ t₁ t₂ : Set X} (sc_st : HasSeparatingCover s₂ t₂)
    (s_sub : s₁ ⊆ s₂) (t_sub : t₁ ⊆ t₂) : HasSeparatingCover s₁ t₁

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
sc_st : HasSeparatingCover s₂ t₂
s_sub : s₁ ⊆ s₂
t_sub : t₁ ⊆ t₂
⊢ HasSeparatingCover s₁ t₁

Tactic:
obtain ⟨u, u_cov, u_props⟩ := sc_st

Result:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
s_sub : s₁ ⊆ s₂
t_sub : t₁ ⊆ t₂
u : ℕ → Set X
u_cov : s₂ ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen (u n) ∧ Disjoint (closure (u n)) t₂
⊢ HasSeparatingCover s₁ t₁

Proof state:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
s_sub : s₁ ⊆ s₂
t_sub : t₁ ⊆ t₂
u : ℕ → Set X
u_cov : s₂ ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen (u n) ∧ Disjoint (closure (u n)) t₂
⊢ HasSeparatingCover s₁ t₁

Tactic:
exact
  ⟨u,
   s_sub.trans u_cov,
   fun n ↦
     ⟨(u_props n).1,
      disjoint_of_subset (fun ⦃_⦄ a ↦ a) t_sub (u_props n).2⟩⟩

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.induction_on (hs : IsCompact s) {p : Set X → Prop} (he : p ∅)
    (hmono : ∀ ⦃s t⦄, s ⊆ t → p t → p s) (hunion : ∀ ⦃s t⦄, p s → p t → p (s ∪ t))
    (hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t) : p s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
this : sᶜ ∈ f
⊢ p s

Tactic:
rwa [← compl_compl s]

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
⊢ p s

Tactic:
have : sᶜ ∈ f := hs.compl_mem_sets_of_nhdsWithin (by simpa [f] using hnhds)

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
this : sᶜ ∈ f
⊢ p s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
⊢ p s

Tactic:
let f : Filter X := comk p he (fun _t ht _s hsub ↦ hmono hsub ht) (fun _s hs _t ht ↦ hunion hs ht)

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
⊢ p s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f

Tactic:
simpa [f] using hnhds

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem reverse_cast {w v : Nat} (h : w = v) (x : BitVec w) :
    (x.cast h).reverse = x.reverse.cast h

Proof state:
w v : Nat
h : w = v
x : BitVec w
⊢ (BitVec.cast h x).reverse = BitVec.cast h x.reverse

Tactic:
subst h

Result:
w : Nat
x : BitVec w
⊢ (BitVec.cast ⋯ x).reverse = BitVec.cast ⋯ x.reverse

Proof state:
w : Nat
x : BitVec w
⊢ (BitVec.cast ⋯ x).reverse = BitVec.cast ⋯ x.reverse

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x

Proof state:
case mk
α✝ : Type
p : α✝ → Bool
n✝ : Nat
toArray✝ : Array α✝
size_toArray✝ : toArray✝.size = n✝
⊢ find? p { toArray := toArray✝, size_toArray := size_toArray✝ } = none ↔
    ∀ (x : α✝), x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → ¬p x = true

Tactic:
simp

Result:
no goals

Proof state:
α✝ : Type
p : α✝ → Bool
n✝ : Nat
l : Vector α✝ n✝
⊢ find? p l = none ↔ ∀ (x : α✝), x ∈ l → ¬p x = true

Tactic:
cases l

Result:
case mk
α✝ : Type
p : α✝ → Bool
n✝ : Nat
toArray✝ : Array α✝
size_toArray✝ : toArray✝.size = n✝
⊢ find? p { toArray := toArray✝, size_toArray := size_toArray✝ } = none ↔
    ∀ (x : α✝), x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → ¬p x = true
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_eval_X (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
ha : autoParam (p a) _auto✝
⊢ cfc (fun a => Polynomial.eval a X) a = a

Tactic:
simpa using cfc_id R a

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
theorem ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι (m : M) :
    RingQuot.mkAlgHom R (Rel R M) (FreeAlgebra.ι R m) = ι R m

Proof state:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m) = (ι R) m

Tactic:
rw [ι]

Result:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m) =
    { toFun := fun m => (RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m), map_add' := ⋯, map_smul' := ⋯ } m

Proof state:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m) =
    { toFun := fun m => (RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m), map_add' := ⋯, map_smul' := ⋯ } m

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem inter_ae_eq_right_of_ae_eq_univ (h : s =ᵐ[μ] univ) : (s ∩ t : Set α) =ᵐ[μ] t

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] univ
⊢ s ∩ t =ᶠ[ae μ] t

Tactic:
convert ae_eq_set_inter h (ae_eq_refl t)

Result:
case h.e'_5
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] univ
⊢ t = univ ∩ t

Proof state:
case h.e'_5
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] univ
⊢ t = univ ∩ t

Tactic:
rw [univ_inter]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem filter_true (l : List α) :
    filter (fun _ => true) l = l

Proof state:
α : Type u
l : List α
⊢ filter (fun x => true) l = l

Tactic:
induction l <;> simp [*, filter]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
/-- The iterated derivative commutes with shifting the function by a constant on the right. -/
lemma iteratedFDerivWithin_comp_add_right (n : ℕ) (a : E) (x : E) :
    iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + a)) s x =
      iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
a x : E
⊢ iteratedFDerivWithin 𝕜 n (fun z => f (z + a)) s x = iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a)

Tactic:
simp [iteratedFDerivWithin_comp_add_right']

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem forall_mem_map {f : α ↪ β} {s : Finset α} {p : ∀ a, a ∈ s.map f → Prop} :
    (∀ y (H : y ∈ s.map f), p y H) ↔ ∀ x (H : x ∈ s), p (f x) (mem_map_of_mem _ H) :=
  ⟨fun h y hy => h (f y) (mem_map_of_mem _ hy),
   fun h x hx => by
    obtain ⟨y, hy, rfl⟩ := mem_map.1 hx
    exact h _ hy⟩

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
p : (a : β) → a ∈ map f s → Prop
h : ∀ (x : α) (H : x ∈ s), p (f x) ⋯
y : α
hy : y ∈ s
hx : f y ∈ map f s
⊢ p (f y) hx

Tactic:
exact h _ hy

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
p : (a : β) → a ∈ map f s → Prop
h : ∀ (x : α) (H : x ∈ s), p (f x) ⋯
x : β
hx : x ∈ map f s
⊢ p x hx

Tactic:
obtain ⟨y, hy, rfl⟩ := mem_map.1 hx

Result:
case intro.intro
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
p : (a : β) → a ∈ map f s → Prop
h : ∀ (x : α) (H : x ∈ s), p (f x) ⋯
y : α
hy : y ∈ s
hx : f y ∈ map f s
⊢ p (f y) hx
-- Mathlib/Algebra/Order/Floor.lean
lemma ceil_le_two_mul (ha : 2⁻¹ ≤ a) : ⌈a⌉₊ ≤ 2 * a :=
  ceil_le_mul one_lt_two (by norm_num at ha ⊢; exact ha)

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a : α
ha : 2⁻¹ ≤ a
⊢ ↑⌈(2 - 1)⁻¹⌉₊ / 2 ≤ a

Tactic:
norm_num at ha ⊢

Result:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a : α
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a : α
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a

Tactic:
exact ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_le_mul_of_nonpos_right {a b c : Int}
    (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c :=
  have : -c ≥ 0 := Int.neg_nonneg_of_nonpos hc
  have : b * -c ≤ a * -c := Int.mul_le_mul_of_nonneg_right h this
  Int.le_of_neg_le_neg <| by rwa [← Int.neg_mul_eq_mul_neg, ← Int.neg_mul_eq_mul_neg] at this

Proof state:
a b c : Int
h : b ≤ a
hc : c ≤ 0
this✝ : -c ≥ 0
this : b * -c ≤ a * -c
⊢ -(b * c) ≤ -(a * c)

Tactic:
rwa [← Int.neg_mul_eq_mul_neg, ← Int.neg_mul_eq_mul_neg] at this

Result:
no goals
-- Mathlib/Algebra/Ring/Semiconj.lean
theorem neg_one_right (a : R) : SemiconjBy a (-1) (-1)

Proof state:
R : Type u
inst✝¹ : MulOneClass R
inst✝ : HasDistribNeg R
a : R
⊢ SemiconjBy a (-1) (-1)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insertManyIfNewUnit_list_le [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List α} :
    (insertManyIfNewUnit m l).1.1.size ≤ m.1.size + l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
⊢ (insertManyIfNewUnit m l).val.val.size ≤ m.val.size + l.length

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.length_insertListIfNewUnit_le

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma map_Φ (n : ℤ) : (W.map f).Φ n = (W.Φ n).map f

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (X * (mapRingHom f) (W.ΨSq n) -
      (mapRingHom f) (W.preΨ (n + 1)) * (mapRingHom f) (W.preΨ (n - 1)) * if Even n then 1 else (mapRingHom f) W.Ψ₂Sq) =
    (mapRingHom f) (X * W.ΨSq n - W.preΨ (n + 1) * W.preΨ (n - 1) * if Even n then 1 else W.Ψ₂Sq)

Tactic:
map_simp

Result:
no goals

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).Φ n = Polynomial.map f (W.Φ n)

Tactic:
simp only [Φ, map_ΨSq, map_preΨ, map_Ψ₂Sq, ← coe_mapRingHom]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (X * (mapRingHom f) (W.ΨSq n) -
      (mapRingHom f) (W.preΨ (n + 1)) * (mapRingHom f) (W.preΨ (n - 1)) * if Even n then 1 else (mapRingHom f) W.Ψ₂Sq) =
    (mapRingHom f) (X * W.ΨSq n - W.preΨ (n + 1) * W.preΨ (n - 1) * if Even n then 1 else W.Ψ₂Sq)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_eq_nil_iff {l} : filterMap f l = #[] ↔ ∀ a, a ∈ l → f a = none

Proof state:
case mk
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
toList✝ : List α✝¹
⊢ filterMap f { toList := toList✝ } = #[] ↔ ∀ (a : α✝¹), a ∈ { toList := toList✝ } → f a = none

Tactic:
simp

Result:
no goals

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
l : Array α✝¹
⊢ filterMap f l = #[] ↔ ∀ (a : α✝¹), a ∈ l → f a = none

Tactic:
cases l

Result:
case mk
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
toList✝ : List α✝¹
⊢ filterMap f { toList := toList✝ } = #[] ↔ ∀ (a : α✝¹), a ∈ { toList := toList✝ } → f a = none
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem mul_ball : s * ball x δ = x • thickening δ s

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ s * ball x δ = x • thickening δ s

Tactic:
rw [← smul_ball_one, mul_smul_comm, mul_ball_one]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma le_of_smul_le_smul_of_neg [PosSMulReflectLE α β] (h : a • b₁ ≤ a • b₂) (ha : a < 0) :
    b₂ ≤ b₁

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝³ : OrderedRing α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLE α β
h : -a • b₂ ≤ -a • b₁
ha : a < 0
⊢ b₂ ≤ b₁

Tactic:
exact le_of_smul_le_smul_of_pos_left h <| neg_pos.2 ha

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝³ : OrderedRing α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLE α β
h : a • b₁ ≤ a • b₂
ha : a < 0
⊢ b₂ ≤ b₁

Tactic:
rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff] at h

Result:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝³ : OrderedRing α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLE α β
h : -a • b₂ ≤ -a • b₁
ha : a < 0
⊢ b₂ ≤ b₁
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem isClosed_setOf_continuous [TopologicalSpace α] (h : RestrictGenTopology 𝔖) :
    IsClosed {f : α →ᵤ[𝔖] β | Continuous (toFun 𝔖 f)}

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
h : RestrictGenTopology 𝔖
f : α →ᵤ[𝔖] β
u : Filter (α →ᵤ[𝔖] β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous ((toFun 𝔖) f)}
huf : u ≤ 𝓝 f
s : Set α
hs : s ∈ 𝔖
⊢ ContinuousOn ((toFun 𝔖) f) s

Tactic:
rw [← tendsto_id', UniformOnFun.tendsto_iff_tendstoUniformlyOn] at huf

Result:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
h : RestrictGenTopology 𝔖
f : α →ᵤ[𝔖] β
u : Filter (α →ᵤ[𝔖] β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous ((toFun 𝔖) f)}
huf : ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(toFun 𝔖) ∘ id) ((toFun 𝔖) f) u s
s : Set α
hs : s ∈ 𝔖
⊢ ContinuousOn ((toFun 𝔖) f) s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
h : RestrictGenTopology 𝔖
⊢ IsClosed {f | Continuous ((toFun 𝔖) f)}

Tactic:
refine isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ h.continuous_iff.2 fun s hs ↦ ?_

Result:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
h : RestrictGenTopology 𝔖
f : α →ᵤ[𝔖] β
u : Filter (α →ᵤ[𝔖] β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous ((toFun 𝔖) f)}
huf : u ≤ 𝓝 f
s : Set α
hs : s ∈ 𝔖
⊢ ContinuousOn ((toFun 𝔖) f) s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
h : RestrictGenTopology 𝔖
f : α →ᵤ[𝔖] β
u : Filter (α →ᵤ[𝔖] β)
x✝ : u.NeBot
hu : u ≤ 𝓟 {f | Continuous ((toFun 𝔖) f)}
huf : ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(toFun 𝔖) ∘ id) ((toFun 𝔖) f) u s
s : Set α
hs : s ∈ 𝔖
⊢ ContinuousOn ((toFun 𝔖) f) s

Tactic:
exact (huf s hs).continuousOn <| hu fun _ ↦ Continuous.continuousOn

Result:
no goals