harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_eq_mul_tprod_ite' [DecidableEq β] {f : β → α} (b : β)
    (hf : Multipliable (update f b 1)) :
    ∏' x, f x = f b * ∏' x, ite (x = b) 1 (f x) :=
  calc
    ∏' x, f x = ∏' x, (ite (x = b) (f x) 1 * update f b 1 x) :=
      tprod_congr fun n ↦ by split_ifs with h <;> simp [update_apply, h]
    _ = (∏' x, ite (x = b) (f x) 1) * ∏' x, update f b 1 x :=
      tprod_mul ⟨ite (b = b) (f b) 1, hasProd_single b fun _ hb ↦ if_neg hb⟩ hf
    _ = ite (b = b) (f b) 1 * ∏' x, update f b 1 x

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
b : β
hf : Multipliable (update f b 1)
⊢ (∏' (x : β), if x = b then f x else 1) * ∏' (x : β), update f b 1 x =
    (if b = b then f b else 1) * ∏' (x : β), update f b 1 x

Tactic:
congr

Result:
case e_a
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
b : β
hf : Multipliable (update f b 1)
⊢ (∏' (x : β), if x = b then f x else 1) = if b = b then f b else 1

Proof state:
case e_a
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
b : β
hf : Multipliable (update f b 1)
⊢ (∏' (x : β), if x = b then f x else 1) = if b = b then f b else 1

Tactic:
exact tprod_eq_mulSingle b fun b' hb' ↦ if_neg hb'

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
b : β
hf : Multipliable (update f b 1)
⊢ (if b = b then f b else 1) * ∏' (x : β), update f b 1 x = f b * ∏' (x : β), if x = b then 1 else f x

Tactic:
simp only [update, eq_self_iff_true, if_true, eq_rec_constant, dite_eq_ite]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
b : β
hf : Multipliable (update f b 1)
n : β
⊢ f n = (if n = b then f n else 1) * update f b 1 n

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

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_empty {a : α} {c} : get? (empty c : Raw₀ α (fun _ => β)) a = none

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
a : α
c : Nat
⊢ get? (empty c) a = none

Tactic:
simp [get?]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem Subgroup.isCyclic_iff_exists_zpowers_eq_top [Group α] (H : Subgroup α) :
    IsCyclic H ↔ ∃ g : α, Subgroup.zpowers g = H

Proof state:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ IsCyclic ↥H ↔ ∃ g, zpowers g = H

Tactic:
rw [isCyclic_iff_exists_zpowers_eq_top]

Result:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ g, zpowers g = ⊤) ↔ ∃ g, zpowers g = H

Proof state:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ a ∈ H, zpowers a = H) ↔ ∃ g, zpowers g = H

Tactic:
exact exists_congr fun g ↦ and_iff_right_of_imp fun h ↦ h ▸ mem_zpowers g

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ g, zpowers g = ⊤) ↔ ∃ g, zpowers g = H

Tactic:
simp_rw [← (map_injective H.subtype_injective).eq_iff, ← MonoidHom.range_eq_map,
  H.range_subtype, MonoidHom.map_zpowers, Subtype.exists, coe_subtype, exists_prop]

Result:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ (∃ a ∈ H, zpowers a = H) ↔ ∃ g, zpowers g = H
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem HasCodetector.hasDetector_of_hasCodetector_op [HasCodetector Cᵒᵖ] :
    HasDetector C

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasCodetector Cᵒᵖ
⊢ HasDetector C

Tactic:
simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/SModEq.lean
theorem smul (hxy : x ≡ y [SMOD U]) (c : R) : c • x ≡ c • y [SMOD U]

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : x ≡ y [SMOD U]
c : R
⊢ c • x ≡ c • y [SMOD U]

Tactic:
rw [SModEq.def] at hxy ⊢

Result:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : Submodule.Quotient.mk x = Submodule.Quotient.mk y
c : R
⊢ Submodule.Quotient.mk (c • x) = Submodule.Quotient.mk (c • y)

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : Submodule.Quotient.mk x = Submodule.Quotient.mk y
c : R
⊢ Submodule.Quotient.mk (c • x) = Submodule.Quotient.mk (c • y)

Tactic:
simp_rw [Quotient.mk_smul, hxy]

Result:
no goals
-- Mathlib/Analysis/Complex/CauchyIntegral.lean
theorem analyticOnNhd_univ_iff_differentiable {f : ℂ → E} :
    AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
⊢ AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f

Tactic:
simp only [← differentiableOn_univ]

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
⊢ AnalyticOnNhd ℂ f univ ↔ DifferentiableOn ℂ f univ

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
⊢ AnalyticOnNhd ℂ f univ ↔ DifferentiableOn ℂ f univ

Tactic:
exact analyticOnNhd_iff_differentiableOn isOpen_univ

Result:
no goals
-- Mathlib/Topology/UniformSpace/Ascoli.lean
/-- Let `X` be a compact topological space, `α` a uniform space, and `F : ι → (X → α)` an
equicontinuous family. Then, the uniform structures of uniform convergence and pointwise
convergence induce the same uniform structure on `ι`.

In other words, pointwise convergence and uniform convergence coincide on an equicontinuous
subset of `X → α`.

This is a version of `Equicontinuous.comap_uniformFun_eq` stated in terms of `IsUniformInducing`
for convenuence. -/
lemma Equicontinuous.isUniformInducing_uniformFun_iff_pi [UniformSpace ι] [CompactSpace X]
    (F_eqcont : Equicontinuous F) :
    IsUniformInducing (UniformFun.ofFun ∘ F) ↔ IsUniformInducing F

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : UniformSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ UniformSpace.comap (⇑UniformFun.ofFun ∘ F) (UniformFun.uniformSpace X α) = inst✝¹ ↔
    UniformSpace.comap F (UniformFun.uniformSpace X α) = inst✝¹

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : UniformSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ IsUniformInducing (⇑UniformFun.ofFun ∘ F) ↔ IsUniformInducing F

Tactic:
rw [isUniformInducing_iff_uniformSpace, isUniformInducing_iff_uniformSpace,
    ← F_eqcont.comap_uniformFun_eq]

Result:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : UniformSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ UniformSpace.comap (⇑UniformFun.ofFun ∘ F) (UniformFun.uniformSpace X α) = inst✝¹ ↔
    UniformSpace.comap F (UniformFun.uniformSpace X α) = inst✝¹
-- Mathlib/RingTheory/Derivation/MapCoeffs.lean
@[simp]
lemma implicitDeriv_X (v : A[X]) :
    implicitDeriv v X = v

Proof state:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
v : A[X]
⊢ (implicitDeriv v) X = v

Tactic:
simp [implicitDeriv]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem inCoordinates_tangent_bundle_core_model_space (x₀ x : H) (y₀ y : H') (ϕ : E →L[𝕜] E') :
    inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x y₀ y ϕ = ϕ

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x y₀ y ϕ = ϕ

Tactic:
erw [VectorBundleCore.inCoordinates_eq] <;> try trivial

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ ((tangentBundleCore I' H').coordChange ((tangentBundleCore I' H').indexAt y) ((tangentBundleCore I' H').indexAt y₀)
          y).comp
      (ϕ.comp
        ((tangentBundleCore I H).coordChange ((tangentBundleCore I H).indexAt x₀) ((tangentBundleCore I H).indexAt x)
          x)) =
    ϕ

Proof state:
case hy
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ y ∈ (tangentBundleCore I' H').baseSet ((tangentBundleCore I' H').indexAt y₀)

Tactic:
trivial

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
x₀ x : H
y₀ y : H'
ϕ : E →L[𝕜] E'
⊢ ((tangentBundleCore I' H').coordChange ((tangentBundleCore I' H').indexAt y) ((tangentBundleCore I' H').indexAt y₀)
          y).comp
      (ϕ.comp
        ((tangentBundleCore I H).coordChange ((tangentBundleCore I H).indexAt x₀) ((tangentBundleCore I H).indexAt x)
          x)) =
    ϕ

Tactic:
simp_rw [tangentBundleCore_indexAt, tangentBundleCore_coordChange_model_space,
  ContinuousLinearMap.id_comp, ContinuousLinearMap.comp_id]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Prod.lean
theorem isPrime_of_isPrime_prod_top' {I : Ideal S} (h : (Ideal.prod (⊤ : Ideal R) I).IsPrime) :
    I.IsPrime

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal S
h : (⊤.prod I).IsPrime
⊢ (I.prod ⊤).IsPrime

Tactic:
rw [← map_prodComm_prod]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal S
h : (⊤.prod I).IsPrime
⊢ (map (↑RingEquiv.prodComm) (⊤.prod I)).IsPrime

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal S
h : (⊤.prod I).IsPrime
⊢ (map (↑RingEquiv.prodComm) (⊤.prod I)).IsPrime

Tactic:
exact map_isPrime_of_equiv (RingEquiv.prodComm (R := R) (S := S))

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal S
h : (⊤.prod I).IsPrime
⊢ I.IsPrime

Tactic:
apply isPrime_of_isPrime_prod_top (S := R)

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal S
h : (⊤.prod I).IsPrime
⊢ (I.prod ⊤).IsPrime
-- Mathlib/Logic/Equiv/Defs.lean
theorem apply_eq_iff_eq_symm_apply {x : α} {y : β} (f : α ≃ β) : f x = y ↔ x = f.symm y

Proof state:
α : Sort u
β : Sort v
x : α
y : β
f : α ≃ β
⊢ f x = f (f.symm y) ↔ x = f.symm y

Tactic:
rw [apply_eq_iff_eq]

Result:
no goals

Proof state:
α : Sort u
β : Sort v
x : α
y : β
f : α ≃ β
⊢ f x = y ↔ x = f.symm y

Tactic:
conv_lhs => rw [← apply_symm_apply f y]

Result:
α : Sort u
β : Sort v
x : α
y : β
f : α ≃ β
⊢ f x = f (f.symm y) ↔ x = f.symm y
-- Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
lemma map_id (i : J) (hi : i ≤ j) :
    map c i i (by rfl) hi = 𝟙 _

Proof state:
case inl
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i ≤ j
hi' : i < j
⊢ (if h₂ : i < j then (objIso c i ⋯).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso c i h₂).inv
    else if h₁ : i < j then (objIso c i h₁).hom ≫ c.ι.app ⟨i, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else 𝟙 (obj c i)) =
    𝟙 (obj c i)

Tactic:
rw [dif_pos hi', F.map_id, id_comp, Iso.hom_inv_id]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
i : J
F : ↑(Set.Iio i) ⥤ C
c : Cocone F
hi : i ≤ i
⊢ ¬i < i

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i ≤ j
⊢ map c i i ⋯ hi = 𝟙 (obj c i)

Tactic:
dsimp [map]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i ≤ j
⊢ (if h₂ : i < j then (objIso c i ⋯).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso c i h₂).inv
    else if h₁ : i < j then (objIso c i h₁).hom ≫ c.ι.app ⟨i, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else 𝟙 (obj c i)) =
    𝟙 (obj c i)

Proof state:
case inr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
i : J
F : ↑(Set.Iio i) ⥤ C
c : Cocone F
hi : i ≤ i
⊢ (if h₂ : i < i then (objIso c i ⋯).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso c i h₂).inv
    else if h₁ : i < i then (objIso c i h₁).hom ≫ c.ι.app ⟨i, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else 𝟙 (obj c i)) =
    𝟙 (obj c i)

Tactic:
rw [dif_neg (by simp), dif_neg (by simp)]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i ≤ j
⊢ (if h₂ : i < j then (objIso c i ⋯).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso c i h₂).inv
    else if h₁ : i < j then (objIso c i h₁).hom ≫ c.ι.app ⟨i, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else 𝟙 (obj c i)) =
    𝟙 (obj c i)

Tactic:
obtain hi' | rfl := hi.lt_or_eq

Result:
case inl
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i ≤ j
hi' : i < j
⊢ (if h₂ : i < j then (objIso c i ⋯).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso c i h₂).inv
    else if h₁ : i < j then (objIso c i h₁).hom ≫ c.ι.app ⟨i, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else 𝟙 (obj c i)) =
    𝟙 (obj c i)

case inr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
i : J
F : ↑(Set.Iio i) ⥤ C
c : Cocone F
hi : i ≤ i
⊢ (if h₂ : i < i then (objIso c i ⋯).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso c i h₂).inv
    else if h₁ : i < i then (objIso c i h₁).hom ≫ c.ι.app ⟨i, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom ⋯ else 𝟙 (obj c i)) =
    𝟙 (obj c i)

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.11878, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i ≤ j
⊢ i ≤ i

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
lemma expect_eq_zero_iff_of_nonneg [Nonempty ι] (hf : 0 ≤ f) : 𝔼 i, f i = 0 ↔ f = 0

Proof state:
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : OrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
f : ι → α
inst✝ : Nonempty ι
hf : 0 ≤ f
⊢ 𝔼 i : ι, f i = 0 ↔ f = 0

Tactic:
simp [expect, sum_eq_zero_iff_of_nonneg hf, univ_nonempty.ne_empty]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_one : (∏ᶠ _ : α, (1 : M)) = 1

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
x : PLift α
h : x ∈ mulSupport fun x => (fun x => 1) x.down
⊢ x ∈ ↑∅

Tactic:
simp at h

Result:
no goals

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
this : (mulSupport fun x => (fun x => 1) x.down) ⊆ ↑∅
⊢ ∏ᶠ (x : α), 1 = 1

Tactic:
rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_empty]

Result:
no goals

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
⊢ ∏ᶠ (x : α), 1 = 1

Tactic:
have : (mulSupport fun x : PLift α => (fun _ => 1 : α → M) x.down) ⊆ (∅ : Finset (PLift α)) :=
  fun x h => by simp at h

Result:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
this : (mulSupport fun x => (fun x => 1) x.down) ⊆ ↑∅
⊢ ∏ᶠ (x : α), 1 = 1
-- Mathlib/GroupTheory/PushoutI.lean
theorem lift_base (f : ∀ i, G i →* K) (k : H →* K)
    (hf : ∀ i, (f i).comp (φ i) = k)
    (g : H) : (lift f k hf) (base φ g : PushoutI φ) = k g

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
g : H
⊢ ((con φ).lift (Coprod.lift (CoprodI.lift f) k) ⋯) (((con φ).mk'.comp inr) g) = k g

Tactic:
simp only [MonoidHom.coe_comp, Con.coe_mk', comp_apply, Con.lift_coe, lift_apply_inr]

Result:
no goals

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
g : H
⊢ (lift f k hf) ((base φ) g) = k g

Tactic:
delta PushoutI lift base

Result:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
g : H
⊢ ((con φ).lift (Coprod.lift (CoprodI.lift f) k) ⋯) (((con φ).mk'.comp inr) g) = k g
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Pairwise.lean
theorem pairwise_iff_get {as : Array α} : as.Pairwise R ↔
    ∀ (i j : Fin as.size), i < j → R (as.get i i.2) (as.get j j.2)

Proof state:
α : Type u_1
R : α → α → Prop
as : Array α
⊢ Pairwise R as ↔ ∀ (i j : Fin as.size), i < j → R (as.get ↑i ⋯) (as.get ↑j ⋯)

Tactic:
unfold Pairwise

Result:
α : Type u_1
R : α → α → Prop
as : Array α
⊢ List.Pairwise R as.toList ↔ ∀ (i j : Fin as.size), i < j → R (as.get ↑i ⋯) (as.get ↑j ⋯)

Proof state:
α : Type u_1
R : α → α → Prop
as : Array α
⊢ List.Pairwise R as.toList ↔ ∀ (i j : Fin as.size), i < j → R (as.get ↑i ⋯) (as.get ↑j ⋯)

Tactic:
simp [List.pairwise_iff_get, getElem_fin_eq_getElem_toList]

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem Int.sq_ne_two_mod_four (z : ℤ) : z * z % 4 ≠ 2

Proof state:
z : ℤ
⊢ ¬z * z % ↑4 = 2 % ↑4

Tactic:
rw [← ZMod.intCast_eq_intCast_iff']

Result:
z : ℤ
⊢ ¬↑(z * z) = ↑2

Proof state:
z : ℤ
this : ¬z * z % ↑4 = 2 % ↑4
⊢ z * z % 4 ≠ 2

Tactic:
exact this

Result:
no goals

Proof state:
z : ℤ
⊢ z * z % 4 ≠ 2

Tactic:
suffices ¬z * z % (4 : ℕ) = 2 % (4 : ℕ) by exact this

Result:
z : ℤ
⊢ ¬z * z % ↑4 = 2 % ↑4

Proof state:
z : ℤ
⊢ ¬↑(z * z) = ↑2

Tactic:
simpa using sq_ne_two_fin_zmod_four _

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_preimage_linearMap {f : E →ₗ[ℝ] E} (hf : LinearMap.det f ≠ 0) (s : Set E) :
    μ (f ⁻¹' s) = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s :=
  calc
    μ (f ⁻¹' s) = Measure.map f μ s :=
      ((f.equivOfDetNeZero hf).toContinuousLinearEquiv.toHomeomorph.toMeasurableEquiv.map_apply
          s).symm
    _ = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
s : Set E
⊢ (ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ) s = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
s : Set E
⊢ (map (⇑f) μ) s = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s

Tactic:
rw [map_linearMap_addHaar_eq_smul_addHaar μ hf]

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
s : Set E
⊢ (ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ) s = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_moveRight_lt {x : PGame} (i : x.RightMoves) :
    (x.moveRight i).birthday < x.birthday

Proof state:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ ((mk α✝ β✝ a✝¹ a✝).moveRight i).birthday < (mk α✝ β✝ a✝¹ a✝).birthday

Tactic:
rw [birthday]

Result:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ ((mk α✝ β✝ a✝¹ a✝).moveRight i).birthday < (lsub fun i => (a✝¹ i).birthday) ⊔ lsub fun i => (a✝ i).birthday

Proof state:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ ((mk α✝ β✝ a✝¹ a✝).moveRight i).birthday < (lsub fun i => (a✝¹ i).birthday) ⊔ lsub fun i => (a✝ i).birthday

Tactic:
exact lt_max_of_lt_right (lt_lsub _ i)

Result:
no goals

Proof state:
x : PGame
i : x.RightMoves
⊢ (x.moveRight i).birthday < x.birthday

Tactic:
cases x

Result:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ ((mk α✝ β✝ a✝¹ a✝).moveRight i).birthday < (mk α✝ β✝ a✝¹ a✝).birthday
-- Mathlib/RingTheory/Noetherian/Defs.lean
theorem isNoetherian_iff :
    IsNoetherian R M ↔ WellFounded ((· > ·) : Submodule R M → Submodule R M → Prop)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ IsNoetherian R M ↔ WellFounded fun x1 x2 => x1 > x2

Tactic:
rw [isNoetherian_iff', ← isWellFounded_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma c₆_of_char_two : W.c₆ = W.a₁ ^ 6

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ -(W.a₁ ^ 2) ^ 3 + 36 * W.a₁ ^ 2 * W.b₄ - 216 * W.b₆ = W.a₁ ^ 6

Tactic:
linear_combination (18 * W.a₁ ^ 2 * W.b₄ - 108 * W.b₆ - W.a₁ ^ 6) * CharP.cast_eq_zero R 2

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.c₆ = W.a₁ ^ 6

Tactic:
rw [c₆, b₂_of_char_two]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ -(W.a₁ ^ 2) ^ 3 + 36 * W.a₁ ^ 2 * W.b₄ - 216 * W.b₆ = W.a₁ ^ 6
-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem hasseDeriv_one' : hasseDeriv 1 f = derivative f

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (hasseDeriv 1) f = derivative f

Tactic:
simp only [hasseDeriv_apply, derivative_apply, ← C_mul_X_pow_eq_monomial, Nat.choose_one_right,
  (Nat.cast_commute _ _).eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_alter [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} (h : m.WF) :
    k' ∈ m.alter k f ↔ if k == k' then (f (m.get? k)).isSome = true else k' ∈ m

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ k' ∈ m.alter k f ↔ if (k == k') = true then (f (m.get? k)).isSome = true else k' ∈ m

Tactic:
simp [mem_iff_contains, contains_alter h]

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
lemma toRight_sdiff : (u \ v).toRight = u.toRight \ v.toRight

Proof state:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u \ v).toRight = u.toRight \ v.toRight

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (u \ v).toRight ↔ x ∈ u.toRight \ v.toRight

Proof state:
case h
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (u \ v).toRight ↔ x ∈ u.toRight \ v.toRight

Tactic:
simp

Result:
no goals