harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem insertMany_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {l : ρ} :
    m.insertMany l = Raw₀.insertMany ⟨m, h.size_buckets_pos⟩ l

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
h : m.WF
ρ : Type w
inst✝ : ForIn Id ρ ((a : α) × β a)
l : ρ
⊢ m.insertMany l = (Raw₀.insertMany ⟨m, ⋯⟩ l).val.val

Tactic:
simp [Raw.insertMany, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem mapL_apply (x : ⨂[𝕜] i, E i) : mapL f x = map (fun i ↦ (f i).toLinearMap) x

Proof state:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
⊢ (mapL f) x = (map fun i => ↑(f i)) x

Tactic:
induction x using PiTensorProduct.induction_on with
| smul_tprod =>
  simp only [mapL, map_smul, liftIsometry_apply_apply, lift.tprod,
  ContinuousMultilinearMap.coe_coe, ContinuousMultilinearMap.compContinuousLinearMap_apply,
  tprodL_toFun, map_tprod, ContinuousLinearMap.coe_coe]
| add _ _ hx hy => simp only [map_add, hx, hy]

Result:
no goals

Proof state:
case add
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x✝ y✝ : ⨂[𝕜] (i : ι), E i
hx : (mapL f) x✝ = (map fun i => ↑(f i)) x✝
hy : (mapL f) y✝ = (map fun i => ↑(f i)) y✝
⊢ (mapL f) (x✝ + y✝) = (map fun i => ↑(f i)) (x✝ + y✝)

Tactic:
simp only [map_add, hx, hy]

Result:
no goals

Proof state:
case smul_tprod
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
r✝ : 𝕜
f✝ : (i : ι) → E i
⊢ (mapL f) (r✝ • (tprod 𝕜) f✝) = (map fun i => ↑(f i)) (r✝ • (tprod 𝕜) f✝)

Tactic:
simp only [mapL, map_smul, liftIsometry_apply_apply, lift.tprod,
ContinuousMultilinearMap.coe_coe, ContinuousMultilinearMap.compContinuousLinearMap_apply,
tprodL_toFun, map_tprod, ContinuousLinearMap.coe_coe]

Result:
no goals
-- Mathlib/Data/Int/CardIntervalMod.lean
theorem Ioc_filter_dvd_card : #{x ∈ Ioc a b | r ∣ x} = max (⌊b / (r : ℚ)⌋ - ⌊a / (r : ℚ)⌋) 0

Proof state:
a b r : ℤ
hr : 0 < r
⊢ ↑(#(filter (fun x => r ∣ x) (Ioc a b))) = (⌊↑b / ↑r⌋ - ⌊↑a / ↑r⌋) ⊔ 0

Tactic:
rw [Ioc_filter_dvd_eq _ _ hr, card_map, card_Ioc, toNat_eq_max]

Result:
no goals
-- Mathlib/ModelTheory/Algebra/Ring/Basic.lean
theorem realize_neg (x : ring.Term α) (v : α → R) :
    Term.realize v (-x) = -Term.realize v x

Proof state:
α : Type u_1
R : Type u_2
inst✝⁵ : Add R
inst✝⁴ : Mul R
inst✝³ : Neg R
inst✝² : One R
inst✝¹ : Zero R
inst✝ : CompatibleRing R
x : ring.Term α
v : α → R
⊢ Term.realize v (-x) = -Term.realize v x

Tactic:
simp [neg_def, funMap_neg]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_def_of_nonpos {x : ℝ} (hx : x ≤ 0) (y : ℝ) :
    x ^ y = if x = 0 then if y = 0 then 1 else 0 else exp (log x * y) * cos (y * π)

Proof state:
case neg
x : ℝ
hx : x ≤ 0
y : ℝ
h : ¬x = 0
⊢ (↑x ^ ↑y).re = rexp (log x * y) * cos (y * π)

Tactic:
exact rpow_def_of_neg (lt_of_le_of_ne hx h) _

Result:
no goals

Proof state:
x : ℝ
hx : x ≤ 0
y : ℝ
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y) * cos (y * π)

Tactic:
split_ifs with h <;> simp [rpow_def, *]

Result:
case neg
x : ℝ
hx : x ≤ 0
y : ℝ
h : ¬x = 0
⊢ (↑x ^ ↑y).re = rexp (log x * y) * cos (y * π)
-- Mathlib/Data/List/Nodup.lean
theorem get_idxOf [DecidableEq α] {l : List α} (H : Nodup l) (i : Fin l.length) :
    idxOf (get l i) l = i

Proof state:
α : Type u
inst✝ : DecidableEq α
l : List α
H : l.Nodup
i : Fin l.length
⊢ idxOf (l.get i) l = ↑i

Tactic:
simp [idxOf_getElem, H]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem inv_hom_id_tensor {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
    (f.inv ⊗ g) ≫ (f.hom ⊗ h) = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f.inv ⊗ g) ≫ (f.hom ⊗ h) = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h)

Tactic:
rw [← tensor_comp, f.inv_hom_id]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ 𝟙 W ⊗ g ≫ h = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ 𝟙 W ⊗ g ≫ h = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h)

Tactic:
simp [id_tensorHom]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Spectrum.lean
/-- A non-unital star algebra homomorphism of complex C⋆-algebras is norm contractive. -/
lemma norm_apply_le (φ : F) (a : A) : ‖φ a‖ ≤ ‖a‖

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
⊢ ‖φ a‖ ≤ ‖a‖

Tactic:
exact_mod_cast nnnorm_apply_le φ a

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem pi_univ_ite (s : Set ι) [DecidablePred (· ∈ s)] (t : ∀ i, Set (α i)) :
    (pi univ fun i => if i ∈ s then t i else univ) = s.pi t

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
⊢ (univ.pi fun i => if i ∈ s then t i else univ) = s.pi t

Tactic:
ext

Result:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ (x✝ ∈ univ.pi fun i => if i ∈ s then t i else univ) ↔ x✝ ∈ s.pi t

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ (∀ i ∈ univ, x✝ i ∈ if i ∈ s then t i else univ) ↔ ∀ i ∈ s, x✝ i ∈ t i

Tactic:
apply forall_congr'

Result:
case h.h
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ ∀ (a : ι), (a ∈ univ → x✝ a ∈ if a ∈ s then t a else univ) ↔ a ∈ s → x✝ a ∈ t a

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ (x✝ ∈ univ.pi fun i => if i ∈ s then t i else univ) ↔ x✝ ∈ s.pi t

Tactic:
simp_rw [Set.mem_pi]

Result:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ (∀ i ∈ univ, x✝ i ∈ if i ∈ s then t i else univ) ↔ ∀ i ∈ s, x✝ i ∈ t i

Proof state:
case h.h
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ ∀ (a : ι), (a ∈ univ → x✝ a ∈ if a ∈ s then t a else univ) ↔ a ∈ s → x✝ a ∈ t a

Tactic:
intro i

Result:
case h.h
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
i : ι
⊢ (i ∈ univ → x✝ i ∈ if i ∈ s then t i else univ) ↔ i ∈ s → x✝ i ∈ t i

Proof state:
case h.h
ι : Type u_1
α : ι → Type u_2
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
i : ι
⊢ (i ∈ univ → x✝ i ∈ if i ∈ s then t i else univ) ↔ i ∈ s → x✝ i ∈ t i

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/Data/Matrix/Kronecker.lean
theorem kroneckerMap_one_one [Zero α] [Zero β] [Zero γ] [One α] [One β] [One γ] [DecidableEq m]
    [DecidableEq n] (f : α → β → γ) (hf₁ : ∀ b, f 0 b = 0) (hf₂ : ∀ a, f a 0 = 0)
    (hf₃ : f 1 1 = 1) : kroneckerMap f (1 : Matrix m m α) (1 : Matrix n n β) = 1 :=
  (kroneckerMap_diagonal_diagonal _ hf₁ hf₂ _ _).trans <| by simp only [hf₃, diagonal_one]

Proof state:
α : Type u_2
β : Type u_4
γ : Type u_6
m : Type u_9
n : Type u_10
inst✝⁷ : Zero α
inst✝⁶ : Zero β
inst✝⁵ : Zero γ
inst✝⁴ : One α
inst✝³ : One β
inst✝² : One γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
hf₃ : f 1 1 = 1
⊢ (diagonal fun mn => f 1 1) = 1

Tactic:
simp only [hf₃, diagonal_one]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
@[to_additive (attr := simp)]
lemma tprod_extend_one {γ : Type*} {g : γ → β} (hg : Injective g) (f : γ → α) :
    ∏' y, extend g f 1 y = ∏' x, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
γ : Type u_4
g : γ → β
hg : Injective g
f : γ → α
⊢ ∏' (y : β), extend g f 1 y = ∏' (x : γ), f x

Tactic:
have : mulSupport (extend g f 1) ⊆ Set.range g := mulSupport_subset_iff'.2 <| extend_apply' _ _

Result:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
γ : Type u_4
g : γ → β
hg : Injective g
f : γ → α
this : mulSupport (extend g f 1) ⊆ Set.range g
⊢ ∏' (y : β), extend g f 1 y = ∏' (x : γ), f x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
γ : Type u_4
g : γ → β
hg : Injective g
f : γ → α
this : mulSupport (extend g f 1) ⊆ Set.range g
⊢ ∏' (y : β), extend g f 1 y = ∏' (x : γ), f x

Tactic:
simp_rw [← hg.tprod_eq this, hg.extend_apply]

Result:
no goals
-- Mathlib/Topology/Algebra/ClopenNhdofOne.lean
theorem exist_openNormalSubgroup_sub_open_nhd_of_one {G : Type*} [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {U : Set G}
    (UOpen : IsOpen U) (einU : 1 ∈ U) : ∃ H : OpenNormalSubgroup G, (H : Set G) ⊆ U

Proof state:
case intro.intro
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
W : Set G
hW : 1 ∈ W ∧ IsClopen W
h : id W ⊆ U
⊢ ∃ H, ↑H ⊆ U

Tactic:
rcases IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhd_of_one hW.2 hW.1 with ⟨H, hH⟩

Result:
case intro.intro.intro
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
W : Set G
hW : 1 ∈ W ∧ IsClopen W
h : id W ⊆ U
H : OpenNormalSubgroup G
hH : ↑H ⊆ W
⊢ ∃ H, ↑H ⊆ U

Proof state:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
⊢ ∃ t ⊆ U, IsOpen t ∧ 1 ∈ t

Tactic:
use U

Result:
no goals

Proof state:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
⊢ ∃ H, ↑H ⊆ U

Tactic:
rcases ((Filter.HasBasis.mem_iff' ((nhds_basis_clopen (1 : G))) U ).mp <|
  mem_nhds_iff.mpr (by use U)) with ⟨W, hW, h⟩

Result:
case intro.intro
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
W : Set G
hW : 1 ∈ W ∧ IsClopen W
h : id W ⊆ U
⊢ ∃ H, ↑H ⊆ U

Proof state:
case intro.intro.intro
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
W : Set G
hW : 1 ∈ W ∧ IsClopen W
h : id W ⊆ U
H : OpenNormalSubgroup G
hH : ↑H ⊆ W
⊢ ∃ H, ↑H ⊆ U

Tactic:
exact ⟨H, fun _ a ↦ h (hH a)⟩

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem modEq_iff_dvd : a ≡ b [MOD n] ↔ (n : ℤ) ∣ b - a

Proof state:
n a b : ℕ
⊢ a ≡ b [MOD n] ↔ ↑n ∣ ↑b - ↑a

Tactic:
rw [ModEq, eq_comm, ← Int.natCast_inj, Int.natCast_mod, Int.natCast_mod,
  Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.dvd_iff_emod_eq_zero]

Result:
no goals
-- Mathlib/Order/Filter/Finite.lean
theorem mem_iInf_of_iInter {ι} {s : ι → Filter α} {U : Set α} {I : Set ι} (I_fin : I.Finite)
    {V : I → Set α} (hV : ∀ (i : I), V i ∈ s i) (hU : ⋂ i, V i ⊆ U) : U ∈ ⨅ i, s i

Proof state:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : ⋂ i, V i ⊆ U
⊢ U ∈ ⨅ i, s i

Tactic:
haveI := I_fin.fintype

Result:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : ⋂ i, V i ⊆ U
this : Fintype ↑I
⊢ U ∈ ⨅ i, s i

Proof state:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : ⋂ i, V i ⊆ U
this : Fintype ↑I
i : ↑I
⊢ V i ∈ ⨅ i, s i

Tactic:
exact mem_iInf_of_mem (i : ι) (hV _)

Result:
no goals

Proof state:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : ⋂ i, V i ⊆ U
this : Fintype ↑I
⊢ U ∈ ⨅ i, s i

Tactic:
refine mem_of_superset (iInter_mem.2 fun i => ?_) hU

Result:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : ⋂ i, V i ⊆ U
this : Fintype ↑I
i : ↑I
⊢ V i ∈ ⨅ i, s i
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma C_addPolynomial_slope {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
    (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : C (W.addPolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂) =
      -(C (X - C x₁) * C (X - C x₂) * C (X - C (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂)))

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ C (-((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))) =
    -(C (X - C x₁) * C (X - C x₂) * C (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

Tactic:
map_simp

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) =
    -(C (X - C x₁) * C (X - C x₂) * C (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

Tactic:
rw [addPolynomial_slope h₁ h₂ hxy]

Result:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ C (-((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))) =
    -(C (X - C x₁) * C (X - C x₂) * C (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem seq_eq_bind_map {α β : Type u} [Monad m] [LawfulMonad m] (f : m (α → β)) (x : m α) : f <*> x = f >>= (. <$> x)

Proof state:
m : Type u → Type u_1
α β : Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : m (α → β)
x : m α
⊢ f <*> x = do
    let x_1 ← f
    x_1 <$> x

Tactic:
rw [← bind_map]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iio_subset_Iic_iff [DenselyOrdered α] : Iio a ⊆ Iic b ↔ a ≤ b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
⊢ Iio a ⊆ Iic b ↔ a ≤ b

Tactic:
rw [← diff_eq_empty, Iio_diff_Iic, Ioo_eq_empty_iff, not_lt]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem norm_iteratedFDerivWithin_fderivWithin {n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    ‖iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x‖ =
      ‖iteratedFDerivWithin 𝕜 (n + 1) f s 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
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ ‖iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x‖ = ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖

Tactic:
rw [iteratedFDerivWithin_succ_eq_comp_right hs hx, comp_apply, LinearIsometryEquiv.norm_map]

Result:
no goals
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_inter_self (hs : s.Finite) : uniformOn s (s ∩ t) = uniformOn s t

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
⊢ (uniformOn s) (s ∩ t) = (uniformOn s) t

Tactic:
rw [uniformOn, cond_inter_self hs.measurableSet]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem intCast_re (n : ℤ) : (n : ℤ√d).re = n

Proof state:
d n : ℤ
⊢ (↑n).re = n

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem rootMultiplicity_mul' {p q : R[X]} {x : R}
    (hpq : (p /ₘ (X - C x) ^ p.rootMultiplicity x).eval x *
      (q /ₘ (X - C x) ^ q.rootMultiplicity x).eval x ≠ 0) :
    rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : eval x (p /ₘ (X - C x) ^ rootMultiplicity x p) * eval x (q /ₘ (X - C x) ^ rootMultiplicity x q) ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
simp_rw [eval_divByMonic_eq_trailingCoeff_comp] at hpq

Result:
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : (p.comp (X + C x)).trailingCoeff * (q.comp (X + C x)).trailingCoeff ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : (p.comp (X + C x)).trailingCoeff * (q.comp (X + C x)).trailingCoeff ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
simp_rw [rootMultiplicity_eq_natTrailingDegree, mul_comp, natTrailingDegree_mul' hpq]

Result:
no goals
-- Mathlib/Topology/Sheaves/Stalks.lean
theorem comp (ℱ : X.Presheaf C) (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    ℱ.stalkPushforward C (f ≫ g) x =
      (f _* ℱ).stalkPushforward C g (f x) ≫ ℱ.stalkPushforward C f x

Proof state:
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
U✝ : Opens ↑Z
hxU✝ : (ConcreteCategory.hom (f ≫ g)) x ∈ U✝
⊢ ((pushforward C (f ≫ g)).obj ℱ).germ U✝ ((ConcreteCategory.hom (f ≫ g)) x) hxU✝ ≫ stalkPushforward C (f ≫ g) ℱ x =
    ((pushforward C (f ≫ g)).obj ℱ).germ U✝ ((ConcreteCategory.hom (f ≫ g)) x) hxU✝ ≫
      stalkPushforward C g ((pushforward C f).obj ℱ) ((ConcreteCategory.hom f) x) ≫ stalkPushforward C f ℱ x

Tactic:
simp [germ, stalkPushforward]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ stalkPushforward C (f ≫ g) ℱ x =
    stalkPushforward C g ((pushforward C f).obj ℱ) ((ConcreteCategory.hom f) x) ≫ stalkPushforward C f ℱ x

Tactic:
ext

Result:
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
U✝ : Opens ↑Z
hxU✝ : (ConcreteCategory.hom (f ≫ g)) x ∈ U✝
⊢ ((pushforward C (f ≫ g)).obj ℱ).germ U✝ ((ConcreteCategory.hom (f ≫ g)) x) hxU✝ ≫ stalkPushforward C (f ≫ g) ℱ x =
    ((pushforward C (f ≫ g)).obj ℱ).germ U✝ ((ConcreteCategory.hom (f ≫ g)) x) hxU✝ ≫
      stalkPushforward C g ((pushforward C f).obj ℱ) ((ConcreteCategory.hom f) x) ≫ stalkPushforward C f ℱ x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_toList_iff (a : α) (v : Vector α n) : a ∈ v.toList ↔ a ∈ v

Proof state:
α : Type u_1
n : Nat
a : α
v : Vector α n
⊢ a ∈ v.toList ↔ a ∈ v

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Trace.lean
lemma trace_submatrix_succ {n : ℕ} [NonUnitalNonAssocSemiring R]
    (M : Matrix (Fin n.succ) (Fin n.succ) R) :
    M 0 0 + trace (submatrix M Fin.succ Fin.succ) = trace M

Proof state:
R : Type u_6
n : ℕ
inst✝ : NonUnitalNonAssocSemiring R
M : Matrix (Fin n.succ) (Fin n.succ) R
⊢ M 0 0 + (M.submatrix Fin.succ Fin.succ).trace = M.trace

Tactic:
delta trace

Result:
R : Type u_6
n : ℕ
inst✝ : NonUnitalNonAssocSemiring R
M : Matrix (Fin n.succ) (Fin n.succ) R
⊢ M 0 0 + ∑ i : Fin n, (M.submatrix Fin.succ Fin.succ).diag i = ∑ i : Fin n.succ, M.diag i

Proof state:
R : Type u_6
n : ℕ
inst✝ : NonUnitalNonAssocSemiring R
M : Matrix (Fin n.succ) (Fin n.succ) R
⊢ M 0 0 + ∑ i : Fin n, (M.submatrix Fin.succ Fin.succ).diag i = ∑ i : Fin n.succ, M.diag i

Tactic:
rw [← (finSuccEquiv n).symm.sum_comp]

Result:
R : Type u_6
n : ℕ
inst✝ : NonUnitalNonAssocSemiring R
M : Matrix (Fin n.succ) (Fin n.succ) R
⊢ M 0 0 + ∑ i : Fin n, (M.submatrix Fin.succ Fin.succ).diag i = ∑ i : Option (Fin n), M.diag ((finSuccEquiv n).symm i)

Proof state:
R : Type u_6
n : ℕ
inst✝ : NonUnitalNonAssocSemiring R
M : Matrix (Fin n.succ) (Fin n.succ) R
⊢ M 0 0 + ∑ i : Fin n, (M.submatrix Fin.succ Fin.succ).diag i = ∑ i : Option (Fin n), M.diag ((finSuccEquiv n).symm i)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/LeftRight.lean
theorem continuousAt_iff_continuous_left_right {a : α} {f : α → β} :
    ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a

Tactic:
simp only [ContinuousWithinAt, ContinuousAt, ← tendsto_sup, nhdsLE_sup_nhdsGE]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
/-- "iff" version of `Multipliable.of_nat_of_neg`. -/
@[to_additive "\"iff\" version of `Summable.of_nat_of_neg`."]
lemma multipliable_int_iff_multipliable_nat_and_neg {f : ℤ → G} :
    Multipliable f ↔ (Multipliable fun n : ℕ ↦ f n) ∧ (Multipliable fun n : ℕ ↦ f (-n))

Proof state:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
⊢ Multipliable f ↔ (Multipliable fun n => f ↑n) ∧ Multipliable fun n => f (-↑n)

Tactic:
refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg hf₁ hf₂⟩ <;>
apply p.comp_injective

Result:
case refine_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Injective Nat.cast

case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Injective fun n => -↑n

Proof state:
case refine_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Injective Nat.cast

case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Injective fun n => -↑n

Tactic:
exacts [Nat.cast_injective, neg_injective.comp Nat.cast_injective]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sub_eq_oangle_sub_rev_of_norm_eq {x y : V} (h : ‖x‖ = ‖y‖) :
    o.oangle x (x - y) = o.oangle (y - 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
h : ‖x‖ = ‖y‖
⊢ o.oangle x (x - y) = o.oangle (y - x) y

Tactic:
simp [oangle, h]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem mul_imJ : (a * b).imJ = a.re * b.imJ - a.imI * b.imK + a.imJ * b.re + a.imK * b.imI :=
  (QuaternionAlgebra.mul_imJ a b).trans <| by ring

Proof state:
R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ a.re * b.imJ + -1 * a.imI * b.imK + a.imJ * b.re + 0 * a.imJ * b.imI - -1 * a.imK * b.imI =
    a.re * b.imJ - a.imI * b.imK + a.imJ * b.re + a.imK * b.imI

Tactic:
ring

Result:
no goals