harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Quaternion.lean
theorem norm_coe (a : ℝ) : ‖(a : ℍ)‖ = ‖a‖

Proof state:
a : ℝ
⊢ ‖↑a‖ = ‖a‖

Tactic:
rw [norm_eq_sqrt_real_inner, inner_self, normSq_coe, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrix_algebraMap (x : R) :
    LinearMap.toMatrix v₁ v₁ (algebraMap R (Module.End R M₁) x) = scalar n x

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
x : R
⊢ (toMatrix v₁ v₁) ((algebraMap R (Module.End R M₁)) x) = (scalar n) x

Tactic:
simp [Module.algebraMap_end_eq_smul_id, LinearMap.toMatrix_id, smul_eq_diagonal_mul]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem le_add_left (a b : Ordinal) : a ≤ b + a

Proof state:
a b : Ordinal.{u_1}
⊢ a ≤ b + a

Tactic:
simpa only [zero_add] using add_le_add_right (Ordinal.zero_le b) a

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem findSomeRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
    l.toArray.findSomeRevM? f = l.reverse.findSomeM? f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
l : List α
⊢ findSomeRevM? f l.toArray = findSomeM? f l.reverse

Tactic:
simp [Array.findSomeRevM?, findSomeRevM?_find_toArray]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Basic.lean
theorem id_comp (F : C ⥤ D) : 𝟭 C ⋙ F = F

Proof state:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
toPrefunctor✝ : C ⥤q D
map_id✝ : ∀ (X : C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ 𝟭 C ⋙ { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ } =
    { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
⊢ 𝟭 C ⋙ F = F

Tactic:
cases F

Result:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
toPrefunctor✝ : C ⥤q D
map_id✝ : ∀ (X : C), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ 𝟭 C ⋙ { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ } =
    { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
@[gcongr] lemma vcDim_mono (h𝒜ℬ : 𝒜 ⊆ ℬ) : 𝒜.vcDim ≤ ℬ.vcDim

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜ℬ : 𝒜 ⊆ ℬ
⊢ 𝒜.vcDim ≤ ℬ.vcDim

Tactic:
unfold vcDim

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜ℬ : 𝒜 ⊆ ℬ
⊢ 𝒜.shatterer.sup card ≤ ℬ.shatterer.sup card

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜ℬ : 𝒜 ⊆ ℬ
⊢ 𝒜.shatterer.sup card ≤ ℬ.shatterer.sup card

Tactic:
gcongr

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_lt_pred_iff_of_not_isMin (ha : ¬IsMin a) (hb : ¬IsMin b) :
    pred a < pred b ↔ a < b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
hb : ¬IsMin b
⊢ pred a < pred b ↔ a < b

Tactic:
rw [pred_lt_iff_of_not_isMin ha, le_pred_iff_of_not_isMin hb]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Root.lean
@[simp] lemma ceilRoot_one_right (hn : n ≠ 0) : ceilRoot n 1 = 1

Proof state:
n : ℕ
hn : n ≠ 0
⊢ n.ceilRoot 1 = 1

Tactic:
simp [ceilRoot, hn]

Result:
no goals
-- Mathlib/RingTheory/EisensteinCriterion.lean
theorem eval_zero_mem_ideal_of_eq_mul_X_pow {n : ℕ} {P : Ideal R} {q : R[X]}
    {c : Polynomial (R ⧸ P)} (hq : map (mk P) q = c * X ^ n) (hn0 : n ≠ 0) : eval 0 q ∈ P

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
P : Ideal R
q : R[X]
c : (R ⧸ P)[X]
hq : map (mk P) q = c * X ^ n
hn0 : n ≠ 0
⊢ eval 0 q ∈ P

Tactic:
rw [← coeff_zero_eq_eval_zero, ← eq_zero_iff_mem, ← coeff_map, hq,
  coeff_zero_eq_eval_zero, eval_mul, eval_pow, eval_X, zero_pow hn0, mul_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem isNone_getElem? {l : List α} {i : Nat} : l[i]?.isNone ↔ l.length ≤ i

Proof state:
α : Type u_1
l : List α
i : Nat
⊢ l[i]?.isNone = true ↔ l.length ≤ i

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem sup_right_idem (a b : α) : a ⊔ b ⊔ b = a ⊔ b

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ⊔ b ⊔ b = a ⊔ b

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem sub (hf : IsBoundedLinearMap 𝕜 f) (hg : IsBoundedLinearMap 𝕜 g) :
    IsBoundedLinearMap 𝕜 fun e => f e - g e

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
hg : IsBoundedLinearMap 𝕜 g
⊢ IsBoundedLinearMap 𝕜 fun e => f e - g e

Tactic:
simpa [sub_eq_add_neg] using add hf (neg hg)

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iUnion_Ioo_right [NoMaxOrder α] (a : α) : ⋃ b, Ioo a b = Ioi a

Proof state:
α : Type v
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
⊢ ⋃ b, Ioo a b = Ioi a

Tactic:
simp only [← Ioi_inter_Iio, ← inter_iUnion, iUnion_Iio, inter_univ]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem prod_eq_sup_map (p : Submodule R M) (q : Submodule R M₂) :
    p.prod q = p.map (LinearMap.inl R M M₂) ⊔ q.map (LinearMap.inr R M M₂)

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ p.prod q = map (inl R M M₂) p ⊔ map (inr R M M₂) q

Tactic:
rw [← map_coprod_prod, coprod_inl_inr, map_id]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedTotalDegree'_zero (w : σ → M) :
    weightedTotalDegree' w (0 : MvPolynomial σ R) = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : SemilatticeSup M
w : σ → M
⊢ weightedTotalDegree' w 0 = ⊥

Tactic:
simp only [weightedTotalDegree', support_zero, Finset.sup_empty]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem sigmaFinite {f : α → β} (hf : MeasurePreserving f μa μb) [SigmaFinite μb] :
    SigmaFinite μa :=
  SigmaFinite.of_map μa hf.aemeasurable (by rwa [hf.map_eq])

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
inst✝ : SigmaFinite μb
⊢ SigmaFinite (map f μa)

Tactic:
rwa [hf.map_eq]

Result:
no goals
-- Mathlib/Topology/UnitInterval.lean
theorem symm_zero : σ 0 = 1 :=
  Subtype.ext <| by simp [symm]

Proof state:
⊢ ↑(σ 0) = ↑1

Tactic:
simp [symm]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem coe_πs' {o₁ o₂ : Ordinal} (h : o₁ ≤ o₂) (f : LocallyConstant (π C (ord I · < o₁)) ℤ) :
    (πs' C h f).toFun = f.toFun ∘ (ProjRestricts C (fun _ hh ↦ lt_of_lt_of_le hh h))

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
f : LocallyConstant ↑(π C fun x => ord I x < o₁) ℤ
⊢ ((πs' C h) f).toFun = f.toFun ∘ ProjRestricts C ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem card_fintypeIic : Fintype.card (Set.Iic b) = b + 1

Proof state:
b : ℕ
⊢ Fintype.card ↑(Set.Iic b) = b + 1

Tactic:
rw [Fintype.card_ofFinset, card_Iic]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Perm.lean
theorem swap_perm {as : Array α} {i j : Nat} (h₁ : i < as.size) (h₂ : j < as.size) :
    as.swap i j ~ as

Proof state:
α : Type u_1
as : Array α
i j : Nat
h₁ : i < as.size
h₂ : j < as.size
⊢ (as.toList.set i as[j]).set j as[i] ~ as.toList

Tactic:
apply set_set_perm

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i j : Nat
h₁ : i < as.size
h₂ : j < as.size
⊢ as.swap i j h₁ h₂ ~ as

Tactic:
simp only [swap, perm_iff_toList_perm, toList_set]

Result:
α : Type u_1
as : Array α
i j : Nat
h₁ : i < as.size
h₂ : j < as.size
⊢ (as.toList.set i as[j]).set j as[i] ~ as.toList
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem kerLiftAlg_mk (f : A →ₐ[R₁] B) (a : A) :
    kerLiftAlg f (Quotient.mk (RingHom.ker f) a) = f a

Proof state:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
a : A
⊢ (kerLiftAlg f) ((Quotient.mk (ker f)) a) = f a

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem tan_eq_of_two_zsmul_eq {θ ψ : Angle} (h : (2 : ℤ) • θ = (2 : ℤ) • ψ) : tan θ = tan ψ

Proof state:
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ θ.tan = ψ.tan

Tactic:
exact tan_eq_of_two_nsmul_eq h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem lift_comp_conePointUniqueUpToIso_hom {r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) :
    P.lift r ≫ (conePointUniqueUpToIso P Q).hom = Q.lift r :=
  Q.uniq _ _ (by simp)

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
r s t : Cone F
P : IsLimit s
Q : IsLimit t
⊢ ∀ (j : J), (P.lift r ≫ (P.conePointUniqueUpToIso Q).hom) ≫ t.π.app j = r.π.app j

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem some_eq_dite_none_right {p : Prop} [Decidable p] {b : p → Option α} :
    some a = (if h : p then b h else none) ↔ ∃ h, some a = b h

Proof state:
α : Type u_1
a : α
p : Prop
inst✝ : Decidable p
b : p → Option α
⊢ (some a = if h : p then b h else none) ↔ ∃ h, some a = b h

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJ_1728_of_three_eq_zero (h3 : (3 : F) = 0) : ofJ 1728 = ofJ1728 F

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h3 : 3 = 0
⊢ ofJ 1728 = ofJ1728 F

Tactic:
rw [ofJ, if_pos (by linear_combination 576 * h3), if_pos h3]

Result:
no goals

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h3 : 3 = 0
⊢ 1728 = 0

Tactic:
linear_combination 576 * h3

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem truncateFun_mul (x y : 𝕎 R) :
    truncateFun n (x * y) = truncateFun n x * truncateFun n y

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ truncateFun n (x * y) = truncateFun n x * truncateFun n y

Tactic:
witt_truncateFun_tac

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
/-- `t` is in the shadow of `𝒜` iff there is a `s ∈ 𝒜` from which we can remove one element to
get `t`. -/
lemma mem_shadow_iff : t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∈ s, erase s a = t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∈ s, s.erase a = t

Tactic:
simp only [shadow, mem_sup, mem_image]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem UniformCauchySeqOn.uniformCauchySeqOnFilter (hF : UniformCauchySeqOn F p s) :
    UniformCauchySeqOnFilter F p (𝓟 s)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
hF : UniformCauchySeqOn F p s
⊢ UniformCauchySeqOnFilter F p (𝓟 s)

Tactic:
rwa [← uniformCauchySeqOn_iff_uniformCauchySeqOnFilter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem lt_asymm : ∀ {x y : Bool}, x < y → ¬ y < x

Proof state:
⊢ ∀ {x y : Bool}, x < y → ¬y < x

Tactic:
decide

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ioc_self : Ioc a a = 0

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Ioc a a = 0

Tactic:
rw [Ioc, Finset.Ioc_self, Finset.empty_val]

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem isOpen_image_coe {s : Set X} : IsOpen ((↑) '' s : Set (OnePoint X)) ↔ IsOpen s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsOpen (some '' s) ↔ IsOpen s

Tactic:
rw [isOpen_iff_of_not_mem infty_not_mem_image_coe, preimage_image_eq _ coe_injective]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem eval_comp
    {η η' : f ⟶ g} {θ θ' : g ⟶ h} {ι : f ⟶ h}
    (e_η : η = η') (e_θ : θ = θ') (e_ηθ : η' ≫ θ' = ι) :
    η ≫ θ = ι

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g h : a ⟶ b
η η' : f ⟶ g
θ θ' : g ⟶ h
ι : f ⟶ h
e_η : η = η'
e_θ : θ = θ'
e_ηθ : η' ≫ θ' = ι
⊢ η ≫ θ = ι

Tactic:
simp [e_η, e_θ, e_ηθ]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_right_differentiableAt_iff {f : F → G} {x : E} :
    DifferentiableAt 𝕜 (f ∘ iso) x ↔ DifferentiableAt 𝕜 f (iso x)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
x : E
⊢ DifferentiableAt 𝕜 (f ∘ ⇑iso) x ↔ DifferentiableAt 𝕜 f (iso x)

Tactic:
simp only [← differentiableWithinAt_univ, ← iso.comp_right_differentiableWithinAt_iff,
  preimage_univ]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem dense_iff {s : Set α} : Dense s ↔ ∀ x, ∀ r > 0, (ball x r ∩ s).Nonempty :=
  forall_congr' fun x => by
    simp only [mem_closure_iff, Set.Nonempty, exists_prop, mem_inter_iff, mem_ball', and_comm]

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ x ∈ closure s ↔ ∀ r > 0, (ball x r ∩ s).Nonempty

Tactic:
simp only [mem_closure_iff, Set.Nonempty, exists_prop, mem_inter_iff, mem_ball', and_comm]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma setIntegral_stieltjesOfMeasurableRat_rat (hf : IsRatCondKernelCDF f κ ν) (a : α) (q : ℚ)
    {s : Set β} (hs : MeasurableSet s) :
    ∫ b in s, stieltjesOfMeasurableRat f hf.measurable (a, b) q ∂(ν a)
      = (κ a (s ×ˢ Iic (q : ℝ))).toReal

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ ∀ᵐ (x : β) ∂ν a, x ∈ s → ↑(stieltjesOfMeasurableRat f ⋯ (a, x)) ↑q = (fun b => f (a, b) q) x

Tactic:
filter_upwards [stieltjesOfMeasurableRat_ae_eq hf a q] with b hb using fun _ ↦ hb

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ ∫ (b : β) in s, ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q ∂ν a = ((κ a) (s ×ˢ Iic ↑q)).toReal

Tactic:
rw [setIntegral_congr_ae hs (g := fun b ↦ f (a, b) q) ?_, hf.setIntegral a hs]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ ∀ᵐ (x : β) ∂ν a, x ∈ s → ↑(stieltjesOfMeasurableRat f ⋯ (a, x)) ↑q = (fun b => f (a, b) q) x
-- Mathlib/LinearAlgebra/AffineSpace/Slope.lean
theorem slope_same (f : k → PE) (a : k) : (slope f a a : E) = 0

Proof state:
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a : k
⊢ slope f a a = 0

Tactic:
rw [slope, sub_self, inv_zero, zero_smul]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Defs.lean
theorem mk_eq_localization_mk (p : K[X]) {q : K[X]} (hq : q ≠ 0) :
    RatFunc.mk p q =
      ofFractionRing (Localization.mk p ⟨q, mem_nonZeroDivisors_iff_ne_zero.mpr hq⟩)

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q : K[X]
hq : q ≠ 0
⊢ RatFunc.mk p q = { toFractionRing := Localization.mk p ⟨q, ⋯⟩ }

Tactic:
rw [mk_def_of_ne _ hq, Localization.mk_eq_mk']

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuousAt_iInf_rng {u : κ → UniformSpace α'} {F : ι → X → α'}
    {x₀ : X} :
    EquicontinuousAt (uα := ⨅ k, u k) F x₀ ↔ ∀ k, EquicontinuousAt (uα := u k) F x₀

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ ∀ (k : κ), EquicontinuousAt F x₀

Tactic:
simp only [← equicontinuousWithinAt_univ (uα := _), equicontinuousWithinAt_iInf_rng]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_sUnion_congr {S : Set (Set α)} (hc : S.Countable) :
    μ.restrict (⋃₀ S) = ν.restrict (⋃₀ S) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S : Set (Set α)
hc : S.Countable
⊢ μ.restrict (⋃₀ S) = ν.restrict (⋃₀ S) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s

Tactic:
rw [sUnion_eq_biUnion, restrict_biUnion_congr hc]

Result:
no goals
-- Mathlib/Algebra/Category/MonCat/Basic.lean
@[to_additive]
lemma hom_inv_apply {M N : MonCat} (e : M ≅ N) (s : N) : e.hom (e.inv s) = s

Proof state:
M N : MonCat
e : M ≅ N
s : ↑N
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
lemma prop.succ_eq {X Y : C} {f : X ⟶ Y} (hf : Φ.prop f) :
    Φ.succ X = Y

Proof state:
case mk
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X : C
⊢ Φ.succ X = Φ.succ X

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
hf : Φ.prop f
⊢ Φ.succ X = Y

Tactic:
cases hf

Result:
case mk
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X : C
⊢ Φ.succ X = Φ.succ X
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem measure_preimage_mul_right (μ : Measure G) [IsMulRightInvariant μ] (g : G) (A : Set G) :
    μ ((fun h => h * g) ⁻¹' A) = μ A :=
  calc
    μ ((fun h => h * g) ⁻¹' A) = map (fun h => h * g) μ A :=
      ((MeasurableEquiv.mulRight g).map_apply A).symm
    _ = μ A

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
A : Set G
⊢ (Measure.map (fun h => h * g) μ) A = μ A

Tactic:
rw [map_mul_right_eq_self μ g]

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem mem_replace {a a' : α} {b : β a} {s : AList β} : a' ∈ replace a b s ↔ a' ∈ s

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s : AList β
⊢ a' ∈ replace a b s ↔ a' ∈ s

Tactic:
rw [mem_keys, keys_replace, ← mem_keys]

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Pi.lean
@[simp] lemma piAntidiag_zero (s : Finset ι) : piAntidiag s (0 : μ) = {0}

Proof state:
case h
ι : Type u_1
μ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : OrderedAddCommMonoid μ
inst✝² : CanonicallyOrderedAdd μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
a✝ : ι → μ
⊢ a✝ ∈ s.piAntidiag 0 ↔ a✝ ∈ {0}

Tactic:
simp [Fintype.sum_eq_zero_iff_of_nonneg, funext_iff, not_imp_comm, ← forall_and]

Result:
no goals

Proof state:
ι : Type u_1
μ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : OrderedAddCommMonoid μ
inst✝² : CanonicallyOrderedAdd μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
⊢ s.piAntidiag 0 = {0}

Tactic:
ext

Result:
case h
ι : Type u_1
μ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : OrderedAddCommMonoid μ
inst✝² : CanonicallyOrderedAdd μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
a✝ : ι → μ
⊢ a✝ ∈ s.piAntidiag 0 ↔ a✝ ∈ {0}
-- Mathlib/Data/Real/GoldenRatio.lean
theorem geom_gold_isSol_fibRec : fibRec.IsSolution (φ ^ ·)

Proof state:
⊢ (X ^ 2 - (X + 1)).IsRoot φ

Tactic:
simp [sub_eq_zero]

Result:
no goals

Proof state:
⊢ fibRec.IsSolution fun x => φ ^ x

Tactic:
rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]

Result:
⊢ (X ^ 2 - (X + 1)).IsRoot φ
-- Mathlib/Data/Set/NAry.lean
theorem image2_union_left : image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
⊢ image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t

Tactic:
simp_rw [← image_prod, union_prod, image_union]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Finset.lean
@[simp, norm_cast]
lemma cast_finsetSup [CanonicallyOrderedAdd R] (s : Finset ι) (f : ι → ℕ) :
    (↑(s.sup f) : R) = s.sup fun i ↦ (f i : R) :=
  comp_sup_eq_sup_comp _ cast_max (by simp)

Proof state:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedSemiring R
inst✝ : CanonicallyOrderedAdd R
s : Finset ι
f : ι → ℕ
⊢ ↑⊥ = ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem mem_compPartialSumSource_iff (m M N : ℕ) (i : Σ n, Fin n → ℕ) :
    i ∈ compPartialSumSource m M N ↔
      (m ≤ i.1 ∧ i.1 < M) ∧ ∀ a : Fin i.1, 1 ≤ i.2 a ∧ i.2 a < N

Proof state:
m M N : ℕ
i : (n : ℕ) × (Fin n → ℕ)
⊢ i ∈ compPartialSumSource m M N ↔ (m ≤ i.fst ∧ i.fst < M) ∧ ∀ (a : Fin i.fst), 1 ≤ i.snd a ∧ i.snd a < N

Tactic:
simp only [compPartialSumSource, Finset.mem_Ico, Fintype.mem_piFinset, Finset.mem_sigma]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_alterKey [EquivBEq α] [Inhabited α] {k k' : α} {f : Option β → Option β}
    (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
    getKey! k' (alterKey k f l) =
      if k == k' then
        if (f (getValue? k l)).isSome then k else default
      else
        getKey! k' l

Proof state:
α : Type u
inst✝² : BEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getKey! k' (alterKey k f l) =
    if (k == k') = true then if (f (getValue? k l)).isSome = true then k else default else getKey! k' l

Tactic:
simp [hl, getKey!_eq_getKey?, getKey?_alterKey, apply_ite Option.get!]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma isIso_homologyMap_of_epi_of_isIso_of_mono' (φ : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology]
    (h₁ : Epi φ.τ₁) (h₂ : IsIso φ.τ₂) (h₃ : Mono φ.τ₃) :
    IsIso (homologyMap φ)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : Epi φ.τ₁
h₂ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
⊢ IsIso (homologyMap φ)

Tactic:
dsimp only [homologyMap]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : Epi φ.τ₁
h₂ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
⊢ IsIso (homologyMap' φ S₁.homologyData S₂.homologyData)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : Epi φ.τ₁
h₂ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
⊢ IsIso (homologyMap' φ S₁.homologyData S₂.homologyData)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Order/Height.lean
theorem singleton_mem_subchain_iff : [a] ∈ s.subchain ↔ a ∈ s

Proof state:
α : Type u_1
inst✝ : LT α
s : Set α
a : α
⊢ [a] ∈ s.subchain ↔ a ∈ s

Tactic:
simp [cons_mem_subchain_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem ne_zero_of_trailingDegree_lt {n : ℕ∞} (h : trailingDegree p < n) : p ≠ 0 := fun h₀ =>
  h.not_le (by simp [h₀])

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ∞
h : p.trailingDegree < n
h₀ : p = 0
⊢ n ≤ p.trailingDegree

Tactic:
simp [h₀]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem map_bind (m : Multiset α) (n : α → Multiset β) (f : β → γ) :
    map f (bind m n) = bind m fun a => map f (n a)

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : α → Multiset β
f : β → γ
⊢ map f (m.bind n) = m.bind fun a => map f (n a)

Tactic:
simp [bind]

Result:
no goals